How to verify clock divider using SVA

In reply to philerpeng:
You need to start with the requirements. Thus, for a 1/2 clock, you could first write something like: chall toggle

  1. Given a system master clock “clk”, there shall be a half clock “clk2” and a quarter clock “clk4”, all of which are generated from the master clock.
  2. “clk2” clock shall toggle at each posedge of the master clock “clk”, and its output shall have a maximum hold time of Xns.
  3. “Clk4” shall toggle when “clk2==0” at the posedge of the master clock “clk”. “clk4” output shall have a maximum hold time of Xns.

Once you have a spec, it becomes trivial to write assertions. Remember, the assertions are a reflection of the requirements.


// 
ap_clk2: assert property(@(posedge clk)  ##1 |-> clk2==!$past(clk2));
ap_clk4: assert property(@(posedge clk)  #2 clk2==0 |-> 
                          clk4==!$past(clk4,2));
// The antecedent ##1 and ##2 are just used for initialization, since the clk2 and clk4 have not started.  
// You need to look at the initial conditions. 
// This code is not tested, but it looks ok to me.  Needs testing anyway. 
 

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


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy