Hi,
I am having questions regarding pass/failures of multi-threaded sequences in SVA.
In "System verilog Assertions handbook, 4 th edition " chapter 2 on “Understanding sequences” following is description is given : follows :
Multi-threaded sequence in antecedent - for example consider property,
assert property ( ($rose (bus_request) ## [1:2] acknowledge |-> done_data );
which means (($rose (bus_request) ## 1 acknowledge |-> done_data) or ($rose (bus_request) ## 2 acknowledge |-> done_data)). There are two threads in antecedent and single thread in consequent. book says "all the threads must be exercised in search of matched antecedent/consequent pair unless assertion fails. Assertion is considered failed if there is matched antecedent with failed consequent. For assertion to be successful two requirements must be met - There must be no failure in search of matched antecedent with consequent. All the threads of antecedent and consequent must be successful. For non-vacuous pass, there must be at least one matched antecedent with successful non-vacuous property, which represents consequent. There must be no failures in consequent. Some threads may however be vacuous. " Now considering following two scenarios:
Case 1. - Now assuming bus_request is low at clock 1, high at clock2 ( which means $rose(bus_request) will be true at clock 2), acknowledge is true at clock3, acknowledge false at clock4, done data is also true at clock3 and done_data is false at clock4. That would mean the thread 1 matched in antecedent, thread 2 is not successful -(not matched). Since one thread has matched in antecedent, is overall property pass at clock3?.
Case 2 - Now assuming bus_request is low at clock 1, high at clock2 ( which means $rose(bus_request) will be true at clock 2), acknowledge is true at clock3, acknowledge true at clock4, done data is also true at clock3 and done_data is false at clock4. That would mean the thread 1 matched in antecedent, thread 2 also matched in antecedent but did not match in consequent (done data is false at clock4) Since one thread has matched in antecedent, but second thread has not matched in consequent, is the property a failure or success (one thread matching and another thread failed).
I am not clear about the conditions of failure and success for overall sequence and property in this case. It will be a great help if someone clarify these points and elaborate on the conditions of success and failure for :
Multi-threaded sequence in antecedent - singe thread in consequent,
Multi-threaded sequence in antecedent - multi-threaded in consequent,
singe threaded sequence in antecedent - multi-threaded in consequent,
In reply to puranik.sunil@tcs.com: 1. Multi-threaded sequence in antecedent - single thread in consequent,
[Ben] All threads must succeed for property to succeed. A vacuous thread in antecedent produces a vacuously true result for that thread.
a ##[1:2]b |-> c; // is same as
(a ##1 b |-> c) and (a ##2 b |-> c); // property AND statement 2. Multi-threaded sequence in antecedent - multi-threaded in consequent,
[Ben] Almost the same answer, except that there is an implicit first_match() in the consequent.
a ##[1:2]b |-> ##[1:2] c; // is same as
(a ##1b |-> first_match(##[1:2] c)) and (a ##2 b |-> first_match(##[1:2] c));
The first_match() is implicit here, and you do not need to write it 3. singe threaded sequence in antecedent - multi-threaded in consequent,
[Ben] a ##1 b |-> ##[1:2] c; // is same as
(a ##1 b |-> first_match(##[1:2] c))
Again, the first_match() is implicit.
Hi Ben,
thanks for immediate reply. So that means, in case 2, the property is not true and assertion fails. Please confirm.
I have purchased your book “System verilog assertions handbook” 4th edition and have some questions regarding it. Can I write to you on “ben@systemverilog.us” for the queries regarding your book?
rgs,
-sunil
Hi Ben,
thanks for immediate reply. So that means, in case 2, the property is not true and assertion fails. Please confirm.
Yes. As I said in my book, if you have multiple threads in an antecedent, then ALL threads of that property must succeed (true or vacuous success) for the property to succeed.
The 2nd Figure above demonstrates that concept. Section 2.5.1 first_match operator of my book goes into great lengths to explain the use of the first_match operator.
In your example, you should write as follows:
thanks a lot for the detailed reply and explanation with waveforms.
One related question: In section 2.3.2 (page 30) of your book, it says "
"For non-vacuous pass, there must be at least one matched antecedent with successful non-vacuous property, which represents consequent. There must be no failures in consequent. Some threads may however be vacuous. "
I am little confused due to word “at least” above, which seems to imply that even if one thread in antecedent succeeds, property would succeed. This indicates OR relationship rather than AND. Can you please clarify this.
In section 2.3.2 (page 30) of your book, it says "
"For non-vacuous pass, there must be at least one matched antecedent with successful non-vacuous property, which represents consequent. There must be no failures in consequent. Some threads may however be vacuous. "
I am little confused due to word “at least” above, which seems to imply that even if one thread in antecedent succeeds, property would succeed. This indicates OR relationship rather than AND. Can you please clarify this.
On that page 30, see below, I also address that there are two types of successes: **vacuous and nonvacuous.**If all the threads result in a vacuous result, the result of the assertion is vacuous. For non-vacuous success, at none of the treads (antecedent |-> consequent) must fail, and at least one of them suceeds non-vacuously.
$rose(bus_request) ##[1:3] acknowledge |-> ##[1:2] done_data);
Because the antecedent has a range delay, the assertion ap_req_done is equivalent to the following assertion with no range delays:
ap_req_done_equivalnt: assert property(
($rose(bus_request) ##1 acknowledge) or
($rose(bus_request) ##2 acknowledge) or
($rose(bus_request) ##3 acknowledge) |->
(##1 done_data) or (##2 done_data) );
// // which is also equivalent to
ap_req_done_equivalnt: assert property(
(($rose(bus_request) ##1 acknowledge) |-> (##1 done_data) or (##2 done_data)) and
(($rose(bus_request) ##2 acknowledge) |-> (##1 done_data) or (##2 done_data)) and
(($rose(bus_request) ##3 acknowledge) |-> (##1 done_data) or (##2 done_data)) );
// If antecedent ==0, that one property is vacuously "true", and that is a true, though vacuous. Thus,
(vacuous true) and (vacuous true) and (vacuous true) yield a vacuous result
(really true) and (vacuous true) and (vacuous true) yield a true PASS result
(vacuous true) and (false) and (really true) yield a false result
