Why Formal Can’t Scale without Methodology

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.

Tags: formal verification, Vigyan Singhal

Category: Blog

This entry was posted on Thursday, September 12th, 2013 at 3:01 pm. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.