SystemVerilog Assertions (SVA)

Abstract

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