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

SystemVerilog
,
7

In reply to ben@SystemVerilog.us:

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)

Sorry for my confusion. I just got the part you explain earlier.
Therefore, the property can handle b, e overlap case
$rose(s) |-> (##1 $fell(b)[->1] ##1 b[=1]) intersect e[->1];

But if b, e requires non-overlap, then
(##1 $fell(b)[->1] ##1 b[=1] ##1 !b) intersect e[->1];

I was confused on the 4 combination among b[=1] within, b[=1] intersect, b[->1] within, b[->1] intersect. Let me summarize them and put 4 property together and bring my questions back.