Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
1998-07-17
2001-10-23
Smith, Matthew (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000
Reexamination Certificate
active
06308299
ABSTRACT:
BACKGROUND OF THE INVENTION
1. Field of the Invention
This invention pertains in general to equivalence checking tools and in particular to a method and system for combinational verification using multiple verification techniques.
2. Description of Background Art
In the field of digital electronics, it is often necessary to determine whether two digital circuit designs are functionally equivalent to each other. Circuits consist of combinational and sequential storage elements. The equivalence determination can be achieved by comparing corresponding combinational blocks of the two circuits. Logic techniques are used to achieve this comparison.
Given two combinational netlists representing combinational blocks of circuits, which have the same sets of inputs and outputs, combinational verification determines if, for every possible input combination, the outputs of the netlists evaluate to the same Boolean value. This problem is known to be coNP-hard, but several real-world techniques have been developed to solve it.
The design methodology which is responsible for deriving one circuit design from the other virtually assures that, besides the pairs of corresponding outputs of the netlists, many internal net pairs should also be equivalent. These equivalent net pairs are called “cutpoints.” By decomposing the combinational verification into smaller problems through the use of cutpoints, combinational verification can be performed on complex netlists.
The central idea behind decomposing the problem into smaller problems using cutpoints is that if f
1
(x)=g
1
(x) for all values of the input vector x, and if f
2
(y,z)=g
2
(y,z) for all values of y and z, then f
2
(f
1
(x),z)=g
2
(g
1
(x),z) for all values of x and z. However, the converse is not true, namely, if f
2
(y,z)≠g
2
(y,z), we cannot say whether f
2
(f
1
(x),z) equals g
2
(g
1
(x),z). This unknown is termed the “false negative problem.” There are two possible resolutions of this problem: either f
2
and g
2
are not equivalent (a real negative), or f
2
and g
2
are equivalent (a false negative). The process of resolving this unknown is called “cutpoint resolution.”
One approach to cutpoint resolution uses binary decision diagrams (BDDs) to represent the netlists. A BDD represents a function as a rooted, directed, acyclic graph, with each non-terminal node labeled by a function variable. Each non-terminal node has two outgoing edges, corresponding to the cases where the function variable evaluates to zero or one. The terminal nodes are labeled with zero or one, corresponding to possible function values. For any assignment to the variables, the function value is determined by tracing a path from the root to a terminal node by following the appropriate branch from each node.
In a BDD-based approach, cutpoints are introduced, and intermediate functions are represented as f(X, Y), where X={x
1
,x
2
, . . . ,x
n
} is the set of variables denoting primary inputs and Y={y
1
,y
2
, . . . ,y
1
} is the set of variables denoting the cutpoints. Each y
i
&egr;Y is associated with a BDD representing its function
h
i
(
X
,
{
y
{
i
+
1
}
,
…
,
y
l
}
)
,
wherein y
i
's are in increasing order from the outputs toward the inputs and y
j
cannot depend on y
k
if k≦j. If two BDDs f(X, Y) and g(X, Y) are not equal, a cutpoint resolution problem exists.
The resolution can be obtained by starting with the BDD for [f(X,Y)≠g(X,Y)] and then iteratively composing the cutpoints until the resulting BDD is independent of y
i
's. A composition is achieved using the BDD-compose operation first described by R. Bryant, Graph-based Algorithms for Boolean Function Manipulation,
IEEE Transactions on Computers, l C-
35:677-691, August 1986, which is hereby incorporated by reference herein. This operation composes y
i
into s(X,Y), which represents
∃
y
i
:
s
(
X
,
Y
)
⋀
(
y
i
≡
h
i
(
X
,
{
y
{
i
+
1
}
,
…
,
y
l
}
)
)
.
If, after all compositions, the final BDD represents zero, a false negative exists. If the final BDD represents one, a true negative exists.
Heuristics for selecting cutpoints are very important in a compositions-based method. To this end, C. A. J. van Eijk, Formal Methods for the Verification of Digital Circuits, Eindhoven: Technische Universiteit Eindhoven, 1997, presents heuristics to select cutpoints so the cutpoint resolution problem does not occur often or is not too difficult to resolve. These heuristics assume that a node is a good cutpoint if its number of fanouts is large or if it is evenly spaced between other cutpoints. Another heuristic, described in Y. Matsunaga, “An efficient equivalence checker for combinatorial circuits,”
Proceedings of the
33
th ACM/IEEE Design Automation Conference,
pp. 629-634, June 1996, determines the order in which cutpoints are composed.
The process of successive composition does not work well if the two candidate netlists are actually unequal (the true negative case). The inequality cannot be determined until a sufficient number of cutpoints have been composed such that primary input variables appear in the BDD. This process is extremely computationally expensive. The system can be configured to threshold the composition scheme by a maximum BDD size, but such a technique results in slower execution and may miss real cutpoints. Since many resolutions yield true negatives, especially when the designs are not equivalent, it is important for the equivalence checker to be equally robust for both the true and false negative cases.
Another approach to combinational verification using cutpoints, described by D. Brand, Verification of Large Synthesized Designs,
Proc. Int'l Conference on Computer
-
Aided Design,
534-537, 1993, uses automatic test pattern generation (ATPG) techniques. An ATPG technique decides the equality of two functions, by determining if there exists a test pattern that tests the presence of a stuck-at-zero fault at the exclusive-or of the two functions. If the technique determines that such a test pattern exists, the function from one circuit is substituted in place of the function in the other circuit. This approach, however, is less effective than BDD-based methods when the required test pattern does not exist. Thus, many approaches use the ATPG-based algorithm only when the standard BDD-based algorithm fails.
The observations that different methods were strong on different classes of circuits prompted approaches using filters. One approach uses a set of combinational verification engines as filters through which the problem instances pass. This approach works well on a large class of circuits; however, if an unsuitable method is applied before the most suitable method, it can be very computationally expensive.
Another, more advanced, approach is to dovetail between the different verification methods to make the problem instance pass through methods with increasing resolution thresholds. The motivation for this approach is that dovetailing avoids committing to using a method on an instance for which the method is not suited. However, this approach still has limitations which can be understood by comparing the performance of this approach with an imaginary tool which uses an oracle; when presented with an equivalence check problem, this oracle magically picks the best method to solve this problem. The dovetail approach necessarily performs worse than the oracle, since the dovetail approach will waste effort on incorrect methods.
Even the oracle, however, can only choose between discrete methods to apply to the problem. The performance of the oracle can be beat, therefore, by allowing methods to work together on a problem and share information among the methods.
Accordingly, there is a need in the art for a method and system of combinational verification that allows multiple methods to work on a problem and share information among the methods. Such methods should preferably be tightly integrated and the method and system should
Burch Jerry R.
Singhal Vigyan
Cadence Design Systems Inc.
Kik Phallaka
Lyon & Lyon LLP
Smith Matthew
LandOfFree
Method and system for combinational verification having... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method and system for combinational verification having..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and system for combinational verification having... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2598890