Abstract: Model checking tools are gaining traction as a practical formal verification solution for industrial designs. However, the use of abstraction models is key to overcoming complexity barriers in applying these tools. Coverage has been a useful metric to determine when simulation-based verification is complete. In this paper, we show how similar coverage metrics can be used to determine the completeness of a formal verification setup. We also show how coverage can be used to determine effectiveness of different abstraction models are. This methodology can be used to set formal verification goals, and to measure the progress of the work, thereby placing formal verification in a chip design schedule. We use a real-world design with a large state space, and present quantitative coverage metrics to illustrate the methodology, and its benefits for faster run-time, faster discovery of bugs, and higher coverage.
End-to-End Formal using Abstractions to Maximize Coverage (516KB)
Publication: FMCAD 2011
How Formal Methodology Shrank the Verification Schedule of a Complex Statistics Block by 6x (644KB)
Publication: DAC 2011
Slides from the Oski-Cisco-Cadence poster presentation for DAC 2011 “How Formal Methodology Shrank the Verification Schedule of a Complex Statistics Block by 6X”.
Using Coverage to Deploy Formal in a Simulation World (206KB)
Publication: CAV 2011
Abstract. Formal verification technology has today advanced to the stage that it can complement or replace simulation effort for selected hardware designs. Yet the completion of a formal verification effort is rarely a requirement for hardware tapeout. Simulation remains the primary verification methodology, and means of deciding when verification is complete. In this paper we discuss how formal verification can be deployed using simulation-based coverage in a simulation-based verification schedule.
Guidelines for Creating a Formal Verification Testplan (153KB)
Publication: DVCon 2006
This paper proposes a systematic set of guidelines for creating an effective formal verification testplan, which consists of an English list of comprehensive requirements that capture the desired functionality of the blocks that are to be verified. This paper won the Best Paper Award at DVCon 2006.
Formal Verification for PCI Express RTL Designs (685KB)
Publication: PCI-SIG Developers Conference, 2006
PCI Express is a classical example of a design that can result in severe complexity challenges in formally verifying end-to-end properties. Yet, data-transport designs like this can be successfully verified using creative abstraction methods. This presentation discusses general strategies for verifying a PCI Express design.
Formal Verification of a Public-Domain DDR2 Controller Design (336KB)
Publication: VLSI Design 2008
Using the Sun OpenSPARC DDR2 Memory Controller design, that has been in the open-source public domain, this paper removes much of the mystery in a successful application of end-to-end formal verification on a memory controller design.
CoverMore: A Methodology to Deliver Re-Usable and Verifiable Design IP (228KB)
Publication: DVCon 2008
Exhaustive verification is especially hard for highly configurable IP designs. Using a constrained-random coverage-driven simulation methodology, this paper shows how more than 10X productivity and higher coverage was achieved on a production design.
Who Verifies Your Third-Party Design IP? (230KB)
Publication: IEEE CEDA Currents, July 2006
This July 2006 issue contains an article that argues that third-party design IP must be accompanied by replayable verification IP, that proves the correctness of the design through end-to-end checks. (Go to the end of the issue to find the article.)
Request Papers
Please select the papers you wish to receive by checking the boxes beside each, below. Brief summaries are to the left.