{"action":"closed","issue":{"url":"https://api.github.com/repos/berkeley-abc/abc/issues/40","repository_url":"https://api.github.com/repos/berkeley-abc/abc","labels_url":"https://api.github.com/repos/berkeley-abc/abc/issues/40/labels{/name}","comments_url":"https://api.github.com/repos/berkeley-abc/abc/issues/40/comments","events_url":"https://api.github.com/repos/berkeley-abc/abc/issues/40/events","html_url":"https://github.com/berkeley-abc/abc/issues/40","id":445720650,"node_id":"MDU6SXNzdWU0NDU3MjA2NTA=","number":40,"title":"PDR bug? Invariant does not imply the proved property","user":{"login":"zhanghongce","id":5318260,"node_id":"MDQ6VXNlcjUzMTgyNjA=","avatar_url":"https://avatars0.githubusercontent.com/u/5318260?v=4","gravatar_id":"","url":"https://api.github.com/users/zhanghongce","html_url":"https://github.com/zhanghongce","followers_url":"https://api.github.com/users/zhanghongce/followers","following_url":"https://api.github.com/users/zhanghongce/following{/other_user}","gists_url":"https://api.github.com/users/zhanghongce/gists{/gist_id}","starred_url":"https://api.github.com/users/zhanghongce/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/zhanghongce/subscriptions","organizations_url":"https://api.github.com/users/zhanghongce/orgs","repos_url":"https://api.github.com/users/zhanghongce/repos","events_url":"https://api.github.com/users/zhanghongce/events{/privacy}","received_events_url":"https://api.github.com/users/zhanghongce/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":4,"created_at":"2019-05-18T14:23:49Z","updated_at":"2019-05-19T19:49:52Z","closed_at":"2019-05-19T19:49:52Z","author_association":"NONE","body":"The design (attached) is converted from Verilog to Blif (by Yosys).\r\nIt is a 2-bit register that can only be updated to 3 or 0, based on other signals. It looks like this:\r\n\r\n```\r\n\r\nalways @(posedge clk) begin\r\n    if (rst) begin\r\n      reg_mstatus_mpp <= rst_mstatus_mpp;\r\n    end else begin\r\n      if (wen) begin\r\n        if (T_5098) begin\r\n          if (T_6142) begin\r\n            reg_mstatus_mpp <= 2'h3;\r\n          end else begin\r\n            reg_mstatus_mpp <= 2'h0;\r\n          end\r\n        end else begin\r\n          if (insn_ret) begin\r\n            if (T_5454) begin\r\n              reg_mstatus_mpp <= 2'h0;\r\n...\r\n```\r\n\r\n\r\nAnd the property to prove is this register should not be 1 (2'b01)\r\n\r\nWhen the initial value is 00:\r\n```\r\nabc 01> read_blif wrapper_init00.blif\r\nabc 02> strash\r\nabc 03> pdr\r\nInvariant F[2] : 1 clauses with 2 flops (out of 10) (cex = 0, ave = 2.00)\r\nVerification of invariant with 1 clauses was successful.  Time =     0.00 sec\r\nProperty proved.  Time =     0.01 sec\r\nabc 03> inv_print\r\nInvariant contains 1 clauses with 2 literals and 2 flops (out of 10).\r\nabc 03> inv_print -v\r\nInvariant contains 1 clauses with 2 literals and 2 flops (out of 10).\r\n10 1\r\nabc 03> ***EOF***\r\n```\r\nThis is as expected.\r\n\r\nWhen initial value is 11:\r\n```\r\nUC Berkeley, ABC 1.01 (compiled Apr 30 2019 02:29:30)\r\nabc 01> read_blif wrapper_init11.blif\r\nabc 02> strash\r\nabc 03> pdr\r\nInvariant F[1] : 1 clauses with 2 flops (out of 10) (cex = 0, ave = 2.00)\r\nVerification of invariant with 1 clauses was successful.  Time =     0.00 sec\r\nProperty proved.  Time =     0.01 sec\r\nabc 03> inv_print -v\r\nInvariant contains 1 clauses with 2 literals and 2 flops (out of 10).\r\n01 1\r\n```\r\n\r\nThis can be interpreted as `reg_mstatus_mpp != 2'b10` , which does not imply `reg_mstatus_mpp != 2'b01`\r\n\r\n[test.zip](https://github.com/berkeley-abc/abc/files/3194151/test.zip)\r\n\r\n"}}
{"actor":{"display_login":"zhanghongce"}}