Jasper Property Synthesis Apps

Jasper restructured JasperGold so that it could deliver its formal technology more flexibly by having a base system and a porfolio of apps. This would also make it easier to upgrade capabilities by creating new apps. Today, Jasper announced two new apps:

• JasperGold Structural Property Synthesis (SPS)
• JasperGold Behavioral Property Synthesis (BPS)

The SPS App is used to detect and eliminate common functional design errors and ensure that the code is clean before validation starts. It is used early in the validation process without the need to write a testbench or provide stimuli. The structural properties are extracted from the RTL semantics and are used in early RTL development as well as during RTL signoff. These structural properties can be configured from a wide variety of pre-defined functional checks such as dead code checks, finite state machine (FSM) checks, arithmetic overflow checks, etc. The SPS App is tightly integrated with the entire set of JasperGold Apps drastically reducing the amount of checks that go undetected, un-proven, and un-diagnosed. Properties can be ranked, pre-classified and output in standard SystemVerilog Assertions (SVA) which can then be used in any assertion-based verification (ABV) flow such as simulation, formal analysis or emulation to increase functional coverage and reduce debug time. The SPS App provides a fully automated flow to identify and generate checks without the need to annotate the RTL.

The BPS App increases productivity and reduces time-to-market by generating assertions, constraints, and covers using the RTL and the existing simulation results obtained from batch simulations (FSDB/VCD) or interactive simulation (PLI). The BPS App is unique in its ability to create ‘white-box’ and ‘black-box’ properties as well as temporal multi-cycle properties. In addition,the BPS App can synthesize properties for signals from different modules across different levels of hierarchy. As with the SPS App, BPS provides an automated method for ranking and pre-classifying properties. The BPS App ranks synthesized properties according to their added functional verification value compared to design and manually written assertions, to reduce the number of property candidates the engineer must review. Moreover, the Apps methodology provides a unique flow that allows engineers to combine the BPS App and other JasperGold Apps to speed formal verification that significantly increases formal proof convergence. BPS supports both VCD and FSDB/VCD file formats.

SPS allows common bugs to be found early (and so cheaply) and improves the quality of verification beyond that achieved just with simulation. BPS can then be used in conjunction with simulation results to increase coverage, find coverage holes and improve the verification process.