Regarding the assertion checking

SystemVerilog
, , ,
7

In reply to venkatasubbarao:
A few comments:

  1. help me to understand my setup check for both anticident and consiquent

if(CK_EDGE_SEL)
$fell(strb_in)  |->  $stable(data)[*HOLD_TIME]
else
$rose(strb_in)  |->  $stable(data)[*HOLD_TIME];
States that if the sampled value of CK_EDGE_SEL==1, then at that cycle, a $fell(strb_in)would require that data is same as it was in past cycle for HOLD_time==1.
IF HOLD_TIME==2, then a $fell(strb_in)would require that data is
the same as it was in the past cycle and in the next cycle. Thus, for hold time ==2 the current data ==$past(data) and data at next cycle is same as current data.
  1. in " |-> ##0 " the ##0 add nothing, not even for syntax. The ##0 just says the current cycle.
  2. The following is a poorly written assertion because the assertion is vacuous if the antecedent is false, and false otherwise. It is also simulation load intensive as at every clock you have an attempt. Also, one of the attempts would fail if data ever changed at the fell(strb_in). Remember, at every attempt you start a new thread. BTW,the intersect requires a sequence, like $fell(strb_in)[->1]

ap_BAD_structure: assert property(@ (posedge clk_in)
##[0:SETUP_TIME] $changed(data) intersect $fell(strb_in)[->1] |-> 0);
  1. I prefer forward looking assertion, and smaller assertions. I would break the “if else” to 2 separate assertions as it is easier to debug and read.

Code below compiled and elaborated OK.


module top;
    bit clk_in, strb_in, data, CK_EDGE_SEL; 
    parameter HOLD_TIME=5, SETUP_TIME=5;
    property hold_checker;
        @(posedge clk_in)
        //disable iff (~resetn || disable_assertion)
        
        if(CK_EDGE_SEL)   
        $fell(strb_in)  |->  $stable(data)[*HOLD_TIME] 
        else    	 
        $rose(strb_in)  |->  $stable(data)[*HOLD_TIME];  
    endproperty
    
    
    property setup_checker;
        @(posedge clk_in)          
        //disable iff (~resetn || disable_assertion)
        if(CK_EDGE_SEL)   
        $fell(strb_in) |->  $past(data)[*SETUP_TIME] 
        else    	 
        $rose(strb_in) |->  $past(data)[*SETUP_TIME] ;
    endproperty 

property hold_checker1;
    @(posedge clk_in)
    //disable iff (~resetn || disable_assertion)
    if(CK_EDGE_SEL)   
    $fell(strb_in)  |-> $stable(data)[*HOLD_TIME]   
	else    	 
    $rose(strb_in)  |-> $stable(data)[*HOLD_TIME];  
endproperty
//You simplify this and remove the if/else entirely. 
property hold_checker2;
    @(posedge clk_in)
    //disable iff (~resetn || disable_assertion)
    $fell(strb_in^CK_EDGE_SEL)  |-> $stable(data)[*HOLD_TIME] ;  
endproperty

//Oh, if HOLD_TIME is 0, you need ##0.
//For your setup check, you need to use an implication such that when the antecedent(LHS) is true, the assertion fails.
ap_BAD_structure: assert property(@ (posedge clk_in)   
  ##[0:SETUP_TIME] $changed(data) intersect $fell(strb_in)[->1] |-> 0);

 
endmodule