The Cadence® Jasper™ Formal Property Verification (FPV) App fully validates block-level properties and high-level requirements. It enables exhaustive and complete verification and provides rapid bug detection as well as end-to-end full proofs of expected design behavior. With its powerful analysis capabilities and ease of use, the app is ideal for early-stage bug hunting as well as for ensuring the highest confidence possible in design functionality via end-to-end full proofs.
Unlike other formal tools, the Jasper FPV App provides unique debug and “what if?” analysis with the Jasper Visualize™ Interactive Debug Environment and QuietTrace™ debugging capability. Visualize technology displays “live” interesting waveforms and significantly speeds up debug. If a counterexample is found, you can add constraints or modify on the fly using the Visualize capability. QuietTrace technology simplifies and accelerates the debug process even further by calculating the minimum signal activity needed to exhibit the behavior in question.
These capabilities make the Jasper FPV App ideal for early-stage proofs, deep bug hunting, and expedited debug. Furthermore, the Complexity Manager provides visibility inside a deep cone of logic and promotes convergence of deep formal proofs for end-to-end, high-level properties.
With its wall clock runtime, low memory consumption, and the overall ability of the high-performance formal engines, the Jasper FPV App can scale to increasingly larger design sizes. Whether you’re a novice taking advantage of our "wizards" and other automated capabilities or a formal power user leveraging the many optional configuration controls, the Jasper FPV App’s GUI provides the industry’s most efficient, easy-to-use workflow.
Key Features
- High-performance formal engines exhaustively prove complex assertions utilizing advanced formal techniques
- The Jasper ProofGrid™ Intelligent Resource Manager gives you a unified tracking console for live updates and detailed controls over the formal engines as they progress toward a solution. It simultaneously leverages the power of the local machine, cluster, and computer farms, while providing seamless and powerful distribution and collaboration management of the proof engines running on the network.
- Formal scoreboarding support enables verification of datapath designs, tracking end-to-end packet integrity by detecting dropped, duplicated, or corrupted data.
The Jasper FPV App supports SystemVerilog Assertion (SVA) or Property Specification Language (PSL) properties, Verilog or VHDL designs under test (DUTs), and also Unified Power Format (UPF) when used in conjunction with our Jasper Low-Power Verification (LPV) App.
