Race condition between two assertions

SystemVerilog
1

I have two properties a1 and a2. Whenever a,b,c and d are high , count should be incremented. Whenever a, b and e are high count should be decremented. In my case a,b,c,d and e all are high at the same instant. My expectation is that the count value should remain the same, since both properties are triggered and increment and decrement cancel out each other thereby keeping the count same. However does this not cause a case of race condition since any property triggering first expects the count to either increment/decrement thereby cause assertion error.

property a1;
    @(posedge clk) disable iff(!rstn)
    (a && b) && (c && d) |=> (count == ($past(count,1) + 1'b1));
endproperty

property a2;
   @(posedge clk) disable iff(!rstn)
    (a && b) && e |=> (count == ($past(count,1) - 1'b1));
endproperty
2

[Ben] There is no race condition. Your properties are incorrect
since the counter does not change when a,b,c,d and e all are high in the same cycle.
My take on your code:

    property a1;
        @(posedge clk) disable iff(!rstn)
        (a && b) && (c && d) |=> (count == ($past(count,1) + !$past(e))); // 1'b1));
    endproperty
    
    property a2;
       @(posedge clk) disable iff(!rstn)
        (a && b) && e |=> (count == ($past(count,1) -!$past(c && d))); //  1'b1));
    endproperty

en Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

3

Thanks Ben. I too recognized that it is my properties that are wrong.

4

Hello. I understood the solution, but I did not understand why the original question posted was wrong. Can you please detail me?

5

Hi Kaushal, what ben meant was the way i coded the properties caused the issue.

1 Like