JasperGold: Behavioral Property Synthesis App


Assertion-Based Verification and Behavioral Property Creation
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 PSL demands specialized knowledge. Even for experts, it can be extremely time-consuming to manually create all the properties required. What designers and verification engineers need are:

  • The ability to automate the deduction and generation of properties for their RTL
  • A methodology that can take into account existing simulation stimulus and/or consider the RTL and the waveform(s) together when extracting properties
  • Support for automatically classifying and categorizing the generated properties so as to reduce the signal-to-noise ratio
  • A mechanism to control the type of properties that are considered and generated
  • Finally, a comprehensive reporting system to allow engineers and managers to track the progress of “coverage”

The Jasper Solution
The JasperGold® Behavioral Property Synthesis App automatically deduces and extracts from your RTL and simulation traces (FSDB or vcd files) behavioral patterns and time/signal values and expresses them as SVA properties. Then it automatically classifies them as assertions or cover properties and also prioritizes them into high/medium/low value categories. This enables engineers with no knowledge of SVA to generate many valuable properties quickly, saving many weeks of tedious error-prone work.

The App automatically creates a wide range of properties that span many behavioral patterns. In addition to the built-in properties, users 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 the user 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 IP block and inserted into the next higher layer of hierarchy, suddenly firing assertions indicate bugs and/or spec mismatches.

Whitepaper: Property Synthesis Throughout the Design Flow for Application in Formal Verification, Simulation, and Emulation

  • 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 Jasper’s formal engines under-the-hood
  • Includes BPS Templates that enable users 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(TM) debug and "What If?" analysis capability of the JasperGold® Formal Property Verification App, as well as other JasperGold Apps like Coverage, Low Power, and Structural Property Synthesis (SPS)

  • Generate valuable properties – both assertions and cover properties in matter of minutes. No knowledge of SVA required
  • Can be used at any stage of the verification, even before simulation testbenches are available
  • Automatically classify properties to drastically reduce the need for manual review of generated properties
  • Provides an unbiased review of your design specification, testbench and verification plan
  • Use of BPS Templates enables rapid, automatic creation of focused, reusable packages of protocol or structural-specific properties