Assertion :- check the signal is asserted whenever count value exceed to 64

SystemVerilog
,
2

In reply to rkg_:
Consider the following; you may have to adjust the 64 (63? 65?)


/* Requirements: whenever count value exceeds 64 , this implies that reference clock is lost and 
  clock loss signal is asserted . 
  This clock loss signal is de asserted at positive edge of reference clock
*/

// Assertion: Two things to consider: 
// 1. the case when following a $rose (refclk_div) and before the incremented counter reaches 64
//    there is a new 2nd $rose (refclk_div).  That is legal, and the assertion should pass.
//    Note: the first $rose (refclk_div)considered the attempt and the antecedent is a match. 
//          The 2nd $rose (refclk_div) occurs in the consequent of that 1st attempt. 
//          At every $rose (refclk_div) there is a new attempt that matches.       
// 2. The case when there is no $rose (refclk_div) after the rhe 1st attempt and count >= 64. 
//    Here, clk_loss should be true. The first_match() is considered because without it
//    the counter will keep on counting waiting for clk_loss to be true.
//    (1'b1, count=count+1'b1)[*1:$] ##0 count>=64) ##0 (clk_loss == 1'b1) is equivalent to 
//    (1'b1, count=count+1'b1)[*1] ##0 count>=64) ##0 (clk_loss == 1'b1)  or 
//    (1'b1, count=count+1'b1)[*2] ##0 count>=64) ##0 (clk_loss == 1'b1)  or // false if count <64 
//     ..                                                                    // or clk_loss==0
//    (1'b1, count=count+1'b1)[*64] ##0 count>=64) ##0 (clk_loss == 1'b1)  or // flase if clk_loss==0
//    (1'b1, count=count+1'b1)[*65] ##0 count>=64) ##0 (clk_loss == 1'b1)  or 
//    (1'b1, count=count+1'b1)[*n] ##0 count>=64) ##0 (clk_loss == 1'b1)  
//    The other threads need to be considered. The first_match() takes care of the 
//    first occurrence of count>=64   
property clk_loss_check;
	int count;
	@(posedge tosc_clk)
    	disable iff( scan_mode || !EN_RLD) 
	    ($rose (refclk_div), count = 0) |->
                  (##[1:$]  $rose (refclk_div))   or 
                  (##1 first_match((1'b1, count=count+1'b1)[*1:$] ##0 count>=64)
                   ##0 clk_loss == 1'b1 );
endproperty
ap_clk_loss_check: assert property(clk_loss_check); 

ap_clk_loss_reset: assert property(@(posedge tosc_clk) $rose(clk_loss) |-> ##[1:3] ref_clk ## 0 clk_loss==1'b0);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** 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) https://rb.gy/cwy7nb
  3. Papers: