Technical Tutorial:
"SVA Advanced Topics: SVAUnit and Assertions for Formal"


SystemVerilogSystemVerilog Assertions (SVA) is one of the central pieces in functional verification for protocol checking or validation of specific functions. This tutorial introduces advanced topics for assertion-based verification including SVAUnit and SVA for formal.

The first half of the tutorial discusses SVA planning, coding guidelines, SVAUnit (SVAUnit framework, self-checking tests, debug), and test patterns. Planning includes parameterization, temporal sequence composition, and sequence reuse as well as consideration of how the SVA package will be integrated with other verification methods. Coding guidelines and avoiding common implementation pitfalls ensures efficiency.

SVAUnit is a new concept that specifically addresses these requirements and more:

The first half of the tutorial closes with the presentation of SVA test patterns for the most common temporal sequences and scenarios.

In the second half of the tutorial describes how to define objects in SystemVerilog by specifying their properties formally. This formal specification is then used for assertion or coverage purposes with real USB interface examples and shows the advantages over scripting and SystemVerilog always blocks. Example include Perl scripting at over 3X less efficiency and SystemVerilog with always structures at 6X less efficiency. In addition, a well-defined SVA library is part of the verification methodology where generic sequences are reused. And, the inclusion of SVA reduces the debug effort since SVA points to a specific area where the error was detected. The tutorial describes the basics of the formal specification using SystemVerilog language as a vehicle and covers the formal specification applications on assertions and coverage.

The tutorial is split into two sections:



Register to view >>