In SVAs we have the concept of “disable iff” for purely asynchronous resets. However, what is the recommended way to handle a reset that is asynchronously set, but synchronously released?
Assume we have a property “A |=> B” and want to consider such a reset (active high). How would the complete property look like?
Version 1.)
If we do it like this:
property p_async_sync_reset;
@(posedge clk)
disable iff ( reset )
A |=> B;
endproperty
We may run into a race condition, if reset was high and is (synchronously) released, at an edge when A is sampled high. In such a case, the actual value of “reset” (as used inside disable iff) would already be 0 and the property would not be disabled.
Version 2.)
Do we have to model explicitly that “reset” is not high, when A is high?
property p_async_sync_reset;
@(posedge clk)
disable iff ( reset )
A && !reset |=> B;
endproperty
This would be quite tedious, since it would impact almost all assertions.
Version 3.)
Shall we use explicitly the sampled value of “reset” in the disable iff?
property p_async_sync_reset;
@(posedge clk)
disable iff ( $sampled(reset) )
A |=> B;
endproperty
Version 4.)
Or shall we use the accept_on operator instead of “disable if”?
property p_async_sync_reset;
@(posedge clk)
accept_on ( reset ) A |=> B;
endproperty
Or is there another way I have not thought about?
Is there any difference between the version 3.) and version 4.) in your eyes? If I understood it correctly, 3 would be “disabled” in case reset becomes active, while 4 would be “pass”.
ap0: assert property(@ (posedge clk) disable iff ( reset )
a |-> b) p0++; else f0++ ;
bit clk , reset=1, a=1, b; int p0, f0;
initial begin @(posedge clk); @ (posedge clk) begin
reset<= 0;
b<=1;
end
reset falls to 0 in the NBA region at t15
“a”, “b” are sampled in the Preponed Region at t15
(a |-> b) is evaluated in the Observed Region at t15, reset==0 in that region
$sample(a)==1
$sample(b)==0
Assertion fails at t15.
***Thus, your version 1 is good ***
thanks for your feedback.
However, I do not agree with your conclusion that version 1 is fine.
My expectation is that we do not see an assertion failure, if reset and b change at the same edge. Accordingly, I would assume that 2, 3, or 4 are the better ways to model it. In my eyes, number 3 would be the recommended way
[You] “My expectation is that we do not see an assertion failure, if reset and b change at the same edge.”
Your epectation is not what tools actually do.
The disable iff(reset) is ansynchronous. “reset” is NOT sampled here.
reset==0 in the NBA, bebore the Observed region where the assertion is processed. Thus, value of reset is seen as ZERO, in the inactive state.
Thus, whenreset fall, the sampled values of a, b are 0, and the assertion shown below fails in that cycle.
Ben, you missed my point.
I asked what is the best way to handle a reset that is synchronously released.
It is perfectly clear that reset==0 in the observed region and that the tools work as expected, when using “disable iff (reset)”.
However, this is not what is required for a reset that is synchronously released.
The best modelling from my perspective is “disable iff ($sampled(reset))”. I just wanted to know, if someone has a better suggestion to handle it.
In my eyes, asynchronously setting and synchronously releasing is the quasi-standard of handling resets. I have not seen any text book that describes this behavior nor I have not found any article that describes how to handle it.
