SystemVerilog Assertions (SVA)
Ming-Hwa Wang, Ph.D.
COEN 207 SoC (System-on-Chip) Verification
Department of Computer Engineering
Santa Clara University
Introduction
• Assertions are primarily used to validate the behavior of a design
• Piece of verification code that monitors a design implementation for
compliance with the specifications
• Directive to a verification tool that the tool should attempt to
prove/assume/count a given property using formal methods
• Capture the design intent more formally and find specification error
earlier
• Find more bugs and source of the bugs faster
• Encourage measurement of function coverage and assertion coverage
• Re-use checks throughout life-cycle, strength regression testing
Formal Method
Formal assertion-based verification flow
Benefits of Assertions
• Improves observability of the design
• Using assertions one can create unlimited number of observation
points any where in the design
• Enables internal state, datapath and error pre-condition coverage
analysis
• Improves debugging of the design
• Assertion help capture the improper functionality of the DUT at or
near the source of the problem thereby reducing the debug time
• With failure of assertion one can debug by considering only the
dependent signals or auxiliary code associated to the specific
assertion in question
• Assertion also helps to capture bugs, which do not propagate to the
output
• Improves the documentation of the Design
• Assertions capture the specification of the Design. The spec is
translated into an executable form in the form of assertions,
assumptions, constraints, restrictions. The specifications are checked
during the entire development and validation process
• Assumptions in assertions capturing the design assumptions
continuously verify whether the assumptions hold true throughout
the simulation
• Assertions always capture the specification in concise form which is
not ambiguous i.e., assertions are the testable form of requirements
• Assertions go along with the design and can also be enabled at SOC
level
• Assertion can be used to provide functional coverage
• Functional coverage is provided by cover property
• Cover property is to monitor the property evaluation for functional
coverage. It covers the properties/sequences that we have specified
• We can monitor whether a particular verification node is exercised or
not as per the specification
• Can be written for
• Low-level functionality coverage inside a block
• High-level functionality coverage at interface level
• Can use these assertions in formal analysis
• Formal analysis uses sophisticated algorithms to prove or disprove
that a design behaves as desired for all the possible operating
states. One limitation is that it is effective only in block level not at
full chip or SOC level
• Desire behavior is not expressed in a traditional test bench, but
rather as a set of assertions. Formal analysis does not require test
vectors
• With Formal analysis many bugs can be found quickly and very
easily in the Design process without the need to develop large sets
of test vectors
Where SVA can reside?
Who writes Assertions?
• White-Box Verification
• Inserted by design engineers
• Block Interfaces
• Internal signals
• Black-box Verification
• Inserted by
• IP Providers
• Verification Engineers
• External interfaces
• End-to-end properties
Testbench Assertions
Interfaces Assertions
Top level DUT Assertions
Block level DUT Assertions
Module Assertions Module Assertions
Different clock domains assertions
评论0
最新资源