PDR bug? Invariant does not imply the proved property

[zhanghongce]

The design (attached) is converted from Verilog to Blif (by Yosys).
It is a 2-bit register that can only be updated to 3 or 0, based on other signals. It looks like this:

always @(posedge clk) begin
    if (rst) begin
      reg_mstatus_mpp <= rst_mstatus_mpp;
    end else begin
      if (wen) begin
        if (T_5098) begin
          if (T_6142) begin
            reg_mstatus_mpp <= 2'h3;
          end else begin
            reg_mstatus_mpp <= 2'h0;
          end
        end else begin
          if (insn_ret) begin
            if (T_5454) begin
              reg_mstatus_mpp <= 2'h0;
...

And the property to prove is this register should not be 1 (2'b01)

When the initial value is 00:

abc 01> read_blif wrapper_init00.blif
abc 02> strash
abc 03> pdr
Invariant F[2] : 1 clauses with 2 flops (out of 10) (cex = 0, ave = 2.00)
Verification of invariant with 1 clauses was successful.  Time =     0.00 sec
Property proved.  Time =     0.01 sec
abc 03> inv_print
Invariant contains 1 clauses with 2 literals and 2 flops (out of 10).
abc 03> inv_print -v
Invariant contains 1 clauses with 2 literals and 2 flops (out of 10).
10 1
abc 03> ***EOF***

This is as expected.

When initial value is 11:

UC Berkeley, ABC 1.01 (compiled Apr 30 2019 02:29:30)
abc 01> read_blif wrapper_init11.blif
abc 02> strash
abc 03> pdr
Invariant F[1] : 1 clauses with 2 flops (out of 10) (cex = 0, ave = 2.00)
Verification of invariant with 1 clauses was successful.  Time =     0.00 sec
Property proved.  Time =     0.01 sec
abc 03> inv_print -v
Invariant contains 1 clauses with 2 literals and 2 flops (out of 10).
01 1

This can be interpreted as reg_mstatus_mpp != 2'b10 , which does not imply reg_mstatus_mpp != 2'b01

test.zip

[zhanghongce]

I was wondering, is it the case that

1. the ordering of latches differs according to the initial value, or
2. the interpretation of the printed clauses differs according to their initial value?

Thanks!

[alanminko]

The problem has likely something to do with the initialization of latches.   In ABC, there is command "zero", which should be called after "strash" before using sequential AIG for verification, because it converts initial values properly.  However, when I added "zero", the result was the same. It is possible that the invariant has to be interpreted differently after "zero", which essentially retimes the flops over an inverter.  In which case the values of the literals in the invariant may have to be complemented...  I am not sure about this because I haven't look into similar issues for a while. Please let me know if the above helps clarify it.  If not, I will look at it more closely next week.  Currently I am traveling.

…

On 5/18/2019 11:23 PM, Hongce Zhang wrote: The design (attached) is converted from Verilog to Blif (by Yosys). It is a 2-bit register that can only be updated to 3 or 0, based on other signals. It looks like this: |always @(posedge clk) begin if (rst) begin reg_mstatus_mpp <= rst_mstatus_mpp; end else begin if (wen) begin if (T_5098) begin if (T_6142) begin reg_mstatus_mpp <= 2'h3; end else begin reg_mstatus_mpp <= 2'h0; end end else begin if (insn_ret) begin if (T_5454) begin reg_mstatus_mpp <= 2'h0; ... | And the property to prove is this register should not be 1 (2'b01) When the initial value is 00: |abc 01> read_blif wrapper_init00.blif abc 02> strash abc 03> pdr Invariant F[2] : 1 clauses with 2 flops (out of 10) (cex = 0, ave = 2.00) Verification of invariant with 1 clauses was successful. Time = 0.00 sec Property proved. Time = 0.01 sec abc 03> inv_print Invariant contains 1 clauses with 2 literals and 2 flops (out of 10). abc 03> inv_print -v Invariant contains 1 clauses with 2 literals and 2 flops (out of 10). 10 1 abc 03> ***EOF*** | This is as expected. When initial value is 11: |UC Berkeley, ABC 1.01 (compiled Apr 30 2019 02:29:30) abc 01> read_blif wrapper_init11.blif abc 02> strash abc 03> pdr Invariant F[1] : 1 clauses with 2 flops (out of 10) (cex = 0, ave = 2.00) Verification of invariant with 1 clauses was successful. Time = 0.00 sec Property proved. Time = 0.01 sec abc 03> inv_print -v Invariant contains 1 clauses with 2 literals and 2 flops (out of 10). 01 1 | This can be interpreted as |reg_mstatus_mpp != 2'b10| , which does not imply |reg_mstatus_mpp != 2'b01| test.zip <https://github.com/berkeley-abc/abc/files/3194151/test.zip> — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#40?email_source=notifications&email_token=AI4DBXSXCVD72XCEGO4V6FDPWAGPNA5CNFSM4HN2MR42YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4GURFBFA>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AI4DBXS7TQ4E5S3MYHHTMA3PWAGPNANCNFSM4HN2MR4Q>.

[alanminko]

1. The initial value is not related to the ordering. 2. It is possible that after converting initial values to 0 (which is required by "pdr"), the invariant needs to be interpreted differently. I am not sure about this.

…

On 5/19/2019 5:35 AM, Hongce Zhang wrote: I was wondering, is it the case that 1. the ordering of latches differs according to the initial value, or 2. the interpretation of the printed clauses differs according to their initial value? Thanks! — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#40?email_source=notifications&email_token=AI4DBXTDYY7RRJ2AN55N3UDPWBSA7A5CNFSM4HN2MR42YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODVWVRWI#issuecomment-493705433>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AI4DBXR3QKRB44YKBJASU5DPWBSA7ANCNFSM4HN2MR4Q>.

[zhanghongce]

Thank you for your reply and thanks for the info!
I currently treat the literals with corresponding initial value 1 as being complemented and this looks okay (haven't found any problem till now). So I think this helps clarify it, and thank you very much!