OpenVera 2.0 assertions empower verification

OpenVera 2.0 assertions empower verification
By Bruce Greene, EEdesign
April 16, 2002 (1:22 p.m. EST)
URL: http://www.eetimes.com/story/OEG20020410S0047

Assertion-based verification has become important because current verification techniques are inadequate at catching errors and eliminating them. Consider the case where you have embedded a core in a system-on-a-chip (SoC) design. If you are just checking signals at the chip level, then you may not catch a bug that is caused by an improper protocol to the embedded core. If the protocols were constantly being monitored, then when the violation occurs, the simulation would immediately respond with an assertion failure -- and the real cause of the problem can be investigated.

Assertions are created to describe design specifications. Assertions can describe undesirable behaviors or specific behaviors that are required to complete a test plan. These assertions can then be checked in either dynamic simulation or formal verification.

OpenVera Assertions (OVAs) are part of the OpenVera hardware verification language, which is available under an open sou rce license. The open source model has proven to provide a path for fast time-to-market with innovation and contribution from multiple sources. SoC design teams, verification teams and EDA developers can access OpenVera by downloading the Language Reference Manual (LRM) from the OpenVera web site.

Assertions in OpenVera 2.0 provide a clear mechanism to describe sequences of events and to test for their occurrence. This method is more concise and intuitive than the procedural descriptions provided by hardware description languages (HDLs) such as Verilog. In addition, OVAs have built-in functions to minimize the amount of code that you need to write. With the expressive power of OVAs, complex protocol assertions can be described in much fewer lines of code than with HDL-based assertions. With clear definitions and less code, verification is more productive.

OVAs can be checked dynamically during simulation, and they can be targeted for proofs by formal verificat ion tools. With this unified support, designers can specify once and use in multiple verification environments. Additionally, OVAs can be used to specify functionality to simulate and measure functional coverage.

OVAs provide language capabilities to build and reuse libraries of pre-built assertions. This macro capability provides a mechanism to build a reusable library of assertions, which can be shared within groups or among the OpenVera community. With a library of assertions, designers will be able to reuse the prior specifications and raise the level of abstraction of the specification.

Features of OpenVera assertions
OVAs are declarative, with semantics that are formally based on the theories of regular expression and linear temporal logic. These two theories provide a powerful combination for expressing common hardware activities, such as sequencing, invariants and finite state machine operations.

OVAs are implicitly and concurrently evaluated during all of verification. In dyna mic verification, the assertions would be evaluated continuously. Each assertion is evaluated at every time step, and its status is updated by the state of simulation. If an assertion completes, then its result can be logged and displayed in a GUI environment. With this implicit evaluation, any overhead of starting, processing and evaluating assertions is a natural feature and does not require any action by the user.

The language includes features to express the following:

Basic events and sequencing to specify the order of events

Time bounded sequences with references to past and future

Composite sequences using logic connectives

Repetition of sequences

Conditional sequences with conditions to hold during sequences

User specified single or multiple clocks

Data storing and checking during sequences

Parameterized library of specifications

Formula expressions based upon linear temporal logic

Asynchronous abort and accept mechanisms for expressions

The OVA language in OpenVera has been designed to support hierarchical verification. Any assertion can be either checked as an assertion, or assumed as a given property of the design. With this capability, assumptions that are used to verify a sub-block can be reused as checks when that sub-block is instantiated at a higher level. This forms a hierarchical proof to enable sub-block verification independent of the enclosing design.

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

Asynchronous set and resets can be added to any expression by prepending accept or reject with a triggering Boolean expression. This provides a mechanism to abort or complete the assertion when an asynchronous condition occurs.

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.

Bruce Greene is a technical marketing manager in Synopsys' Verification Technology group. Previously, Greene worked as a Field application engineer at C Level Design selling and supporting the synthesis and simulation products. Prior to that, he worked as a corporate application engineer in the Nanometer Analysis and Test group at Synopsys, Inc.