Introduction - SVA: The Power of Assertions in SystemVerilog - page 13

1.2.2 Using Assertions for RTL Models

The methodology of using assertions for RTL design verification is commonly
known as Assertion-Based Verification (ABV), [ 19 , 37 , 44 , 67 ]. The idea is to
instrument RTL code with assertions to capture the design intent and to check
the local correctness of the design. In the former case, assertions are written for
checking the behavior at the interfaces. In the latter case, assertions are embedded
in the design units, interspersed through the code as needed to check the local
correctness.

Assertions on Interfaces

In this method, assertions are written to express the behavior as seen at an interface.
Customarily, verification engineers write such assertions as they do not require
intimate knowledge of the design details. This method of verification where the
design units are viewed as black boxes, meaning without the knowledge of internal
design details, is called black-box verification .
Verification engineers examine the high level specification of a design unit to
infer rules and properties that must be satisfied by the design unit. Each rule may
translate to one or more assertions. Once written and corrected, these assertions
tend to remain unaffected by the changes in the internal design unit code. They are
nonintrusive to the design units and can be retained physically outside the design
units as well. SystemVerilog provides means of attaching checkers to the design
units whenever needed using the bind statement, without actually modifying the
source code of the design units (see Sect. 9.3.3 ).
Some examples of the functionality checked by the interface assertions are:

￿ Bus communication protocols
￿ Memory transactions
￿ Data transformations
￿ Transaction arbitration

Another pivotal use of these assertions is to detect errors when various design
units are assembled into a larger unit. As integration issues emerge, they are effec-
tively captured by these assertions. By maintaining the consistency of interfaces,
individual design units are effectively freed from outside considerations, at least for
verification purposes.

Embedding Assertions Within Design

Most often designers attend to their design units for local correctness. Within the
scope of the design unit, they write assertions as they develop code to ensure signal