Readily Available JasperGold Apps and Their Functionalities #
The Cadence JasperGold platform offers a comprehensive suite of specialized “Apps” designed to address various verification challenges efficiently. These apps abstract much of the underlying formal complexity, making the technology more accessible to design and verification engineers.
JasperGold Formal Property Verification (FPV) App: #
This is a core application for assertion-based verification. It allows users to specify properties (e.g., using SystemVerilog Assertions or SVA) that define the correct behavior of the design. The FPV app then mathematically proves or disproves these properties exhaustively, covering all corner cases and possible input combinations. It does not require a testbench or stimuli and can begin analysis as soon as RTL is available, providing fast turnaround times.9 The Visualize debugger is frequently used with FPV to gain design insight and trace failures to their root cause. It is particularly effective for control path verification and can be applied hierarchically using a “divide-and-conquer” approach for complex designs.
JasperGold Sequential Equivalence Checking (SEC) App: #
This app is used to formally verify the functional equivalence of two different RTL circuit descriptions, even if they have sequential differences. It is crucial for verifying design changes, such as those made for clock-gating optimization, power optimization, or minor RTL modifications, ensuring they do not alter functionality. SEC is significantly faster and more exhaustive than simulation-based approaches for this task, capable of comparing large sub-system blocks or even complete SoCs. It can detect issues like “chicken bits” and radiation hardening changes.
JasperGold Superlint App: #
This app combines traditional RTL linting with formal verification capabilities to automatically derive a comprehensive set of functional checks directly from the RTL. It aims to detect and eliminate common functional design errors early in the validation process, without the need for a testbench or stimuli. The Superlint App helps improve IP design quality by reducing late-stage RTL changes by up to 80% and cutting IP development time by up to four weeks.
JasperGold Clock Domain Crossing (CDC) App: #
This app addresses the critical challenge of verifying accurate and reliable data transfer between asynchronous clock domains. It uses formal technology to identify functional and structural CDC issues early in the RTL sign-off phase. The CDC App can reduce design and verification time for IP by several weeks and is integrated with the Visualize debug environment for efficient debugging. It also offers a metastability injection flow for rigorous CDC verification.
JasperGold Coverage App / Coverage Unreachability (UNR) App: #
These apps are designed to accelerate coverage closure and provide formal signoff metrics.2 The Coverage App helps identify where the big holes in coverage are and where over-constraints exist. The UNR App specifically helps evaluate coverage unreachability, identifying unreachable items in the design and assisting in their waiver or exclusion, thereby accelerating coverage closure. The platform’s new formal coverage technologies allow for IP signoff purely within JasperGold, offering improved proof-core accuracy and new techniques for deriving meaningful coverage from deep bug hunting.
JasperGold X-Propagation App: #
This app is crucial for detecting and preventing the propagation of unknown logic values (‘X’) in designs, which can mask bugs or lead to incorrect behavior in simulation. Formal verification, through this app, can exhaustively prove whether Xs are unreachable or will not impact correct logic operation. It treats X-prone signals as both 0 and 1 to mimic hardware behavior and provides flows to check clocks, resets, and control structures for X propagation.
JasperGold Low Power Verification (LPV) App: #
This dedicated formal app enables exhaustive verification of design functionality combined with dynamic power optimization techniques. It automatically creates checks and assertions from the power intent and allows users to add custom assertions to ensure no new hazards or bugs are introduced by power optimizations. It helps catch issues like corrupted reset values, unexpected initial states in flops, and problems with isolation control signals.
Jasper C2RTL App (part of Jasper C Apps): #
Optimized for checking pipelined datapaths against their C/C++ algorithmic specifications, this app uses C++ models as the golden reference for verifying RTL implementation. It offers significant performance improvements (e.g., 100X compared to general-purpose formal engines) and allows direct comparisons of C++ and RTL code traces for root-cause analysis. It supports integer, fixed-point, and floating-point arithmetic, as well as higher-level image processing algorithms. This app is tailored for algorithm-centric and datapath-heavy applications such as AI/ML, graphics, image processing, and encryption.
JasperGold Structural Property Synthesis (SPS) App: #
This app is used early in the validation process to detect and eliminate common functional design errors and ensure code cleanliness before full validation begins. It extracts structural properties from the RTL semantics, configured from pre-defined functional checks such as dead code checks, FSM checks, and arithmetic overflow checks. It provides a fully automated flow to identify and generate checks without needing RTL annotation.
JasperGold Behavioral Property Synthesis (BPS) App: T #
his app accelerates verification closure by leveraging both RTL and simulation information to find and fill coverage holes, thereby increasing functional coverage and overall assertion density. It automatically generates properties either directly from the RTL design or from higher-level specifications.
JasperGold Reverse Connectivity App: #
This app helps verify that connections in untouched blocks remain intact when compared to a legacy design. It extracts connectivity information from a legacy design to generate a CSV file, which is then used to verify connections in the new design. This ensures that no unintended connections have been broken during design modifications.