Formal Verification IPs: the corner stone for a broader adoption of Formal Verification

By Samuel Dellacherie, AerieLogic

Abstract

Formal verification associated with assertions is a well known approach to functional verification of SoC digital circuits. This technique bears several advantages over dynamic-based solutions, but also many drawbacks that still confine its usage to a side tool reserved for experts. Efforts toward automation and smooth integration with simulation-based techniques are key to have formal verification deliver indisputable benefits.

In this article we show how several areas of the functional verification task can benefit from automated formal verification: design coverage enhancement, protocol compliance checking and functional performance analysis. With our proposed methodology, these tasks can be achieved seamlessly by designers or verification engineers, thus bringing more automation and robustness to the verification of SoC designs.

1 Introduction

Formal verification (also known as model checking or property checking or even bug hunting) is the art of using complex mathematical algorithms to exhaustively verify the functionalities of digital circuits. Its major advantage over simulation-based techniques is its capacity to either compute a proof that a property (or assertion) holds, or compute a sequence that violates the property. Formal verification often uncovers bugs and corner cases that are complex or impossible to discover with simulation alone. Industrial experiences on using formal verification are numerous, see for instance [5] [2].

Assertions are the natural way to apply formal verification, but they also strongly enhance traditional simulationbased techniques. They offer a shared implementation model for the specification, the design and the verification plan. In addition, assertions give better observability on the design and detect bugs earlier and closer to their origin. Many successful stories on using assertions with simulation have been reported, for instance [1] [4].

Unfortunately formal verification and assertions are not so easy to bring into operation. The fact is somehow underestimated in the literature, even though some analysis attempts exist, see for instance [8] [7]. Still, in practice, the approach is under-used, and this for several reasons.

First of all, assertions can be difficult to capture from the specification, and very tricky to elaborate and to debug. This becomes really problematic if assertions are wished to take a central part in verification, in which case a high amount - if not all - assertions must be extracted from the specification. A related problem is on how to measure that all the assertions are extracted from the specification so that a high percentage of functional coverage is achieved. When using formal verification, there is in addition the necessity to create assertions that model the environment This task can be easy when working on a single specific property to prove, but gets complex when using formal verification on a wider amount of properties. The environment behavior needs to be extracted from the written specification, and erroneous assertions coding many times leads to deadlocking the environment or creating false positives that need time-consuming analysis.

In order to alleviate the use of formal verification with assertions, the fundamental idea we propose here is to leverage the robustness of the SoC protocol specifications to build ready-to-use Formal Verification IPs. A Formal- VIP is much more than a simple library of assertions, as it includes the automatic generation of the environment for formal verification and many ease-of-use enhancements. We detail further this notion of Formal-VIP in section 2.

Once a Formal-VIP is available, formal verification can be applied for automatic protocol compliance checking, automatic functional performance evaluation and automatic coverage enhancement. We will illustrate each subject respectively in sections 3, 4, and 5 with the OCP or AXI protocols.

2 Formal Verification IPs

With recent protocols such as OCP or AXI that facilitate reuse and integration, blocks are not aware of the system configuration, and the bus protocol interconnect is the functional backbone of the SoC design. Any controlrelated problem, being a functional bug within a block (loss of data, live-lock, etc) or a functional incompatibility between blocks (performance, latency, etc) shall be detected at the bus protocol level. The bus protocol layer is where all functional activities of the SoC design can be monitored, and should thus be the corner stone for any functional verification task.

A Formal Verification IP is for formal verification and assertions what a Verification IP is for simulation. It includes complete documentation, automated environment and assertions creation, automated scripts and report generation, all targeted at analysing the designs through the bus protocol interface.

The Formal-VIP documentation includes a precise description of all the protocol assertions that have been extracted from the official protocol specification. Creation of such a document can be quite a complex task as the goal is to certify that 100% of the protocol specification is covered with assertions.

Assertions created with a Formal-VIP are of two types:

1. coverage scenarios that produce test-sequences illustrating particular functionalities of the protocol

2. properties (or compliance checks) that must always hold on the design

