A set of four modeling extensions to Jasper Design Automation’s Proof Accelerators provides for fast—and exhaustive—verification of intractable datapath designs. Jasper’s JasperGold Proof Accelerators can be used to speed the functional verification of any complex chip design in which datapath, multiple clock domains, caches, and FIFOs pose challenges.
The four modeling extensions are Formal Scoreboard Proof Accelerator, Clock Domain Crossing (CDC) Proof Accelerator, Cache Proof Accelerator and FIFO Proof Accelerator.
In Formal Scoreboard, a formal-optimized equivalent of a simulation scoreboard, verification engineers will find a collection of checks and techniques which exhaustively ensures datapath design functionality. For blocks containing multiple asynchronous clock domains, Jasper’s clock-domain-crossing (CDC) Proof Accelerator enables exhaustive formal verification of design blocks historically known to be particularly challenging to verify. Despite the rapid increase in the number and complexity of clock domains in today’s system chips, the CDC Proof Accelerator exhaustively verifies the correctness of a design across all clock edge combinations, including clock variation and jitter.
While both cache and FIFO verification typically result in state-space explosion, Jasper’s Cache and FIFO Proof Accelerators provide a “formal safe” way of rapidly and successfully modeling complex caches and FIFOs. These JasperGold modeling extensions are able to manage complexity, thereby ensuring formal functional equivalents of the cache and FIFO blocks in the design.
The set of four JasperGold Verification System Proof Accelerator extensions—Formal Scoreboard, Clock Domain Crossing, Cache and FIFO—are currently available with the JasperGold Verification System. Contact Jasper Design directly for pricing and delivery information.
Jasper Design Automation
www.jasper-da.com