Muutke küpsiste eelistusi

System-Level Validation: High-Level Modeling and Directed Test Generation Techniques 2013 [Kõva köide]

  • Formaat: Hardback, 250 pages, kõrgus x laius: 235x155 mm, kaal: 5325 g, XXII, 250 p., 1 Hardback
  • Ilmumisaeg: 19-Sep-2012
  • Kirjastus: Springer-Verlag New York Inc.
  • ISBN-10: 1461413583
  • ISBN-13: 9781461413585
  • Kõva köide
  • Hind: 95,02 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Tavahind: 111,79 €
  • Säästad 15%
  • Raamatu kohalejõudmiseks kirjastusest kulub orienteeruvalt 2-4 nädalat
  • Kogus:
  • Lisa ostukorvi
  • Tasuta tarne
  • Tellimisaeg 2-4 nädalat
  • Lisa soovinimekirja
  • Formaat: Hardback, 250 pages, kõrgus x laius: 235x155 mm, kaal: 5325 g, XXII, 250 p., 1 Hardback
  • Ilmumisaeg: 19-Sep-2012
  • Kirjastus: Springer-Verlag New York Inc.
  • ISBN-10: 1461413583
  • ISBN-13: 9781461413585
This book covers state-of-the art techniques for high-level modeling and validation of complex hardware/software systems, including those with multicore architectures. It helps reader avoid time-consuming and error-prone validation methodologies.

