Drechsler Formal System Verification

State-of the-Art and Future Trends
1. Auflage 2018
ISBN: 978-3-319-57685-5
Verlag: Springer Nature Switzerland
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 193 Seiten

This book provides readers with a comprehensive introduction to the formal verification of hardware and software. World-leading experts from the domain of formal proof techniques show the latest developments starting from electronic system level (ESL) descriptions down to the register transfer level (RTL). The authors demonstrate at different abstraction layers how formal methods can help to ensure functional correctness. Coverage includes the latest academic research results, as well as descriptions of industrial tools and case studies.

Rolf Drechsler is head of Cyber-Physical Systems department at the German Research Center for Artificial Intelligence (DFKI) since 2011. Furthermore, he is a Full Professor at the Institute of Computer Science, University of Bremen, since 2001. Before, he worked for the Corporate Technology Department of Siemens AG, and was with the Institute of Computer Science, Albert-Ludwig University of Freiburg/Breisgau, Germany. Rolf Drechsler received the Diploma and Dr. Phil. Nat. degrees in computer science from the Goethe-University in Frankfurt/Main, Germany, in 1992 and, respectively, 1995. Rolf Drechsler focusses in his research at DFKI and in the Group for Computer Architecture, which he is heading at the Institute of Computer Science of the University of Bremen, on the development and design of data structures and algorithms with an emphasis on circuit and system design. Rolf Drechsler has been and still is a member of the Program Committees of numerous conferences (including e.g. DAC, ICCAD, DATE, ASP-DAC, FDL, MEMOCODE, FMCAD) and is co-founder of the Graduate School of Embedded Systems which started in 2006. Since 2012, he additionally coordinates the Graduate School System Design. He has received Best Paper Awards from numerous international scientific conferences, e.g.: Haifa Verification Conference (HVC) 2006, Forum on Specification & Design Languages (FDL) 2007 and 2010, IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS) 2010, IEEE/ACM International Conference on Computer-Aided Design (ICCAD) 2013.

Autoren/Hrsg.

Drechsler, Rolf

Inhaltsverzeichnis

1;Preface;6
2;Acknowledgements;8
3;Contents;9
4;Editors and Contributors;12
5;1 Formal Techniques for Verification and Coverage Analysis of Analog Systems;14
5.1;1.1 Introduction;14
5.2;1.2 State of the Art;15
5.3;1.3 State-Space Description;17
5.3.1;1.3.1 Solving a DAE System;18
5.3.2;1.3.2 Analog Transition System;19
5.4;1.4 Verification Methodology;22
5.4.1;1.4.1 Model Checking;23
5.4.2;1.4.2 Analog Specification Language (ASL);23
5.4.3;1.4.3 ASL-Example: Verification of Oscillation and Oscillator Voltage Sensitivity;24
5.4.4;1.4.4 Model Checking of an SRAM Cell;26
5.5;1.5 State Space Coverage;28
5.5.1;1.5.1 State-Space Coverage Calculation;28
5.5.2;1.5.2 Coverage Maximization Algorithm;30
5.5.3;1.5.3 Path Planning;31
5.6;1.6 ? State-Space Coverage;32
5.7;1.7 Coverage Analysis and Optimization Results;35
5.7.1;1.7.1 Detailed Case Study of a Level-Shifter Circuit;38
5.8;1.8 System-Level Verification;40
5.8.1;1.8.1 System Refinement and Verification;43
5.9;1.9 Conclusion;45
5.10;References;46
6;2 Verification of Incomplete Designs;49
6.1;2.1 Introduction;49
6.2;2.2 Preliminaries;52
6.3;2.3 Incomplete Combinational Circuits;54
6.3.1;2.3.1 The Partial Equivalence Checking Problem (PEC);55
6.3.2;2.3.2 SAT-based Approximations;56
6.3.3;2.3.3 QBF-based Methods;58
6.3.4;2.3.4 DQBF-based Methods;59
6.4;2.4 Incomplete Sequential Circuits;60
6.4.1;2.4.1 BMC for Incomplete Designs;62
6.4.2;2.4.2 Model Checking for Incomplete Designs;68
6.5;2.5 Conclusion;81
6.6;References;82
7;3 Probabilistic Model Checking: Advances and Applications;85
7.1;3.1 Introduction;85
7.2;3.2 Probabilistic Model Checking;86
7.2.1;3.2.1 Discrete-Time Markov Chains;87
7.2.2;3.2.2 Markov Decision Processes;94
7.2.3;3.2.3 Stochastic Multi-player Games;97
7.2.4;3.2.4 Tool Support;99
7.3;3.3 Controller Synthesis;100
7.3.1;3.3.1 Controller Synthesis for MDPs;100
7.3.2;3.3.2 Multi-objective Controller Synthesis;103
7.4;3.4 Modelling and Verification of Large Probabilistic Systems;105
7.4.1;3.4.1 Compositional Modelling of Probabilistic Systems;106
7.4.2;3.4.2 Compositional Probabilistic Model Checking;107
7.4.3;3.4.3 Quantitative Abstraction Refinement;109
7.4.4;3.4.4 Case Study: The Zeroconf Protocol;111
7.5;3.5 Real-Time Probabilistic Model Checking;112
7.5.1;3.5.1 Probabilistic Timed Automata;112
7.5.2;3.5.2 Continuous-Time Markov Chains;119
7.6;3.6 Parametric Probabilistic Model Checking;121
7.6.1;3.6.1 Parametric Model Checking for DTMCs;121
7.6.2;3.6.2 Parametric Model Checking for Other Probabilistic Models;124
7.7;3.7 Future Challenges and Directions;124
7.8;References;127
8;4 Software in a Hardware View;134
8.1;4.1 Introduction;134
8.2;4.2 Program Netlists;136
8.2.1;4.2.1 Basic Idea;138
8.2.2;4.2.2 Model Generation;139
8.2.3;4.2.3 Modeling Memory and I/O;140
8.3;4.3 Verification Scenarios for HW-dependent Software;142
8.4;4.4 Equivalence Checking of HW-dependent Software;144
8.4.1;4.4.1 Sequence-Based Model of the HW/SW Interface;145
8.4.2;4.4.2 Software Miter;149
8.4.3;4.4.3 Equivalence Checking Using SAT;150
8.4.4;4.4.4 Experimental Results;151
8.5;4.5 Cycle-Accurate HW/SW Co-verification of Firmware-Based Designs;155
8.5.1;4.5.1 Joint Hardware/Firmware Model;155
8.5.2;4.5.2 Timed Interface Model;156
8.5.3;4.5.3 Experimental Results;161
8.6;4.6 Conclusion;163
8.7;References;164
9;5 Formal Verification---The Industrial Perspective;166
9.1;5.1 Introduction;166
9.2;5.2 Automating Design Verification with Formal;167
9.2.1;5.2.1 Design Inspection;167
9.2.2;5.2.2 IP Integration Verification;172
9.2.3;5.2.3 Verification of Design Transformations;179
9.3;5.3 Assertion-Based Verification of IP Blocks;182
9.3.1;5.3.1 Assertions in the Verification Flow;182
9.3.2;5.3.2 Verification Planning;185
9.3.3;5.3.3 Quantitative Analysis and Coverage;186
9.4;5.4 Challenges Ahead;188
9.4.1;5.4.1 High-Level Design;189
9.4.2;5.4.2 High Reliability and Safety Critical Systems;189
9.4.3;5.4.3 Hardware Security;191
9.4.4;5.4.4 Low-Power Devices;192
9.5;References;193