## Verification by Error Modeling: Using Testing Techniques in Hardware VerificationVerification presents the most time-consuming task in the integrated circuit design process. The increasing similarity between implementation verification and the ever-needed task of providing vectors for manufacturing fault testing is tempting many professionals to combine verification and testing efforts. This book presents the basis for reusing the test vector generation and simulation for the purpose of implementation verification, to result in a significant timesaving. The book brings the results in the direction of merging manufacturing test vector generation and verification. It first discusses error fault models suitable for approaching the verification by testing methods. Then, it elaborates a proposal for an implicit fault model that uses the Arithmetic Transform representation of a circuit and the faults. Presented is the fundamental link between the error size and the test vector size, which allows parametrizable verification by test vectors. Furthermore, the test vector set is sufficient not only for detecting, but also for diagnosing and correcting the design errors. The practical use of any such simulation-based verification scheme can be seriously impaired by redundant faults, that otherwise require exhaustive simulations. The redundant fault identification methods are presented that are well suited for the type of faults considered. Finally, the same representation can be used to augment and expand the formal verification schemes that are to be used in conjunction with the simulation-based verification. The primary audience for Verification by Error Modeling includes researchers in verification and testing, managers in charge of verification of test and practicing engineers. Due to its comprehensive coverage of background topics, the book can also be used for teaching courses on verification and test topics. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

INTRODUCTION | 1 |

2 VERIFICATION APPROACHES AND PROBLEMS | 4 |

21 Verification Approaches | 5 |

24 Design Error Models | 7 |

25 Other Simulation Methods | 9 |

252 Other Metrics | 10 |

26 Formal Verification | 11 |

27 Modelbased Formal Verification Methods | 12 |

3 EXPLICIT DESIGN ERROR MODELS | 107 |

31 Detecting Explicit Errors | 110 |

313 Universal Test Set Approach | 111 |

4 IMPLICIT ERROR MODEL PRECURSORS | 112 |

41 Rationale for Implicit Models | 113 |

42 Related Work Error Models | 114 |

5 ADDITIVE IMPLICIT ERROR MODEL | 115 |

51 Arithmetic Transform of Basic Design Errors | 117 |

28 Prooftheoretical Formal Verification Methods | 14 |

3 BOOK OBJECTIVES | 15 |

BOOLEAN FUNCTION REPRESENTATIONS | 19 |

11 Truth Tables | 20 |

12 Boolean Equations Sum of Products | 21 |

13 Satisfiability of Boolean Functions | 23 |

131 Algorithms for Solving Satisfiability | 24 |

14 Shannon Expansion | 28 |

2 DECISION DIAGRAMS | 30 |

21 Reduced Ordered Binary Decision Diagrams | 31 |

22 WordLevel Decision Diagrams | 33 |

222 Limitations of WLDDs | 35 |

3 SPECTRAL REPRESENTATIONS | 38 |

31 WalshHadamard Transform | 39 |

32 Walsh Transform Variations | 40 |

33 WalshHadamard Transform as Fourier Transform | 41 |

4 ARITHMETIC TRANSFORM | 44 |

41 Calculation of Arithmetic Transform | 47 |

412 Boolean Lattice and AT Calculation | 48 |

42 AT and WordLevel Decision Diagrams | 49 |

DONT CARES AND THEIR CALCULATION | 51 |

12 Dont Cares in Testing for Manufacturing Faults | 52 |

13 Dont Cares in Circuit Verification | 54 |

2 USING DONT CARES FOR REDUNDANCY IDENTIFICATION | 55 |

21 Basic Definitions | 56 |

22 Calculation of All Dont Care Conditions | 57 |

222 Algorithms for Determining CDCs | 59 |

23 Algorithms for Computing ODCs | 65 |

24 Approximations to Observability Dont Cares CODCs | 67 |

TESTING | 71 |

2 FAULT LIST REDUCTION | 73 |

31 TrueValue Simulator Types | 74 |

32 Logic Simulators | 75 |

4 FAULT SIMULATORS | 79 |

41 Random Simulations | 81 |

411 Linear Feedback Shift Registers | 82 |

412 Other PseudoRandom Test Pattern Generators | 88 |

413 Final remarks | 93 |

5 DETERMINISTIC VECTOR GENERATION ATPG | 94 |

52 Search for Vectors | 98 |

