Next-Generation Formal Verification

As SoC and IP designs continue to increase in complexity while schedules accelerate, verification teams are looking for methodologies to improve design confidence more quickly. Formal verification techniques provide one route to improved design confidence, and the increase in papers and interest at industry conferences like DVCon and DAC reflect the growing usage of formal verification tools in the industry. Despite the increase in usage of formal verification, there are still few opportunities for verification engineers interested in formal techniques to exchange ideas, knowledge, and best practices.

The Synopsys VC Formal Special Interest Group (SIG) events are a step towards broadening knowledge of formal verification. In the inaugural year of the VC Formal SIG, Synopsys held events in India, Japan, and the United States. In all three events, VC Formal customers shared their experience and successes in using VC Formal to address verification problems, alongside Synopsys AEs who presented new or advanced applications of formal verification. The most recent event was held in November in Santa Clara, California, with a keynote discussion from Sean Safarpour and Pratik Mahajan from Synopsys discussing the history and future of formal verification. The Santa Clara event showcased experts from AMD, ST Microelectronics, Qualcomm and Juniper Networks, highlighting the use of formal verification to solve challenging verification problems.

Formal Sign-Off of a Control Unit (AMD)
Wayne Yun discussed the verification of a complex control block using formal methods. The block included an AHB arbiter, microprocessor, data collector, accumulator, and glue logic. First, each block was considered in isolation. Formal techniques such as formal model creation, case splitting, invariant identification, and symbolic variables were applied to each sub-block. Assume-guarantee reasoning validated assertions on interfaces between sub-blocks. He also discussed how AMD used the coverage collection, overconstraint analysis, and fault injection features of VC Formal to signoff the design. VC Formal formal core analysis and fault injection identified several areas that required additional assertions. At the end of the project, over 94% of assertions were proven, all blocks had full formal core coverage, and most blocks detected over 99.8% of injected faults.

Formal Verification of a GPU Shader Sequencer (AMD)Chirag Dhruv and Vaibhav Tendulkar showed the benefits of VC Formal FPV App’s bug hunting effort to find bugs in a GPU shader sequencer. A wide variety of parallel instructions, asynchronous events, and dynamic configuration changes make simulation coverage closure difficult in this block. Sub-block decomposition allowed quick bug exposure and rapid iteration time. Formal reachability analysis, COI coverage analysis, and formal core coverage analysis identified dead code and design areas requiring more assertions. Formal verification found over 30 RTL bugs, several which would have been difficult to discover through simulation, absolutely.

Accelerate Digital IP Formal Verification with Machine Learning Technology (ST Microelectronics)
Giovanni Auditore described a shift of verification resources within ST towards formal verification. They used Verdi Planner to combine the formal and simulation verification plans, allowing a single view of verification progress as formal use increased from project to project. A variety of VC Formal Apps were applied to the design, including FCA for unreachability analysis, FRV for register verification, and FPV for property and protocol verification. Giovanni also described how the Regression Mode Acceleration (RMA) feature of VC Formal sped up formal regression. RMA uses machine learning techniques to accelerate proof time on future runs of the same or incremental versions of RTL. After applying RMA learning to an initial release of RTL, proof time for subsequent RTL releases took 1/3 the time as running identical regressions without RMA. RMA also reduced runtime of fault injection qualification from 21 to 16.5 hours.

Verification Sign-Off with Formal (Qualcomm)
Anmol Sondhi shared how to layer various coverage metrics available in VC Formal to build confidence in assertion quality throughout the design cycle. Early in the project, cone-of-influence based property density will identify testing holes in the design. Unreachability analysis through the FCA App, and over constraint analysis identifies areas in the design where formal stimulus won’t reach, allowing targeted review of RTL and formal constraints. Formal core coverage represents the logic that formal engines use to prove a property. Uncovered areas represent potential test holes. Finally, fault injection identifies areas where modifications in RTL behavior trigger assertion failures. He also showed how RMA resulted in between 2X and 10X improvement in regression runtime. Using VC Formal, the example project achieved over 99.5% property density and 90% formal core coverage and identified only 12 areas of undetected faults that required further investigation.

Designing for Formal Verification (Juniper Networks)
Anamaya Sullerey explained how RTL designers can be involved with formal verification through design methodology and short, frequent formal regressions of RTL. He described how changing an event driven implementation with a complicated state machine and complex, interacting side effects to a functionally driven implementation with lots of small modules that perform simple tasks can simplify and accelerate formal verification. Efficient decomposition of the design allows for meaningful sub-block formal verification regressions of no more than five minutes. Other recommendations for formal friendly design include early parameterization of RTL code, isolating complex blocks into separate modules for easy abstraction, creating meaningful intermediate expressions, and coding assertions for design invariants such as one-hot bit vectors. With a high level of formal friendly design methods, designers or verification engineers could quickly build module level formal testbenches that catch a majority of bugs with five minutes of regression time.

The Synopsys formal verification team presented tutorials on datapath operations and how to discover design invariants. JT Longino talked about using Synopsys tools for formally proving datapath operations. Datapath correctness continues to be a challenge for the industry. High confidence in datapath operations is difficult or impossible to achieve using simulation, but datapath operations have historically exceeded the capacity of formal property verification tools. Synopsys HECTOR technology provides users the ability to prove equivalence between an implementation RTL design and a reference design. The two designs can have different latencies, and the reference design can be untimed C or C++ code. The new VC Formal DPV App integrated HECTOR technology into the VC Formal GUI, allowing formal verification engineers to work on datapath verification problems in a familiar environment.

Iain Singleton described how to use VC Formal to discover design invariants to help converge complex properties. Invariants describe properties that remain unchanged when a specific transformation is applied and can restrict the state space of subsequent proofs if used as assumptions. Although they are powerful tools or assisting convergence, invariants can be difficult to identify and write. The VC Formal Iterative Convergence Methodology (ICM) provides users a methodical, tool-assisted approach to identifying design invariants. Using ICM, convergence time for a selected set of difficult properties was reduced from over three hours to around one minute. To learn more about VC Formal and to stay up to date on dates on VC Formal SIG 2019 events, visit HERE.