Assertions for Two clock cycles

SystemVerilog
,
1

Hi All

I have two clocks
clk1 = 100mhz - This clock is available always.
clk2 = 10mhz
I need to write assertions to check
if clk2 is not available for two consecutive cycles then output signal should go low.

Help me with assertions.

2

In reply to mpradhani:

Edit code - EDA Playground code
EPWave Waveform Viewer // waveform
This code has a lot of debug features; you’ll need to remove them for your needs.
The “go” was for debug to isolate the evaluation of the assertion to one attempt.


module top;
  bit clk10=1, clk1=0; 
  int pass, fail, start, thecount, im_fail;
  bit sp_clk1, go=1; // support logic 
  initial forever #3 clk10 = !clk10;
  initial forever #30 clk1 = !clk1;
  initial forever #30 sp_clk1 = !sp_clk1;
  
  function automatic void f(); start=start+1; go=0; endfunction // debug
  function automatic void f2(int v); thecount=v; endfunction // debug

  property p_clk1; 
    int count=0;
    bit vck1; 
    @(posedge sp_clk1) go |->  ##0 @(posedge clk10) ##1 (1, f()) ##0
                 ((1,count=count+1, vck1=clk1, f2(count)) ##5 
                  (1,count=count+ $changed(clk1), vck1=clk1, f2(count)) ##4 1)[*2] 
    ##1 (1, f2(count)) ##0 count==4;
   endproperty 
  ap_clk1: assert property(p_clk1) pass=pass+1; else fail=fail+1; 
    
    function automatic void f3(); im_fail=im_fail+1; endfunction
    // Does not meet the requirements for 2 cycles, but is presented as an idea. 
    am_clk1: assert final(clk1==sp_clk1) else f3(); 

  initial begin
    $dumpfile("dump.vcd"); $dumpvars;
    repeat(50) @(posedge clk10);
    $finish(2);
  end
    
   initial #100 force clk1=1; 
endmodule

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

3

In reply to ben@SystemVerilog.us:**
Update**: The count should be based on changes only. Thus,
(1) - EDA Playground code
EPWave Waveform Viewer wave


module top;
  bit clk10=1, clk1=0; 
  int pass, fail, start, thecount, im_fail;
  bit sp_clk1, go=1; // support logic 
  initial forever #3 clk10 = !clk10;
  initial forever #30 clk1 = !clk1;
  initial forever #30 sp_clk1 = !sp_clk1;
  
  function automatic void f(); start=start+1; go=0; endfunction // debug
  function automatic void f2(int v); thecount=v; endfunction // debug

  property p_clk1; 
    int count=0;
    bit vck1; 
    @(posedge sp_clk1) go |->  ##0 @(posedge clk10) ##1 (1, f()) ##0
    (1,count=0, vck1=clk1, f2(count)) ##5 
    ((1,count=count+ $changed(clk1), vck1=clk1, f2(count)) ##4 1)[*4] 
    ##1 (1, f2(count)) ##0 count==4;
   endproperty 
  ap_clk1: assert property(p_clk1) pass=pass+1; else fail=fail+1; 
    
    function automatic void f3(); im_fail=im_fail+1; endfunction
    // Does not meet the requirements for 2 cycles, but presented as an idea. 
    am_clk1: assert final(clk1==sp_clk1) else f3(); 

  initial begin
    $dumpfile("dump.vcd"); $dumpvars;
    repeat(50) @(posedge clk10);
    $finish(2);
  end
    
   //initial #100 force clk1=1; 
endmodule

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

4

In reply to ben@SystemVerilog.us:
If you want to add the error state test, then


bit error; 
// If error is clk1 drops for 2 or 3 half-cycles
// end the final test with 
... ##1 (1, f2(count)) ##0 (count==1 &&  error) ||  // drop for 3 half-cycles, error
                           (count==2 &&  error) ||  // drop for 2 half-cycles, error
                           (count==3 && !error) ||  // drop for 1 half-cycle, no error
                           (count==4 && !error);    // no drops
5

In reply to mpradhani:

How about:


    a_p_slow_clk_is_off : assert property (
      @(posedge clk10) !clk1[*20] |-> !out_slow_clk_is_off);

Regards
Srini

6

In reply to ben@SystemVerilog.us:
My co-author and colleague Srinivasan Venkataramanan suggested a simpler approach, here it is:
(2) - EDA Playground code
EPWave Waveform Viewer // wave


 property p_clk1_v2; 
    bit vclk1; 
    @(posedge sp_clk1) go |->  
    @(posedge clk10) ##1 (1, vclk1=clk1) ##1 clk1==vclk1[*4] ##1
     ( ($changed(clk1), vclk1=clk1) ##1 clk1==vclk1[*4]) [*3];
 endproperty
    
 ap_clk1_v2: assert property(p_clk1_v2) pass1=pass1+1; else fail1=fail1+1;
7

In reply to ben@SystemVerilog.us:

A different approach
(2) - EDA Playground code
EPWave Waveform Viewer wave


 property p_clk1_v2; 
    bit vclk1; 
    @(posedge sp_clk1) go |->  
    @(posedge clk10) not(##1 $changed(clk1)[*20]);
     endproperty
    
 ap_clk1_v2: assert property(p_clk1_v2) pass1=pass1+1; else fail1=fail1+1;