The fundamental assertions are the properties that will certify that the design is fully compliant with the protocol (see next section). Nevertheless, coverage scenarios are useful to illustrate at a glance how the selected protocol features behave and interact, for instance to

• compute a succession of multi-threaded read wrapping bursts of size 4, 8, and 16

• compute a succession of out-of-order responses to incrementing bursts of size 4, 8 and 16

The OCP protocol is in constant evolution and includes now more than 100 different parameters to select active protocol features. The AXI protocol does not propose such a set of parameters, but it is not always clear how features interact if part of the AXI protocol is or is not selected. The coverage scenarios will compute automatically timing diagrams that show how the design reacts according to the functionalities of the protocol, without spending time at test-bench creation.

The Formal-VIP also creates automatically a formal environment for the design in accordance with the selected protocol configuration. This is key to eliminate wrong properties violations (false negatives) or wrong testsequences generation (false positives) that occur when the environment is not well defined. In our experience, robust environment creation can take 80% of the overall time spent on formal verification.

To ensure ease of use and flexibility with the Formal-VIP, assertions and formal environment are both automatically selected and sized according to a set of parameters (the Formal-VIP configuration file) that can be filled-in in text or graphical mode. With OCP designs, usually an OCP RTL configuration file describing the OCP configuration and signals names already exists and can be directly processed. A regression script is then built up, or the created assertions can be checked manually one at a time. A detailed report enables to quickly evaluate which assertions passed or failed.

Providing a good graphical interface is key to enabling non-experts to easily use a Formal-VIP. This GUI includes inline help, automated links to the protocol specification and assertions definitions, automatic signals mapping, syntax and semantic checks to capture configurations errors, automatic generation of the rtl.conf file for OCP, etc. It also provides a common and systematic way to build an interface configuration for all protocols.

More explanations on how Formal-VIPs work can be found in the datasheets available on www.aerielogic.com.

3 Protocol Compliance

Protocol compliance is the first natural task that can be performed automatically with formal verification. Both the OCP and AXI protocols include more than a hundred compliance properties, ranging from very simple ones like stability of signals during a given phase to complex ones such as

• Responses to requests that target overlapping addresses must not be re-ordered

• If a ReadEx is issued on a location, no other request to the same location can be issued from another thread until the lock is unset

With OCP and to a certain extent with AXI, tens of features are available that can be combined or not. Each protocol compliance check usually has several different instanciations depending on the selected protocol configuration. The Formal-VIP will extract and instanciate the set of compliance assertions according to the protocol features selected, and similarly build a formal environment around the design compatible with the same protocol configuration.

Instead of spending time analysing which protocol properties need to be checked and building complex stimuli to uncover complex corner-cases, the user simply launches the Formal-VIP automatic compliance regression script.

Furthermore, as formal verification performs exhaustive search and the Formal-VIP covers 100% of the protocol specification, once a design goes through the Formal-VIP regression with success, it is certified 100% protocol compliant. If a violation is found during the regression, formal verification creates a short test-sequence that can be analysed or replayed in simulation. As a sound formal environment is set, the violation is usually a bug of the design, or it can be a misunderstanding of a protocol features, or an inconsistency between the design and its specification.

A designer can thus hand-over, with almost no effort, to the verification team or to the integration team a nonambiguous and 100% proved protocol compliant design.

4 Functional Performance

The Formal-VIP functional performance assertions track down the latencies, the counters or fifos overflows effects, or the back-pressure and pipelining results on the design. Examples of performance assertions can be

• The slave will always answer a request in less than N cycles

• The master will always fulfill it’s burst transaction in less than N cycles

For instance a FSM dead-lock or live-lock, a loss of data, will all have an impact at the protocol level as a loss of performance, and thus be detected with such properties.

The Formal-VIP will automatically create the functional performance assertions from a set of parameters that describe the worst latencies of the formal environment and the supposed worst latencies of the design. Whenever a violation is found, it can be a deep bug or corner-case uncovered in the design, but also a wrong parameter value coming from a lack of understanding of the design’s performances.

