Atjaunināt sīkdatņu piekrišanu

Formal Equivalence Checking and Design Debugging 1998 ed. [Hardback]

,
  • Formāts: Hardback, 229 pages, height x width: 235x155 mm, weight: 1170 g, XVIII, 229 p., 1 Hardback
  • Sērija : Frontiers in Electronic Testing 12
  • Izdošanas datums: 30-Jun-1998
  • Izdevniecība: Springer
  • ISBN-10: 079238184X
  • ISBN-13: 9780792381846
Citas grāmatas par šo tēmu:
  • Hardback
  • Cena: 162,93 €*
  • * ši ir gala cena, t.i., netiek piemērotas nekādas papildus atlaides
  • Standarta cena: 191,69 €
  • Ietaupiet 15%
  • Grāmatu piegādes laiks ir 3-4 nedēļas, ja grāmata ir uz vietas izdevniecības noliktavā. Ja izdevējam nepieciešams publicēt jaunu tirāžu, grāmatas piegāde var aizkavēties.
  • Daudzums:
  • Ielikt grozā
  • Piegādes laiks - 4-6 nedēļas
  • Pievienot vēlmju sarakstam
Formal Equivalence Checking and Design Debugging 1998 ed.Palielināt
  • Formāts: Hardback, 229 pages, height x width: 235x155 mm, weight: 1170 g, XVIII, 229 p., 1 Hardback
  • Sērija : Frontiers in Electronic Testing 12
  • Izdošanas datums: 30-Jun-1998
  • Izdevniecība: Springer
  • ISBN-10: 079238184X
  • ISBN-13: 9780792381846
Citas grāmatas par šo tēmu:
Permanent link: https://www.kriso.lv/db/9780792381846.html
Keywords:
Reviews the electronic design problems that require logic equivalence checking, describes the underlying technologies that are used to solve them, and presents in detail some novel approaches to verifying design revisions after re-timing or other intensive sequential transformations. Considers symbolic, incremental, and RTL-to-gate verification. Also surveys previous and recent literature on diagnosing and correcting design error, and analyzes the algorithms used in two logic debugging software programs, ErrorTracer and AutoFix, developed by Huang and Cheng. Double spaced. Annotation c. by Book News, Inc., Portland, Or.

