--:: JASPER ::--

JasperGold ®

JasperExpress®

GamePlan™

Proof Accelerators

Services

JasperGold® Verification Family

Formal Verification Unleashed!

OVERVIEW
Jasper formal verification technology delivers compelling benefits throughout the entire SoC design flow, from RTL debug through verification and regression test to post-silicon debug. JasperGold Verification System provides rapid bug detection and debug as well as end-to-end full proofs of expected design behavior. It is the only production-proven formal verification solution that enables seamless scalability from formal assertion-based verification (ABV) to exhaustive end-to-end proofs of microarchitecture-level properties. Its powerful analysis capabilities and ease of use make it ideal for early-stage bug hunting as well as ensuring the highest confidence possible in your design functionality via end-to-end full proof.

JasperGold Express Verification System

BENEFITS

Provides highest verification ROI through low effort / high quality exhaustive verification
Dramatically reduces risk of bug escapes and design respins
Greatly improves verification productivity
Enables fast ramp-up from simulation ABV to full formal verification
Provides strongest verification assurance for aggressive design schedules

FEATURES

The only formal verification solution capable of exhaustively verifying block-level end-to-end High-Level Requirements (HLRs)
Unique Design Tunneling™ infrastructure enables advanced proof verification
Multiple parallelized formal engines for maximum verification
Fast, easy and complete verification using predefined 'plug-and-play' formal Proof Accelerator verification components
Pre-emptive notification of logic complexity using Formal Predictor™
Sophisticated built-in formal debugging capability and interfaces to Novas suite of debugging tools

'LIGHT FORMAL' EASES FORMAL ADOPTION
JasperGold Express Verification System delivers a powerful, exhaustive formal verification solution to users already familiar with simulation-based ABV. Simulation ABV properties are used to identify potential failures in the design without costly testbench development. Jasper's unique formal debugging environment automatically isolates the root cause of bugs down to the individual line of code and automatically generates waveforms as it detects bugs. This intuitive, integrated environment greatly reduces overall debug time.

JasperGold Express Verification System contains a broad array of powerful formal engines, each optimized for different design configurations. Engines can be run in parallel to for fast bug detection with no additional user effort required. Jasper's unique Formal Predictor provides up-front analysis that resolves the complexity of the design early before formal verification is run. Automatic counter abstraction systematically reduces proof complexity by modeling the large state space generated by counters in a formal-friendly way without any loss in verification accuracy.

No other formal ABV solution provides as rich a collection of useful analysis and debugging tools in an easily adopted formal verification solution.

'DEEP FORMAL' VERIFIES COMPLEX END-TO-END PROPERTIES
With Jasper's unique Design Tunneling formal infrastructure, JasperGold Verification System provides the highest level of deep formal productivity available. Properties can be specified as end-to-end block-level microarchitecture statements known as High-Level Requirements. These 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 ABV assertions scattered throughout the logic. JasperGold Verification System consistently performs full proofs on properties where other formal tools fail to converge, with an average of 10x proof capacity advantage over the competition.

ACCELERATE YOUR PROOFS!
Jasper's family of Proof Accelerators are included with JasperGold Verification System. These easy-to-use modeling components speed up formal proofs on

Deep Formal High-Level Requirements

significantly reduce the complexity of the verification. Often users can simply drop these models into their design to get proofs to converge. They can also be used together with Design Tunneling to converge on an exhaustive solution that would otherwise be unobtainable. Models include such components as:

Datapath modeling
Scoreboarding
FIFOs ... and more!

GamePlan Verification Planner

PLANNING FOR VERIFICATION SUCCESS
GamePlan™ Verification Planner is a verification planning tool for systematic hierarchical planning of the most complex verification tasks. GamePlan Verification Planner makes it easy to integrate formal verification into your existing simulation environment with pre-defined planning templates and powerful analysis capabilities to determine the most critical sections of the verification plan. Verification plans can be linked to external documents, and automatic HTML report generation make it easy to share verification progress with all stakeholders. GamePlan Verification Planner is available for download on the Jasper website.

EXPECT MORE FROM YOUR FORMAL
Today's challenging verification schedules demand correctness, clarity, confidence and closure. Formal verification is a powerful tool for detecting bugs early in the design flow, ensuring the RTL completely meets the specification, regression test and post-silicon debug. Together, JasperGold Express and JasperGold Verification

Systems provide the only formal analysis solution available today with seamless scalability from formal ABV all the way up to end-to-end exhaustive proofs of High-Level Requirements. Rapid bug detection and conclusive bug elimination are the keys to fast, high quality verification.