ActiveProp™ Assertion-based Verification System

Accelerate Assertion-based Verification

  • Generate standard SVA for formal, simulation and emulation
  • Jump-start and automate assertion creation compared to writing assertions manually
  •  Eliminate common RTL design errors with automatic assertion creation from RTL before testbench creation with ActiveProp Structural Property Synthesis
  • Identify simulation-based functional coverage holes to increase functional coverage and reduce debug time with unique multi-cycle analysis and hierarchy support with ActiveProp Behavioral Property Synthesis
  •  Extract block level constraints from simulation for usage with formal property verification
  • Enhance formal proof convergence and usage with push-button validation flow available with JasperGold formal property verification integration

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 SystemVerilog Assertions (SVA) or PSL demands specialized knowledge. Even for experts, it can be extremely time-consuming to manually create all the properties required.

Jasper’s ActiveProp™ property synthesis increases productivity and reduces time to market by generating assertions, constraints, and covers using the RTL and the existing simulation information. ActiveProp properties are ranked, pre-classified and output in standard SVA or PSL which can then be used in any assertion-based verification (ABV) flow such as simulation, formal or emulation to increase functional coverage and reduce debug time. ActiveProp can enhance formal verification with JasperGold formal property verification by capturing “assumes” from simulation and exporting them seamlessly into JasperGold.


ActiveProp screenshot

ActiveProp automatically generates assertions, contraints, and covers from RTL and simulation information.



Structural Property Synthesis

Structural property synthesis helps eliminate common functional design errors and make sure the code is clean before validation starts! The structural properties are extracted from the RTL semantics and are used for early RTL development as well as RTL sign-off. These structural properties can be configured from a wide variety of checks such as dead code checks, FSM checks, arithmetic overflow checks, etc. 

Behavioral Property Synthesis

Behavioral property synthesis accelerates verification closure by leveraging both RTL and simulation information to find coverage holes, increase functional coverage and raise the overall assertion density.

These automatically synthesized properties are intelligent. ActiveProp extracts critical expressions to guide, simplify and merge properties to reduce the number of property candidates the engineer must review. It includes multi-cycle analysis for improved temporal property quality. Properties can be extracted among signals from different modules across different levels of hierarchy.

The flexible use model allows simulation information to be provided via an existing FSDB or VCD file or via the simulator PLI link at runtime. 

Adopt and Accelerate Assertion-based Verification with ActiveProp

ActiveProp reduces the need to create assertions manually and helps engineers learn about assertions. Designers and verification engineers can use ActiveProp in standalone mode to generate standard human-readable SVA properties. Designers can use it in conjunction with JasperGold RTL Development App to study and explore design functionality fast for new or existing designs. Verification engineers can use it with JasperGold Apps to expand the set of verification properties, identify coverage holes and increase formal proof coverage.

ActiveProp increases engineering productivity and shortens the overall schedule so that the focus can be shifted to other important verification tasks rather than spending time on manually creating these assertions from scratch. It consequently accelerates the adoption of assertion-based verification.