Add `verif.bmc` VerifToSMT lowering #7603

TaoBi22 · 2024-09-16T16:35:40Z

This PR adds a pattern to lower the verif.bmc op into the program to actually perform the check (from the splitting up of #7259 - only the actual tool left after this!), similarly to what circt-lec currently does.

Co-authored-by: Martin Erhart <[email protected]>

TaoBi22 · 2024-09-16T16:37:43Z

lib/Conversion/VerifToSMT/VerifToSMT.cpp

@@ -30,7 +35,8 @@ using namespace hw;
 //===----------------------------------------------------------------------===//

 namespace {
-/// Lower a verif::AssertOp operation with an i1 operand to a smt::AssertOp.
+/// Lower a verif::AssertOp operation with an i1 operand to a smt::AssertOp,
+/// negated to check for unsatisfiability.


Currently verif.assert is lowered directly to smt.assert, whereas we want it negated in this context to check for unsatisfiability. I'm not aware of any verif dialect use cases that mean this negation is undesirable, but let me know if any exist

Sorry for the drive-by comment, I haven't looked into this properly. But won't this change inevitably lead to effectively the same problem as in #5358 ? I.e., any verif.assert(true) will now become smt.assert(false), thus rendering the model unsatisfiable regardless of all other (failing) assertions?

Yeah I ran into a similar issue in btor and opted simply the prune those assertions as they're trivially true, maybe the same should be done here -- or maybe we should just do this in a fold for the verif.assert and verif.assume ops themselves?

Removing such trivial assertions is nice, but I'd probably not do it in a canonicalizer because it makes it harder to keep track of a list of passed assertions to report back to the engineer, etc.
Also, just pruning these trivial ones doesn't make the model checker sound.

Given

assert P1 assert P2 assert P3 // equivalent to assert P1 & P2 & P3

we currently emit

assert !P1 assert !P2 assert !P3 // equivalent to assert !(P1 || P2 || P3)

but we want

assert !(P1 & P2 & P3)

Not sure how other open-source or commercial model checkers deal with that. I see two options

add assertion by assertion "interactively" by checking satisfiability after each added assertion (bad performance-wise unless the solver is really good in caching things, which I don't know enough about)

Combine all assertions into a single one (returning good counter-examples may need some post processing/running additional checks)

I like the approach here of keeping the assert lowering simple. Maybe we can add a separate pass earlier in the pipeline to restructure the circuit for one of the two approaches later on.

Thanks everyone for taking a look, and thanks for catching that @fzi-hielscher!

This is a great point - thanks for the suggestions @maerhart, those sound good to me! I guess the easy interrim fix is to add on an error in this lowering (or a canonicalizer to the BMC op, though to me this seems more of a point in the lowering than the op itself) that requires the BMC op to have only one assertion - that shouldn't really introduce any compromises in functionality as what would have previously been individual assertions can all just be ANDed, but means that we won't unsoundly produce an unsat when there's actually an assertion that can be violated.

I think checking for a single assert in the pass that inserts the verif.bmc operation and emitting an error or at least warning would be a reasonable solution for now. Should be quite easy using an InstanceGraph.

maerhart

Really cool, thanks a lot!

lib/Conversion/VerifToSMT/CMakeLists.txt

lib/Conversion/VerifToSMT/VerifToSMT.cpp

maerhart · 2024-09-17T09:46:43Z

lib/Conversion/VerifToSMT/VerifToSMT.cpp

@@ -30,7 +35,8 @@ using namespace hw;
 //===----------------------------------------------------------------------===//

 namespace {
-/// Lower a verif::AssertOp operation with an i1 operand to a smt::AssertOp.
+/// Lower a verif::AssertOp operation with an i1 operand to a smt::AssertOp,
+/// negated to check for unsatisfiability.


I think checking for a single assert in the pass that inserts the verif.bmc operation and emitting an error or at least warning would be a reasonable solution for now. Should be quite easy using an InstanceGraph.

test/Conversion/VerifToSMT/verif-to-smt.mlir

TaoBi22 · 2024-09-17T16:35:36Z

@maerhart I think that should be all comments addressed - if you could take a quick scan over the added assertion count checker that would be great!

maerhart

Thanks!

maerhart · 2024-09-18T11:54:21Z

lib/Conversion/VerifToSMT/VerifToSMT.cpp

+  matchAndRewrite(verif::BoundedModelCheckingOp op, OpAdaptor adaptor,
+                  ConversionPatternRewriter &rewriter) const override {
+    // Check there is exactly one assertion
+    auto topAssertions = op.getCircuit().getOps<verif::AssertOp>();


You might want to do a walk here, because getOps doesn't visit ops in nested regions (also for the other 2 getOps uses below). On the other hand, we're not really using nested regions at the HW level, so should also be fine as is.

maerhart · 2024-09-18T11:56:43Z

lib/Conversion/VerifToSMT/VerifToSMT.cpp

+    auto topAssertions = op.getCircuit().getOps<verif::AssertOp>();
+    int numAssertions =
+        std::distance(topAssertions.begin(), topAssertions.end());
+    SymbolTable symbolTable(op->getParentOfType<ModuleOp>());


Usually this shouldn't be recomputed for each pattern invocation. It might also be unsafe to iterate of the entire module while the rewriting is in progress.
I'd just instantiate it in runOnOperation and pass it to the pattern to be safe.

maerhart · 2024-09-18T11:57:14Z

lib/Conversion/VerifToSMT/VerifToSMT.cpp

+    SmallVector<mlir::Operation *> worklist;
+    for (auto instance : op.getCircuit().getOps<InstanceOp>()) {
+      worklist.push_back(symbolTable.lookup(instance.getModuleName()));
+    }


Nit: we typically omit curly braces here (and also the two other cases further down) 😉

🤦‍♀️ thanks!

test/Conversion/VerifToSMT/verif-to-smt-errors.mlir

maerhart · 2024-09-18T12:09:32Z

lib/Conversion/VerifToSMT/VerifToSMT.cpp

+    SmallVector<Value> inputDecls;
+    SmallVector<int> clockIndexes;
+    for (auto [curIndex, types] :
+         llvm::enumerate(llvm::zip(oldCircuitInputTy, circuitInputTy))) {


Nit: Enumerate can zip at the same time

Suggested change

llvm::enumerate(llvm::zip(oldCircuitInputTy, circuitInputTy))) {

llvm::enumerate(oldCircuitInputTy, circuitInputTy)) {

TaoBi22 and others added 4 commits September 13, 2024 13:09

Add BMC to SMT lowering

0bdaccc

Co-authored-by: Martin Erhart <[email protected]>

Format & clean-up

80736fc

Remove now-unnecessary assert

8353a4b

Drop error conversions

8a8f912

TaoBi22 requested a review from maerhart September 16, 2024 16:35

TaoBi22 commented Sep 16, 2024

View reviewed changes

maerhart approved these changes Sep 17, 2024

View reviewed changes

maerhart reviewed Sep 17, 2024

View reviewed changes

test/Conversion/VerifToSMT/verif-to-smt.mlir Show resolved Hide resolved

TaoBi22 added 3 commits September 17, 2024 11:11

Address nits & add missing Func dialect dep

1d0dcec

Add lowering tests for assert & assume ops

ef796fa

Error on multiple assertions

b6740f8

maerhart approved these changes Sep 18, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add `verif.bmc` VerifToSMT lowering #7603

Add `verif.bmc` VerifToSMT lowering #7603

TaoBi22 commented Sep 16, 2024

TaoBi22 Sep 16, 2024

fzi-hielscher Sep 16, 2024

dobios Sep 16, 2024 •

edited

Loading

maerhart Sep 17, 2024

TaoBi22 Sep 17, 2024

maerhart Sep 17, 2024

maerhart left a comment

maerhart Sep 17, 2024

TaoBi22 commented Sep 17, 2024 •

edited

Loading

maerhart left a comment

maerhart Sep 18, 2024

maerhart Sep 18, 2024

maerhart Sep 18, 2024

TaoBi22 Sep 18, 2024

maerhart Sep 18, 2024

TaoBi22 Sep 18, 2024

	llvm::enumerate(llvm::zip(oldCircuitInputTy, circuitInputTy))) {
	llvm::enumerate(oldCircuitInputTy, circuitInputTy)) {

Add verif.bmc VerifToSMT lowering #7603

Are you sure you want to change the base?

Add verif.bmc VerifToSMT lowering #7603

Conversation

TaoBi22 commented Sep 16, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dobios Sep 16, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

maerhart left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

TaoBi22 commented Sep 17, 2024 • edited Loading

maerhart left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Add `verif.bmc` VerifToSMT lowering #7603

Add `verif.bmc` VerifToSMT lowering #7603

dobios Sep 16, 2024 •

edited

Loading

TaoBi22 commented Sep 17, 2024 •

edited

Loading