Traditionally, formal verification is used after the fact for bug hunting or design-rule checking. It has yet to be applied up front, where it would affect design decisions at the RTL coding stage. However, the release of JasperGold 3.0 and an accompanying methodology could alter users' perceptions of formal verification. JasperGold 3.0 looks at RTL blocks during the design stage to ensure that they meet fundamental high-level requirements even before they're "checked in" for system simulation.
In most simulation-based verification approaches, design concurrency and complexity can only be fully explored late in the design cycle. Often, key interdependencies between blocks in a design can't be examined in simulation until it's too late. As a result, extremely complex bugs turn up in the last stages of the process, if they turn up at all.
With JasperGold 3.0 and Jasper's Provably Correct Design methodology, designers of any given RTL block incrementally prove that each implemented aspect of the design's functionality works as intended as the RTL evolves. Users apply the tool early in the RTL coding process before the blocks are submitted to verification teams for system simulation (see the figure).
Typically, formal tools are applied to implementation-specific assertions that relate to relatively small portions of the RTL. JasperGold 3.0 differs in that it has the capacity and speed to prove what the company calls high-level requirements, which specify end-to-end microarchitectural behavior for the entire block. For example, a high-level requirement for a block might be that data is always transmitted through the block correctly without ever being duplicated, dropped, or corrupted. That single high-level requirement would replace checking for a series of low-level assertions dealing with the behavior of a retry buffer or packet arbiter.
New to JasperGold 3.0 is an adjunct tool called Formal Testplanner, which is a knowledge base of design-specific methodology tips. Intended to get users past the "blank-page syndrome" in crafting high-level requirements for design blocks, Formal Testplanner provides strategies and examples of Verilog source code for high-level requirements. It simplifies the creation and management of requirements and quickly gets users up the learning curve for the tool.
In examining RTL blocks, the tool's interactive use model extends capacity. The user fully controls the level of interactivity from step-by-step navigation to pushbutton automation. The tool performs exhaustive, unbounded proofs until it uncovers all bugs.
Also new in version 3.0 is what Jasper calls the "proving environment." The tool looks at a block waveform by waveform, color-coding both the signals and their related RTL code. It provides design-specific "next steps" in proceeding with verification, steering users through the design and quickly uncovering root causes of bugs.
JasperGold 3.0, including Formal Testplanner, is available now. A one-year time-based license costs $225,000 for the base engine and $45,000 per user license.
Jasper Design Automationwww.jasper-da.com