Logic Designers and Verification
Corporate efficiency consultants love to talk about "the dead moose on the table"—the important topic that everyone knows about but no one wants to bring up. In system-on-chip (SoC) verification, there is just such a dead moose: logic designer involvement in verification. All the clichs about designers not wanting to do verification and verification engineers not trusting them to verify don't matter anymore. While a dedicated verification team is essential at the cluster (multi-block) and chip levels, effective, efficient verification of large, complex chips must also involve the designers.
The most compelling reason for this is simply that bugs must be found as early in the development process as possible, when diagnosing and fixing them is fast and inexpensive. Recognizing this, many projects are placing quality requirements on the designers mandating that fewer bugs escape to be found by the verification team. Bugs resolved at the block level involve only the logic designer, minimizing engineering resources and preventing iterations through multiple team members.
In contrast, feeding a bug found in cluster-level simulation back to designers for debug and resolution can take days, stretching into weeks for problems found in chip-level or system-level simulation, acceleration, and emulation. Inevitably, this process takes a lot of time for the designers as well as the verification engineers. Chip-level and system-level verification should be used to find high-level issues, especially those related to hardware-software interaction, not basic RTL bugs.
Benefits for the Logic Designers
Finding as many bugs as possible at the block level directly benefits logic designers as well as the entire verification team. However, designers often develop only minimal block-level simulation tests, usually with a simple stimulus generator written in HDL and manual examination of waveforms to determine correctness. Such an approach finds only very basic design bugs and is not sufficient for SoC projects. Logic designers have to change their ways and become more involved in verification.
Past attempts to convince designers of this have not been very successful. To logic designers, any requirement for more effective block-level verification may look like a large and unfair burden. Trying to convince them to adopt the sort of advanced testbench techniques used at the cluster and chip level has usually not worked. Designers approach verification differently than verification engineers, complementing traditional black-box testing with a white-box approach that reflects their understanding of the design internals.
Recent innovations have led to a new approach dubbed "design with verification" because it integrates the design process with verification while providing a much higher return on designer investment. This approach is based upon several key technologies that provide direct benefit to the logic design team, the overall verification effort, and the SoC project schedule as a whole:
- Early, proactive formal analysis of assertions
- Assertion-based Verification IP (ABVIP) for standard protocols
- Additional formal analysis for functional coverage
- Designer-oriented testbench technology and methodology
- Seamless hardware simulation acceleration
Assertions and Formal
Early, block-level use of assertion-based verification techniques, starting with formal analysis, finds the majority of bugs prior to cluster-level and chip-level simulation. This is made possible both by widespread adoption of assertions and by recent advancements in formal speed and ease of use. Logic designers who had previously resisted placing assertions in their RTL "for the good of the project" adopt assertions much more eagerly when they see the direct benefits of formal analysis for their own block-level efforts.
Today's standard assertion languages—the SVA subset of SystemVerilog and Property Specification Language (PSL)—provide designers tremendous power and flexibility for the specification of their design intent. However, it can take many assertions to capture all the intended behavior for common design structures such as arbiters, FIFOs, power control modules, and standard interfaces. Language-based assertions are complemented by a rich, flexible assertion-checker library and ABVIP. Many common types of assertions can be specified more quickly and easily using these verification components.
ABVIP is especially valuable since it checks for compliance to standard bus protocols with minimal investment required. In the case of a bus bridge, such as OCP-AHB or AXI-AHB, the ABVIP components for the two protocols completely describe all behavior on the bridge interfaces and so can be used for fully automated formal analysis. The result is interface verification in hours rather than weeks or months.
Commercial ABVIP can be supplemented by in-house components for proprietary protocols, capturing critical design intent for easy use across multiple projects. Regardless of the assertion method, with formal analysis designers receive instant feedback showing how assertions can both pass and fail. Best-in-class formal tools provide a wide array of features for assertion debug and visualization to accelerate specification and adoption.
Functional Coverage
Many assertion checkers and ABVIP components contain functional coverage points as well as assertions. Beyond these, it is important for designers to specify functional coverage points in their RTL. Designers know the corner cases of their designs that must be exercised in order to achieve thorough verification. Coverage and assertions are really two sides of the same coin. One common example is a FIFO, which may have an assertion that it should never overflow (accept a write when full) and a coverage point that the FIFO must be filled.
A power control module (PCM) is a more complex example. The PCM supplies the signals necessary to turn off specific regions of a chip, typically to reduce power consumption and prolong battery life. There are several steps required to power down and power up each region, so the PCM might have assertions that power-up and power-down signals be applied in the proper sequence, and functional coverage specifying that all such sequences must be exercised.
1. A power control module (PCM) may require many assertions and coverage points.
Click here for a larger version
Although most commonly associated with simulation, functional coverage also has high value in formal analysis. Extending formal analysis beyond assertions to also target coverage points within the design exercises the design thoroughly at the block level. Formal analysis warns about coverage points that are unreachable, indicating either incorrectly specified functional coverage or design bugs preventing parts of the block from being exercised. The traces provided by formal analysis to exercise reachable coverage points can be run in block-level simulation or used as examples when developing chip-level tests.
