{"action":"closed","issue":{"url":"https://api.github.com/repos/YosysHQ/SymbiYosys/issues/59","repository_url":"https://api.github.com/repos/YosysHQ/SymbiYosys","labels_url":"https://api.github.com/repos/YosysHQ/SymbiYosys/issues/59/labels{/name}","comments_url":"https://api.github.com/repos/YosysHQ/SymbiYosys/issues/59/comments","events_url":"https://api.github.com/repos/YosysHQ/SymbiYosys/issues/59/events","html_url":"https://github.com/YosysHQ/SymbiYosys/issues/59","id":488166384,"node_id":"MDU6SXNzdWU0ODgxNjYzODQ=","number":59,"title":"fib liveness example non functional","user":{"login":"lighteningfingers","id":36622660,"node_id":"MDQ6VXNlcjM2NjIyNjYw","avatar_url":"https://avatars0.githubusercontent.com/u/36622660?v=4","gravatar_id":"","url":"https://api.github.com/users/lighteningfingers","html_url":"https://github.com/lighteningfingers","followers_url":"https://api.github.com/users/lighteningfingers/followers","following_url":"https://api.github.com/users/lighteningfingers/following{/other_user}","gists_url":"https://api.github.com/users/lighteningfingers/gists{/gist_id}","starred_url":"https://api.github.com/users/lighteningfingers/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/lighteningfingers/subscriptions","organizations_url":"https://api.github.com/users/lighteningfingers/orgs","repos_url":"https://api.github.com/users/lighteningfingers/repos","events_url":"https://api.github.com/users/lighteningfingers/events{/privacy}","received_events_url":"https://api.github.com/users/lighteningfingers/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2019-09-02T12:29:37Z","updated_at":"2019-09-05T16:14:29Z","closed_at":"2019-09-05T16:14:29Z","author_association":"NONE","body":"I have been experimenting with some liveness proofs and have resorted to running the \"fib\" example presented in many slide presentations for symbiyosys:\r\n\r\n\r\n```\r\nmodule fib(\r\n    input clk, pause, start,\r\n    input [3:0] n,\r\n    output reg busy, done,\r\n    output reg [9:0] f\r\n);\r\n\r\nreg [3:0] count;\r\nreg [9:0] q;\r\n\r\ninitial begin\r\n    done = 0;\r\n    busy = 0;\r\nend\r\n\r\nalways @(posedge clk) begin\r\n    done <= 0;\r\n    if (!pause) begin\r\n        if (!busy) begin\r\n            if (start) busy <= 1;\r\n            count <= 0;\r\n            q <= 1;\r\n            f <= 0;\r\n        end\r\n        else begin\r\n            q <= f;\r\n            f <= f + q;\r\n            count <= count + 1;\r\n            if (count == n) begin\r\n                busy <= 0;\r\n                done <= 1;\r\n            end\r\n        end\r\n    end\r\nend\r\n\r\n`ifdef FORMAL\r\n    always @(posedge clk) begin\r\n        if (busy) begin\r\n            assume (!start); assume ($stable(n));\r\n        end\r\n        if (done) begin\r\n            case ($past(n))\r\n                0: assert (f == 1);\r\n                1: assert (f == 1);\r\n                2: assert (f == 2);\r\n                3: assert (f == 3);\r\n                4: assert (f == 5);\r\n                //5: assert (f == 8);\r\n                5: assert (f == 300);               // prove fail\r\n            endcase\r\n            cover (f == 13);\r\n            cover (f == 144);\r\n            cover ($past(n) == 15); end\r\n            assume (s_eventually !pause);\r\n            if (start && !pause) assert (s_eventually done);\r\n        end\r\n`endif\r\n\r\nendmodule\r\n```\r\n\r\n\r\nwhere the script is:\r\n```\r\n[options]\r\n#mode prove\r\nmode live\r\n\r\n[engines]\r\naiger suprove\r\n\r\n[script]\r\nread -formal fib.v\r\nprep -top fib\r\n\r\n[files]\r\nfib.v\r\n```\r\n\r\nwhen running the proof as presented, I get the following tool response which is not expected:\r\n```\r\n$ sby -f fib.sby\r\nSBY 13:22:26 [fib] Removing direcory 'fib'.\r\nSBY 13:22:26 [fib] Copy 'fib.v' to 'fib/src/fib.v'.\r\nSBY 13:22:26 [fib] engine_0: aiger suprove\r\nSBY 13:22:26 [fib] nomem: starting process \"cd fib/src; yosys -ql ../model/design_nomem.log ../model/design_nomem.ys\"\r\nSBY 13:22:26 [fib] nomem: finished (returncode=0)\r\nSBY 13:22:26 [fib] aig: starting process \"cd fib/model; yosys -ql design_aiger.log design_aiger.ys\"\r\nSBY 13:22:27 [fib] aig: finished (returncode=0)\r\nSBY 13:22:27 [fib] engine_0: starting process \"cd fib; suprove +simple_liveness model/design_aiger.aig\"\r\nSBY 13:22:27 [fib] engine_0: finished (returncode=0)\r\nSBY 13:22:27 [fib] engine_0: Status returned by engine: FAIL\r\nSBY 13:22:27 [fib] engine_0: Engine did not produce a counter example.\r\nSBY 13:22:27 [fib] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)\r\nSBY 13:22:27 [fib] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)\r\nSBY 13:22:27 [fib] summary: engine_0 (aiger suprove) returned FAIL\r\nSBY 13:22:27 [fib] DONE (FAIL, rc=2)\r\n```\r\n\r\nI would have expected a pass (?) with the example as delivered.\r\nI have run other proofs with other engines (such as \"prove and cove\" with yices.\r\nBoth generate outputs from the tool as expected for this example.\r\n\r\n\r\nShould this example demonstrate the liveness proof success/pass as written?\r\n\r\n"}}
{"actor":{"display_login":"cliffordwolf"}}