1 Introduction -- 1.1 Property checking -- 1.2 Verification techniques -- 1.3 What is an assertion? -- 1.4 Phases of the design process -- 1.5 Summary -- 2 Assertion Methodology -- 2.1 Design methodology -- 2.2 Assertion methodology for new designs -- 2.3 Assertion methodology for existing designs -- 2.4 Assertions and simulation -- 2.5 Assertions and formal verification -- 2.6 Summary -- 3 Specifying RTL Properties -- 3.1 Definitions and concepts -- 3.2 Property classification -- 3.3 RTL assertion specification techniques -- 3.4 Pragma-based assertions -- 3.5 SystemVerilog assertions -- 3.6 PCI property specification example -- 3.7 Summary -- 4 PLI-Based Assertions -- 4.1 Procedural assertions -- 4.2 PLI-based assertion library -- 4.3 Summary -- 5 Functional Coverage -- 5.1 Verification approaches -- 5.2 Understanding coverage -- 5.3 Does functional coverage really work? -- 5.4 Functional coverage methodology -- 5.5 Specifying functional coverage -- 5.6 Functional coverage examples -- 5.7 AHB example -- 5.8 Summary -- 6 Assertion Patterns -- 6.1 Introduction to patterns -- 6.2 Signal patterns -- 6.3 Set patterns -- 6.4 Conditional patterns -- 6.5 Past and future event patterns -- 6.6 Window patterns -- 6.7 Sequence patterns -- 6.8 Applying patterns to a real example -- 6.9 Summary -- 7 Assertion Cookbook -- 7.1 Queue-FIFO -- 7.2 Fixed depth pipeline register -- 7.3 Stack-LIFO -- 7.4 Caches-direct mapped -- 7.5 Cache-set associative -- 7.6 FSM -- 7.7 Counters -- 7.8 Multiplexers -- 7.9 Encoder -- Appendix A Open Verification Library -- A.1 OVL methodology advantages -- A.2 OVL standard definition -- A.2.1 OVL runtime macro controls -- A.2.2 Customizing OVL messages -- A.3 Firing OVL monitors -- A.4 Using OVL assertion monitors -- A.5 Checking invariant properties -- A.5.1 assert_always -- A.5.2 assert_never -- A.5.3 assert_ zero_ one_ hot -- A.5.4 assert_range -- A.6 Checking cycle relationships -- A.6.1 assert_next -- A.6.2 assert_frame -- A.6.3 assert_cycle_sequence -- A.7 Checking event bounded windows -- A.7.1 assert_win_change -- A.7.2 assert_win_unchange -- A.8 Checking time bounded windows -- A.8.1 assert_change -- A.8.2 assert_unchange -- A.9 Checking state transitions -- A.9.1 assert_no_transition -- A.9.2 assert transition -- Appendix B PSL Property Specification Language. -- B.1 Introduction to PSL -- B.2 Operators and keywords -- B.3 PSL Boolean layer -- B.4 PSL Temporal Layer -- B.4.1 Named SERE -- B.4.2 SERE concatenation (;) operator -- B.4.3 Consecutive repetition ([*]) operator -- B.4.4 Nonconsecutive repetition ([=]) operator -- B.4.5 Goto repetition ([->]) operator -- B.4.6 Sequence fusion (:) operator -- B.4.7 Sequence non-length-matching (&) operator -- B.4.8 Sequence length-matching (&) operator -- B.4.9 Sequence or (I) operator -- B.4.10 until* sequence operators -- B.4.11 within* sequence operators -- B.4.12 next operator -- B.4.13 eventually! operator -- B.4.14 before* operators -- B.4.15 abort operator -- B.4.16 Endpoint declaration -- B.4.17 Suffix implication operators -- B.4.18 Logical implication operator -- B.4.19 always temporal operator -- B.4.20 never temporal operator -- B.5 PSL properties -- B.5.1 Property declaration -- B.5.2 Named properties -- B.5.3 Property clocking -- B.5.4 forall property replication -- B.6 The verification layer -- B.6.1 assert directive -- B.6.2 assume directive -- B.6.3 cover directive -- B.7 The modeling layer -- B.7.1 rose() and fell() functions -- B.7.2 prey() and next() functions -- B.8 BNF -- B.8.1 Verilog Extensions -- B.8.2 Flavor macros -- B.8.3 Syntax productions -- Appendix C SystemVerilog Assertions -- C.1. Introduction to SystemVerilog -- C.2 Operator and keywords -- C.3 Sequence and property operations -- C.3.1 Temporal delay -- C.3.2 Consecutive repetition -- C.3.3 Goto repetition -- C.3.4 Nonconsecutive repetition -- C.3.5 Sequence and -- C.3.6 Sequence intersection -- C.3.7 Sequence or -- C.3.8 Boolean until (throughout) -- C.3.9 Within sequence -- C.3.10 Ended -- C.3.11 Matched -- C.3.12 First match -- C.3.13 Implication -- C.4 Sequences and properties -- C.5 Assert and cover statements. -- C.6 Dynamic data within sequences -- C.7 Templates -- C.8 System Functions -- C.9 SystemTasks -- C.10 BNF -- C.10.1 Use of Assertions BNF: -- C.10.2 Assertion statements -- C.10.3 Property and sequence declarations -- C.10.4 Property construction -- C.10.5 Sequence construction.