Once a certain sequence occurs that another seq shouldn't occur till simulation ends

SystemVerilog
,
1

Hi All,

For the above requirement I tried the following edalink

module top;
  
  bit clk , a , b , c , d ;
  
  always #5 clk = !clk;
  
  sequence  seq1;
    a ##1 b ; 
  endsequence

 sequence  seq2;
    c ##1 d ; 
 endsequence

 property ab; 
   @( posedge clk )  seq1 |=>  not( always seq2 );
 endproperty

  assert property( ab ) $display("T:%0t Pass",$time);
    
                  else $display("T:%0t Fails",$time);
    
  initial begin
    #4 ; a = 1;
    #10; b = 1 ; a = 0;
    #40; c = 1 ; 
    #10; d = 1 ;
    #2 ; $finish();
  end  
  
    endmodule

However I observe that ‘seq2’ isn’t checked till end of simulation. I expected assertion to fail at T:65 whereas using the above code the assertion passes at T:25

2

In reply to MICRO_91:
I think you are confusing not( always seq2 ) with always ( not seq2 ). They are not the same.

3

In reply to dave_59:
Thanks Dave,
I was confused with the order of ‘not’ and ‘always’.
An alternative which works ( provided the latter is part of sequence body ) as well


  property ab; 
    @(posedge clk) seq1 |=> not( seq2.triggered[->1] ); 
 endproperty

Is there any preference between the two solution ? or can I easily swap one with the other

4

In reply to dave_59:

Dave,
Please see: Once seq1 matches, seq2 shouldn't occur(1) - EDA Playground

In Original code (from micro_91) - seq2 was unclocked, so QU is correct in saying:

[log]
** Error: testbench.sv(29): Use of a method on an unclocked sequence is illegal.
[/log]

but I added a default clocking block in the above link, I still see the error. Is this to do with some fancy cocking event resolution clause in the LRM?

Thanks

5

In reply to Srini @ CVCblr.com:

In the latter example I had added an explicit clocking event to ‘seq2’ to use .triggered.
But thanks for the interesting question, does default clocking apply to sequences (with no explicit clocks) methods ?

Here is what I found in the LRM


LRM 16.13.6 Sequence Methods ::
The sequence on which a method is applied shall either be clocked or infer the clock from the context where it is used. 
The same rules are used to infer the clocking event as specified in 16.9.3 for sampled value functions.

LRM 16.9.3 Sampled value functions ::
If called in an assertion, sequence, or property, the appropriate clocking event as determined by clock flow rules (see 16.13.3) is used.

As per LRM 16.13.3 Clock flow, sequence seq2 (with no clocking event) infers the clock from clocking event in property ‘ab’ . 2 tools agree with this


 // LRM 16.13.6  further provides an example
 default clocking cb @(posedge clk_d); endclocking
 sequence e4;
  $rose(b) ##1 c;
 endsequence
 // e4 infers posedge clk_a as per clock flow rules
 a1: assert property (@(posedge clk_a) a |=> e4.triggered);

 // Illegal use in a disable condition, e4 is not explicitly clocked
 a5_illegal: assert property( @(posedge clk_a) disable iff (e4.triggered) a |=> b );

 // Note :: 'e4.triggered' doesn't inherit the clock from default clocking !!

However LRM 16.13.3 Clock flow doesn’t mention about default clocking.

Whereas LRM 16.9.3 mentions :

Otherwise, if called outside an assertion, default clocking (see 14.12) is used.

does default clocking apply to sequences (with no explicit clocks) methods ?

Still looking for a definitive answer, any comments/suggestions from forum moderators are welcome

6

In reply to MICRO_91:

I think the clock should have been inferred in the sequence used in the triggered method. This is a tool specific issue.

The use of the triggered method was a workaround for a different tool specific issue.

7

In reply to dave_59:

Hi Dave,

I think the clock should have been inferred in the sequence used in the triggered method. This is a tool specific issue.

Just wanted to confirm whether the above quote is meant for clock inheritance via default clocking ( Eg: (2) below ) as well ?


// (1) Using un-clocked sequences 'seq1' and 'seq2' similar to the top of the thread
   property ab; 
    @(posedge clk) seq1 |=> not( seq2.triggered[->1] ); 
   endproperty
   assert property(ab);

// (2) Using un-clocked sequences 'seq1' and 'seq2' and default clocking block
   default clocking def @(posedge clk); endclocking

   property ab2; 
     seq1 |=> not( seq2.triggered[->1] );  // No clock
   endproperty
   assert property(ab2);

For (1) the LRM does confirm the clock flow from property ‘ab’ to un-clocked sequence ‘seq2’.
However for (2) I couldn’t find the clock inheritance via default clocking for ‘seq2’ ( else wouldn’t ‘a5_illegal’ inherit the clock from default clock ‘cb’ ? )

8

Although unrelated to the above discussion, I find this thread interesting from not v/s ! operator perspective.

(1) Although consequent i.e sequence method ‘triggered’ returns 1’b1 / 1’b0 i.e boolean value

(2) Goto repetition [→N] / Non-consecutive repetition [=N] works with boolean_expression

We can’t write consequent as :: ! (seq2.triggered[→1])

Unary operator ! can’t be used with a temporal sequence
9

Hi Dave,

On running the code at top ( using not( always seq2 ) as consequent ) I observe that pass action block executes at time: 25 units ( same time as consequent is evaluated )

I am clear on reason behind execution of pass action block.

How does consequent behave in this code ?

Thanks