Formal System Verification (eBook)

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.

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