Basic model checking API (#1653)

* Add assume, assert, cover statements
* Assert submodule assumptions
* Add warning when removing verification statements
* Remove System Verilog behaviour emitter warning
* Add option to disable AssertSubmoduleAssumptions
* Document verification statements in the spec

The syntax for the new statements is

    assert(clk, cond, en, msg)
    assume(clk, cond, en, msg)
    cover(clk, cond, en, msg)

With assert as a representative example, the semantics is as follows:
`clk` is the clock, `cond` is the expression being asserted, `en` is the
enable signal (if `en` is low then the assert is not checked) and `msg`
is a string message intended to be reported as an error message by the
model checker if the assertion fails.

In the Verilog emitter, the new statements are handled by a new
`formals` map, which groups the statements by clock domain. All model
checking statements are then emitted within the context of an `ifdef
FORMAL` block, which allows model checking tools (like Symbiyosys) to
utilize the statements while keeping them out of synthesis flows.

Co-authored-by: Albert Magyar <albert.magyar@gmail.com>

5 files changed, 131 insertions, 1 deletions

diff --git a/src/main/scala/firrtl/transforms/DeadCodeElimination.scala b/src/main/scala/firrtl/transforms/DeadCodeElimination.scala
index b8cfa54e..4182e496 100644
--- a/src/main/scala/firrtl/transforms/DeadCodeElimination.scala
+++ b/src/main/scala/firrtl/transforms/DeadCodeElimination.scala
@@ -154,6 +154,10 @@ class DeadCodeElimination extends Transform
         Seq(clk, en).flatMap(getDeps(_)).foreach(ref => depGraph.addPairWithEdge(circuitSink, ref))
       case Print(_, _, args, clk, en) =>
         (args :+ clk :+ en).flatMap(getDeps(_)).foreach(ref => depGraph.addPairWithEdge(circuitSink, ref))
+      case s: Verification =>
+        for (expr <- Seq(s.clk, s.pred, s.en)) {
+          getDeps(expr).foreach(ref => depGraph.addPairWithEdge(circuitSink, ref))
+        }
       case Block(stmts) => stmts.foreach(onStmt(_))
       case ignore @ (_: IsInvalid | _: WDefInstance | EmptyStmt) => // do nothing
       case other => throw new Exception(s"Unexpected Statement $other")
@@ -256,6 +260,7 @@ class DeadCodeElimination extends Transform
           else decl
         case print: Print => deleteIfNotEnabled(print, print.en)
         case stop: Stop => deleteIfNotEnabled(stop, stop.en)
+        case formal: Verification => deleteIfNotEnabled(formal, formal.en)
         case con: Connect =>
           val node = getDeps(con.loc) match { case Seq(elt) => elt }
           if (deadNodes.contains(node)) EmptyStmt else con
diff --git a/src/main/scala/firrtl/transforms/LegalizeClocks.scala b/src/main/scala/firrtl/transforms/LegalizeClocks.scala
index 333eb096..f439fdc9 100644
--- a/src/main/scala/firrtl/transforms/LegalizeClocks.scala
+++ b/src/main/scala/firrtl/transforms/LegalizeClocks.scala
@@ -45,6 +45,10 @@ object LegalizeClocksTransform {
         val node = DefNode(s.info, namespace.newTemp, s.clk)
         val sx = s.copy(clk = WRef(node))
         Block(Seq(node, sx))
+      case s: Verification if illegalClockExpr(s.clk) =>
+        val node = DefNode(s.info, namespace.newTemp, s.clk)
+        val sx = s.copy(clk = WRef(node))
+        Block(Seq(node, sx))
       case other => other
     }
 
diff --git a/src/main/scala/firrtl/transforms/RemoveWires.scala b/src/main/scala/firrtl/transforms/RemoveWires.scala
index 0504c19d..33daa8ce 100644
--- a/src/main/scala/firrtl/transforms/RemoveWires.scala
+++ b/src/main/scala/firrtl/transforms/RemoveWires.scala
@@ -124,7 +124,7 @@ class RemoveWires extends Transform with DependencyAPIMigration {
               netlist(we(expr)) = (Seq(ValidIf(Utils.zero, UIntLiteral(BigInt(0), width), expr.tpe)), info)
             case _ => otherStmts += invalid
           }
-        case other @ (_: Print | _: Stop | _: Attach) =>
+        case other @ (_: Print | _: Stop | _: Attach | _: Verification) =>
           otherStmts += other
         case EmptyStmt => // Dont bother keeping EmptyStmts around
         case block: Block => block.foreach(onStmt)
diff --git a/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala b/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala
new file mode 100644
index 00000000..7370fcfb
--- /dev/null
+++ b/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala
@@ -0,0 +1,68 @@
+
+package firrtl.transforms.formal
+
+import firrtl.ir.{Circuit, Formal, Statement, Verification}
+import firrtl.stage.TransformManager.TransformDependency
+import firrtl.{CircuitState, DependencyAPIMigration, Transform}
+import firrtl.annotations.NoTargetAnnotation
+import firrtl.options.{PreservesAll, RegisteredTransform, ShellOption}
+
+
+/**
+  * Assert Submodule Assumptions
+  *
+  * Converts `assume` statements to `assert` statements in all modules except
+  * the top module being compiled. This avoids a class of bugs in which an
+  * overly restrictive assume in a child module can prevent the model checker
+  * from searching valid inputs and states in the parent module.
+  */
+class AssertSubmoduleAssumptions extends Transform
+  with RegisteredTransform
+  with DependencyAPIMigration
+  with PreservesAll[Transform] {
+
+  override def prerequisites: Seq[TransformDependency] = Seq.empty
+  override def optionalPrerequisites: Seq[TransformDependency] = Seq.empty
+  override def optionalPrerequisiteOf: Seq[TransformDependency] =
+    firrtl.stage.Forms.MidEmitters
+
+  val options = Seq(
+    new ShellOption[Unit](
+      longOption = "no-asa",
+      toAnnotationSeq = (_: Unit) => Seq(
+        DontAssertSubmoduleAssumptionsAnnotation),
+      helpText = "Disable assert submodule assumptions" ) )
+
+  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 t => t.mapStmt(assertAssumption)
+  }
+
+  def run(c: Circuit): Circuit = {
+    c.mapModule(mod => {
+      if (mod.name != c.main) {
+        mod.mapStmt(assertAssumption)
+      } else {
+        mod
+      }
+    })
+  }
+
+  def execute(state: CircuitState): CircuitState = {
+    val noASA = state.annotations.contains(
+      DontAssertSubmoduleAssumptionsAnnotation)
+    if (noASA) {
+      logger.info("Skipping assert submodule assumptions")
+      state
+    } else {
+      state.copy(circuit = run(state.circuit))
+    }
+  }
+}
+
+case object AssertSubmoduleAssumptionsAnnotation extends NoTargetAnnotation {
+  val transform = new AssertSubmoduleAssumptions
+}
+
+case object DontAssertSubmoduleAssumptionsAnnotation extends NoTargetAnnotation
diff --git a/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala b/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala
new file mode 100644
index 00000000..9bf4f779
--- /dev/null
+++ b/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala
@@ -0,0 +1,53 @@
+
+package firrtl.transforms.formal
+
+import firrtl.ir.{Circuit, EmptyStmt, Statement, Verification}
+import firrtl.{CircuitState, DependencyAPIMigration, MinimumVerilogEmitter, Transform, VerilogEmitter}
+import firrtl.options.{Dependency, PreservesAll, StageUtils}
+import firrtl.stage.TransformManager.TransformDependency
+
+
+/**
+  * Remove Verification Statements
+  *
+  * Replaces all verification statements in all modules with the empty statement.
+  * This is intended to be required by the Verilog emitter to ensure compatibility
+  * with the Verilog 2001 standard.
+  */
+class RemoveVerificationStatements extends Transform
+  with DependencyAPIMigration
+  with PreservesAll[Transform] {
+
+  override def prerequisites: Seq[TransformDependency] = Seq.empty
+  override def optionalPrerequisites: Seq[TransformDependency] = Seq.empty
+  override def optionalPrerequisiteOf: Seq[TransformDependency] =
+    Seq( Dependency[VerilogEmitter],
+      Dependency[MinimumVerilogEmitter])
+
+  private var removedCounter = 0
+
+  def removeVerification(s: Statement): Statement = s match {
+    case _: Verification => {
+      removedCounter += 1
+      EmptyStmt
+    }
+    case t => t.mapStmt(removeVerification)
+  }
+
+  def run(c: Circuit): Circuit = {
+    c.mapModule(mod => {
+      mod.mapStmt(removeVerification)
+    })
+  }
+
+  def execute(state: CircuitState): CircuitState = {
+    val newState = state.copy(circuit = run(state.circuit))
+    if (removedCounter > 0) {
+      StageUtils.dramaticWarning(s"$removedCounter verification statements " +
+        "were removed when compiling to Verilog because the basic Verilog " +
+        "standard does not support them. If this was not intended, compile " +
+        "to System Verilog instead using the `-X sverilog` compiler flag.")
+    }
+    newState
+  }
+}