如何防止SVA的新线程

Question

假设我的设计中有一个按钮。当按钮被按下三次时，我想在接下来的两个时钟之间增加计数器，我想用 SVA 检查这个行为。我写了这个：

`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

这在第一次按下三下时效果很好，但之后它总是会抛出断言错误，因为它在每次按下按钮时都会启动新的断言线程。所以，我需要防止测试平台这样做。当重复已经开始时，我不需要开始新线程。
我该怎么做？

Answer 1

我不确定我完全理解你的问题。先说说我的理解，以及我认为你的问题出在哪里。如果我弄错了，请道歉。

您打算在 button_n ("presses") 上检测负数，并且在第三个上，您增加 "counter".

这里的问题是您声明的 objective（实际上与 SVA 匹配）和您的设计做了不同的事情。

您的 SVA 将在每三次否定后检查计数器是否具有预期值 1-3 个周期。这适用于按下 0、1 和 2。但它也必须适用于按下 1、2 和 3。然后按下 2、3 和 4 等。我怀疑断言在按下 2 时通过，然后在按下 3 时失败。即你检查在第三次之后每次按下你的计数器。

另一方面，您的设计有所不同。它计数 3 个否定，递增计数器，然后从头开始计数。

我建议不要在断言中使用局部变量，除非您确定它是您需要的——我认为这里不是这种情况。您可以在 key_press_count == 3 上设置 SVA 触发器（假设您适当地定义了 key_press_count 而不是自动变量）。

如果您坚持使用本地 SVA 变量，您可以稍微修改触发条件以包含计数器。例如一些类似的东西（虽然可能有点错误，还没有测试过）： (counter == 0 || $changed(counter)) ##1 ($fell(button_n)[=3], val = counter)

IMO，这是个坏主意，支持 RTL 是更好的方式来记录您的意图，并准确检查您所追求的行为。

希望对您有所帮助

如何防止SVA的新线程

How to prevent new threads of SVA

system-verilog

verification

system-verilog-assertions