This book covers state-of-the art techniques for high-level modeling and validation of complex hardware/software systems, including those with multicore architectures. Readers will learn to avoid time-consuming and error-prone validation from the comprehensive coverage of system-level validation, including high-level modeling of designs and faults, automated generation of directed tests, and efficient validation methodology using directed tests and assertions. The methodologies described in this book will help designers to improve the quality of their validation, performing as much validation as possible in the early stages of the design, while reducing the overall validation effort and cost.
1 Introduction
1(18)
1.1 Growing SoC Validation Complexity
1(2)
1.2 System-Level Validation: Opportunities and Challenges
3(11)
1.2.1 Top-Down Design and Validation Flow
4(2)
1.2.2 SoC Validation Approaches
6(4)
1.2.3 Opportunities in System-Level Validation
10(2)
1.2.4 System-Level Validation Challenges
12(2)
1.3 A Comprehensive Approach for System-Level Validation
14(1)
1.4 Book Organization
14(5)
References
15(4)
2 Modeling and Specification of SoC Designs
19(24)
2.1 Introduction
19(1)
2.2 Modeling of Complex Systems
19(3)
2.2.1 Graph-Based Modeling
20(1)
2.2.2 FSM-Based Behavior Modeling
20(2)
2.3 Specification Using SystemC TLMs
22(7)
2.3.1 Modeling of SystemC TLM Designs
22(2)
2.3.2 Transformation from SystemC TLM to SMV
24(4)
2.3.3 Case Study: A Router Example
28(1)
2.4 Specification Using UML Activity Diagrams
29(11)
2.4.1 Graphic Notations
30(2)
2.4.2 Formal Modeling of UML Activity Diagrams
32(4)
2.4.3 Transformation from UML Activity Diagrams to SMV
36(4)
2.4.4 Case Study: A Stock Exchange System
40(1)
2.5
Chapter Summary
40(3)
References
40(3)
3 Automated Generation of Directed Tests
43(18)
3.1 Introduction
43(1)
3.2 Related Work
44(1)
3.3 The Workflow of Model Checking Based Test Generation
45(1)
3.4 Coverage-Driven Property Generation
46(5)
3.4.1 Safety Property and Its Negation
46(2)
3.4.2 Testing Adequacy Using Model Checking
48(1)
3.4.3 Fault Models
48(3)
3.4.4 Functional Coverage Based on Fault Models
51(1)
3.5 Test Generation Using Model Checking Techniques
51(3)
3.5.1 Test Generation Using Unbounded Model Checking
51(1)
3.5.2 Test Generation Using Bounded Model Checking
52(2)
3.6 Case Studies
54(3)
3.6.1 A Control System
55(1)
3.6.2 A Stock Exchange System
56(1)
3.7
Chapter Summary
57(4)
References
58(3)
4 Functional Test Compaction
61(18)
4.1 Introduction
61(1)
4.2 Manufacturing Test Reduction Techniques
61(6)
4.2.1 Test Compression
63(1)
4.2.2 Test Compaction
63(2)
4.2.3 Applicability and Limitations
65(2)
4.3 Functional Test Compaction
67(9)
4.3.1 Binary Format of FSM Models
68(2)
4.3.2 Number of FSM States and Transitions
70(1)
4.3.3 Property Compaction of FSM States and Transitions
71(2)
4.3.4 FSM Coverage-Driven Test Selection and Generation
73(1)
4.3.5 A Case Study
74(2)
4.4
Chapter Summary
76(3)
References
76(3)
5 Property Clustering and Learning Techniques
79(28)
5.1 Introduction
79(1)
5.2 Related Work
80(1)
5.3 Background: SAT Solver Implementation
81(3)
5.3.1 DPLL Algorithm
81(1)
5.3.2 Conflict Clause
82(2)
5.4 Property Clustering
84(5)
5.4.1 Similarity Based on Structural Overlap
85(1)
5.4.2 Similarity Based on Textual Overlap
86(1)
5.4.3 Similarity Based on Influence
87(1)
5.4.4 Similarity Based on CNF Intersection
88(1)
5.4.5 Determination of Base Property
88(1)
5.5 Conflict Clause Based Test Generation
89(4)
5.5.1 Conflict Clause Forwarding Techniques
89(2)
5.5.2 Name Substitution for Computation of Intersections
91(1)
5.5.3 Identification and Reuse of Common Conflict Clauses
92(1)
5.6 Case Studies
93(11)
5.6.1 A MIPS Processor
94(8)
5.6.2 A Stock Exchange System
102(2)
5.7
Chapter Summary
104(3)
References
105(2)
6 Decision Ordering Based Learning Techniques
107(22)
6.1 Introduction
107(1)
6.2 Related Work
108(1)
6.3 Decision Ordering Based Learnings
108(5)
6.3.1 Motivation
109(1)
6.3.2 Bit Value Ordering
110(1)
6.3.3 Variable Ordering
111(1)
6.3.4 Hybrid Learning from Conflict Clauses and Decision Ordering
112(1)
6.4 Test Generation Using Decision Ordering Techniques
113(6)
6.4.1 Test Generation for a Single Property
114(2)
6.4.2 Test Generation for Similar Properties
116(3)
6.5 Case Studies
119(8)
6.5.1 Intra-Property Learning
119(4)
6.5.2 Inter-Property Learning
123(4)
6.6
Chapter Summary
127(2)
References
127(2)
7 Synchronized Generation of Directed Tests
129(16)
7.1 Introduction
129(1)
7.2 Related Work
130(1)
7.3 Synchronized Test Generation
130(7)
7.3.1 Correctness of STG
135(1)
7.3.2 Implementation Details
136(1)
7.4 Case Studies
137(5)
7.4.1 A Stock Exchange System
137(3)
7.4.2 A MIPS Processor
140(2)
7.5
Chapter Summary
142(3)
References
142(3)
8 Test Generation Using Design and Property Decompositions
145(24)
8.1 Introduction
145(2)
8.2 Related Work
147(1)
8.3 Decomposition of Design and Property
148(7)
8.3.1 Design Decomposition
149(1)
8.3.2 Property Decomposition
150(5)
8.4 Decompositional Test Generation
155(6)
8.4.1 Test Generation Using Module-Level Partitioning
158(2)
8.4.2 Test Generation Using Path-Level Partitioning
160(1)
8.5 Merging Partial Counterexamples
161(1)
8.6 A Case Study
162(4)
8.6.1 Module-Level Decomposition
163(1)
8.6.2 Group-Level Decomposition Based on Time Step
164(2)
8.6.3 Discussion: Applicability and Limitations
166(1)
8.7
Chapter Summary
166(3)
References
166(3)
9 Learning-Oriented Property Decomposition Approaches
169(16)
9.1 Introduction
169(1)
9.2 Related Work
170(1)
9.3 Learning-Oriented Property Decomposition
171(5)
9.3.1 Spatial Property Decomposition
171(3)
9.3.2 Temporal Property Decomposition
174(2)
9.4 Decision Ordering Based Learning Techniques
176(2)
9.5 Test Generation Using Decomposition and Learning Techniques
178(1)
9.6 An Illustrative Example
179(2)
9.6.1 Spatial Decomposition
179(1)
9.6.2 Temporal Decomposition
180(1)
9.7 Case Studies
181(2)
9.7.1 A MIPS Processor
181(1)
9.7.2 A Stock Exchange System
182(1)
9.8
Chapter Summary
183(2)
References
184(1)
10 Directed Test Generation for Multicore Architectures
185(16)
10.1 Introduction
185(1)
10.2 Related Work
186(1)
10.3 Test Generation for Multicore Architectures
187(8)
10.3.1 Correctness of TGMA
191(2)
10.3.2 Implementation Details
193(1)
10.3.3 Heterogeneous Multicore Architectures
194(1)
10.4 Case Studies
195(4)
10.4.1 Experimental Setup
195(1)
10.4.2 Results
196(3)
10.5
Chapter Summary
199(2)
References
199(2)
11 Test Generation for Cache Coherence Validation
201(14)
11.1 Introduction
201(1)
11.2 Related Work
202(1)
11.3 Background and Motivation
203(1)
11.4 Test Generation for Transition Coverage
204(6)
11.4.1 SI Protocol
205(1)
11.4.2 MSI Protocol
206(2)
11.4.3 MESI Protocol
208(1)
11.4.4 MOSI Protocol
209(1)
11.5 Case Studies
210(3)
11.6
Chapter Summary
213(2)
References
213(2)
12 Reuse of System-Level Validation Efforts
215(20)
12.1 Introduction
215(1)
12.2 Related Work
216(1)
12.3 RTL Test Generation from TLM Specifications
217(7)
12.3.1 Automatic TLM Test Generation
217(2)
12.3.2 Translation from TLM Tests to RTL Tests
219(3)
12.3.3 A Prototype Tool for TLM-to-RTL Validation Refinement
222(2)
12.4 Case Studies
224(9)
12.4.1 A Router Example
224(4)
12.4.2 A Pipelined Processor Example
228(5)
12.5
Chapter Summary
233(2)
References
233(2)
13 Conclusions
235(4)
13.1 Summary
235(2)
13.2 Future Directions
237(2)
Appendix A Acknowledgments of Copyrighted Materials 239(4)
Index 243