February 2, 2007 -- Hundreds, if not thousands, of articles have been written to discuss the “verification crisis” for system-on-chip (SOC) designs. The crisis is real: many studies have shown that two or three very expensive silicon iterations are the norm today. Of the many techniques and methodologies that have arisen to improve this situation, few have had more impact than assertion-based verification.
Assertions are, quite simply, expressions of design intent. As architects write chip and system specifications, they make many assumptions about the functionality. As designers write RTL, they develop implementation-level beliefs on how the design should operate and expectations about how neighboring blocks will communicate. Verification engineers document intended and unintended design behavior as part of developing a test plan.
All of the different elements of design intent can be captured with assertions, starting very early in the project schedule. The traditional test plan is replaced by a more comprehensive verification plan identifying which assertions should be written. The architects, designers, and verification engineers should all contribute to this plan. As the assertions are specified, links can be added to tie the plan to the verification results.
There are many methods for specifying assertions, including checker libraries, the VHDL assertion construct, Property Specification Language (PSL), and various proprietary formats. This article focuses on SystemVerilog since this standard language includes sophisticated assertion constructs that have gained wide acceptance. As will be discussed in later sections, these constructs also support functional coverage specification.
The role of assertions
Assertion-based verification is the technique of creating assertions early in the development process and leveraging them throughout the verification effort. Ideally, the designers place assertions in the RTL code for every block. As shown in Figure 1, some of these assertions will involve only the inputs and outputs of the block, while others will involve internal design structures.
Figure 1. Design intent is captured on inputs, outputs, and internal structures.
Assertions that reference only the block I/O are often called “black-box” since they do not directly relate to the internal implementation. Assertions that specify behavior from the inputs to the outputs are termed “end-to-end” since they relate the expected results on the outputs to the values on the inputs. Assertions that reference internal data structures are “white-box” since they are tied to the specific RTL implementation.
Assertions that specify input or output protocols reflect not just a single block, but rather the interaction between the block and its neighbors. Output assertions check that the results from the block agree with what is expected by other blocks receiving the output signals. Conversely, input assertions represent the range of inputs for which the block is designed, serving to screen out illegal inputs from other blocks.
Input assertions are especially important for formal analysis, which can be applied to the block before any testbench or tests have been written. As shown in Figure 2, input assertions are treated as constraints, ensuring that formal analysis considers only legal input combinations. A problem detected by using illegal inputs is generally not of interest to the designer since it’s usually not a true design bug.
Figure 2. Assertions on design inputs are treated as constraints for formal analysis.
For each assertion not converted to a constraint, formal analysis tries either to prove that the assertion can never be violated or to generate a “counter-example” showing how a violation can occur. Some formal tools can generate the counter-example as a test case that can be run in simulation, or directly support use of simulation debuggers. This allows the bug causing the assertion violation to be diagnosed in a familiar environment.
Although many types of blocks can be completely verified by formal analysis, assertion-based verification does not require this. Some types of design intent may be easier to check in a traditional simulation testbench than with assertions. As shown in Figure 3, assertions add value in block-level testbench simulation as well as in formal analysis. In fact, SystemVerilog assertions run equally well and can detect bugs in either environment.
Figure 3. Assertions improve bug detection and diagnosis in block-level simulation.
Most block-level testbenches are developed by designers, who generally do not use high-level verification techniques such as object-oriented programming and constrained-random stimulus generation. Assertions thus provide additional checking beyond the relatively simple testbenches created by designers. Assertions in simulation report any violations as they occur, making it quick and easy to diagnose design bugs.
Although testbenches at the SOC level tend to be more sophisticated than for individual blocks, it is still important to run assertions. As shown in Figure 4, the same assertions used in block-level formal analysis and simulation also run unchanged in full-chip testbench simulation and hardware acceleration or emulation. Chip-level assertions provide two valuable results: faster bug isolation and more thorough verification.
Figure 4. Assertions detect and isolate deeply-buried bugs during chip-level simulation.
A bug buried deep inside a block can take literally thousands of cycles to propagate its effects to the chip output and be detected in the testbench. If an assertion catches this bug at its source, diagnosis time is reduced from hours or even days down to minutes. Further, assertions sometimes detect bugs that would have been missed by the testbench, perhaps because the simulation test stopped before bug effects reached the outputs.
Assertions in SystemVerilog
The standards teams that defined the SystemVerilog language were well aware of the value of assertions in SOC verification. Accordingly, they defined the SystemVerilog Assertions (SVA) subset to provide a flexible yet powerful way for designers and verification engineers to specify assertions. One simple example is the assertion that a FIFO should not be read when it is empty:
assert_no_underflow: assert property (@(posedge clk1)
!(fifo_read && fifo_empty && reset_n));
This assertion reports a violation when the FIFO read signal and FIFO empty signal are both active. In such a case, the data returned will be corrupt since the FIFO does not contain a valid entry to be read. This is a good example of an assertion with high value in chip-level simulation. The FIFO bug can be detected when it occurs instead of when the corrupted data reaches the testbench checkers, perhaps hundreds of cycles later.
SystemVerilog assertions are not limited to checks performed on every clock cycle; complex sequences can be required to set up the conditions for particular errors to be checked. For example, an assertion might apply only for a particular type of incoming packet in a networking chip, so the setup sequence involves decoding the packet header information from the serial input stream. A much simpler example is the following:
devsel_delay: assert property (@(posedge pci_clk)
(!frame_l |=> ##[1:3] !devsel_l ));
This assertion checks the PCI protocol rule that some slave device must respond that it has been selected between 1 and 3 clock cycles after a master starts a new transaction frame. This assertion is an example of a building block for a complete protocol checker. Assertions for each protocol rule and some “helper” RTL code can be combined together into an assertion-based verification IP component for use in simulation, formal analysis, or hardware.
SVA provides many features for assertion specification, some beyond the scope of this article. These include the ability to define local variables valid only within an assertion specification, “liveness” assertions in which something should eventually happen with no strict time bound, and action blocks defining tasks to be executed upon assertion pass or failure. Some of these features may not be supported in all formal analysis tools.
SVA for functional coverage
Another very nice aspect of SVA is that it supports the specification of functional coverage points within the design. Coverage points define conditions that must be exercised for complete verification; assertions specify behavior that must hold for the design to operate correctly. A common language works well due to the similar nature of these two types of specification.
SVA functional coverage points use all the same powerful constructs as assertions, including properties, sequences, local variables, and action blocks. Thus, coverage points can express very specific corner-case conditions with long setup sequences. Further, there are often close relationships between assertions and coverage. Consider the following two coverage points for the PCI protocol rule checked in a previous example:
minimum_devsel: cover property (@(posedge pci_clk)
(!frame_l ##1 !devsel_l ));
maximum_devsel: cover property (@(posedge pci_clk)
(!frame_l ##3 !devsel_l ));
These two cover points ensure that the two extremes of PCI slave device response occur. If one of these points remains uncovered, then verification is not complete. Similarly, functional coverage points can be defined to ensure that FIFO full and empty conditions are hit or that all possible packet types on a network interface are tried. These points can be tracked in any testbench, as shown in Figure 5.
Figure 5. Coverage points assess how well the design is exercised in any testbench.
Sometimes, coverage results for individual tests are interesting. For example, a FIFO full coverage point can be used to validate a test designed to generate data at the maximum rate. More often, composite functional coverage across the entire test suite is most valuable, since it provides a measure of verification progress and is an important factor in deciding when to tape out the design.
As with assertions, functional coverage points should be included in the verification plan from the earliest phases of the SOC project. Architects, designers, and verification engineers should all contribute to this process. As the coverage points are written in the RTL, links can be placed in the plan. This allows coverage results to be reported back against the original plan, clearly showing what verification work remains to be done.
Some formal analysis tools accept SVA functional coverage points as well as assertions. For each coverage point, such a tool will try either to provide that the point can never be reached or to generate a trace showing how to reach it. The former most likely indicates a design bug that is blocking intended behavior; the latter can serve as a good hint on how to hit the coverage point with a simulation test.
SystemVerilog also provide sophisticated constructs for higher-level functional coverage typically included in the testbench code rather than in the RTL. These constructs are not part of SVA and fall outside the scope of this article. It is worth noting, however, that such coverage points should also be included in the verification plan and must be tracked as part of assessing verification completeness.
Assertion-based verification is a key technique for today’s large, complex SOC projects, raising quality and improving overall project productivity. The SVA subset of the standard SystemVerilog language provides mechanisms for easy specification of powerful assertions that can be leveraged in both formal analysis and simulation. By writing assertions as they code the RTL, designers can capture critical intent while it is fresh in their minds.
SVA also supports specification of functional coverage points, thereby verifying that desirable legal conditions are exercised while checking that illegal conditions do not occur. When both assertions and coverage points are included within the SoC verification plan and tracked against this plan, the development team has quantifiable verification metrics to make a tape-out decision with the best chance for first-silicon success.
By Thomas L. Anderson
Thomas is a Product Marketing Director at Cadence Design Systems, Inc. where his responsibilities include formal analysis and assertion-based verification. His previous positions include Director of Technical Marketing in the Verification Group at Synopsys, Vice President of Applications Engineering at 0-In Design Automation, and Vice President of Engineering at Virtual Chips. He has published more than 150 technical articles and presented more than 100 conference talks on topics including advanced verification techniques, formal analysis, SystemVerilog, and design reuse. He holds an MS in Electrical Engineering and Computer Science from MIT and a BS in Computer Systems Engineering from the University of Massachusetts at Amherst.
Go to the Cadence Design Systems, Inc. website to learn more.