Question on muti-thread and single-thread sequences

Hi,
system verilog assertions handbook 4th Edition by Ben Cohen states the following on Multi-threaded sequences :

“A sequence is multi-threaded if it includes any of the following operators: and, or, intersect, range delay, consecutive range repetition, non-consecutive range repetition (e.g. a[=2] ## 1b)”. I have the following questions with reference to the above statement-

  1. I am not clear how a[=2] ## 1b is multi-threaded - having multiple search paths which can result in success of threads. For example,
    a !a !a a b and a !a !a a !a b are two possible search paths possible. (assuming a is high at clock 1, low at clocks 2 and 3, high at 4 and b is high at clock 5 and 6). Both search paths will succeed in this case. Is this the reason it is multi-threaded? Is the understanding correct?

  2. By the same logic, a[->2]##1b is not multi-threaded since b has to immediately follow the last (second) a. Is that correct?

  3. Can we give a range for non-consecutive and goto repetition operators ? (a[=2:4] ## 1b), (a[->2:4] ## 1b).

  4. For sequences a[=2:4] ## 1b), (a[->2:4] ## 1b) both will be multi-threaded. Is this understanding correct?

  5. Also the sequence b ##1 a[=2] is not multi-threaded, since there are not multiple search paths. Is this correct?

regards,
-sunil puranik

In reply to puranik.sunil@tcs.com:

See annotations
the following on Multi-threaded sequences :

“A sequence is multi-threaded if it includes any of the following operators: and, or, intersect, range delay, consecutive range repetition, non-consecutive range repetition (e.g. a[=2] ## 1b)”. I have the following questions with reference to the above statement-

[Ben] That is correct

  1. I am not clear how a[=2] ## 1b is multi-threaded - having multiple search paths which can result in success of threads. For example,
    a !a !a a b and a !a !a a !a b are two possible search paths possible. (assuming a is high at clock 1, low at clocks 2 and 3, high at 4 and b is high at clock 5 and 6). Both search paths will succeed in this case. Is this the reason it is multi-threaded? Is the understanding correct?

[Ben] Yes. From my book, in the chapter of definitions, I write
thread: A thread is a search path for success of the property within an evaluation attempt that starts at the leading clocking event of the property. For example, a bus request that is acknowledged within 1 to 5 cycles may have 5 threads: request followed by acknowledge in 1 cycle, request followed by acknowledge in 2 cycles, …, request followed by acknowledge in 5 cycles. Thus, a new thread may be started at every cycle, and every thread is independent from other threads that may have started at earlier cycles.

  1. By the same logic, a[->2]##1b is not multi-threaded since b has to immediately follow the last (second) a. Is that correct?

[Ben] NO! a[->2] ##1 b IS multithreaded. it is equivalent to
b[->2] is equivalent to: !b[*0:] ##1 b ##1 !b[*0:] ##1 b
// first 2 not necessarily consecutive b’s

Thus, a[->2] ##1 b is equivalent to:
(a##1 a ##1 b) or ( a ##1 !a a ##1 b) or …(!a ##1 a##1 !a ##1 !a ##1 a ##1 b) or …
There are zillions of threads !

  1. Can we give a range for non-consecutive and goto repetition operators ? (a[=2:4] ## 1b), (a[->2:4] ## 1b).

[Ben] Yes. 1800 syntax pg 379

non_consecutive_repetition ::= [= const_or_range_expression ] 
goto_repetition ::= [-> const_or_range_expression ] 
const_or_range_expression ::= constant_expression | cycle_delay_const_range_expression 
cycle_delay_const_range_expression ::= constant_expression : constant_expression
 | constant_expression : $ 
expression_or_dist ::= expression [ dist { dist_list } ]
  1. For sequences a[=2:4] ## 1b), (a[->2:4] ## 1b) both will be multi-threaded. Is this understanding correct?
    [Ben] If you have a range, it is multithreaded
    You have options, this sequence OR that sequence Or this other sequence OR …

Hi Ben,
thanks a lot for the immediate reply. I have following questions with reference to above:

  1. In your book, in section 2.3.1, page 27, following example is given :
    An example of a single threaded sequence is a ##2 b ##1 c[->1]. However, this would mean-
    (a##2b##1c) or (a##2b##1!c##1c) or (a##2b##1!c ##1!c##1c) … there are many possibilities. So will it be multi-threaded and not single threaded? Or it is single threaded since if one combination is true, others cannot be true and simulator does not need to evaluate them

  2. Using the logic given above ( i.e. b[->2] is equivalent to: !b[*0:] ##1 b ##1 !b[*0:] ##1 b),
    expression b[->2] or b[=2] is also a sequence which is multi-threaded since
    b[-> 2] means b##1b or b ##1!b ##1!b ##1 b … there are so many possibilities (till end of simulation). Is that understanding correct?

  3. If 2 is true, the expression b[->1] or b[=1] is a sequence which is not multithreaded since b appears only once. Is this understanding correct? Or it IS multi-threaded because you can have combinations like (!b##1b) or (!b##1!b##1b). However, does the thread evaluation start only when b is 1 or evaluation starts even when b is 0 as in (!b##1b) or in (!b##1!b##1b)

  4. b[=1] ## 1 c is multi-threaded since this would mean -
    b ##1c or b##1 !b ##1c or b##1!b ##1 !b ##1 c … There are many possibilities till simulation ends. Is this correct understanding?

  5. However, b[->1] ##1 c is single threaded since after b, c must follow. Is this correct?

thanks and regards,
-sunil p.

In reply to puranik.sunil@tcs.com:
I had the wrong English word but the right concept when I categorized the goto operator as single-threaded. The goto operator [->n] is multi-threaded but, like single-threaded sequences, it is singly-ended (i.e., there can be ONE match at its end point.
or example:


a[->1] // has all these threads
a          // If a==1, then all other threads are false
!a  a      // when a==1, then all other threads are false
!a !a  a   // when a==1, then all other threads are false
!a !a !a ............ a

Thus, here is how I am correcting my English

Sequences can be single-threaded singly-matched, or be multi-threaded singly or muli-matched (i.e., more than one occurrence of a match).
Single-thread and singly-matched sequence: A sequence is singly-matched if it has single matched search path. That can occur if a sequence does NOT include any of the following operators: and, intersect, or, range delay (i.e., ##[1:5]), consecutive range repetition (i.e., a[*1:5]) , non-consecutive repetition (i.e., a[=3], a[=1:3]). An example of a singly-matched sequence is: a ##2 b ##1 c[->1]. Note that the goto operator is multi-threaded but can have only one possible match, thus it is singly-matched.
Multi-thread sequence: A sequence is multi-threaded if it includes any of the following operators: and, intersect, or, range delay (e.g., a ##[1:2] b), consecutive range repetition (e.g., a[*1:2] ##1 b), non-consecutive repetition (e.g., a[=2] ##1 b).


[Ben] the goto is important when used in an antecedent because 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. The use of the goto ensures a single match; this is why, in my mind, I viewed it as single-threaded. Bad English, I should view the goto as singly-matched or singly-ended.

My Apologies, and thank you for pointing this out.
Ben

Thanks a lot Ben for the explanation. Your book is very detailed and gives excellent treatment of the topic.
I have some more questions as follows :
On page no. 38, there is an example sequence where a new “a” is repeated g times and g is an integer-

(rose (a), v = g) |-> first_match((a==1'b1, v=v-1'b1)[*1:] ##0 v==1’b0) ##0 a==1’b1

Now assuming g = 3, this would translate into -

($rose (a), v = 3)|-> first_match((a==1’b1, v=2) or ((a==1’b1, v=2) ##1 (a==1’b1, v=2) ##1 a==1’b1 v=1) or ((a==1, v=2) ##1 (a==1, v=2)##1 (a==1, v=1)##1 (a==1, v=0)…)##0 v==1’b0)##0 a==1’b1

I am not clear about what is the next step and how this would result in a match. Do we need to distribute last term (fusion) over all the or terms (which are infinite). In that case, only the third or term (which has a==1 for 3 consecutive clocks) results in a match.
Will that be correct interpretation. Why is a==1’b1 fused with all the terms?

regards,
-sunil puranik

In reply to puranik.sunil@tcs.com:
The sequence_match_item executes at the end point of a sequence. Thus,


($rose (a), v = g) |-> first_match((a==1'b1, v=v-1'b1)[*1:$] ##0 v==1'b0) ##0 a==1'b1
//Now assuming g = 3, this would translate into -
($rose (a), v = 3)|-> first_match(
  ((a==1'b1, v=2) ##0 v==1'b0) or // (a==1'b1, v=v-1'b1)[*1]
  ((a==1'b1 ##1 a==1'b1, v=1) ##0 v==1'b0) or // (a==1'b1, v=v-1'b1)[*2]
  ((a==1 ##1 a==1 ##1 a==1, v=0) ##0 v==1'b0) )  // (a==1'b1, v=v-1'b1)[*3]
  ##0 a==1'b1


Thank you Ben for the reply and explanation. I have following questions wrt above:

  1. The sequence match results only in the third OR term as v=0 is anded with v==1’b0. First two OR terms will be zero when fused with v==1’b0 as v is not equal to 1’b0 in first two OR terms.
    Is this correct?

  2. What is the sequence_mathc_item here?

  3. Why is last term a==1 fused with the resultant expression?

Actually I am not clear about how the last term (v==1’b0) is fused (anded). (a==1 ##1 a==1 ##1 a==1, v=0) ##0 v==1’b0). Sequence fusion is equivalent to an and operation. So how is (a==1 ##1 a==1 ##1 a==1, v=0) ##0 v==1’b0) evaluated? Last term (a==1, v=0) has to be anded with v==1’b0. I am not clear how this works. May be something seriously wrong with my understanding.

regards,
-sunil

In reply to puranik.sunil@tcs.com:

Thank you Ben for the reply and explanation. I have following questions wrt above:

  1. The sequence match results only in the third OR term as v=0 is anded with v==1’b0. First two OR terms will be zero when fused with v==1’b0 as v is not equal to 1’b0 in first two OR terms.
    Is this correct?

// first_match((a==1’b1, v=v-1’b1)[*1:$] ##0 v==1’b0) ##0 a==1’b1
Correct

  1. What is the sequence_mathc_item here?
//1800 syntax
sequence_expr ::=
...
| (sequence_expr {, sequence_match_item}) [sequence_abbrev]    
// example: (a ##1 b[->1], v=v+1)[*2]

The sequence_match_item is v=v-1’b1

  1. Why is last term a==1 fused with the resultant expression?

Apologies, this was not a good example. It should be


/* Consider the following  example where a new "a" must be repeated up to "g" times until b;  "g" is a module variable of type int: */
property p_g; //   
  int v;     //  
  ($rose(a),v=g)|->(a==1'b1, v=v-1'b1)[*1:$] ##0 (v==1'b0 || b==1'b1); 
endproperty 
/* In a consequent the first_match is not needed.  However, if that sequence were an 
antecedent then a first_match would be needed. 
 ($rose(a),v=g) ##1 first_match((a==1'b1, v=v1'b1)[*1:$] ##0 (v==1'b0 || b==1'b1) |-> c 

Apologies for the confusion; I must have gotten carried away.
Rhnaks for pointing this out.

Hi Ben,
thank you for the explanation.
I have a requirement in which we need to check if a clock is toggling throughout the simulation. Now if the clock is derived from another clock by dividing by an integer (which is programmed in a register), we can check this using statement similar to following :

  1. (assuming clock period is 2n, n is passed as argument)

drclk_prop1: assert property (
                              disable iff (reset) @ (posedge clk)$rose(clk_derived) |-> ##n !clk_derived
);

Similar statement can be written for clk_derived falling edge followed after n clks by clk_derived.

Is it a correct approach?

  1. Another way would be to write a sequence of (clk_derived ##n !clk_derived) repeated very large number of time and write it in assert property statement.

drclk_prop2 : assert property ((clk_derived ##n !clk_derived)[*1000]); //1000 number is 
                                                                   //arbitrarily chosen.

but there may not be 1000 clocks till simulation ends. How does one ensure that this sequence repeats till end of simulation?

  1. If the clock in above problem is not a derived clock but a basic clock, it is not possible to check using an any assertion if it toggles continuously. Is this correct?

  2. For the clock which is not derived but basic clock, we can however check if the period of the basic clock is 100 or 200 ns by using $time to get the interval between the times at which it is toggling. Is this correct approach?

regards,
-sunil

In reply to puranik.sunil@tcs.com:

I have a requirement in which we need to check if a clock is toggling throughout the simulation. Now if the clock is derived from another clock by dividing by an integer (which is programmed in a register), we can check this using statement similar to following :

  1. (assuming clock period is 2n, n is passed as argument)

drclk_prop1: assert property (
disable iff (reset) @ (posedge clk)$rose(clk_derived) |-> ##n !clk_derived
);

Assuming this code for the derivation:

always  #1  clk  =  !clk ;
  always @(posedge clk) begin 
     clk1 <= !clk1; 
     if(clk1) clk2 <= !clk2; 
  end

you’ll have posedges of clk, clk1, clk2 in the same time step and the sampling of clk1 at those time steps will be zero. This may work for clk1 by using the negedge of clk
EPWave Waveform Viewer waves


drclk2: assert property (
   disable iff (reset) @ (negedge clk) clk1==0 |-> ##1 clk1==1);
drclk1: assert property (
   disable iff (reset) @ (negedge clk) clk2==0 |-> ##1 clk2==0 ##1 clk2==1[*2]);

  1. Another way would be to write a sequence of (clk_derived ##n !clk_derived) repeated very large number of time and write it in assert property statement.

NO

  1. For the clock which is not derived but basic clock, we can however check if the period of the basic clock is 100 or 200 ns by using $time to get the interval between the times at which it is toggling. Is this correct approach?

Yes, Do a search, this was addressed many times, including me.
I just did this search: ben cohen verificationacademy period $realtime
It yielded:

Another approach modeled after my reply to

uses the fork join_any. It is modeled after my paper
Understanding the SVA Engine Using the Fork-Join Model
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
Using a model, the paper addresses important concepts about attempts and threads. Emphasizes the total independence of attempts.

For reuse of the task, I wanted to use arguments with a ref to the clock.
Example: task automatic check_clk(int rpt, ref bit ck); and pass clk1. BUT:
// Actual argument ‘clk1’ passed as reference cannot be used
// within fork-join_any or fork_join_none blocks
If you can write separate tasks for each clock, this will also work, but it definitely looks complex. I am throwing it in to get you thinking about other possibilities.

(3) - EDA Playground // code
EPWave Waveform Viewer // wave


module test();
  int pass, fail, deb;
  bit clk, clk1=1, clk2=1;  // period clk=2, clk1==4, clk2==8
  always  #1  clk  =  !clk ;
  always @(posedge clk) begin 
     clk1 <= !clk1; 
     if(clk1) clk2 <= !clk2; 
  end 

  always @(posedge clk) begin 
    fork check_clk(2); // trigger the task 
    join_none
    fork check_clk4(4); // trigger the task 
    join_none
  end

  task automatic check_clk(int rpt); 
    // Actual argument 'clk1' passed as reference cannot be used 
   // within fork-join_any or fork_join_none blocks
      bit timeout_flag;
        fork 
          begin
            @(posedge clk1);  
          end
          begin
            repeat(rpt) @(posedge clk); 
            #1 timeout_flag = 1;            
          end
        join_any;
    am_stat_ok: assert(timeout_flag == 0) pass=pass +rpt +1 + rpt; //debug 
        else begin fail=fail+1 +rpt; $display("Fail"); end
    endtask

  task automatic check_clk4(int rpt); 
    // Actual argument 'clk1' passed as reference cannot be used 
   // within fork-join_any or fork_join_none blocks
      bit timeout_flag;
        fork 
          begin
            @(posedge clk2);  
          end
          begin
            repeat(rpt) @(posedge clk); 
            #1 timeout_flag = 1;            
          end
        join_any;
    am_stat_ok4: assert(timeout_flag == 0) pass=pass +rpt +1 + rpt; //debug 
        else begin fail=fail+1 +rpt; $display("Fail"); end
    endtask

  initial begin
    $dumpfile("dump.vcd"); $dumpvars;
    #50 force clk1=0; 
    #20 $finish;    
   end
endmodule

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

Hi Ben,
thanks a lot for immediate reply.

  1. Now the property for clk2 has been written as :

drclk1: assert property (
   disable iff (reset) @ (negedge clk) clk2==0 |-> ##1 clk2==0 ##1 clk2==1[*2]);


Since clk2 is clk divided by 4, we could also have written this as :


drclk1: assert property (
   disable iff (reset) @ (negedge clk) clk2==0 |-> ##2 clk2==1);
drclk1_1: assert property (
   disable iff (reset) @ (negedge clk) clk2==1 |-> ##2 clk2==0);


Though this will not check the clk2 at intermediate clocks. It will not ensure a 50% duty cycle clk2. Have you written it to ensure 50% duty cycle.

  1. Can this property also be written using @rose and $fell, since for clk2, referring to the waveform you have given, after a posedge is detected for clk2, clk2 will be 0 after two clks and after clk2 falling edge, it will be 1 after two clks again:

drclk1: assert property (
   disable iff (reset) @ (negedge clk) $rose(clk2) |-> ##2 clk2==0);
drclk1_1: assert property (
   disable iff (reset) @ (negedge clk) $fell(clk2) |-> ##2 clk2==1);


Though this does not check for 50% duty cycle. Is this correct?

thanks and regards,
-sunil

In reply to puranik.sunil@tcs.com:

My assertions just checked for toggling.

for detailed time measurements, use the approach described in
https://verificationacademy.com/forums/systemverilog/checking-clock-period-using-system-verilog-assertion

The question though is: DO you really need to do this for the whole sim run?
Seems excessive. An analysis can check the clock divisions.
I see clock toggling checks for cases when the clock is being switched off under certain circumstances.
Ben