Although the use of Formal Verification tools has become more popular and easier since they were first introduced, creating assertions can still be challenging and time demanding. Jasper Design Automation has introduced ActiveProp™, a new property synthesis tool that helps accelerate the adoption of assertion-based verification, including formal verification, by automatically generating high-level properties in standard SVA format.

ActiveProp produces SVA properties (assertions, constraints and covers), as well as human-readable reports, based on RTL and simulation information. ActiveProp automatically synthesizes these properties from waveforms or simulation runs to expand the verification property set, increase functional coverage, and identify coverage holes.
The new tool is certainly a step forward in the use of assertions and formal methods in designing integrated circuits. ActiveProp helps designers capture the intent of the design, something that an engineer might know intrinsically but fail to document and test, since it "just feels obvious". The new tool can be used standalong in conjunction with third party simulators, or integrated with Jasper's own products.
"ActiveProp delivers tremendous ROI by automating the creation of properties from RTL and simulation data, producing high-quality results faster than ever thought possible," said Kathryn Kranen, Jasper President and CEO. "Deploying ActiveProp standalone greatly improves verification efficiency for any assertion-based verification flow. It can also be used with Jasper formal tools to achieve faster proofs with JasperGold®, or with ActiveDesign™ to enable rapid exploration of design functionality."

Stand-Alone ActiveProp Flow

ActiveProp generates intelligent properties automatically, with a large proportion of useful, high-quality properties. Multiple simulation runs can further refine the intelligence of generated properties. Unique multi-cycle analysis contributes to property quality, and generates properties where the causal effects are far removed from the resulting effects, not just two or three cycles away. ActiveProp also handles hierarchy, extracting properties across different modules and levels of hierarchy.
In addition, ActiveProp features a number of pre-defined checks including identification of syntactic and other errors; static checks such as arithmetic overflow, bus conflicts, and CDC checks; and formal checks and verification to prevent deadlock, mitigate unwanted X propagation, and more.

ActiveProp Integrated With Other Jasper Tools

The inputs to ActiveProp are RTL, simulation information and scoped signals of interest which the user controls. Any simulation or testbench, block, system–level, or full SoC, can be used as input. ActiveProp simulator input can be provided in two ways, either running ActiveProp on previously created VCD/FSDB files, or linked runtime with the simulator via its PLI. The output of ActiveProp is industry-standard SVA properties that can be used in a variety of ways:

• Standalone: Extract interface constraints, transactions, etc.; generate reports with human-readable SVA; automatically create SVA modules for simulation, emulation or formal analysis
• With ActiveDesign: Creates a powerful design-exploration flow to answer “what-if” questions by composing extracted covers, and comparing formal-generated waveforms to simulation waveforms
• With JasperGold: Uses JasperGold formal verification to prove generated assertions and covers, highlight RTL code based on generated properties, classify coverage holes and assertion failures, and accelerate convergence during design-space and state-space tunneling flows.