Jasper XPROP App
Key Benefits
- Avoids issues from “X optimism” or “X pessimism”
- Provides rapid X-propagation fault analysis
- Requires no knowledge of formal or SVAs
Employing special formal engines with correct “X” semantics, the Cadence® Jasper™ X-Propagation Verification (XPROP) App analyzes your register-transfer level (RTL) design to ensure that no unexpected ‘X’ values emerge and propagate. The app automatically creates and executes checks for sources of, and conditions that lead to, unwanted Xs. A customized GUI provides rapid X-propagation fault analysis. And the best part? You don’t need to know assertion-based verification or SystemVerilog Assertions (SVAs).
The semantics of X are language and tool dependent. In RTL design, X tells the synthesis tool that it doesn't matter whether a 0 or 1 is assigned during logic optimization and in verification. But in simulation, X tells the simulator that a signal value is “unknown.” This mismatch in semantics and incomplete test vectors in simulation can hide bugs that are likely to show up in silicon no matter how careful you are about considering “X optimism” or “X pessimism.”
The Jasper XPROP App automatically creates exhaustive checks for unwanted Xs on various design elements, such as:
- Clocks and resets to ensure that they are free of Xs
- Control and data structures to see which areas of the code Xs can propagate to
- Outputs to see if Xs can be propagated out of the design
The Jasper XPROP App’s GUI is highly optimized for the desired workflow: a wizard guides the setup and configuration to control the source and targets for Xs. The debug waveform/CEX GUI always gives a concise failure trace with the path of the detected Xs from source to destination.
Key Features
- The Fault Analysis view quickly points out the reason(s) for the X, significantly speeding up debug and reducing the effort needed to find X-related bugs
- Combined with our powerful Jasper Visualize™ Interactive Debug Environment, the app allows you to add or modify constraints on-the-fly to test out “what if?” scenarios before modifying the RTL
- Provides higher throughput by allowing multiple proofs in parallel to be managed and tracked using the Jasper ProofGrid™ Intelligent Resource Manager
-
Jasper RTL Apps
- Jasper FPV App
- Jasper Sequential Equivalence Checking App
- Jasper Design Coverage Verification App
- Jasper Coverage Unreachability App
- Jasper X-Propagation Verification App
- Jasper Control and Status Register App
- Jasper Connectivity Verification App
- Jasper Superlint App
- Jasper Behavioral Property Synthesis App
- Jasper Low-Power Verification App
- Jasper Security Path Verification App
- Jasper Clock Domain Crossing App
- Formal VIP
- Jasper FSV App