Systemverilog断言信号为真，在仿真过程中至少发生了1次

Question

我在试图写这个断言时遇到了一个问题。我试图断言，信号B必须在信号A为真之后至少出现1次。

我所写的断言如下：

example  : assert property(
       @(posedge clk) disable iff(reset)
       A |-> ##[0:$] B[->1]) else `uvm_error(....)

问题是，如果在仿真信号B为真之后，A不再为真，那么uvm_error就不会执行。我期望它被执行，并且模拟报告了这个消息：

example: started at xxxxxxps not finished

这一断言似乎还没有完成，甚至连仿真结果都没有结束。

我在google上看过，有一个类似的问题：Assertion to check for the toggle (0->1) of a signal

我也尝试过使用strong()操作，这也没有帮助。

如何解决这个问题？

Answer 1

不幸的是，您的解决方案取决于您正在使用的模拟器。我试了四次，每一次都有不同的行为。

我认为你的解决办法是：

  example3  : assert property(
       @(posedge clk) disable iff(reset)
    A |-> s_eventually B)
    else 
      $error("%t - Assertion example3 failed", $time);

在此基础上，设计了两台模拟器，并对SVA进行了理解。在一个模拟器上，实际执行动作块中的$error语句，并显示消息"Assertion example3 failed“；在另一个模拟器中，显示一个通用错误消息。

s_代表“强大”。断言意味着B必须发生在模拟结束之前的某个时间。

这是一个MCVE。如果你包括这样的内容，你的问题会更容易回答。

module M;

  bit stop;  bit clk; initial while (!stop) #5 clk = ~clk;

  bit A, B;

  initial begin
    #20 A = 1;
    #10 A = 0;
    // #10 B = 1;
    #10 B = 0;
    #50 stop = 1;
  end

  example1  : assert property(
       @(posedge clk)
    A |-> B[->1]) 
    else 
      $error("%t - Assertion example1 failed", $time);

  example2  : assert property(
       @(posedge clk)
    A |-> eventually [0:7] B)
    else 
      $error("%t - Assertion example2 failed", $time);

  example3  : assert property(
       @(posedge clk)
    A |-> s_eventually B)
    else 
      $error("%t - Assertion example3 failed", $time);

   final
     $display("Finished!");

endmodule

https://www.edaplayground.com/x/2RtF