Logic Synthesis And Verification Algorithms

by Hachtel, Gary D.

• ISBN13: 9780387310046
• ISBN10: 0387310045
• Format: Paperback
• Copyright: 2006-03-01
• Publisher: Springer Verlag

Summary

Logic Synthesis and Verification Algorithms is a textbook designed for courses on VLSI Logic Synthesis and Verification, Design Automation, CAD and advanced level discrete mathematics. It also serves as a basic reference work in design automation for both professionals and students. Logic Synthesis and Verification Algorithms is about the theoretical underpinnings of VLSI (Very Large Scale Integrated Circuits). It combines and integrates modern developments in logic synthesis and formal verification with the more traditional matter of Switching and Finite Automata Theory. The book also provides background material on Boolean algebra and discrete mathematics. A unique feature of this text is the large collection of solved problems. Throughout the text the algorithms covered are the subject of one or more problems based on the use of available synthesis programs.

Table of Contents

I. Introduction	1	(72)
Introduction	5	(42)
VLSI: Opportunity and Challenge	5	(2)
Manufacturing Technology	5	(1)
Design technology	6	(1)
Why VLSI	7	(1)
VLSI Processes	7	(1)
Design Styles	8	(6)
Design Decomposition	8	(2)
Logic (Circuit) Design Styles	10	(4)
Overview of Optimal Logic Synthesis	14	(10)
Area-Time Tradeoff Curves	15	(1)
The Technology Independent View --- A Bit-Serial Full Adder Circuit	16	(2)
The Technology Dependent View --- Technology Mapping	18	(1)
Testing --- Is What I Fabricated What I Wanted?	19	(2)
Graph Models and Finite State Machines	21	(3)
Successors and Predecessors	24	(1)
Graph Algorithms and Complexity	24	(9)
Complexity	24	(2)
Computing the Product of Sets of Sets	26	(1)
Longest Paths	27	(2)
Backtracing	29	(3)
Complexity of Computing the Longest Path	32	(1)
Asymptotic Complexity (or just complexity)	33	(4)
Worst Case Asymptotic Upper Bound Complexity	34	(2)
Complexity of Algorithms	36	(1)
Practical Complexities	36	(1)
Brief Summary of MOS Device Behavior	37	(2)
Notes	39	(1)
Summary	39	(1)
Problems	39	(8)
A Quick Tour of Logic Synthesis with the Help of a Simple Example	47	(26)
A Simple Case Conversion Circuit	47	(2)
First Refinement	49	(1)
The Transform Block	50	(4)
The CC Block	52	(1)
An Optimized Transform Block	53	(1)
The Command Interpreter	54	(3)
Checking for Equality	54	(1)
Optimizing the Command Interpreter	54	(3)
Technology Mapping	57	(1)
Problems	58	(15)
II. Two Level Logic Synthesis	73	(178)
Boolean Algebras	77	(50)
Sets, Relations, and Functions	77	(8)
Sets	77	(2)
Relations	79	(1)
Reflexive Binary Relations	80	(4)
Functions	84	(1)
Partial Orders	85	(10)
Partially Ordered Sets	86	(1)
Hasse Diagrams	87	(1)
The Meet and Join Operations	87	(2)
Totally Ordered Sets, Well-Ordered Sets, and Induction	89	(1)
Lattices	90	(2)
Definition of Boolean Algebras	92	(1)
Examples and Properties of Boolean Algebras	92	(3)
Boolean Functions	95	(8)
Boolean Formulae	96	(1)
Boolean Functions	97	(1)
Boole's Expansion Theorem	98	(1)
The Minterm Canonical Form	99	(2)
Pseudo-Boolean Functions	101	(1)
The Boolean Algebra of n-variable Boolean Functions	101	(1)
Atoms of a Boolean Algebra	101	(2)
Don't Care Conditions as Boolean Function Algebra Intervals	103	(3)
Satisfiability Don't Care Conditions	104	(1)
Observability Don't Care Conditions	105	(1)
Deriving Don't Cares From and Interval Specification	106	(1)
Incomplete Specification of Boolean Functions	106	(2)
Incompletely Specified Switching Functions	106	(1)
Incompletely Specified Boolean Functions	107	(1)
Notes	108	(1)
Summary	108	(1)
Problems	108	(19)
Synthesis of Two-Level Circuits	127	(58)
Design Optimality	127	(2)
Two-Level Logic	129	(3)
Cost Functions for Two-Level Implementations	130	(1)
Minimality and Testability	131	(1)
Sums of Products and Products of Sums	132	(2)
Implicants and Prime Implicants	134	(1)
Quine's Prime Implicant Theorem	134	(1)
Iterated Consensus	134	(4)
Consensus and Implications: A Digression	135	(1)
The Tabular Method of Computing the Prime Implicants	135	(2)
Iterated Consensus in General	137	(1)
Recursive Computation of Prime Implicants	138	(3)
Selecting a Subset of Primes	141	(2)
The Unate Covering Problem	143	(9)
Reduction Techniques	146	(1)
Essential Columns or Variables	146	(1)
Row or Constraint Dominance	146	(1)
Column or Variable Dominance	147	(1)
Systematically Exploring the Search Space	148	(1)
Computation of the Lower Bound	149	(3)
The Branch-and-Bound Algorithm	152	(8)
Choice of the Splitting Variable	154	(1)
Examples of Splitting and Lower Bounding	155	(5)
The Unate Covering Problem as an Integer Linear Program	160	(1)
Multiple Output Functions	160	(4)
Multiple-Output Primes	161	(2)
Formulating the Covering Problem	163	(1)
Incompletely Specified Multiple Output Functions	163	(1)
Notes	164	(1)
Summary	165	(1)
Problems	165	(20)
Heuristic Minimization of Two-Level Circuits	185	(34)
Local Search	185	(6)
Local Search Applied to Logic Minimization	187	(3)
A Simple Local Search Algorithm for Logic Minimization	190	(1)
Checking for Equivalence and Tautology	191	(9)
Unate Functions	194	(3)
Additional Speed-Up Techniques for Tautology Checking	197	(2)
Examples of Tautology Checks	199	(1)
Choosing the Right Direction	200	(3)
Recursive Complementation	201	(2)
Using the OFF-set in the Expansion	203	(1)
Identifying Essential Primes	203	(1)
Multiple-Valued Logics	204	(1)
Notes	205	(1)
Summary	206	(1)
Problems	206	(13)
Binary Decision Diagrams (BDDs)	219	(32)
Representing Logic Functions with BDDs	220	(11)
Binary Decision Diagrams by Way of Examples	220	(2)
Formal Definition of BDDs	222	(3)
How to Build the BDD for f	225	(1)
Reduced BDDs	226	(4)
Why Ordering is Important	230	(1)
Design Considerations for a BDD Package	231	(2)
Algorithms	233	(10)
The ITE Algorithm	234	(3)
Complement Edges	237	(1)
The Computed Table	238	(1)
Conditioning of the ITE Calls	238	(2)
The ITE.CONSTANT Algorithm	240	(3)
Notes	243	(1)
Summary	244	(1)
Problems	244	(7)
III. Models of Sequential Systems	251	(154)
Models of Sequential Systems	255	(70)
Introduction to Finite State Machines	255	(2)
Synthesis of Finite State Machines	257	(4)
FSMs: Definitions, Notation, and Examples	261	(4)
Examples	261	(2)
Incomplete Specification	263	(2)
FSM Minimization for Completely Specified Machines	265	(10)
Identifying the Equivalent States of an FSM	265	(4)
State Equivalence Checking: the Partition/Refinement Approach	269	(3)
Finding the Reduced Machine	272	(1)
Moore Machines and DFAs	272	(1)
The Iterative Collapsing Approach	273	(2)
Summary of State Equivalence Checking Methods	275	(1)
Graph Algorithms for FSM Traversal	275	(14)
Graphs, Subgraphs, and Components	276	(2)
Graph Traversal --- Breadth First Search	278	(2)
Traversal --- Depth First Search	280	(2)
Finding the SCCs of a Directed Graph	282	(4)
Shortest Paths	286	(3)
Models of Sequential Systems	289	(3)
FSTs: Strings, Runs, Reachability and Products	292	(8)
Finite State Transition Structures	292	(3)
NFAs and ε-moves	295	(1)
FSTs as Labeled Digraphs	295	(2)
Strings, Tapes and Runs of FSTs	297	(1)
Product of FSTs	298	(2)
FSM Equivalence Checking	300	(5)
Strings which Distinguish Two Machines	300	(1)
Building the Product Machine	301	(4)
Equivalence Identification by Isomorphism	305	(1)
Reachability Analysis	305	(3)
FSM Traversal Using Binary Decision Diagrams	305	(3)
Symbolic FSM State Traversal	308	(4)
Transition Relations and Symbolic Image Computation	308	(4)
Notes	312	(1)
Summary	313	(1)
Problems	313	(12)
Synthesis and Verification of Finite State Machines	325	(44)
Minimization of Incompletely Specified Machines	325	(10)
Finding the Compatible Pairs	328	(1)
Finding the Maximal Compatibles	329	(1)
Finding the Prime Compatibles	329	(3)
Setting up the Covering Problem	332	(2)
Forming the Reduced Table	334	(1)
The Binate Covering Problem	335	(8)
Formulation of BCP	337	(1)
Reduction Techniques	337	(3)
Choice of the Splitting Variable and Bounding	340	(1)
Maximal independent set	340	(1)
Choice of the branching column	341	(1)
Infeasible problems	341	(1)
An Example of Reductions	342	(1)
State Encoding	343	(4)
Practical Encoding Algorithms	343	(4)
Decomposition and Encoding	347	(9)
Partitions	348	(2)
Partitions with Substitution Property	350	(2)
Computation of the S.P. Partitions	352	(2)
General Decomposition and State Encoding	354	(2)
Notes	356	(1)
Notes	357	(1)
Summary	357	(1)
Problems	357	(12)
Finite Automata	369	(36)
Finite Automata and Regular Languages	370	(8)
String Acceptance	372	(1)
Languages of Finite Automata	373	(3)
Complements of Languages	376	(1)
Examples	377	(1)
DFA Synthesis	378	(9)
Determinization of FSTs and FAs	383	(1)
The Subset Construction	383	(2)
The Deterministic Image	385	(2)
ω-Regular Automata	387	(3)
Formal Verification with L-Automata	390	(2)
ω-Regular Languages	390	(2)
ω-regular Language Containment	392	(5)
Lifting Acceptance Conditions to a Product L-Automaton	393	(1)
Example of Product L-Automaton	393	(1)
BDD Representation of Cycle Sets and Recur Edges	394	(1)
The Language Containment Algorithm	395	(1)
Example of Containment Check	396	(1)
Notes	397	(1)
Summary	397	(1)
Problems	398	(7)
IV. Multilevel Logic Synthesis	405	(118)
Multi-Level Logic Synthesis	409	(46)
Introduction	409	(3)
Networks and Algebraic Operations	410	(2)
Representation Issues and Choices	412	(5)
Alternate Node Representations	413	(4)
Representing Switching Functions in Factored Form	417	(5)
Factored Forms	417	(1)
Algebraic and Boolean Expressions	418	(1)
Algebraic and Boolean Factored Forms	419	(1)
Value of a Factorization	420	(1)
Equivalent, Maximal, and Optimum Factorizations	420	(2)
Size, Unateness, and Cofactors of a Factored Form	422	(1)
Division	422	(3)
Kernels and Co-Kernels	425	(3)
Computation of Co-Kernels and Kernels	427	(1)
Heuristic Factoring Algorithms	428	(8)
Generic Factoring Algorithm	429	(4)
Quick Factor	433	(1)
Good Factor	434	(1)
Boolean Factor	434	(1)
Summary of Factoring Algorithms	435	(1)
Rectangle Covering	436	(1)
Decomposition and Restructuring	436	(4)
Algebraic Resubstitution	436	(1)
Selective Node Elimination	437	(2)
Extraction	439	(1)
Notes	440	(1)
Summary	441	(1)
Problems	441	(14)
Multi-Level Minimization	455	(20)
Introduction	455	(1)
Boolean Networks	456	(5)
Network Cost	459	(2)
Don't Cares in Multi-Level Networks	461	(3)
Satisfiability Don't Cares	461	(1)
Observability Don't Cares	462	(1)
Use of Don't Cares in Minimization	462	(1)
Internal and External Don't Cares	463	(1)
External Satisfiability Don't Care Conditions	463	(1)
External Observability Don't Care Conditions	463	(1)
Internal Satisfiability Don't Cares	464	(1)
Observability Don't Cares	465	(3)
Computing ODCs with the Boolean Difference	468	(1)
Prime and Irredundant Networks	468	(1)
Two-Level Minimization with Multi-Level Don't Cares	469	(1)
Notes	470	(1)
Summary	470	(1)
Problems	471	(4)
Automatic Test Generation for Combinational Circuits	475	(30)
Introduction	475	(1)
Faults and Fault Models	476	(2)
Automatic Test Generation	478	(10)
Excitation and Sensitization	478	(3)
A Simple Test Generation Algorithm	481	(2)
Implications and Backtracking	483	(3)
Choice of the Decision Variables	486	(2)
Putting the Pieces Together	488	(1)
Redundancy Removal	488	(4)
Notes	492	(1)
Summary	492	(1)
Problems	492	(13)
Technology Mapping	505	(18)
Graph Covering and Technology Mapping	506	(1)
Choice of Base Functions	507	(1)
Creating the Subject Graph	508	(1)
The DAG-Covering Problem	509	(1)
Tree Covering by Dynamic Programming	509	(3)
Decomposition	512	(1)
Delay Optimization and Graph Covering	513	(1)
Notes	514	(1)
Summary	514	(1)
Problems	515	(8)
ASCII Codes	523	(2)
Supplementary Problems	525	(12)
Bibliography	537	(18)
Index	555