Hello all
I was trying to write an assertion for SPI, if CS goes low, the “hold” and “wp” has to be 1 until CS goes high. it was not giving any error but the assertion was not finished. it was active even CS goes high.
property quadspi_support;
@(clk_out)
!cs_n_out |-> !cs_n_out throughout (hold_n_out == 1 && wp_n_out == 1) until ($rose(cs_n_out));
endproperty
In reply to Malai_21:
3.10.2 until
An until property can be of many forms: strong or weak, and of overlapping or non-overlapping :
Weak non-overlapping form property_expr1 until property_expr2
Strong non-overlapping form property_expr1 s_until property_expr2
weak overlapping form property_expr1 until_with property_expr2
strong overlapping form property_expr1 s_until_with property_expr2
Rule: [1] An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.
// if CS goes low, the "hold" and "wp" has to be 1 until CS goes high.
// it was not giving any error but the assertion was not finished.
// it was active even CS goes high.
property quadspi_support;
@(clk_out)
$fell(cs_n_out) |-> (hold_n_out == 1 && wp_n_out == 1) until ($rose(cs_n_out));
endproperty
property quadspi_support2;
@(clk_out)
!cs_n_out |-> (hold_n_out == 1 && wp_n_out == 1)[*1:$] ##1 ($rose(cs_n_out));
endproperty