Tool provides hierarchical verification
By Gabe Moretti -- EDN, July 8, 2004
Designers know that using a hierarchical approach to circuit design improves the quality of results and often decreases development time. Verification engineers often separately verify blocks of a design before integrating them into circuits to perform validation tests on the integrated system. Formal verification methods are still evolving, and engineers have little tool support in using hierarchical methods for formal verification. In many cases, formal verification tools cannot handle large designs, so engineers have to manually keep track of verified blocks and invent their own integration-verification procedures.
Jasper Design Automation has addressed these problems with the JasperGold 3.0 tool, which supports “provably correct design” methodology (Picture). This approach to verification advocates early application of formal methods before designers check in RTL blocks. Users can specify a high-level requirement of the block under creation and then use JasperGold to either find a sequential combination of inputs that violates the requirement or confirm that the design meets the requirement under all possible circumstances. In case of failure, JasperGold returns the scenario that would trigger the failure and enables users to find the cause of the design error. Designers can then stitch together formally verified blocks and have only to verify that the they have properly implemented the interface protocols among the various blocks.
Designers can interactively use the tool, and verification engineers can set up batch execution of the product for regression testing. Combining JasperGold with Formal Testplanner provides a complete environment for hierarchical formal verification. Price for JasperGold 3.0, including Formal Testplanner, is $225,000 for a one-year time-based license for the base engine and $45,000 per user license.
Jasper Design Automation, 1-650-966-0200, www.jasper-da.com.
