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>

3 files changed, 9 insertions, 0 deletions

diff --git a/src/main/scala/firrtl/passes/CheckFlows.scala b/src/main/scala/firrtl/passes/CheckFlows.scala
index b4ce4d5f..3a9cc212 100644
--- a/src/main/scala/firrtl/passes/CheckFlows.scala
+++ b/src/main/scala/firrtl/passes/CheckFlows.scala
@@ -105,6 +105,10 @@ object CheckFlows extends Pass {
         case (s: Stop) =>
           check_flow(info, mname, flows, SourceFlow)(s.en)
           check_flow(info, mname, flows, SourceFlow)(s.clk)
+        case (s: Verification) =>
+          check_flow(info, mname, flows, SourceFlow)(s.clk)
+          check_flow(info, mname, flows, SourceFlow)(s.pred)
+          check_flow(info, mname, flows, SourceFlow)(s.en)
         case _ =>
       }
       s foreach check_flows_e(info, mname, flows)
diff --git a/src/main/scala/firrtl/passes/CheckTypes.scala b/src/main/scala/firrtl/passes/CheckTypes.scala
index 5173b8c4..601ee524 100644
--- a/src/main/scala/firrtl/passes/CheckTypes.scala
+++ b/src/main/scala/firrtl/passes/CheckTypes.scala
@@ -310,6 +310,10 @@ object CheckTypes extends Pass {
             errors.append(new PrintfArgNotGround(info, mname))
           if (wt(sx.clk.tpe) != wt(ClockType)) errors.append(new ReqClk(info, mname))
           if (wt(sx.en.tpe) != wt(ut)) errors.append(new EnNotUInt(info, mname))
+        case sx: Verification =>
+          if (wt(sx.clk.tpe) != wt(ClockType)) errors.append(new ReqClk(info, mname))
+          if (wt(sx.pred.tpe) != wt(ut)) errors.append(new PredNotUInt(info, mname))
+          if (wt(sx.en.tpe) != wt(ut)) errors.append(new EnNotUInt(info, mname))
         case sx: DefMemory => sx.dataType match {
           case AnalogType(w) => errors.append(new IllegalAnalogDeclaration(info, mname, sx.name))
           case t =>
diff --git a/src/main/scala/firrtl/passes/ExpandWhens.scala b/src/main/scala/firrtl/passes/ExpandWhens.scala
index 32fec4ed..75aad29a 100644
--- a/src/main/scala/firrtl/passes/ExpandWhens.scala
+++ b/src/main/scala/firrtl/passes/ExpandWhens.scala
@@ -156,6 +156,7 @@ object ExpandWhens extends Pass {
       case sx: Stop =>
         simlist += (if (weq(p, one)) sx else Stop(sx.info, sx.ret, sx.clk, AND(p, sx.en)))
         EmptyStmt
+      case sx: Verification => if (weq(p, one)) sx else sx.copy(en = AND(p, sx.en))
       // Expand conditionally, see comments below
       case sx: Conditionally =>
         /* 1) Recurse into conseq and alt with empty netlist, updated defaults, updated predicate