How to prevent new threads of SVA

Question

Lets assume, I have a button in my design. I want to increment counter between next two clock when button has been pressed three times and I want to check this behaviour with SVA. I have wrote this one:

`timescale 1ns / 1ps
module tb();

parameter NUMBER_OF_PRESSES = 10;
parameter CLK_SEMI_PERIOD = 5;

bit clk;
always #CLK_SEMI_PERIOD clk = ~clk;

bit button_n;
bit reset_n;
logic [7:0] counter;

property p;
  logic[7:0] val;
  disable iff(!reset_n) @(posedge clk) (($fell(button_n)[=3]),val=counter) |=> ##[0:2] (counter== val+1);
endproperty
assert property(p);



initial begin
    automatic bit key_d;
    automatic byte key_lat;
    automatic byte key_press_count;
    reset_n = 1;
    button_n = 1;
    counter = 0;
    fork
        begin
            repeat(NUMBER_OF_PRESSES) begin
                repeat(5)begin
                    @(negedge clk);
                end
                button_n = 0;
                key_lat = $urandom_range(1,4);
                repeat(key_lat) begin
                    @(negedge clk);
                end
                button_n = 1;
            end
        end
        begin
            forever begin
                @(posedge clk);
                if(!button_n && key_d) begin
                    key_press_count++;
                end
                if(key_press_count == 3) begin
                    counter++;
                    key_press_count = 0;
                end
                key_d = button_n;
            end
        end
    join_any
end

endmodule

This works good at first three press, but then it will always throw assertion error, because it has been started new thread of assertion at each button press. So, I need to prevent testbench from doing this. When repetitition has been started I don't need to start new threads.
How can I do this?

Answer 1

I am not confident I fully understand your question. Let me first state my understanding and where I think your problem is. Apologise if I am mistaken.

You intend to detect negedges on button_n ("presses"), and on the third one, you increment "counter".

The problem here is that your stated objective (which actually matches the SVA) and your design do different things.

Your SVA will check that the counter has the expected value 1-3 cycles after every third negedge. This holds for press 0, 1 and 2. But it must also hold for press 1, 2 and 3. And press 2, 3 and 4 etc. I suspect the assertion passes on press 2 and then fails on press 3. I.e. you check that you increment your counter on every press after the third.

Your design, on the other hand does something different. It counts 3 negedges, increments counter, and it then starts counting from scratch.

I would advise against the use of local variables in assertions unless you are certain that it is what you need - I don't think this is the case here. You can have your SVA trigger on key_press_count == 3 (assuming you ofc define key_press_count appropriately and not as an automatic var).

If you insist on using your local SVA variable you can slightly modify your trigger condition to include counter. For example something along the lines of (though may be slightly wrong, have not tested): (counter == 0 || $changed(counter)) ##1 ($fell(button_n)[=3], val = counter)

IMO that's a bad idea and having supporting RTL is the better way to go here to document your intention as well as check exactly the behaviour you are after.

Hope this helps