Jasper Design Automation | Products

Products

Proof Accelerators

Accelerate Your Proofs

Verification problems exist in many design applications today such as wireless, microprocessors, networking, etc. Verification complexity can arise from complex datapath multiplexers, large internal buffers, datapath passing through
memory / FIFOs and multiple asynchronous clock domains.

Jasper's family of Proof Accelerators (PAs) is included with JasperGold® and readily accessible via Formal Testplanner™. These easy-to-use modeling components speed up formal proofs and significantly reduce the verification complexity.

Using PAs eliminates the need to reinvent the wheel for verification problems that are frequently encountered in real-world designs, and they ensure that you can put more effort in the actual verification instead of worrying about defining your model efficiently.

Engineers simply drop these pre-packaged macro models into their design to get proofs to converge. They can be used with Design Tunneling™ to converge on an exhaustive solution that would otherwise be unobtainable. They help in improving overall formal verification performance while maintaining design integrity.

FEATURES AND BENEFITS

	Speed up formal proofs with powerful modeling extensions for rapid, exhaustive verification of complex designs
	Exhaustively verify datapath logic with Jasper Scoreboard™ PA
	Enable full proof across multiple asynchronous clock domains with Clock Domain Crossing PA
	Reduce sequential depth complexity with FIFO PA
	Reduce state space complexity with Cache and Memory PAs
	Achieve full, unbounded, proofs on properties that involve logic containing multipliers with Multiplier PA

Formal TestPlanner

Jasper Formal Testplanner helps in planning and creating an effective formal verification strategy. It greatly simplifies the process of creating and managing high-level requirements. It also provides examples and templates for various functional verification components such as proof accelerators, arbiters, cache and memory controllers, Intelligent Proof Kits etc.

Scoreboard™ Proof Accelerator

With simulation, verification only occurs on the supplied vectors and so only those vectors generated by the testbench can be tested. This leads to missed sources of data corruption or not hitting corner-case bugs. Also, the higher the level of the testbench, the more complicated it is to generate specific data patterns at block-level inputs, which could lead to longer simulation runs and less verification coverage for the datapath.

With Jasper’s formal verification solution, which is exhaustive, each tested behavior is verified against all possible input sequences, so corner-case scenarios and bugs cannot be missed.

Proof Accelerators	Functionality	Examples
Verification Components	Reduce verification development costs and run-time on common design constructs.	Formal Scoreboard™, Formal Cache
Abstraction Components	Speed-up verification time by safely abstracting design features that can cause state-space explosion, thus enabling complex formal proofs	Datapath (FIFO), Cache, Memory, Multiplier
Verification Enablers	Enable complete verification of complex design behavior	Asynchronous CDC, Frequency Jitter

Jasper Scoreboard with built-in checkers enables verification of input and output data transport behavior for all possible phase and frequency jitter combinations. It detects duplicated, re-ordered, or corrupted transactions across all possible transaction types, sequences as well as multiple clock domains.

As shown in the figure on the right, the scoreboard macro is hooked up to the design under test (DUT). It compares data packets coming in (expected output) with the data packets going out (real output). There is an unexpected data packet “B” at the output which it flags immediately as a data mismatch. In this way, Jasper Scoreboard can help in verifying whether data packets are dropped, duplicated or corrupted by comparing the output of the DUT to the predicted output of the scoreboard (registered data at the input of the DUT).

Jasper Scoreboard leverages several formal modeling optimizations to enable full proofs.

Jasper Scoreboard Verifies End-to-End Data Integrity

Asynchronous Proof Accelerator

Asynchronous design challenges which have proven hard to verify using traditional verification methods include modeling non-behavior in asynchronous clock domain crossings (CDC), modeling phase and frequency jitter accurately, data path verification, etc. These complex and hard-to-identify asynchronous design issues need to be detected and verified early in the SoC design cycle.

Asynchronous Proof Accelerator enables full formal verification of asynchronous designs with multiple clock domains. It generates asynchronous effects such as phase and frequency jitters, which help in verifying the design functionality in spite of such non-deterministic effects.

Other Proof Accelerators

In addition to the Scoreboard and Asynchronous Proof Accelerators, Jasper also provides FIFO, cache and memory, and multiplier Proof Accelerators.

Reduce Verification Complexity and Time With Jasper Proof Accelerators

Jasper Proof Accelerators accurately model non-deterministic behavior in asynchronous designs, effects of phase and frequency jitter and help in data integrity verification. They greatly reduce the verification property coding effort, as designers do not have to recode the RTL. These models are optimized to provide high-performance verification when used with Jasper’s formal technology and significantly help in accelerating the overall formal proof process.