How to write assertions for a Clock divider

SystemVerilog
1

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?

1 Like
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

3

In reply to yoshiko:

You can use the local variable in assertions and apply checks for consecutive rising edge and consecutive falling edge. For example : -
if you have to check div/VALUE , where VALUE=2 then you can write the following

property o_clk_even_rose_div(div_clk , n) ; 
 int local_cnte;
  @(posedge i_clk ) disable iff (~div_reset_check) 
($rose(div_clk[n]) ,local_cnte=0) |=> (1'b1,local_cnte=local_cnte+1)[*1:$] ##0 (local_cnte==VALUE/2) ##0 $fell(div_clk[n]);

endproperty

similarly you can write for the falling edge this will take care of your duty cycle.
In the case of odd division type
apply the assertion for posedge and the negedge and local_cnt will be equal to VALUE and not VALUE/2 in case of odd division.

PS:CHECK FOR SYNTAX

Prashant

4

In reply to pk_94:

That assertion can never fail because of the [*1:$] as there are other threads to test if any thread fails.
Ben systemverilog.us

5

In reply to ben@SystemVerilog.us:

This assertion is properly working. Suppose for VALUE=4 ,that is div/4 ,the local counter will start incrementing , and when the local_counter is equal to value/2 , it will check the falling edge of the divider,and if the divider do not falls for that ,it will give error. I missed to apply the first_match above.It should be : -

($rose(div_clk[n]) ,local_cnte=0) |=> first_match((1'b1,local_cnte=local_cnte+1)[*1:$] ##0 (local_cnte==VALUE/2)) ##0 $fell(div_clk[n]);

6

In reply to pk_94:


($rose(div_clk[n]) ,local_cnte=0) |=> ((1'b1,local_cnte=local_cnte+1)[*1:$] ##0 (local_cnte==VALUE/2)) ##0 $fell(div_clk[n]);
If (local_cnte==VALUE/2) is true and in the same cycle $fell(div_clk[n] is false, the consequent will keep on trying for another thread.  Specifically, an assertion of the form: 
(a, v=k) |=> (1, v=v+1)[*1:$] ##0 v==x ##0 b; // is same as 
(a, v=k) |=? (1, v=v+1)[*1] ##0 v==x   ##0 b or
      (1, v=v+1)[*2] ##0 v==x   ##0 b or 
      (1, v=v+1)1[*3]##0 v==x ##0 b or 
      .......
      (1, v=v+1)[*n] ##0 v==x##0 b; // where n is infinity/ 
Thus, if any of the thread fails, the simulator will try other threads. 
The first_match() traps the 1st good condition when v==x, and then tests of the b. 
If b==0, assertion fails. thus, 
(a, v=k) |=> first_match((1, v=v+1)[*1:$] ##0 v==x) ##0 b;

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

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
7

In reply to ben@SystemVerilog.us:

I agreed. Then I can modify the following assertion to the following , where repetition is fixed depending on the VALUE.

($rose(div_clk[n]) ,local_cnte=0) |=> first_match((1’b1,local_cnte=local_cnte+1)[*(VALUE/2)])##0 $fell(div_clk[n]);

Here the repetition is fixed so for only one thread condition will be checked and if $fell is not met the assertion will fail.

8

In reply to pk_94:


//structurally, the first_match() is not needed here 
($rose(div_clk[n]) ,local_cnte=0) |=> first_match((1'b1,local_cnte=local_cnte+1)[*(VALUE/2)])##0 $fell(div_clk[n]);

// But the above is same as 
let MY_DELAY = VALUE; // VALUE is a constant 
$rose(div_clk[n]) |=> ##MY_DELAY $fell(div_clk[n]);

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

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
9

In reply to ben@SystemVerilog.us:

Yes agreed , that first match is not needed here.
I also tried your solution but it gives me compile error : -
// But the above is same as

property even_rose_div(clk_div , n) ;
let MY_DELAY = VALUE[2*n+:2] ; // VALUE is a constant
$rose(div_clk[n]) |=> ##MY_DELAY $fell(div_clk[n]);

Here value is coming from parameter ,where n is an argument. But it is giving me compile error.
*E :- Expected specification terminator “;”.

I think the local variable is the best way to check divider.

10

In reply to pk_94:
I did not write a separate property, just a direct assertion.
If you need arguments, then write a full property


let n=3;
let MY_DELAY = VALUE[2*n+:2] ; // VALUE is a constant 
property p_even_rose_div(clk_div , n) ; 
  $rose(div_clk[n]) |=> ##MY_DELAY $fell(div_clk[n]); 
endproperty 
ap_even_rose_div: assert property(p_even_rose_div(some_clk, 4);  
// syntaxed not checked, looks OK though

If you want dynakic delay, see my papers (1 and 2 referenced below).
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
11

In reply to ben@SystemVerilog.us:

Hi Ben,

Could you please let me know in brief of the below mentioned line.
ap_clk2: assert property(##8 1’b1 |-> @ (negedge clk) !$past(clk,1, @(posedge clk)));

12

In reply to sudharshan:
Iwouldn’t use that assertion.
Ben

13

for a clock divider circuit by 3/5/7… is it possible to write a generic property

please help me out
Thanks in advance

Kind regards,
Sudharshan

14

In reply to yoshiko:

Assuming your clock divider provides a single master clock pulse every 3rd, 5th, 7th clock


bit clk, b, c; // b is divide by 3, c is divide by 5
property divide(bit a, int n); 
  @(posedge clk) $rose(a) |=> !a[*n-1] ##1 $rose(a); 
endproperty 
ap_div3: assert property(@ (posedge clk) divide(b, 3);  
ap_div5: assert property(@ (posedge clk) divide(c, 5);

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

  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment
1 Like
15

Hi Ben,

Could you please help me understand what is “b” and “c” in the above property? I can see that you are already using “clk” (which I believe is the master clock pulse)

16

b is divide by 3, c is divide by 5