[smt] PropagatePresetAnnotations is now a real prereq (#2325)

1 files changed, 9 insertions, 15 deletions

diff --git a/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala
index 7bc80102..c100da56 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/FirrtlModuleToTransitionSystemSpec.scala
@@ -148,7 +148,7 @@ class FirrtlModuleToTransitionSystemSpec extends AnyFlatSpec {
         |    when en:
         |      o <= UInt<8>(0)
         |""".stripMargin
-    val sys = SMTBackendHelpers.toSys(src)
+    val sys = SMTBackendHelpers.toSys(src, modelUndef = true)
     assert(sys.inputs.length == 2)
     val invalids = sys.inputs.filter(_.name.contains("_invalid"))
     assert(invalids.length == 1)
@@ -192,25 +192,19 @@ class FirrtlModuleToTransitionSystemSpec extends AnyFlatSpec {
     assert(err.getMessage.contains("clk, c.clk"))
   }
 
-  it should "throw an error on async reset" in {
+  it should "throw an error on async reset driving a register" in {
     val err = intercept[AsyncResetException] {
       SMTBackendHelpers.toSys(
         """circuit m:
           |  module m:
+          |    input clock : Clock
           |    input reset : AsyncReset
-          |""".stripMargin
-      )
-    }
-    assert(err.getMessage.contains("reset"))
-  }
-
-  it should "throw an error on casting to async reset" in {
-    val err = intercept[AssertionError] {
-      SMTBackendHelpers.toSys(
-        """circuit m:
-          |  module m:
-          |    input reset : UInt<1>
-          |    node async = asAsyncReset(reset)
+          |    input in : UInt<4>
+          |    output out : UInt<4>
+          |
+          |    reg r : UInt<4>, clock with : (reset => (reset, UInt<8>(0)))
+          |    r <= in
+          |    out <= r
           |""".stripMargin
       )
     }