#SVA语法滴水穿石# (014)关于链式蕴含的陷阱
前面介绍了蕴含和 非蕴含操作符,#SVA语法滴水穿石# (001)关于 |-> 和 |=>
本以为两个小小的操作符,能有什么难度,知道大概意思,就算是掌握了,太过于骄傲了,今天,将最近遇到的陷阱,和大家分享一下。
1. 问题背景
假设,有下面一组握手信号。
目的:当req 上升之后,若干clk ack 上升,ack 上升后若干clk state 信号上升; state 信号上升之后,持续一个clk 后,req/ack/state 三个信号同时拉低。
随手写了下面一段断言语句:
property req_ack_handshake_1 ;
@(posedge clk)
$rose(req) |-> ##[1:$] $rose(ack) |-> ##[*] $rose(state) |-> ##1 ($fell(state) and $fell(req) and $fell(ack) ) ;
endpropertyassert property (req_ack_handshake_1) ;
仿真结果:始终显示incomplete 状态。