Jasper Design Automation, the leader in successful deployment of production proven formal verification solutions, unveiled a powerful set of modeling extensions – Formal Scoreboard(tm) Proof Accelerator, Clock Domain Crossing (CDC) Proof Accelerator, Cache Proof Accelerator and FIFO Proof Accelerator – for the rapid and exhaustive verification of intractable datapath designs. Delivering orders of magnitude greater coverage than traditional simulation alone, the unique JasperGold® Verification System Proof Accelerators reduce complexity, improve performance and dramatically increase formal capacity. While used successfully on production computing, consumer electronics, networking, and microprocessor chips, JasperGold’s Proof Accelerators can also be used to accelerate the functional verification of any complex chip where datapath, multiple clock domains, caches and FIFOs pose a verification challenge.
Jasper is the first and only company to deliver Formal Scoreboard, a formal-optimized equivalent of a simulation scoreboard. This unique 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 unique 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, with the CDC Proof Accelerator, JasperGold users can now exhaustively 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 “formal safe” way of rapidly and successfully modeling complex caches and FIFOs. These JasperGold modeling extensions are uniquely able to manage complexity, thereby ensuring formal functional equivalents of the cache and FIFO blocks in the design.
“One of the reasons for the increasing design verification burden, is the growing pervasiveness of datapath blocks in nearly every complex SoC design.” stated Rajeev Ranjan, chief technical officer at Jasper. “We have been successfully using JasperGold for several years on datapath designs ranging from bus protocols to complex arbitration schemes. Used in combination with our unique Proof Accelerators, JasperGold is now ideally suited to tackle datapath verification. And unlike simulation, formal verification from Jasper delivers exhaustive proof and complete confidence that all possible datapath sequences have been verified.”
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. Please call +1.650.966.0245 for complete details.
About Jasper Design Automation
Jasper Design Automation’s production proven formal verification solutions are used by logic designers, verification engineers and silicon bring-up teams to explore legacy IP, conduct fast RTL debug, to ensure correctness of block-level functionality and for rapid post-silicon debug. JasperGold® Verification System delivers complete “deep formal” systematic verification, ensuring correctness of critical design features without any testbench development. JasperGold Express, a “light formal” solution, complements simulation by accelerating bug-hunting and coverage attainment.
Jasper Design Automation, the Jasper Design Automation logo, JasperGold, Formal Testplanner, GamePlan, Proof Accelerators, Lossless Abstractions, Formal Scoreboard, and Design Tunneling are trademarks or registered trademarks of Jasper Design Automation, Inc.