Hachtel G.D., Somenzi F. Logic Synthesis and Verification Algorithms

Издательство Kluwer, 2002, -568 pp.This book grew from courses taught at the University of Colorado (Boulder) and at the Universidad Politecnica de Madrid, Spain. As the title suggests, we were motivated by two disparate objectives. First, the VLSI CAD group at Boulder was given the responsibility for teaching a course which satisfied the ABET requirement for an upper division algorithms and discrete mathematics course in a EE or ECE curriculum. Hence we started looking for an appropriate book, and taught trial courses from various books including [241], [162], and [190]. While each of these books had their individual strengths, there were always significant areas that were neglected.
Second, logic synthesis has matured as a field to the point of almost universal designer acceptance and is used in every major IC design/production house worldwide. Further, the younger field of formal verification, perhaps spurred on by the infamous Pentium bug, appears to be following a trajectory very much like that taken by logic synthesis over the last decade.
Consequently, we wanted an orderly integration of modern developments in logic synthesis and formal verification, into the traditional subject matter of Switching and Finite Automata Theory. This clearly eliminated texts like [241], [190], and [146]. The book that came closest to our requirements was Kohavi’s book. Although this text was excellent and long lived, it is now outdated, since it does not deal many modern developments in discrete mathematics that were significant to bringing VLSI CAD to its current advanced state.
Thus we decided to occupy the niche previously filled by the Kohavi book and supplement the coverage with recent theoretical developments most significant to the emergence of automatic synthesis and verification tools during the nineties.I IntroductionA Quick Tour of Logic Synthesis with the Help of a Simple Example
II Two Level Logic Synthesis
Boolean Algebras
Synthesis of Two-Level Circuits
Heuristic Minimization of Two-Level Circuits
Binary Decision Diagrams (BDDs)
III Models of Sequential Systems
Models of Sequential Systems
Synthesis and Verification of Finite State Machines
Finite Automata
IV Multilevel Logic Synthesis
Multi-Level Logic Synthesis
Multi-Level Minimization
Automatic Test Generation for Combinational Circuits
Technology Mapping
A: ASCII Codes
B: Supplementary Problems