Assertion-Based Design
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...
Main Authors: | , , |
---|---|
Format: | eBook |
Language: | English |
Published: |
New York, NY
Springer US
2003, 2003
|
Edition: | 1st ed. 2003 |
Subjects: | |
Online Access: | |
Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- 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
- 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
- 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
- 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