Property Synthesis

Many designs today rely on assertion-based verification, whether simulation, formal verification or emulation. High-quality assertions and properties are critical to improve verification coverage, expose functional coverage holes, and achieve high confidence in the quality of the design. However, writing assertions in standard languages such as System Verilog Assertions (SVA) demands specialized knowledge. Even for experts, it can be extremely time-consuming to manually create all the properties required.

The JasperGold Behavioral Property Synthesis App increases productivity and reduces time-to-market by generating assertions, constraints, and covers using the RTL and simulation information. The properties generated from the BPS App are automatically ranked and pre-classified and can be output in standard SVA which can then be used in any assertion-based verification (ABV) flow such as simulation, formal or emulation to increase functional coverage, aid in verification closure, and reduce debug time.

The JasperGold Structural Property Synthesis solution is used early in the validation process without the need to write a testbench or provide any stimuli. The structural properties are extracted from the RTL semantics and are used in early RTL development as well as RTL sign­-off. 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 JasperGold SPS App is tightly integrated with the entire set of JasperGold Apps drastically reducing the amount of checks that go undetected, unproven, and undiagnosed. 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 JasperGold SPS App provides a fully automated flow to identify and generate checks without the need to annotate the RTL.

 

Learn more about the JasperGold Behavioral Property Synthesis App.

Learn more about the JasperGold Structural Property Synthesis App.