Formal Equivalence Checking and Design Debugging covers two major topics in design verification: logic equivalence checking and design debugging. The first part of the book reviews the design problems that require logic equivalence checking and describes the underlying technologies that are used to solve them. Some novel approaches to the problems of verifying design revisions after intensive sequential transformations such as retiming are described in detail. The second part of the book gives a thorough survey of previous and recent literature on design error diagnosis and design error correction. This part also provides an in-depth analysis of the algorithms used in two logic debugging software programs, ErrorTracer and AutoFix, developed by the authors. From the Foreword: `With the adoption of the static sign-off approach to verifying circuit implementations the application-specific integrated circuit (ASIC) industry will experience the first radical methodological revolution since the adoption of logic synthesis. Equivalence checking is one of the two critical elements of this methodological revolution. This book is timely for either the designer seeking to better understand the mechanics of equivalence checking or for the CAD researcher who wishes to investigate well-motivated research problems such as equivalence checking of retimed designs or error diagnosis in sequential circuits.' Kurt Keutzer, University of California, Berkeley

Papildus informācija

Springer Book Archives
Foreword xi(6)
Preface xvii
Chapter 1 Introduction
1(16)
1.1 Problems of Interest
1(9)
1.1.1 Equivalence Checking
3(5)
1.1.2 Design Error Diagnosis and Correction
8(2)
1.2 Organization
10(7)
PART I EQUIVALENCE CHECKING 17(122)
Chapter 2 Symbolic Verification
17(22)
2.1 Symbolic Verification by FSM Traversal
17(2)
2.2 Implicit State Enumeration by BDD
19(11)
2.2.1 Set Representation
20(1)
2.2.2 Input/Output Relation
21(2)
2.2.3 Transition Relation
23(2)
2.2.4 Next-State Computation
25(1)
2.2.5 Complete Flow
26(2)
2.2.6 Error Trace Generation
28(2)
2.3 Speed-up Techniques
30(7)
2.3.1 An Efficient Method for Constructing Transition Relation
30(3)
2.3.2 Reduction on Image Computation
33(3)
2.3.3 Reduction on Reachable State Computation
36(1)
2.4 Summary
37(2)
Chapter 3 Incremental Verification for Combinational Circuits
39(22)
3.1 Substitution-Based Algorithms
39(11)
3.1.1 Brand's Algorithm Using ATPG
39(2)
Pairing up candidate pairs
41(1)
Pruning the miter incrementally
42(2)
Checking the equivalence of primary outputs
44(1)
3.1.2 Enhancement by Local BDD
44(2)
Constructing BDDs using a dynamic support
46(2)
Experimental results
48(2)
3.2 Learning-Based Algorithms
50(3)
3.2.1 Recursive Learning
50(1)
3.2.2 Verification Flow Using Recursive Learning
51(2)
3.3 Transformation-Based Algorithm
53(4)
3.3.1 Identifying Dissimilar Region
53(2)
3.3.2 Similarity Enhancing Transformation (SET)
55(2)
3.4 Summary
57(4)
Chapter 4 Incremental Verification for Sequential Circuits
61(30)
4.1 Definition of Equivalence
62(10)
4.1.1 Equivalence of Circuits With A Reset State
62(1)
4.1.2 Equivalence of Circuits Without A Reset State
62(1)
Sequential Hardware Equivalence
63(2)
Safe Replaceability
65(1)
Three-Valued Safe Replaceability
66(1)
Three-Valued Equivalence
67(1)
4.1.3 Comparison of Definitions
67(5)
4.2 Methodology
72(4)
4.2.1 Checking Three-Valued Safe Replaceability
73(1)
4.2.2 Checking Reset Equivalence
74(2)
4.2.3 Checking Three-Valued Equivalence
76(1)
4.3 The Speed-Up Techniques
76(8)
4.3.1 Test Generation with Breadth-First-Search
77(2)
4.3.2 Exploring the Structural Similarity
79(1)
4.3.3 Identifying Equivalent Flip-Flop Pairs
80(4)
4.4 Experimental Results
84(2)
4.5 Summary
86(1)
4.6 Appendix
87(4)
Chapter 5 AQUILA: A Local BDD-based Equivalence Verifier
91(20)
5.1 Overall Flow
91(2)
5.2 Two-Level Inductive Algorithm
93(4)
5.2.1 Second-Level Assume-And-Then-Verify
95(2)
5.3 Symbolic Backward Justification
97(8)
5.3.1 Partial Justification
100(2)
5.3.2 An Example
102(3)
5.4 Experimental Results
105(2)
5.5 Summary
107(4)
Chapter 6 Algorithm for Verifying Retimed Circuits
111(12)
6.1 Introduction
111(2)
6.2 Pre-Processing Algorithm
113(5)
6.2.1 Signature Computation
115(1)
6.2.2 Deriving Candidate Delayed-Equivalent Pairs
115(2)
6.2.3 Delay Compensation
117(1)
6.3 Experimental Results
118(3)
6.4 Summary
121(2)
Chapter 7 RTL-to-Gate Verification
123(16)
7.1 Introduction
123(2)
7.2 Don't Care Modeling
125(2)
7.3 Integration with FSM Traversal
127(5)
7.3.1 Computing a Subset of Unreachable States
128(2)
7.3.2 Incremental Verification with Don't Cares
130(2)
7.4 Overall Flow for RTL-to-Gate Verification
132(1)
7.5 Experimental Results
132(4)
7.6 Summary
136(3)
PART II LOGIC DEBUGGING 139(72)
Chapter 8 Introduction to Logic Debugging
139(20)
8.1 Introduction
139(2)
8.2 Symbolic Approach
141(5)
8.2.1 Search for Error Locations
142(1)
Single-fix function computation
143(1)
8.2.2 Correction by Re-synthesis
144(1)
8.2.3 Generalization
144(1)
Output Partitioning
145(1)
Multiple signal re-synthesis
145(1)
8.3 Simulation-Based Approach
146(8)
8.3.1 Cone Intersection
147(1)
8.3.2 Filter Based on Sensitization
148(2)
8.3.3 Back Propagation
150(3)
8.3.4 Enhancement with Observability Measure
153(1)
8.4 Structural Approach
154(2)
8.5 Summary
156(3)
Chapter 9 Error Tracer: Error Diagnosis by Fault Simulation
159(16)
9.1 Introduction
159(1)
9.2 Basic Terminology
160(1)
9.3 Single Error Diagnosis
161(4)
9.3.1 Correctability
161(1)
9.3.2 The Algorithm for Single Error Diagnosis
162(1)
9.3.3 Correctability Check via Fault Simulation
163(2)
9.4 Multiple Error Diagnosis
165(3)
9.4.1 k-Correctability
166(1)
9.4.2 A Two-Stage Algorithm for Diagnosing Multiple Errors
167(1)
9.5 Experimental Results
168(5)
9.6 Summary
173(2)
Chapter 10 Extension to Sequential Error Diagnosis
175(14)
10.1 Introduction
175(1)
10.2 Diagnosing Sequential Circuits
176(6)
10.2.1 Correctability
176(1)
10.2.2 The Necessary and Sufficient Condition
177(3)
10.2.3 Correctability Check via Fault Simulation
180(1)
10.2.4 Generalization for Multiple Errors
181(1)
10.3 Experimental Results
182(5)
10.3.1 Results of Diagnosing Single-error Circuits
183(2)
10.3.2 Results of Diagnosing Double-Error Circuits
185(1)
10.3.3 Challenges
186(1)
10.4 Summary
187(2)
Chapter 11 Incremental Logic Rectification
189(22)
11.1 Preliminaries
190(2)
11.1.1 Definitions
190(1)
11.1.2 Single Signal Correctable Circuit
190(2)
11.2 Incremental Logic Rectification
192(8)
11.2.1 Error Region Pruning
192(1)
11.2.2 Symbolic Partial Correction
193(4)
11.2.3 Single-Gate Correction Criterion
197(2)
11.2.4 The Algorithm
199(1)
11.3 A Divide and Conquer Heuristic
200(4)
11.3.1 Pure Structural Approach Based on Back-Substitution
201(3)
11.4 Experimental Results
204(5)
11.5 Summary
209(2)
Bibliography 211(12)
Index 223