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>

1 files changed, 10 insertions, 6 deletions

diff --git a/src/test/scala/firrtlTests/CustomTransformSpec.scala b/src/test/scala/firrtlTests/CustomTransformSpec.scala
index d736ec3c..677aa6ff 100644
--- a/src/test/scala/firrtlTests/CustomTransformSpec.scala
+++ b/src/test/scala/firrtlTests/CustomTransformSpec.scala
@@ -6,12 +6,11 @@ import firrtl.ir.Circuit
 import firrtl._
 import firrtl.passes.Pass
 import firrtl.ir._
-
 import firrtl.stage.{FirrtlSourceAnnotation, FirrtlStage, Forms, RunFirrtlTransformAnnotation}
 import firrtl.options.Dependency
 import firrtl.transforms.{IdentityTransform, LegalizeAndReductionsTransform}
-
 import firrtl.testutils._
+import firrtl.transforms.formal.RemoveVerificationStatements
 
 import scala.reflect.runtime
 
@@ -173,10 +172,15 @@ class CustomTransformSpec extends FirrtlFlatSpec {
         .map(target => new firrtl.stage.transforms.Compiler(target))
         .map(_.flattenedTransformOrder.map(Dependency.fromTransform(_)))
 
-    Seq( (Seq(Dependency[LowFirrtlEmitter]),                                                  Seq(low.last)      ),
-         (Seq(Dependency[LegalizeAndReductionsTransform], Dependency[MinimumVerilogEmitter]), Seq(lowMinOpt.last)),
-         (Seq(Dependency[LegalizeAndReductionsTransform], Dependency[VerilogEmitter]),        Seq(lowOpt.last)    ),
-         (Seq(Dependency[LegalizeAndReductionsTransform], Dependency[SystemVerilogEmitter]),  Seq(lowOpt.last)   )
+    Seq( (Seq(Dependency[LowFirrtlEmitter]),             Seq(low.last)      ),
+         (Seq(Dependency[LegalizeAndReductionsTransform],
+           Dependency[RemoveVerificationStatements],
+           Dependency[MinimumVerilogEmitter]),           Seq(lowMinOpt.last)),
+         (Seq(Dependency[LegalizeAndReductionsTransform],
+           Dependency[RemoveVerificationStatements],
+           Dependency[VerilogEmitter]),                  Seq(lowOpt.last)    ),
+         (Seq(Dependency[LegalizeAndReductionsTransform],
+           Dependency[SystemVerilogEmitter]),            Seq(lowOpt.last)   )
     ).foreach((testOrder _).tupled)
   }