Doubt on multi threaded assertions

[kpdeepak]

I have a property as shown below,

    ap_basic1 : assert property (@(posedge clk)
                a ##1 (b[=2]) |=> c);

I understand that the antecedent in this case is multi threaded and all threads should finish in order for the property to PASS.

But following waveforms indicates failures,

Please help me understand,
How many threads are forked off by the antecedent here?
Will this property ever PASS?

[dave_59]

Question on goto and non-consecutive repetition operators

The SYSTEM VERILOG ASSERTIONS HANDBOOK, 4th Edition states following on page no. 36: Do not use first_match function in a sequence that is an antecedent that has goto repetition operator unless that sequence has other expressions which are multi-ranged. Thus a ##1 b[->1] |-> c; //first_match is not needed here because once b==1, there could not be another thread of !b. The book also states on page no. 37 that for non-consecutive repetition operator, in an antecedent, we NEED TO USE first_matc…

[kpdeepak]

Hi Dave,

Thanks for the link. I think it explains the situation well. But on further experimentation with multiple threads, .ended and first_match constructs, I have a doubt which I tried to explain below,

   sequence s_basic2 ;
        a ##[2:4] b;
    endsequence
    ap_basic2 : assert property (@(posedge clk)
                s_basic2 |=> c);
    ap_basic3 : assert property (@(posedge clk)
                s_basic2.ended |=> c);
    ap_basic4 : assert property (@(posedge clk)
                first_match(s_basic2) |=> c);

A sample waveform is shown below,

Here I would think that the ap_basic2 would behave similar to basic3, because there will be multiple threads forked off by a ##[2:4] b in the antecedent and failure should be flagged for each of these.
So I’m not sure why ap_basic2 goes inactive at 290ns, which I would expect a first_match to do.

[hdlcohen]

1. .ended is deprecated. Use .triggered
2. the s_basic2.triggered will has 3 endpoints if all the threads are a match
3. first_match(s_basic2) with have the first matched thread of ; i.e., ONE match
   Thus, ap_basic2 would not behave similar to basic3
   Ben Cohen
   Ben@systemverilog.us
   Link to the list of papers and books that I wrote, many are now donated.
   https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf