JASPER DESIGN AUTOMATION PIONEERS PROVABLY CORRECT DESIGN METHODOLOGY

State of the Art Proving Environment and Formal TestPlanner Dramatically Enhance JasperGold Verification System 3.0 User Experience JasperGold Verification System.

Mountain View, Calif. – May 3, 2004– Jasper Design Automation announced today the first-of-its-kind Provably Correct Design methodology, enabled by innovative new technology within release 3.0 of Jasper’s flagship product, JasperGold Verification System™.  Provably Correct Design offers a new paradigm for when and how to apply formal verification, and to what types of problems. JasperGold Verification System release 3.0 provides the capacity, performance, and usability to enable the breakthrough methodology.

Provably Correct Design allows users to guarantee that their designs will meet fundamental high-level requirements, derived from the micro-architecture spec. The process of Provably Correct Design provides users with insightful and specific feedback into how designs could possibly fail, influencing design creation to improve inherent design quality.

JasperGold Verification System has already been used on 40 customer chips”, says Kathryn Kranen, president and CEO of Jasper.  “We’ve seen our experienced end users apply JasperGold Verification System earlier and earlier in the design process.  With that has come a major shift in mentality - from ‘verify-after-the-fact’ to ‘prove-as-you-design’. We’ve dramatically enhanced JasperGold Verification System to facilitate the Provably Correct Design methodology.”

When to Apply Provably Correct Design

Provably Correct Design advocates early application of formal verification, before RTL blocks are checked in by designers, and long before simulation testbenches are available.  Early formal verification ensures that bugs are found while designs are still fluid and the cost of bug fixes - as well as the risk of collateral damage associated with those bug fixes - is still low.  JasperGold Verification System’s pure formal approach means no testbench, stimulus, or simulator license is required.

After RTL check-in, formally-proven, “clean” design blocks are integrated into system simulation, dramatically shortening overall schedules.

How to Apply Provably Correct Design

With this methodology and enabling tool, users incrementally prove that each piece of design functionality works as intended, as the design evolves.  The user – typically the RTL designer or verification engineer - specifies a high-level requirement of the design under creation, and then challenges JasperGold Verification System to do one of two things: either find a sequential combination of inputs that violates the requirement, or confirm that the requirement is met under all possible circumstances.  In the case of a failure, JasperGold Verification System returns the precise scenario that would trigger the failure, and enables the user to quickly expose the root cause of the bug, isolated down to the faulty line of RTL.  This capability dramatically enhances verification productivity, in contrast to a simulation-only approach, in which users try to create all possible stimulus scenarios and checks in order to empirically test whether or not a design will fail, and spend hours or days manually diagnosing the cause of each failure.

Type of Problems Addressed by Provably Correct Design and JasperGold Verification System

Formal verification tools have traditionally been applied to problems involving relatively small portions of design logic.  In contrast, JasperGold Verification System delivers the capacity and performance to prove high-level requirements on designer-sized blocks.  A powerful step-up from local assertions, a high-level requirement specifies end-to-end micro-architecture behavior. Formal verification of high-level requirements greatly enhances verification coverage and provides measurable proof of quality.  Some examples of high-level requirements proven by JasperGold Verification System include data is always transmitted correctly, without ever being dropped, duplicated or corrupted; flow control credits do not leak from your system under any corner-case scenario; and no sequencing of abnormal, infrequent error conditions can ever corrupt the control in your design.

JasperGold Verification System 3.0 and Formal Testplanner Power Provably Correct Design

JasperGold Verification System™ 3.0 is a major expansion to Jasper’s RTL formal verification product that provides the critical capabilities to make Provably Correct Design possible. JasperGold Verification System 3.0 incorporates Formal TestPlanner™, a knowledge base of design-specific methodology tips, formal verification strategy, and example source code for high-level requirements. Formal Testplanner greatly simplifies the creation and management of high-level requirements, and jumpstarts the learning curve for Provably Correct Design. The highly-productive Proving Environment in JasperGold Verification System 3.0 accelerates time to complete proof, with state-of-the-art new proof engines and the addition of features such as progress metrics, a design illumination mode, and design-specific next step guidance.

Pricing and Availability

JasperGold Verification System 3.0, including Formal Testplanner, is currently available and is priced as a one-year time-based license: $225,000 for the base engine and $45,000 per user license.

About Jasper

Founded in 1999, Jasper Design Automation is a privately-held Electronic Design Automation (EDA) company headquartered in Mountain View, CA.  Enabling the first Provably Correct Design, JasperGold Verification System™ exhaustively verifies that your complex design blocks meet their high level requirements as defined by the micro-architecture spec.  By focusing on “what” to check, not “how”, JasperGold Verification System formally verifies designer-sized blocks without any test-bench development.  Pre-verified, bug-free blocks are then integrated into system-level verification trimming months off the verification schedule.  For further details visit: http://www.jasper-da.com.           

 #                      #                      #

 Jasper Design Automation, the Jasper Design Automation logo, Tempus Quest, JasperGold Verification System and Formal Testplanner are trademarks of Jasper Design Automation, Inc. All other names mentioned are trademarks, registered trademarks, or service marks of their respective companies.