[circt-bmc] handle 'verif.formal' / 'verif.contract' op in module by Clo91eaf · Pull Request #10772 · llvm/circt

Clo91eaf · 2026-07-05T10:59:03Z

This fixes circt-bmc on verif.contract lowering results.

circt-bmc already supports verif.formal: its pipeline runs verif-lower-tests, which lowers a selected formal test into an hw.module before BMC lowering. The issue is specific to the IR shape produced by lower-contracts.

lower-contracts emits a generated verif.formal proof op, but also keeps the original hw.module in the surrounding builtin.module with the contract applied to it. In that apply-mode module, contract results are replaced by verif.symbolic_value, and contract ensures become verif.assume.

When invoking circt-bmc --module <generated-formal>, the intended target is only the generated verif.formal. However, the BMC pipeline runs over the whole builtin.module, so unrelated top-level tests and modules may still be processed. This patch detects when --module resolves to a verif.formal, keeps that formal and its top-level symbol dependencies, and removes unrelated top-level hw.module, verif.formal, and verif.simulation ops before running the existing BMC pipeline.

This also handles generated formals that depend on callee contract abstractions. After contract lowering, a caller proof may instantiate a callee whose contract has been applied as an abstraction. During BMC lowering, hw-flatten-modules inlines that callee abstraction into the selected target, which can leave verif.symbolic_value ops constrained by verif.assume inside the flattened module. The patch materializes those symbolic values as additional module inputs after flattening, preserving their nondeterministic semantics in a form the BMC pipeline can lower.

For example:

hw.module @Callee(in %a : i8, out y : i8) {
  %y = verif.contract %a : i8 {
    %ok = comb.icmp eq %y, %a : i8
    verif.ensure %ok : i1
  }
  hw.output %y : i8
}

hw.module @Caller(in %a : i8, out y : i8) {
  %callee.y = hw.instance "callee" @Callee(a: %a: i8) -> (y: i8)

  %y = verif.contract %callee.y : i8 {
    %ok = comb.icmp eq %y, %a : i8
    verif.ensure %ok : i1
  }

  hw.output %y : i8
}

would be lowered after --lower-contracts to

hw.module @Callee(in %a : i8, out y : i8) {
  %sym = verif.symbolic_value : i8
  %ok = comb.icmp eq %sym, %a : i8
  verif.assume %ok : i1
  hw.output %sym : i8
}

verif.formal @Caller_CheckContract_0 {
  %a = verif.symbolic_value : i8
  %callee.y = hw.instance "callee" @Callee(a: %a: i8) -> (y: i8)
  %ok = comb.icmp eq %callee.y, %a : i8
  verif.assert %ok : i1
}

Here the @Caller_CheckContract_0 is depending the @Callee and the hw-flatten-modules pass will flatten the @Callee in the @Caller_CheckContract_0 to

hw.module @Caller_CheckContract_0(...) {
  %a = ...  // caller proof input

  // Inlined from Callee abstraction:
  %callee.sym = verif.symbolic_value : i8
  %callee.ok = comb.icmp eq %callee.sym, %a : i8
  verif.assume %callee.ok : i1

  // Caller contract check:
  %caller.ok = comb.icmp eq %callee.sym, %a : i8
  verif.assert %caller.ok : i1
}

So that the @Callee can become an abstract module rather than a specified implement during the formal verification solving. But this can not be processed by circt-bmc because

'verif.symbolic_value' op expects parent op to be one of 'verif.formal, hw.module'

And this pr move it to the input so we can see the symbolic value of the children module as the symbolic value of the parent module.

hw.module @Caller_CheckContract_0(
  in %a : i8,
  in %symbolic_value : i8
) {
  %callee.ok = comb.icmp eq %symbolic_value, %a : i8
  verif.assume %callee.ok : i1

  %caller.ok = comb.icmp eq %symbolic_value, %a : i8
  verif.assert %caller.ok : i1
}

Testing

This PR adds regression coverage that starts from real verif.contract IR, runs --lower-contracts, and then invokes circt-bmc on the generated verif.formal, including a caller/callee case where the selected proof depends on an applied callee contract abstraction.

Assisted-by: Codex:GPT-5.5

circt-bot · 2026-07-05T11:25:36Z

Results of circt-tests run for 722bcb1 compared to results for 0228f99: no change to test results.

Clo91eaf · 2026-07-06T04:10:33Z

@TaoBi22 wdyt? In this way we can handle the verif.contract in circt-bmc!

circt-bot · 2026-07-06T04:40:03Z

Results of circt-tests run for 425108f compared to results for 0228f99: no change to test results.

TaoBi22 · 2026-07-07T07:20:38Z

Thanks for looking into this @Clo91eaf! I wonder if it would make sense to make this hw.module input technique a new lowering strategy in LowerSymbolicValues rather than creating a new pass - WDYT?

Clo91eaf · 2026-07-07T07:31:09Z

That's really make sense! I will try this new lowering strategy!

TaoBi22

Thanks!

TaoBi22 · 2026-07-07T08:35:44Z

