Next Generation Formal Technology to Boost Verification

With growing complexities and sizes of SoCs, verification has become a key challenge for design closure. There isn’t a single methodology that can provide complete verification closure for an SoC. Moreover creation of verification environment including hardware, software, testbench and testcases requires significant resources and time. Formal verification tools have been there in the semiconductor design industry and are known to provide exhaustive verification coverage without the need of any testbench. However, they use assertions for particular verification tasks. For performing assertion checks, specific properties are defined in standard languages such as SVA (System Verilog Assertion) and PSL (Property Specification Language). Here is the problem; for designers it’s very difficult to learn assertion languages and use them for design verification to get the full benefit of formal technology.

Clearly, this is an opportunity available for EDA vendors to automate and ease the verification process where formal technology is combined with ABV (Assertion-based Verification). This approach can provide tremendous benefits provided it can be used efficiently in the overall verification environment. Cadencehas been working since a few years on filling up this gap. Today, I am happy to see this approach really working in Cadence’s JasperGold Formal Verification Platform which is quite nicely integrated with the Incisive Platform.

This platform provides a unique and innovative way to address the pain points of using formal and ABV technologies. JasperGold (Cadence acquired Jasper Design Automation in 2014) provides Verification Apps that are targeted to solve specific verification problems. The apps are seamlessly integrated between different applications through a common database. They can be easily setup and run. As they are vertically integrated into the overall system, the problems are solved most efficiently using the formal and ABV methods with support from simulation and other metric-driven technology. The needed properties for ABV or formal verification can be automatically created or even pre-packaged properties can be used. Also, Jasper’s patented Visualize[SUP]TM[/SUP]Formal Debug and What-If Analysis environment provides instant feedback on any change in any particular parameter. The effective verification, analysis and debug platform provides 15x performance gain compared to previous solutions.

The JasperGold Apps Platform is very rich with several verification apps including ‘Formal Property Verification’, ‘Behavioral Property Synthesis’, ‘X-Propagation Verification’, ‘Control/Status Register Verification’, ‘Coverage Unreachability’, ‘Sequential Equivalence Checking’, ‘Security Path Verification’, and many more. Also a custom app can be created for any specific task. The platform architecture is extensible for developing and deploying new apps as needed in the future. There is a single GUI that allows different applications to work together with a consistent look and feel, thus improving designers’ productivity and analysis efficiency.

Incisive and JasperGold formal engines are combined together for an exhaustive search to find deeper bugs quicker. With the support of different engines, complete proof of properties is obtained on datapath, control logic as well as memory. All combinations of inputs are tried without a testbench. With new formal-assisted simulation methods, deep state-space penetration is done for very deep bug hunting. The new Trident engine provides word-level and memory abstractions that significantly boost performance.

This platform is integrated with the Cadence System Development Suite where formal-assisted simulation, emulation and verification closure management can be performed in sync with each other. The Indago[SUP]TM[/SUP] debug infrastructure provides a powerful debugging environment. The Indago resources include ‘Debug Analyzer App’, ‘Embedded Software Debug App’, ‘Protocol Debug App’, and ‘Advanced Debug Analyzer App’ that provides on-the-fly what-if analysis for design exploration and debugging.

In formal-assisted emulation with Palladium XP II, the assertion-based VIP complements accelerated VIP. The assertion-based VIP coded in SVA can replace the checkers which cannot be compiled on Palladium platform and hence removed by accelerated VIP. The formal property creation from emulation traces also assists in debugging.

The JasperGold is integrated with Incisive vManager to assist in verification status management and closure. The report can clearly show the status of tasks completed by formal. The coverage unreachability app (UNR) automatically generates properties to explore coverage holes and determines if the holes are reachable or unreachable. The unreachable cover points form an unreachable coverage database that guides users to exclude these unreachable cover points, thus saving time.

The JasperGold SPS (Structural Property Synthesis App) integrates automatic formal analysis with the basic HAL (Cadence HDL Analysis) and provides a fully integrated lint solution. Property grading, violations, and waivers can be analyzed and managed with ease in the Visualize[SUP]TM[/SUP] GUI environment.

A new LPV App for low-power verification has also been added in JasperGold platform. It performs all low power functional checks, power-aware sequential equivalence check, and runs other formal apps in power-aware mode. This combined with Incisive low-power simulation and Conformal low-power capabilities form a powerful low-power verification solution.

It was a very pleasant occasion talking to Pete Hardee, Product Management Director at Cadence who explained about this innovative solution in detail. I see this as a unique solution in the verification segment of EDA that significantly boosts verification performance and productivity. The Next-generation JasperGold Formal Verification Platform is being released this month. A live presentation/demo can be seen at Cadence booth #3515 in DAC.

Pawan Kumar Fangaria
Founder & President at www.fangarias.com