具有抢先启动的 SystemVerilog 断言 (SVA) 含义

Question

我是 SVA 的新手。我对 SVA 的含义有疑问。

1: sequence s1;
2:   start ##[1:$] !start;
3: endsequence: s1
4:
5: sequence s2;
6:   ready && (!start);
7: endsequence: s2;
8: 
9: assert_ready: assert property (@(posedge clk) s1 |-> ##5 s2);

这个断言的目的是检查时间属性：

当'start'切换时，'ready'在5个时钟周期后被激活。
但是，当有抢先 'start'，即在 'ready' 被激活之前另一个 'start' 切换，这个时间属性应该被重置并且 'ready' 应该静音。

我试图通过使用形式验证工具 Synopsys 的 VC formal 来验证这个属性。它表明此断言失败，因为当优先 'start' 发生时 s2 序列为零。

我想我在第6行的描述有误，这是一个真正的新手代码。您能否让我知道如何正确描述抢先启动的断言？

Answer 1

我想你想要

sequence s1;
   start ##1 !start [*5]
endsequence: s1
sequence s2;
  ready;
endsequence: s2;

assert_ready: assert property (@(posedge clk) s1 |->  s2);

尽管您可能需要根据您对第 5 个周期 start 与 ready 重合时发生的情况的要求进行调整。

具有抢先启动的 SystemVerilog 断言 (SVA) 含义

SystemVerilog Assertion (SVA) Implication with Preemtive Start

verilog

system-verilog

assertion

system-verilog-assertions