Using formal verification to create robust IP

Given the criticality of IP in today's designs, it is vital that an IP provider thoroughly verify each design before it is used in SoC projects. This is equally true for designers providing blocks for reuse within their company, often via an internal design repository, and commercial providers. A designer's job may hinge upon how well his or her blocks can be leveraged by other projects in the company. A commercial IP provider's very existence relies on positive customer experience and a good reputation.

SoC designers evaluating IP also know the important of verification, but it can be very hard to assess verification quality for a block designed by someone else. Today, this assessment is accomplished by inquiring about past user experience and evaluating the verification methods used by the IP provider. As this article will discuss, current methods leave some gaps in IP verification and therefore some shortfalls in the metrics used to gauge verification thoroughness.

This article presents the technique of formal analysis as a superior method to verify an IP block under all possible user scenarios, and to thereby produce a higher-quality reusable design. This article also explains how formal verification relies on assertions of designer intent, some generated automatically and some specified explicitly by the designers, and how these assertions assist with IP verification using both simulation and formal methods.

Traditional IP verification

As shown in Figure 1, most IP is verified in the same way that most chips are verified: by using a suite of self-checking simulation tests to provide stimulus to the design and to ensure that the design produces the expected results. Once the designer completes the IP block, either the designer or a dedicated verification engineer develops a testbench around the block to provide stimulus generation and results checking. Next, the engineer develops a series of tests that use these capabilities to verify the design.

Figure 1 — Traditional standalone IP verification relies exclusively on manual and automatic simulation tools

Traditionally, the IP team develops a test plan for all the features to be verified, checking off each feature as the appropriate tests are written, debugged and run successfully. Today, the team is more likely to use a testbench automation tool to generate constrained-random stimulus, which can exercise corner-case behavior that would be hard to hit with explicit tests. Constrained-random tests are especially effective for generating variable sequences of processor instructions and bus transactions.

Whatever the mix of hand-written and automatic tests, any simulation-based method requires metrics so that the development team can assess the thoroughness of the verification. For RTL-based designs, code coverage is the traditional answer. More recently, designer-specified functional coverage points have become more common to supplement code coverage. These metrics have the advantage of directly correlating to design functionality and therefore having more meaning to the engineers.

The combination of simulation-based testing and coverage metrics is a powerful way to verify an IP design, but it inherently has holes. Simulation, by its very nature, only exercises a tiny percentage of all possible design behavior. Each individual test resets the design to a known state and then applies a series of changes to the inputs. Even across an extensive test suite, many legal input sequences are never exercised. Formal analysis is the only way to dramatically improve verification thoroughness.

Automatic formal analysis

The process of formal verification is easy to initiate, since it begins with automatic analysis of the design and extraction of assertions for certain important types of design properties. This step, sometimes called implied intent verification, uses formal analysis to find proofs or counter-examples for these assertions. A proof means that the assertion is always correct; a counter-example is a demonstration of the conditions under which the assertion can be violated.

These assertions represent complex sequential design properties that identify corner-case design errors, especially valuable in the early stages of RTL development. Therefore, IP designers should run a formal verification tool as soon as each RTL block has been coded, and whenever changes are made. The tool analyzes the RTL for every applicable instance of a design element, extracts all the relevant assertions, and performs formal analysis on these assertions. The automatic assertions can include:

• No dead (unreachable) code
• No uninitialized memory elements
• No constant signals
• No constant state vector bits
• No unreachable finite state machine (FSM) states
• No single FSM deadlocks
• No pair-wise FSM deadlocks
• No bus contention
• No floating buses
• No array-bound violations
• No Verilog full-case synthesis pragma errors
• No Verilog parallel-case synthesis pragma errors

Clock intent verification

Perhaps the most valuable automatic assertions are those that check correctness of multi-clock designs. Many IP blocks, especially those that implement external interfaces, contain portions of logic running on independent, asynchronous clocks. For example, most PCI blocks allow connection to a chip running at a frequency unrelated to the PCI clock. Other bus protocols extract their clocks from incoming data, so there is no relationship at all between the interface clock and the rest of the chip.

Experienced IP designers know that meta-stability is a real concern for designs with multiple clock domains. Whenever a signal passes from one clock domain to another, care must be taken to include an effective synchronizer so that meta-stability does not produce incorrect data in the receiving clock domain. Designers must take additional steps to ensure that multiple signals (such as bits of a bus) crossing clock domains do not fall out of correlation in the receiving domain.

Proper multi-clock design is greatly simplified by the automatic analysis of clock intent verification (CIV). This approach definitively identifies most types of multi-clock design errors and provides detailed warnings about suspicious logic. The CIV process starts with a structural analysis of an RTL design, tracing all clocks and resets from the state elements. This process can automatically identify:

• All asynchronous clock domains in the design
• All control and data signals crossing between clock domains
• Any domain-crossing signals that have missing or incorrect synchronizers
• Any synchronizers that have the potential for glitches on their inputs
• Any signals that have fan-outs to multiple synchronizers
• Any independently synchronized signals that reconverge in the receiving clock domain
• Any clock domains whose reset signals are not properly synchronized
• Any gated or derived clocks with glitch potential

• Assertions that multi-bit signals crossing clock domains must always be Gray-coded
• Assertions that signals with synchronizers remain stable long enough to be detected in the receiving clock domain
• Assertions that signals without synchronizers (such as data buses) are held stable during the time that the signals are sampled in the receiving clock domain

Although formal analysis is an exhaustive technology, in practice not all assertions can be proven in complex designs. For this reason, CIV also generates the three types of assertions in a form suitable for simulation. If a proof cannot be found, but the assertion runs with no violations throughout a test suite of many millions or even billions of cycles, then the designers gain a high degree of confidence in the correctness of their multi-clock design.

