SystemVerilog Simulation Semantics - SVA: The Power of Assertions in SystemVerilog - page 55

Exercises

3.1. Identify all potential cases of glitches and races in the following code. Assume
that clk changes at most once per time step.
module m( input logic in, clk);
wire w, not_w, w_or_not_w;
logic next_w, v, not_v, v_or_not_v, next_v;
logic onev = 1'b1, onew = 1'b1;
assign w = in;
assign not_w = !in;
assign w_or_not_w = w || not_w;

always @( posedge clk) begin
next_w <= w;
onev <= v_or_not_v;
onew <= w_or_not_w;
end
always_comb begin
v=in;
not_v = !in;
v_or_not_v = v || not_v;
end
a1: assert property (@( posedge clk) w_or_not_w);
a2: assert property (@( posedge clk) v_or_not_v);
endmodule :m

3.2. Explain why SystemVerilog requires that all assertion clocks tick at most once
per simulation cycle (= time step).

3.3. Continue Table 3.1 in Example 3.7 for time steps 10 and 15. Assume that in
time step 15 $random returns an even number.
3.4. Fill a table analogous to Table 3.1 for the code in Example 3.8 .