Formal Verification

Chapter 3

Introduction to systemverilog assertions

In Chapter 3, we describe the basics of the System Verilog 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 points, 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 by describing ...