Regarding clock inheritance for sequence methods and event control

SystemVerilog
, ,
1

Hi Forum ,
In one of the books I am referring to, I read the following quote

“Any sequence that will have a method attached to it must have an explicit clock”

In relation to the quote I tried the following : edalink

When tested on edaplayground the output isn’t unanimous, two tools throw a compilation error

Section 16.16 of the LRM mentions the following in relation to my example :

a) In a module, interface, program, or checker with a default clocking event, a concurrent assertion
statement that has no otherwise specified leading clocking event is treated as though the default
clocking event had been written explicitly as the leading clocking event.

d) An explicitly specified leading clocking event in a concurrent assertion statement supersedes a
default clocking event

[Q1] Via a) shouldn’t ‘sva2’ and ‘sva3’ inherit the default clocking event i.e @(posedge clk1) as it’s leading clock ?

[Q2] Via d) shouldn’t ‘sva1’ use explicit clocking event i.e @(posedge clk2) as it’s leading clock ?

[Q3] For same reasons as a) when sequence s1 is used as event control , shouldn’t the default clocking event i.e @(posedge clk1) be used as it’s leading clock ?

Thanks in advance

2

The edaplayground tools do not reflect the latest versions of the tools.
1800 is correct

3

Hi Ben,
Just to confirm

  1. From LRMs perspective the code is legal
  2. Yes is the answer for the 3 questions above
4

Yes to your questions. see
Clock inheritance for Seq. methods N event con(1) - EDA Playground code
EPWave Waveform Viewer wave.
Good practice to specify the clock if you need an endpoint

5

Ben,
Does the left to right clock flow rule also apply for sequence s1 ?

 always #5 clk1 = !clk1;
  
 default clocking cb @(posedge clk1); endclocking

 sequence s1;
   a ##1 b;  // Sequence method called on a sequence declared without an explicit clock
 endsequence 

 property prop;
   @(posedge clk3) c |=>  s1.triggered[->1]; 
 endproperty

ap1:assert property( prop ) $display("T:%0t ap1 Pass",$time);
                      else  $display("T:%0t ap1 Fails",$time);

[1] Would @(posedge clk3) take precedence over default clock and flow to s1 OR would default clocking be used for sequence s1 ?

However when using the sequence ( w/o explicit clock ) as event control the clock can’t be inherited via left to right clock flow rule

always@(s1) begin // Uses default clocking @(posedge clk1)
    $display("Sequence s1 matches at T:%0t",$time);
  end
6

Though sequence s1 has no Leading Clocking Event (LCE), when it is applied in an
assertion @(posedge clk2) s1.triggered[->1], the sequence s1 in s1 .triggered has Leading Clocking Event (LCE), and the endpoint is computed at that LCE.

I am checking on this with a colleague from the committee.
Stay tuned.

7

Turns out the LRM does indeed explain all the scenarios mentioned above.

From LRM section 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 following examples illustrate how a clock is inferred by a sequence when a method is applied to it.
module mod_sva_checks;
 .......
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);

sequence e5;
// e4 will infer posedge clk_e1 as per clock flow rules
// wherever e5 is instantiated (with/without a method)
  @(posedge clk_e1) a ##[1:3] e4.triggered ##1 c;
endsequence
// e4, used in e5, infers posedge clk_e1 from e5
a2: assert property (@(posedge clk_a) a |=> e5.matched);

sequence e6(f);
  @(posedge clk_e2) f;
endsequence
// e4 infers posedge clk_e2 as per clock flow rules
a3: assert property (@(posedge clk_a) a |=> e6(e4.triggered));

sequence e7;
  e4 ##1 e6(d);
endsequence
// Leading clock of e7 is posedge clk_a as per clock flow rules
a4: assert property (@(posedge clk_a) a |=> e7.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);

always @(posedge clk_a) begin
// e4 infers default clocking cb and not posedge clk_a as there is
// more than one event control in this procedure (16.14.6)
 @(e4);
 d = a;
end

Similar to ‘a1’ , within ‘prop’ the sequence s1 would infer posedge clk3 as per clock flow rules.

@ben2 One final question regarding ‘a5_illegal’
Why is it the ‘e4’ doesn’t infer the default clocking event ?
Is it due to ‘disable iff’ being asynchronous ?

8

MAny thanks for the clarifications.

9

Hi Ben ,
Would like to hear your thoughts on the following

10

Yes, the ‘disable iff’ is asynchronous and the clocking event
@(posedge clk_a) flows only into the property (a |=> b);
It does not flow into the disable iff .
Ben

11

LRM 16.13.3 mentions

The scope of a clocking event does not flow into the disable condition of disable iff .

Thus to make ‘a5_illegal’ work , explicit clock must be part of sequence e4.

sequence e4;
    @(posedge clk) $rose(b) ##1 c; // Explicit clock  added
endsequence
  
 a5_now_legal: assert property ( @(posedge clk) disable iff (e4.triggered) a |=> b) ;
12

Correct