Formal-verification technology is steadily gaining credence as a way to ferret out well hidden bugs in designs. Yet formal technology suffers from the huge number of state spaces found in nanometer designs. They're simply becoming too large for even the most powerful computers to verify.
Intended to overcome limitations of other formal tools, JasperGold's PreCognitive Engine overcomes the capacity problem by using what's called State Space Tunneling. This technique guides the tool's formal proof engines to analyze only those portions of the design relevant to proving each requirement, without having the user modify the design.
Some formal tools attempt to address capacity issues by using various techniques that limit the state-space exploration to a small "proof radius." This can result in sacrificing the goal of 100% verification, as well as missing corner-case bugs found in the unproven segments of the design outside the proof radius. JasperGold's PreCognitive Engine doesn't use restrictive proof radius bounding of the state space. Rather, requirements are proven across the entire design state space to ensure that blocks are bug-free.
Rather than operate at the assertion level, JasperGold executes spec-level requirements. These are captured either in Verilog or translated from higher-level languages. Such an approach enables users to fully capture the spec-level requirements for a design block and exhaustively verify that the requirements are met. Requirements are captured in many fewer lines of register-transfer level (RTL) than the design block itself, typically one-tenth to one-hundredth the number of lines.
A wide variety of standard interfaces offer prebuilt Jasper Proof Kits, including a new PCI Express kit. Today, the tool is applicable to control logic and datapath-related design blocks that don't undergo data transformation or perform mathematical computations.
JasperGold is available now. Prices start at $225,000.
Jasper Design Automation
www.jasper-da.com