Tutorial: SVA Advanced Topics: SVAUnit and Assertions for Formal
Presented at DVCon U.S. 2016 on February 29, 2016
SystemVerilog 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 specifically addresses these requirements and more:
- Decouple assertion validation code from assertion definition code
- Simplify the generation of a wide range of stimuli, from 1-bit signal toggling to transactions
- Provide the ability to reuse scenarios
- Provide self-checking mechanisms
- Report test status automatically
- Integrate with major simulators
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:
- Part 1: SystemVerilog Assertions Verification with SVAUnit
Ionut Ciocirîan and Andra Radu, AMIQ
(00:00) - Part 2: Formal Specification, SystemVerilog Assertions & Coverage
Rodrigo Calderón-Rico and Israel Tapia, Intel
(48:24)
Thanks to our Sponsors
