May 3, 2004 -- Jasper Design Automation has announced its Provably Correct Design methodology, enabled by new technology in release 3.0 of Jasper's flagship product, JasperGold. Provably Correct Design offers a new paradigm for when and how to apply formal verification, and to what types of problems.

Provably Correct Design allows users to guarantee that their designs will meet fundamental high-level requirements, derived from the micro-architecture specification. 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.

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'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.

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 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 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.

Formal verification tools have traditionally been applied to problems involving relatively small portions of design logic. In contrast, JasperGold 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 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 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 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 Proving Environment in JasperGold 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