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 )
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.
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
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.
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.
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…?
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.
in " |-> ##0 " the ##0 add nothing, not even for syntax. The ##0 just says the current cycle.
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]