Employing special formal engines with correct “X” semantics, the JasperGold® X-Propagation Verification App analyzes your RTL design for X-propagation issues. The app then automatically creates and executes checks for sources/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 and/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 JasperGold X-Propagation Verification App reads your RTL and automatically creates and executes checks for sources/conditions that lead to unwanted Xs, 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 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
A 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 Visualize™ technology, 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 to be kicked off in parallel with ProofGrid while proof jobs can be managed and tracked using ProofGrid Manager in a regression mode