From 781ffa505aa999ed896651d5aa88ea76065f07d9 Mon Sep 17 00:00:00 2001 From: leizaf <45155667+leizaf@users.noreply.github.com> Date: Sat, 4 Jul 2026 22:04:39 -0700 Subject: [PATCH] [VerifToSMT] Keep assumptions asserted across BMC timesteps --- integration_test/circt-bmc/assumptions.mlir | 43 ++++++++++ integration_test/circt-bmc/split-asserts.mlir | 4 +- lib/Conversion/VerifToSMT/VerifToSMT.cpp | 81 ++++++++++++++++--- .../VerifToSMT/verif-to-smt-errors.mlir | 31 ++++--- test/Conversion/VerifToSMT/verif-to-smt.mlir | 6 +- 5 files changed, 142 insertions(+), 23 deletions(-) create mode 100644 integration_test/circt-bmc/assumptions.mlir diff --git a/integration_test/circt-bmc/assumptions.mlir b/integration_test/circt-bmc/assumptions.mlir new file mode 100644 index 000000000000..54e4783d5699 --- /dev/null +++ b/integration_test/circt-bmc/assumptions.mlir @@ -0,0 +1,43 @@ +// REQUIRES: libz3 +// REQUIRES: circt-bmc-jit + +// Register r starts at 1 and samples input in; the assumption forces in == 1, +// so r can never become 0. Assumptions must keep holding for past timesteps +// when the solver checks later ones; if they are dropped along with the +// per-step assertions, this reports a spurious violation. +// RUN: circt-bmc %s -b 10 --module AssumeDrop --shared-libs=%libz3 | FileCheck %s --check-prefix=ASSUMEDROP +// ASSUMEDROP: Bound reached with no violations! +hw.module @AssumeDrop(in %clk: !seq.clock, in %in: i1) { + %init = seq.initial () { + %c1 = hw.constant true + seq.yield %c1 : i1 + } : () -> !seq.immutable + %r = seq.compreg %in, %clk initial %init : i1 + verif.assume %in : i1 + verif.assert %r : i1 +} + +// Same design without the assumption: r becomes 0 one cycle after in == 0. +// RUN: circt-bmc %s -b 10 --module Violation --shared-libs=%libz3 | FileCheck %s --check-prefix=VIOLATION +// VIOLATION: Assertion can be violated! +hw.module @Violation(in %clk: !seq.clock, in %in: i1) { + %init = seq.initial () { + %c1 = hw.constant true + seq.yield %c1 : i1 + } : () -> !seq.immutable + %r = seq.compreg %in, %clk initial %init : i1 + verif.assert %r : i1 +} + +// Same design with the input hardwired to 1 instead of assumed. +// RUN: circt-bmc %s -b 10 --module Control --shared-libs=%libz3 | FileCheck %s --check-prefix=CONTROL +// CONTROL: Bound reached with no violations! +hw.module @Control(in %clk: !seq.clock) { + %c1 = hw.constant true + %init = seq.initial () { + %c1i = hw.constant true + seq.yield %c1i : i1 + } : () -> !seq.immutable + %r = seq.compreg %c1, %clk initial %init : i1 + verif.assert %r : i1 +} diff --git a/integration_test/circt-bmc/split-asserts.mlir b/integration_test/circt-bmc/split-asserts.mlir index 5ba647cda080..4e8b91da53fb 100644 --- a/integration_test/circt-bmc/split-asserts.mlir +++ b/integration_test/circt-bmc/split-asserts.mlir @@ -1,5 +1,7 @@ +// Without flattening, the asserts stay inside instantiated modules, where +// they cannot be scoped correctly; they are rejected rather than mis-scoped. // RUN: not circt-bmc %s -b 10 --module ModuleAsserts --shared-libs=%libz3 --flatten-modules=false 2>&1 | FileCheck %s -// CHECK: error: bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions +// CHECK: error: assertions inside instantiated modules or called functions are not supported - inline them into the top module first (e.g. with --flatten-modules) hw.module @OneAssert(in %in: i1) { verif.assert %in : i1 diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp index a557ab0f0ca6..ef12c28fe6c2 100644 --- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp +++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp @@ -70,6 +70,28 @@ static void attachDebugVariables( } } +/// Temporary markers used to scope property assertions separately from +/// assumptions after conversion. They are only ever attached to ops inside +/// the circuit scope of a verif.bmc op and are consumed (and removed) by this +/// pass before it finishes; conversions outside BMC circuits are untouched. +static constexpr StringLiteral kPropertyAttr = "verif.bmc_property"; +static constexpr StringLiteral kCircuitAttr = "verif.bmc_circuit"; + +/// Returns true if the op lives in the circuit scope of a verif.bmc op: +/// either still inside the op's circuit region, or inside the circuit +/// function the BMC conversion split that region into. +static bool isInBMCCircuit(Operation *op) { + for (Region *region = op->getParentRegion(); region; + region = region->getParentOp()->getParentRegion()) { + Operation *parent = region->getParentOp(); + if (auto bmcOp = dyn_cast(parent)) + return region == &bmcOp.getCircuit(); + if (auto funcOp = dyn_cast(parent)) + return funcOp->hasAttr(kCircuitAttr); + } + return false; +} + /// Lower a verif::AssertOp operation with an i1 operand to a smt::AssertOp, /// negated to check for unsatisfiability. struct VerifAssertOpConversion : OpConversionPattern { @@ -78,11 +100,14 @@ struct VerifAssertOpConversion : OpConversionPattern { LogicalResult matchAndRewrite(verif::AssertOp op, OpAdaptor adaptor, ConversionPatternRewriter &rewriter) const override { + bool isProperty = isInBMCCircuit(op); Value cond = typeConverter->materializeTargetConversion( rewriter, op.getLoc(), smt::BoolType::get(getContext()), adaptor.getProperty()); Value notCond = smt::NotOp::create(rewriter, op.getLoc(), cond); - rewriter.replaceOpWithNewOp(op, notCond); + auto assertOp = rewriter.replaceOpWithNewOp(op, notCond); + if (isProperty) + assertOp->setAttr(kPropertyAttr, rewriter.getUnitAttr()); return success(); } }; @@ -461,6 +486,7 @@ struct VerifBoundedModelCheckingOpConversion loopFuncOp.end()); circuitFuncOp = func::FuncOp::create( rewriter, loc, names.newName("bmc_circuit"), circuitFuncTy); + circuitFuncOp->setAttr(kCircuitAttr, rewriter.getUnitAttr()); rewriter.inlineRegionBefore(op.getCircuit(), circuitFuncOp.getFunctionBody(), circuitFuncOp.end()); @@ -487,9 +513,6 @@ struct VerifBoundedModelCheckingOpConversion ValueRange initVals = func::CallOp::create(rewriter, loc, initFuncOp)->getResults(); - // Initial push - smt::PushOp::create(rewriter, loc, 1); - // InputDecls order should be // // Get list of clock indexes in circuit args @@ -560,10 +583,6 @@ struct VerifBoundedModelCheckingOpConversion builder, loc, oldCircuitInputTy, iterArgs.take_front(circuitFuncOp.getNumArguments()), debugNames); - // Drop existing assertions - smt::PopOp::create(builder, loc, 1); - smt::PushOp::create(builder, loc, 1); - // Execute the circuit ValueRange circuitCallOuts = func::CallOp::create( @@ -626,6 +645,11 @@ struct VerifBoundedModelCheckingOpConversion // If we created an IfOp, make sure we start inserting after it again builder.restoreInsertionPoint(insideForPoint); + // Discard this step's property assertions (scoped by the push at + // the end of the circuit function); assumptions were asserted + // before that push and persist across steps. + smt::PopOp::create(builder, loc, 1); + // Call loop func to update clock & state arg values SmallVector loopCallInputs; // Fetch clock values to feed to loop @@ -800,21 +824,35 @@ void ConvertVerifToSMTPass::runOnOperation() { if (auto func = dyn_cast(curOp)) worklist.push_back(symbolTable.lookup(func.getCallee())); }); + // Assertions inside instantiated modules or called functions + // convert inside the callee's body, outside the circuit function's + // per-step property scope: their negated conditions would be + // asserted permanently and mask later violations (a silent false + // pass). Reject them instead. Assumptions are fine: persisting is + // exactly the lifetime they need. // TODO: probably negligible compared to actual model checking time // but cacheing the assertion count of modules would speed this up + int numNestedAssertions = 0; while (!worklist.empty()) { auto *module = worklist.pop_back_val(); module->walk([&](Operation *curOp) { if (isa(curOp)) - numAssertions++; + numNestedAssertions++; if (auto inst = dyn_cast(curOp)) worklist.push_back(symbolTable.lookup(inst.getModuleName())); if (auto func = dyn_cast(curOp)) worklist.push_back(symbolTable.lookup(func.getCallee())); }); - if (numAssertions > 1) + if (numNestedAssertions > 0) break; } + if (numNestedAssertions > 0) { + op->emitError( + "assertions inside instantiated modules or called functions " + "are not supported - inline them into the top module first " + "(e.g. with --flatten-modules)"); + return WalkResult::interrupt(); + } if (numAssertions == 0) { op->emitWarning("no property provided to check in module - will " "trivially find no violations."); @@ -848,4 +886,27 @@ void ConvertVerifToSMTPass::runOnOperation() { if (failed(mlir::applyPartialConversion(getOperation(), target, std::move(patterns)))) return signalPassFailure(); + + // Sink property assertions in each BMC circuit function past a push, so the + // caller's pop after smt.check discards only them; assumptions and + // definitions above the push persist across timesteps. Property markers are + // only ever attached inside circuit scopes, so no other functions need + // visiting. + for (auto funcOp : getOperation().getOps()) { + if (!funcOp->hasAttr(kCircuitAttr)) + continue; + funcOp->removeAttr(kCircuitAttr); + SmallVector properties; + funcOp.walk([&](smt::AssertOp assertOp) { + if (assertOp->hasAttr(kPropertyAttr)) { + assertOp->removeAttr(kPropertyAttr); + properties.push_back(assertOp); + } + }); + Operation *terminator = funcOp.getBody().front().getTerminator(); + OpBuilder builder(terminator); + smt::PushOp::create(builder, funcOp.getLoc(), 1); + for (Operation *property : properties) + property->moveBefore(terminator); + } } diff --git a/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir b/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir index a97ad3249372..853172d9349c 100644 --- a/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir +++ b/test/Conversion/VerifToSMT/verif-to-smt-errors.mlir @@ -38,8 +38,11 @@ func.func @multiple_assertions_bmc() -> (i1) { // ----- -func.func @multiple_asserting_modules_bmc() -> (i1) { - // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} +// Asserts inside instantiated modules are rejected: they would convert +// inside the callee, outside the per-step property scope, and their negated +// conditions would be asserted permanently, masking later violations. +func.func @nested_asserts_via_instances() -> (i1) { + // expected-error @below {{assertions inside instantiated modules or called functions are not supported - inline them into the top module first (e.g. with --flatten-modules)}} %bmc = verif.bmc bound 10 num_regs 0 initial_values [] init {} loop {} @@ -59,8 +62,9 @@ hw.module @OneAssertion(in %x: i1) { // ----- -func.func @multiple_asserting_funcs_bmc() -> (i1) { - // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} +// Asserts reachable through func.call are rejected as well. +func.func @nested_asserts_via_calls() -> (i1) { + // expected-error @below {{assertions inside instantiated modules or called functions are not supported - inline them into the top module first (e.g. with --flatten-modules)}} %bmc = verif.bmc bound 10 num_regs 0 initial_values [] init {} loop {} @@ -100,9 +104,12 @@ hw.module @empty() { // ----- -// Check that we don't see an error when there's one nested assertion +// Even a single nested assert is rejected; assumptions in callees are fine +// (they persist, which is the lifetime assumptions need), but a permanently +// asserted negated property would mask later violations. func.func @one_nested_assertion() -> (i1) { + // expected-error @below {{assertions inside instantiated modules or called functions are not supported - inline them into the top module first (e.g. with --flatten-modules)}} %bmc = verif.bmc bound 10 num_regs 0 initial_values [] init {} loop {} @@ -122,8 +129,11 @@ hw.module @OneAssertion(in %x: i1) { // ----- -func.func @two_separated_assertions() -> (i1) { - // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} +// A nested assert is rejected even when accompanied by a top-level assert +// (which on its own would be fine). The multiple-assertion diagnostic only +// counts asserts in the top module, so it does not apply here. +func.func @nested_and_toplevel_assertions() -> (i1) { + // expected-error @below {{assertions inside instantiated modules or called functions are not supported - inline them into the top module first (e.g. with --flatten-modules)}} %bmc = verif.bmc bound 10 num_regs 0 initial_values [] init {} loop {} @@ -143,8 +153,11 @@ hw.module @OneAssertion(in %x: i1) { // ----- -func.func @multiple_nested_assertions() -> (i1) { - // expected-error @below {{bounded model checking problems with multiple assertions are not yet correctly handled - instead, you can assert the conjunction of your assertions}} +// Two asserts inside one instantiated module hit the nested-assert +// rejection; the multiple-assertion diagnostic only counts top-module +// asserts. +func.func @nested_asserts_in_one_module() -> (i1) { + // expected-error @below {{assertions inside instantiated modules or called functions are not supported - inline them into the top module first (e.g. with --flatten-modules)}} %bmc = verif.bmc bound 10 num_regs 0 initial_values [] init {} loop {} diff --git a/test/Conversion/VerifToSMT/verif-to-smt.mlir b/test/Conversion/VerifToSMT/verif-to-smt.mlir index 0221e6cb5920..fe98b79fdccf 100644 --- a/test/Conversion/VerifToSMT/verif-to-smt.mlir +++ b/test/Conversion/VerifToSMT/verif-to-smt.mlir @@ -115,7 +115,6 @@ func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) { // CHECK-LABEL: func.func @test_bmc() -> i1 { // CHECK: [[BMC:%.+]] = smt.solver // CHECK: [[INIT:%.+]]:2 = func.call @bmc_init() -// CHECK: smt.push 1 // CHECK: [[F0:%.+]] = smt.declare_fun "input_1" : !smt.bv<32> // CHECK: [[F1:%.+]] = smt.declare_fun "reg_0" : !smt.bv<32> // CHECK: [[C42_BV32:%.+]] = smt.bv.constant #smt.bv<42> : !smt.bv<32> @@ -126,8 +125,6 @@ func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) { // CHECK: [[FALSE:%.+]] = arith.constant false // CHECK: [[TRUE:%.+]] = arith.constant true // CHECK: [[FOR:%.+]]:7 = scf.for [[ARG0:%.+]] = [[C0_I32]] to [[C10_I32]] step [[C1_I32]] iter_args([[ARG1:%.+]] = [[INIT]]#0, [[ARG2:%.+]] = [[F0]], [[ARG3:%.+]] = [[F1]], [[ARG4:%.+]] = [[C42_BV32]], [[ARG5:%.+]] = [[ARRAYFUN]], [[ARG6:%.+]] = [[INIT]]#1, [[ARG7:%.+]] = [[FALSE]]) -// CHECK: smt.pop 1 -// CHECK: smt.push 1 // CHECK-NOT: scf.if // CHECK: [[CIRCUIT:%.+]]:4 = func.call @bmc_circuit([[ARG1]], [[ARG2]], [[ARG3]], [[ARG4]], [[ARG5]]) // CHECK: [[SMTCHECK:%.+]] = smt.check sat { @@ -138,6 +135,7 @@ func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) { // CHECK: smt.yield [[FALSE]] // CHECK: } // CHECK: [[ORI:%.+]] = arith.ori [[SMTCHECK]], [[ARG7]] +// CHECK: smt.pop 1 // CHECK: [[LOOP:%.+]]:2 = func.call @bmc_loop([[ARG1]], [[ARG6]]) // CHECK: [[F2:%.+]] = smt.declare_fun "input_1" : !smt.bv<32> // CHECK: [[OLDCLOCKLOW:%.+]] = smt.bv.not [[ARG1]] @@ -181,6 +179,8 @@ func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) { // CHECK: [[XOR:%.+]] = comb.xor [[C6]], [[CN1_I32]] // CHECK: [[C9:%.+]] = builtin.unrealized_conversion_cast [[XOR]] : i32 to !smt.bv<32> // CHECK: [[C10:%.+]] = builtin.unrealized_conversion_cast [[ADD]] : i32 to !smt.bv<32> +// CHECK: smt.push 1 +// CHECK: smt.assert // CHECK: return [[C9]], [[C10]], [[ARG3]], [[ARG4]] // CHECK: }