admin管理员组

文章数量:1530012

我们经常会碰到一个验证以下场景的需求：

一个信号在仿真结束前应该至少拉高过一次或者只拉高一次，比如一个简单的握手协议要求ready每拉高一次就要收到一个acknowledge信号。

如果acknowledge需等待的cycle数不确定，我们在构造断言时会自然而然的想到##[1:$]这类写法，如：

property p_handshake_check;
  always @ (posedge clk) rdy |-> ##[1:$] acpt ##1 !acpt;
endproperty

a_handshake_check: assert property(p_handshake_check);

但是##[1:$]这样的写法会影响仿真效率，为什么呢？因为这样写法可以分解为无数个并行check的进程, 以如下sequence为例

$rose(a) |-> b[*1:8000] ##1 c ##1 d

可以分解为8000个并行的进程：

$rose(a) |-> b[*1] ##1 c ##1 d
$rose(a) |-> b[*2] ##1 c ##1 d
$rose(a) |-> b[*3] ##1 c ##1 d
...
$rose(a) |-> b[*8000] ##1 c ##1 d

那么##[1:$]就意味着断言触发后的每个cycle都要做这个check, 会极大的影响仿真效率。

如果我们想实现##[1:$]功能，但不想影响仿真效率或者在查找到一次目标信号后就想让assertion check停掉该怎么实现呢：

  1. 用go to (->)语法

将上面的property写法

property p_handshake_check;
  always @ (posedge clk) rdy |-> ##[1:$] ##1 !acpt;
endproperty

改成

property p_handshake_check;
  always @ (posedge clk) rdy |-> acpt[->1] ##1 !acpt;
endproperty

2.用s_eventually 和$assertoff结合

s_eventually是增强型eventually, s_意为strong, s_eventually(a)等效于strong (##[*0: ] a ) , 当查找到一次 a c p t 后用 ] a), 当查找到一次acpt后用 ]a),当查找到一次acpt后用assertoff中止

property p_handshake_check;
  always @ (posedge clk) rdy |-> s_eventually(acpt) ##1 !acpt;
endproperty

a_handshake_check: assert property(p_handshake_check) $assertoff(0, a_handshake_check);

本文标签： 断言场景条件结束测试

版权声明：本文标题：【验证-SVA】怎样通过断言测试“直到仿真结束,一个条件被满足过“这种场景（关于s_eventually, [0:$]） 内容由热心网友自发贡献，该文观点仅代表作者本人， 转载请联系作者并注明出处：https://m.elefans.com/dianzi/1726654305a1080073.html， 本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌抄袭侵权/违法违规的内容，一经查实，本站将立刻删除。