Local variable assignment in Multithread consequent

SystemVerilog
,
7

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