Principles of Verifiable RTL Design: A functional coding style supporting verification processes in Verilog

Principles of Verifiable RTL Design (2nd Ed.)......Page 1
Copyright......Page 5
Table of Contents......Page 8
Foreword......Page 16
Preface......Page 20
Ch1 Introduction......Page 26
1.1.1 What is it?......Page 27
1.1.2 Verifiable RTL......Page 28
1.2 Assumptions......Page 29
1.3 Organization of this Book......Page 30
Ch2 Verification Process......Page 34
2.1 Specification Design Decomposition......Page 35
Fundamental Verification Principle......Page 36
2.1.4 Synthesis & Physical Design......Page 38
2.2 Functional Test Strategies......Page 39
2.2.1 Deterministic or Directed Test......Page 40
2.2.2 Random Test......Page 41
2.2.3 Transaction Analyzer Verification......Page 43
2.2.4 Chip Initialization Verification......Page 44
2.3 Transformation Test Strategies......Page 45
2.4 Summary......Page 46
Ch3 Coverage, Events & Assertions......Page 48
3.1 Coverage......Page 49
3.1.2 Programming Code Metrics......Page 50
3.1.5 Fault Coverage Metrics......Page 52
3.2 Event Monitors & Assertion Checkers......Page 53
3.2.1 Events......Page 54
3.2.2 Assertions......Page 56
3.2.3 Assertion Monitor Library Details......Page 61
3.2.4 Event Monitor & Assertion Checker Methodology......Page 62
3.2.4.2 Implementation Considerations......Page 64
3.2.4.3 Event Monitor Database & Analysis......Page 65
3.3 Summary......Page 66
Ch4 RTL Methodology Basics......Page 68
4.1 Simple RTL Verifiable Subset......Page 69
Recommendation: for Loop Construct......Page 72
Project Linting Principle......Page 73
4.2.1 Linting in Design Project......Page 74
4.2.2.1 Project Oriented......Page 75
4.2.2.2 Linting Message Examples......Page 76
4.3 Object-Based Hardware Design......Page 78
4.3.1 OBHD & Simulation......Page 81
4.3.2 OBHD & Formal Verification......Page 84
4.3.3.1 OBHD Synthesis......Page 85
4.3.3.2 OBHD Scan Chain Hookup......Page 87
4.3.4 Text Macro Implementation......Page 89
Object-Based Hardware Design Principle......Page 79
4.4 Summary......Page 92
Ch5 RTL Logic Simulation......Page 94
5.1.1 First Steps......Page 96
5.1.3 Function & Timing......Page 98
5.1.5 Acceleration & Emulation......Page 99
5.1.6 Language Standardization......Page 101
5.2 Project Simulation Phases......Page 103
5.2.1 Debugging Phase......Page 104
5.2.2 Performance Profiling Phase......Page 105
5.2.3 Regression Phase......Page 106
5.2.5 Performance......Page 107
5.3 Operation......Page 108
Visit Minimization Principle......Page 109
5.3.1.2 Rank-Ordered......Page 111
5.3.2.2 Compiled Code......Page 113
5.4 Optimizations......Page 114
5.4.3 Bus Reconstruction......Page 115
5.4.3.2 Expression Simplification......Page 116
5.4.5 Partitioning......Page 117
5.4.5.1 Branch Partitioning......Page 118
5.4.5.3 Chip Partitioning......Page 119
5.5.1.1 Design Method......Page 120
5.5.1.2 Zero Initialization......Page 121
5.5.1.3 Random Initialization......Page 122
5.5.2 Tri-State Buses......Page 123
5.5.3 Assertion Monitors......Page 124
5.6 Summary......Page 125
Ch6 RTL Formal Verification......Page 128
6.1 Formal Verification Introduction......Page 131
6.2 Finite State Machines......Page 132
6.2.1 Machine Equivalence......Page 135
6.2.2 FSM Property Verification......Page 136
6.3.1.1 Equivalence Checking Flow......Page 137
6.3.1.2 Closing Verification Loop......Page 139
6.3.2 Cutpoint Definition......Page 140
Cutpoint Identification Principle......Page 142
6.3.3.3 Equivalence Checking OBHD Practices......Page 143
6.3.4 RTL Static Sign-Off......Page 145
6.3.5 Effective Equivalence Checking Methodology......Page 147
6.4.1 Specification......Page 149
6.4.2 Model Checking & Parameterized Modules......Page 151
Numeric Value Parameterization Principle......Page 152
6.5 Summary......Page 153
Ch7 Verifiable RTL Style......Page 156
7.1.1 Asynchronous Logic......Page 157
Asynchronous Principle......Page 158
7.1.3 Combinational Feedback......Page 160
Combinational Feedback Principle......Page 162
7.1.4.1 Fully-Specified case Statements......Page 163
7.1.4.2 Test Signal & Constant Widths......Page 168
7.1.5 Tri-State Buses......Page 169
7.2.1.1 Compiler Options......Page 171
7.2.1.2 Design Hierarchy......Page 173
7.2.1.3 Files......Page 174
7.2.1.4 Libraries......Page 175
7.2.2.1 Overall Organization......Page 176
7.2.3 Expression Organization......Page 178
7.3.1.1 Consistency......Page 180
7.3.1.2 Upper/Lower Case......Page 181
7.3.1.3 Hierarchical Name References......Page 182
7.3.1.4 Global/Local Name Space......Page 183
7.3.1.5 Profiling Support......Page 184
7.3.2.3 Instances......Page 186
7.3.2.4 Modules......Page 187
7.3.2.5 Port Names......Page 188
7.3.2.6 Signal Names......Page 189
7.3.2.7 User Tasks/Functions & Program Libraries......Page 190
7.5 Editing Practices......Page 191
7.5.2 Comments......Page 192
7.5.2.2 Declarations......Page 193
7.5.2.4 Tool Controls......Page 194
Property Principle......Page 196
7.6 Summary......Page 197
Ch8 Bad Stuff......Page 198
8.1 In-Line Storage Element Specification......Page 199
8.2 RTL X-State......Page 200
8.2.1.1 RTL X-State Pessimism......Page 201
8.2.1.3 Impractical......Page 202
8.3.1 Bit Visits......Page 205
8.3.2 Configuration Test Visits......Page 206
8.3.3 for Loops......Page 207
Faithful Semantics Principle......Page 209
8.4.1.1 Full & Parallel Case......Page 210
8.4.1.2 X Assignment......Page 213
8.4.1.3 Other Forms of State Machines......Page 214
8.4.1.4 Initial Blocks......Page 215
8.4.2.1 Incomplete Sensitivity List......Page 216
8.4.2.3 Incorrect Procedural Statement Ordering......Page 217
8.4.3.1 Delays......Page 218
8.4.3.2 Race Conditions......Page 221
8.5.1 Linting & Problematic RTL Verilog......Page 223
8.5.3 Formal Verification & Problematic Verilog......Page 224
Good Vendor Principle......Page 225
8.6.1 Tool Library Function Naming......Page 226
8.6.2 Command Line Consistency......Page 227
8.6.3 Vendor Specific Properties......Page 228
8.7 Design Team Discipline......Page 229
8.8.2 Parameters......Page 230
8.8.3 User-Defined Primitives......Page 231
8.9 Summary......Page 232
Ch9 Verifiable RTL Tutorial......Page 234
9.1.1 Specification......Page 235
9.1.2 Comments......Page 236
9.1.4 Interconnection......Page 237
9.2 Adding Behavior......Page 240
9.3 Multi-Bit Interconnect & Behavior......Page 241
9.4 Parameters......Page 242
9.5.1.1 Binary Operators......Page 243
9.5.1.2 Unary Operators......Page 244
9.5.1.3 Miscellaneous Operators......Page 245
9.5.2 Operator Precedence......Page 246
9.6.1.1 Procedural Assignments......Page 247
9.6.1.2 Functions......Page 249
9.6.1.4 case, casex Statements......Page 250
9.6.2.1 Flip-Flops......Page 252
9.6.2.3 Memories......Page 253
9.6.3 Debugging......Page 254
9.6.3.1 $display & $write Statements......Page 255
9.7 Testbench......Page 256
9.8.1.1 Constants......Page 260
9.8.1.2 Code Inclusion......Page 261
9.8.1.3 Command Line......Page 262
9.9 Summary......Page 263
10.1 Principles......Page 264
10.1.4 Orthogonal Verification Principle......Page 265
10.1.7 Project Linting Principle......Page 266
10.1.11 Cutpoint Identification Principle......Page 267
10.1.13 Consistency Principle......Page 268
10.1.17 Faithful Semantics Principle......Page 269
10.2 Summary......Page 270
Bibliography......Page 272
AppA Comparing Verilog Construct Performance......Page 280
Lexical Elements......Page 284
Reserved Words......Page 285
Module Organization......Page 286
Procedural Statements......Page 287
Operators......Page 288
Compiler Directives......Page 289
AppC Assertion Monitors......Page 290
assert_always......Page 291
assert_change......Page 292
assert_window......Page 295
assert_frame......Page 297
Index......Page 302