User guide

20-61
Using OpenVera Assertions
The parallel_case and full_case statements enable their own
type of case check on the associated case statement and disable the
other type unless both are present.
The no_case statement disables any case checking on that case
statement.
The following rules govern assertion pragmas:
• These assertions verify the correct operation of case statements.
They are triggered any time the case statement is executed. That
is, no sampling of signals by a clock takes effect.
• The same pragma may be applied multiple times within a module.
Each appearance will be considered an invocation of the assertion
for its associated statement.
• If no such pragma assertion is associated with a case statement
then the default setting established by an // ova command takes
effect.
• Each // ova pragma may contain only one assertion terminated
by “;”.
• Multiple case pragmas can be associated with a case statement,
each on a separate line.
• The no_case pragma takes precedence over any other
specification.