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.
EETimes - 1/30/2012 9:59 AM EST

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.

Click here to read more ...