Legal ways to specify the leading clock in SVA

SystemVerilog
,
1

Hi,
I was trying to summarize on different ways on how leading clock is inferred in SVA

  1. Using default clocking block

    default clocking cb1 @(posedge clk); endclocking 
    sequence sr1;
     a ##2 b ; 
    endsequence
   property pr1;
    c |=> sr1;
   endproperty  
  ap1:assert property(pr1);
  1. Specifying clock in sequence

    sequence sr1;
     @(posedge clk) a ##2 b ; 
    endsequence
   property pr1;
    c |=> sr1;
   endproperty  
  ap2:assert property(pr1);
  1. Specifying clock in property

    sequence sr1;  // Infers the clock from pr1
      a ##2 b ; 
    endsequence
   property pr1;
    @(posedge clk) c |=> sr1;
   endproperty  
  ap3:assert property(pr1);
  1. Clock Inferred from always block

   sequence sr1;  // Infers the clock from pr1
    req ##2 gnt ; 
   endsequence
   property pr1;  // Infers the clock from always block
    cStart |=> sr1;
   endproperty  
   always@(posedge clk) 
   ap4:assert property(pr1);
  1. Clock inferred from forever block

  sequence sr1;
    req  ##2 gnt ; 
  endsequence
  property pr1;
    cStart |=> sr1;
  endproperty  
  initial begin
    forever @(posedge clk) begin
      ap5:assert property(pr1);
    end  
  end

I notice that (2) and (5) are illegal whereas (1),(3) and (4) are legal.

[Q1] I am curious to know what makes (2) and (5) illegal ?

(a) For (2) , why doesn’t property pr1 inherit the clock from sequence sr1 ?
(b) For (5) , similar to inheriting the clock from always block , why isn’t the clock inherited from forever block ?

[Q2] Are there any other legal ways to specify/infer the leading clock ?

[Q3] Do the same rules apply for cover property as well ?

2

In reply to Have_A_Doubt:
I think this has been specified in 16.16 Clock resolution in IEEE std 1800 2017 as follows:

There are a number of ways to specify a clock for a property. They are as follows:
— Sequence instance with a clock, for example:

sequence s2; @(posedge clk) a ##2 b; endsequence
property p2; not s2; endproperty
assert property (p2);

— Property, for example:

property p3; @(posedge clk) not (a ##2 b); endproperty
assert property (p3);

— Contextually inferred clock from a procedural block, for example:

always @(posedge clk) assert property (not (a ##2 b));

— A clocking block, for example:

clocking master_clk @(posedge clk); 
property p3; not (a ##2 b); endproperty
endclocking
assert property (master_clk.p3);

— Default clock, for example:

default clocking master_clk ; // master clock as defined above 
property p4; (a ##2 b); endproperty
assert property (p4);

As For Q1:
(a) For 2, there is a variable c has been used and there is no clock defined for this variable, so if you remove it from pr1, it should be legal.
(b) For 5, forever isn’t a procedural block.

For Q2 and Q3: As mentioned, there is nothing mentioned about whether the directive you’re using (assert, cover, …) will affect the clock resolution or not. So it’s fair to say that the rules still apply.

3

1800’2017: 16.16 Clock resolution addresses this topic.

1) Using default clocking block: LEGAL


    default clocking cb1 @(posedge clk); endclocking 
    sequence sr1; a ##2 b ; endsequence
   property pr1; c |=> sr1; endproperty  
  ap1:assert property(pr1);  // LEGAL

**2) Specifying clock in sequence: LEGALITY DEPENDS ON USE/b]
See embedded comments


    sequence sr1;  @(posedge clk) a ##2 b;  endsequence
    property pr1; c |=> sr1; endproperty  
    ap2:assert property(pr1); // ILLEGAL 
    // Illegal because c has no leading clocking event (LCE)
    // the clocking event in sr1 does not flow backwards
//-----------
   property pr2; sr1 |-> c; endproperty  
  // Directive 'ap2' has un-clocked expressions or constructs. Please fix
  ap2b:assert property(pr2); // ILLEGAL
  // The clocking event in sr1 does not flow out of the sequence 
//--------------
sequence s2; @(posedge clk) a ##2 b; endsequence 
property p2; not s2; endproperty 
assert property (p2); // LEGAL because the s2 has a LCE

[b]Specifying clock in property: DEPENDS**


    sequence sr1;  a ##2 b ;  endsequence
    property pr1; @(posedge clk) c |=> sr1; endproperty  
    ap3:assert property(pr1); LEGAL 
    // Clocking event in property is the LCE and 
    // it flows into sr1.  It cannot flow out of the sequence
    // but can flow into sequences following the sr1
    property pr1b; @(posedge clk) c |=> sr1 ##1 d; endproperty  
//  ----- 
  sequence sq;  a ##2 b ;  endsequence
    property p1x; @(posedge clk) c |=> sq; endproperty  
    property p2x; @(posedge clk2) c |=> a ##1 sq; endproperty  
    ap3:assert property(pr1); // LEGAL 
      ap4: assert property(p1 implies p2x);// illegal
        // Directive 'ap3' has un-clocked expressions or constructs

4) Clock Inferred from always block: LEGAL


   sequence sr1; seq ##2 gnt ;  endsequence
   property pr1;  cStart |=> sr1;  endproperty  
   always@(posedge clk) ap4:assert property(pr1);
   // Infers the clock from always block

5) Clock inferred from forever block is ILLEGAL


  sequence sr1b; req  ##2 gnt ; endsequence
  property pr1b; cstart |=> sr1; endproperty  
  initial begin
    forever @(posedge clk) begin
      // The sva directive is not sensitive to a clock. .
      // Procedural assertion ( i.e., assert, assume or cover property) is not 
      // allowed in looping statement.Only immediate assertions are allowed in this 
      ap5:assert property(pr1b);