Designer-specified assertions

Automatic assertions, while very effective at eliminating many IP design problems, cannot find all types of errors. Assertions represent designer intent, and only certain types of intent can be extracted automatically from RTL. IP design (and verification) engineers can specify their own assertions, sometimes called expressed intent. The same formal analysis methods used for the automatic assertions can be used to verify the designer-specified assertions. Typical assertions for an IP block might include:

• A state machine must make only certain transitions between states.
• A FIFO or stack must be neither written when full nor read when empty.
• A memory location must not be read before it is written with valid data.
• An arbiter must grant requests as per the intended arbitration scheme.

Assertions in simulation

All common assertion libraries and languages are designed to work in simulation. As shown in Figure 2, during stand-alone IP verification, the internal and interface assertions can run in parallel with the traditional simulation tests to provide an extra level of checking for the design. Even when the testbench detects a design error at the IP outputs, assertion violations can help to determine the precise location of the design bug. This is especially true for large and complex IP blocks, in which tracing back from the outputs to a bug is hard.

Figure 2 — Assertions aid in standalone IP verification by checking that designer intent is not violated.

One great advantage of assertions is that they can run in any simulation, whether verifying the IP block or an entire SoC. When the provider delivers the IP to the SoC team, the CIV and designer-specified assertions should be provided along with the design itself. Then, the SoC verification team can run the assertions in full-chip simulations, as shown in Figure 3. Both the internal and IP interface assertions are extremely valuable in helping the SoC team ensure that they have integrated the IP block and are using it correctly.

Figure 3 — Assertions in IP aid in chip-level verification by isolating design errors at their source.

The assertions on the IP block inputs are especially useful, since they check that the stimulus provided by the rest of the chip is correct. An IP team designs the logic to operate correctly within the range of legal input sequences. Failure to follow these rules usually results in the IP block misbehaving. For example, most AMBA-based blocks are designed to expect only legal protocol from the AMBA on-chip bus; illegal sequences will likely cause the blocks to generate illegal protocol in return.

The assertions internal to the IP block are also useful during chip-level simulation. If the IP design somehow gets into an inconsistent internal state, this might indicate that it was not integrated properly into the SoC or that there is a bug in the IP block itself. It is very embarrassing for a provider when an SoC team discovers an IP bug. However, this is greatly preferable to a bug ending up in silicon, endangering both the SoC project and the survival of the IP provider.

There is a way for an IP provider to eliminate the possibility of a bug making it to SoC simulation; the comprehensive use of formal analysis during stand-alone IP verification. Formal algorithms can exhaustively explore all possible design behavior over all time, ensuring that no SoC team can ever use an IP block in a way that has not already been fully verified. The result is a very robust IP design that can be safely reused by anyone.

Formal verification of IP

The use of formal analysis for IP verification involves two phases. The first phase — automatic assertions for CIV and other types of design properties — has already been discussed in detail. All IP designers should make automatic formal analysis a part of their verification process; it is easy to use and as natural as running lint tools, measuring code coverage, and using other traditional techniques. SoC teams should insist that any potential IP providers run automatic formal analysis.

The second phase is the formal verification of the designer-specified assertions as well as the assertions generated from CIV. As shown in Figure 4, this entails one additional step. The internal IP assertions and those on the IP block outputs are treated as targets for formal analysis, while the input assertions are treated as constraints. This ensures that formal analysis considers only legal input sequences as it tries to find either a proof or a counter-example for each target assertion.

Figure 4 — Formal verification of IP ensures that no possible legal input sequence can violate the designer assertions.

The specification of constraints might appear to be a burden for using formal verification, but in fact it is a natural outgrowth of the overall verification process. An accurate set of assertions to capture an IP block's input protocol provides great benefit for both stand-alone and chip-level simulations. Treating these assertions as formal constraints is easy, and in practice the set of input assertions from simulation is very close to that needed for accurate formal verification.

As formal verification has emerged as a more mainstream technique, a great deal of work has been done to improve the power and capacity of formal algorithms. Automatic formal analysis can be performed on designs of virtually any size, and many types of IP blocks can be exhaustively analyzed for the designer-specified assertions as well. For very large IP blocks, there may be divide-and-conquer methods available to formally verify sub-blocks and work up to the complete IP design.

Summary

Successful IP providers take verification seriously and use a wide range of techniques to produce the most robust possible design. Traditional methods include sophisticated stand-alone simulation environments, extensive suites of hand-written and constrained-random tests, coverage metrics, and lint analysis. These methods are necessary, but unfortunately not sufficient, to verify complex IP blocks well enough to find all bugs before integration into an SoC.

Only the comprehensive power of formal verification can create a truly robust IP block. Automatic formal analysis eliminates many common design errors, including improper handling of signals crossing between multiple, asynchronous clock domains. The addition of designer-specified assertions allows formal analysis to verify that the IP design will work as intended in any future SoC integration, a very powerful guarantee not possible with simulation alone.

IP providers should use formal verification to ensure that their designs will work properly and not result in chip re-spins. SoC teams should carefully evaluate the verification processes for any potential IP providers, insisting that formal analysis play a key role. The result will be a more successful commercial IP industry, higher confidence in reused designs of all types, and a dramatic reduction in the number of chip turns required to fix design bugs.

Jay Littlefield (jay@realintent.com) is Director of Applications Engineering at Real Intent, Inc. His background includes simulation and formal verification. Real Intent provides the Verix Assertion Verification System, which offers a hierarchical formal analysis capability including clock intent verification.