ExpandWhens: VerificationStatements should be part of the simlist (#1829)

2 files changed, 22 insertions, 3 deletions

diff --git a/src/main/scala/firrtl/passes/ExpandWhens.scala b/src/main/scala/firrtl/passes/ExpandWhens.scala
index 3c1ff675..4384aca7 100644
--- a/src/main/scala/firrtl/passes/ExpandWhens.scala
+++ b/src/main/scala/firrtl/passes/ExpandWhens.scala
@@ -133,7 +133,9 @@ object ExpandWhens extends Pass {
       case sx: Stop =>
         simlist += (if (weq(p, one)) sx else Stop(sx.info, sx.ret, sx.clk, AND(p, sx.en)))
         EmptyStmt
-      case sx: Verification => if (weq(p, one)) sx else sx.copy(en = AND(p, sx.en))
+      case sx: Verification =>
+        simlist += (if (weq(p, one)) sx else sx.copy(en = AND(p, sx.en)))
+        EmptyStmt
       // Expand conditionally, see comments below
       case sx: Conditionally =>
         /* 1) Recurse into conseq and alt with empty netlist, updated defaults, updated predicate
diff --git a/src/test/scala/firrtlTests/formal/VerificationSpec.scala b/src/test/scala/firrtlTests/formal/VerificationSpec.scala
index 31c54e76..73d1404d 100644
--- a/src/test/scala/firrtlTests/formal/VerificationSpec.scala
+++ b/src/test/scala/firrtlTests/formal/VerificationSpec.scala
@@ -2,10 +2,11 @@
 
 package firrtlTests.formal
 
-import firrtl.{SystemVerilogCompiler}
+import firrtl.{CircuitState, SystemVerilogCompiler, ir}
 import firrtl.testutils.FirrtlFlatSpec
 import logger.{LogLevel, Logger}
-import firrtl.ir
+import firrtl.options.Dependency
+import firrtl.stage.TransformManager
 
 class VerificationSpec extends FirrtlFlatSpec {
   behavior of "Formal"
@@ -77,4 +78,20 @@ class VerificationSpec extends FirrtlFlatSpec {
     assert(ir.Serializer.serialize(c) == "assume(clk, pred, en, \"test \\t test\")")
 
   }
+
+  "VerificationStatements" should "end up at the bottom of the circuit like other simulation statements" in {
+    val compiler = new TransformManager(Seq(Dependency(firrtl.passes.ExpandWhens)))
+    val in =
+      """circuit m :
+        |  module m :
+        |    input clock : Clock
+        |    input a : UInt<8>
+        |    output b : UInt<16>
+        |    b <= a
+        |    assert(clock, eq(a, b), UInt<1>("h1"), "")
+        |""".stripMargin
+    val afterExpandWhens = compiler.transform(CircuitState(firrtl.Parser.parse(in), Seq())).circuit.serialize
+    val lastLine = afterExpandWhens.split("\n").last
+    assert(lastLine.trim.startsWith("assert"))
+  }
 }