I want to write assertion to check the below property :-
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
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);
In reply to harsh pandya:
The concept of adding support logic is good.
I don’t believe that your solution works though.
FOr example, there is a requirement that This clock loss signal is de asserted at positive edge of reference clock The following does not even reference that signal.
(count > 64) |-> clk_lost[*1:$] ##1 (!clk_lost && count==0);
Ben
Thanks Ben,
Yes, you are correct.
I missed de assertion checking at reference clock spec requirement.
( Which covered via ap_clk_loss_reset in your example ).
One more doubt :
Even when EN_FLL = 1 if the REF_CLK is not toggling then the PROG_OUT_FLL bits should remain same as PROG_TRIM and the block should wait for REF_CLK to start the operation
1 0 Not toggling X PROG_TRIM Even when EN_FLL = 1
if the REF_CLK is
not toggling then
the PROG_OUT_FLL
bits should remain
same as PROG_TRIM
wait for REF_CLK to
start the operation
$past(expr1 [, number_of_ticks] [, expr2] [,clk_evnt])
// needed to add the clocking event in $past
initial begin
repeat(2) @(posedge i_mon_clk); // startup for $past, need 1 clk min
forever begin : fvr
@(posedge i_mon_clk);
if ((i_ref_clk) == $past(i_ref_clk, 1,,@(posedge i_mon_clk)) ) ref_clk_toggling<=1'b0;
else ref_clk_toggling<=1'b1;
end : fvr
end
ap_ref_clk16: assert property(@(posedge i_ref_clk) ($rose(refclk_en_fll_sync) && i_refclk_div == 4'b0100) |->
refclk_output==!$past(refclk_output,8));[/systemverilog
Is their any better approch to write the assertion for different value of refclk_div (supported till divide by 32768 i.e. refclk_div == 4'b1111 )
ap_ref_clk16: assert property(@(posedge i_ref_clk) ($rose(refclk_en_fll_sync) && i_refclk_div == 4'b0100) |->
refclk_output==!$past(refclk_output,8));[/systemverilog
Is their any better approch to write the assertion for different value of refclk_div (supported till divide by 32768 i.e. refclk_div == 4'b1111 )
In reply to rkg_:
If $past(var) is X its value is like a ZERO, or a no-match for that element of the sequence.
I am not trying to be facetious, but many of these language issues or uncertainties can easily be answered in simulation with very simple testbenches. The probability that the simulator understands SystemVerilog is much higher than yours, particularly since the language has matured. Here is a simple model that I created for the**$past(a)** where “a” transitions form Xs to 1/0.
module top;
`include "uvm_macros.svh"
import uvm_pkg::*;
logic clk=1'b1, a, b;
initial forever #10 clk = !clk;
ap: assert property(@ (posedge clk) ##1 1 |-> a==$past(a, 1));
initial begin
#100;
repeat (20) begin
@(posedge clk);
if (!randomize(a, b) with {
a dist {1'b1 := 1, 1'b0 := 1};
b dist {1'b1 := 1, 1'b0 := 2};
})
`uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule