[circt-lec] Introduce the circt-lec tool
#3991
Conversation
|
Super cool! Thank you for working this! I tried using circt-lec but I encountered a following build error (on z3-4.11.2). Do you have any idea on this? |
|
Hello @uenoku, Those errors seem to indicate you're missing the Z3 C API includes, which the Z3 C++ API depend on: indeed |
|
This is great! Were there any lessons/issues from trying to formally encode our semantics have been/should be propagated up as issues? That process has a tendency to turn up all sorts of overlooked details in pretty much everything that isn't already built around formal semantics (LLVM IR, ISA behavior, etc.). Anyway having semantics defined enough to pass to a solver has a lot of exciting applications! I've often thought it'd be great to do something like Alive(2) to check our canonicalizers/folders, especially as support for multi-valued logic grows, and also to identify/verify new optimization opportunities. Having our own LEC is awesome! re:Z3 and building, my experience: My distribution doesn't include the cmake bits for This seems like it might be the way to go, especially if we're okay using Z3 in same way/versions as LLVM does (requires > 4.7.1). WDYT? @uenoku if you modify things to use |
That worked, thanks! |
They're not really errors but
I've updated the procedure for locating Z3 to enter |
|
This is great to see! I haven't reviewed in detail yet, but I will try to do so. Taking the optional dependence on Z3 sounds good to me. Eventually, I think it might be nice to try to install smt-switch, so we could use one API for multiple solvers (Z3, cvc5, etc.). I think moving forward with Z3 to start is a good approach, and if we figure out how to install smt-switch, we can refactor this (and other tools using SMT solvers) to use smt-switch later. |
|
This work looks super interesting! Just as an FYI, it looks like changes to CIRCT since this PR was originally created mean that this won't build when merged with the current state of |
frog-in-the-well
force-pushed
the
circt-lec
branch
from
ad83007
to
bdfb142
Compare
|
@TaoBi22 thank you for the notice; I was indeed expecting to have to fix linking when rebasing to main. |
frog-in-the-well
force-pushed
the
circt-lec
branch
from
1a854b8
to
3da27b5
Compare
frog-in-the-well
force-pushed
the
circt-lec
branch
from
1b219c4
to
848301c
Compare
frog-in-the-well
force-pushed
the
circt-lec
branch
from
848301c
to
11392d5
Compare
|
With the latest commits, CI should now avoid building |
Z3 is a state-of-the-art SMT solver widely employed in the development of verification tools. As of now, when an image would install `clang-tidy` or `llvm`, `z3-4.8.7` would be downloaded as well as a dependency. Because this is fairly old version, CI would report errors when building llvm/circt#3991 which I've been trying to merge. I have therefore introduced a script download and install the current latest version of Z3 available. Because the repo's `README` suggests to test the images locally, I also added logic to detect the host machine's architecture and download or compile an appropriate release of CMake and Z3; previously `circt-integration-test` would fail to build on my ARM machine.
I'm actually working on a CIRCT model checking tool at the moment that builds pretty heavily on this work, since there's a lot of overlap in the logic that it doesn't really make sense to duplicate. I was anticipating potentially having to submit a PR to move a lot of this code into the library anyway, so from that angle, it also makes sense to make that move. Being able to put the model checking and LEC code together in the same library would also make it much easier to get equivalence checking on sequential designs up and running at some point in the future. |
frog-in-the-well
force-pushed
the
circt-lec
branch
from
11392d5
to
66b3c89
Compare
frog-in-the-well
force-pushed
the
circt-lec
branch
from
66b3c89
to
0ac16e2
Compare
|
Thanks for the z3 fix @frog-in-the-well! On a branch of my fork, I've moved the bulk of the |
|
@TaoBi22 Great work, please do. |
There was a problem hiding this comment.
@frog-in-the-well seems like some erroneous semicolons will cause CI failure once approved, as can be seen in #4544's CI (though there's another issue there too - the first batch of errors relates to this problem). However, clang-format then expects indentation after each of the macro instances - maybe it's worth not linting those lines?
Indeed -visitBinaryCombOp(ModS, comb.mods, circt::comb::ModSOp &);
+// clang-format off
+visitBinaryCombOp(ModS, comb.mods, circt::comb::ModSOp &)
-visitBinaryCombOp(ModU, comb.modu, circt::comb::ModUOp &);
+visitBinaryCombOp(ModU, comb.modu, circt::comb::ModUOp &)
-visitVariadicCombOp(Mul, comb.mul, circt::comb::MulOp &);
+visitVariadicCombOp(Mul, comb.mul, circt::comb::MulOp &)
+ // clang-format on
-mlir::LogicalResult
-LogicExporter::Visitor::visitComb(circt::comb::MuxOp &op,
- Solver::Circuit *circuit) {
+ mlir::LogicalResult LogicExporter::Visitor::visitComb(
+ circt::comb::MuxOp &op, Solver::Circuit *circuit) {
The reported warnings alone shouldn't cause the CI build to fail, but removing them would compromise on legibility. In case warnings have to be avoided, I could try to hack around the linter's limitations. |
|
@frog-in-the-well sorry, entirely my mistake - somehow misread and thought those were errors! Thanks for catching that, sorry for the false alarm! |
Added logic to conditionally build the tool only when detecting a Z3 installation newer than version 4.8.11. Previous versions do not provide the `sge` and `sgt` operators in the C++ API, which are instead referenced by the cirt-lec codebase and would cause linting and compiling issues. Discussed with @maerhart and @teqdruid.
As reported by @TaoBi22.
Adding only the supported dialects to the registry reduces the dependencies the tool has to be linked with. Suggested by @uenoku and @darthscsi.
Building with the install runpath could cause dependent shared libraries to not be found.
Suggested by @uenoku.
Suggested by @uenoku.
As suggested by @uenoku.
As suggested by @darthscsi.
Replace `LogicExporter::fetchModuleOp` with a `HWInstanceLike::getReferencedModule` call.
Avoid their static construction, as suggested by @darthscsi.
As suggested by @darthscsi.
As suggested by @darthscsi.
As suggested by @darthscsi and discussed with @maerhart, representing `LogicExporter` as a pass was more forced than useful.
As suggested by @darthscsi.
Inline `performVariadicCombOp` and `performBinaryCombOp` macros as suggested by @darthscsi.
For soundness reasons, `comb` operations are no longer assumed to only have binary operators. Suggested by @darthscsi.
Suggested by @darthscsi.
frog-in-the-well
force-pushed
the
circt-lec
branch
from
2a5d0a8
to
c0d1f34
Compare
- Specify `DEBUG_TYPE`s; - handle `Solver` references instead of nullable pointers; - remove superfluous inline specifier; - use auto for excessive temporary values. Suggested by @darthscsi.
- Change `circuits` field to a C-style array; - drop `firstCircuit` parameter from `addCircuit` method; - set statisticsOpt in constructor initialization list; - rephrase destructor as default; - remove empty if block; - `printModel` and `printStatistic` on `outs` stream.
Suggested by @uenoku. Co-authored-by: Hideto Ueno <uenoku.tokotoko@gmail.com>
There was a problem hiding this comment.
To me this looks good to land with all the CI passing. I expect that there are a lot of small things that we'll want to tweak and refactor afterwards, for example @TaoBi22's work on bounded model checks that would love to reuse some of this code as a library.
But just adding this to CIRCT and having it open to be tweaked and worked on by everyone is a fantastic step forward! Love it! 🎉
| // 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 | ||
| } |
There was a problem hiding this comment.
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 🤩
| // Defining persistent output streams such that text will be printed in | ||
| // accordance with the globally set indentation level. | ||
| inline mlir::raw_indented_ostream &dbgs() { | ||
| static auto stream = mlir::raw_indented_ostream(llvm::dbgs()); | ||
| return stream; | ||
| }; | ||
|
|
||
| inline mlir::raw_indented_ostream &errs() { | ||
| static auto stream = mlir::raw_indented_ostream(llvm::errs()); | ||
| return stream; | ||
| }; | ||
|
|
||
| inline mlir::raw_indented_ostream &outs() { | ||
| static auto stream = mlir::raw_indented_ostream(llvm::outs()); | ||
| return stream; | ||
| }; | ||
|
|
||
| /// RAII struct to indent the output streams. | ||
| struct Scope { | ||
| mlir::raw_indented_ostream::DelimitedScope indentDbgs = lec::dbgs().scope(); | ||
| mlir::raw_indented_ostream::DelimitedScope indentErrs = lec::errs().scope(); | ||
| mlir::raw_indented_ostream::DelimitedScope indentOuts = lec::outs().scope(); | ||
| }; |
There was a problem hiding this comment.
I'm curious if this would be something that's worth upstreaming to MLIR at a later point. Seems useful in general.
| class LogicExporter { | ||
| public: | ||
| LogicExporter(llvm::StringRef moduleName, Solver::Circuit *circuit) | ||
| : moduleName(moduleName), circuit(circuit){}; | ||
|
|
||
| /// Initializes the exporting by visiting the builtin module. | ||
| mlir::LogicalResult run(mlir::ModuleOp &module); | ||
|
|
||
| private: | ||
| /// This class provides logic-exporting functions for the implemented | ||
| /// operations, along with a dispatcher to visit the correct handler. | ||
| struct Visitor |
There was a problem hiding this comment.
I like that this exporter is reusable. Depending on the sat problem we're trying to solve, I could see different tools using this LogicExporter to get the main Z3 mapping out of the way, and then have special handling for things like registers (e.g. to handle differences between bounded model checks and inductive proofs).
We might be able to save on some repetition by moving Visitor into the LogicExporter.cpp file and pulling all function bodies into the struct Visitor declaration. Just some nitpicking though, no need to change this PR.
| #define visitVariadicCombOp(OP_NAME, MLIR_NAME, TYPE) \ | ||
| mlir::LogicalResult LogicExporter::Visitor::visitComb( \ | ||
| TYPE op, Solver::Circuit *circuit) { \ | ||
| LLVM_DEBUG(lec::dbgs() << "Visiting " #MLIR_NAME "\n"); \ | ||
| lec::Scope indent; \ | ||
| LLVM_DEBUG(debugOperands(op)); \ | ||
| bool twoState = op.getTwoState(); \ | ||
| REJECT_N_STATE_LOGIC(); \ | ||
| mlir::Value result = op.getResult(); \ | ||
| LLVM_DEBUG(debugOpResult(result)); \ | ||
| circuit->perform##OP_NAME(result, op.getOperands()); \ | ||
| return mlir::success(); \ | ||
| } |
There was a problem hiding this comment.
One way to avoid the macro could be to have just a circuit-perform function that is overloaded for the different ops, and use the type system to switch between them. That still leaves the problem that the visitComb function bodies share a lot of code. You could have a templated function like template <class ConcreteOp> LogicalResult visitVariadicCombOp(ConcreteOp op) that you call from visitComb, and which then contains the common code.
But I think this is definitely something we can tweak and iterate on after this PR has landed, since having all of this available in the codebase is already extremely useful. And people will want to iterate and tweak and improve and extend things anyway 👍
| class Circuit; | ||
| /// Create a new circuit to be compared and return it. | ||
| Circuit *addCircuit(llvm::StringRef name); |
There was a problem hiding this comment.
After this PR lands, we could look into turning this into something like getCircuitA and getCircuitB, since the solver has this Circuit *circuit[2] member that really forces two circuits to be present. Having addCircuit makes it easy to abuse the solver by not having exactly two calls to addCircuit. Just some random thoughts on future refactorings.
| // Parse the command-line options provided by the user. | ||
| cl::ParseCommandLineOptions( | ||
| argc, argv, | ||
| "circt-lec - logical equivalence checker\n\n" | ||
| "\tThis tool compares two input circuit descriptions to determine whether" | ||
| " they are logically equivalent.\n"); |
There was a problem hiding this comment.
Very cool. I love that CIRCT has gotten to a point where we can have a tool print this help output 😎
|
Status? What is the intention on landing? |
|
I think we should just land this as-is so others can take advantage of the Z3 dep and the logic exporter. @frog-in-the-well is that okay with you? |
|
Thank you @uenoku and @fabianschuiki for the approvals. |
|
Thank you very much @frog-in-the-well for all your effort and revisions to get this landed! 🥳 💯 It's fantastic to have a solid starting point for Logical Equivalence Checking in CIRCT 🎉! |
A logical equivalence checking tool for CIRCT.
As of now, it covers some basic
hwoperations and the wholecombdialect, making it suitable for combinational equivalence checking with the caveat of lowering data types likehw.arrayto bitvectors.Z3acts as the logical backend and has been introduced as a build dependency for the tool; that said I think it would merit getting added to CI before merging this PR.Furthermore, regression tests for part of the implemented operations and features have been written. I tried to adhere to the operational semantics as defined in the CIRCT documentation, but errors or omissions might still be present. Specifically, the lack of multi-valued logic support arose during a developer's meeting.
Information about the tool's usage can be found in the README file from the tool's directory.
This has been my Google's Summer of Code project (url).
I want to thank @fabianschuiki and @maerhart for their guidance.