1

我有一个 SV 断言，它检查如下属性

propert my_property;
@(posedge clk) disable iff(reset) $rose(halt) ##0 ((rx_prio) > (expec_prio)) ##[0:$] $rose(rdy) |-> ##[1:100] (my_prio[rx_prio]==1'b1);
endproperty:my_property

我有如下断言：

MY_PROPERTY_CHECK:assert property (my_propert)
else
$error;

在这里，场景是，前件为真，后件在 1 到 100 个时钟周期之间进行检查。在先行之后，由于时钟门控，时钟停止了一段时间，然后时钟再次开始滴答作响。信号my_prio[rx_prio]在时钟门控之后但在 100 个时钟周期内再次置位。但我仍然得到断言失败。

无法弄清楚失败的问题。断言检查之间的时钟门控是否有问题？还是其他原因失败？谢谢。

4

2 回答 2

2

可能有很多线程正在启​​动。尝试在下面的显示语句中使用局部变量。参见IEEE Std 1800-2012 § 16.10局部变量

propert my_property;
  static int prop_cnt=0; // shared
  local  int prop_id; // Note: some require the "local", other need it omitted
  @(posedge clk) disable iff(reset) 
    ($rose(halt) ##0 ((rx_prio) > (expec_prio)),
        prop_id=prop_cnt++,
        $display("Spawn prop_id:%0d prop_cnt:%0d @ %0t %m",
                   prop_id,prop_cnt,$time) )
    ##[0:$] ($rose(rdy),
        $display("Trigger prop_id:%0d prop_cnt:%0d @ %0t %m",
                     prop_id,prop_cnt,$time) )
    |-> ##[1:100] (my_prio[rx_prio]==1'b1,
        $display("Pass prop_id:%0d prop_cnt:%0d @ %0t %m",
                     prop_id,prop_cnt,$time) );
endproperty : my_property

如果您看到 Spawn-Spawn-Trigger 或 Spawn-Trigger-Trigger，我们超出预期的任何内容（即 Spawn-Triger-Pass），那么就会出现意外线程。

如果是这种情况，请查看IEEE Std 1800-2012 § 16.9.8 First_match 操作 

first_match(
    $rose(halt) ##0 ((rx_prio) > (expec_prio)) ##[0:$] $rose(rdy),
      $display("Spawn-Trigger prop_id:%0d prop_cnt:%0d @ %0t %m",
                   prop_id,prop_cnt,$time)

) |-> // ...

或§ 16.9.10序列包含在另一个序列中

(
    ( $rose(halt) ##0 ((rx_prio) > (expec_prio)) ) within $rose(rdy)[->1],
      $display("Spawn-Trigger prop_id:%0d prop_cnt:%0d @ %0t %m",
                   prop_id,prop_cnt,$time)
) |-> // ...

您可能想要sequence为触发器创建一个。

于 2014-03-04T23:24:41.827 回答
0

由于我不知道您的设置，我可以假设您可能正在触发未门控的层次结构更上层的时钟，但是您在时钟被门控的确切层次结构中调试波。

如果您正在为无法用断言改造的 RTL 块编写断言（它是 VHDL/Verilog 或者您不允许触摸文件），请使用 bind 在该块内实例化您的断言：http://www.asic- world.com/systemverilog/assertions22.html

于 2014-03-04T11:16:20.453 回答