Jasper Design Automation Logo Formal Verification Unleashed!

Formal Verification Unleashed Jasper Design Automation Jasper Design Automation Contact Details Jasper Company Overview Jasper’s Formal Expert Support Jasper Design Automation's Customers Jasper-Formal Verification News and Events Jasper Design Automation Formal Verification Solutions Portfolio
Jasper Design Automation Contact Details Jasper Company Overview Jasper’s Formal Expert Support Jasper Design Automation's Customers Jasper-Formal Verification News and Events Jasper Design Automation Formal Verification Solutions Portfolio
 
Products
JasperGold®
ActiveDesign™
JasperCore™
ActiveProp
Jasper Proof Accelerators
Jasper Intelligent Proof Kits
Jasper Services
 

JasperGold® and JasperCore™

Advanced Formal Property Verification

Functional verification is a critical element in the development of today’s complex digital designs. The reality is that no matter how long you simulate or how intelligent the testbench is, validating the design intent through simulation is inherently incomplete for all but the smallest circuits. Corner-case bugs are artifacts of simulation since they are not detected due to the non-exhaustive nature of simulation-based verification.

JasperGold® enables exhaustive and complete verification and provides rapid bug detection as well as end-to-end full proofs of expected design behavior. Its powerful analysis capabilities and ease of use makes it ideal for early-stage bug hunting as well as ensuring the highest confidence possible in design functionality via end-to-end full proofs.

JasperCore™ promotes economically-scalable formal verification. It consists primarily of the formal engines which fuel the solution, and intelligent resource management schema.

JasperGold/JasperCore Flow
As shown in the flow, RTL can be visualized early in the design cycle even without a testbench or input stimulus, with powerful Visualize™ technology. Visualize displays “live” interesting waveforms and significantly speeds up design exploration fueled by understanding of behaviors and root cause analysis. If a counter-example is found, constraints can be added or modified on-the-fly using Visualize.

 
FEATURES AND BENEFITS
 
Accelerate RTL development with waveform views of design functionality and dependencies with Visualize™
Simplify debug and find interesting behaviors with QuietTrace™
Advance proof verification with unique Design Space Tunneling™ and State Space Tunneling™ infrastructure
Accelerate multiple proofs in parallel with ProofGrid™ and ProofGrid Manager™
Launch and run interactive proofs with Complexity Manager™
Enable fast, easy and complete verification using predefined and easy-to-use Proof Accelerators
Quickly and exhaustively verify standard protocols including AMBA, AXI, memory controllers, with plug-and-play Intelligent Proof Kits
 

QuietTrace™ simplifies the debug process even further. It is a unique Visualize debugging capability that finds interesting behaviors with fewer signal events. Simplification of traces with minimal signal activity accelerates exploration and debugging tasks.

The next step is to prove properties using JasperGold and JasperCore’s multiple formal proof engines. Multiple proofs can be kicked off in parallel with ProofGrid™ and proof jobs can be managed and tracked using ProofGrid Manager™. ProofGrid and ProofGrid Manager boosts the overall performance of formal verification, leveraging the power of local machine, cluster and computer farms, while providing seamless and powerful distribution and collaboration management of the proof engines running on the network, under a unified tracking console. If the property is proved, then the overall goal of proving the property is accomplished. If it fails, there are additional techniques that can help in achieving proof convergence.

Design Space Tunneling™ and State Space Tunneling™ can accelerate the proof convergence process for challenging high-level properties. High-level properties express input-to-output block-level design intent. Proving properties at these higher levels of abstraction is far more powerful and efficient than writing and testing hundreds of lower-level, individual assertions scattered throughout the logic. Complexity Manager™ assists Design Tunneling to provide visibility inside a deep cone of logic and promotes convergence of deep formal proofs for end-to-end, high-level properties.

Proof Accelerators are easy-to-use modeling components, which significantly reduce verification complexity by speeding up formal proofs. Examples include Scoreboard™ for verifying end-to-end data integrity, an asynchronous clock-domain crossing Proof Accelerator, and more.


JasperGold-JasperCore Flow

 

Intelligent Proof Kits enable SoC design teams to accelerate verification by quickly and exhaustively certifying standard protocols including AMBA, AXI, memory controllers and others.

Spectrum of Applications

Jasper delivers targeted ROI across the entire SoC design cycle ranging from architectural validation, RTL design, design and IP reuse, verification, protocol certification, low-power design, chip integration, and post-silicon validation.

 
Targeted ROI Across The Spectrum Of Applications
 
Expect More From Your Formal With JasperGold and JasperCore

Today's challenging verification schedules demand correctness, clarity and closure. Rapid bug detection and conclusive bug elimination are the keys to fast, high quality verification. JasperGold and JasperCore ensure the highest verification ROI by providing exhaustive and complete verification. It gives higher confidence and confirms that once a bug is identified and fixed, it will not resurface or introduce other bugs in the design. It dramatically reduces risk of bug escapes and design respins and greatly improves verification productivity.

Copyrights © 2000 -2011 Jasper Design Automation, Inc. All rights reserved.
Privacy Policy | Trademarks