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, 3 insertions, 0 deletions

diff --git a/src/main/antlr4/FIRRTL.g4 b/src/main/antlr4/FIRRTL.g4
index 39988e18..f0ea5b10 100644
--- a/src/main/antlr4/FIRRTL.g4
+++ b/src/main/antlr4/FIRRTL.g4
@@ -107,6 +107,9 @@ stmt
   | 'printf(' exp exp StringLit ( exp)* ')' info?
   | 'skip' info?
   | 'attach' '(' exp+ ')' info?
+  | 'assert' '(' exp exp exp StringLit ')' info?
+  | 'assume' '(' exp exp exp StringLit ')' info?
+  | 'cover' '(' exp exp exp StringLit ')' info?
   ;
 
 memField