The worst performance analysis is very difficult with simulation techniques alone, and functional performance is usually analysed only late in the design cycle at integration level. With the Formal-VIP automatic generation of functional performance assertions, this analysis can be performed earlier in the design cycle directly by the block designer.

Using a Formal-VIP the designer can hand-over to the integration team a block having its functional performance fully documented and verified. At integration level, the performance results of different blocks can then be crosschecked to make sure all blocks can be interconnected, and to detect earlier which blocks could create a functional bottleneck. The formal environment can also be modified at will to evaluate how the design reacts to different environments configurations prior to integration.

Other categories of assertions can be automatically created with the Formal-VIP. For instance sampling properties verifying that the design’s inputs are sampled when and only when they are valid, or cross-interface properties verifying the consistency of a transaction that goes through a design (for example a bridge or a memory controller).

5 Coverage Enhancement

Code coverage stimuli is the popular way to measure how well a design has been verified with dynamic solutions. Many coverage metrics are involved, ranging from simply counting lines or branches to analysing how expressions are exercised. Difficulties arise when getting close to the coverage sign-off point. With simulation alone it can take a lot of time and effort to find the right test stimuli that will exercise the last few uncovered items, or worse to find out that some particular items are in fact not reachable at all.

Formal verification techniques should be used to automatically compute test stimuli that will address the uncovered items, or prove that some of these items are not reachable. A module-level formal analysis, often referred to as dead-code detection, can be performed. It is fast but inaccurate as most coverage items will be triggered with false positives. This type of formal analysis is more related to advanced linting useful in the early stages of the block creation.

A design-level formal analysis, usually referred to as coverability analysis, is well suited to complement simulation-based coverage techniques. It has a good level of accuracy as the whole design is taken into account, and a fair analysis speed as only the difficult coverage items are processed. Dynamic and formal results are merged in a single report that will provide enhanced coverage information. Additional details on coverability analysis can be found for example in [3] [6].

Aside from helping reaching a good coverage signoff percentage, coverability analysis also helps in various more specific situations. It detects expressions or branches useless with respect to a design’s configuration. This can be useful for instance to fine tune the low-power mode of a chip or eliminate irrelevant portions of a configurable IP.With modern bus-protocols such as OCP and AXI, the RTL of the protocol interconnect and protocol interfaces are often automatically created. Coverability will detect any spurious expression or branch that can safely be removed.

Going further, when used in conjunction with a Formal- VIP, coverability computes test-sequences targeting coverage items that are now sound with respect to the protocol layer. This enables to automatically enhance the dynamic test-bench with short sequences of stimuli that will cover the remaining reachable expressions or branches missed with simulation.

6 Conclusion

We described how formal verification, when using a Formal Verification IP that automatically creates a formal environment, can efficiently solve design verification tasks. We showed how protocol compliance and functional performance analysis can be automatically performed, and also how dynamic coverage analysis can be automatically enhanced. For such areas of the verification flow, formal verification is now a must-have.

References

[1] B. Bentley. Validating the intel pentium 4 microprocessor. In DAC, 2001.

[2] T. Blackmore, S. Marchese, and F. Bruno. Formal verification of a key block of the tricore 2 microprocessor. In Euro DesignCon, 2004.

[3] G. Cunningham, P. Jackson, and J. Dines. Expression coverability analysis: Improving code coverage with model checking. In DVCON, 2004.

[4] H. Foster and C. Coelho. Assertions targeting a diverse set of verification tools. In HDLCon, 2001.

[5] I. Moussa, J. Blasquez, S. Lasserre, C. Chapuy, S. Dellacherie, and G. Nguyen. Using model checking techniques for debugging a data-cache management block. In DATE, 2002.

[6] G. Ratzaby, S. Ur, and Y. Wolfsthal. Coverability analysis using symbolic model checking. In CHARME, 2001.

[7] U. Rossi. Can we really do without the support of formal methods in the verification of large designs? In DAC, 2005.

[8] Y. Wolfsthal and R. Gott. Formal verification - is it real enough ? In DAC, 2005.