1 Introduction.- 1.1 Property Checking.- 1.2 Verification Techniques.- 1.3 What Is An Assertion?.- 1.3.1 A Historical Perspective.- 1.3.2 Do Assertions Really Work?.- 1.3.3 What Are The Benefits Of Assertions?.- 1.3.4 Why Are Assertions Not Used?.- 1.4 Phases Of The Design Process.- 1.4.1 Ensuring Requirements Are Satisfied.- 1.4.2 Techniques For Ensuring Consistency.- 1.4.3 Roles And Ownership.- 1.5 Summary.- 2 Assertion Methodology.- 2.1 Design Methodology.- 2.1.1 Project Planning.- Project Documents.- Eda And Internal Tools.- Rtl Styles And Conventions.- Support Infrastructure.- Partner Coordination.- 2.1.2 Design Requirements.- 2.1.3 Design Documents.- 2.1.4 Design Reviews.- 2.1.5 Design Validation.- 2.2 Assertion Methodology For New Designs.- 2.2.1 Key Learnings.- 2.2.2 Best Practices.- 2.2.3 Assertion Density.- 2.2.4 Process For Adding Assertions.- 2.2.5 When Not To Add Assertions.- 2.3 Assertion Methodology For Existing Designs.- 2.4 Assertions And Simulation.- 2.5 Assertions And Formal Verification.- 2.5.1 Formal Verification Framework.- 2.5.2 Formal Methodology.- 2.5.3 Ecc Example.- 2.6 Summary.- 3 Specifying Rtl Properties.- 3.1 Definitions And Concepts.- 3.1.1 Property.- 3.1.2 Events.- 3.2 Property Classification.- 3.2.1 Safety Versus Liveness.- 3.2.2 Constraint Versus Assertion.- 3.2.3 Declarative Versus Procedural.- 3.3 Rtl Assertion Specification Techniques.- 3.3.1 Rtl Invariant Assertions.- Ovl Invariant 6.- Psl Invariant 7.- 3.3.2 Declaring Properties With Psl.- 3.3.3 Rtl Cycle Related Assertions.- 3.3.4 Psl And Default Clock Declaration.- 3.3.5 Specifying Sequences.- Declaring Sequences Within Psl 8.- Sequence Operators Within Psl 8.- Checking Sequences With The Ovl 8.- 3.3.6 Specifying Eventualities.- Ovl Event Bounded Window Checkers 8.- 3.3.7 Psl Built-in Functions.- 3.4 Pragma-based Assertions.- 3.5 Systemverilog Assertions.- 3 5 1 Immediate Assertions.- 3.5.2 Concurrent Assertions.- Sequence Declaration 9.- Sequence Operations 9.- Repetition Op