53 Fault Diagnosis | 100 |

6 CONCLUSIONS | 101 |

DESIGN ERROR MODELS | 103 |

2 DESIGN ERRORS | 105 |

6 DESIGN ERROR DETECTION AND CORRECTION | 123 |

Path Trace Procedure | 125 |

62 Backpropagation | 126 |

63 Boolean Difference Approximation by Simulations | 127 |

7 CONCLUSIONS | 128 |

DESIGN VERIFICATION BY AT Using Implicit Fault Model | 129 |

2 DETECTING SMALL AT ERRORS | 132 |

22 ATbased Universal Diagnosis Set | 133 |

3 BOUNDING ERROR BY WALSH TRANSFORM | 135 |

31 Spectrum Comparison | 137 |

32 Spectrum Distribution and Partial Spectra Comparison | 138 |

33 Absolute Value Comparison | 140 |

4 EXPERIMENTAL RESULTS | 142 |

411 Improvements Neighborhood Subspace Points | 145 |

5 CONCLUSIONS | 146 |

IDENTIFYING REDUNDANT GATE AND WIRE REPLACEMENTS | 147 |

2 GATE REPLACEMENT FAULTS | 149 |

21 Redundant Replacement Faults | 150 |

211 Overview of the Proposed Approach | 151 |

31 Using Local Dont Cares | 152 |

32 Using Testing Single Minterm Approximation | 154 |

33 Redundant Single Cube Replacements | 159 |

331 Use of SAT in Redundancy Identification | 160 |

332 Passing Proximity Information to SAT | 161 |

4 EXACT REDUNDANT FAULT IDENTIFICATION | 163 |

411 Preprocessing | 164 |

51 Wire Replacement Faults and Rewiring | 166 |

52 Detection by Dont Cares | 167 |

53 Dont Care Approximations | 169 |

54 SAT for Redundant Wire Identification | 170 |

541 Approximate Redundancy Identification | 171 |

6 EXACT WIRE REDUNDANCY IDENTIFICATION | 172 |

7 IO PORT REPLACEMENT DETECTION | 175 |

8 EXPERIMENTAL RESULTS | 177 |

82 Wire Replacement Experiments | 182 |

821 True Fanin Acyclic Replacements | 184 |

83 SAT vs ATPG | 185 |

CONCLUSIONS AND FUTURE WORK | 187 |

2 FUTURE WORK | 189 |

APPENDICES | 191 |

197 | |

211 | |

### Common terms and phrases

adder algorithm applied approach approximate arithmetic circuits Arithmetic Transform assignment ATPG BDDs binary Binary Decision Diagrams BMDs Boolean difference Boolean function calculated Chapter circuit representation clauses CODC columns considered cube datapath DC set decision diagrams design errors diagnosis Equation erroneous exact Example fault coverage fault list fault model fault simulation Figure formal verification function f function representation gate and wire gate replacement errors Hamming distance Hence implementation implicit error modeling integer irredundant lattice layers Lemma LFSR manufacturing faults manufacturing testing minterms multiple netlist netlist errors netlist verification node obtained polynomial primary outputs primitive polynomial pseudo-random random redundancy identification redundant faults represented SAT formulation scheme SGRE Shannon expansion signal simulation-based verification single s-a-v faults spectral coefficients spectrum stuck-at faults subset techniques test pattern test set test vectors Theorem truth table vector set verification methods w-bit Walsh-Hadamard wire replacement errors wire replacement faults WLDDs word-level XOR gate

### Popular passages

Page 203 - Recursive learning: a new implication technique for efficient solutions to CAD problems - test, verification, and optimization," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol.

Page 208 - White. Applications of distributed arithmetic to digital signal processing: A tutorial review, IEEE ASSP Magazine, July 1989.

Page 201 - LA Entrena and K.-T. Cheng, Combinational and sequential logic optimization by redundancy addition and removal, IEEE Trans.

Page 204 - M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engineering an Efficient SAT Solver,

Page 204 - G. De Micheli, Synthesis and Optimization of Digital Circuits, McGraw-Hill, New York, 1994.

Page 201 - A note on the polynomial form of Boolean functions and related topics", IEEE Trans, on Computers.

Page 208 - DA Wood, GA Gibson, and RH Katz. Verifying a Multiprocessor Cache Controller Using Random Test Generation.