E-raamat: Verification Techniques for System-Level Design

Acknowledgments		ix
Introduction		1	(4)
Higher-Level Design Methodology and Associated Verification Problems		5	(28)
Introduction		5	(1)
Issues in High-Level Design		6	(6)
C/C++-Based Design and Specification Languages		12	(12)
SpecC Language		14	(4)
The Semantics of par Statements		18	(3)
Relationship with Simulation Time		21	(3)
System-Level Design Methodology Based on C/C++-Based Design and Specification Languages		24	(4)
Verification Problems in High-Level Designs		28	(5)
Basic Technology for Formal Verification		33	(24)
The Boolean Satisfiability Problem		33	(1)
The DPLL Algorithm		34	(1)
Enhancements to Modern SAT Solvers		35	(3)
Capabilities of Modern SAT Solvers		38	(1)
Binary Decision Diagrams		38	(6)
Manipulation of BDDs		42	(1)
Variants of BDDs		43	(1)
Automatic Test Pattern Generation Engines		44	(5)
Single Stuck-at Testing for Combinational Circuits		45	(3)
Stuck-at Testing in Sequential Circuits		48	(1)
SAT, BDD, and ATPG Engines for Validation		49	(1)
Theorem-Proving and Decision Procedures		49	(8)
References		54	(3)
Verification Algorithms for FSM Models		57	(44)
Combinational Equivalence Checking		57	(9)
Sequential Equivalence Checking as Combinational Equivalence Checking		57	(1)
Latch Mapping Problem		58	(3)
EC Based on Internal Equivalences		61	(3)
Anatomy and Capabilities of Modern CEC Tools		64	(2)
Model Checking		66	(17)
Modeling Concurrent Systems		66	(1)
Temporal Logics		66	(4)
Types of Properties		70	(1)
Basic Model-Checking Algorithms		70	(4)
Symbolic Model Checking		74	(9)
Semi-Formal Verification Techniques		83	(10)
SAT-Based Bounded Model Checking		83	(5)
Symbolic Simulation		88	(3)
Enhancing Simulation Using Formal Methods		91	(2)
Conclusion		93	(8)
References		93	(8)
Static Checking of Higher-Level Design Descriptions		101	(36)
Program Slicing		102	(4)
System Dependence Graph		104	(1)
Nodes and Edges		104	(1)
Concurrency		104	(1)
Synchronization on Concurrent Processes		104	(2)
Checking Method and Its Implying Design Flow		106	(23)
Basic Static Description Checking		108	(7)
Improvement of Accuracy Using Conditions of Control Nodes		115	(14)
Application of the Checking Methods to HW/SW Partitioning and Optimization		129	(3)
Case Study		132	(5)
MPEG2		132	(1)
JPEG2000		132	(1)
Experimental Results on Static Checking		133	(1)
References		134	(3)
Equivalence Checking on Higher-Level Design Descriptions		137	(26)
Introduction		137	(1)
High-Level Design Flow from the Viewpoint of Equivalence Checking		138	(3)
Symbolic Simulation for Equivalence Checking		141	(3)
Equivalence-Checking Methods Based on the Identification of Differences between two Descriptions		144	(11)
Identification of Differences between Two Descriptions		147	(1)
Symbolic Simulation Based on Textual Differences		148	(2)
Example		150	(1)
Experimental Results		151	(4)
Further Improvement on the Use of Differences between Two Descriptions		155	(8)
Extension of the Verification Area		158	(1)
Symbolic Simulation on SDGs		159	(1)
Verification Example		159	(1)
Discussion of the Strategy of Extension		160	(1)
Experimental Results on the Extension-Based Method		160	(2)
References		162	(1)
Model Checking on Higher-Level Design Descriptions		163	(24)
Introduction		163	(1)
Goal of Synchronization Verification in High-Level Designs		164	(3)
Model Checking and High-Level Design Descriptions		167	(1)
Brief Review of SpecC and Its Semantics for Synchronization Verification		168	(5)
Synchronization Verification Framework		173	(8)
From SpecC to Boolean SpecC		175	(1)
From Boolean SpecC to Mathematical Representations of Equalities/Inequalities		176	(1)
Verification Method		177	(2)
Validating the Abstract Counterexample		179	(1)
Checking for Race Conditions		179	(1)
Renaming Variables		180	(1)
Predicate Discovery and Boolean SpecC Refinement		180	(1)
Experimental Results		181	(6)
References		185	(2)
Simulation-Based Verification Techniques for System-Level Designs		187	(44)
Introduction		187	(1)
Simulation Types		188	(5)
Event-Driven Simulation		189	(1)
Cycle-Based Simulation		190	(1)
Specification/Behavior-Level Simulation		191	(1)
Mixed-Mode Simulation		191	(2)
High-Level Simulation Tools		193	(3)
Static Checking (Linting)		193	(1)
Simulators, Waveform Viewers, and Debuggers		194	(2)
Simulation Drawbacks		196	(1)
Coverage Metrics		196	(8)
Drawbacks of Coverage Metrics		202	(2)
Test-Bench Automation		204	(9)
Transaction Level Modeling		204	(2)
Property Specification Languages		206	(2)
Test-Bench Automation Frameworks		208	(1)
Model-Driven Automatic Test-Bench Generation		209	(3)
Automatic Test-Bench Generation from Implementation Design		212	(1)
Tackling Performance Issues		213	(6)
Emulation and Hardware Acceleration		214	(3)
Using Preverified IPs/Cores and Higher Abstraction Levels		217	(1)
Correct by Construction Design		218	(1)
Stopping Criteria		219	(1)
An Example Case Study		220	(8)
Conclusion		228	(1)
Future Directions		228	(3)
References		229	(2)
Conclusion		231	(4)
Index		235

*Spent 15 years at Fujitsu research laboratories.*Research on synthesis and verification of digital systems for more than 25 years*Full professor at VLSI Design and Education Center in the University of Tokyo Indradeep Ghosh received the Bachelor of Technology degree in Computer Science and Engineering from the Indian Institute of Technology, Kharagpur, India, in 1993, and the M.A. and Ph.D. degrees in Electrical Engineering from Princeton University, Princeton, New Jersey, in 1995 and 1998, respectively.Since 1998 he has been a member of research staff in at Fujitsu Laboratories of America, Sunnyvale, California. He has authored or co-authored more that 40 technical articles in international journals and conferences and holds 6 US patents. He has given numerous presentations in international conferences and workshops. In Fujitsu he has been involved in design verification and testing of industrial systems that are currently in production. His research interests include testing, verification, and validation of hardware and software systems. He is senior member of the IEEE and a member of the ACM. Mukul Prasad:Mukul Prasad received the Bachelor of Technology degree in Electrical Engineering from the Indian Institute of Technology, Delhi, India, in 1995, and the Ph.D. degree in Electrical Engineering & Computer Sciences from the University of California at Berkeley in 2001. Since 2001 he has been a member of the research staff in the Trusted Systems Innovation group at Fujitsu Laboratories of America in Sunnyvale, California. His doctoral thesis and his subsequent research has involved the development and application of verification technologies such as Satisfiability solvers. His work has received a Best Paper Award at the Design Automation & Test in Europe Conference (DATE 2002). His current research addresses various problems in system-level design validation. He has co-authored more than 20 technical papers and presented three tutorials at international conferences and jointly holds 3 U.S. patents in the area of formal validation.