Hi,
As a part of my verification environment I try to check with assertion the following constraint:
“The output remain stable until the next result_valid is rising again (not include the cycle of rising result_valid)”
My property is:
property RESULT_STABILITY(signal);
@(posedge clk) disable iff (~resetn)
($rose(result_valid)) |-> stable(signal)[*1:] ##0 ($rose(result_valid));
endproperty: RESULT_STABILITY
This property is wrong because the output signal is changing in same cycle the result_valid is rising, and hence the property is not compatible with the end of the constraint
My guess is that the right solution somehow involve the $past function, but I don’t know how.
Any help?
Hi Ben,
Thank you for your quick response.
I have some questions about your solution: sigtype v;
(rose(result_valid)) |-> ##1 **(1,v=sig)** ##1 v==sig[*0:] ##1 ($rose(result_valid));
In reply to akivama:
1800 defines one of options for a sequence as:
sequence_expr ::=
| (sequence_expr {, sequence_match_item}) [sequence_abbrev]
For example:
property p;
int v;
(a , v=data) [*2] |-> ##1 sig==data;
// (sequence_expr {, sequence_match_item}) [sequence_abbrev]
endproperty
// for your example:
bit[15:0] sig;
property p;
bit[15:0] v; // same type as the type for sig
($rose(result_valid)) |->
##1 (1,v=sig) ##1 v==sig[*0:$] ##1 ($rose(result_valid));
// The "1" in (1, v=sig) is the sequence_expr, alwasy true to set the local variable
