5

For this code, I see both assertions fail. It seems that disable iff (value) is evaluated later than the expression itself. Can someone explain this.

module tb();
reg clk = 1;
always #5 clk = !clk;
reg rst = 1;
always @ (posedge clk)
    rst <= 0;

initial #11ns $finish();

assert property (@ (posedge clk) disable iff (rst) 1 |-> 0);
assert property (@ (posedge clk) rst |-> 0);
endmodule

Followup, how would one test this:

always_ff @ (posedge clk or posedge rst) begin
    if (rst) q <= 0;
    else q <= d;
end

where rst is deasserted based on a delay:

always_ff @ (posedge clk)
    rst <= rst_a;

Seems like disable iff would no longer work. as it evaluates rst late.

nachum
  • 567
  • 9
  • 17

1 Answers1

5

The expression within disable iff (expr) is asynchronous and uses unsampled values. The property gets evaluated as part of the observed region, which comes after the NBA region.

For the first assertion, rst is already low by the time of the first attempt to evaluate the property at time 10 in the observed region. So the disable iff does not prevent an attempt to evaluate the property, which always fails.

For the second property, the sampled value of rst is still 1 at the time of the first attempt to evaluate the property, so it must fail too.

Followup,

I think you may be worrying about an impractical case. How likely will the antecedent be true after reset? And if it were true, then the assertion should be still be valid. For example, suppose you had a counter with an assertion to check that it rolls over when hitting the maximum value

assert property (@ (posedge clk) disable iff (rst) (counter==maxval) |=> (counter ==0) );

If the reset value of the counter was the maximum value, you would not want the assertion disabled.

dave_59
  • 39,096
  • 3
  • 24
  • 63
  • Can you please point me to the portion of the standard that says disable iff (expr) is evaluated at observed time. – nachum Apr 18 '18 at 18:04
  • I did not say that. See page 423 of the 1800-2017 LRM. Basically the expression gets evaluated inclusively between the start and end attempts of the property using unsampled values. It is asynchronous in-between the start and end attempts. But your property happens to be a single clock cycle, so all that matters is that `rst` is already 0 by the time of the first attempt to evaluate the property in the observed region. – dave_59 Apr 18 '18 at 18:25
  • So disable iff evaluates continuously and begins starting at the observed region of the same clock. that makes sense. Can you explain then how one would disable a property when reset is deasserted without a delay using non-blocking assignment? Added code to question. – nachum Apr 18 '18 at 21:39
  • What about the simplest case of testing a d flip-flop? I want to make sure q is equal to d one clock later except in the case of reset. In my case I was writing code for a clock gate (to get my feet wet). – nachum Apr 18 '18 at 22:48
  • Move the change of reset away from the posedge clock, like on the negedge. That is a good practice for all your stimulus. – dave_59 Apr 18 '18 at 22:52
  • I feel we are going around in circles. Thanks for the answers. It does clarify a bunch of things. – nachum Apr 18 '18 at 22:54