CODEWITHSUNDEEP
system-verilogsystem-verilog-assertions
nachum
nachum

Reputation: 567

when are assertion "disable iff" values evaluated?

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.

Upvotes: 5

Views: 11346

Answers (1)

dave_59
dave_59

Reputation: 42623

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.

Upvotes: 5

Related Questions