User guide

20-16
Using OpenVera Assertions
The problem is that any evaluation attempt that matches on "a" will
remain active till the end of simulation, waiting for (yet another)
occurrence of "b". Most likely this is not intended. Consider rewriting
"e1" to terminate on the first match of "b" as follows:
event e1: a #1 (!b)*[0..] #1 b;
Applying Magellan Rules for Formal Verification
This section describes use of Magellan Rules (MR) for checking OVA
code to be used with formal verification tools such as Magellan.
The compile-time option for enabling MR rules is
-ova_lint_magellan.
Linter General Rule Messages:
This section lists the messages generated by the general rules and
describes the condition that caused the message along with a
recommended alternate model.
MR1: ERROR the unit instance name in a bind statement
is missing. The instance name must be provided.
MR2: WARNING an assertion is stated solely over an
OVA variable value.
Example:
logic [bw-1:0] tmp = 1'b0;
clock posedge clk {
tmp <= c1 ? reg_A :
c2 ? reg_B;
event e: |tmp == 1'b1;
}
assert c: check(tmp);