With the advances in formal technology and the introduction of Formal Sign-off Methodology in recent years, it has become possible to create a formal testbench that can find all bugs in a design. However, this is a very new concept that most design and verification teams do not know well enough to adopt and leverage for sign-off. The paper explains in detail the process to achieve Formal Sign-off, focusing on End-to-End checkers, constraints, complexity and formal coverage. In addition, we present a live case study as proof that Formal Sign-off is possible.
Check the box next to the paper(s) you would like and then click "Request Papers" button.
The Process and Proof for Formal Sign-Off – A Live Case Study
Authors: Ipshita Tripathi, Ankit Saxena, Anant Verma and Prashant Aggarwal Publication: DVCon 2016
Compositional Reasoning Gotchas in Practice
Authors: Chirag Agarwal, Paul Hylander, Yogesh Mahajan, Jonathan Michelson and Vigyan SinghalPublication: FMCAD 2015
Model checking has become a formal sign-off requirement in the verification plans of many hardware designs. For design sizes encountered in practice, compositional assumeguarantee reasoning is often necessary to achieve satisfactory results. However, many pitfalls exist that can create unsound or unexpected results for users of commercial model checking tools. Users need to watch out for circularity in properties, for dead-ends getting trimmed by tools, as well as understand the differences in proof composition for liveness and safety properties. We present many real design examples to illustrate these points, as well as describe our experiences with compositional reasoning in practice.
Creative Formal Techniques to Verify PCache
Authors: Normando Montecillo, Keyu Chang, Ipshita Tripathi, HarGovind Singh, Vigyan SinghalPublication: DAC 2015
Coloring is a very powerful formal technique to verify data transport designs. It adds minimum number of flops to the formal testbench, making formal complexity managable by formal tools. PCache is a data transport design and an ideal fit for formal verification. However, conventional coloring technique cannot be readily used as PCache allows drop data based on certain rules. To formally verify PCache, we came up with creative ideas to enhance the conventional coloring technique, without adding complexity to the formal testbench. We found 12 bugs using the technique and achieved formal sign-off on Pcache.
Modeling Xs in Behavioral Models of Hard IPs
Authors: Prashant Aggarwal, George Curkowicz, Mark Glasser,Vigyan SinghalPublication: DAC 2014
Behavior models of hard IPs are often used to replace traditional SPICE models to reduce simulation time. However X-modeling is prone to simulation race conditions and is hard to verify which could lead to missing bugs in SoC integration. We present an assertion-based approach of verifying X-modeling of a behavioral model which handles simulation race conditions and avoids false positives and negatives. Our approach is the first solution that can be used by developers of behavioral models to systematically detect missing X-assignment bugs.
Sign-off with Bounded Formal Verification Proofs (2nd BEST PAPER AWARD)
Authors: NamDo Kim, Junhyuk Park, HarGovind Singh, Vigyan SinghalPublication: DVCon 2014
Inconclusive formal verification results or bounded proofs have been hindering the adoption of formal verification. This paper describes a formal sign-off methodology in presence of bounded proofs. With an understanding of the DUT and a systematic analytical approach, we can qualify bounded proofs and use Abstraction Models to achieve formal sign-off.
Deploying Model Checking for Bypass Verification (BEST PAPER AWARD)
Authors: Prashant Aggarwal, Michelle Liu, Wanli Wu, Vigyan Singhal Publication: DAC 2012
Bypass logic in used to achieve performance in deeply pipelined designs, but comes at a significant increase in verification complexity. This paper describes how we applied model checking to establish the correctness of the bypass case, and found corner case bugs that are almost impossible to find with simulation.
Liveness vs Safety – A Practical Viewpoint
Authors: B. A. Krishna1, Jonathan Michelson, Vigyan Singhal, Alok JainPublication: HVC 2011
Within the formal verification community, choosing between liveness and safety approaches has long been a subject of debate. This paper applies both approaches to a common design in the networking industry, a Deficit Weighted Round Robin (DWRR) arbiter. It then presents the tradeoffs we encountered while applying both approaches and also describes how we overcame state space explosion. We also describe two real post-silicon design bugs that we found, which were missed by all simulation methods.
Using Coverage to Deploy Formal in a Simulation World
Authors: Vigyan Singhal, Prashant Aggarwal Publication: CAV 2011
Formal verification can complement or replace simulation effort for selected hardware designs. In this paper we discuss how formal verification can be deployed using simulation-based coverage in a simulation-based verification schedule.
End-to-End Formal using Abstractions to Maximize Coverage
Authors: Prashant Aggarwal, Darrow Chu, Vijay Kadamby, Vigyan Singhal Publication: FMCAD 2011
The use of abstraction models is key to overcoming complexity barriers in applying formal verification.. In this paper, we show how simulation-like coverage metrics can be used to determine the completeness of a formal verification setup, for a real-world design with a large state space, that needed abstractions for end-to-end proofs.
How Formal Methodology Shrank the Verification Schedule of a Complex Statistics Block by 6x
Authors: Sandesh Borgaonkar, Chirag Agarwal, Rajesh Kothari, Darrow Chu Publication: DAC 2011
To insure high quality of service, today’s routers need to record and react to numerous statistics in real time, across all the routing paths. Architectural features needed to support the throughput requirements risked creating numerous corner cases. This presentation summarizes how an 18-month simulation-based effort was shrunk down into only 3 months using formal verification.
CoverMore: A Methodology to Deliver Re-Usable and Verifiable Design IP
Authors: Sriram Swaminathan, Prakash Bare, Guruprasad Karaje, Vigyan Singhal 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.
Formal Verification of a Public-Domain DDR2 Controller Design
Authors: Abhishek Datta, Vigyan Singhal 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.
Formal Verification for PCI Express RTL Designs
Authors: Vigyan Singhal 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.
Who Verifies Your Third-Party Design IP?
Authors: Vigyan Singhal, Harry Foster 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.)
Guidelines for Creating a Formal Verification Testplan (BEST PAPER AWARD)
Authors: Harry Foster, Lawrence Loh, Bahman Rabii, Vigyan Singhal 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.