[circt-bmc][VerifToSMT] Add initial value support (#7903)

Author: TaoBi22

integration_test/circt-bmc/seq-errors.mlir

@@ -1,17 +1,21 @@
 // REQUIRES: libz3
 // REQUIRES: circt-bmc-jit
 
-//  RUN: circt-bmc %s -b 10 --module Counter --shared-libs=%libz3 | FileCheck %s --check-prefix=COUNTER
-//  COUNTER: Assertion can be violated!
+//  Test with two bounds - one that doesn't run long enough for the counter to reach 3, and one that does
+//  RUN: circt-bmc %s -b 2 --module Counter --shared-libs=%libz3 | FileCheck %s --check-prefix=COUNTER2
+//  COUNTER2: Bound reached with no violations!
+//  RUN: circt-bmc %s -b 10 --module Counter --shared-libs=%libz3 | FileCheck %s --check-prefix=COUNTER10
+//  COUNTER10: Assertion can be violated!
 
 hw.module @Counter(in %clk: !seq.clock, out count: i2) {
+  %init = seq.initial () {
+    %c0_i2 = hw.constant 0 : i2
+    seq.yield %c0_i2 : i2
+  } : () -> !seq.immutable<i2>
   %c1_i2 = hw.constant 1 : i2
   %regPlusOne = comb.add %reg, %c1_i2 : i2
-  %reg = seq.compreg %regPlusOne, %clk : i2
-  // Condition - count should never reach 3 (deliberately not true)
-  // FIXME: add an initial condition here once we support them, currently it
-  // can be violated on the first cycle as 3 is a potential initial value.
-  // Can also use this to check bounds are behaving as expected.
+  %reg = seq.compreg %regPlusOne, %clk initial %init : i2
+  // Condition - count should never reach 3
   %c3_i2 = hw.constant 3 : i2
   %lt = comb.icmp ult %reg, %c3_i2 : i2
   verif.assert %lt : i1

lib/Conversion/VerifToSMT/VerifToSMT.cpp

@@ -9,6 +9,7 @@
 #include "circt/Conversion/VerifToSMT.h"
 #include "circt/Conversion/HWToSMT.h"
 #include "circt/Dialect/SMT/SMTOps.h"
+#include "circt/Dialect/SMT/SMTTypes.h"
 #include "circt/Dialect/Seq/SeqTypes.h"
 #include "circt/Dialect/Verif/VerifOps.h"
 #include "circt/Support/Namespace.h"
@@ -206,8 +207,8 @@ struct VerifBoundedModelCheckingOpConversion
     if (failed(rewriter.convertRegionTypes(&op.getCircuit(), *typeConverter)))
       return failure();
 
-    unsigned numRegs =
-        cast<IntegerAttr>(op->getAttr("num_regs")).getValue().getZExtValue();
+    unsigned numRegs = op.getNumRegs();
+    auto initialValues = op.getInitialValues();
 
     auto initFuncTy = rewriter.getFunctionType({}, initOutputTy);
     // Loop and init output types are necessarily the same, so just use init
@@ -272,9 +273,19 @@ struct VerifBoundedModelCheckingOpConversion
       if (isa<seq::ClockType>(oldTy)) {
         inputDecls.push_back(initVals[initIndex++]);
         clockIndexes.push_back(curIndex);
-      } else {
-        inputDecls.push_back(rewriter.create<smt::DeclareFunOp>(loc, newTy));
+        continue;
       }
+      if (curIndex >= oldCircuitInputTy.size() - numRegs) {
+        auto initVal =
+            initialValues[curIndex - oldCircuitInputTy.size() + numRegs];
+        if (auto initIntAttr = dyn_cast<IntegerAttr>(initVal)) {
+          inputDecls.push_back(rewriter.create<smt::BVConstantOp>(
+              loc, initIntAttr.getValue().getSExtValue(),
+              cast<smt::BitVectorType>(newTy).getWidth()));
+          continue;
+        }
+      }
+      inputDecls.push_back(rewriter.create<smt::DeclareFunOp>(loc, newTy));
     }
 
     auto numStateArgs = initVals.size() - initIndex;
@@ -434,6 +445,19 @@ void ConvertVerifToSMTPass::runOnOperation() {
   WalkResult assertionCheck = getOperation().walk(
       [&](Operation *op) { // Check there is exactly one assertion and clock
         if (auto bmcOp = dyn_cast<verif::BoundedModelCheckingOp>(op)) {
+          // We also currently don't support initial values on registers that
+          // don't have integer inputs.
+          auto regTypes = TypeRange(bmcOp.getCircuit().getArgumentTypes())
+                              .take_back(bmcOp.getNumRegs());
+          for (auto [regType, initVal] :
+               llvm::zip(regTypes, bmcOp.getInitialValues())) {
+            if (!isa<IntegerType>(regType) && !isa<UnitAttr>(initVal)) {
+              op->emitError("initial values are currently only supported for "
+                            "registers with integer types");
+              signalPassFailure();
+              return WalkResult::interrupt();
+            }
+          }
           // Check only one clock is present in the circuit inputs
           auto numClockArgs = 0;
           for (auto argType : bmcOp.getCircuit().getArgumentTypes())

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

@@ -122,3 +122,26 @@ func.func @multiple_clocks() -> (i1) {
   }
   func.return %bmc : i1
 }
+
+// -----
+
+func.func @multiple_clocks() -> (i1) {
+  // expected-error @below {{initial values are currently only supported for registers with integer types}}
+  %bmc = verif.bmc bound 10 num_regs 1 initial_values [0]
+  init {
+    %c0_i1 = hw.constant 0 : i1
+    %clk = seq.to_clock %c0_i1
+    verif.yield %clk : !seq.clock
+  }
+  loop {
+    ^bb0(%clk: !seq.clock):
+    verif.yield %clk: !seq.clock
+  }
+  circuit {
+  ^bb0(%clk: !seq.clock, %arg0: !hw.array<2xi32>):
+    %true = hw.constant true
+    verif.assert %true : i1
+    verif.yield %arg0 : !hw.array<2xi32>
+  }
+  func.return %bmc : i1
+}

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

@@ -93,33 +93,37 @@ func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) {
 // CHECK:      smt.push 1
 // CHECK:      [[F0:%.+]] = smt.declare_fun : !smt.bv<32>
 // CHECK:      [[F1:%.+]] = smt.declare_fun : !smt.bv<32>
+// CHECK:      [[C42_BV32:%.+]] = smt.bv.constant #smt.bv<42> : !smt.bv<32>
+// CHECK:      [[ARRAYFUN:%.+]] = smt.declare_fun : !smt.array<[!smt.bv<1> -> !smt.bv<32>]>
 // CHECK:      [[C0_I32:%.+]] = arith.constant 0 : i32
 // CHECK:      [[C1_I32:%.+]] = arith.constant 1 : i32
 // CHECK:      [[C10_I32:%.+]] = arith.constant 10 : i32
 // CHECK:      [[FALSE:%.+]] = arith.constant false
 // CHECK:      [[TRUE:%.+]] = arith.constant true
-// CHECK:      [[FOR:%.+]]:5 = scf.for [[ARG0:%.+]] = [[C0_I32]] to [[C10_I32]] step [[C1_I32]] iter_args([[ARG1:%.+]] = [[INIT]]#0, [[ARG2:%.+]] = [[F0]], [[ARG3:%.+]] = [[F1]], [[ARG4:%.+]] = [[INIT]]#1, [[ARG5:%.+]] = [[FALSE]])
+// 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:        [[CIRCUIT:%.+]]:2 = func.call @bmc_circuit([[ARG1]], [[ARG2]], [[ARG3]])
+// CHECK:        [[CIRCUIT:%.+]]:4 = func.call @bmc_circuit([[ARG1]], [[ARG2]], [[ARG3]], [[ARG4]], [[ARG5]])
 // CHECK:        [[SMTCHECK:%.+]] = smt.check sat {
 // CHECK:          smt.yield [[TRUE]]
 // CHECK:        } unknown {
 // CHECK:          smt.yield [[TRUE]]
 // CHECK:        } unsat {
 // CHECK:          smt.yield [[FALSE]]
 // CHECK:        }
-// CHECK:        [[ORI:%.+]] = arith.ori [[SMTCHECK]], [[ARG5]]
-// CHECK:        [[LOOP:%.+]]:2 = func.call @bmc_loop([[ARG1]], [[ARG4]])
+// CHECK:        [[ORI:%.+]] = arith.ori [[SMTCHECK]], [[ARG7]]
+// CHECK:        [[LOOP:%.+]]:2 = func.call @bmc_loop([[ARG1]], [[ARG6]])
 // CHECK:        [[F2:%.+]] = smt.declare_fun : !smt.bv<32>
 // CHECK:        [[OLDCLOCKLOW:%.+]] = smt.bv.not [[ARG1]]
 // CHECK:        [[BVPOSEDGE:%.+]] = smt.bv.and [[OLDCLOCKLOW]], [[LOOP]]#0
 // CHECK:        [[BVTRUE:%.+]] = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
 // CHECK:        [[BOOLPOSEDGE:%.+]] = smt.eq [[BVPOSEDGE]], [[BVTRUE]]
-// CHECK:        [[NEWREG:%.+]] = smt.ite [[BOOLPOSEDGE]], [[CIRCUIT]]#1, [[ARG3]]
-// CHECK:        scf.yield [[LOOP]]#0, [[F2]], [[NEWREG]], [[LOOP]]#1, [[ORI]]
+// CHECK:        [[NEWREG1:%.+]] = smt.ite [[BOOLPOSEDGE]], [[CIRCUIT]]#1, [[ARG3]]
+// CHECK:        [[NEWREG2:%.+]] = smt.ite [[BOOLPOSEDGE]], [[CIRCUIT]]#2, [[ARG4]]
+// CHECK:        [[NEWREG3:%.+]] = smt.ite [[BOOLPOSEDGE]], [[CIRCUIT]]#3, [[ARG5]]
+// CHECK:        scf.yield [[LOOP]]#0, [[F2]], [[NEWREG1]], [[NEWREG2]], [[NEWREG3]], [[LOOP]]#1, [[ORI]]
 // CHECK:      }
-// CHECK:      [[XORI:%.+]] = arith.xori [[FOR]]#4, [[TRUE]]
+// CHECK:      [[XORI:%.+]] = arith.xori [[FOR]]#6, [[TRUE]]
 // CHECK:      smt.yield [[XORI]]
 // CHECK:    }
 // CHECK:    return [[BMC]]
@@ -143,19 +147,19 @@ func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) {
 // CHECK:    [[C5:%.+]] = builtin.unrealized_conversion_cast [[NARG]] : i1 to !smt.bv<1>
 // CHECK:    return [[C4]], [[C5]]
 // CHECK:  }
-// CHECK:  func.func @bmc_circuit([[ARGO:%.+]]: !smt.bv<1>, [[ARG1:%.+]]: !smt.bv<32>, [[ARG2:%.+]]: !smt.bv<32>)
+// CHECK:  func.func @bmc_circuit([[ARGO:%.+]]: !smt.bv<1>, [[ARG1:%.+]]: !smt.bv<32>, [[ARG2:%.+]]: !smt.bv<32>, [[ARG3:%.+]]: !smt.bv<32>, [[ARG4:%.+]]: !smt.array<[!smt.bv<1> -> !smt.bv<32>]>)
 // CHECK:    [[C6:%.+]] = builtin.unrealized_conversion_cast [[ARG2]] : !smt.bv<32> to i32
 // CHECK:    [[C7:%.+]] = builtin.unrealized_conversion_cast [[ARG1]] : !smt.bv<32> to i32
 // CHECK:    [[CN1_I32:%.+]] = hw.constant -1 : i32
 // CHECK:    [[ADD:%.+]] = comb.add [[C7]], [[C6]]
 // 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:    return [[C9]], [[C10]]
+// CHECK:    return [[C9]], [[C10]], [[ARG3]], [[ARG4]]
 // CHECK:  }
 
 func.func @test_bmc() -> (i1) {
-  %bmc = verif.bmc bound 10 num_regs 1 initial_values [unit]
+  %bmc = verif.bmc bound 10 num_regs 3 initial_values [unit, 42, unit]
   init {
     %c0_i1 = hw.constant 0 : i1
     %clk = seq.to_clock %c0_i1
@@ -171,12 +175,12 @@ func.func @test_bmc() -> (i1) {
     verif.yield %newclk, %newStateArg : !seq.clock, i1
   }
   circuit {
-  ^bb0(%clk: !seq.clock, %arg0: i32, %state0: i32):
+  ^bb0(%clk: !seq.clock, %arg0: i32, %state0: i32, %state1: i32, %state2: !hw.array<2xi32>):
     %c-1_i32 = hw.constant -1 : i32
     %0 = comb.add %arg0, %state0 : i32
     // %state0 is the result of a seq.compreg taking %0 as input
     %2 = comb.xor %state0, %c-1_i32 : i32
-    verif.yield %2, %0 : i32, i32
+    verif.yield %2, %0, %state1, %state2 : i32, i32, i32, !hw.array<2xi32>
   }
   func.return %bmc : i1
 }