Assertion for a before b condition

SystemVerilog
1

Hi,

I came across an assertion for “a before b” as:

@(posedge clk)
     (not (##[0:$] b)) or (!b[*0:$] ##1 (a && !b));

What is the significance of not (##[0:$] b)?

2

Significance of (not (##[0:$] b))
This is a property that says

(not (##[0:$] b)) // same as 
not(b or ##1 b or .. ##n b).  
// I do not see its application here. 
// I prefer the following using the intersect 
// some would prefer the until operator. It is clearer to me.
// a before b -- no "b" until "a" then one "b"
// no b followed by 1 cycle is of same length as 
// one occurrence of b
  assert property(@(posedge clk)
   c|-> ((!b[*1:$] ##1 1) intersect a[->1]) ##0 b[->1]);

  // a before b -- no "b" until "a" then one "b" and no "a" 
   assert property(@(posedge clk)
   c|-> ((!b[*1:$] ##1 1) intersect a[->1]) ##0 
        (b[->1] intersect !a[*1:$]) );

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

3

NOTE: 1) The Intersect is a length-matching sequence conjunction. It gives you lots of flexibility in defining when seq1 matches seq2. After that match, you can follow this with another sequence.
2) The until is a property expression.
property_expr until property_expr
| property_expr s_until property_expr
| property_expr until_with property_expr
| property_expr s_until_with property_expr
It cannot be followed by a sequence.
In my aging mind, with the “until” I always have to go thru an internal mental jingling to fully understand what it is doing for my assertion.
3) See my paper on this topic:
Reflections on Users’ Experiences with SVA, part 2

Addresses the usage of these four relationship operators: throughout, until, intersect, implies