Jasper Unveils Proof Accelerators

Delivering greater coverage than traditional simulation alone, the JasperGold® Formal Verification System Proof Accelerators reduce complexity, improve performance and increase formal capacity. The Accelerators can be used to accelerate the functional verification of any complex chip where datapath, multiple clock domains, caches and FIFOs pose a verification challenge.

Formal Scoreboard is a formal-optimized equivalent of a simulation scoreboard. This collection of checks and techniques exhaustively ensures datapath design functionality. For blocks containing multiple asynchronous clock domains, Jasper delivers a Clock Domain Crossing (CDC) Proof Accelerator. This Proof Accelerator enables 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, with the CDC Proof Accelerator, JasperGold users can now verify 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 way of rapidly and successfully modeling complex caches and FIFOs by ensuring formal functional equivalents of the cache and FIFO blocks in the design.