How to write assertions for a Clock divider

SystemVerilog
2

In reply to yoshiko:
/ We want to verify a clock divider clocks(period , duty cycle and enable )
using assertions. Do we need to write separate assertions for every clock period ,
duty cycle etc. clocks are related to each other like (div2, div4,div8,div16and so on).
how to verify phase synchronization? /
There are various methodologies to verify models.
Comming from an old school of thoughts, I recommend the verification of clocks divisions to be done as follows:

  1. Verify through code reviews that ALL THE DERIVED CLOCKED ARE SOURCED BY A MASTER CLOCK. I demonstrate that below with clk2, clk4, clk8
  2. Verify through simulation that the design functions as you intended.
  3. If the design is not modified, there is little need for assertions. However, it does not hurt to add assertions; I would do that as a low priority after the top 2 items are done. Clock periods, or better yet, duration LOW and durations HIGH for each clock could done, along with the synchronization of the clocks.

I demonstrated this in the model below. The randomization stuff is part of my testbench template I use to test assertions; it is not used here.


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
  timeunit 1ns;     timeprecision 100ps;    
    bit clk, clk2, clk4, clk8, a, b;  
    realtime clk_period= 20ns; 
	default clocking @(posedge clk); endclocking
    initial forever #10 clk=!clk;  
    initial begin
      $timeformat(-9, 1, "ns", 8);
      $display("%t", $realtime);
   end 
   
    always  @(posedge clk)  begin 
        clk2 <= !clk2; // div 2 
        if(clk2) clk4 <= !clk4;
        if(clk2 && clk4) clk8 <= !clk8; 
    end 
    // Example of a frequency check 
    property p_clk_freq3;
        realtime current_time;
        @ (posedge clk)
        // disable iff ( !(!(reset) && (flag)))
        ('1, current_time = $realtime) |=> (1, $display ("p=%t", $realtime - current_time))
        ##0 (($realtime - current_time) <= clk_period + 1ns && // logical and
             ($realtime - current_time) >= clk_period - 1ns); 
    endproperty
    ap_clk_freq3: assert property (p_clk_freq3);
    // $past( expression1 [, number_of_ticks] [, expression2] [, clocking_event])
    ap_clk2: assert property(##8 1'b1 |-> @ (negedge clk) !$past(clk,1,, @(posedge clk)));  
// ##8 is to take care of the $past at startup. Use whateve ##n you need. 


    initial begin 
       bit va, vb; 
      repeat(200) begin 
        @(posedge clk);   
        if (!randomize(va, vb)  with 
        { va dist {1'b1:=1, 1'b0:=3};
          vb dist {1'b1:=1, 1'b0:=2};      
      }) `uvm_error("MYERR", "This is a randomize error")
       a <= va; 
       b <= vb;
    end 
    $stop; 
  end 
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

See Paper: 1) VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
2) http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf