Top 10 Tips for Success with Formal Analysis – Part 2

Thomas L. Anderson, is a technical marketing consultant who recently served as Product Management Group Director for Cadence.
Joseph Hupcey III, Product Management Director, Advanced Verification Systems, Cadence Design Systems, Inc.

This is the second in a series of three articles presenting the “top 10” tips for the successful use of formal analysis on IP and SoC projects. As discussed in the first installment, formal analysis has many strengths as a verification technique, including exhaustive mathematical proofs, discovery of bugs that are hard to find in simulation, and an ability to analyze coverage properties (covers) as well as assertions. The first three tips presented were:

• Tip 1: Involve designers in property specification and, whenever possible, in formal analysis
• Tip 2: Apply formal analysis early in the project so that engineers specifying properties see an immediate payoff
• Tip 3: Leverage all forms of automatic assertions, from basic design checkers through assertion synthesis

Although most properties are written using either SystemVerilog Assertions (SVA) or Property Specification Language (PSL), assertion libraries play a significant role in making it easier to add “automatic” assertions and covers to a design. The best-known is the Open Verification Library (OVL), for which Accellera provides both a written specification and example implementations [1]. OVL assertion checkers are designed to attach easily to common design structures and signals. The 50 OVL checkers include:

• ovl_arbiter – check that an arbiter follows the specified method (round robin, LRU, etc.)
• ovl_decrement/ovl_increment – check that a value decrements/increments by the specified amount
• ovl_even_parity/ovl_odd_parity – check that a multi-bit signal has specified parity
• ovl_fifo – check that a FIFO does not overflow, underflow, or corrupt data
• ovl_handshake – check that a request-acknowledge handshake works as specified
• ovl_memory_async/ovl_memory_sync – check the data integrity of a memory
• ovl_next_state – check that a state machine transitions only to specified states
• ovl_range – check that a value remains within a specified range
• ovl_stack – checks that a stack (LIFO) does not overflow, underflow, or corrupt data

All of these checkers contain both assertions and covers appropriate for the data structures or signals being checked. Many of the signal checkers are designed to capture individual interface protocol rules. It is possible to combine multiple OVL checkers (usually with “helper” RTL code) to check for the complete behavior of an interface protocol. If this protocol is a standard bus used by many customers, a commercial verification IP (VIP) solution may be available. Protocol checkers written using assertions are often called assertion-based VIP.

Tip 4: Leverage assertion-based IP (ABVIP) for standard protocols, especially for on-chip buses

As with other forms of commercial VIP, such as Universal Verification Components compliant with the Universal Verification Methodology (UVM), there is clear value for the user in choosing an independent checker validated with many designs. ABVIP components are available for a wide range of industry-standard buses and interfaces. Most run in both simulation and formal analysis; some may run in simulation acceleration and in-circuit emulation (ICE) hardware as well.

The most commonly used ABVIP components are those for on-chip buses, including Open Core Protocol (OCP) and several generations of the AMBA^® bus family for ARM^® processors, including APB, AHB^™, AXI^™, and ACE^™ protocols. This is partly because on-chip buses connect most of the major blocks in an SoC, so the same ABVIP component can be used in formal analysis of multiple blocks with minimal variation. In addition, on-chip bus protocols tend to be amenable to formal analysis, unlike some of the deep serial protocols used on SoC I/O pins.

For a real-world example, consider the case where Texas Instruments applied an OCP ABVIP to exhaustively verify all the OCP buses on-board a multi-million–gate SoC [2].  Given the resource and schedule constraints of the project, they employed OCP ABVIP to give a scalable, plug-and-play setup that offers complete protocol coverage for and confidence in the IP within a short timeframe. Their prior simulation-based flow was taking a distressing amount of time to set up, the controllability of the stimulus was difficult, and the time to debug issues was increasing.  Even worse, the simulation methods could not provide the degree of completeness—and therefore risk reduction—that they wanted. By using ABVIP in combination with formal verification tools—without having to write testbenches—they were able to exhaustively prove their IP was compliant with the OCP protocol specification, in only a few weeks from start to finish.

Tip 5: Leverage formal “apps” such as connectivity checking for highly multi-plexed SoC pins

The notion of “apps”—applications for specific purposes—has become well-known among users of smartphones and similar consumer products. The term apps also applies to formal analysis, since well-designed applications can enable non-experts to be successful without having to learn much about properties or formal algorithms. The use of ABVIP to verify a standard interface is one example, since most or all of the assertions, assumptions, and covers are provided within the ABVIP component and referenced to the appropriate page in the standard specification.

SoC connectivity checking is another excellent example of a formal app. Most SoCs use multiple complex protocols to communicate with other devices, and often the protocols are programmable depending upon the target system. In such cases, designers multi-plex two or more protocol controllers to share the same set of I/O pins. This leads to a complex connectivity verification problem at the top level of the SoC since it’s critical that the right signals are connected to the right pins during different operating modes.

Formal analysis does a much better job of exercising all of the combinations than simulation does. SoC connectivity checking is perhaps the most automated formal app since it can be run by a design or verification engineer with no knowledge of assertions or formal analysis. Cadence has pioneered an approach in which the engineer captures the intended behavior in a simple spreadsheet. An automated process then converts the spreadsheet into a set of assertions and runs them in formal analysis. The goal is usually proof of all assertions, while finding and fixing bugs along the way.

The first installment in this series mentioned the capacity limitations of formal analysis and it may seem as if this full-SoC app is contradictory. In practice, the vast majority of the chip can be “black-boxed” for formal, leaving only the top-level connections and I/O pads. This small amount of logic is well within the capabilities of formal analysis, and so a full proof is usually possible. The following diagram shows top-level cases that are typical of an SoC connectivity verification effort.

A real-world case study of this tip can be found in a DAC 2011 User Track paper entitled “Push Button Verification of Complex Pad Ring Logic Direct from an Executable Specification” [3].  As the title suggests, author Olivia Wu describes how she and her colleagues were able to automate the black-boxing and assertion-generation process to exhaustively verify their block- and chip-level connectivity. Specifically, they were able to completely verify the multi-mode connectivity of more than 1,000 I/O pads, with more than 50 pins per pad, and multiple operational modes (reset, test, and normal operation)―a total of more than 20,000 separate use cases at the block level alone. The results were dramatic versus the prior simulation methodology: the team was able to achieve 100% coverage of all use cases, and run analysis significantly faster—hours rather than weeks.

Tip 6: Recognize the value of formal analysis for both proving assertions and finding design and specification bugs

This tip may seem obvious given the topics discussed so far in this article and its predecessor, but there are some subtleties worth mentioning. Until recently, there was somewhat of a split in the way that formal analysis was applied. Academic formal users and formal experts verifying IP and SoC designs both focused on complete proofs for all assertions. The classic example is verification of cache-coherency algorithms, a challenging project but one deemed so critical that a large investment in advanced formal techniques is a given.

On the other hand, mainstream formal-analysis users focused mostly on finding design bugs. They did not put a lot of effort into finding proofs, since proving is a formal result with no correlation in the more familiar world of simulation. The “separate worlds” of simulation and formal analysis meant that it was hard to develop planning and tracking methods for both activities. More recently, project managers have demanded accountability for the effort spent in formal analysis, which means that the two worlds must be brought together.

The best way to accomplish this is to translate formal results into simulation terms. Bugs found in formal analysis should be tracked just as those found in simulation, giving due credit to the engineers running formal tools. Further, the combined formal/simulation results should include covers reached using both techniques, again giving credit to the contributions of formal analysis. These results should be expanded to include the concept of proven assertions since knowing that an assertion is “safe” may influence how it is handled in simulation.

The Cadence^® metric-driven verification (MDV) flow provides all of these combined results. MDV enables the development of a single verification plan spanning simulation and formal analysis (as well as hardware acceleration and in-circuit emulation). Common metrics for coverage, assertions, and other forms of checks are collected from simulation and formal analysis, and then reported back against the plan. These metrics include formal proofs or assertions as well as formal proofs of unreachability for covers.

In the next installment of this series, we will elaborate on a specific “coverage unreachability” flow that uses simulation and formal analysis together for detailed coverage analysis and signoff. As always, any comments, suggestions, or personal anecdotes on the use of properties and formal analysis are most welcome.

References

[1]    “Accellera Standard OVL V2 Library Reference Manual” http://www.accellera.org/activities/ovl/

[2]   “Quality and Confidence Improvement on OCP IPs Using Assertion-Based Verification IP” by Aneet Agarwal and Mithun Ghosh, CDNLive! India 2007, http://www.cadence.com/rl/Resources/conference_papers/1.2_presentationIndia.pdf

[3] “Push Button Verification of Complex Pad Ring Logic Direct from an Executable Specification” by Olivia Wu, Proceedings of the 48^th Design Automation Conference, 2011