Skip to content

Commit

Permalink
[patch] Clarify cover string argument as comment not message.
Browse files Browse the repository at this point in the history
This is different than the explanatory message argument on
assert and assume statements.
  • Loading branch information
dtzSiFive committed Jan 20, 2023
1 parent 51c7f71 commit 58b9779
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 5 deletions.
2 changes: 2 additions & 0 deletions revision-history.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,8 @@ revisionHistory:
be preserved by a FIRRTL compiler
- Add Compiler Implementation Details documenting Lower Types pass
- Allow out-of-bounds errors to be caught at compile time.
- Clarify the string argument for cover is a comment, not a message
as it is for assert and assume.
# Information about the old versions. This should be static.
oldVersions:
- version: 1.1.0
Expand Down
12 changes: 7 additions & 5 deletions spec.md
Original file line number Diff line number Diff line change
Expand Up @@ -1435,11 +1435,12 @@ Format strings support the following escape characters:
To facilitate simulation, model checking and formal methods, there are three
non-synthesizable verification statements available: assert, assume and
cover. Each type of verification statement requires a clock signal, a predicate
signal, an enable signal and an explanatory message string literal. The
predicate and enable signals must have single bit unsigned integer type. When an
assert is violated the explanatory message may be issued as guidance. The
explanatory message may be phrased as if prefixed by the words "Verifies
that\...".
signal, an enable signal and a string literal. The predicate and enable
signals must have single bit unsigned integer type. Assert and assume use the
string as an explanatory message. For cover statements the string indicates a
suggested comment. When an assert or assume is violated the explanatory
message may be issued as guidance. The explanatory message may be phrased as
if prefixed by the words "Verifies that\...".

Backends are free to generate the corresponding model checking constructs in the
target language, but this is not required by the FIRRTL specification. Backends
Expand Down Expand Up @@ -1494,6 +1495,7 @@ The cover statement verifies that the predicate is true on the rising edge of
some clock cycle when the enable is true. In other words, it directs the model
checker to find some way to make both enable and predicate true at some time
step.
The string argument may be emitted as a comment with the cover.

``` firrtl
wire clk: Clock
Expand Down

0 comments on commit 58b9779

Please sign in to comment.