[circt-bmc] Support seq.firreg with sync reset

integration_test/circt-bmc/seq.mlir

@@ -70,3 +70,18 @@ hw.module @Counter_with_reset(in %clk: !seq.clock, in %rst: i1, out count: i3) {
   verif.assert %neq : i1
   hw.output %reg : i3
 }
+
+// Check that reset of firreg can be triggered
+// RUN: circt-bmc %s -b 4 --module Counter_with_firreg_sync_reset --shared-libs=%libz3 | FileCheck %s --check-prefix=FIRREGRESET
+// FIRREGRESET: Assertion can be violated!
+hw.module @Counter_with_firreg_sync_reset(in %clk: !seq.clock, in %rst: i1, out count: i3) {
+  %c0_i3 = hw.constant 0 : i3
+  %c1_i3 = hw.constant 1 : i3
+  %regPlusOne = comb.add %reg, %c1_i3 : i3
+  %reg = seq.firreg %regPlusOne clock %clk reset sync %rst, %c0_i3 preset 1 : i3
+  %neq = comb.icmp bin ne %reg, %c0_i3 : i3
+  // Assertion will be violated if the reset is triggered
+  verif.assert %neq : i1
+  hw.output %reg : i3
+}
+

lib/Tools/circt-bmc/ExternalizeRegisters.cpp

@@ -43,18 +43,24 @@ struct ExternalizeRegistersPass
     : public circt::impl::ExternalizeRegistersBase<ExternalizeRegistersPass> {
   using ExternalizeRegistersBase::ExternalizeRegistersBase;
   void runOnOperation() override;
-};
-} // namespace
 
