Assertion-Based Design

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.