Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[circt-lec] Introduce the circt-lec tool #3991

Merged
merged 39 commits into from
May 1, 2023
Merged

[circt-lec] Introduce the circt-lec tool #3991

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
39 commits
Select commit Hold shift + click to select a range
f52dd6e
[circt-lec] Introduce the `circt-lec` tool
frog-in-the-well Sep 24, 2022
d3ca95a
Update Z3 configuration procedure for building
frog-in-the-well Sep 29, 2022
ca36d01
Fix formatting issues
frog-in-the-well Sep 29, 2022
74ae51b
Fix tests requirements and status
frog-in-the-well Sep 30, 2022
ae04de2
Modify `Solver::symbolTable` implementation
frog-in-the-well Sep 30, 2022
743b41d
Refactor operation dispatching
frog-in-the-well Oct 20, 2022
b295bac
Respect namespace consistency
frog-in-the-well Oct 20, 2022
d926e54
Restore main branch compatibility
frog-in-the-well Oct 29, 2022
63f2e12
Comply with `clang-tidy`
frog-in-the-well Oct 29, 2022
7697030
Fix `clang-tidy` errors
frog-in-the-well Nov 17, 2022
79d5d1d
Adjust build procedure
frog-in-the-well Nov 17, 2022
75a3ae0
Use CIRCT-specific bug message
frog-in-the-well Nov 17, 2022
16fd18d
CIRCT integrations tests depend on `circt-lec`
frog-in-the-well Nov 18, 2022
3087f81
Add missing file header
frog-in-the-well Nov 25, 2022
6e36bb1
Report Z3 details when self-compiled
frog-in-the-well Nov 25, 2022
3626a41
Fix integration tests dependency
frog-in-the-well Nov 25, 2022
c762ee1
Remove superfluous semicolon
frog-in-the-well Nov 25, 2022
8f4ac68
Correct the runpath when linking shared libraries
frog-in-the-well Nov 25, 2022
2b5d3db
Avoid building `circt-lec` if the detected `Z3` version is outdated
frog-in-the-well Dec 11, 2022
dbcfb50
Rephrase the README's `Building` section
frog-in-the-well Dec 11, 2022
7fdcec5
Fix package version checking
frog-in-the-well Jan 12, 2023
d80f9d7
Minimize dependencies
frog-in-the-well Feb 24, 2023
8515594
Fix shared library linking
frog-in-the-well Feb 24, 2023
d6cc972
Pass wrapper objects by value
frog-in-the-well Feb 24, 2023
0bb2973
Simplify printing block arguments
frog-in-the-well Feb 24, 2023
993c834
Refactor `builtin.module` visiting logic
frog-in-the-well Feb 26, 2023
e52f227
Reject on n-state logic comparisons
frog-in-the-well Feb 26, 2023
4ce5155
Revamp `hw.instance` visitor
frog-in-the-well Feb 26, 2023
7e3d7be
Initialize output streams on first use
frog-in-the-well Mar 11, 2023
351eaed
Remove `VERBOSE` macro
frog-in-the-well Mar 11, 2023
4391f24
Pass command-line options directly
frog-in-the-well Mar 11, 2023
97a8c2f
`LogicExporter` is no longer a pass
frog-in-the-well Mar 11, 2023
3852499
Retain `DEBUG_TYPE` definitions
frog-in-the-well Mar 11, 2023
4921d85
Expand `Circuit` operation macros
frog-in-the-well Mar 17, 2023
6d4869c
Explicitly reject on unimplemented n-state logic
frog-in-the-well Mar 17, 2023
c0d1f34
Encapsulate and expand `INDENT` macro.
frog-in-the-well Mar 28, 2023
41dd724
Various code style improvements
frog-in-the-well Mar 29, 2023
96f5fee
`Solver` class improvements
frog-in-the-well Mar 30, 2023
20866dc
Remove unnecessary const reference
frog-in-the-well Apr 3, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 41 additions & 1 deletion CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -390,7 +390,7 @@ else()

