It is a challenging problem to formally verify mathematical datapath designs. Such designs, by nature, do not lend themselves well to be verified via traditional model checking algorithms. However, formal transactional equivalence checking with a “golden” reference model can be used successfully to verify datapath designs. In this paper, we describe how we used HECTOR – a C-vs-RTL transactional equivalence checking tool from Synopsys – to formally establish the correctness of a multiplier design for an X86 processor core. We also used the Synopsys VC Formal tool to prove correctness of a complex divider design. The transactional equivalence checking was repeated several times as the designs went through changes to satisfy power and performance requirements. Due to the large complexity in the designs, we pushed the limits and had deployed various recipes and techniques, including transitivity and assume-guarantee.
Check the box next to the paper(s) you would like and then click "Request Papers" button.
Using Formal Tools to Verify Datapath Designs During Various Phases of Processor Development
Authors: Sankar Gurumurthy, Farhan Rahman, Ankit Saxena and Ashutosh Prasad
Publication: SNUG 2016
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
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.
Compositional Reasoning Gotchas in Practice
Authors: Chirag Agarwal, Paul Hylander, Yogesh Mahajan, Jonathan Michelson and Vigyan Singhal
Publication: 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 Singhal
Publication: 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 Singhal
Publication: 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 Singhal
Publication: 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 Jain
Publication: 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.