system-verilog-assertions - 这两个断言有什么区别？

Question

假设我有两个属性；

property p1;
sig_a ##1 sig_b;
endproperty

property p2;
sig_a |=> sig_b;
endproperty

现在，如果我这样断言：

a1: assert property (p1);
a2: assert property (p2);

a1 和 a2 有什么区别吗？

Answer 1

propertysystem_verilog和sequence语法 之间存在差异。property p1没有触发条件。换句话说，它将始终在时钟事件上进行检查。它只是提到要检查的操作顺序。即sequence在 sv 断言中。您可以按以下方式假设property p1。

property p1;
  1'b1 |-> sig_a ##1 sig_b;
endproperty

如果 sig_a 为零值，它将始终失败。

现在property p2有触发条件，即 sig_a == non_zero 值。如果此条件为真，那么它将在 1 个时钟事件后评估 sig_b 值。