|
|
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) |
|
|
14 | (5) |
|
|
15 | (4) |
|
2 Modeling and Specification of SoC Designs |
|
|
19 | (24) |
|
|
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) |
|
|
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) |
|
|
40 | (3) |
|
|
40 | (3) |
|
3 Automated Generation of Directed Tests |
|
|
43 | (18) |
|
|
43 | (1) |
|
|
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) |
|
|
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) |
|
|
54 | (3) |
|
|
55 | (1) |
|
3.6.2 A Stock Exchange System |
|
|
56 | (1) |
|
|
57 | (4) |
|
|
58 | (3) |
|
4 Functional Test Compaction |
|
|
61 | (18) |
|
|
61 | (1) |
|
4.2 Manufacturing Test Reduction Techniques |
|
|
61 | (6) |
|
|
63 | (1) |
|
|
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) |
|
|
74 | (2) |
|
|
76 | (3) |
|
|
76 | (3) |
|
5 Property Clustering and Learning Techniques |
|
|
79 | (28) |
|
|
79 | (1) |
|
|
80 | (1) |
|
5.3 Background: SAT Solver Implementation |
|
|
81 | (3) |
|
|
81 | (1) |
|
|
82 | (2) |
|
|
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) |
|
|
93 | (11) |
|
|
94 | (8) |
|
5.6.2 A Stock Exchange System |
|
|
102 | (2) |
|
|
104 | (3) |
|
|
105 | (2) |
|
6 Decision Ordering Based Learning Techniques |
|
|
107 | (22) |
|
|
107 | (1) |
|
|
108 | (1) |
|
6.3 Decision Ordering Based Learnings |
|
|
108 | (5) |
|
|
109 | (1) |
|
|
110 | (1) |
|
|
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) |
|
|
119 | (8) |
|
6.5.1 Intra-Property Learning |
|
|
119 | (4) |
|
6.5.2 Inter-Property Learning |
|
|
123 | (4) |
|
|
127 | (2) |
|
|
127 | (2) |
|
7 Synchronized Generation of Directed Tests |
|
|
129 | (16) |
|
|
129 | (1) |
|
|
130 | (1) |
|
7.3 Synchronized Test Generation |
|
|
130 | (7) |
|
|
135 | (1) |
|
7.3.2 Implementation Details |
|
|
136 | (1) |
|
|
137 | (5) |
|
7.4.1 A Stock Exchange System |
|
|
137 | (3) |
|
|
140 | (2) |
|
|
142 | (3) |
|
|
142 | (3) |
|
8 Test Generation Using Design and Property Decompositions |
|
|
145 | (24) |
|
|
145 | (2) |
|
|
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) |
|
|
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) |
|
|
166 | (3) |
|
|
166 | (3) |
|
9 Learning-Oriented Property Decomposition Approaches |
|
|
169 | (16) |
|
|
169 | (1) |
|
|
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) |
|
|
181 | (2) |
|
|
181 | (1) |
|
9.7.2 A Stock Exchange System |
|
|
182 | (1) |
|
|
183 | (2) |
|
|
184 | (1) |
|
10 Directed Test Generation for Multicore Architectures |
|
|
185 | (16) |
|
|
185 | (1) |
|
|
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) |
|
|
195 | (4) |
|
10.4.1 Experimental Setup |
|
|
195 | (1) |
|
|
196 | (3) |
|
|
199 | (2) |
|
|
199 | (2) |
|
11 Test Generation for Cache Coherence Validation |
|
|
201 | (14) |
|
|
201 | (1) |
|
|
202 | (1) |
|
11.3 Background and Motivation |
|
|
203 | (1) |
|
11.4 Test Generation for Transition Coverage |
|
|
204 | (6) |
|
|
205 | (1) |
|
|
206 | (2) |
|
|
208 | (1) |
|
|
209 | (1) |
|
|
210 | (3) |
|
|
213 | (2) |
|
|
213 | (2) |
|
12 Reuse of System-Level Validation Efforts |
|
|
215 | (20) |
|
|
215 | (1) |
|
|
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) |
|
|
224 | (9) |
|
|
224 | (4) |
|
12.4.2 A Pipelined Processor Example |
|
|
228 | (5) |
|
|
233 | (2) |
|
|
233 | (2) |
|
|
235 | (4) |
|
|
235 | (2) |
|
|
237 | (2) |
Appendix A Acknowledgments of Copyrighted Materials |
|
239 | (4) |
Index |
|
243 | |