Local variable assignment in Multithread consequent

Hi,
I was trying a code where the consequent is multi-threaded : edalink
The local variable ‘local_data’ is assigned whenever sequence ‘rdC’ is True .
Since the consequent is multithreaded I observe that there are 3 dynamic variable ‘local_data’ assignment .
(1) For +define+P_F_F :

There is ONLY 1 PASS/FAIL report and that is only for success of the 1st thread that completes in the consequent at T:85

So the question arises why don’t I observe failure report for last 2 threads at T:95 and T:105 ?
Is it because there is an implicit first_match for the consequent ? Thereby there would be only 1 PASS/FAIL report for the 1st thread that completes

(2) For +define+F_P_P :

Using same logic as (1), I expected as the 1st thread fails at T:85 there would be a failure report at T:85 and No Pass reports at T:95 and 105.
However,I observe pass report at T:85 , why is it so ?

In reply to MICRO_91:
Your property is expanded to


property p_check; 
       int  local_data;
       RdWr |-> 
             ##[1:5] (rdDone, local_data = rData) ##5  
             wData == local_data + 'hFF; 
       endproperty 
// As you expressed, it is multithreaded; thus you have the consequent as 
(##1(rdDone, local_data = rData) ##5 wData == local_data + 'hFF) or 
(##2(rdDone, local_data = rData) ##5 wData == local_data + 'hFF) or 
(##3(rdDone, local_data = rData) ##5 wData == local_data + 'hFF) or 
(##4(rdDone, local_data = rData) ##5 wData == local_data + 'hFF) or 
(##5(rdDone, local_data = rData) ##5 wData == local_data + 'hFF)  

The success of any one thread concludes the assertion.
A failure would occur if none of the ORed thread are a match (BTW, sequences match or do not match; properties are true or false; assertions pass or fail)

Comments on your style:

  • Reduce the number of parentheses, use only what is really needed; it makes the code hard to read.
  • You have too many unneeded character and line spaces.
  • You have too many sequence declarations that are not really needed.

I recommend that you read my paper on Underdatandin the SVA Engine.

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

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

In reply to ben@SystemVerilog.us:

Thanks Ben,
I missed out on the time of pass report for the 2nd case. It occurs at T:95 ( when the 2nd thread completes ) rather than T:85

The code was from a book I am referring to currently.For debug purposes I added $display as part of sequence_match_item

In reply to ben@SystemVerilog.us:

Ben,
A follow-up question. I made some changes to the code such that the antecedent is multi-threaded : edalink2

EDIT: Added changes to the code such that rdDone is 0 from T:34 to end of simulation.
( Previously rdDone was true from T:34 to end of simulation )

The expectation is that since sequence: ##5( wData == ( local_data + 'hFF ) ) is True at T:85 and T:105 , I expected the assertion to pass twice.
Once at T:85 and other at T:105 , however I observe that assertion passes only once at T:105.
Any suggestions on why is it so ?

In reply to MICRO_91:

Fig9_1_Part2(1) - EDA Playground code
EPWave Waveform Viewer wave
ap_test: assert property( dataCheck |-> 1 ) pass=pass+1; else fail=fail+1;
I don’t see a pass.
Anyway, do more test using waveform traces, as I did. FOR
multithreaded_antecedent |-> 1;
All threads have to first be tested before you get a PASS,
Otherwise, there could be another thread that fails.
A thread is ANTECEDENT followed by the consequent thread
FOr a pass, each thread must pass (vacuously or nonvacuously).
Nonvacuous pass for the assertion if no thread fails and at least one threat passes nonvacuously.

In reply to ben@SystemVerilog.us:

All threads have to first be tested before you get a PASS,

Thanks Ben ,
With the multi-threaded antecedent for the assertion to pass :
each thread must have either a non-vacuous pass or vacuous pass , without any thread failing
i.e if antecedent has non-vacuous pass then the consequent must have a match else the assertion fails.

Have added changes to the code with pass and fail counter: edalink2
What should be the pass count at end of simulation ? I observe different results across tools.

In reply to MICRO_91:

i.e if antecedent has non-vacuous pass then the consequent must have a match else the assertion fails.

Correct

Have added changes to the code with pass and fail counter: edalink2
What should be the pass count at end of simulation ? I observe different results across tools.

The question is:
In a multithreaded antecedent, when should the pass action block be called?
Upon each pass or at the end of all threads?
[Ben] EPWave Waveform Viewer wave
Fig9_1_Part2(1) - EDA Playground code
I added a “go” to restrict the model to one successful attempt

    sequence dataCheck ;
      int  local_data;
      ( $rose(go) ##[1:5] rdDone,local_data = rData )  ##5 ( ( wData == (local_data) ) ); //$display("T: %3t  wData == %0d ",$time , wData ) ); 
    endsequence
  
  function void count(); at_end=at_end+1; endfunction
  ap_test: assert property(  dataCheck  |->  (1, count())  ) 
    begin pass=pass+1; $display("T: %3t  Assertion  PASS " , $time );  end
    else begin fail=fail+1; $display("T: %3t  Assertion  FAILS " , $time ); end

The action block of the assertion occurs when the assertion passes or fails.
As I said before, for a pass you need to test each thread of the antecedent with its consequent. The pass of one thread is NOT a pass of the assertion; you need them ALL.
Here we have 5 threads with 2 of them being nonvacuous pass.
The action pass block is fired once at the end of the last thread (antecedent then consequent).

I strongly suggest that you read my paper Understanding the SVA Engine as it explains treads and attempts.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

In reply to ben@SystemVerilog.us:

The question is:
In a multithreaded antecedent, when should the pass action block be called?

I believe the pass action block should execute if all threads in an attempt have atleast one non-vacuous pass with no thread failing.

Using the same approach I documented the threads for each attempt ( NVP is Non-vacuous pass , VP is Vacuous pass ) : All_Attempts
(1) For 1st attempt at T:5 , there are 5 threads T1 to T5 . T1 and T2 have vacuous pass as ‘rdDone’ is false at T:15 and T:25 respectively.

So 1st attempt at T:5 results in no thread failing. Last thread with NVP is at T:105.
Hence assertion pass action block should execute at T:105

(2) For 2nd attempt at T:15 , there are 5 threads T1 to T5. T1 and T5 have vacuous pass as ‘rdDone’ is false at T:25 and T:65 respectively.

So 2nd attempt at T:15 results in no thread failing. Last thread with NVP is at T:105.
Hence assertion pass action block should execute at T:105

(3) For 3rd attempt at T:25 , there are 5 threads T1 to T5. T4 and T5 have vacuous pass as ‘rdDone’ is false at T:65 and T:75 respectively.

So 3rd attempt at T:25 results in no thread failing. Last thread with NVP is at T:105.
Hence assertion pass action block should execute at T:105

(4) For 4th attempt at T:35 , there are 5 threads T1 to T5. T3 to T5 have vacuous pass as ‘rdDone’ is false

So 4th attempt at T:35 results in no thread failing. Last thread with NVP is at T:105.
Hence assertion pass action block should execute at T:105

(5) For 5th attempt at T:45 , there are 5 threads T1 to T5. T2 to T5 have vacuous pass as ‘rdDone’ is false

So 5th attempt at T:45 results in no thread failing. Last thread with NVP is at T:105.
Hence assertion pass action block should execute at T:105

(6) Other attempts have all vacuous pass as ‘rdDone’ is sampled false for each thread.

Therefore the pass action block should execute 5 times

I added a “go” to restrict the model to one successful attempt

I later tried using: first_match

I observe different output across tools.
Using first_match, assertion should pass as soon as the 1st thread of an attempt is successful.

So using:All_Attempts, ideally shouldn’t the output be :
T: 85 Assertion PASS
T: 85 Assertion PASS
T: 85 Assertion PASS
T: 105 Assertion PASS
T: 105 Assertion PASS

Please correct me if wrong.

Thanks

In reply to MICRO_91:
Hopefully, your reply was to my reply with
EPWave Waveform Viewer wave
Fig9_1_Part2(1) - EDA Playground code
I added a “go” to restrict the model to one successful attempt

    sequence dataCheck ;
      int  local_data;
      ( $rose(go) ##[1:5] rdDone,local_data = rData )  ##5 ( ( wData == (local_data) ) ); //$display("T: %3t  wData == %0d ",$time , wData ) ); 
    endsequence
 
  function void count(); at_end=at_end+1; endfunction
  ap_test: assert property(  dataCheck  |->  (1, count())  ) 
    begin pass=pass+1; $display("T: %3t  Assertion  PASS " , $time );  end
    else begin fail=fail+1; $display("T: %3t  Assertion  FAILS " , $time ); end

Q: When does a sim tool fire the action block for a pass or a fail?

  • An assertion evaluation for each attempt can either PASS or FAIL
  • There NO some pass but other fail
  • A PASS can be vacuous or nonvacuous
  • Verification tools provide various options and switches to control how assertions are handled during simulation, including suppressing vacuous assertion passes.
  • If you wish, you can change the default switch of not executing the vacuous pass action block. However, because vacuous passes have no value or interest, users prefer the default.
    Edaplayground is set to not execute the action block for a vacuous pass.
  • A vacuous pass occurs in the cycle in which the evaluation of vacuity exists; that could be in at its attempt or within a thread.> So 1st attempt at T:5 results in no thread failing. Last thread with NVP is at T:105.
    Hence assertion pass action block should execute at T:105At T5 you determined vacuity, then that attempt passed vacuity at T5. Where do you get this T105? Also, the pass action block is suppressed, and the pass=pass+1; action block is not executed (see the simulation waveforms).
  • An assertion FAIL and its action block occurs in the cycle in which it occurs
  • This model and TB have 5 threads when the attempt with $rose(go) is true, 2 of which are NV. All the other attempts are vacuous since $rose(go) is false. The PASS action block is executed when all the threads are evaluated and one of the threads is NV. SIm shows ONE PASS action block, with the variable pass==1 at T105

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

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

In reply to ben@SystemVerilog.us:
Hi Ben,

Hopefully, your reply was to my reply with
EPWave Waveform Viewer wave
Fig9_1_Part2(1) - EDA Playground code
I added a “go” to restrict the model to one successful attempt

The reply was actually in response to my previous code i.e without $rose( go ) : edalink2
I had some free time today so I was debugging the threads for each attempt and documented the same in a tabular format: all_attempts