[circt-bmc] Add multi-clock BMC support

lib/Tools/circt-bmc/ExternalizeRegisters.cpp

@@ -80,16 +80,6 @@ void ExternalizeRegistersPass::runOnOperation() {
         continue;
 
       unsigned numRegs = 0;
-      bool foundClk = false;
-      for (auto ty : module.getInputTypes()) {
-        if (isa<seq::ClockType>(ty)) {
-          if (foundClk) {
-            module.emitError("modules with multiple clocks not yet supported");
-            return signalPassFailure();
-          }
-          foundClk = true;
-        }
-      }
       module->walk([&](Operation *op) {
         if (auto regOp = dyn_cast<seq::CompRegOp>(op)) {
           mlir::Attribute initState = {};

lib/Tools/circt-bmc/LowerToBMC.cpp

@@ -124,68 +124,57 @@ void LowerToBMCPass::runOnOperation() {
     return signalPassFailure();
   }
 
-  // Check that there's only one clock input to the module
-  // TODO: supporting multiple clocks isn't too hard, an interleaving of clock
-  // toggles just needs to be generated
-  bool hasClk = false;
+  // Count top-level clock inputs. Each gets an independent toggle entry in the
+  // init/loop regions so the BMC explores all synchronous interleavings.
+  // Struct-embedded clocks are not yet supported.
+  unsigned numClocks = 0;
   for (auto input : hwModule.getInputTypes()) {
     if (isa<seq::ClockType>(input)) {
-      if (hasClk) {
-        hwModule.emitError("designs with multiple clocks not yet supported");
-        return signalPassFailure();
-      }
-      hasClk = true;
+      ++numClocks;
     }
     if (auto hwStruct = dyn_cast<hw::StructType>(input)) {
       for (auto field : hwStruct.getElements()) {
         if (isa<seq::ClockType>(field.type)) {
-          if (hasClk) {
-            hwModule.emitError(
-                "designs with multiple clocks not yet supported");
-            return signalPassFailure();
-          }
-          hasClk = true;
+          hwModule.emitError(
+              "designs with struct-embedded clocks not yet supported");
+          return signalPassFailure();
         }
       }
     }
   }
   {
     OpBuilder::InsertionGuard guard(builder);
-    // Initialize clock to 0 if it exists, otherwise just yield nothing
-    // We initialize to 1 if we're in rising clocks only mode
+    // Initialize all clocks to 0 (or 1 in rising-clocks-only mode).
     auto *initBlock = builder.createBlock(&bmcOp.getInit());
     builder.setInsertionPointToStart(initBlock);
-    if (hasClk) {
+    SmallVector<Value> initClocks;
+    for (unsigned i = 0; i < numClocks; ++i) {
       auto initVal = hw::ConstantOp::create(builder, loc, builder.getI1Type(),
                                             risingClocksOnly ? 1 : 0);
-      auto toClk = seq::ToClockOp::create(builder, loc, initVal);
-      verif::YieldOp::create(builder, loc, ValueRange{toClk});
-    } else {
-      verif::YieldOp::create(builder, loc, ValueRange{});
+      initClocks.push_back(seq::ToClockOp::create(builder, loc, initVal));
     }
+    verif::YieldOp::create(builder, loc, initClocks);
 
-    // Toggle clock in loop region if it exists, otherwise just yield nothing
+    // Toggle every clock each step (synchronous multi-clock interleaving).
     auto *loopBlock = builder.createBlock(&bmcOp.getLoop());
     builder.setInsertionPointToStart(loopBlock);
-    if (hasClk) {
+    for (unsigned i = 0; i < numClocks; ++i)
       loopBlock->addArgument(seq::ClockType::get(ctx), loc);
-      if (risingClocksOnly) {
-        // In rising clocks only mode we don't need to toggle the clock
-        verif::YieldOp::create(builder, loc,
-                               ValueRange{loopBlock->getArgument(0)});
-      } else {
-        auto fromClk =
-            seq::FromClockOp::create(builder, loc, loopBlock->getArgument(0));
+    SmallVector<Value> nextClocks;
+    if (risingClocksOnly) {
+      // Rising-clocks-only mode: pass clocks through unchanged.
+      for (auto arg : loopBlock->getArguments())
+        nextClocks.push_back(arg);
+    } else {
+      for (auto arg : loopBlock->getArguments()) {
+        auto fromClk = seq::FromClockOp::create(builder, loc, arg);
         auto cNeg1 =
             hw::ConstantOp::create(builder, loc, builder.getI1Type(), -1);
         auto nClk = comb::XorOp::create(builder, loc, fromClk, cNeg1);
-        auto toClk = seq::ToClockOp::create(builder, loc, nClk);
-        // Only yield clock value
-        verif::YieldOp::create(builder, loc, ValueRange{toClk});
+        nextClocks.push_back(seq::ToClockOp::create(builder, loc, nClk));
       }
-    } else {
-      verif::YieldOp::create(builder, loc, ValueRange{});
     }
+    verif::YieldOp::create(builder, loc, nextClocks);
   }
   bmcOp.getCircuit().takeBody(hwModule.getBody());
   hwModule->erase();

test/Tools/circt-bmc/externalize-registers-errors.mlir

@@ -1,14 +1,5 @@
 // RUN: circt-opt --externalize-registers --split-input-file --verify-diagnostics %s
 
-// expected-error @below {{modules with multiple clocks not yet supported}}
-hw.module @two_clks(in %clk0: !seq.clock, in %clk1: !seq.clock, in %in: i32, out out: i32) {
-  %1 = seq.compreg %in, %clk0 : i32
-  %2 = seq.compreg %1, %clk1 : i32
-  hw.output %2 : i32
-}
-
-// -----
-
 hw.module @two_clks(in %clk_i1: i1, in %in: i32, out out: i32) {
   %clk = seq.to_clock %clk_i1
   // expected-error @below {{only clocks directly given as block arguments are supported}}

test/Tools/circt-bmc/externalize-registers.mlir

@@ -133,6 +133,16 @@ hw.module @named_firregs(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out ou
   hw.output %secondreg : i32
 }
 
+// Multi-clock: two registers on independent clocks are both externalized.
+// CHECK:  hw.module @two_clk_regs(in [[CLK0:%.+]] : !seq.clock, in [[CLK1:%.+]] : !seq.clock, in [[IN:%.+]] : i32, in [[REG0:%.+]] : i32, in [[REG1:%.+]] : i32, out {{.+}} : i32, out {{.+}} : i32, out {{.+}} : i32) attributes {initial_values = [unit, unit], num_regs = 2 : i32} {
+// CHECK:    hw.output [[REG1]], [[IN]], [[REG0]]
+// CHECK:  }
+hw.module @two_clk_regs(in %clk0: !seq.clock, in %clk1: !seq.clock, in %in: i32, out out: i32) {
+  %reg0 = seq.compreg %in,   %clk0 : i32
+  %reg1 = seq.compreg %reg0, %clk1 : i32
+  hw.output %reg1 : i32
+}
+
 // CHECK:  hw.module @firreg_with_sync_reset(in [[CLK:%.+]] : !seq.clock, in [[RST:%.+]] : i1, in [[IN:%.+]] : i32, in [[OLD_REG1:%.+]] : i32, out {{.+}} : i32, out {{.+}} : i32) attributes {initial_values = [unit], num_regs = 1 : i32} {
 // CHECK:    [[C0_I32:%.+]] = hw.constant 0 : i32
 // CHECK:    [[MUX1:%.+]] = comb.mux [[RST]], [[C0_I32]], [[IN]] : i32

test/Tools/circt-bmc/lower-to-bmc-errors.mlir

@@ -54,17 +54,7 @@ hw.module @testModule(in %clk0 : !seq.clock, in %in0 : i32, in %in1 : i32, in %r
 
 // -----
 
-// expected-error @below {{designs with multiple clocks not yet supported}}
-hw.module @testModule(in %clk0 : !seq.clock, in %clk1 : !seq.clock, in %in0 : i32, in %in1 : i32, in %reg0_state : i32, in %reg1_state : i32, out out : i32, out reg0_input : i32, out reg1_input : i32) attributes {num_regs = 2 : i32, initial_values = [unit, unit]} {
-  %0 = comb.add %reg0_state, %reg1_state : i32
-  %1 = comb.icmp eq %0, %in0 : i32
-  verif.assert %1 : i1
-  hw.output %0, %in0, %in1 : i32, i32, i32
-}
-
-// -----
-
-// expected-error @below {{designs with multiple clocks not yet supported}}
+// expected-error @below {{designs with struct-embedded clocks not yet supported}}
 hw.module @testModule(in %clk0 : !seq.clock, in %clkStruct : !hw.struct<clk: !seq.clock>, in %in0 : i32, in %in1 : i32, in %reg0_state : i32, in %reg1_state : i32, out out : i32, out reg0_input : i32, out reg1_input : i32) attributes {num_regs = 2 : i32, initial_values = [unit, unit]} {
   %0 = comb.add %reg0_state, %reg1_state : i32
   %1 = comb.icmp eq %0, %in0 : i32

test/Tools/circt-bmc/multi-clock-bmc.mlir

@@ -0,0 +1,34 @@
+// RUN: circt-opt --externalize-registers --lower-to-bmc="top-module=two_clk_design bound=10" %s | FileCheck %s
+
+// Verify that multi-clock designs are handled end-to-end: each clock gets an
+// independent toggle in the init/loop regions of verif.bmc.
+
+// CHECK: func.func @two_clk_design() {
+// CHECK:   [[BMC:%.+]] = verif.bmc bound 20 num_regs 2 initial_values [unit, unit] init {
+// CHECK:     [[FALSE0:%.+]] = hw.constant false
+// CHECK:     [[CLK0_INIT:%.+]] = seq.to_clock [[FALSE0]]
+// CHECK:     [[FALSE1:%.+]] = hw.constant false
+// CHECK:     [[CLK1_INIT:%.+]] = seq.to_clock [[FALSE1]]
+// CHECK:     verif.yield [[CLK0_INIT]], [[CLK1_INIT]]
+// CHECK:   } loop {
+// CHECK:   ^bb0([[CLK0:%.+]]: !seq.clock, [[CLK1:%.+]]: !seq.clock):
+// CHECK:     [[FROM0:%.+]] = seq.from_clock [[CLK0]]
+// CHECK:     [[TRUE0:%.+]] = hw.constant true
+// CHECK:     [[NCLK0:%.+]] = comb.xor [[FROM0]], [[TRUE0]]
+// CHECK:     [[NEW_CLK0:%.+]] = seq.to_clock [[NCLK0]]
+// CHECK:     [[FROM1:%.+]] = seq.from_clock [[CLK1]]
+// CHECK:     [[TRUE1:%.+]] = hw.constant true
+// CHECK:     [[NCLK1:%.+]] = comb.xor [[FROM1]], [[TRUE1]]
+// CHECK:     [[NEW_CLK1:%.+]] = seq.to_clock [[NCLK1]]
+// CHECK:     verif.yield [[NEW_CLK0]], [[NEW_CLK1]]
+// CHECK:   } circuit {
+// CHECK:   ^bb0([[C0:%.+]]: !seq.clock, [[C1:%.+]]: !seq.clock,
+
+hw.module @two_clk_design(in %clk0: !seq.clock, in %clk1: !seq.clock,
+                           in %in: i32, out out: i32) {
+  %reg0 = seq.compreg %in,   %clk0 : i32
+  %reg1 = seq.compreg %reg0, %clk1 : i32
+  %prop = comb.icmp uge %reg1, %in : i32
+  verif.assert %prop : i1
+  hw.output %reg1 : i32
+}