// Write a SV checker for the below RTL behavior
num_out is a 32 bit output coming from DUT at every posedge of clock in below fashion .
When there is a decrementing fashion decrement of num_out , checker should through the error otherwise its okay .
when there is no change in num_out value w.r.t previous one , it should not through any assertion error .
20 *1 // meaning num_out=20 for 1 time (takes 1 clk)
30*2 // meaning num_out=20 for 2 time (takes 2 clks)
8*3 // meaning num_out=8 for 3 time (takes 3 clks). assertion should fail here at intial clock.
100*4
10*2 //assertion should fail here at initial clock
50*3
200*4
80*4 //assertion should fail here at initial clock
60*3 //assertion should fail here at initial clock
70*4
100*1
Can somebody please confirm if I have written below checker correctly ?
Solution :
module seq_behavior_checker (logic clk,logic rst ,logic [31:0]num_out) ;
logic [31:0] num_temp;
logic [2:0] seq_incr_decre_const;
always @(posedge clk )begin
if (!rst) begin
num_temp=0 ;
seq_incr_decre_const = 3'b000;
end
else if (num_out == num_temp) begin // constant sequence case
seq_incr_decre_const = 3'b001;
end
else if ( num_out > num_temp) begin // incrementing sequece case
seq_incr_decre_const = 3'b100;
num_temp = num_out;
end
else begin // decrementing sequence case
num_temp= num_out;
seq_incr_decre_const = 3'b010;
end
end
//When there is a decrementing fashion decrement of num_out , checker should through the error otherwise its okay . when there is no change in num_out value w.r.t previous one , it should not through any assertion error .
property incr_check ( logic clk ,logic seq_incr_decre_const) ; // incrementing sequeuce pre-condition hit
@(posedge clk) disable if (!rst)
(seq_incr_decre_const ==3'b100) |=> ((seq_incr_decre_const ==3'b100) || (seq_incr_decre_const ==3'b001) );
endproperty
property decr_check ( logic clk ,logic seq_incr_decre_const) ; // decrementing sequence pre-condition hit
@(posedge clk) disable if (!rst)
(seq_incr_decre_const ==3'b010) |=> ((seq_incr_decre_const ==3'b100) || (seq_incr_decre_const ==3'b001) );
endproperty
property const_check ( logic clk ,logic seq_incr_decre_const) ; // constant sequence pre-condition hit .
@(posedge clk) disable if (!rst)
(seq_incr_decre_const ==3'b001) |=> (seq_incr_decre_const ==3'b100) || (seq_incr_decre_const ==3'b001) ) ;
endproperty
A1: assert property (incr_check (clk ,seq_incr_decre_const)) ;
A2: assert property (decr_check (clk ,seq_incr_decre_const)) ;
A3: assert property (const_check (clk ,seq_incr_decre_const)) ;
endmodule