I am trying to understand the basics of “or” construct and have following Code :: EDA_LINK
The antecedent is ::
a[ *1:2 ] ##1 b is equivalent to ( a ## 1 b ) or ( a ##1 a ##1 b )
As a result the resultant expression is :: ( ( a ## 1 b ) or ( a ##1 a ##1 b ) ) |-> c ;
I am confused why does the 1st assertion Pass at TIME : 500 instead of TIME : 400
Let's assume ( a ## 1 b ) is Thread 1 and ( a ##1 a ##1 b ) is Thread2
At TIME : 300 , ' a ' is True hence both Threads start evaluation .
As ' b ' is True at TIME : 400 , Thread1 succeeds .
However as ' c ' is also True at TIME : 400 , why doesn't the assertion Pass at TIME : 400 ?
As per :: seq1 or seq2 , match occurs whenever either of the 2 sequences complete .
So I expected Pass at TIME : 400 as Thread1 was successful
i.e antecedent was a match and then the consequent ' c ' was True at TIME : 400 too .
Thread2 succeeds at TIME : 500 ( as expected ) and the assertion passes at TIME : 500 .
NOTE :: Using first_match in antecedent makes the assertion Pass at TIME : 400 as per expectation .
If a multi-threaded sequence is used in an antecedent (e.g., a ##1 b[*1:3] ##1 c |-> d), then all threads must be tested with its consequent for the assertion to terminate as successful.
In reply to hisingh:
then all threads must be tested with its consequent for the assertion to terminate as successful.
Could you please elaborate on this ?
I am having a hard time of making sense of it logically .
For the Attempt1 at TIME : 300 , the “or” construct is behaving as “and” construct as it waits for longer sequence ( a ##1 a ##1 b |-> c ) to complete .
In the 2 paths possible ( Path1 :: Thread1 |-> c and Path2 :: Thread2 |-> c )
why is taking the longer path instead of the shorter one ?
a[*1:2] ##1 b |-> c; // is equivalent to
(a ##1 b ) or (a ##1 a ##1 b) |-> c; // also equivalent to
((a ##1 b ) |-> c) and ((a ##1 a ##1 b) |-> c);
Thread1 |-> c and Thread2 |-> c; // YES
At each clocking event the two threads start at the same time.
All threads of the antecedent must be tested.
An antecedent thread can be a no-match (yielding vacuity “true vacuously” for that thread)
For an assertion to PASS, there can be no failure in any of the attempted threads.
For a nonvacuous PASS, at least one of the threads in nonvacuous.
I have a better understanding of the Question I posted at the top and understand the O/P
However if I do a slight modification to the Sequence Expression .
sequence ant_seq ;
// Attached a Subroutine within an expression in a ' sequence '
( ( a[ *1:2 ] ##1 b ) , $display(" TIME : %0t Antecedent is True " , $time ) ) ;
endsequence
[ Q ] When does the $display() execute ?
**How do I expand the above expression ::**
Would it be interpreted as ::
( ( a ##1 b ) , $display(" TIME : %0t Antecedent is True " , $time ) ) or
( ( a ##1 a ##1 b ) , $display(" TIME : %0t Antecedent is True " , $time ) )
[Ben] What you have is (sequence_expr {, sequence_match_item})
The sequence_match_item} is executed if the endpoint of sequence_expr is a match
How do I expand the above expression ::
Would it be interpreted as ::
( ( a ##1 b ) , $display(" TIME : %0t Antecedent is True " , $time ) ) or
( ( a ##1 a ##1 b ) , $display(" TIME : %0t Antecedent is True " , $time ) )
Because you are running the property ab twice, once in the assertion and the other in the cover. You don’t need the cover. If you comment it out you get
a_property : assert property ( ab ) else $display(" TIME : %0t AB FAIL " , $time , ) ;
// c_property : cover property ( ab ) $display(" TIME : %0t AB PASS " , $time ) ;
TIME : 400 Antecedent is True
# TIME : 500 Antecedent is True
# TIME : 500 Antecedent is True
# TIME : 700 AB FAIL