From 8322316a2f7c7fe7dad72f413e75d6b4600823f0 Mon Sep 17 00:00:00 2001 From: Tom Alcorn Date: Tue, 23 Jun 2020 13:12:05 -0700 Subject: 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 --- src/main/antlr4/FIRRTL.g4 | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/main/antlr4') 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 -- cgit v1.2.3