Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2001-06-28
2003-02-25
Lam, Tuan T. (Department: 2816)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000, C716S030000, C716S030000
Reexamination Certificate
active
06526551
ABSTRACT:
BACKGROUND
1. Field of the Invention
This invention relates to automated, formal verification techniques for logical systems such as digital circuits or communication protocol systems. More specifically, the invention relates to algorithms for such formal verification which are based on applications of graph theory.
2. Description of the Problem
Asynchronous circuits and systems are becoming an increasingly important alternative to synchronous systems. The formal verification of these circuits and systems, however, has been given somewhat less attention than their synchronous counterparts. In addition, many aggressively designed synchronous circuits rely on two-sided timing assumptions which are difficult to verify. Formal verification is often accomplished using graph theory and analysis. A logical system can assume any of a fixed set of states. These states, and their relationship to one another, can be represented by a directed graph (digraph). Such a digraph is commonly called a state transition graph (STG).
For computer analysis, a digraph such as an STG can be represented using an explicit data structure such as an adjacency list or an adjacency matrix. The decomposition of the digraph can be done in linear time using a depth-first search. However, in many real applications, the size of the digraph can be too large for explicit algorithms to be practical. One promising alternative is to use an implicit data structure to represent the digraph, for example, a binary decision diagram (BDD). Binary decision diagrams are described in an article by R. E. Bryant, “Graph-Based Algorithm for Boolean Function Manipulation,”
IEEE Transactions on Computers,
August 1986, which is incorporated herein by reference. Using a BDD, a digraph can be decomposed by finding all strongly connected components (SCC's) in the reachable state space of a finite state machine that characterizes the logical system being analyzed. Computerized algorithms that decompose a digraph in this way compute the transitive closure of the state transition relation of the machine and then compute all SCC's simultaneously. In practice, despite the advantages of an implicit data structure such a BDD, computing the transitive closure is very computationally expensive in both processor time and memory, resulting in large amounts of money and time being spent on formal verification.
SUMMARY
The present invention provides for efficient, cost-effective formal verification of logical circuits and systems using an implicit enumeration of strongly connected components that is much less computationally expensive than other known methods. Using the method of the invention, a digraph is recursively partitioned and decomposed using reachability analysis. The algorithm of the invention can be applied to partitions or legal blocks of the circuit or system being analyzed so that each one can be verified separately and hierarchically. Non-trivial, strongly connected components derived through the use of the invention can be compared to expected behavior of a circuit or system. Alternatively, the invention can be applied to detect so-called “bad cycles” which are encountered in many formal verification problems.
According to the present invention, a design is verified by first deriving a state transition graph (STG) for the design. If the logical system which is sought to be verified is large and complex, the system is partitioned into smaller logical blocks, partitions, or designs, and the algorithm is executed against each one. In any case a state transition graph for the design is recursively decomposed to determine all nontrivial strongly connected components of the STG. Each strongly connected component (SCC) represents an infinite behavior of the design. Each infinite behavior can be compared to an expected behavior in order to validate the design. This comparison can be made manually, or by a computer implemented comparison algorithm. In one embodiment, the algorithm of the invention recursively decomposes the STG by determining a backward set for each node in the STG, and finding non-trivial SCC's in the backward set. It is also possible to use forward sets, or a combination of forward and backward sets.
In another embodiment of the invention, formal verification may be extended by determining if any non-trivial SCC derived as described above represents a bad cycle indicating a problem with a design. This determination is made by finding out if a non-trivial SCC is not in any cycle set. In another embodiment, the determination is made by finding out if an SCC intersects compliment sets of all cycle sets. Either bad cycle algorithm can stop and prompt an operator or designer upon finding the first bad cycle. Alternatively, an algorithm may find all bad cycles and present these to the designer.
In example embodiments of the invention, computer software is used to implement many aspects of the invention. The software can be stored on a medium. The medium can be magnetic, such as a diskette, tape, or fixed disk, or optical, such as a CD-ROM or DVD-ROM. The software can also be stored in a semiconductor device. Additionally, the software can be supplied via the Internet or some other type of network. A workstation or computer system that typically runs the software includes a plurality of input/output devices and a processor. The software in combination with the computer system and any peripheral hardware forms the means to execute the method of the invention.
REFERENCES:
patent: 5731983 (1998-03-01), Balakrishnan et al.
patent: 5978588 (1999-11-01), Wallace
Xie, A., et al., “Implicit Enumeration of Strongly Connected Components and an Application to Formal Verification,”Proc. Of the International Conference on Computer Aided Verification,Nov., 1999.
Aho, A., et al.,The Design and Analysis of Computer Algorithms,Addison-Wesley Publishing Co., 1974.
Singhal, V., “Design Replacements for Sequential Circuits,” PhD Thesis, University of California at Berkeley, 1996.
Hasteer, G., et al., “An Implicit Algorithm for Finding Steady States and its Application to FSM Verification,”Proceedings of the ACM/IEEE Design Automation Conference,pp. 611-614, 1998.
Bryant, R., “Graph-Based Algorithms for Boolean Function Manipulation,”IEEE Transactions on Computers,vol. C35 No. 8, Aug. 1996.
Hardin, R. et al., “A New Heuristic for Bad Cycle Detection Using BDDs,”Proceedings of the International Workshop on Computer Aided Verification,pp. 268-278, 1974.
Burch, J., et al., “Symbolic Model Checking for Sequential Circuit Verification,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,vol. 13, No. 4, pp. 401-424, Apr. 1994.
Hachtel, G., et al., “Markovian Analysis of Large Finite State Machines,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,-vol. 15, No. 12, pp. 1479-1493, Dec. 1996.
Qadeer, S., et al., “Latch Redundancy Removal Without Global Reset,”Proceedings of the International Conference on Computer Design(ICCD), Oct., 1996.
Xie, A., et al., “Efficient State Classification of Finite-State Markov Chains,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,vol. 17., No. 12, pp. 1334-1339, Dec. 1998.
Brayton, R., et al., “VIS: A System for Verification and Synthesis,”Proceedings of the International Conference on Computer Aided Verification,pp. 428-432, 1996.
Beerel Peter A.
Xie Aiguo
Lam Tuan T.
Moore & Van Allen PLLC
Phillips Steven B.
University of Southern California
LandOfFree
Formal verification of a logic design through implicit... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Formal verification of a logic design through implicit..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Formal verification of a logic design through implicit... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3152315