diff options
| -rw-r--r-- | src/main/scala/firrtl/passes/ExpandWhens.scala | 4 | ||||
| -rw-r--r-- | src/test/scala/firrtlTests/formal/VerificationSpec.scala | 21 |
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")) + } } |