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

1 module shreg ( input logic clk, rst, set, logic [7:0] val,
2 output logic [7:0] shift_reg);
3 always @( posedge clk or posedge rst) begin
4 if (rst) shift_reg <= 0;
5 else begin
6 if (set) shift_reg <= val;
7 else begin
8 shift_reg <= shift_reg << 1;
9 shift_reg[0] <= shift_reg[7];
10 end
11 end
12 end
13 check_shift: assert property (@( posedge clk) disable iff (rst)
14 set or
15 nexttime shift_reg == $past({shift_reg[6:0], shift_reg[7]}));
16 check_rst: assert final (rst -> shift_reg == '0);
17 endmodule : shreg

Fig. 1.7 Checks for a shift register

relationships. When assertions are written over internal signals of a design unit for
performing local checks, the verification process is termed as white-box verification .
A typical example is shown in Fig. 1.7 .
Module shreg in Fig. 1.7 implements a shift register shift_reg in RTL code
(Lines 3 - 12 ). Two assertions check_shift and check_rst verify the implementa-
tion correctness of the code.
The first assertion check_shift checks that the new value of shift_reg is
obtained by left rotation of its old value unless the new value was set explicitly
when set was asserted. The system function $past used in this assertion returns
the value of its argument evaluated at the previous clock cycle (see Sect. 7.2.1.2 ).
Note the operator disable iff , which disables the assertion check when the reset
signal is active.
The second assertion check_rst checks that shift_reg is reset correctly. We
use a final assertion which is not clocked, and not a concurrent one here because the
register reset is asynchronous and we need to check it at each simulation step, and
not only at the clock cycles. Section 1.3 and Chap. 4 explain the difference between
deferred and concurrent assertions in more detail.
Below are some typical items to check in white-box verification:

￿ Compliance of interface
￿ Finite State Machine (FSM) transitions
￿ Memory access correctness
￿ Stack and queue overflow and underflow
￿ Arithmetic overflow
￿ Signal stability

The complete list depends on a specific methodology; see [ 19 , 37 , 44 , 67 ]for
suggestions.