Browse Prior Art Database

Method and System for Enhanced Formal and Semi-Formal Verification using Simulation, Reduction, and Case-Splitting Strategies

IP.com Disclosure Number: IPCOM000212747D
Publication Date: 2011-Nov-27
Document File: 9 page(s) / 36K

Publishing Venue

The IP.com Prior Art Database

Abstract

A framework for efficient semi-exhaustive as well as exhaustive simulation of logic designs is disclosed. This framework consists of an auto-tuner which determines how wide of bit-parallel simulation vectors to attempt to push through the design, as well as a variety of transformation and case-splitting techniques to reduce the number of patters that need to be analyzed.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 14% of the total text.

Page 01 of 9

Method and System for Enhanced Formal and Semi -Formal Verification using Simulation, Reduction, and Case-Splitting Strategies

Formal and semiformal verification techniques are powerful tools for the construction of correct logic designs. They have the power to expose even the most probabilistically uncommon scenario that may result in a functional design failure, and ultimately have the power to prove that the design is functionally correct - i.e. no failing scenario exists. However, formal verification techniques do not scale very well in practice, since they require resources that are exponential with respect to design under verification. Semi-formal techniques apply formal algorithms in a resource-bounded manner, resulting in much higher coverage when compared to simulation, but coverage generally decreases as the size of design under verification increases.

In most cases, the use of symbolic algorithms such as Binary Decision Diagrams or Boolean satisfiability solvers constitutes the most scalable method to exhaustively analyze the behavior of a system, even for an incomplete time-bound of behavior. However, there are complex problems for which symbolic solvers are basically ineffective, immediately encountering fatal capacity problems which would require exponential runtime vs design size. This is particularly true for designs with complex arithmetic such as multipliers. In such cases, logic simulation may constitute the best mechanism to analyze the behavior of the design. In particular, one may use a bit-parallel simulator to analyze the behavior of the design relative to a fairly large number of test cases executed in parallel and packed into machine words. Using such an approach, one may cover a large set of design behaviors - in cases, even exhaustively covering design behavior. Unfortunately, exhaustive simulation generally requires analysis of an exponential number of patterns with respect to the number of inputs in the design times the depth to be analyzed.

Disclosed is a framework for efficient semi-exhaustive as well as exhaustive simulation of logic designs. This framework consists of an auto-tuner which determines how wide of bit-parallel simulation vectors to attempt to push through the design, as well as a variety of transformation and case-splitting techniques to reduce the number of patters that need to be analyzed.

A design verification using semi-formal techniques is described. Methods to efficiently simulate the netlist, utilizing bit-parallel simulation to dramatically increase the simulator throughput are disclosed. Also disclosed are several techniques to transform the design and make it more amenable to simulation. These techniques include:


* Reducing the number of RANDOM gates to enable higher simulation coverage.


* Reducing the number of RANDOM gates via cofactoring.


* Reducing the number of RANDOM gates via circuit reparameterization.


* Reducing the number of RANDOM gates via case-splitting.

A netl...