From fe7754a4ef92b2333f43458e53478e29cedad1c7 Mon Sep 17 00:00:00 2001
From: Albert Magyar
Date: Thu, 25 Jun 2020 13:05:52 -0700
Subject: Add ConvertAsserts transform to map asserts to Verilog-friendly nodes

* ConvertAsserts maps each assert into a gated print-and-stop
* ConvertAsserts is an optional prereq of RemoveVerificationStatements
* ConvertAsserts generates Low FIRRTL
* Drop print for asserts that have an empty message
* Fix scaladoc formatting from review

Co-authored-by: Schuyler Eldridge <schuyler.eldridge@ibm.com>
---
 .../firrtl/transforms/formal/ConvertAsserts.scala  | 39 ++++++++++++++++++++++
 .../formal/RemoveVerificationStatements.scala      |  2 +-
 2 files changed, 40 insertions(+), 1 deletion(-)
 create mode 100644 src/main/scala/firrtl/transforms/formal/ConvertAsserts.scala

(limited to 'src')

diff --git a/src/main/scala/firrtl/transforms/formal/ConvertAsserts.scala b/src/main/scala/firrtl/transforms/formal/ConvertAsserts.scala
new file mode 100644
index 00000000..ddead331
--- /dev/null
+++ b/src/main/scala/firrtl/transforms/formal/ConvertAsserts.scala
@@ -0,0 +1,39 @@
+// See LICENSE for license details.
+
+package firrtl.transforms.formal
+
+import firrtl._
+import firrtl.ir._
+import firrtl.options.Dependency
+
+/** Convert Asserts
+  *
+  * Replaces all Assert nodes with a gated print-and-stop. This effectively
+  * emulates the assert for IEEE 1364 Verilog.
+  */
+object ConvertAsserts extends Transform with DependencyAPIMigration {
+  override def prerequisites = Nil
+  override def optionalPrerequisites = Nil
+  override def optionalPrerequisiteOf = Seq(
+    Dependency[VerilogEmitter],
+    Dependency[MinimumVerilogEmitter],
+    Dependency[RemoveVerificationStatements])
+
+  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 {
+        case StringLit("") => stop
+        case _ => Block(Print(i, msg, Nil, clk, gatedNPred), stop)
+      }
+    case s => s.mapStmt(convertAsserts)
+  }
+
+  def execute(state: CircuitState): CircuitState = {
+    state.copy(circuit = state.circuit.mapModule(m => m.mapStmt(convertAsserts)))
+  }
+}
diff --git a/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala b/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala
index 40626765..72890c07 100644
--- a/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala
+++ b/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala
@@ -19,7 +19,7 @@ class RemoveVerificationStatements extends Transform
   with PreservesAll[Transform] {
 
   override def prerequisites: Seq[TransformDependency] = Seq.empty
-  override def optionalPrerequisites: Seq[TransformDependency] = Seq.empty
+  override def optionalPrerequisites: Seq[TransformDependency] = Seq(Dependency(ConvertAsserts))
   override def optionalPrerequisiteOf: Seq[TransformDependency] =
     Seq( Dependency[VerilogEmitter],
       Dependency[MinimumVerilogEmitter])
-- 
cgit v1.2.3