June 2, 2008 -- Avery Design Systems, Inc. today announced Insight, a new formal analysis tool that delivers a deterministic bug hunting and coverage closure process with flexibility and complements today’s SystemVerilog-based intelligent testbench methodologies.

"Formal analysis can be made significantly more productive by breaking the RTL synthesis barrier and tapping into the key information about design intent and environment which is captured in today’s intelligent testbench methodologies," said Chilai Huang, president of Avery Design Systems. "Unlike conventional formal analysis tools that run orthogonal to simulation-based methods, Insight complements simulation making it more broadly within reach of designers and verification engineers alike."

Insight performs formal analysis to hunt down deep, corner-case bugs in designs and improve functional coverage resulting in shortened functional verification cycles and higher design quality. Insight can be used at numerous phases of design implementation. For example, in processor verification, Insight can be used for sequential bug hunting by comparing instruction set simulator (ISS) and RTL pipeline implementations as well as at later stages when optimized RTL pipeline implementations are available. Insight is based on a mixed logic and symbolic simulation engine, called Fusion, that works in conjunction with several formal satisfiability (SAT) and word-level algebraic solver engines.

Insight's algebraic solver utilizes current multi-core platforms to break a problem into several sub-problems to be solved in parallel. In bug hunting mode, Insight targets an intelligent testbench’s assertions and scoreboard checkers (reference model based or ad hoc) to find sequential non-compliance and then generates transaction-level counterexamples which are replayed through the existing testbench. In coverage closure mode, Insight targets coverage monitor points that are missed using constrained random verification (CRV) methods and deterministically generates transaction-level directed Page 2 of 3 tests. Existing intelligent testbenches are easily extended for use with Insight’s symbolic verification. Insight automatically generates directed tests that can be added to existing simulation regression suites.

Insight delivers other benefits beyond conventional approaches including: bug hunting and coverage closure is deterministic and requires significantly fewer verification cycles over CRV approaches; less setup time required and more reliable results achieved by leveraging an intelligent testbench that is already hardened first in simulation before it is used in formal analysis; and fewer new assertions and constraints need to be added to the intelligent testbench to run comprehensive formal analysis compared to other formal tool approaches.

Avery Design has made a white paper on Insight available entitled, “Applying Symbolic Bug Hunting and Coverage Closure Methods to Processor Verification”. To receive an electronic copy, please email insight@avery-design.com.

Pricing and Availability