User guide
20-9
Using OpenVera Assertions
If used without any Verilog design file, only the OVA files are analyzed
(including bind statements), and potential problems are reported. The
command is:
vcs ova_files_list -ova_lint
If used with Verilog and OVA files (or inlined OVA), the compilation
proceeds normally while detailed linting analysis is also done. If no
fatal error is found, the simulation can go ahead and any
recommendations from the linter can be incorporated for later runs.
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
suggested remedy.
GR1: WARNING "assert forbid" used on an event that
contains an "if" without an "else".
Example:
event e: if a then #1 b;
assert c: forbid(e);
Whenever "a" is false, the assertion will fail because the "if - then"
implication is satisfied. This may not be, however, what is intended.
A modification to consider is to change the event definition as follows:
event e: a #1 b;
GR2: WARNING "ended" or "matched" is used on an
event that contains an "if" without an "else"
Example:
event e1: if a then #1 b;
event e2: if ended e1 then #1 c;