Assertion implementation

How to implement the following check through assertions:
When the en signal is pulled low, the clk can still jump normally for a maximum of 3 times, and then it must be turned off, that is, it should remain unchanged.

// When the en signal is pulled low, the clk can still jump normally for
// a maximum of 3 times, and then it must be turned off,
// that is, it should remain unchanged.

// Two approaches: 
// 1) Using a task that can be called without a running other tb clock 
    task automatic t_clk_en0();
       int count; 
       fork
          #10; // 5 clks
          forever @(posedge clk) if((!en) count=count+1;
       join_any
      am_3clk_after_en: assert(count < 3) else err=err+1;
    endtask
    always @(!en) t_clk_en0(); 
    // or called with a running other clock 
    cover property(@(posedge clk_tb) !en |-> (1, t_clk_en0()));
// 2) An assertion using a running tb clock 
// Using the tb clock 
    property p_noclk_en; // adjust the max count allowed 
      int count=0; 
      @(posedge clk_tb) $fell(en) |-> ##1
         (1, count=count+1)[*1:$] ##0 count<4 intersect $rose(en)[->1];
    endproperty
    ap_noclk_en: assert property(p_noclk_en) else err1=err1+1; 


module  top2;
  bit  clk, en=1, en1=1, clk_tb;
  int err, err1;
  always #1 clk_tb=!clk_tb; 
  always_comb clk = clk_tb && en1;
  always en1 = #10 en;
    // When the en signal is pulled low, the clk can still jump normally for
    // a maximum of 3 times, and then it must be turned off, 
    // that is, it should remain unchanged.
    task automatic t_clk_en0();
       int count; 
       fork
          #10; // 5 clks
          forever @(posedge clk) if((!en) count=count+1;
       join_any
      am_3clk_after_en: assert(count < 3) else err=err+1;
    endtask
    // fire the task 
    // cover property(@(posedge clk_tb) !en |-> (1, t_clk_en0()));
    always @(!en) t_clk_en0(); 

    // Using the tb clock 
    property p_noclk_en; // adjust the max count allowed 
      int count=0; 
      @(posedge clk_tb) $fell(en) |-> ##1
         (1, count=count+1, count=count+1)[*1:$] ##0 count<4 intersect $rose(en)[->1];
    endproperty
    ap_noclk_en: assert property(p_noclk_en) else err1=err1+1; 

    initial begin 
      $dumpfile("dump.vcd"); $dumpvars;
      #10 en=0;
      #25 en=1; 
      #30 en=0;
      #50 en=1;
      #30; $finish();
    end
endmodule


Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

In reply to ben@SystemVerilog.us:

Hi Ben,
I have a minor qualm here. I saw that in the condition checking term/part ( I don’t know whether this is the proper technical term) You have written count=count+1 twice.
Could you tell me why?
Another question regarding the same is whether we can add more than one condition by using “,” or use logical operators only in that case.

In reply to Shubhabrata:

In reply to ben@SystemVerilog.us:
Hi Ben,
I have a minor qualm here. I saw that in the condition checking term/part ( I don’t know whether this is the proper technical term) You have written count=count+1 twice.
Could you tell me why?

That was an error on my part, apologies.

Another question regarding the same is whether we can add more than one condition by using “,” or use logical operators only in that case.

1800 defines one of the possible way to define a sequence as:


sequence_instance [ sequence_abbrev ] | ( sequence_expr {, sequence_match_item } ) [ sequence_abbrev ] 
//Thus, 
a ##1 (b, v1=state, v2=0, function_f1(v1, c), v3=f2(), task_k1())[*2]// is all legal
// Of course, a task does not return a value, and it should be automatic
assert property(@(!en) (1, t_clk_en0())); 

How to interpret or read this line in assertion ?

(1, count=count+1, count=count+1)[*1:$] ##0 count<4 intersect $rose(en)[->1];

In reply to MP:

// I made a mistake, probably a copy/paste error 
(1, count=count+1, count=count+1)[*1:$] ##0 count<4 intersect $rose(en)[->1];
// Should have been 
(1, count=count+1)[*1:$] ##0 count<4 intersect $rose(en)[->1];

(1, count=count+1, count=count+1)[*1:$] // is equivalent to 
(1, count=count+2)[*1:$] 
// My apologies

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

In reply to ben@SystemVerilog.us:

Hi Ben ,

Have 2 questions related to 2nd approach .

(1) What is the LHS for the intersect operator ?

Is it the sequence : *(1, count=count+1)[1:$] ##0 count<4 OR Only count < 4 ?

 I  could  **replace  intersect  with  throughout**  if  it  were  the  latter  as  LHS  can't  be  sequence  for  throughout.

(2) In your code the local variable is incremented on posedge of clk_tb .
What if I wanted to increment it only when clk toggles and then use clk_tb for intersect operator ?


   property p_noclk_en; 
      int count=0; 
    @(posedge clk_tb) $fell(en) |=> @( clk ) (1, count=count+1)[*1:$] ##0 @(posedge clk_tb) count<4 intersect $rose(en)[->1];
    endproperty
   
     

Would this be a correct approach ?

In reply to Have_A_Doubt:

In reply to ben@SystemVerilog.us:
Have 2 questions related to 2nd approach .
(1) What is the LHS for the intersect operator ?
Is it the sequence : *(1, count=count+1)[1:$] ##0 count<4 OR Only count < 4 ?

with
(1, count=count+1)[*1:$] ##0 count<4 intersect rose(en)[->1]; the LHS is (1, count=count+1)[*1:] ##0 count<4
You can put parentheses if you want; thus,
((1, count=count+1)[*1:$] ##0 count<4) intersect $rose(en)[->1];

I could replace intersect with throughout if it were the latter as LHS can’t be sequence for throughout.

See my paper Reflections on Users’ Experiences with SVA, Part II
Throughout
The syntax for this sequence is: expression_or_dist throughout sequence_expr. The throughout operator specifies that a signal (expression) must hold throughout a sequence. ( b throughout R ) is equivalent to ( b [*0:] intersect R ) ((1, count=count+1)[*1:] ##0 count<4) is NOT an expression, but a sequence.

(2) In your code the local variable is incremented on posedge of clk_tb .
What if I wanted to increment it only when clk toggles and then use clk_tb for intersect operator ?


property p_noclk_en; 
int count=0; 
@(posedge clk_tb) $fell(en) |=> @( clk ) (1, count=count+1)[*1:$] ##0 @(posedge clk_tb) count<4 intersect $rose(en)[->1];
endproperty

Would this be a correct approach ?

The issues are:
(5) - EDA Playground

With **intersect $rose(en)[->1];
**// * Error: (vsim-3937) Asserting on an illegal multiply clocked temporal expression. 
  // The clock flow cannot change in the RHS of 'intersect' operator.
//------------------------------------
// with **intersect  @(posedge clk_tb) $rose(en)[->1];**
    property p_noclk_en2; // adjust the max count allowed 
      int count=0; 
    @(posedge clk_tb) $fell(en) |=> (@( clk ) (1, count=count+1)[*1:$] ##0 @(posedge clk_tb) count<4) intersect  @(posedge clk_tb) $rose(en)[->1];
    endproperty
  ap_noclk_en2: assert property(p_noclk_en2) else err2=err2+1; 
    // * Error: (vsim-3937) Asserting on an illegal multiply clocked temporal expression. 
    // The clock flow cannot change in the RHS of 'intersect' operator.
#   // Time: 0 ns  Iteration: 0  Instance: /top2 File: testbench.sv Line: 28


Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog