Counter assertion

SystemVerilog
1

Hi,

`timescale 1us/1ns
module clk_gen();
   reg clk_tb;
   real clk_period_tb = 0.04 ;
   integer count ;
initial begin
	   clk_tb=0;
	   count  = 0;
   end

   always #0.02 clk_tb = ~clk_tb;
   always @(posedge clk_tb) begin
	   if(count < 7)
		  begin
		#15 count  = count+1; 
                   end
	    else if(count == 7)
	    begin
		#15    count = 0;
	    end
   end
   initial
   begin
	   $monitor($time,"clk =%d",clk_tb);
	   #1000;
	   $finish;
   end
   
endmodule

I write this code for counting the clock clock after 15us.Now I don’t know how to write assertion for checking whether the counter is incremented every 15us as well as assert the counter should be reset when it reaches 7 and again it should count from zero

thanks
kani

2

In reply to kanimozhi:
Your code is very poorly written, and from what I see you need strong fundamentals in digital design. I thus strongly believe that you’ll benefit from my book
Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
I just put a promotion at Amazon.com the book is free from 9/18/21 - 9/22/21; it will be $3 afterward. See TOC at http://systemverilog.us/RealChipDesign_preface.pdf

This link is an example for a complex counter, along with assertions
http://systemverilog.us/vf/counter_rtlOK.sv

Code below:


// requirements: 
    // Loadable counter, reset to 0 if reset_n==0, 
    // Min count -2, Max count ==5 
    // This is an activity counter, thus count must change at least 
    // every 8 cycles 
    // module counter_max #(MAX_COUNT=9, MIN_COUNT=2)(  
    module counter_max (  
            input logic[3:0] data_in, 
            input logic ld, 
            output logic[3:0] counter, 
            input logic clk, rst_n) ;
        import counter_pkg::*;
        int cover_count=0; 
        int fail_count=0; 
        // ap_P:  assert property(@ (posedge clk) P ) 
   
        // parameter MIN_COUNT=2; // module item parameter
        // If use of parameter port list, then can't use defparam 
        default disable iff !rst_n;                     
        property p_load;
            logic[3:0] v_data_in; // local variable to property 
            (ld && (data_in>= MIN_COUNT && data_in <= MAX_COUNT), v_data_in=data_in) |=> 
            counter==v_data_in;
        endproperty : p_load
        ap_load: assert property ( @(posedge clk) p_load); 
        	
        property p_hold_on_load;
            ld && (data_in< MIN_COUNT || data_in > MAX_COUNT) |=> 
            $stable(counter);
        endproperty : p_hold_on_load 
        ap_hold_on_load: assert property ( @(posedge clk) p_hold_on_load);          	
        	
        ap_count: assert property(@(posedge clk) 
                !ld && (counter!=MAX_COUNT) |=> counter==$past(counter)+1'b1);
                            
        ap_hold: assert property(@(posedge clk) 
                !ld && counter==MAX_COUNT |=> counter==$past(counter)); 
                
        mp_min_load: assume property(@(posedge clk)  
            ld |-> not(data_in<MIN_COUNT)); 
        
        mp_max_load: assume property(@ (posedge clk) 
            ld |-> not(data_in > MAX_COUNT))
        cover_count++; else fail_count++ ;         	
                
        ap_statble8: assume property(@(posedge clk) 
            $stable(counter)|-> ##[1:8] !$stable(counter));
            
        ap_reset: assert property(@ (posedge clk) disable iff (1'b0) 
        	 !rst_n |=> counter==MIN_COUNT);
    		
        always @(posedge clk) begin : counter1
            if(!rst_n) counter <= MIN_COUNT; 
            else if (ld && data_in >= MIN_COUNT && data_in <= MAX_COUNT) 
                counter <= data_in;
            else if (!ld && counter!=MAX_COUNT) begin : counter2
                counter <= counter + 1'b1;
            end : counter2
        end : counter1
	
    endmodule : counter_max

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

3 

HI All, 

Question_1 : 
Assertion requirement : When Enable is HIGH, counter should be increment to previous clock cycle value, when Enable is LOW, counter should keep same value as previous cycle. 

Below is my understanding. May I know is this satisfying the requirement or require changes?

property p1;
@(posedge clk)
Enable |=> (count == $past(count+1));
endproperty

Question_2 : also, do we require one more property for else condition. Like

property p2;
@(posedge clk)
(!Enable) |=> (count == $past(count));
endproperty

Is only one property (p1) is sufficient for above requirement. 

Kindly suggest