Formal Verification, 2nd Edition

Chapter 3: Introduction to SystemVerilog Assertions

Abstract

In Chapter 3, we describe the basics of the SystemVerilog Assertion (SVA) language, which is the current industry standard for verification statements that describe properties of an RTL design. Using a simple arbiter as an example verification target, we introduce each of the basic concepts of SVA. First, we define the three types of verification statements: assertions, facts that are claimed to be true; assumptions, axioms used to prove the assertions; and cover properties, which specify interesting test conditions. There are two major types of assertion statements that we describe in detail: immediate, or unclocked, and concurrent, or clocked, assertion statements. We then continue ...