Open side-bar Menu
 Decoding Formal
Vigyan Singhal
Vigyan Singhal
Vigyan Singhal is President and CEO of Oski Technology, and is responsible for overall leadership of the company. He has worked in the semiconductor and EDA industries for 20 years, having led two venture-funded start-ups – Jasper Design Automation, a formal verification EDA company, and Elastix, … More »

Why Formal Can’t Scale without Methodology

September 12th, 2013 by Vigyan Singhal

Formal verification, and in particular model checking, has been around for a few decades now. I found my first post-silicon bug using formal 20 years ago at Motorola Austin in the cache controller block of a PowerPC chip. The power of formal technology drove my Ph.D research and subsequent career in formal verification.

Early on in my career, I focused on developing formal verification tools at Cadence. Later, I founded Jasper and did more of the same. Over the years however, despite the continuous improvement of formal technology, I find that formal adoption has been less than stellar. In particular, I feel people are not harnessing the full power that formal tools can provide. What is needed besides good tools is a scalable methodology.

Methodology is a body of practices, procedures, and rules used in a discipline. In simulation, both open source methodologies e.g. OVM (open verification methodology), UVM (universal verification methodology) and proprietary verification methodologies, internally developed by design teams of a company, exist. These have been of great help to the design and verification communities, which help scale simulation to keep up with the ever increasing complexity of the designs.

Unfortunately, there was no formal sign-off methodology that existed when I left Jasper in 2005. As an example, I know of semiconductor companies that have invested (and wasted) time and money evaluating and buying a formal tool, but the tool was abandoned eventually due of lack of methodology to scale formal verification to sign-off levels. This limitation prevents SoC teams, adopting formal for the first time, from verifying large design blocks of SoC. They need a formal methodology that can verify interesting blocks and integrate with existing simulation methodology, help verification leaders and managers to track progress of formal verification and sign-off.

This realization seeded the founding of Oski Technology to offer a formal sign-off methodology that helps SoC design teams to follow best practices in both design & verification to prevent nasty surprises after tape-out. We help our customers leverage the full power of formal to deliver high quality ICs in the ever-decreasing time-to-market window.

Oski formal sign-off methodology scales end-to-end formal verification to larger design blocks, some may have over 1 million flops. The methodology enables seamless integration of formal verification with customers’ pre-existing simulation methodology(s) and helps verification teams get up and running with formal verification within days of deployment. Oski formal methodology consists of 6 stages, namely Plan, Pre-verify, Verify, Analyze, Debug and Measure (Figure 1).

Plan: This stage focuses on finding the right verification approach, whether simulation or formal or even both, to verify the different design blocks and then partitioning the verification tasks accordingly. This involves understanding the design functionality and micro-architecture, identifying possible complexity issues for formal. A list of possible checkers and shortlisted Oski Abstraction Models™ for the blocks suitable for formal verification is also developed in this stage.

Pre-verify: A review of the DUT’s (design under test) RTL and implementation of covers for a detailed understanding of the design functionality and complexity are part of this stage. We also experiment to test effectiveness of different Abstraction Models and select the most effective Abstraction Models for the specific DUT and planned checkers. The goal is to find the best strategy that scales with the size of the DUT.

Verify: First, constraints and checkers are implemented in this stage. Next, the formal tool is run to verify the DUT and run-time results are measured.

Debug: Waveforms corresponding to failure reported in Verify stage are analyzed and corresponding fix(es) in the design. Sometimes adjustments are made to constraint(s), checker(s) or/and Abstraction Models.

Analyze: If a formal proof run-time exceeds acceptable time limit, an analysis of cones-of-influence (COI) and run-time is done by looking at design structures. This could result in decomposition of checkers, or development of new Abstraction Models. This stage is not necessary if the Abstraction Models created in the Pre-verify stage perform effectively.

Measure: Coverage results of the formal verification testbench are generated and analyzed in this stage. The result validates whether verification goals are met. All this results in a sign-off worthy methodology to use formal to complete verification of certain blocks. Moreover, the coverage results of formal verification are integrated with simulation coverage results and thus provide a single and complete view to observe and measure verification progress of the SoC.

With a systematic and customized approach to each verification project, Oski has helped many leading semiconductor companies adopt formal tools and make formal verification a part of their sign-off criteria. It feels good to see how the powerful formal technology, when coupled with a sound methodology, can broaden formal adoption and help realize the full value of formal to our customers.

Related posts:

Tags: ,

Category: Blog

2 Responses to “Why Formal Can’t Scale without Methodology”

  1. Joe Hupcey III says:

    Hi Vigyan,

    Great article! Two comments:

    1 – Indeed methodology is important, but even the most well-conceived and executed methodology will be unsuccessful if the underlying formal tools and engines don’t have the scalability, wall clock performance, and automation to simplify the users’ work-flow. Investment in each of these elements has been and continues to be Jasper’s R&D roadmap in a nutshell. As such, in a growing number of cases thanks to breakthroughs in performance and/or our core algorithms formal runs that used to require expert level methodologies to work are now running and producing results without extraordinary user intervention. Rephrasing, thanks to new automation in many cases formal CAN scale without special methodologies.

    2 – Today Jasper provides apps that generate metrics in service of the formal signoff methodology you [correctly] advocate. For example, in reference to your “Measure” item, Jasper’s Coverage App is unique in offering formal-centric coverage metrics and reporting. And via our UCIS support this app can also supply data to simulation-centric coverage flows and/or unreachability analysis, thus supporting combined formal+simulation verification signoff.


  2. Jin Zhang says:

    Thanks Joe for your comments. We agree that methodology has no place, if formal tools and engines were not good enough. But they are. Your company, Jasper, has also made significant advances in engine capacity. Today, it is possible to replace simulation by formal completely at the designer-sized block-level (and higher), and leave simulation for higher system-level issues. But, that is feasible only with effective methodology to: plan, use abstractions, decompose proofs, deploy cross-proofs, measure with formal coverage. For formal to become part of sign-off everywhere, not just at selected companies, such methodology needs to available to every verification engineer through education and practical training.

    Oski is also a big fan of the formal coverage feature you mentioned. That is key to deploy bounded proof in a sign-off methodology. We described a need for this in CAV 2011, and it is great that this is available to users today.


Leave a Reply

Your email address will not be published. Required fields are marked *


You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>

S2C: FPGA Base prototyping- Download white paper

Internet Business Systems © 2016 Internet Business Systems, Inc.
595 Millich Dr., Suite 216, Campbell, CA 95008
+1 (408)-337-6870 — Contact Us, or visit our other sites:
TechJobsCafe - Technical Jobs and Resumes EDACafe - Electronic Design Automation GISCafe - Geographical Information Services  MCADCafe - Mechanical Design and Engineering ShareCG - Share Computer Graphic (CG) Animation, 3D Art and 3D Models
  Privacy Policy