llvm · leizaf · Jul 5, 2026
diff --git a/integration_test/circt-bmc/assumptions.mlir 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<i1>
+  %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<i1>
+  %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<i1>
+  %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
@@ -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
@@ -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<verif::BoundedModelCheckingOp>(parent))
+      return region == &bmcOp.getCircuit();
+    if (auto funcOp = dyn_cast<func::FuncOp>(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<verif::AssertOp> {
@@ -78,11 +100,14 @@ struct VerifAssertOpConversion : OpConversionPattern<verif::AssertOp> {
   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<smt::AssertOp>(op, notCond);
+    auto assertOp = rewriter.replaceOpWithNewOp<smt::AssertOp>(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 <circuit arguments> <state arguments>
     // <wasViolated>
     // 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<Value> loopCallInputs;
           // Fetch clock values to feed to loop
@@ -800,21 +824,35 @@ void ConvertVerifToSMTPass::runOnOperation() {
             if (auto func = dyn_cast<func::CallOp>(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<verif::AssertOp>(curOp))
-                numAssertions++;
+                numNestedAssertions++;
               if (auto inst = dyn_cast<InstanceOp>(curOp))
                 worklist.push_back(symbolTable.lookup(inst.getModuleName()));
               if (auto func = dyn_cast<func::CallOp>(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<func::FuncOp>()) {
+    if (!funcOp->hasAttr(kCircuitAttr))
+      continue;
+    funcOp->removeAttr(kCircuitAttr);
+    SmallVector<Operation *> 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
@@ -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
@@ -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:  }