-void ExternalizeRegistersPass::runOnOperation() {
-  auto &instanceGraph = getAnalysis<hw::InstanceGraph>();
-  DenseSet<Operation *> handled;
+private:
   DenseMap<StringAttr, SmallVector<Type>> addedInputs;
   DenseMap<StringAttr, SmallVector<StringAttr>> addedInputNames;
   DenseMap<StringAttr, SmallVector<Type>> addedOutputs;
   DenseMap<StringAttr, SmallVector<StringAttr>> addedOutputNames;
   DenseMap<StringAttr, SmallVector<Attribute>> initialValues;
 
+  LogicalResult externalizeReg(HWModuleOp module, Operation *op, Twine regName,
+                               Value clock, Attribute initState, Value reset,
+                               bool isAsync, Value resetValue, Value next);
+};
+} // namespace
+
+void ExternalizeRegistersPass::runOnOperation() {
+  auto &instanceGraph = getAnalysis<hw::InstanceGraph>();
+  DenseSet<Operation *> handled;
+
   // Iterate over all instances in the instance graph. This ensures we visit
   // every module, even private top modules (private and never instantiated).
   for (auto *startNode : instanceGraph) {
@@ -86,12 +92,7 @@ void ExternalizeRegistersPass::runOnOperation() {
       }
       module->walk([&](Operation *op) {
         if (auto regOp = dyn_cast<seq::CompRegOp>(op)) {
-          if (!isa<BlockArgument>(regOp.getClk())) {
-            regOp.emitError("only clocks directly given as block arguments "
-                            "are supported");
-            return signalPassFailure();
-          }
-          mlir::Attribute initState;
+          mlir::Attribute initState = {};
           if (auto initVal = regOp.getInitialValue()) {
             // Find the constant op that defines the reset value in an initial
             // block (if it exists)
@@ -111,40 +112,36 @@ void ExternalizeRegistersPass::runOnOperation() {
                               "not yet supported");
               return signalPassFailure();
             }
-          } else {
-            // If there's no initial value just add a unit attribute to maintain
-            // one-to-one correspondence with module ports
-            initState = mlir::UnitAttr::get(&getContext());
           }
-          addedInputs[module.getSymNameAttr()].push_back(regOp.getType());
-          addedOutputs[module.getSymNameAttr()].push_back(
-              regOp.getInput().getType());
-          OpBuilder builder(regOp);
-          auto regName = regOp.getName();
-          StringAttr newInputName, newOutputName;
-          if (regName && !regName.value().empty()) {
-            newInputName = builder.getStringAttr(regName.value() + "_state");
-            newOutputName = builder.getStringAttr(regName.value() + "_input");
-          } else {
-            newInputName =
-                builder.getStringAttr("reg_" + Twine(numRegs) + "_state");
-            newOutputName =
-                builder.getStringAttr("reg_" + Twine(numRegs) + "_input");
+          Twine regName = regOp.getName() && !(regOp.getName().value().empty())
+                              ? regOp.getName().value()
+                              : "reg_" + Twine(numRegs);
+
+          if (failed(externalizeReg(module, op, regName, regOp.getClk(),
+                                    initState, regOp.getReset(), false,
+                                    regOp.getResetValue(), regOp.getInput()))) {
+            return signalPassFailure();
           }
-          addedInputNames[module.getSymNameAttr()].push_back(newInputName);
-          addedOutputNames[module.getSymNameAttr()].push_back(newOutputName);
-          initialValues[module.getSymNameAttr()].push_back(initState);
-
-          regOp.getResult().replaceAllUsesWith(
-              module.appendInput(newInputName, regOp.getType()).second);
-          if (auto reset = regOp.getReset()) {
-            auto resetValue = regOp.getResetValue();
-            auto mux = builder.create<comb::MuxOp>(
-                regOp.getLoc(), regOp.getType(), reset, resetValue,
-                regOp.getInput());
-            module.appendOutput(newOutputName, mux);
-          } else {
-            module.appendOutput(newOutputName, regOp.getInput());
+          regOp->erase();
+          ++numRegs;
+          return;
+        }
+        if (auto regOp = dyn_cast<seq::FirRegOp>(op)) {
+          mlir::Attribute initState = {};
+          if (auto preset = regOp.getPreset()) {
+            // Get preset value as initState
+            initState = mlir::IntegerAttr::get(
+                mlir::IntegerType::get(&getContext(), preset->getBitWidth()),
+                *preset);
+          }
+          Twine regName = regOp.getName().empty() ? "reg_" + Twine(numRegs)
+                                                  : regOp.getName();
+
+          if (failed(externalizeReg(module, op, regName, regOp.getClk(),
+                                    initState, regOp.getReset(),
+                                    regOp.getIsAsync(), regOp.getResetValue(),
+                                    regOp.getNext()))) {
+            return signalPassFailure();
           }
           regOp->erase();
           ++numRegs;
@@ -210,3 +207,50 @@ void ExternalizeRegistersPass::runOnOperation() {
     }
   }
 }
+
+LogicalResult ExternalizeRegistersPass::externalizeReg(
+    HWModuleOp module, Operation *op, Twine regName, Value clock,
+    Attribute initState, Value reset, bool isAsync, Value resetValue,
+    Value next) {
+  if (!isa<BlockArgument>(clock)) {
+    op->emitError("only clocks directly given as block arguments "
+                  "are supported");
+    return failure();
+  }
+
+  OpBuilder builder(op);
+  auto result = op->getResult(0);
+  auto regType = result.getType();
+
+  // If there's no initial value just add a unit attribute to maintain
+  // one-to-one correspondence with module ports
+  initialValues[module.getSymNameAttr()].push_back(
+      initState ? initState : mlir::UnitAttr::get(&getContext()));
+
+  StringAttr newInputName(builder.getStringAttr(regName + "_state")),
+      newOutputName(builder.getStringAttr(regName + "_next"));
+  addedInputs[module.getSymNameAttr()].push_back(regType);
+  addedInputNames[module.getSymNameAttr()].push_back(newInputName);
+  addedOutputs[module.getSymNameAttr()].push_back(next.getType());
+  addedOutputNames[module.getSymNameAttr()].push_back(newOutputName);
+
+  // Replace the register with newInput and newOutput
+  auto newInput = module.appendInput(newInputName, regType).second;
+  result.replaceAllUsesWith(newInput);
+  if (reset) {
+    if (isAsync) {
+      // Async reset
+      op->emitError("registers with an async reset are not yet supported");
+      return failure();
+    }
+    // Sync reset
+    auto mux = builder.create<comb::MuxOp>(op->getLoc(), regType, reset,
+                                           resetValue, next);
+    module.appendOutput(newOutputName, mux);
+  } else {
+    // No reset
+    module.appendOutput(newOutputName, next);
+  }
+
+  return success();
+}

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

@@ -54,3 +54,11 @@ hw.module @reg_with_instance_initial(in %clk: !seq.clock, in %in: i32, out out:
   %1 = seq.compreg %in, %clk initial %init : i32
   hw.output %1 : i32
 }
+
+// -----
+hw.module @firreg_with_async_reset(in %clk: !seq.clock, in %rst: i1, in %in: i32, out out: i32) {
+  %c0_i32 = hw.constant 0 : i32
+  // expected-error @below {{registers with an async reset are not yet supported}}
+  %1 = seq.firreg %in clock %clk reset async %rst, %c0_i32 : i32
+  hw.output %1 : i32
+}

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

@@ -58,8 +58,8 @@ hw.module @nested_reg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out:
   hw.output %0 : i32
 }
 
-// CHECK:  hw.module @nested_nested_reg(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in %single_reg_state : i32, in %top_reg_state : i32, out {{.+}} : i32, out single_reg_input : i32, out top_reg_input : i32) attributes {initial_values = [0 : i32, unit], num_regs = 2 : i32} {
-// CHECK:    [[INSTOUT:%.+]], [[INSTREG:%.+]] = hw.instance "nested_reg" @nested_reg(clk: [[CLK]]: !seq.clock, in0: [[IN0]]: i32, in1: [[IN1]]: i32, single_reg_state: %single_reg_state: i32) -> ({{.+}}: i32, single_reg_input: i32)
+// CHECK:  hw.module @nested_nested_reg(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in %single_reg_state : i32, in %top_reg_state : i32, out {{.+}} : i32, out single_reg_next : i32, out top_reg_next : i32) attributes {initial_values = [0 : i32, unit], num_regs = 2 : i32} {
+// CHECK:    [[INSTOUT:%.+]], [[INSTREG:%.+]] = hw.instance "nested_reg" @nested_reg(clk: [[CLK]]: !seq.clock, in0: [[IN0]]: i32, in1: [[IN1]]: i32, single_reg_state: %single_reg_state: i32) -> ({{.+}}: i32, single_reg_next: i32)
 // CHECK:    hw.output %top_reg_state, [[INSTREG]], [[INSTOUT]]
 // CHECK:  }
 hw.module @nested_nested_reg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32) {
@@ -68,7 +68,7 @@ hw.module @nested_nested_reg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, ou
   hw.output %top_reg : i32
 }
 
-// CHECK:  hw.module @different_initial_values(in [[CLK:%.+]] : !seq.clock, in [[IN:%.+]] : i32, in %reg0_state : i32, in %reg1_state : i32, in %reg2_state : i32, out reg0_input : i32, out reg1_input : i32, out reg2_input : i32) attributes {initial_values = [0 : i32, 42 : i32, unit], num_regs = 3 : i32} {
+// CHECK:  hw.module @different_initial_values(in [[CLK:%.+]] : !seq.clock, in [[IN:%.+]] : i32, in %reg0_state : i32, in %reg1_state : i32, in %reg2_state : i32, out reg0_next : i32, out reg1_next : i32, out reg2_next : i32) attributes {initial_values = [0 : i32, 42 : i32, unit], num_regs = 3 : i32} {
 // CHECK:    [[INITIAL:%.+]]:2 = seq.initial() {
 // CHECK:      [[C0_I32:%.+]] = hw.constant 0 : i32
 // CHECK:      [[C42_I32:%.+]] = hw.constant 42 : i32
@@ -98,3 +98,48 @@ hw.module @reg_with_reset(in %clk: !seq.clock, in %rst: i1, in %in: i32, out out
   %1 = seq.compreg %in, %clk reset %rst, %c0_i32 : i32
   hw.output %1 : i32
 }
+
+// -----
+
+// CHECK:  hw.module @one_firreg(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in [[OLD_REG:%.+]] : i32, out {{.+}} : i32, out {{.+}} : i32) attributes {initial_values = [0 : i32], num_regs = 1 : i32} {
+// CHECK:    [[ADD:%.+]] = comb.add [[IN0]], [[IN1]]
+// CHECK:    hw.output [[OLD_REG]], [[ADD]]
+// CHECK:  }
+hw.module @one_firreg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32) {
+  %0 = comb.add %in0, %in1 : i32
+  %single_reg = seq.firreg %0 clock %clk preset 0 : i32
+  hw.output %single_reg : i32
+}
+
+// CHECK:  hw.module @compreg_and_firreg(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in [[OLD_REG0:%.+]] : i32, in [[OLD_REG1:%.+]] : i32, out {{.+}} : i32, out {{.+}} : i32, out {{.+}} : i32) attributes {initial_values = [unit, unit], num_regs = 2 : i32} {
+// CHECK:    [[ADD:%.+]] = comb.add [[IN0]], [[IN1]]
+// CHECK:    hw.output [[OLD_REG1]], [[ADD]], [[OLD_REG0]]
+// CHECK:  }
+hw.module @compreg_and_firreg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32) {
+  %0 = comb.add %in0, %in1 : i32
+  %1 = seq.compreg %0, %clk : i32
+  %2 = seq.firreg %1 clock %clk : i32
+  hw.output %2 : i32
+}
+
+// CHECK:  hw.module @named_firregs(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in %firstreg_state : i32, in %secondreg_state : i32, out {{.+}} : i32, out {{.+}} : i32, out {{.+}} : i32) attributes {initial_values = [unit, unit], num_regs = 2 : i32} {
+// CHECK:    [[ADD:%.+]] = comb.add [[IN0]], [[IN1]]
+// CHECK:    hw.output %secondreg_state, [[ADD]], %firstreg_state
+// CHECK:  }
+hw.module @named_firregs(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32) {
+  %0 = comb.add %in0, %in1 : i32
+  %firstreg = seq.firreg %0 clock %clk : i32
+  %secondreg = seq.firreg %firstreg clock %clk : i32
+  hw.output %secondreg : 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
+// CHECK:    hw.output [[OLD_REG1]], [[MUX1]]
+// CHECK:  }
+hw.module @firreg_with_sync_reset(in %clk: !seq.clock, in %rst: i1, in %in: i32, out out: i32) {
+  %c0_i32 = hw.constant 0 : i32
+  %1 = seq.firreg %in clock %clk reset sync %rst, %c0_i32 : i32
+  hw.output %1 : i32
+}