Formal system verification : state-of the-art and future trends

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. Read more... Abstract: 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 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 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. Provides latest results on formal methods along the complete design flow; Covers different abstraction layers, from ESL to RTL; Addresses formal verification in both digital and analog contexts; Demonstrates techniques in current industrial use Front Matter....Pages i-xvi Formal Techniques for Verification and Coverage Analysis of Analog Systems....Pages 1-35 Verification of Incomplete Designs....Pages 37-72 Probabilistic Model Checking: Advances and Applications....Pages 73-121 Software in a Hardware View....Pages 123-154 Formal Verification—The Industrial Perspective....Pages 155-182