Regarding the assertion checking

Following are the questions

  1. I have written a property for assertion as follows, property checks for setup and hold between strobe and data. Basically, I am trying to check when a strobe is at falling edge on the same clock data should be stable for 10 cycles in the past and future note=(10 is a parameter value HOLD_TIME/SETUP_TIME )
  2. I’m using if else in the property so that I can make strobe for falling edge and rising edge i.e if CK_EDGE_SEL=1 it will check for falling edge strobe else it will check for negative edge strobe.
  3. I am getting error for begin and end ,else in the property , can any one suggest me why
property hold_checker;
   @(posedge clk_in)
   disable iff (~resetn || disable_assertion)
   
    	if(CK_EDGE_SEL)   
    	begin
          $fell(strb_in)  |-> ##0 $stable(data)[*HOLD_TIME] ;  
         end 
	else    	 
	begin
	  $rose(strb_in)  |-> ##0 $stable(data)[*HOLD_TIME];  
	end
  endproperty
   
   
  property setup_checker;
   @(posedge clk_in)          
   disable iff (~resetn || disable_assertion)
   
	if(CK_EDGE_SEL)   
	begin
           $fell(strb_in) |-> ##0 $past(data)[*SETUP_TIME] 
	  
	end 
        else    	 
	begin
	  $rose(strb_in) |-> ##0 $past(data)[*SETUP_TIME] ;
	end
  endproperty 

In reply to venkatasubbarao:

You do not use begin/end in a property; it is not procedural code. You are selecting property expressions. Also, do not put ##0 at the beginning of a sequence; it does not do anything. You use it to concatenate two sequences.

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

You simplify this and remove the if/else entirely.

property hold_checker;
   @(posedge clk_in)
   disable iff (~resetn || disable_assertion)
       $fell(strb_in^CK_EDGE_SEL)  |-> $stable(data)[*HOLD_TIME] ;  
endproperty

Your setup checker does not do what you specified at all.

In reply to dave_59:

So according to you what should be my setup checker, could you please inform me?

and I hope hold checker is fine right?

In reply to dave_59:

and moreover, if I don’t use ##0 at the consequent then it gives following error always period.

Error-[SVA-SEQPROPEMPTYMATCH] Invalid sequence as property
/vobs/asic_adc_dac_testchip/hydra_t/SE/assertions/hydra_t_strobe_assertions.sv, 112
“($stable(data) [* HOLD_TIME])”
A sequence that is used as property must be non-degenerate and admit no
empty match.

In reply to venkatasubbarao:

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.

##[0:SETUP_TIME] $changed(data) intersect $fell(strb_in) |-> 0

This may not be correct, but should get you going in the right direction.

In reply to dave_59:

could you please help me to understand my setup check for both anticident and consiquent, i have run out of options and not able to figure out i am just stuck in the loop not going anywhere…?

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  

In reply to ben@SystemVerilog.us:

Thank you for your time, sir.