“Signal a is low, before next time signal a is asserted signal b may only rise for one clock cycle”
I know it can be easily tested with auxiliary code but I want to use just SVA to test it.
I was able to test for when b is high for only one clock cycle but the assertion fails if b is never asserted before next a.
1) b[=1] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$]
2) thus, ( ((b[=1]) ##1 !b[*0:$]) is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 !b[*0:$]); also equivalent to
b[=1]
3) !a |=> ( ((b[=1]) ##1 !b[*0:$]) or (!b[*0:$]) ) intersect (!a[*0:$] ##1 a) ; // equivalent to
!a |=> ( b[=1] or (!b[*0:$]) ) intersect (!a[*0:$] ##1 a) ; // equivalent to
// b[=1] or (!b[*0:$] says an accurrance of b or no occurrence of b
// basically true at all cycles, like 1[*0:$]
4) !a |=> ( (1[*0:$]) ) intersect (!a[*0:$] ##1 a) // equivalent to
!a |=> a[->1] // equivalent to
$rose(a) |-> 1
Essentially,
!a |=> ( ((b[=1]) ##1 !b[*0:$]) or (!b[*0:$]) ) intersect (!a[*0:$] ##1 a) ;
gets reduced to
$rose(a)
requirements: “Signal a is low, before next time signal a is asserted signal b may only rise for one clock cycle”