The same rules do apply for cover property as well ?

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

4

In reply to ben@SystemVerilog.us:

Hi Ben,

I couldn’t find anything in the 2017 LRM that justifies your comment in number [5]

// Procedural assertion ( i.e., assert, assume or cover property) is not 
// allowed in looping statement.

Could you point me to the section where that is explained? As I’ve tried the following code and it seems like it’s legal. in the below code always_asrt (defined in always block) is equivalent to forever_asrt (defined in a loop).

EDA link : forever vs always assertion - EDA Playground

module test;

  bit clk;
  bit a,b;
  
  default clocking @(posedge clk); endclocking
  
  always #1 clk = ~clk;

  //----------------------//
  property always_pp;
    a |-> b;
  endproperty
  
  //----------------------//
  property forever_pp;
    a |-> b;
  endproperty
  
  //----------------------//
  always @(posedge clk) begin
    always_asrt: assert property(always_pp);
  end
  
  //----------------------//
  initial begin
    forever @(posedge clk)begin
      forever_asrt: assert property(forever_pp);
    end
  end
        
  //----------------------//     
  initial begin
    #2 a=1; b=0;
    #20 $finish;
  end
        
endmodule
5

In reply to Ahmed Kelany:

I couldn’t find anything in the 2017 LRM that justifies your comment in number [5]
// Procedural assertion ( i.e., assert, assume or cover property) is not
// allowed in looping statement.

1800’21017: 16.16
— Contextually inferred clock from a procedural block, for example:
always @(posedge clk) assert property (not (a ##2 b));


1800:2017 Clause 9 describes the SystemVerilog **procedural blocks**:
 initial, always, always_comb, always_ff, always_latch, and final.  

9.2 Structured procedures All structured procedures in SystemVerilog are specified within one of the following constructs: 
— initial procedure, denoted with the keyword initial (see 9.2.1 ) 
— always procedure, denoted with the keywords: • always (see 9.2.2.1 ) 
     • always_comb (see 9.2.2.2 ) 
     • always_latch (see 9.2.2.3 ) 
     • always_ff (see 9.2.2.4 ) 
— final procedure, denoted with the keyword final (see 9.2.3) 
— Task 
— Function 

The syntax for these structured procedures is shown in Syntax 9-1 )

I’ve tried the following code and it seems like it’s legal. in the below code always_asrt (defined in always block) is equivalent to forever_asrt (defined in a loop).

You touched on tool issues, and we don’t discuss tools in this forum.
If you have a problem, contact your vendor.
In any case, 1800 is specific as to what is a procedural block.


  //----------------------//
  initial begin
    forever @(posedge clk)begin
      forever_asrt: assert property(forever_pp);  // line 28
    end
  end
sim: Error-[PAOCNAILS] Procedural assertion in a loop
testbench.sv, 28
test, "assert property(forever_pp);"
  Procedural assertion ( i.e., assert, assume or cover property) is not 
  allowed in looping statement.Only immediate assertions are allowed in this 
  context.

Ben

6

In reply to ben@SystemVerilog.us:
Note that the following is also ILLEGAL even if you have a Leading Clocking Event (LCE)


initial begin
    forever @(posedge clk)begin
      forever_asrt: assert property( @(posedge clk) forever_pp);
    end
  end
 "assert property(@(posedge clk) forever_pp);"
  Procedural assertion ( i.e., assert, assume or cover property) is not 
  allowed in looping statement.  Only immediate assertions are allowed in this 
  context.

1800’2017: 9.2 Structured procedures All structured procedures in SystemVerilog are specified within one of the following constructs:
— initial procedure, denoted with the keyword initial (see 9.2.1 )
— always procedure, denoted with the keywords: • always (see 9.2.2.1 )
• always_comb (see 9.2.2.2 )
• always_latch (see 9.2.2.3 )
• always_ff (see 9.2.2.4 )
— final procedure, denoted with the keyword final (see 9.2.3)
— Task
— Function

Ben

7

In reply to ben@SystemVerilog.us:

I think you might misunderstood my question, I am not saying forever is a procedural block. I know it’s not. 2017 LRM section 16.16 is about clock inference, and it doesn’t say anything about the illegality of forever_asrt statement in the following code

module test;

  bit clk;
  bit a,b;
  
  default clocking @(posedge clk); endclocking
  
  always #1 clk = ~clk;

  //----------------------//
  property forever_pp;
    a |-> b;
  endproperty
  
  //----------------------//
  initial begin
    forever @(posedge clk)begin
      forever_asrt: assert property(forever_pp);
    end
  end
        
  //----------------------//     
  initial begin
    #2 a=1; b=0;
    #20 $finish;
  end

So my question is which section in the LRM says using

assert property

is illegal in a looping statement?

8

In reply to Ahmed Kelany:

So my question is which section in the LRM says using assert property is illegal in a looping statement?

You are correct, 1800 does not specifically say that it is illegal for looping statements.
The following reasons, based on SV rules, are possibly why one vendor is enforcing this restriction:

  1. Unrolling errors:
    Concurrent asserts are essentially static objects; if they are placed in a loop, the loop would have to be either unrolled or the assertion placed in an equivalent generate loop. For example:
    Edit code - EDA Playground

always @(posedge clk) begin
for (int i=0; i<=3; i++) begin
assert property(a|-> b);
// ILLEGAL:  Range must be bounded by constant expressions.
ap_arbiter: assert property(@(posedge clk)
(req[i]==1'b1) ##0 req[i:0] !=0 |=>
grnt[i]==1'b1 ##0 $onehot(grnt) );
end
end

One could say, yah, but the following should be legal if I change req[i:0] to req[i]

2. Infinite loop in a clocking block: For example (2) - EDA Playground


always @(posedge clk) begin
while(c==1) begin  // ifinite loop
assert property(a|-> b);
end
end
// System virtual memory limit exceeded -

We have the same issue with the forever

Getting back to the question: Should looping allowed in an always, always_ff?
Maybe there is a philosophical or inference reason for a tool to put such a code constraint because it can cause trouble or implementation issues.

Ben

9

In reply to ben@SystemVerilog.us:

Personally, I always try to avoid it. Thanks for the answer :-)

10

In reply to ben@SystemVerilog.us:

Hi Ben,
I was trying a few variations of always block


  property  pr1;
    a ##2 b;
  endproperty

1) always  begin
     if ( bstate )  begin
       @( posedge clk );
       assert  property( pr1 )  $display("TIME:%2t  Assertion  pr1  PASS", $time );
                          else  $display("TIME:%2t  Assertion  pr1  Fails", $time );
     end 
    end 

2) always  begin
     @( posedge clk );
     if ( bstate )  begin
       
       assert  property( pr1 )  $display("TIME:%2t  Assertion  pr1  PASS", $time );
                          else  $display("TIME:%2t  Assertion  pr1  Fails", $time );
     end 
    end 

