A roadmap for formal property verification / by Pallab Dasgupta.

Format:

Book

Author/Creator:

Dasgupta, Pallab.

Language:

English

Subjects (All):

Integrated circuits--Verification.

Integrated circuits.

Physical Description:

xiii, 251 pages : illustrations ; 25 cm

Place of Publication:

Dordrecht : Springer, [2006]

Summary:

Integrating formal property verification (FPV) into an existing design process raises several interesting questions. Have I written enough properties? Have I written a consistent set of properties? What should I do when the FPV tool runs into capacity issues? This book develops the answers to these questions and fits them into a roadmap for formal property verification - a roadmap that shows how to glue FPV technology into the traditional validation flow. A Roadmap for Formal Property Verification explores the key issues in this powerful technology through simple examples - you do not need any background on formal methods to read most parts of this book.

Contents:

1.1 Writing Our First Formal Specification 2

1.2 Is My Specification Correct? 5

1.3 Have I written Enough Properties? 6

1.4 Property Verification 8

1.4.1 The Dynamic ABV Approach 9

1.4.2 The FPV Approach 11

1.5 Verification by Specification Refinement 14

1.6 The New Flow 17

2 Languages for Temporal Properties 19

2.1 The Basic Temporal Operators 22

2.1.1 Intuitive Explanation 23

2.1.2 Formal Semantics 24

2.2 Logics for Temporal Specification 25

2.2.1 Linear Temporal Logic 26

2.2.2 Computation Tree Logic 27

2.2.3 LTL versus CTL 29

2.2.4 Real Time Temporal Logics 30

2.3 System Verilog Assertions 31

2.3.1 A Quick Overview 32

2.3.2 The Notion of Sequences 37

2.3.3 Sequence Operations: Repetition 38

2.3.4 Sequence Operations: And, Intersect, Or 40

2.3.5 Local Variables 41

2.3.6 Properties 42

2.3.7 Assume-Assert Specifications 44

2.3.8 The Cover Statement 47

2.4 Architectural Styles for Assertion IPs 47

2.4.1 The Main Steps 49

2.4.2 Coding Styles: Event and State-based Checkers 50

3 How Does the Property Checker Work? 59

3.1 Checkers are State Machines! 61

3.2 The Verification Strategy 63

3.3 Dynamic Property Verification 64

3.4 Formal Property Verification 67

3.4.1 Creating the Checker Automaton 68

3.4.2 FSM Extraction 72

3.4.3 Computing the Product 74

3.5 BDD-based Formal Property Verification 78

3.5.1 What is a BDD? 79

3.5.2 BDDs for State Machines 83

3.5.3 Symbolic Reachability 84

3.5.4 CTL Model Checking 90

3.6 SAT-based Formal Property Verification 92

3.6.1 What is SAT? 92

3.6.2 SAT-based Reachability 93

3.6.3 Detecting Loops 95

3.6.4 Unfolding Properties 96

3.6.5 Bounded Model Checking 96

4 Is My Specification Consistent? 101

4.1 Satisfiability and Vacuity 103

4.1.1 Writing Unsatisfiable Specifications 103

4.1.2 The Notion of Vacuity 105

4.2 Satisfiability is not Enough 105

4.2.1 Readability 107

4.2.2 Receptiveness 109

4.3 Games with the Environment 114

4.4 Methods for Consistency Checking 115

4.4.1 Alternating Automata and LTL 117

4.4.2 Satisfiability Checks 119

4.4.3 Realizability Checks 121

4.4.4 Receptiveness Checks 124

4.5 The SpecChecker Tool 125

5 Have I Written Enough Properties? 129

5.1 Simulation Coverage Metrics 131

5.2 Mutation-based FPV Coverage 132

5.2.1 Falsity and Vacuity Coverage 134

5.2.2 FSM Coverage 135

5.2.3 Code and Circuit Coverage 136

5.3 Structural Versus Functional Coverage 136

5.4 Fault-based FPV Coverage 138

5.4.1 The Coverage Strategy 141

5.4.2 Coverage of Faults on Non-inputs 142

5.4.3 Coverage of Faults on Inputs 145

5.4.4 LTL-Covanalyzer: The Tool 148

5.4.5 Building it Over FPV Tools 149

5.4.6 Other Fault Models 153

6 Design Intent Coverage 157

6.1 An Introductory Example 160

6.1.1 Priority Cache Access: Architectural Specs 160

6.1.2 Is my Implementation Plan Correct? 162

6.1.3 The Correct Architecture 165

6.1.4 How Does Design Intent Coverage Help? 166

6.2 The Formal Problem 167

6.2.1 Where is the Coverage Gap? 171

6.2.2 How Should We Present the Coverage Hole? 173

6.3 The Intent Coverage Algorithm 174

6.3.1 Unfolding the Coverage Gap 175

6.3.2 Elimination of Non-architectural Signals 177

6.3.3 The Term Distribution Algorithm 178

6.3.4 Weakening Unbounded Temporal Properties 182

6.3.5 Special Treatment of Invariant Properties 184

6.4 Soundness of the Intent Coverage Algorithm 186

6.5 Multi-property Representation of the Coverage Gap 186

6.6 SpecMatcher - The Intent Coverage Tool 188

6.7 Priority Cache Access - A Closer Look 189

7 Test Generation Games 195

7.1 Constrained Random Test Generation 196

7.1.1 Layered Verification Methodologies 197

7.1.2 The Benefits 199

7.1.3 The Limitations 201

7.1.4 Dynamic Coverage Driven Verification 202

7.2 Assertions Viewed as Coverage Points! 203

7.3 Games with the Environment 204

7.3.1 Vacuity Games 205

7.3.2 Readability Games 207

7.4 Intelligent Test Generation for Property Coverage 208

7.4.1 Dynamic Monitoring 208

7.4.2 Online Test Generation 209

7.4.3 Test Generation Algorithms 210

7.5 The Integrated Verification Flow 212

8 A Roadmap for Formal Property Verification 217

8.1 Simulation-based Validation Flow 218

8.2 Formal Verification Flow 221

8.3 The Three Pillars 224

8.3.1 What's Between Simulation and Model Checking? 229

8.3.2 What's between Intent Coverage and Model Checking? 231

8.3.3 What's between Intent Coverage and Simulation? 233

8.4 The Integrated Flow 234

8.4.1 Architectural Validation 235

8.4.2 RTL Validation 236

8.5 Sharing the Task 238

8.5.1 Architect's Corner 238

8.5.2 Design Manager's Corner 239

8.5.3 Unit Designer's Corner 240.

Notes:

Includes bibliographical references (pages [243]-248) and index.

ISBN:

1402047576

OCLC:

71200310