TABLE OF CONTENTS	6
	PREFACE	15
	Book organization	17
	New in Second Edition	20
	Acknowledgements	20
	1 INTRODUCTION	22
	1.1 Property checking	22
	1.2 Verification techniques	23
	1.3 What is an assertion?	24
	1.3.1 A historical perspective	25
	1.3.2 Do assertions really work?	27
	1.3.3 What are the benefits of assertions?	28
	1.3.4 Why are assertions not used?	32
	1.4 Phases of the design process	35
	1.4.1 Ensuring requirements are satisfied	37
	1.4.2 Techniques for ensuring consistency	39
	1.4.3 Roles and ownership	40
	1.5 Summary	41
	2 ASSERTION METHODOLOGY	42
	2.1 Design methodology	42
	2.1.1 Project planning	43
	2.1.2 Design requirements	48
	2.1.3 Design documents	49
	2.1.4 Design reviews	50
	2.1.5 Design validation	51
	2.2 Assertion methodology for new designs	51
	2.2.1 Key learnings	52
	2.2.2 Best practices	54
	2.2.3 Assertion density	58
	2.2.4 Process for adding assertions	60
	2.2.5 When not to add assertions	60
	2.3 Assertion methodology for existing designs	61
	2.4 Assertions and simulation	63
	2.5 Assertions and formal verification	65
	2.5.1 Formal verification framework	65
	2.5.2 Formal methodology	69
	2.5.3 ECC example	74
	2.5.4 Gradual exhaustive formal verification	77
	2.6 Summary	80
	3 SPECIFYING RTL PROPERTIES	81
	3.1 Definitions and concepts	82
	3.1.1 Property	82
	3.1.2 Events	85
	3.2 Property classification	85
	3.2.1 Safety versus liveness	86
	3.2.2 Constraint versus assertion	87
	3.2.3 Declarative versus procedural	87
	3.3 RTL assertion specification techniques	88
	3.3.1 RTL invariant assertions	89
	3.3.2 Declaring properties with PSL	92
	3.3.3 RTL cycle related assertions	93
	3.3.4 PSL and default clock declaration	94
	3.3.5 Specifying sequences	95
	3.3.6 Specifying eventualities	100
	3.3.7 PSL built- in functions	102
	3.4 Pragma- based assertions	102
	3.5 SystemVerilog assertions	104
	3.5.1 Immediate assertions	104
	3.5.2 Concurrent assertions	106
	3.5.3 System functions	115
	3.6 PCI property specification example	116
	3.6.1 PCI overview	116
	3.7 Summary	122
	4 PLI-BASED ASSERTIONS	123
	4.1 Procedural assertions	124
	4.1.1 A simple PLI assertion	125
	4.1.2 Assertions within a simulation time slot	128
	4.1.3 Assertions across simulation time slots	131
	4.1.4 False firing across multiple time slots	136
	4.2 PLI-based assertion library	138
	4.2.1 Assert quiescent state	139
	4.3 Summary	143
	5 FUNCTIONAL COVERAGE	144
	5.1 Verification approaches	145
	5.2 Understanding coverage	146
	5.2.1 Controllability versus observability	147
	5.2.2 Types of traditional coverage metrics	147
	5.2.3 What is functional coverage?	149
	5.2.4 Building functional coverage models	151
	5.2.5 Sources of functional coverage	152
	5.3 Does functional coverage really work?	153
	5.3.1 Benefits of functional coverage	154
	5.3.2 Success stories	154
	5.3.3 Why is functional coverage not used	155
	5.4 Functional coverage methodology	156
	5.4.1 Steps to functional coverage	157
	5.4.2 Correct coverage density	158
	5.4.3 Incorrect coverage density	160
	5.4.4 Coverage analysis	161
	5.4.5 Coverage best practices	164
	5.4.6 Coverage-driven test generation	168
	5.5 Specifying functional coverage	169
	5.5.1 Embedded in the RTL	169
	5.5.2 Functional coverage libraries	170
	5.5.3 Assertion- based methods	171
	5.5.4 Post processing	173
	5.5.5 PLI logging and reporting	173
	5.5.6 Simulation control	174
	5.6 Functional coverage examples	175
	5.7 AHB example	177
	5.8 Summary	179
	6 ASSERTION PATTERNS	180
	6.1 Introduction to patterns	180
	6.1.1 What are assertion patterns?	181
	6.1.2 Elements of an assertion pattern	182
	6.2 Signal patterns	183
	6.2.1 X detection pattern	183
	6.2.2 Valid range pattern	186
	6.2.3 One- hot pattern	188
	6.2.4 Gray-code pattern	191
	6.3 Set patterns	192
	6.3.1 Valid opcode pattern	192
	6.3.2 Valid signal combination pattern	194
	6.3.3 Invalid signal combination pattern	196
	6.4 Conditional patterns	198
	6.4.1 Conditional expression pattern	198
	6.4.2 Sequence implication pattern	200
	6.5 Past and future event patterns	204
	6.5.1 Past event pattern	204
	6.5.2 Future event pattern	206
	6.6 Window patterns	208
	6.6.1 Time-bounded window patterns	208
	6.6.2 Event-bounded window patterns	211
	6.7 Sequence patterns	213
	6.7.1 Forbidden sequence patterns	213
	6.7.2 Buffered data validity pattern	214
	6.7.3 Tagged transaction pattern	215
	6.7.4 Pipelined protocol pattern	218
	6.8 Applying patterns to a real example	221
	6.8.1 Intra-interface assertions	223
	6.8.2 Inter-interface assertions	227
	6.9 Summary	229
	7 ASSERTION COOKBOOK	230
	7.1 Queue-FIFO	232
	7.1.1 Assertions	233
	7.1.2 FIFO functional coverage	237
	7.2 Fixed depth pipeline register	238
	7.2.1 Assertions	239
	7.2.2 Functional coverage	241
	7.3 Stack-LIFO	241
	7.3.1 Assertion	242
	7.3.2 Functional coverage	243
	7.4 Caches - direct mapped	244
	7.4.1 Assertions	246
	7.4.2 Functional coverage	248
	7.5 Cache - set associative	250
	7.5.1 Assertion	252
	7.5.2 Functional coverage	253
	7.6 FSM	255
	7.6.1 Assertions	256
	7.6.2 Functional coverage	258
	7.7 Counters	259
	7.7.1 Assertions	260
	7.7.2 Functional coverage	261
	7.8 Multiplexers	263
	7.8.1 Encoded multiplexer	263
	7.8.2 Decoded one-hot multiplexer	264
	7.8.3 Priority multiplexer	265
	7.8.4 Complex multiplexer	267
	7.9 Encoder	268
	7.10 Priority encoder	270
	7.10.1 Functional coverage	270
	7.11 Simple single request protocol	271
	7.11.1 Assertions	271
	7.11.2 Functional Coverage	272
	7.12 In-order multiple request protocol	273
	7.12.1 Functional Coverage	273
	7.13 Out-of-order request protocol	276
	7.13.1 Functional coverage	277
	7.14 Memories	278
	7.14.1 Assertions	279
	7.15 Arbiter	281
	7.15.1 Assertions	282
	7.15.2 Functional coverage	284
	7.16 Summary	285
	8 SPECIFYING CORRECT BEHAVIOR	286
	8.1 Natural language interpretation	286
	8.1.1 Temporal ambiguity	287
	8.1.2 Active ambiguity	290
	8.1.3 Boundary ambiguity	292
	8.1.5 Implicit assumption	295
	8.1.6 Partial specification	296
	8.2 Property specification guidelines	297
	8.2.1 Sequence ambiguity	299
	8.2.2 Syntax ambiguity	299
	8.3 Clarity in higher- level specification	300
	8.3.1 Implementation assertions	302
	8.3.2 Higher-level requirements	304
	8.3.3 Modeling high-level requirements	306
	8.4 Summary	307
	A OPENVERIFICATION LIBRARY	309
	A. 1 OVL methodology advantages	309
	A. 2 OVL standard definition	310
	A. 2.1 OVL runtime macro controls	311
	A. 2.2 Customizing OVL messages	312
	A. 3 Firing OVL monitors	314
	A. 4 Using OVL assertion monitors	315
	A. 5 Checking invariant properties	316
	A. 5.1 assert_always	316
	A. 5.2 assert_never	318
	A. 5.3 assert_ zero_ one_ hot	320
	A.5.4 assert_range	321
	A.6 Checking cycle relationships	323
	A.6.1 assert_next	323
	A.6.2 assert frame	325
	A.6.3 assert_cycle_sequence	327
	A.7 Checking event bounded windows	329
	A.7.1 assert_win_change	329
	A.7.2 assert_win_unchange	331
	A.8 Checking time bounded	332
	A.8.1 assert_change	333
	A.8.2 assert_unchange	334
	A.9 Checking state transitions	336
	A.9.1 assert_no_transition	336
	A.9.2 assert_transition	337
	B PSL PROPERTY SPECIFICATIONLANGUAGE	339
	B.1 Introduction to PSL	339
	B.2 Operators and keywords	340
	B. 3 PSL Boolean layer	341
	B. 4 PSL Temporal Layer	342
	B.4.1 SERE	342
	B.4.2 Sequence	343
	B.4.3 Braced SERE	343
	B.4.4 SERE concatenation (	343
	B.4.5 Consecutive repetition ([* ]) operator	343
	B.4.6 Nonconsecutive repetition ([= ]) operator	345
	B.4.9 Sequence non-length-matching (&) operator	347
	B.4.10 Sequence length-matching (&&) operator	347
	B.4.11 Sequence or (|) operator	347
	B.4.12 until* sequence operators	348
	B.4.13 within sequence operators	348
	B.4.14 next operator	348
	B.4.15 eventually! operator	349
	B.4.16 before* operators	349
	B.5 PSL properties	352
	B.5.1 Property declaration	352
	B.5.2 Named properties	352
	B.5.3 Property clocking	352
	B.5.4 forall property replication	353
	B.6 The verification layer	354
	B.6.1 assert directive	354
	B.6.2 assume directive	354
	B.6.3 cover directive	354
	B.7 The modeling layer	355
	B.7.1 prev()	355
	B.7.2 next()	355
	B.7.3 stable()	356
	B.7.4 rose()	356
	B.7.5 fell()	357
	B.7.6 isunknown()	357
	B.7.7 countones()	357
	B.7.8 onehot(), onehot0()	358
	B. 8 BNF	358
	C SYSTEMVERILOG ASSERTIONS	370
	C.1 . Introduction to SystemVerilog	370
	C.2 Operator and keywords	370
	C.3 Sequence and property operations	372
	C.3.1 Temporal delay	373
	C.3.2 Consecutive repetition	374
	C.3.3 Goto repetition	374
	C.3.4 Nonconsecutive repetition	375
	C.3.5 Sequence and Property AND	376
	C.3.6 Sequence intersection	377
	C.3.7 Sequence and Property OR	377
	C.3.8 Boolean until (throughout)	378
	C.3.9 Within sequence	379
	C.3.10 Ended	379
	C.3.11 Matched	380
	C.3.12 First match	380
	C.3.13 Property Implication	381
	C.3.14 Conditional property selection	382
	C.4 Property declarations	383
	C.4.1 Sequence composition	385
	C.5 Assert, Assume and Cover statements.	386
	C.6 Dynamic data within sequences	387
	C.7 System Functions	388
	C.7.1 New operators	389
	C.8 SystemTasks	390
	C.9 BNF	391
	C.9.1 Use of Assertions BNF:	392
	C.9.2 Assertion statements	392
	C.9.3 Property and sequence declarations	393
	C.9.4 Property construction	394
	C.9.5 Sequence construction	395
	BIBLIOGRAPHY	396
	Index	401