assertion sequence

Posted 2021-03-24 lybinger

assertion是在pre-poned阶段sample，post-poned阶段evaluation。

##1指的是哥一个clock tick。##0指的是同一个clock tick。##[m:n]指隔m到n各clock，m必须小于n，n如果为$则表示到仿真结束。

a[*3] => a ##1 a ##1 a

a[*0]为空sequence，对于空sequence:

— (empty ##0 seq) does not result in a match
— (seq ##0 empty) does not result in a match
— (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq)
— (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) ‘true)

a[*0:2] ##1 b =>

##1 b

or a ##1 b

or a ##1 a ##1 b

a ##1 b [->2:10] ##1 c 等价于 a ##1 ((!b[*0:$] ##1 b) [*2:10]) ##1 c，即a ##1之后可以有b从0->1的跳变.

a ##1 b [=2:10] ##1 c 等价于a ##1 ((!b [*0:$] ##1 b) [*2:10]) ##1 !b[*0:$] ##1 c，##1 c前面可以有b 1-> 0的跳变。

— $onehot (<expression>) returns true if only one bit of the expression is high.
— $onehot0(<expression>) returns true if at most one bit of the expression is high.
— $isunknown (<expression>) returns true if any bit of the expression is X or Z. This is equivalent to ^<expression> === ’bx.

$sampled()

$rose() 指的是相对前一个clock，当前值得最低位有从0->1得跳变；

$fell() 指的是相对前一个clock，当前值得最低位有从1->0得跳变；

$stable() 指的是相对前一个clock，当前值不变；

$past( expression1 [, number_of_ticks] [, expression2] [, clocking_event]) 获得number_of_ticks（默认值为1）之前的值。如果有expression2的值，则expression2为1时，才获取expression1。

seq1 intersect seq2有点类似seq1 and seq2

exp throughout seq等价于exp [*0:$] intersect seq

seq1 within seq2等价于: (1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2