Assertion-Based Design

The focus of this volume is three-fold: how to specify assertions; how to create and adopt a methodology that supports assertion-based design (predominately for RTL design); and what to do with the assertions and methodology once you have them.

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 operators 9.- First match operator 9.- Throughout operators 9.- Dynamic variables within sequences 9.- 3.5.3 System functions.- 3.6 PCI property specification example.- 3.6.1 PCI overview.- 3.7 Summary.- 4 PLI-Based Assertions.- 4.1 Procedural assertions.- 4.1.1 A simple PLI assertion.- Checktf routine 11.- Calltf routine 11.- 4.1.2 Assertions within a simulation time slot.- Nested PLI assertion problem 11.- 4.1.3 Assertions across simulation time slots.- Controlling assertion evaluations by a clock 11.- 4.1.4 False firing across multiple time slots.- 4.2 PLI-based assertion library.- 4.2.1 Assert quiescent state.- 4.3 Summary.- 5 Functional Coverage.- 5.1 Verification approaches.- 5.2 Understanding coverage.- 5.2.1 Controllability versus observability.- 5.2.2 Types of traditional coverage metrics.- 5.2.3 What is functional coverage?.- 5.2.4 Building functional coverage models.- 5.2.5 Sources of functional coverage.- 5.3 Does functional coverage really work?.- 5.3.1 Benefits of functional coverage.- 5.3.2 Success stories.- 5.3.3 Why is functional coverage not used.- 5.4 Functional coverage methodology.- 5.4.1 Steps to functional coverage.- 5.4.2 Correct coverage density.- 5.4.3 Incorrect coverage density.- 5.4.4 Coverage analysis.- Coverage data organization 15.- Tracking functional coverage 15.- Actions to take 15.- 5.4.5 Coverage best practices.- 5.4.6 Coverage-driven test generation.- 5.5 Specifying functional coverage.- 5.5.1 Embedded in the RTL.- 5.5.2 Functional coverage libraries.- 5.5.3 Assertion-based methods.- 5.5.4 Post processing.- 5.5.5 PLI logging and reporting.- 5.5.6 Simulation control.- 5.6 Functional coverage examples.- 5.7 AHB example.- 5.8 Summary.- 6 Assertion Patterns.- 6.1 Introduction to patterns.- 6.1.1 What are assertion patterns?.- 6.1.2 Elements of an assertion pattern.- 6.2 Signal patterns.- 6.2.1 X detection pattern.- 6.2.2 Valid range pattern.- 6.2.3 One-hot pattern.- 6.2.4 Gray-code pattern.- 6.3 Set patterns.- 6.3.1 Valid opcode pat...