From a6d53c9df25dba7da9d923faff9bf3c32f71b2d9 Mon Sep 17 00:00:00 2001
From: Kevin Laeufer
Date: Fri, 7 Aug 2020 10:33:29 -0700
Subject: ExpandWhens: VerificationStatements should be part of the simlist
 (#1829)

---
 src/main/scala/firrtl/passes/ExpandWhens.scala      |  4 +++-
 .../scala/firrtlTests/formal/VerificationSpec.scala | 21 +++++++++++++++++++--
 2 files changed, 22 insertions(+), 3 deletions(-)

(limited to 'src')

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"))
+  }
 }
-- 
cgit v1.2.3