Efficient Branch and Bound Search with Application to Computer-Aided Design

I Theory.- 1 Introduction.- 1.1 Branch-and-Bound Search.- 1.2 Efficient Branch-and-Bound Search.- 1.3 Justification with Branch-and-Bound.- 1.4 Why Use Justification Equivalence?.- 1.5 Prior Work.- 1.6 Organization of the Book.- 2 Justification Equivalence.- 2.1 Introduction.- 2.2 Justification Decomposition.- 2.3 Properties.- 2.4 Identification of Shared Justification Decisions.- 2.5 Justification Equivalence.- 2.6 Efficient Representation.- 2.7 An ATPG Example.- 2.8 Summary.- 3 Justification in Finite State Space.- 3.1 Introduction.- 3.2 What is State Justification?.- 3.3 Justifiability of States.- 3.4 State Justification Equivalence.- 3.5 Covering Properties.- 3.6 An Example.- 3.7 Summary.- II Applications.- 4 Sequential Circuit Test Generation.- 4.1 Introduction.- 4.2 What is Sequential Circuit Test Generation?.- 4.3 Complexity of Test Generation.- 4.4 How Can Justification Equivalence Help?.- 4.5 Prior Work.- 5 Fault Effects.- 5.1 Introduction.- 5.2 Fault Effect Analysis.- 5.3 Summary.- 6 The Sest Algorithm.- 6.1 Introduction.- 6.2 The Control Flow.- 6.3 Complexity of Retrieval.- 6.4 Implementation.- 6.5 Summary.- 7 Experimental Results.- 7.1 Introduction.- 7.2 Experimental Procedures.- 7.3 ATPG Time Proportions.- 7.4 SEST Efficiency Evaluation.- 7.5 Benchmark Results.- 7.6 Summary.- 8 Redundancy Identification.- 8.1 Introduction.- 8.2 Why is Redundancy Identification Needed?.- 8.3 Prior Work.- 8.4 Efficient Redundancy Identification.- 8.5 Summary.- 9 Logic Verification.- 9.1 Introduction.- 9.2 Prior Work.- 9.3 Logic Verification via Test Generation.- 9.4 Summary.- 10 Conclusion.- A Sest User's Guide.- A.1 Introduction.- A.2 Command Synopsis.- A.3 Options.- A.4 Inputs and Outputs.- A.5 Output Files.- A.6 Example.- A.7 Down-Loading SEST from the Disk.- A.8 Reporting Bugs.- A.9 Author.- References.