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>

2 files changed, 121 insertions, 0 deletions

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
+  }
+}