JasperGold Behavioral Property Synthesis App

High-quality assertions and properties are critical to improve verification coverage, expose code and functional coverage holes, and achieve high confidence in the quality of the design. However, writing assertions in standard languages such as SVA or Property Specification Language (PSL) 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 automatically creates a wide range of properties that span many behavioral patterns. In addition to the built-in properties, you can guide the app to create focused libraries of properties with the included BPS Templates capability. 

The app helps users enhance verification coverage and identify RTL bugs in several ways: 

1.   The app may generate a property indicating a specific behavior that you did not anticipate. This may be an indication that the RTL is out of spec.

2.   A generated cover can indicate that the testbench has a limited reach and a verification hole is present in the available simulation suite. 

3.   When the generated assertions are included with the intellectual property (IP) block and inserted into the next higher layer of hierarchy, suddenly firing assertions indicate bugs and/or spec mismatches. 

Key Features

• Automatically classifies properties to drastically reduce the need for manual review of generated properties
• Provides an unbiased review of your design specification, testbench, and verification plan
• Automatically extracts properties from simulation traces—with or without knowledge of the RTL
• Automatically classifies the derived properties (assert/assume/cover)
• Automatically ranks the derived properties as high-/medium-/low-value, and supports further qualification by leveraging our formal engines under-the-hood
• Includes BPS Templates that enable you to increase the “signal-to-noise” ratio of generated properties, automatically creating reusable packages of protocol or structural-focused properties
• Provides ability to override any of the app's selections
• Can be used in “vectorless”, formal-only flows without simulation, and in post-silicon debug flows
• Seamlessly integrates with the Visualize™ debug and "what if?" analysis capability of the Cadence® JasperGold Formal Property Verification App