User guide

20-4
Using OpenVera Assertions
How Sequences Are Tested Using the assert Directive
Testing starts with a temporal assertion file, which contains the
descriptions of the sequences and instructions for how they should
be tested. OVA is designed to resemble Verilog with similar data
types, operators, and lexical conventions.
A typical temporal assertion file consists mostly of temporal
expressions in OVA units. These temporal expressions are the
descriptions of the event sequences. Events are values or changes
in value of any OVA signal. Temporal expressions can be combined
to form longer or more complex expressions. The language supports
not only linear sequences but logical and conditional combinations.
When you instantiate the OVA unit, you connect the OVA signals to
Verilog variables and nets. You cannot connect OVA signals to Verilog
named events.The basic instruction for testing is a temporal
assertion. Assertions specify an expression or combination of
expressions to be tested. Assertions come in two forms: check, which
succeeds when the simulation matches the expression, and forbid,
which succeeds when the simulation does not match.
The temporal expressions and assertions must also be associated
with a clock that specifies when the assertions are to be tested.
Different assertions can be associated with different clocks. A clock
can be defined as posedge, negedge, or any edge of a signal; or
based on a temporal expression. Also, asynchronous events can use
the simulation time as a clock.
An assertion can be associated with all instances of a specified
module or limited to a specific instance.
Example 20-1 shows an example temporal assertion file. It tests for
a simple sequence of values (4, 6, 9, 3) on the device’s output bus.