SVA to check the signal how many times it has changed in the previous cycles

SystemVerilog
,
1

Hello SV experts,
I run into a situation where I need to check a signal how many times it has toggled in the previous cycles. Below is my waveform. based on the i_discard selection, I need to check after 16 clk cycles how many times the signal o_discard has changed. It’s a decimation logic. When i_discard == 0, I need to make sure at 1,3,5,7,9,11,13,15 clk cycle, o_dicard should be high. Similarly, when i_difscard==2’b01, o_discard should be high only at 1,3,9,11th clk cycle. Similarly for i_discard== 2 and i_discard==3. The decimation factor i_discard decides how many pairs should be discarded (It’s self explanatory from the waveform. )

// Positive Edges 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
// _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
// i_clk = | || || || || || || || || || || || || || || || |_
// ___ ___ ___ ___ ___ ___ ___ ___
// i_to_decimate = | || || || || || || || |_
//-------------------------------------------------------------------------------------
// i_discard = 2’b00:
// _ _ _ _ _ _ _ _
// o_discard = | || || || || || || || |
//-------------------------------------------------------------------------------------
// i_discard = 2’b01:
// _ _ _ _
// o_discard = | || || || |____________
//-------------------------------------------------------------------------------------
// i_discard = 2’b10:
// _ _ _ _
// o_discard = | |_____| |____________________________________| || |
//-------------------------------------------------------------------------------------
// i_discard = 2’b11:
// _ _
// o_discard = | || |_______________________________________________
//--------------------------------------------------------------------------------------
I tried the following code but it doesn’t work. I know the consequent part of the property is wrong. Can anyone please help me resolve this issue?

sequence seq_1;
(i_to_decimate ##1 !i_to_decimate) [*8];
endsequence

property decimate;
@(posedge i_clk) disable iff(i_discard!=0)
 seq_1.triggered |-> $past(o_decimated_sig,1) && $past(o_decimated_sig,2) && $past(o_decimated_sig,3); 
endproperty

sva_test_property: assert property(decimate);
2

In reply to Nandeesh:

Instead of $past, use support logic to store the data you need to analyze. Thus,


// Tune as needed 
bit[0:15] store; 
       always_ff @(posedge i_clk) begin
              store <= {0_discard, store[0:14]};
              
       end
       sequence seq_1;
       (i_to_decimate ##1 !i_to_decimate) [*8];
       endsequence

       ap_00: assert property(@(posedge i_clk) disable iff(i_discard!=0))
       seq_1.triggered && i_discard == 0 |-> store== 16'b0101010101010101); //1,3,5,7,9,11,13,15

// when i_difscard==2'b01, o_discard should be high only at 1,3,9,11th clk cycle. 
       ap_01: assert property(@(posedge i_clk) disable iff(i_discard!=0))
       seq_1.triggered && i_discard == 01 |-> store== 16'b0101000001010000); //1,3,9,11

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.