OpenVera 2.0 assertions empower verification

The OVA language provides capabilities to refer to data values in the past, present or future. This enables checks of data values at specific time points. An example of this usage is to check that FIFO output corresponds to input after several operations. In addition, the language provides capabilities to have a non-deterministic variable called a free variable specification, which enables formal verification tools to verify for all possible variable assignments. This provides a shorthand method of asserting all possible values.

Language hierarchy
The OpenVer a 2.0 language is broken down into five main sections or levels. The first level is called Context and is used to help define the scope of the assertions, and the sampling time used. The next level, Directive, is used to specify what properties are to be monitored or checked. The third level consists of Boolean Expressions. The fourth level contains Event Expressions that describe temporal sequences. The last level is Formula Expressions, which are useful to describe how temporal sequences must occur in relation to one another.

Context
The OVA language provides three mechanisms to bind an assertion to a device under test (DUT). The first mechanism uses the module keyword, which binds a specific set of assertions to a design unit. The second mechanism uses the scope keyword, which binds a specific set of assertions to a specific design instance. The third mechanism is to use an absolute path name to uniquely refer to a design signal.

I t is usually necessary to define a sampling clock to determine when to sample the design signals. OVA provides the clock keyword in order to specify when to sample the design signals.

Directives
Directives are statements that define a property that is to be monitored during simulation. Directives need to be placed within the context of a module or an instance, and cannot be placed within a clock grouping. There are two general types of directives that can be used: check and forbid. Positive directives may written; that is, a property that should always be true. In this case the construct check is used. Negative directives may also be written; that is, a property that should never be true. In this case the construct forbid is used.

Boolean expressions
Boolean expressions are used as building blocks to create properties. The expressions are evaluated to be either True or False. OVA supports four-state values -- 0, 1, x, z -- and thes e values can be used in Boolean expressions. All logical operators from the Verilog language are supported within OVA expressions.

Event expressions
Event expressions are very useful for describing sequence of events over time. One can write very powerful descriptions of sequences of events using OVA. It is usually desirable from a debugging perspective to break complex checkers into smaller parts that are checked separately, but jointly imply the original sequence of events. Consider the following example:

"If ready is True intermittently or continuously for 3 clock cycles, then after that transmit must be True within 4 clock cycles, unless reset happened in the meantime."

Figure 1 - OVA code for protocol

The OVA code shown in Figure 1 starts with a module specification "module protocol". This specification implies that all of the statements in this definition should apply to all instances of module protocol. The next line is "clock posedge clk". This specification implies that all events within this grouping should sample their design signals at the rising edge of clk.

The initial sequence that we want to check for is "ready is True intermittently or continuously for 3 clock cycles." Let's first look at:

ready #[1..] ready #[1..] ready

This sequence will succeed whenever ready is high in three clock cycles, which do not need to be consecutive. Figure 2 shows two valid sequences.
Figure 2 -- Valid protocol sequences

In the first waveform, ready is high for three consecutive clock cycles. The start and end time of the event is shown. In the second waveform, ready is high in every other cycle that is also a valid sequence. This condition is necessary but not sufficient. We must also constrain the reset from triggering as well as transmit from going h igh. In order to constrain these signals the istrue construct is used:

istrue (!transmit && !reset) in (ready #[1..] ready #[1..ready);
Now, both transmit and reset are inactive during the ready sequence. Whenever this event succeeds or is matched, we want to check that transmit goes high. We use the matched construct, which is True at the end of the event ready3.

if (matched ready3) then #[1..4] (transmit || reset);

Whenever event ready3 succeeds, then between one and four clock cycles later either transmit goes high or reset goes high. If ready3 never matches, then we do not check the then condition. Only if ready matches do we perform this check. Finally, we use the assert directive to enforce this check during design verification.

Formula expressions
Complex sequence checks can be written using temporal formulas. Temporal formulas are useful to assert how temporal sequences must occur in relation to one another. The temporal formulas can be composed using the following operators:

• followed_by: (ex. X followed_by Y), sequence X must be followed in one clock cycle by formula Y being true
• triggers: (ex. X triggers Y), all sequences of X must be followed in one clock cycle by formula Y being true
• until, wuntil: (ex. X until Y), formula X must stay true until formula Y becomes true
• next, wnext: (ex. next Y), formula Y must be true at the next clock cycle

Consider the example of an arbiter. The OVA code is shown in Figure 3.

Figure 3 - OVA code for arbiter

A possible waveform for the arbiter is shown in Figure 4:

Figure 4 - Arbiter waveform

We want to check for the condition that can occur whenever a grant signal and lock are asserted. If this condition happens, then grant should stay asserted until lock is de-asserted. First we need to check if grant and lock are asserted simultaneously:

if (grant && lock

This condition is true whenever both grant and lock are true at the same falling clock edge. At clock cycle 2 this condition holds. The then clause "grant until !lock" specifies that grant should stay high until lock is de-asserted. At cycle 5 lock is de-asserted, and thus the sequence terminates. The value of grant is immaterial when "!lock" is sampled. Finally, an assert directive is required to ensure the sequence holds for the entire simulation:

assert a_grant : globally f_grant;

Consider another example of a protocol using the triggers construct. Figure 5 shows an example of an assertion for a data transf er protocol. Figure 6 shows the waveform for the protocol.

Figure 5 - OVA code for data transfer

Figure 6 -- Waveform for data transfer protocol

The signal "burst_start" signals the start of a burst mode protocol, "burst_end" signals the end of a burst mode, and transfer is asserted when there is a transfer of data. If reset occurs during data transfer, this should not cause an assertion failure and the sequence is accepted.

All signals within the assertion are relative to the arbiter module because of the module definition module "data_transfer." All signals are sampled on the negative edge of the clock because of the clock definition clock "negedge clk." "Formula f_burst" specifies that whenever there is a start of a burst mode, then transfer should be asserted until the end of the burst mo de transfer. Now, if during this sequence, reset is asserted, although the property would fail, we should not report a failure because it is caused by an external reset. The formula

formula f_burst_r : accept (reset) in f_burst;

specifies that reset is a condition that will cause "f_burst_r" to succeed if reset occurs during the sequence "f_burst." The construct "accept reset in" specifies that the formula is true whenever reset is asserted in the sequence. Finally an assert directive is required to ensure the sequence holds for the entire simulation:

assert a_burst_r : globally f_burst_r;

Consider a third example using the eventually construct. Figure 7 shows the OVA code and Figure 8 shows the waveform diagram.

Figure 7 - OVA code for eventuality construct

Figure 8 -- Waveform using eventually construct

The temporal sequence description

request #[1..3] request

succeeds whenever there are 2 requests separated by 1 through 3 clock cycles. In Figure 8 there is a request at cycle1, and at cycle 3, which is a valid sequence. The construct "triggers" implies that whenever the above sequence holds, then the second formula must also hold one cycle later. The second expression

eventually[3..5] grant

implies that grant must be true 3 to 5 cycles from that time. Finally the formula must be asserted to be true:

assert a_grant : globally f_grant;

The construct globally is used to assert that this formula must always be true.

Summary
The OpenVera 2.0 assertions language is a high-level language for expressing temporal sequences of events. There are powerful constructs available for describing and checking complex protocols for verification in both dynamic and formal verification environments. With OVAs, verification and design engineers can increase productivity and the ability to find design bugs by writing less code to check assertions on their designs.

OpenVera Assertions provide a language platform on which an assertion-based methodology can be constructed. Libraries of assertion intellectual property (IP) can be developed and exchanged to increase verification abstraction and productivity.