Description
Springer Assertion-Based Design by Harry D. Foster, Adam C. Krolnik, David J. Lacey
There is much excitement in the design and verification community about assertion-based design. The question is, who should study assertion-based design? The emphatic answer is, both design and verification engineers. What may be unintuitive to many design engineers is that adding assertions to RTL code will actually reduce design time, while better documenting design intent. Every design engineer should read this book! Design engineers that add assertions to their design will not only reduce the time needed to complete a design, they will also reduce the number of interruptions from verification engineers to answer questions about design intent and to address verification suite mistakes. With design assertions in place, the majority of the interruptions from verification engineers will be related to actual design problems and the error feedback provided will be more useful to help identify design flaws. A design engineer who does not add assertions to the RTL code will spend more time with verification engineers explaining the design functionality and intended interface requirements, knowledge that is needed by the verification engineer to complete the job of testing the design._x000D_ Table of contents :- _x000D_
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 pattern.- 6.3.2 Valid signal combination pattern.- 6.3.3 Invalid signal combination pattern.- 6.4 Conditional patterns.- 6.4.1 Conditional expression pattern.- 6.4.2 Sequence implication pattern.- 6.5 Past and future event patterns.- 6.5.1 Past event pattern.- 6.5.2 Future event pattern.- 6.6 Window patterns.- 6.6.1 Time-bounded window patterns.- 6.6.2 Event-bounded window patterns.- 6.7 Sequence patterns.- 6.7.1 Forbidden sequence patterns.- 6.7.2 Buffered data validity pattern.- 6.7.3 Tagged transaction pattern.- 6.7.4 Pipelined protocol pattern.- 6.8 Applying patterns to a real example.- 6.8.1 Intra-interface assertions.- 6.8.2 Inter-interface assertions.- 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.8.1 Encoded multiplexer.- 7.8.2 Decoded (one-hot) multiplexer.- 7.8.3 Priority multiplexer.- 7.8.4 Complex multiplexer.- 7.9 Encoder.- 7.10 Priority encoder.- 7.11 Simple single request protocol.- 7.12 In-order multiple request protocol.- 7.13 Out-of-order request interface.- 7.14 State tables.- 7.15 Memories.- 7.16 Arbiter.- 7.17 Summary.- 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._x000D_