JasperGold(TM) by Jasper Design Automation

Product Description

JasperGold™ Delivers:
- 100% proof of high-level requirements without simulation
- A Proving Environment that manages the proof process
- A Design Illumination mode that transfers design knowledge to the verification engineer/non-designer
* Automatic isolation of the root causes of bugs
* Formal Testplanner: design-specific methodology/requirements templates

JasperGold 3.0, a block-level verification solution for RTL designs, uses state-of-the-art formal verification technology to exhaustively verify functional behaviors of RTL blocks statically, without simulation or test vectors. JasperGold analyzes a block against high-level requirements, and either isolates bugs that cause the requirements to fail, or proves the requirements true for all legal input sequences.

High-level requirements describe end-to-end behavior (from inputs to outputs) that a design must always or never exhibit. A powerful step up from implementation-specific assertions, high-level requirements represent design intent, and cover large portions of the design. For example data can never be dropped or corrupted and flow control credits can never be leaked. If a high-level requirement is proven true, no legal set of input vectors can cause the design to fail.

JasperGold incorporates Jasper Formal Testplanner™, a knowledge base of design-specific methodology and example source code for high-level requirements. Jasper's breakthrough PreCognitive Engine™ provides the capacity necessary for 100% proof, and the JasperGold Proving Environment™ includes a context-sensitive debug environment, progress metrics, and design-specific proof navigation.

Ideally, formal verification is used during the process of RTL design, before blocks are checked in and long before simulation testbenches are available. Pragmatically, JasperGold can be used at all stages in a project, for pre- and post-silicon verification.

JasperGold(TM)

Market Segment(s)

• Embedded
• Enterprise
• Home
• Mobile

ARM Processor(s)

• ARM7EJ-S
• ARM7TDMI
• ARM7TDMI-S
• ARM720T
• ARM920T
• ARM922T
• ARM926EJ-S
• ARM940T
• ARM946E-S
• ARM966E-S
• ARM968E-S
• VFP9-S
• ARM1020E
• ARM1022E
• ARM1026EJ-S
• VFP10
• ARM1136J-S
• ARM1136JF-S
• ARM1156T2(F)-S
• ARM1176JZ(F)-S
• Cortex-A53
• Cortex-A57
• SC100
• SC200
• SC300
• ARMv8
• StrongARM
• XScale