[circt-bmc] Add simple initial value support to ExternalizeRegisters (#…

…7728)

lib/Tools/circt-bmc/ExternalizeRegisters.cpp

@@ -52,6 +52,7 @@ void ExternalizeRegistersPass::runOnOperation() {
   DenseMap<StringAttr, SmallVector<StringAttr>> addedInputNames;
   DenseMap<StringAttr, SmallVector<Type>> addedOutputs;
   DenseMap<StringAttr, SmallVector<StringAttr>> addedOutputNames;
+  DenseMap<StringAttr, SmallVector<Attribute>> initialValues;
 
   // Iterate over all instances in the instance graph. This ensures we visit
   // every module, even private top modules (private and never instantiated).
@@ -93,9 +94,37 @@ void ExternalizeRegistersPass::runOnOperation() {
             regOp.emitError("registers with reset signals not yet supported");
             return signalPassFailure();
           }
-          if (regOp.getInitialValue()) {
-            regOp.emitError("registers with initial values not yet supported");
-            return signalPassFailure();
+          mlir::Attribute initState;
+          if (auto initVal = regOp.getInitialValue()) {
+            // Find the seq.initial op where the initial value is defined and
+            // fetch the operation inside that defines the value
+            auto initialOp =
+                regOp.getInitialValue().getDefiningOp<seq::InitialOp>();
+            if (!initialOp) {
+              regOp.emitError("registers with initial values not directly "
+                              "defined by a seq.initial op not yet supported");
+              return signalPassFailure();
+            }
+            auto index = cast<OpResult>(initVal).getResultNumber();
+            auto initValDef =
+                initialOp->getRegion(0).front().getTerminator()->getOperand(
+                    index);
+            // If it's defined by a constant op then just fetch the constant
+            // value - otherwise unsupported
+            if (auto constantOp = initValDef.getDefiningOp<hw::ConstantOp>()) {
+              // Fetch value from constant op - leave removing the dead op to
+              // DCE
+              initState = constantOp.getValueAttr();
+            } else {
+              regOp.emitError("registers with initial values not directly "
+                              "defined by a hw.constant op in a seq.initial op "
+                              "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(
@@ -114,6 +143,7 @@ void ExternalizeRegistersPass::runOnOperation() {
           }
           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);
@@ -136,6 +166,8 @@ void ExternalizeRegistersPass::runOnOperation() {
           addedInputNames[module.getSymNameAttr()].append(newInputNames);
           addedOutputs[module.getSymNameAttr()].append(newOutputs);
           addedOutputNames[module.getSymNameAttr()].append(newOutputNames);
+          initialValues[module.getSymNameAttr()].append(
+              initialValues[instanceOp.getModuleNameAttr().getAttr()]);
           SmallVector<Attribute> argNames(instanceOp.getArgNamesAttr().begin(),
                                           instanceOp.getArgNamesAttr().end());
           SmallVector<Attribute> resultNames(
@@ -173,6 +205,10 @@ void ExternalizeRegistersPass::runOnOperation() {
       module->setAttr(
           "num_regs",
           IntegerAttr::get(IntegerType::get(&getContext(), 32), numRegs));
+
+      module->setAttr("initial_values",
+                      ArrayAttr::get(&getContext(),
+                                     initialValues[module.getSymNameAttr()]));
     }
   }
 }

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

@@ -27,13 +27,39 @@ hw.module @reg_with_reset(in %clk: !seq.clock, in %rst: i1, in %in: i32, out out
 
 // -----
 
-hw.module @reg_with_initial(in %clk: !seq.clock, in %in: i32, out out: i32) {
+hw.module @reg_with_indirect_initial(in %clk: !seq.clock, in %in: i32, out out: i32) {
+  %init = seq.initial () {
+    %c0_i32 = hw.constant 0 : i32
+    %sum = comb.add %c0_i32, %c0_i32 : i32
+    seq.yield %sum : i32
+  } : () -> !seq.immutable<i32>
+
+  // expected-error @below {{registers with initial values not directly defined by a hw.constant op in a seq.initial op not yet supported}}
+  %1 = seq.compreg %in, %clk initial %init : i32
+  hw.output %1 : i32
+}
+
+// -----
+
+hw.module @reg_with_argument_initial(in %clk: !seq.clock, in %in: i32, in %init: !seq.immutable<i32>, out out: i32) {
+  // expected-error @below {{registers with initial values not directly defined by a seq.initial op not yet supported}}
+  %1 = seq.compreg %in, %clk initial %init : i32
+  hw.output %1 : i32
+}
+
+// -----
+
+hw.module @init_emitter(out out: !seq.immutable<i32>) {
   %init = seq.initial () {
     %c0_i32 = hw.constant 0 : i32
     seq.yield %c0_i32 : i32
   } : () -> !seq.immutable<i32>
+  hw.output %init : !seq.immutable<i32>
+}
 
-  // expected-error @below {{registers with initial values not yet supported}}
+hw.module @reg_with_instance_initial(in %clk: !seq.clock, in %in: i32, out out: i32) {
+  %init = hw.instance "foo" @init_emitter () -> (out: !seq.immutable<i32>)
+  // expected-error @below {{registers with initial values not directly defined by a seq.initial op not yet supported}}
   %1 = seq.compreg %in, %clk initial %init : i32
   hw.output %1 : i32
 }

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

@@ -1,6 +1,6 @@
 // RUN: circt-opt --externalize-registers %s | FileCheck %s
 
-// CHECK:  hw.module @comb(in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, out {{.+}} : i32) attributes {num_regs = 0 : i32} {
+// CHECK:  hw.module @comb(in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, out {{.+}} : i32) attributes {initial_values = [], num_regs = 0 : i32} {
 // CHECK:    [[ADD:%.+]] = comb.add [[IN0]], [[IN1]]
 // CHECK:    hw.output [[ADD]]
 // CHECK:  }
@@ -9,17 +9,25 @@ hw.module @comb(in %in0: i32, in %in1: i32, out out: i32) {
   hw.output %0 : i32
 }
 
-// CHECK:  hw.module @one_reg(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in [[OLD_REG:%.+]] : i32, out {{.+}} : i32, out {{.+}} : i32) attributes {num_regs = 1 : i32} {
+// CHECK:  hw.module @one_reg(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:    [[INITIAL:%.+]] = seq.initial() {
+// CHECK:      [[C0_I32:%.+]] = hw.constant 0 : i32
+// CHECK:      seq.yield [[C0_I32]]
+// CHECK:    }
 // CHECK:    hw.output [[OLD_REG]], [[ADD]]
 // CHECK:  }
 hw.module @one_reg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32) {
   %0 = comb.add %in0, %in1 : i32
-  %single_reg = seq.compreg %0, %clk : i32
+  %1 = seq.initial() {
+    %c0_i32 = hw.constant 0 : i32
+    seq.yield %c0_i32 : i32
+  } : () -> !seq.immutable<i32>
+  %single_reg = seq.compreg %0, %clk initial %1 : i32
   hw.output %single_reg : i32
 }
 
-// CHECK:  hw.module @two_reg(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 {num_regs = 2 : i32} {
+// CHECK:  hw.module @two_reg(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:  }
@@ -30,7 +38,7 @@ hw.module @two_reg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32
   hw.output %2 : i32
 }
 
-// CHECK:  hw.module @named_regs(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 {num_regs = 2 : i32} {
+// CHECK:  hw.module @named_regs(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:  }
@@ -41,7 +49,7 @@ hw.module @named_regs(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out:
   hw.output %secondreg : i32
 }
 
-// CHECK:  hw.module @nested_reg(in [[CLK:%.+]] : !seq.clock, in [[IN0:%.+]] : i32, in [[IN1:%.+]] : i32, in [[OLD_REG:%.+]] : i32, out {{.+}} : i32, out {{.+}} : i32) attributes {num_regs = 1 : i32} {
+// CHECK:  hw.module @nested_reg(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:    [[INSTOUT:%.+]], [[INSTREG:%.+]] = hw.instance "one_reg" @one_reg(clk: [[CLK]]: !seq.clock, in0: [[IN0]]: i32, in1: [[IN1]]: i32, {{.+}}: [[OLD_REG]]: i32) -> ({{.+}}: i32, {{.+}}: i32)
 // CHECK:    hw.output [[INSTOUT]], [[INSTREG]]
 // CHECK:  }
@@ -50,7 +58,7 @@ 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 {num_regs = 2 : 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.output %top_reg_state, [[INSTREG]], [[INSTOUT]]
 // CHECK:  }
@@ -59,3 +67,23 @@ hw.module @nested_nested_reg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, ou
   %top_reg = seq.compreg %0, %clk : i32
   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:    [[INITIAL:%.+]]:2 = seq.initial() {
+// CHECK:      [[C0_I32:%.+]] = hw.constant 0 : i32
+// CHECK:      [[C42_I32:%.+]] = hw.constant 42 : i32
+// CHECK:      seq.yield [[C0_I32]], [[C42_I32]]
+// CHECK:    }
+// CHECK:    hw.output [[IN]], [[IN]], [[IN]]
+// CHECK:  }
+hw.module @different_initial_values(in %clk: !seq.clock, in %in : i32) {
+  %0:2 = seq.initial () {
+    %c0_i32 = hw.constant 0 : i32
+    %c42_i32 = hw.constant 42 : i32
+    seq.yield %c0_i32, %c42_i32 : i32, i32
+  } : () -> (!seq.immutable<i32>, !seq.immutable<i32>)
+  %reg0 = seq.compreg %in, %clk initial %0#0 : i32
+  %reg1 = seq.compreg %in, %clk initial %0#1  : i32
+  %reg2 = seq.compreg %in, %clk : i32
+  hw.output
+}