diff options
3 files changed, 24 insertions, 15 deletions
diff --git a/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala b/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala index e5e65d1d..3199cedf 100644 --- a/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala +++ b/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala @@ -36,8 +36,7 @@ class AssertSubmoduleAssumptions ) def assertAssumption(s: Statement): Statement = s match { - case Verification(Formal.Assume, info, clk, cond, en, msg) => - Verification(Formal.Assert, info, clk, cond, en, msg) + case v: Verification if v.op == Formal.Assume => v.withOp(Formal.Assert) case t => t.mapStmt(assertAssumption) } diff --git a/src/main/scala/firrtl/transforms/formal/ConvertAsserts.scala b/src/main/scala/firrtl/transforms/formal/ConvertAsserts.scala index e49be6eb..b609f685 100644 --- a/src/main/scala/firrtl/transforms/formal/ConvertAsserts.scala +++ b/src/main/scala/firrtl/transforms/formal/ConvertAsserts.scala @@ -19,19 +19,28 @@ object ConvertAsserts extends Transform with DependencyAPIMigration { override def invalidates(a: Transform): Boolean = false - def convertAsserts(stmt: Statement): Statement = stmt match { - case Verification(Formal.Assert, i, clk, pred, en, msg) => - val nPred = DoPrim(PrimOps.Not, Seq(pred), Nil, pred.tpe) - val gatedNPred = DoPrim(PrimOps.And, Seq(nPred, en), Nil, pred.tpe) - val stop = Stop(i, 1, clk, gatedNPred) - msg match { + def convertAsserts(namespace: Namespace, stmt: Statement): Statement = stmt match { + case v: Verification if v.op == Formal.Assert => + val nPred = DoPrim(PrimOps.Not, Seq(v.pred), Nil, v.pred.tpe) + val gatedNPred = DoPrim(PrimOps.And, Seq(nPred, v.en), Nil, v.pred.tpe) + val name = if (v.name.nonEmpty) { v.name } + else { namespace.newName("assert") } + val stop = Stop(v.info, 1, v.clk, gatedNPred, name) + v.msg match { case StringLit("") => stop - case _ => Block(Print(i, msg, Nil, clk, gatedNPred), stop) + case msg => + val printName = namespace.newName(name + "_print") + Block(Print(v.info, msg, Nil, v.clk, gatedNPred, printName), stop) } - case s => s.mapStmt(convertAsserts) + case s => s.mapStmt(convertAsserts(namespace, _)) } def execute(state: CircuitState): CircuitState = { - state.copy(circuit = state.circuit.mapModule(m => m.mapStmt(convertAsserts))) + state.copy(circuit = state.circuit.mapModule { m => + val namespace = Namespace(m) + // make sure the name assert is reserved + if (!namespace.contains("assert")) { namespace.newName("assert") } + m.mapStmt(convertAsserts(namespace, _)) + }) } } diff --git a/src/test/scala/firrtlTests/formal/ConvertAssertsSpec.scala b/src/test/scala/firrtlTests/formal/ConvertAssertsSpec.scala index f21f0878..c315c472 100644 --- a/src/test/scala/firrtlTests/formal/ConvertAssertsSpec.scala +++ b/src/test/scala/firrtlTests/formal/ConvertAssertsSpec.scala @@ -24,11 +24,12 @@ class ConvertAssertsSpec extends FirrtlFlatSpec { |""".stripMargin val ref = preamble + - """ printf(clock, and(not(ne5), not(reset)), "x should not equal 5") - | stop(clock, and(not(ne5), not(reset)), 1) + """ printf(clock, and(not(ne5), not(reset)), "x should not equal 5") : assert_0_print + | stop(clock, and(not(ne5), not(reset)), 1) : assert_0 |""".stripMargin - val outputCS = ConvertAsserts.execute(CircuitState(parse(input), Nil)) + val state = CircuitState(parse(input), Nil) + val outputCS = ConvertAsserts.execute(state) (parse(outputCS.circuit.serialize)) should be(parse(ref)) } @@ -38,7 +39,7 @@ class ConvertAssertsSpec extends FirrtlFlatSpec { |""".stripMargin val ref = preamble + - """ stop(clock, and(not(ne5), not(reset)), 1) + """ stop(clock, and(not(ne5), not(reset)), 1) : assert_0 |""".stripMargin val outputCS = ConvertAsserts.execute(CircuitState(parse(input), Nil)) |