+  auto result = module.walk([&](SymbolicValueOp op) -> WalkResult {
+    if (!op->getParentOfType<HWModuleOp>())
+      return op.emitError()
+             << "cannot lower symbolic value to HW module input outside of an "


nit:

Suggested change

<< "cannot lower symbolic value to HW module input outside of an "

<< "cannot lower symbolic value to hw.module input outside of an "

TaoBi22 · 2026-07-07T08:36:39Z

+
+    if (referencedModules.contains(hwModule.getModuleNameAttr())) {
+      hwModule.emitError()
+          << "cannot lower symbolic values in instantiated module '"


nit: can we clarify that this is only the case for this particular lowering strategy?

TaoBi22 · 2026-07-07T08:41:18Z

@@ -0,0 +1,22 @@
+// RUN: circt-opt %s --verif-lower-symbolic-values=mode=hw-input --split-input-file --verify-diagnostics | FileCheck %s


Could these be moved into the existing test files for this pass?

TaoBi22 · 2026-07-07T08:42:12Z

@@ -0,0 +1,22 @@
+// RUN: circt-opt %s --verif-lower-symbolic-values=mode=hw-input --split-input-file --verify-diagnostics | FileCheck %s
+
+// CHECK-LABEL: hw.module @M(in %symbolic_value : i8, out y : i8)


Can these be regex rather than hardcoded names?

TaoBi22 · 2026-07-07T08:42:21Z

+
+// CHECK-NOT:   verif.symbolic_value
+// CHECK-LABEL: func.func @Callee(
+// CHECK-SAME:  %arg0: !smt.bv<8>, %arg1: !smt.bv<8>


As above re: regex

TaoBi22 · 2026-07-07T08:44:12Z

+// CHECK-NOT:   verif.symbolic_value
+// CHECK-LABEL: func.func @Callee(
+// CHECK-SAME:  %arg0: !smt.bv<8>, %arg1: !smt.bv<8>
+// CHECK:       smt.assert


maybe check what we're asserting too?

fixed. Thanks!

circt-bot · 2026-07-07T08:58:39Z

Results of circt-tests run for 7eea901 compared to results for 0228f99: no change to test results.

…tions

circt-bot · 2026-07-07T10:36:51Z

Results of circt-tests run for da63082 compared to results for 0228f99: no change to test results.

TaoBi22

Thanks @Clo91eaf! A couple of remaining nits, let me know when those are addressed and you're happy for merge!

TaoBi22 · 2026-07-10T11:58:08Z

+  hw.output %0 : i8
+}
+
+// expected-error @+1 {{cannot lower symbolic values in instantiated module}}


nit: can we include the full error message?

TaoBi22 · 2026-07-10T11:58:21Z

+  auto result = module.walk([&](SymbolicValueOp op) -> WalkResult {
+    if (!op->getParentOfType<HWModuleOp>())
+      return op.emitError()
+             << "cannot lower symbolic value to hw.module input outside of an "


I think this is missing a test

Clo91eaf changed the title ~~Circt bmc verif formal~~ [circt-bmc] handle 'verif.formal' op in module Jul 5, 2026

[circt-bmc] handle 'verif.formal' op in module

722bcb1

Clo91eaf mentioned this pull request Jul 5, 2026

[lit] run contract BMC directly xinpian-tech/zaozi#126

Open

Clo91eaf changed the title ~~[circt-bmc] handle 'verif.formal' op in module~~ [circt-bmc] handle 'verif.formal' / 'verif.contract' op in module Jul 6, 2026

TaoBi22 self-requested a review July 6, 2026 07:53

Clo91eaf force-pushed the circt-bmc-verif-formal branch 2 times, most recently from 29ecaf5 to 7eea901 Compare July 7, 2026 08:28

TaoBi22 approved these changes Jul 7, 2026

View reviewed changes

[Verif] add new pass to lower symbolic values to input port

54661f9

Clo91eaf force-pushed the circt-bmc-verif-formal branch from 7eea901 to da63082 Compare July 7, 2026 10:08

[circt-bmc] materialize symbolic values in flattened contract abstrac…

da63082

…tions

Clo91eaf requested a review from TaoBi22 July 7, 2026 17:31

TaoBi22 approved these changes Jul 10, 2026

View reviewed changes

	<< "cannot lower symbolic value to HW module input outside of an "
	<< "cannot lower symbolic value to hw.module input outside of an "

		@@ -0,0 +1,22 @@
		// RUN: circt-opt %s --verif-lower-symbolic-values=mode=hw-input --split-input-file --verify-diagnostics \| FileCheck %s

		@@ -0,0 +1,22 @@
		// RUN: circt-opt %s --verif-lower-symbolic-values=mode=hw-input --split-input-file --verify-diagnostics \| FileCheck %s

		// CHECK-LABEL: hw.module @M(in %symbolic_value : i8, out y : i8)

Uh oh!

Conversation

Clo91eaf commented Jul 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Testing

Uh oh!

circt-bot Bot commented Jul 5, 2026

Uh oh!

Clo91eaf commented Jul 6, 2026

Uh oh!

circt-bot Bot commented Jul 6, 2026

Uh oh!

TaoBi22 commented Jul 7, 2026

Uh oh!

Clo91eaf commented Jul 7, 2026

Uh oh!

TaoBi22 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

circt-bot Bot commented Jul 7, 2026

Uh oh!

circt-bot Bot commented Jul 7, 2026

Uh oh!

TaoBi22 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Clo91eaf commented Jul 5, 2026 •

edited

Loading