| Mountain View, Calif. –
April 9, 2008 – Jasper Design Automation, the leader
in successful deployment of production proven formal verification
solutions, today unveiled a powerful set of modeling extensions
– Formal Scoreboard™ 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.”
Availability
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. For expert help with large scale formal
verification deployment, RTL exploration or post-silicon
debug, please visit http://www.jasper-da.com.
|
