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)
?
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)
?
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.
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