Hi,
I have doubt on AND operation in assertions. Can somebody explain example no 16.6,section 16.9.6,page no :-404 in LRM IEEE Std 1800-2017. In that example how there is a match on 13th tick for composite sequence?.
Here is the example :-
(te1 ##[1:5] te2) and (te3 ##2 te4 ##2 te5) where te1,te2…etc are Boolean expressions and this sequence is checked on every posedge of clock.
Thank you
sasi kiran
In reply to sasi_8985:
The sequence operator and is used when both operands are expected to match, but the end times of the operand sequences can be different. Each of two sequences starts at the first clocking event of their respective sequence. The composite sequence completes and matches when there is a match in both subsequences, and the longer sequence completes. However, the composite sequence fails to match when any of the subsequences fail to match.
(te1 ##[1:5] te2) and (te3 ##2 te4 ##2 te5)
// Since you have ranges
(te1 ##[1:5] te2) // is equivalent to
(te1 ##1 t2) or (te1 ##2 t2) or (te1 ##3 t2) or (te1 ##4 t2) or (te1 ##5 t2)
te1==1 at cycle 8
te2==1 at cycles 9, 10, 11, 12, 13
//Thus, (te1 ##[1:5] te2) is true in cycles 8,9,10,11,12,13
// (te3 ##2 te4 ##2 te5)
te3==1 at cycle 8
(te3 ##2 te4 // true at cycle 10, 2 cycles later
(te3 ##2 te4 ##2 te5 // true at cycle 12
THUS, te3 ##2 te4 ##2 te5 is true at cycle 12
That satisfies that sequence of the ANding
The other sequence (te1 ##[1:5] te2)is is true in cycles 8 or 9, or 10, or 11, or 12, or 13
When you AND, the ending time is not important (unlike the intersect)
Thus, (te1 ##[1:5] te2) and (te3 ##2 te4 ##2 te5) is true
In cycle 12 or 13. Because of the “or”, you don’t have to wait till t5 to declare success.
However, there are 2 matches, and if used as a antecedent you would need a first_match() since all threads of an antecedent must be tested (see my paper “Understanding the SVA Engine”, link below
(te1 ##[1:5] te2) and (te3 ##2 te4 ##2 te5) |-> d; // 2 matches for waveform in 1800
first_match((te1 ##[1:5] te2) and (te3 ##2 te4 ##2 te5)) |-> d; // 1 match at cycle 12
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
In reply to ben@SystemVerilog.us:
Hi Ben,
Thanks for the reply.
I still didn’t get it.
“The composite sequence completes and matches when there is a match in both subsequences, and the longer sequence completes”. This means when two subsequences match then only whole composite sequence gets matched right?.
see this image :-
Your text to link here…
I am not getting why there is match in 13th clock for composite sequence even there is no match in one of the subsequence.
Thank you
sasi kiran
In reply to sasi_8985:
(te1 ##[1:5] te2) and (te3 ##2 te4 ##2 te5)
// same as
((te1 ##1 t2) or (te1 ##2 t2) or (te1 ##3 t2) or (te1 ##4 t2) or (te1 ##5 t2)) and
te3 ##2 te4 ##2 te5);
// same as
((te1 ##1 t2) and (te3 ##2 te4 ##2 te5)) or // in evaluation at t9
((te1 ##2 t2) and (te3 ##2 te4 ##2 te5)) or // in evaluation at 10
((te1 ##3 t2) and (te3 ##2 te4 ##2 te5)) or // in evaluation at t11
((te1 ##4 t2) and (te3 ##2 te4 ##2 te5)) or // PASS testcase at t12, PASSED @t12 because
// (te1 ##4 t2) is a match at t12 and (te3 ##2 te4 ##2 te5) completed and is a match at t12
((te1 ##5 t2) and (te3 ##2 te4 ##2 te5); // PASS testcase at t13, PASSED @t13 because
// (te1 ##5 t2) is a match at t13 and (te3 ##2 te4 ##2 te5) was a match at t12
// and was completed
// In other words, for any ANDing of 2 sequences of different lengths,
// The ANDing is a match (or PASS) is from the start of the evaluation
// sequence1 completes at some point in time AND
// sequence2 completes at some point in time.
// Those completion cycle times need not be identical.
((te1 ##1 t2) or (te1 ##2 t2) or (te1 ##3 t2) or (te1 ##4 t2) or (te1 ##5 t2)) and
te3 ##2 te4 ##2 te5);
// represents the ORing of 5 separate sequences, with each one having an AND operation.
// BTW, I used the colloquial PASS for a sequence, but when you talk about sequences
// you should refer to matches or no matches. Properties are true or false,
// assertions PASS or FAIL.
//
// If you wrote
(te1 ##[1:5] te2) intersect (te3 ##2 te4 ##2 te5)
// then the following sequence in the ORing is the only one that matches
((te1 ##4 t2) and (te3 ##2 te4 ##2 te5)) // PASS testcase at t12,
Let me add an analogy.
You can say 1) I’ll save $1M and I’ll buy a house and pay for it.
Either of these 2 sequences need not be completed at the same instant of time,
but the statement is true when both conditions are true.
After you save the $1M, it may take you a while to find a house you like.
If you say 2) the instant I have $1M I’ll pay for my house.
That is the intersect. Getting the $1M may take a while, and so does escrow for the payment. Escrow closes the moment you submit the check for the $1M.
In reply to ben@SystemVerilog.us:
// Note that you have 5 threads in this example, and four of them
// match at t12. The fifth thread matches at t13. (RHS::= Righ Hand Sequence)
((te1 ##1 t2) and (te3 ##2 te4 ##2 te5)) or // Q1: RHS matches @t9, LHS in evaluation
((te1 ##2 t2) and (te3 ##2 te4 ##2 te5)) or // Q2: RHS matches @t10, LHS in evaluation
((te1 ##3 t2) and (te3 ##2 te4 ##2 te5)) or // Q3: RHS matches @t11, LHS in evaluation
((te1 ##4 t2) and (te3 ##2 te4 ##2 te5)) or // Q4: RHS matches @t12, LHS matches @t12
// Threads Q1, Q2, Q3, Q4 all match at t12
((te1 ##5 t2) and (te3 ##2 te4 ##2 te5); // Q5: RHS matches @t13, LHS matched @t12
In an assertion with this ANDing sequence as an antecedent, all threads with their corresponding consequent must be tested.