From 034445e31ec53100abe259d407e62e278fdb50fa Mon Sep 17 00:00:00 2001
From: Kevin Laeufer
Date: Thu, 23 Sep 2021 16:34:28 -0700
Subject: transforms.formal: ensure named statements as output (#2367)

---
 .../formal/AssertSubmoduleAssumptions.scala        |  3 +--
 .../firrtl/transforms/formal/ConvertAsserts.scala  | 27 ++++++++++++++--------
 .../firrtlTests/formal/ConvertAssertsSpec.scala    |  9 ++++----
 3 files changed, 24 insertions(+), 15 deletions(-)

(limited to 'src')

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