User guide

20-8
Using OpenVera Assertions
Checking OVA Code With the Linter Option
The linter option adds predefined rules. Rule violations other than
syntax / semantic errors are not errors in the strict sense of the word,
but are warnings of potential performance issues or differences in
intended and real semantics of the OVA expressions.
The linter option has two sets of rules:
• General Rules (GR) that are applicable to both simulation and
formal verification tools, synthesis tools such as VCS and
verification tools
• Magellan Rules (MR) that are specific to Magellan (or other similar
formal verification tools).
Upon detecting a violation of any one of the rules and normal parsing
errors, the linter will output a message in the same format as the OVA
parser does now. It will prefix the message by ERROR, WARNING
or RECOMMENDATION, depending on the type of message.
The rules as listed next are classified as "e" for ERROR, "w" for
WARNING, and "r" for RECOMMENDATION.
Each rule contains two information blocks. The first one is the error
message text output by the linter. The second provides further
information on the kind of problem identified.
Applying General Rules with VCS
The linter option in VCS is -ova_lint.