3)  always@(posedge clk)  begin
     if ( bstate )  begin
       @(negedge regcheck);
       assert  property( pr1 )  $display("TIME:%2t  Assertion  pr1  PASS", $time );
                          else  $display("TIME:%2t  Assertion  pr1  Fails", $time );
     end 
    end 

4)  always@(posedge clk)  begin
     #1;
     if ( bstate )  begin
       assert  property( pr1 )  $display("TIME:%2t  Assertion  pr1  PASS", $time );
                          else  $display("TIME:%2t  Assertion  pr1  Fails", $time );
     end 
    end

I observe that although all tools unanimously throw compilation error for (1),(2) and (4).
Whereas some tools allow (3).

Would like to hear your thoughts/comments on the above four code ?

11

In reply to Have_A_Doubt:

1800 16.16 and 16.16.1 exhaustively go thru al the rules for inferred leading clocking event (LCE). It is tiresome to read and fully comprehend. Byt in simple terms, and as a guideline, if the property does not have a clocking event then the inferred LCE is only in an always in the style of always @(clocing_event)
Just stick to this rule if you do not want to include the clocking event in the assertion.
You’re making life too complicated if you violate simple design rules; and that is true for SV in general. Funky stuff can lead to funky behavior.
Ben

12

In reply to ben@SystemVerilog.us:

Hi Ben,
If it’s not too much to ask, I would like to hear your thoughts on (3) only


 always@(posedge clk)  begin
     if ( bstate )  begin
       @(negedge regcheck);
       assert  property( pr1 )  $display("TIME:%2t  Assertion  pr1  PASS", $time );
                          else  $display("TIME:%2t  Assertion  pr1  Fails", $time );
     end 
    end

Shouldn’t it be equivalent to


   property  pr1;
     @(posedge clk) bstate ##1 @(negedge regcheck) |=> @(posedge clk) a ##2 b;
   endproperty
   assert  property( pr1 );
13

In reply to Have_A_Doubt:

In reply to ben@SystemVerilog.us: your thoughts on (3) only


  property  pr1; a ##2 b; endproperty

 always@(posedge clk)  begin
     if ( bstate )  begin
       @(negedge regcheck);
       assert  property( pr1 ); // ERROR! No leading clocking event (LCE)
     end 
    end

You are thinking of the following to be legal:


   property  pr1;
     @(posedge clk) bstate ##0 @(negedge regcheck) 1 |-> @(posedge clk) a ##2 b;
   endproperty
   assert  property( pr1 );

Ben