By Didier Ribault and Stephen Bailey
The military and its associated industries historically have been the primary motivators and innovators of high technology. Today, more than ever, there is an emphasis on instrumentation that delivers unprecedented precision and accuracy.
These quality-critical electronic systems are sensitive to correct functionality because errors in avionics systems may have severe consequences; human lives depend on the proper functioning of aircraft electronics. As well, the success of tactical operations depends on electronic devices that dependably behave as expected.
Thales Airborne Systems in Paris, a supplier of onboard systems and equipment for civil and military aircraft, has adopted an assertion-based verification (ABV) approach to design verification of field-programmable gate arrays (FPGAs). Making this procedure practical was standardizing on the Property Specification Language (PSL) and developing tools that support ABV.
The value of assertion-based verification centers on debug productivity and design quality. Assertions speed up the debug process by identifying errors close to or at their source. As shown in Figure 1, assertions open verification to white-box testing by creating an unlimited number of observation points throughout the design. White-box testing provides full visibility and controllability of the internal structure and implementation of a design, making it easy to observe results as verification progresses and immediately report any discrepancies. Our experience indicates that the time we saved in debugging problems compensates for the time spent adding assertions to the design.
Assertions also improve design quality by exposing bugs that might otherwise have gone undetected. Assertions identify problems before they propagate to a primary output. With debug productivity balancing the cost of adding assertions, the increase in quality remains as the net benefit of assertion-based verification.
Engineers chose the Property Specification Language as the assertion and property language for three reasons. First, PSL is a standard language with a proven history supporting simulation and formal verification tools. Second, the language defines how it works with the VHSIC Hardware Description Language (VHDL), ensuring that the PSL syntax is familiar to users of VHDL. This reduces the time for designers and verification engineers to learn PSL. Third, the semantic definition of PSL is rigorous and based on a formal specification of the language itself.
Functional verification of FPGAs is a crucial task at Thales Airborne Systems where VHDL is used for register-transfer-level (RTL) design. Traditionally, the verification process includes writing the testbench, Boolean assertions, running the simulation, and analyzing waveforms and output files to determine the results. Thales experts have used several commercial simulators within FPGA design verification flows.
VHDL supports writing simple Boolean assertions, which consist of expressions that evaluate true or false. The assertion holds when the expression evaluates true. There is no temporal component to the expression (property) being checked. Simulation can stop when a VHDL Boolean assertion fails, which facilitates debugging the problem. For example, an assertion that ensures mutual exclusion of two signals (both cannot be high at the same time) is described by the following code:
assert not(a and b) report “A and B not mutually exclusive” severity ERROR;
VHDL, however, does not support complex temporal assertions to check for correct sequences of events separated by a known, variable, or unknown number of cycles. Fortunately, Property Specification Language does support the specification of very complex temporal properties. PSL provides the ability to specify properties to monitor even the most complex bus protocol transactions.
Recognizing that designers and verification engineers have unique desires and constraints, Property Specification Language supports two use modes. Designers typically want to specify their properties, assertions, and coverage directives within the context of their HDL code.
Conversely, verification engineers typically are prohibited from touching synthesizable RTL code. Also, designers may develop a common library of assertion monitors or checkers. For these situations, PSL defines how properties can be specified external to the RTL code in vunits and bound to the design. The following code is an example of inlined PSL code and the use of vunits:
PSL A1: assert never
(a and b);
vunit mutex(bind_2_entity) {
A1 : assert never(a and b);
}
The properties in this example look familiar because it is the mutual exclusion check. Here we use the never operator, which checks to ensure that the specified sequence does not occur. The name in parenthesis after the vunit name (mutex) denotes a VHDL entity to which this vunit will be bound to all instances of mutex. It is also possible to bind only to a specific instance.
Simulators dynamically evaluate assertions to ensure they hold throughout the simulation. However, assertion-based verification with simulation does not replace functional analysis of RTL code and simulation results. It is complementary. Therefore, our current functional verification flow is not replaced; it is augmented by the addition of ABV into the flow.
Construction of the VHDL testbench continues to be the central aspect of our functional verification process.
The VHDL testbench writes assertions and drives simulations; assertions monitor the state of the design to ensure correct functionality. The quality of results in using assertion-based verification in verification depends on the quality of support and integration of Property Specification Language within the simulation environment.
PSL and dynamic simulation
Because assertions identify problems close to or at their sources, a main benefit of assertion-based verification is eliminating or reducing the tedious and painstaking task of back tracing to the root cause of problems. However, our evaluation also revealed the importance of tool support to facilitate the debug process.
The state of assertions over time can be displayed analogous to a Boolean signal waveform in the wave window. Passes and failures are identified as a function of time. Signals referenced in the specification of the assertion should be displayed as “children” of the assertion to help identify the signal responsible for violating the property specification. Figure 2 shows how one simulator, Questa from Mentor Graphics Corp. in Wilsonville, Ore., helps visualize and debug assertions over time in a wave window.
In figure 2, the green triangle indicates when an assertion passed. The low blue line indicates that the assertion is not active, while a high green line indicates it is active. An inverted red triangle indicates that an assertion has failed. The bottom pane in the window displays the assertion that failed, the time the assertion began evaluation, and three signals and their values at the time of failure. Note that this assertion refers to five signals (exclusive of clk and reset_n). The three signals specified in the debug pane have values different from that specified by the property for that point in the property’s evaluation. Therefore, one of these three signals is most likely the cause of the assertion failure.
Assertions also should be linked easily to the source code as it is not possible to remember the exact property specification. If the assertion fails a few cycles after the cause, it is easy to get from the assertion failure to a dataflow or logic browser that assists in tracing back the causality of a signal that has an incorrect value.
Questa provides links to the assertion declaration in the source. Double clicking on the assertion failure in the wave window automatically activates the Questa dataflow window, where signal causality can be graphically traced back through the design connectivity. Figure 3 shows the Questa dataflow window and the trace back for the rw input pin.
After simulation has completed, a global report provides information whether an assertion was attempted and the number of times it has passed or failed during simulation. It is important to know whether your simulator reports vacuous successes grouped with all assertion successes, reports them separately, or leaves it for the user to infer. Questa only reports successes if the entire property matches; it does not count vacuous successes.
The assertion report provides a quick analysis of design and verification quality, especially in regression testing. Assertion-based verification provides more accurate reports on the coverage of verification tests by using the Property Specification Language cover directive and viewing and analyzing the functional coverage information reported from the simulation run. This is particularly well adapted for protocol and control functionality.
Cover directives indicate when a specific set of events has occurred during verification. While PSL cover directives can be used creatively to gather additional functional coverage information, assertion coverage is not as well suited for capturing data value oriented coverage. For example, if it is important to know which addresses were read and written during verification, then one cover directive would be necessary for each combination of legal address and read and write transactions. An 8-bit address space would require 512 cover directives.
Thales Airborne Systems develops intellectual property blocks for internal reuse. Embedding assertions within the RTL code facilitates integration of these IP blocks, as assertions ensure proper integration and use of the IP and free the system verification from the burden of reverifying the IP block functionality. Designers can use assertion-based verification to provide an active means to check that IP assumptions and restrictions at the interfaces to IP blocks are not violated (by another designer).
Didier Ribault is with the Thales Airborne Systems Aerospace Division in Paris. Stephen Bailey is with Mentor Graphics in Longmont, Colo.
