E-Book Content
A Surv ey of T echniques for F ormaleri cation V of Combinational Circuits Jawahar Jain1 Amit Nara yan2 M. F ujita1 A. Sangiovanni-Vincentelli 2 tation veri cation typically proceeds in two phases. In the rst phase, a Boolean network representing the original design is extracted from the RTL description or the transistor level netlist [40, 14, 15, 38, 63]. In the second phase, the correctness of this Boolean network is veri ed using some formal methods. In this paper we will focus only on the second phase. We will describe some recent advances made in the area of verifying the equivalence of two Boolean networks. More speci cally, we will focus only on the veri cation of combinational circuits i.e., circuits in which the outputs depend only on the current inputs (as opposed to sequential circuits in which the outputs depend not only on the present inputs but also on the past sequence of inputs). Some sequential veri cation problems can also be reduced to a combinational veri cation problem (e.g. when the corresponding latches in the two designs can be identi ed). Although techniques exist for verifying general sequential circuits, currently it is not practical to verify large industrial designs using them. The combinational veri cation problem can be stated as follows: Given two Boolean netlists, check if the corresponding outputs of the two circuits are equal for all possible inputs. This problem is NP-hard and hence a general solution which can handle arbitrary Boolean functions is not likely to exist. However, since the functions that are implemented in practice are not random Boolean functions, various techniques have been developed which can successfully verify large designs. Research in combinational equivalence checking has seen signi cant and rapid improvements since introduction of OBDDs [13]. Thus, details of numerous equivalence checking techniques [19, 27, 29, 45, 55, 59, 64, 65, 66, 6