JasperGold Connectivity Verification App

Key Benefits

Captures complex specifications in familiar, human, and machine-readable formats
Generates all properties automatically
Performs exhaustive verification in hours vs. days or weeks
Debugs fast via QuietTrace™ debug technology

Capturing complex specifications in a familiar format, the JasperGold^® Connectivity Verification App allows you to exhaustively verify the static/structural, temporal, and conditional connectivity of intellectual property (IP) blocks inside a system on chip (SoC). Specifically, the app first takes the connectivity specification – captured in an Excel or OpenOffice spreadsheet, comma-separated-values (CSV) files, or an IP-XACT xml file – and the implementation register-transfer level (RTL) as inputs. Then the app automatically generates structural, behavioral, and temporal connectivity checks, exhaustively verifying the connectivity is as specified. A utility is included so you can quickly black-box out the internals of IP blocks to keep the analysis focused on connectivity.

While “correct by construction” tools and techniques go a long way, errors can still creep in due to unclear or erroneous specifications, the addition of low-power structures, built-in self-test (BIST), and JTAG support, or downstream changes/engineering change orders (ECOs) that weren’t fully propagated. In addition, connectivity of a sub-module that appears correct may prove to be erroneous in a larger scope.

JasperGold Connectivity Verification App performs exhaustive verification in hours, not the days or weeks common for simulation-based approaches. Unlike competitive formal connectivity apps that output noisy, hard to read counterexamples (CEX), the app’s QuietTrace™ debug technology shows errors via “low-noise”, minimum-length CEX traces for high user productivity. Since creating the connectivity definition can be tedious and error-prone, the app can also extract connectivity from a golden RTL and verify any unintended changes in a subsequent RTL revision. The app is completely automated, so you won’t need to learn formal or SystemVerilog Assertions (SVAs).

Key Features

Supports all connectivity types: unconditional/static (i.e. basic "point-to-point"), constant and dynamic conditional, combinational value propagation without latencies, and sequential value propagation with latencies
Captures the connectivity description in open, human, and machine-readable Excel/OpenOffice spreadsheets, comma-separated-values (CSV) files, or IP-XACT xml
Includes a utility to quickly black-box out the internals of IP blocks so the verification only focuses on connectivity
Makes it easy, once the connectivity description is set up, for you to fully automate this flow and run it in a regression mode
Includes innovative reverse connectivity capability, enabling you to automatically create a high-level connectivity specification from your known-good design
Supports parallelism with our ProofGrid formal engine control utility

REQUEST A DEMO

JasperGold Formal Verification Platform (Apps)