High-Level Verification: Methods and Tools for Verification of System-Level Designs

✍ Scribed by Lerner, Sorin;Gupta, Rajesh K

• Publisher: Springer
• Year: 2011
• Tongue: English
• Leaves: 176
• Category: Library

✦ Synopsis

Given the growing size and heterogeneity of Systems on Chip (SOC), the design process from initial specification to chip fabrication has become increasingly complex. This growing complexity provides incentive for designers to use high-level languages such as C, SystemC, and SystemVerilog for system-level design. While a major goal of these high-level languages is to enable verification at a higher level of abstraction, allowing early exploration of system-level designs, the focus so far for validation purposes has been on traditional testing techniques such as random testing and scenario-based testing. This book focuses on high-level verification, presenting a design methodology that relies upon advances in synthesis techniques as well as on incremental refinement of the design process. These refinements can be done manually or through elaboration tools. This book discusses verification of specific properties in designs written using high-level languages, as well as checking that the refined implementations are equivalent to their high-level specifications. The novelty of each of these techniques is that they use a combination of formal techniques to do scalable verification of system designs completely automatically. The verification techniques presented in this book include methods for verifying properties of high-level designs and methods for verifying that the translation from high-level design to a low-level Register Transfer Language (RTL) design preserves semantics. Used together, these techniques guarantee that properties verified in the high-level design are preserved through the translation to low-level RTL.

✦ Table of Contents

8.3 Illustrative Example......Page 3
8.3.4 Executing Optimizations......Page 5
7.3.4 Inference Algorithm......Page 7
8.3.9 Solving Constraints......Page 9
Index......Page 13
Cover......Page 1
9.4 Future Work......Page 2
High-Level Verification......Page 4
Preface......Page 6
Acknowledgments......Page 8
Contents......Page 10
8.4.2 Architectural Overview......Page 11
Acronyms......Page 14
8.7 Permute Module......Page 15
Chapter 1 Introduction......Page 16
1.1 Overview of High-Level Verification......Page 17
8.8 Experiments and Results......Page 18
1.2.2 Translation Validation......Page 20
1.4 Book Organization......Page 23
7.9 Further Reading......Page 24
2.1 High-Level Design......Page 25
2.3 High-Level Synthesis......Page 26
6.12 Summary......Page 27
8.5 GenerateConstraints Module......Page 12
1.2.1 High-Level Property Checking......Page 19
1.3 Contributions of the Book......Page 22
1.2.3 Synthesis Tool Verification......Page 21
2.4 Model Checking......Page 29
2.4.1 Simple Elevator Example......Page 30
2.4.2 Property Specification......Page 32
2.4.3 Reachability Algorithm......Page 33
2.5.1 Representation of Concurrent Programs......Page 34
2.5.2 Partial-Order Reduction......Page 35
2.6 Summary......Page 37
3.1.1 Explicit Model Checking......Page 38
3.1.2 Symbolic Model Checking......Page 40
3.2.1 Relational Approach......Page 42
3.2.2 Model Checking......Page 43
3.2.3 Theorem Proving......Page 44
3.3.1 Formal Assertions......Page 45
3.3.2 Transformational Synthesis Tools......Page 46
3.4 Summary......Page 48
Chapter 4 Verification Using Automated Theorem Provers......Page 49
4.1 Satisfiability Modulo Theories......Page 50
4.2 Hoare Logic......Page 51
4.3 Weakest Preconditions......Page 52
4.4.1 Path-Based Weakest Precondition......Page 56
4.4.2 Pointers......Page 58
4.4.3 Loops......Page 61
5.1 Verification of Concurrent Programs......Page 63
5.3 Problem Statement......Page 64
5.5 SystemC Example......Page 65
5.6.1 Nondeterminism......Page 67
5.7 State Transition System......Page 68
5.8 The EMC-SC Approach......Page 70
5.8.1 Static Analysis......Page 71
5.8.2 The Explore Algorithm......Page 72
5.9 The Satya Tool......Page 75
5.10.1 FIFO Benchmark......Page 76
5.10.2 TAC Benchmark......Page 77
5.12 Summary......Page 78
6.1 Introduction......Page 79
6.1.1 Synchronous Models......Page 81
6.1.2 Asynchronous Models......Page 82
6.1.3 Outline......Page 83
6.2.1 Interleaving (Operational) Semantics......Page 84
6.2.2 Axiomatic (Non-Operational) Semantics......Page 86
6.3 Bounded Model Checking......Page 87
6.4 Concurrent System: Model......Page 88
6.5 Synchronous Modeling......Page 89
6.6 BMC on Synchronous Models......Page 91
6.6.1 BMC Formula Sizes......Page 93
6.8.1 Thread Program Constraints: TP......Page 95
6.8.3 BMC Formula Sizes......Page 96
6.9.1 MAT-Based Partial Order Reduction......Page 98
6.9.2 Independent Modeling......Page 101
6.9.3 Concurrency Constraints......Page 102
6.9.4 BMC Formula Sizes......Page 103
6.10 Comparison Summary......Page 104
6.11 Further Reading......Page 105
7.1 Overview of Translation Validation......Page 108
7.2 Overview of the TV-HLS Approach......Page 109
7.3 Illustrative Example......Page 110
7.3.2 Simulation Relation......Page 112
7.3.4 Inference Algorithm......Page 114
7.4 Definition of Refinement......Page 117
7.5 Simulation Relation......Page 119
7.6.1 Checking Algorithm......Page 120
7.6.2 Inference Algorithm......Page 123
7.7 Equivalence of Transition Diagrams......Page 126
7.8.1 Automatic Refinement Checking of CSP Programs......Page 127
7.8.2 SPARK: High-Level Synthesis Framework......Page 129
7.9 Further Reading......Page 131
7.10 Summary......Page 132
8.1 Overview of Synthesis Tool Verification......Page 133
8.1.1 Once-And-For-All Vs. Translation Validation......Page 134
8.3 Illustrative Example......Page 135
8.3.1 Expressing Loop Pipelining......Page 136
8.3.3 Side Conditions......Page 137
8.3.5 Proving Correctness of Loop Pipelining......Page 138
8.3.8 Generating Constraints......Page 140
8.3.9 Solving Constraints......Page 141
8.4 Parameterized Equivalence Checking......Page 142
8.4.2 Architectural Overview......Page 143
8.5 GenerateConstraints Module......Page 144
8.7 Permute Module......Page 147
8.8 Experiments and Results......Page 150
8.9 Execution Engine......Page 152
8.10 Further Reading......Page 153
8.11 Summary......Page 154
9.1 High-Level Property Checking......Page 156
9.4 Future Work......Page 157
References......Page 160
Index......Page 172