smt: run DeadCodeElimination after PropagatePresetAnnotations (#2036)

2 files changed, 39 insertions, 13 deletions

diff --git a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
index 145b5b0f..9c309917 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
@@ -10,18 +10,8 @@ import firrtl.options.Dependency
 import firrtl.passes.PassException
 import firrtl.stage.Forms
 import firrtl.stage.TransformManager.TransformDependency
-import firrtl.transforms.PropagatePresetAnnotations
-import firrtl.{
-  ir,
-  CircuitState,
-  DependencyAPIMigration,
-  MemoryArrayInit,
-  MemoryInitValue,
-  MemoryScalarInit,
-  Namespace,
-  Transform,
-  Utils
-}
+import firrtl.transforms.{DeadCodeElimination, PropagatePresetAnnotations}
+import firrtl.{CircuitState, DependencyAPIMigration, MemoryArrayInit, MemoryInitValue, MemoryScalarInit, Namespace, Transform, Utils, ir}
 import logger.LazyLogging
 
 import scala.collection.mutable
@@ -67,9 +57,12 @@ object FirrtlToTransitionSystem extends Transform with DependencyAPIMigration {
   // Verilog emission passes.
   // Ideally we would go in and enable the [[PropagatePresetAnnotations]] to only depend on LowForm.
   private val presetPass = new PropagatePresetAnnotations
+  // We also need to run the DeadCodeElimination since PropagatePresets does not remove possible remaining
+  // AsyncReset nodes.
+  private val deadCodeElimination = new DeadCodeElimination
   override protected def execute(state: CircuitState): CircuitState = {
     // run the preset pass to extract all preset registers and remove preset reset signals
-    val afterPreset = presetPass.execute(state)
+    val afterPreset = deadCodeElimination.execute(presetPass.execute(state))
     val circuit = afterPreset.circuit
     val presetRegs = afterPreset.annotations.collect {
       case PresetRegAnnotation(target) if target.module == circuit.main => target.ref
diff --git a/src/test/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystemPassSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystemPassSpec.scala
new file mode 100644
index 00000000..7dc5298c
--- /dev/null
+++ b/src/test/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystemPassSpec.scala
@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: Apache-2.0
+
+package firrtl.backends.experimental.smt
+
+import firrtl.annotations.{CircuitTarget, PresetAnnotation}
+import firrtl.options.Dependency
+import firrtl.testutils.LeanTransformSpec
+
+class FirrtlToTransitionSystemPassSpec extends LeanTransformSpec(Seq(Dependency(firrtl.backends.experimental.smt.FirrtlToTransitionSystem))) {
+  behavior of "FirrtlToTransitionSystem"
+
+  it should "support preset wires" in {
+    // In order to give registers an initial wire, we use preset annotated resets.
+    // When using a wire instead of an input (which has the advantage of working regardless of the
+    // module hierarchy), we need to initialize it in order to get through the wire initialization check.
+    // In Chisel this generates a node which needs to be removed.
+
+    val src = """circuit ModuleAB :
+      |  module ModuleAB :
+      |    input clock : Clock
+      |    node _T = asAsyncReset(UInt<1>("h0"))
+      |    node preset = _T
+      |    reg REG : UInt<1>, clock with :
+      |      reset => (preset, UInt<1>("h0"))
+      |    assert(clock, UInt(1), not(REG), "REG == 0")
+      |""".stripMargin
+    val anno = PresetAnnotation(CircuitTarget("ModuleAB").module("ModuleAB").ref("preset"))
+
+    val result = compile(src, List(anno))
+    val sys = result.annotations.collectFirst{ case TransitionSystemAnnotation(sys) => sys }.get
+    assert(sys.states.head.init.isDefined)
+  }
+}