System Verilog:Assertions and Our Coverage of System Verilog.

Assertions

Assertions are used to validate that a design works correctly. Assertions can be checked dynamically by a simulation tool. An assertion or property language is designed to capture the design intent in an executable, formal, and unambiguous way. In System Verilog, there are two types of assertions: immediate assertion and concurrent assertion which are described here.

Immediate Assertion

The immediate assertion statement is used to test a nontemporal expression as a condition in an if statement. If the expression is evaluated to 1 then assertion passes and the first statement, called pass statement is executed. And if the expression is evaluated to 0, Z, or X then the assertion fails and the statement associated with else, called fail statement is executed. Figure 90.49 illustrates an example of immediate assertion designed to verify the multiplier behavior. The use of pass statement and fail statement are optional.

The failure of an assertion has a severity associated with it. There are four severity system tasks that can be used in the fail statement to specify a severity level: $fatal, $error, $warning, and $info. By default, the $error is used as severity level of an assertion failure [1].

Concurrent Assertion

Concurrent assertions describe the clocked behavior of the design. Therefore a concurrent assertion is evaluated only at the clock edges. Figure 90.50 shows an example of using concurrent assertion to verify that the asynchronous clr and pr input of a flip-flop never be asserted simultaneously. Note that in this example both pass and fail statements are omitted.

Concurrent assertions are often constructed by sequential behavior and described using a list of System Verilog Boolean expressions in a linear order of increasing time. The implication construct (|->) allows to monitor sequences based on satisfying some conditions. The syntax of the implication is as follows:

where both s1 and s2 are sequences. The left-hand side operand of the implication is called antecedent sequence while the right-hand side operand is called consequent sequence. If the antecedent sequence matches then the consequent sequence should match. If there is no match of antecedent operand then the implication returns true. As an example consider a bus arbiter that receives a req input and provides a gnt output. Suppose that the gnt should occur no more than two clock cycles after the req is asserted. Figure 90.51 shows that the concurrent assertion describes this behavior. The ## operator followed by [1:2] is used to illustrate that gnt should occur in the next or in the following clock cycles after the clock cycle in which req is asserted.

Our Coverage of System Verilog

This chapter provides an overview of the new System Verilog language constructs, including new basic data types, user-defined data types, structures, unions, arrays, typecasting, enhancements in loops, new do-while loop, new operators, new procedural blocks (always_comb, always_latch, always_ff), and interface. In each case the construct was described and several examples were provided to clarify its usage. Then a complete example, an add-and-shift multiplier, was described and modeled by System Verilog. Finally, we had a brief overview of assertions in System Verilog.