如何防止 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 上的 negedges（“presses”），并在第三个上增加“counter”。

这里的问题是你声明的目标（实际上与 SVA 相匹配）和你的设计做不同的事情。

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

另一方面，你的设计做了一些不同的事情。它计数 3 个 needges，递增 counter，然后从头开始计数。

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

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

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

希望对你有帮助