Equivalence Checking of Digital Circuits: Fundamentals, Principles, Methods
Hardware verification is the process of checking whether a design conforms to its specification of functionality. In today's design processes it becomes more and more important. Very large scale integrated (VLSI) circuits and the resulting digital systems have conquered a place in almost all areas of our life, even in security sensitive applications. Complex digital systems control airplanes, have been used in banks and on intensive-care units. Hence, the demand for error-free designs is more important than ever. In addition, economic reasons underline this demand as well. The design and production process of present day VLSI-circuits is highly time- and cost-intensive. Moreover, it is nearly impossible to repair integrated circuits. Thus, it is desirable to detect design errors early in the design process and not just after producing the prototype chip. All these facts are reflected by developing and production statistics of present day companies. For example, nowadays about 60% to 80% of the overall design time is spent for verification. This shows that verifying logical correctness of the design of hardware systems is a major gate to the problem of time-to-market. With the chip complexity constantly increasing, the difficulty as well as the importance of functional verification of new product designs has been increased. It is not only more important to get error-free designs. Moreover, it becomes an increasingly difficult task for a team of human designers to carry out a full design without errors. The traditional training of new verification engineers has to be adapted to the new situation. New skills are necessary. For these reasons, nearly all major universities offer lectures on basic verification techniques such as propositional temporal logic, model checking, equivalence checking, and simulation coverage measures. The present book is designed as a textbook covering one of the most important aspects in the verification process – equivalence checking of Boolean circuits. Equivalence Checking of Digital Circuits is a textbook for advanced students in electrical and computer engineering, but is also intended for researchers who will find it useful as a reference text.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
algorithm aliasing groups applied approach assigned value assume backward construction binary decision diagram black box Boolean formula Boolean network called canonical Chapter cofactor combinational circuits computed conjunctive normal form cutpoints cutset variables decomposition defined DEFINITION denote encoding error-free EXOR-gate F and G fanout fault finite state machines formal verification FSMs functionally equivalent h-symmetry holds implication graph independent Boolean comparison input permutation input signature function integer multiplier internal node iteration LEMMA m-ary Boolean function minterm minterm form miter one-literal clause output signature partial implementation partition Per(Xn permutation independent Boolean primary inputs primary output pseudo-Boolean function reduced ordered representation of Boolean represented respect ROBDD root node rule Section sequential circuits shown in Figure signal line single-output Boolean functions space traversal specification specified Boolean functions subsets symbol symmetric variables symmetry terminal node THEOREM truth table uniquely identified variable assignments variable order variable xi verification
Page 250 - RK Ranjan, A. Aziz, RK Brayton, BF Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. Presented at IWLS95, Lake Tahoe, CA, May 1995.
Page 243 - B. Becker, R. Drechsler, and R. Enders. On the computational power of bit-level and word-level decision diagrams. In ASP Design Automation Conf, pages 461^167, 1997.
Page 247 - A. Kuehlmann and F. Krohm. Equivalence checking using cuts and heaps.
Page 251 - P. Tafertshofer, A. Ganz, and M. Henftling. A SAT-based implication engine for efficient ATPG, equivalence checking, and optimization of netlists. In Int'l Conf. on CAD, pages 648 - 655, 1997.