March 2-5, 2020

DoubleTree Hotel, San Jose, CA

MP Associates, Inc.

MONDAY February 29, 9:00am - 12:00pm | Fir

SVA Advanced Topics: SVAUnit and Assertions for Formal

Ionut Ciocirlan - AMIQ
Andra Radu - AMIQ
Rodrigo Calderon-Rico - Intel Corp.
Israel Tapia - Intel Corp.
Adam Sherer - Accellera Systems Initiative
SystemVerilog Assertions (SVA) is one of the central pieces in functional verification for protocol checking or validation of specific functions. This tutorial will introduce advanced topics for assertion based verification including SVAunit and SVA for formal. This first half of the tutorial discusses SVA planning, coding guidelines, SVAUnit (SVAUnit framework, self-checking tests, debug), and test patterns. Planning includes parametrization, temporal sequence composition, sequence reuse and also consider how the SVA package will be integrated with other verification methods. Coding guidelines ensure efficiency as well as avoid common implementation pitfalls.

SVAUnit is a new concept that 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

This 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 we learn how to define objects in SystemVerilog by specifying their properties formally. Then, this formal specification is used for assertion or coverage purposes with real USB interface examples and show the advantages over scripting and SystemVerilog always blocks. For example, the Perl scripting was at least 3X less efficient, while using SystemVerilog with always structures was 6X worse. In addition, a well-defined SVA library is part of the verification methodology where generic sequences are reused.

Finally, the inclusion of SVA reduces the debug effort since SVA points to a specific area where the error was detected. This second half of the tutorial contains 3 sections, the first part explains the formal specification where its basics are clearly described using SystemVerilog language as a vehicle. The second and third part cover the formal specification applications on assertions and coverage respectively.