Jasper rolls ActiveProp property synthesis tool

Jasper Design Automation Inc. has released the ActiveProp property synthesis tool with the intention to accelerate the adoption of assertion-based verification, including formal verification and simulation.



Main features:
. Generate standard SVA for formal, simulation and emulation
. Jump-start and automate assertion creation compared to writing assertions manually
. Expand verification property set with intelligent properties
. Increase functional coverage with unique multi-cycle analysis and hierarchy support
. Identify and fix coverage holes

The inputs to ActiveProp include the RTL, simulation information and the opportunity for users to scope signals, or points of interest in the design. Based on these three inputs, ActiveProp automatically generates (SystemVerilog Assertion) SVA properties in human-readable format in the form of constraints, asserts, covers and HTML reports.

The next step is to review the properties.

If the property generated is good, it can be certified, published in SVA format, and exported to any standard assertion-based verification flow.

If the property generated discovers real issues, there are three options:
• If a coverage hole is found, more tests can be added in order to refine the property over multiple simulation runs. This process can be simply repeated to increase coverage
• If an RTL bug is found, the RTL can be modified and the property can be re-generated
• If the property is different than design intent, it could be edited and published in SVA

The analysis flow, with ActiveProp synthesis, can be iterated multiple times to refine the properties as required and finally publish all properties as the SVA output.


ActiveProp works in synergy with existing Jasper formal solutions, namely ActiveDesign and JasperGold, for intelligent properties, for design exploration and for improved convergence.

The designer or verification engineer can review and debug the SVA properties generated from ActiveProp using Visualize technology in either ActiveDesign or JasperGold. ActiveDesign can help designers during property review by generating transaction-level wave forms that are useful in understanding properties, design behaviors and accelerating the overall RTL development process.


Availability:
Now

To access a video presentation on ActiveProp, click here.