[circt-bmc] Add multi-clock BMC support

docs/Tools/circt-bmc.md

@@ -32,6 +32,12 @@ a `verif.assert` operation. Calling
 emit `Bound reached with no violations!`, as the property holds over the 10
 cycles checked.
 
+## Multi-Clock Support
+
+`circt-bmc` supports model checking designs with multiple independent clock domains, enabling the verification of Clock Domain Crossing (CDC) logic. When a module has multiple `!seq.clock` inputs, the BMC tool generates a non-deterministic loop where each clock independently decides whether to toggle at each step using a `verif.symbolic_value`. This allows the underlying SMT solver to explore all possible asynchronous clock interleavings, making it possible to catch metastability and data corruption bugs that only manifest at specific clock phases. 
+
+To toggle all clocks synchronously at the exact same time every cycle, you can pass the `--sync-clocks` flag to `circt-opt --lower-to-bmc`.
+
 ## (Draft) Building a BMC tool
 
 For completeness, this section describes how a BMC (bounded model checking)

include/circt/Dialect/Verif/VerifOps.td

@@ -486,7 +486,7 @@ def SimulationOp : VerifOp<"simulation", [
 }
 
 def SymbolicValueOp : VerifOp<"symbolic_value", [
-  ParentOneOf<["verif::FormalOp", "hw::HWModuleOp"]>,
+  ParentOneOf<["verif::FormalOp", "hw::HWModuleOp", "verif::BoundedModelCheckingOp"]>,
 ]>{
   let summary = "Create a symbolic value for formal verification";
   let description = [{
@@ -499,6 +499,24 @@ def SymbolicValueOp : VerifOp<"symbolic_value", [
   let assemblyFormat = "attr-dict `:` type($result)";
 }
 
+def ClockedByOp : VerifOp<"clocked_by"> {
+  let summary = "Records that a value is the next state of a register driven by a clock";
+  let description = [{
+    Emitted by ExternalizeRegisters for each externalized register. Associates the
+    clock SSA value that drove the original seq.compreg/firreg with the next-state
+    output value that replaced it. Used downstream by LowerToBMC and VerifToSMT to
+    correctly gate register state updates to the posedge of their respective clock.
+
+    This op solves the problem that MLIR attributes cannot reference SSA values:
+    by using a proper operation, both operands are first-class IR values that are
+    maintained correctly by all standard MLIR transformations (renaming, DCE, etc.).
+  }];
+  let arguments = (ins ClockType:$clock, AnyType:$nextState);
+  let assemblyFormat = [{
+    $clock `->` $nextState attr-dict `:` type($clock) `,` type($nextState)
+  }];
+}
+
 //===----------------------------------------------------------------------===//
 // Formal Contracts
 //===----------------------------------------------------------------------===//

include/circt/Tools/circt-bmc/Passes.td

@@ -34,6 +34,9 @@ def LowerToBMC : Pass<"lower-to-bmc", "::mlir::ModuleOp"> {
     Option<"risingClocksOnly", "rising-clocks-only", "bool",
            /*default=*/"false",
            "Only consider the circuit and property on rising clock edges.">,
+    Option<"syncClocks", "sync-clocks", "bool",
+           /*default=*/"false",
+           "Force all clocks to toggle together synchronously.">,
   ];
 
   let dependentDialects = [
@@ -46,7 +49,7 @@ def ExternalizeRegisters : Pass<"externalize-registers", "::mlir::ModuleOp"> {
   let summary = "Removes registers and adds corresponding input and output ports";
 
   let dependentDialects = [
-    "circt::seq::SeqDialect", "circt::hw::HWDialect"
+    "circt::seq::SeqDialect", "circt::hw::HWDialect", "circt::verif::VerifDialect"
   ];
 }
 

lib/Conversion/VerifToSMT/VerifToSMT.cpp

@@ -412,6 +412,7 @@ struct VerifBoundedModelCheckingOpConversion
 
     func::FuncOp initFuncOp, loopFuncOp, circuitFuncOp;
 
+    SmallVector<unsigned> regToClockArgIdx(numRegs);
     {
       OpBuilder::InsertionGuard guard(rewriter);
       rewriter.setInsertionPointToEnd(
@@ -429,6 +430,38 @@ struct VerifBoundedModelCheckingOpConversion
       rewriter.inlineRegionBefore(op.getCircuit(),
                                   circuitFuncOp.getFunctionBody(),
                                   circuitFuncOp.end());
+
+      {
+        // Extract the clock-to-register mapping from verif.clocked_by ops.
+        // These ops were added by ExternalizeRegisters to associate each
+        // externalized register's next-state value with the specific clock
+        // that drives it. We need this mapping so we can correctly route
+        // the posedge detection for each register in the SMT loop.
+        auto &circuitBlock = circuitFuncOp.getBody().front();
+        auto *circuitYield = circuitBlock.getTerminator();
+        for (auto clockedBy :
+             llvm::make_early_inc_range(circuitBlock.getOps<verif::ClockedByOp>())) {
+          auto nextState = clockedBy.getNextState();
+          auto clockArg = cast<BlockArgument>(clockedBy.getClock());
+          unsigned nextStateIdx = 0;
+          bool found = false;
+          for (auto [idx, operand] :
+               llvm::enumerate(circuitYield->getOperands())) {
+            if (operand == nextState) {
+              nextStateIdx = idx;
+              found = true;
+              break;
+            }
+          }
+          if (found) {
+            unsigned regIdx =
+                nextStateIdx - (circuitYield->getNumOperands() - numRegs);
+            regToClockArgIdx[regIdx] = clockArg.getArgNumber();
+          }
+          rewriter.eraseOp(clockedBy);
+        }
+      }
+
       auto funcOps = {&initFuncOp, &loopFuncOp, &circuitFuncOp};
       // initOutputTy is the same as loop output types
       auto outputTys = {initOutputTy, initOutputTy, circuitOutputTy};
@@ -600,41 +633,47 @@ struct VerifBoundedModelCheckingOpConversion
 
           // Only update the registers on a clock posedge unless in rising
           // clocks only mode
-          // TODO: this will also need changing with multiple clocks - currently
-          // it only accounts for the one clock case.
-          if (clockIndexes.size() == 1) {
-            SmallVector<Value> regInputs = circuitCallOuts.take_back(numRegs);
-            if (risingClocksOnly) {
-              // In rising clocks only mode we don't need to worry about whether
-              // there was a posedge
-              newDecls.append(regInputs);
-            } else {
-              auto clockIndex = clockIndexes[0];
-              auto oldClock = iterArgs[clockIndex];
-              // The clock is necessarily the first value returned by the loop
-              // region
-              auto newClock = loopVals[0];
+          SmallVector<Value> regInputs = circuitCallOuts.take_back(numRegs);
+          if (risingClocksOnly) {
+            // In rising clocks only mode we don't need to worry about whether
+            // there was a posedge
+            newDecls.append(regInputs);
+          } else {
+            // Map: clock circuit arg index -> isPosedge bool
+            DenseMap<unsigned, Value> isPosedgePerClock;
+            for (auto [i, clockIdx] : llvm::enumerate(clockIndexes)) {
+              auto oldClock = iterArgs[clockIdx];
+              // The clocks are necessarily the first values returned by the
+              // loop region
+              auto newClock = loopVals[i];
               auto oldClockLow = smt::BVNotOp::create(builder, loc, oldClock);
               auto isPosedgeBV =
                   smt::BVAndOp::create(builder, loc, oldClockLow, newClock);
               // Convert posedge bv<1> to bool
               auto trueBV = smt::BVConstantOp::create(builder, loc, 1, 1);
               auto isPosedge =
                   smt::EqOp::create(builder, loc, isPosedgeBV, trueBV);
-              auto regStates =
-                  iterArgs.take_front(circuitFuncOp.getNumArguments())
-                      .take_back(numRegs);
-              SmallVector<Value> nextRegStates;
-              for (auto [regState, regInput] :
-                   llvm::zip(regStates, regInputs)) {
-                // Create an ITE to calculate the next reg state
-                // TODO: we create a lot of ITEs here that will slow things down
-                // - these could be avoided by making init/loop regions concrete
-                nextRegStates.push_back(smt::IteOp::create(
-                    builder, loc, isPosedge, regInput, regState));
-              }
-              newDecls.append(nextRegStates);
+              isPosedgePerClock[clockIdx] = isPosedge;
+            }
+
+            auto regStates =
+                iterArgs.take_front(circuitFuncOp.getNumArguments())
+                    .take_back(numRegs);
+            SmallVector<Value> nextRegStates;
+            for (unsigned regIdx = 0; regIdx < numRegs; ++regIdx) {
+              auto regInput = regInputs[regIdx];
+              auto regState = regStates[regIdx];
+              auto clockIdx = regToClockArgIdx[regIdx];
+              if (!isPosedgePerClock.count(clockIdx) && !clockIndexes.empty())
+                clockIdx = clockIndexes[0];
+              auto isPosedge = isPosedgePerClock[clockIdx];
+              // Create an ITE to calculate the next reg state
+              // TODO: we create a lot of ITEs here that will slow things down
+              // - these could be avoided by making init/loop regions concrete
+              nextRegStates.push_back(smt::IteOp::create(
+                  builder, loc, isPosedge, regInput, regState));
             }
+            newDecls.append(nextRegStates);
           }
 
           // Add the rest of the loop state args
@@ -658,6 +697,21 @@ struct VerifBoundedModelCheckingOpConversion
   SmallVectorImpl<Operation *> &propertylessBMCOps;
 };
 
+struct VerifSymbolicValueOpConversion
+    : OpConversionPattern<verif::SymbolicValueOp> {
+  using OpConversionPattern<verif::SymbolicValueOp>::OpConversionPattern;
+
+  LogicalResult
+  matchAndRewrite(verif::SymbolicValueOp op, OpAdaptor adaptor,
+                  ConversionPatternRewriter &rewriter) const override {
+    Type targetType = typeConverter->convertType(op.getType());
+    if (!targetType)
+      return failure();
+    rewriter.replaceOpWithNewOp<smt::DeclareFunOp>(op, targetType);
+    return success();
+  }
+};
+
 } // namespace
 
 //===----------------------------------------------------------------------===//
@@ -677,8 +731,8 @@ void circt::populateVerifToSMTConversionPatterns(
     bool risingClocksOnly, SmallVectorImpl<Operation *> &propertylessBMCOps) {
   patterns.add<VerifAssertOpConversion, VerifAssumeOpConversion,
                LogicEquivalenceCheckingOpConversion,
-               RefinementCheckingOpConversion>(converter,
-                                               patterns.getContext());
+               RefinementCheckingOpConversion, VerifSymbolicValueOpConversion>(
+      converter, patterns.getContext());
   patterns.add<VerifBoundedModelCheckingOpConversion>(
       converter, patterns.getContext(), names, risingClocksOnly,
       propertylessBMCOps);
@@ -723,13 +777,6 @@ void ConvertVerifToSMTPass::runOnOperation() {
           for (auto argType : bmcOp.getCircuit().getArgumentTypes())
             if (isa<seq::ClockType>(argType))
               numClockArgs++;
-          // TODO: this can be removed once we have a way to associate reg
-          // ins/outs with clocks
-          if (numClockArgs > 1) {
-            op->emitError(
-                "only modules with one or zero clocks are currently supported");
-            return WalkResult::interrupt();
-          }
           SmallVector<mlir::Operation *> worklist;
           int numAssertions = 0;
           op->walk([&](Operation *curOp) {

lib/Tools/circt-bmc/ExternalizeRegisters.cpp

@@ -49,6 +49,7 @@ struct ExternalizeRegistersPass
   DenseMap<StringAttr, SmallVector<StringAttr>> addedInputNames;
   DenseMap<StringAttr, SmallVector<Type>> addedOutputs;
   DenseMap<StringAttr, SmallVector<StringAttr>> addedOutputNames;
+  DenseMap<StringAttr, SmallVector<unsigned>> addedClockPortIndices;
   DenseMap<StringAttr, SmallVector<Attribute>> initialValues;
 
   LogicalResult externalizeReg(HWModuleOp module, Operation *op, Twine regName,
@@ -80,16 +81,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 = {};
@@ -157,6 +148,8 @@ void ExternalizeRegistersPass::runOnOperation() {
               addedOutputs[instanceOp.getModuleNameAttr().getAttr()];
           auto newOutputNames =
               addedOutputNames[instanceOp.getModuleNameAttr().getAttr()];
+          auto childClockPortIndices =
+              addedClockPortIndices[instanceOp.getModuleNameAttr().getAttr()];
           addedInputs[module.getSymNameAttr()].append(newInputs);
           addedInputNames[module.getSymNameAttr()].append(newInputNames);
           addedOutputs[module.getSymNameAttr()].append(newOutputs);
@@ -184,6 +177,24 @@ void ExternalizeRegistersPass::runOnOperation() {
               instanceOp.getInputs(), builder.getArrayAttr(argNames),
               builder.getArrayAttr(resultNames), instanceOp.getParametersAttr(),
               instanceOp.getInnerSymAttr(), instanceOp.getDoNotPrintAttr());
+
+          for (auto [i, clockPortIdx] : llvm::enumerate(childClockPortIndices)) {
+            auto clockVal = newInst.getOperand(clockPortIdx);
+            auto nextVal = newInst.getResult(instanceOp->getNumResults() + i);
+            verif::ClockedByOp::create(builder, instanceOp.getLoc(), clockVal,
+                                       nextVal);
+            if (auto arg = dyn_cast<BlockArgument>(clockVal)) {
+              addedClockPortIndices[module.getSymNameAttr()].push_back(
+                  arg.getArgNumber());
+            } else {
+              // If the clock is not a block argument of the parent module, we
+              // cannot hoist this register's clock association as a direct
+              // module port. `externalizeReg` handles this error case during
+              // the initial externalization step. Here, we safely skip adding
+              // an invalid index to `addedClockPortIndices`.
+            }
+          }
+
           for (auto [output, name] :
                zip(newInst->getResults().take_back(newOutputs.size()),
                    newOutputNames))
@@ -233,6 +244,8 @@ LogicalResult ExternalizeRegistersPass::externalizeReg(
   addedInputNames[module.getSymNameAttr()].push_back(newInputName);
   addedOutputs[module.getSymNameAttr()].push_back(next.getType());
   addedOutputNames[module.getSymNameAttr()].push_back(newOutputName);
+  addedClockPortIndices[module.getSymNameAttr()].push_back(
+      cast<BlockArgument>(clock).getArgNumber());
 
   // Replace the register with newInput and newOutput
   auto newInput = module.appendInput(newInputName, regType).second;
@@ -247,9 +260,13 @@ LogicalResult ExternalizeRegistersPass::externalizeReg(
     auto mux = comb::MuxOp::create(builder, op->getLoc(), regType, reset,
                                    resetValue, next);
     module.appendOutput(newOutputName, mux);
+    builder.setInsertionPointAfter(mux);
+    verif::ClockedByOp::create(builder, op->getLoc(), clock, mux);
   } else {
     // No reset
     module.appendOutput(newOutputName, next);
+    OpBuilder bodyBuilder(module.getBody().front().getTerminator());
+    verif::ClockedByOp::create(bodyBuilder, op->getLoc(), clock, next);
   }
 
   return success();