Assertions are temporal checks on given protocol.
- counter_assertions.sv contains temporal checks, with assertion sequence and property, on counter DUT protocol.
- As each signal here is coming from DUT, it should be defined as inputs.
module counter_assertion(clk, rst, data, updown, load, count);
input logic clk, rst;
input logic updown, load;
input logic [3:0] data, count;
property reset_prpty;
@(posedge clk) rst |=> (count == 4'b0);
endproperty
sequence up_seq;
!load && updown;
endsequence
sequence down_seq;
!load && !updown;
endsequence
property up_count_prpty;
@(posedge clk) disable iff(rst)
up_seq |=> (count == ($past(count, 1) + 1'b1));
endproperty
property down_count_prpty;
@(posedge clk) disable iff(rst)
down_seq |=> (count == ($past(count, 1) - 1'b1));
endproperty
property count_Fto0_prpty;
@(posedge clk) disable iff(rst)
(!load && updown) && (count == 4'hF) |=> (count == 4'b0);
endproperty
property count_0toF_prpty;
@(posedge clk) disable iff(rst)
(!load && !updown) && (count == 4'b0) |=> (count == 4'hF);
endproperty
property load_prpty;
@(posedge clk) disable iff(rst)
load |=> (count == $past(data, 1));
endproperty
RST: assert property (reset_prpty);
UP_COUNT: assert property (up_count_prpty);
DOWN_COUNT: assert property (down_count_prpty);
F2O: assert property (count_Fto0_prpty);
O2F: assert property (count_0toF_prpty);
LOAD: assert property (load_prpty);
endmodule
