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

diff --git a/src/main/resources/META-INF/services/firrtl.options.RegisteredTransform b/src/main/resources/META-INF/services/firrtl.options.RegisteredTransform
index 638404be..bb72d45c 100644
--- a/src/main/resources/META-INF/services/firrtl.options.RegisteredTransform
+++ b/src/main/resources/META-INF/services/firrtl.options.RegisteredTransform
@@ -2,3 +2,4 @@ firrtl.transforms.DeadCodeElimination
 firrtl.transforms.CheckCombLoops
 firrtl.passes.InlineInstances
 firrtl.passes.clocklist.ClockListTransform
+firrtl.transforms.formal.AssertSubmoduleAssumptions