Assertion to check signal change only once(1->0->1) between 2 events

SystemVerilog
,
6

In reply to mlsxdx:

 //if the rising edge of e may or may not overlap with rising edge of b, 
// the following  allows that 
 $rose(s) |-> (##1 $fell(b)[->1] ##1 b[=1]) intersect e[->1];
// But 
  $rose(s) |-> (##1 $fell(b)[->1] ##1 b[=1] ##[0:$] !b) intersect e[->1];
// will not allow b==1 in the same cycle as e==1  

(##1 $fell(b)[->1] ##1 b[=1] ##[0:$] !b) // is same as 
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0:$] ##[0] !b) // same as 
  (##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##[1] !b) or 
  (##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##[2] !b)  or 
  ...
This gets simplified to 
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0:$] ##[0] !b) // null 
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b) or 
(##1 $fell(b)[->1] ##1 b[->1] ##1 ##1 !b)  or 
..

You can just use the following if b and e cannot be in the same cycle
(##1 $fell(b)[->1] ##1 b[=1] ##1 !b) intersect e[->1];
// same as 
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0:$] ##1 !b); // same as
  (##1 $fell(b)[->1] ##1 b[->1] ##1 !b) or 
  (##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*1:$] ##1 !b)