string(REGEX MATCH "Icarus Verilog version (([0-9]+)\.([0-9]+)) \.*"
MATCH ${IVERILOG_VERSION})

if (${CMAKE_MATCH_1} LESS 11.0)
message(FATAL_ERROR "CIRCT only supports Icarus Verilog version 11.0 and up. \
Found version: ${CMAKE_MATCH_1}. You can disable \
Expand Down Expand Up @@ -472,6 +472,46 @@ endif()

llvm_canonicalize_cmake_booleans(CIRCT_LLHD_SIM_ENABLED)

#-------------------------------------------------------------------------------
# circt-lec Configuration
#-------------------------------------------------------------------------------
# If circt-lec hasn't been explicitly disabled, find it.
option(CIRCT_LEC_DISABLE "Disable the Logical Equivalence Checker" OFF)
if(CIRCT_LEC_DISABLE)
message(STATUS "Disabling circt-lec")
else()
if(Z3_DIR)
# Search and load the package configuration file in the specified directory.
find_package(Z3 CONFIG REQUIRED PATHS ${Z3_DIR} NO_DEFAULT_PATH)
if(Z3_FOUND)
# Report the found library location and version
# similarly to LLVM's `FindZ3` CMake module.
get_target_property(Z3_LIB_LOCATION z3::libz3 IMPORTED_LOCATION_DEBUG)
message(STATUS "Found Z3: ${Z3_LIB_LOCATION} (found version \"${Z3_VERSION_STRING}\")")
endif()
# Link against the reported library and include locations.
list(APPEND CIRCT_LEC_LIBS ${Z3_LIBRARIES})
list(APPEND CIRCT_LEC_INCLUDES ${Z3_CXX_INCLUDE_DIRS})
else()
# Attempt initialising Z3 according to LLVM's `FindZ3` CMake module.
find_package(Z3)
# Link against the reported library and include locations.
list(APPEND CIRCT_LEC_LIBS ${Z3_LIBRARIES})
list(APPEND CIRCT_LEC_INCLUDES ${Z3_INCLUDE_DIR})
endif()

if(Z3_FOUND)
SET(CIRCT_LEC_Z3_VER 4.8.11)
if(Z3_VERSION_STRING VERSION_LESS ${CIRCT_LEC_Z3_VER})
message(WARNING "Cannot build circt-lec with outdated Z3 version ${Z3_VERSION_STRING}, requires ${CIRCT_LEC_Z3_VER}.")
else()
message(STATUS "Z3 identified as a logical backend.")
# Signal to proceed building circt-lec.
set(CIRCT_LEC_ENABLED ON)
endif()
endif()
endif()

#-------------------------------------------------------------------------------
# Python Configuration
#-------------------------------------------------------------------------------
Expand Down
5 changes: 5 additions & 0 deletions integration_test/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,11 @@ if (TARGET EsiCosimDpiServer)
set(ESI_COSIM_PATH ${ESI_COSIM_LIB_DIR}/libEsiCosimDpiServer.so)
endif()

# Enable circt-lec tests if it is built.
if(CIRCT_LEC_ENABLED)
list(APPEND CIRCT_INTEGRATION_TEST_DEPENDS circt-lec)
endif()

set(CIRCT_INTEGRATION_TIMEOUT 60) # Set a 60s timeout on individual tests.
configure_lit_site_cfg(
${CMAKE_CURRENT_SOURCE_DIR}/lit.site.cfg.py.in
Expand Down
10 changes: 10 additions & 0 deletions integration_test/circt-lec/builtin.mlir
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
// These tests will be only enabled if circt-lec is built.
// REQUIRES: circt-lec

// builtin.module implementation
// RUN: circt-lec %s -v=false | FileCheck %s --check-prefix=BUILTIN_MODULE
// BUILTIN_MODULE: c1 == c2

hw.module @basic(%in: i1) -> (out: i1) {
hw.output %in : i1
}
254 changes: 254 additions & 0 deletions integration_test/circt-lec/comb.mlir
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,254 @@
// These tests will be only enabled if circt-lec is built.
// REQUIRES: circt-lec

hw.module @basic(%in: i1) -> (out: i1) {
hw.output %in : i1
}

hw.module @not(%in: i1) -> (out: i1) {
%true = hw.constant true
%out = comb.xor bin %in, %true : i1
hw.output %out : i1
}

// comb.add
// RUN: circt-lec %s -c1=adder -c2=completeAdder -v=false | FileCheck %s --check-prefix=COMB_ADD
// COMB_ADD: c1 == c2

hw.module @adder(%in1: i2, %in2: i2) -> (out: i2) {
%sum = comb.add bin %in1, %in2 : i2
hw.output %sum : i2
}

hw.module @halfAdder(%in1: i1, %in2: i1) -> (carry: i1, sum: i1) {
%sum = comb.xor bin %in1, %in2 : i1
%carry = comb.and bin %in1, %in2 : i1
hw.output %carry, %sum: i1, i1
}

hw.module @completeAdder(%in1: i2, %in2 : i2) -> (out: i2) {
%in1_0 = comb.extract %in1 from 0 : (i2) -> i1
%in1_1 = comb.extract %in1 from 1 : (i2) -> i1
%in2_0 = comb.extract %in2 from 0 : (i2) -> i1
%in2_1 = comb.extract %in2 from 1 : (i2) -> i1
%c1, %s1 = hw.instance "h1" @halfAdder(in1: %in1_0: i1, in2: %in2_0: i1) -> (carry: i1, sum: i1)
%c2, %s2 = hw.instance "h2" @halfAdder(in1: %in1_1: i1, in2: %in2_1: i1) -> (carry: i1, sum: i1)
%c3, %s3 = hw.instance "h3" @halfAdder(in1: %s2: i1, in2: %c1: i1) -> (carry: i1, sum: i1)
%fullsum = comb.concat %s3, %s1 : i1, i1
hw.output %fullsum : i2
}

// comb.and
// RUN: circt-lec %s -c1=and -c2=decomposedAnd -v=false | FileCheck %s --check-prefix=COMB_AND
frog-in-the-well marked this conversation as resolved.
Show resolved Hide resolved
// COMB_AND: c1 == c2

hw.module @and(%in1: i1, %in2: i1) -> (out: i1) {
%out = comb.and bin %in1, %in2 : i1
hw.output %out : i1
}

hw.module @decomposedAnd(%in1: i1, %in2: i1) -> (out: i1) {
%not_in1 = hw.instance "n_in1" @not(in: %in1: i1) -> (out: i1)
%not_in2 = hw.instance "n_in2" @not(in: %in2: i1) -> (out: i1)
%not_and = comb.or bin %not_in1, %not_in2 : i1
%and = hw.instance "and" @not(in: %not_and: i1) -> (out: i1)
hw.output %and : i1
}

// comb.concat
// TODO

// comb.divs
// TODO

// comb.divu
// TODO

// comb.extract
// TODO

// comb.icmp
// TODO

// comb.mods
// TODO

// comb.modu
// TODO

// comb.mul
// RUN: circt-lec %s -c1=mulBy2 -c2=addTwice -v=false | FileCheck %s --check-prefix=COMB_MUL
// COMB_MUL: c1 == c2

hw.module @mulBy2(%in: i2) -> (out: i2) {
%two = hw.constant 2 : i2
%res = comb.mul bin %in, %two : i2
hw.output %res : i2
}

hw.module @addTwice(%in: i2) -> (out: i2) {
%res = comb.add bin %in, %in : i2
hw.output %res : i2
}
Comment on lines +79 to +92
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's very cool that we can have these kinds of self-contained tests where we just logically compare two things to each other. Very exciting. I could totally see us use this pattern to verify canonicalizations and folders which aren't supposed to functionally change the circuit 🤩


// comb.mux
// RUN: circt-lec %s -c1=mux -c2=decomposedMux -v=false | FileCheck %s --check-prefix=COMB_MUX
// COMB_MUX: c1 == c2

hw.module @mux(%cond: i1, %tvalue: i8, %fvalue: i8) -> (out: i8) {
%res = comb.mux bin %cond, %tvalue, %fvalue : i8
hw.output %res : i8
}

hw.module @decomposedMux(%cond: i1, %tvalue: i8, %fvalue: i8) -> (out: i8) {
%cond_bar = hw.instance "n" @not(in: %cond: i1) -> (out: i1)
%lead_0 = hw.constant 0 : i7
%c_t = comb.concat %lead_0, %cond : i7, i1
%c_f = comb.concat %lead_0, %cond_bar : i7, i1
%t = comb.mul bin %tvalue, %c_t : i8
%f = comb.mul bin %fvalue, %c_f : i8
%res = comb.add bin %t, %f : i8
hw.output %res : i8
}

// comb.or
// RUN: circt-lec %s -c1=or -c2=decomposedOr -v=false | FileCheck %s --check-prefix=COMB_OR
// COMB_OR: c1 == c2

hw.module @or(%in1: i1, %in2: i1) -> (out: i1) {
%out = comb.or bin %in1, %in2 : i1
hw.output %out : i1
}

hw.module @decomposedOr(%in1: i1, %in2: i1) -> (out: i1) {
%not_in1 = hw.instance "n_in1" @not(in: %in1: i1) -> (out: i1)
%not_in2 = hw.instance "n_in2" @not(in: %in2: i1) -> (out: i1)
%not_or = comb.and bin %not_in1, %not_in2 : i1
%or = hw.instance "or" @not(in: %not_or: i1) -> (out: i1)
hw.output %or : i1
}

// comb.parity
// RUN: circt-lec %s -c1=parity -c2=decomposedParity -v=false | FileCheck %s --check-prefix=COMB_PARITY
// COMB_PARITY: c1 == c2

hw.module @parity(%in: i8) -> (out: i1) {
%res = comb.parity bin %in : i8
hw.output %res : i1
}

hw.module @decomposedParity(%in: i8) -> (out: i1) {
%b0 = comb.extract %in from 0 : (i8) -> i1
%b1 = comb.extract %in from 1 : (i8) -> i1
%b2 = comb.extract %in from 2 : (i8) -> i1
%b3 = comb.extract %in from 3 : (i8) -> i1
%b4 = comb.extract %in from 4 : (i8) -> i1
%b5 = comb.extract %in from 5 : (i8) -> i1
%b6 = comb.extract %in from 6 : (i8) -> i1
%b7 = comb.extract %in from 7 : (i8) -> i1
%res = comb.xor bin %b0, %b1, %b2, %b3, %b4, %b5, %b6, %b7 : i1
hw.output %res : i1
}

// comb.replicate
// RUN: circt-lec %s -c1=replicate -c2=decomposedReplicate -v=false | FileCheck %s --check-prefix=COMB_REPLICATE
// COMB_REPLICATE: c1 == c2

hw.module @replicate(%in: i2) -> (out: i8) {
%res = comb.replicate %in : (i2) -> i8
hw.output %res : i8
}

hw.module @decomposedReplicate(%in: i2) -> (out: i8) {
%res = comb.concat %in, %in, %in, %in : i2, i2, i2, i2
hw.output %res : i8
}

// comb.shl
// RUN: circt-lec %s -c1=shl -c2=decomposedShl -v=false | FileCheck %s --check-prefix=COMB_SHL
// COMB_SHL: c1 == c2

hw.module @shl(%in1: i2, %in2: i2) -> (out: i2) {
%res = comb.shl bin %in1, %in2 : i2
hw.output %res : i2
}

hw.module @decomposedShl(%in1: i2, %in2: i2) -> (out: i2) {
%zero = hw.constant 0 : i2
%one = hw.constant 1 : i2
%two = hw.constant 2 : i2
// first possible shift
%cond1 = comb.icmp bin ugt %in2, %zero : i2
%mul1 = comb.mux bin %cond1, %two, %one : i2
%shl1 = comb.mul bin %in1, %mul1 : i2
// avoid subtraction underflow
%cond1_1 = comb.icmp bin eq %in2, %zero : i2
%sub1 = comb.mux bin %cond1_1, %zero, %one : i2
%in2_2 = comb.sub bin %in2, %sub1 : i2
// second possible shift
%cond2 = comb.icmp bin ugt %in2_2, %zero : i2
%mul2 = comb.mux bin %cond2, %two, %one : i2
%shl2 = comb.mul bin %shl1, %mul2 : i2
hw.output %shl2 : i2
}

// comb.shrs
// TODO

// comb.shru
// TODO

// comb.sub
// RUN: circt-lec %s -c1=subtractor -c2=completeSubtractor -v=false | FileCheck %s --check-prefix=COMB_SUB
// COMB_SUB: c1 == c2

hw.module @subtractor(%in1: i8, %in2: i8) -> (out: i8) {
%diff = comb.sub bin %in1, %in2 : i8
hw.output %diff : i8
}

hw.module @halfSubtractor(%in1: i1, %in2: i1) -> (borrow: i1, diff: i1) {
%diff = comb.xor bin %in1, %in2 : i1
%not_in1 = hw.instance "n_in1" @not(in: %in1: i1) -> (out: i1)
%borrow = comb.and bin %not_in1, %in2 : i1
hw.output %borrow, %diff: i1, i1
}

hw.module @fullSubtractor(%in1: i1, %in2: i1, %b_in: i1) -> (borrow: i1, diff: i1) {
%b1, %d1 = hw.instance "s1" @halfSubtractor(in1: %in1: i1, in2: %in2: i1) -> (borrow: i1, diff: i1)
%b2, %d_out = hw.instance "s2" @halfSubtractor(in1: %d1: i1, in2: %b_in: i1) -> (borrow: i1, diff: i1)
%b_out = comb.or bin %b1, %b2 : i1
hw.output %b_out, %d_out: i1, i1
}

hw.module @completeSubtractor(%in1: i8, %in2 : i8) -> (out: i8) {
%in1_0 = comb.extract %in1 from 0 : (i8) -> i1
%in1_1 = comb.extract %in1 from 1 : (i8) -> i1
%in1_2 = comb.extract %in1 from 2 : (i8) -> i1
%in1_3 = comb.extract %in1 from 3 : (i8) -> i1
%in1_4 = comb.extract %in1 from 4 : (i8) -> i1
%in1_5 = comb.extract %in1 from 5 : (i8) -> i1
%in1_6 = comb.extract %in1 from 6 : (i8) -> i1
%in1_7 = comb.extract %in1 from 7 : (i8) -> i1
%in2_0 = comb.extract %in2 from 0 : (i8) -> i1
%in2_1 = comb.extract %in2 from 1 : (i8) -> i1
%in2_2 = comb.extract %in2 from 2 : (i8) -> i1
%in2_3 = comb.extract %in2 from 3 : (i8) -> i1
%in2_4 = comb.extract %in2 from 4 : (i8) -> i1
%in2_5 = comb.extract %in2 from 5 : (i8) -> i1
%in2_6 = comb.extract %in2 from 6 : (i8) -> i1
%in2_7 = comb.extract %in2 from 7 : (i8) -> i1
%b0, %d0 = hw.instance "s0" @halfSubtractor(in1: %in1_0: i1, in2: %in2_0: i1) -> (borrow: i1, diff: i1)
%b1, %d1 = hw.instance "s1" @fullSubtractor(in1: %in1_1: i1, in2: %in2_1: i1, b_in: %b0: i1) -> (borrow: i1, diff: i1)
%b2, %d2 = hw.instance "s2" @fullSubtractor(in1: %in1_2: i1, in2: %in2_2: i1, b_in: %b1: i1) -> (borrow: i1, diff: i1)
%b3, %d3 = hw.instance "s3" @fullSubtractor(in1: %in1_3: i1, in2: %in2_3: i1, b_in: %b2: i1) -> (borrow: i1, diff: i1)
%b4, %d4 = hw.instance "s4" @fullSubtractor(in1: %in1_4: i1, in2: %in2_4: i1, b_in: %b3: i1) -> (borrow: i1, diff: i1)
%b5, %d5 = hw.instance "s5" @fullSubtractor(in1: %in1_5: i1, in2: %in2_5: i1, b_in: %b4: i1) -> (borrow: i1, diff: i1)
%b6, %d6 = hw.instance "s6" @fullSubtractor(in1: %in1_6: i1, in2: %in2_6: i1, b_in: %b5: i1) -> (borrow: i1, diff: i1)
%b7, %d7 = hw.instance "s7" @fullSubtractor(in1: %in1_7: i1, in2: %in2_7: i1, b_in: %b6: i1) -> (borrow: i1, diff: i1)
%diff = comb.concat %d7, %d6, %d5, %d4, %d3, %d2, %d1, %d0 : i1, i1, i1, i1, i1, i1, i1, i1
hw.output %diff : i8
}

// comb.xor
// TODO
18 changes: 18 additions & 0 deletions integration_test/circt-lec/commandline.mlir
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// These tests will be only enabled if circt-lec is built.
// REQUIRES: circt-lec

// RUN: split-file %s %t

// Passing two input files
// RUN: circt-lec %t/first.mlir %t/second.mlir -v=false | FileCheck %s
// CHECK: c1 == c2

//--- first.mlir
hw.module @basic(%in: i1) -> (out: i1) {
hw.output %in : i1
}

//--- second.mlir
hw.module @basic(%in: i1) -> (out: i1) {
hw.output %in : i1
}
42 changes: 42 additions & 0 deletions integration_test/circt-lec/hw.mlir
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
// These tests will be only enabled if circt-lec is built.
// REQUIRES: circt-lec

hw.module @basic(%in: i1) -> (out: i1) {
hw.output %in : i1
}

// hw.constant
// RUN: circt-lec %s -c1=basic -c2=notnot -v=false | FileCheck %s --check-prefix=HW_CONSTANT
// HW_CONSTANT: c1 == c2

hw.module @onePlusTwo() -> (out: i2) {
%one = hw.constant 1 : i2
%two = hw.constant 2 : i2
%three = comb.add bin %one, %two : i2
hw.output %three : i2
}

hw.module @three() -> (out: i2) {
%three = hw.constant 3 : i2
hw.output %three : i2
}

// hw.instance
// RUN: circt-lec %s -c1=basic -c2=notnot -v=false | FileCheck %s --check-prefix=HW_INSTANCE
// HW_INSTANCE: c1 == c2

hw.module @not(%in: i1) -> (out: i1) {
%true = hw.constant true
%out = comb.xor bin %in, %true : i1
hw.output %out : i1
}

hw.module @notnot(%in: i1) -> (out: i1) {
%n = hw.instance "n" @not(in: %in: i1) -> (out: i1)
%nn = hw.instance "nn" @not(in: %n: i1) -> (out: i1)
hw.output %nn : i1
}

// hw.output
// RUN: circt-lec %s -c1=basic -c2=basic -v=false | FileCheck %s --check-prefix=HW_OUTPUT
// HW_OUTPUT: c1 == c2
Loading