{"action":"created","issue":{"url":"https://api.github.com/repos/YosysHQ/yosys/issues/764","repository_url":"https://api.github.com/repos/YosysHQ/yosys","labels_url":"https://api.github.com/repos/YosysHQ/yosys/issues/764/labels{/name}","comments_url":"https://api.github.com/repos/YosysHQ/yosys/issues/764/comments","events_url":"https://api.github.com/repos/YosysHQ/yosys/issues/764/events","html_url":"https://github.com/YosysHQ/yosys/issues/764","id":393892278,"node_id":"MDU6SXNzdWUzOTM4OTIyNzg=","number":764,"title":"Double indirection not supported for memories?","user":{"login":"whitequark","id":54771,"node_id":"MDQ6VXNlcjU0Nzcx","avatar_url":"https://avatars1.githubusercontent.com/u/54771?v=4","gravatar_id":"","url":"https://api.github.com/users/whitequark","html_url":"https://github.com/whitequark","followers_url":"https://api.github.com/users/whitequark/followers","following_url":"https://api.github.com/users/whitequark/following{/other_user}","gists_url":"https://api.github.com/users/whitequark/gists{/gist_id}","starred_url":"https://api.github.com/users/whitequark/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/whitequark/subscriptions","organizations_url":"https://api.github.com/users/whitequark/orgs","repos_url":"https://api.github.com/users/whitequark/repos","events_url":"https://api.github.com/users/whitequark/events{/privacy}","received_events_url":"https://api.github.com/users/whitequark/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-12-24T14:37:36Z","updated_at":"2018-12-24T14:50:59Z","closed_at":null,"author_association":"MEMBER","body":"I am writing a formal specification for a CPU instruction that performs double indirection. I.e. it does `reg = mem[mem[op]];`\r\n\r\nI am trying to write an assertion like this:\r\n```sv\r\nassert (fi_w_data == mem[mem[a_regY] + i_imm5]);\r\n```\r\nThis fails, indicating a logic loop. I have worked around this by rewriting it as:\r\n```sv\r\nassert (fi_w_data == mem[$past(mem[a_regY]) + i_imm5]);\r\n```\r\nAs I understand, this effectively adds a register, but without the need to explicitly declare variables, expand processes, etc. So this register breaks the logic loop.\r\n\r\nAs I also understand, the only case where the `mem[mem[r]]` construct would be absolutely *necessary* is if you had a dual read port asynchronous memory where the data of the first port is chained to the address of the second port. In all other cases, there is at least one cycle between reads, and so the `$past` trick will work (although it might get messy with intervening writes..?).\r\n\r\nCan you please explain the nature of this limitation? Is this a real logic loop according to Verilog semantics or is this an artifact of the way Yosys lowers Verilog features? Is my workaround 'correct'? \r\n\r\nWhat would I have to do if I had the dual read port asynchronous memory as described above and wanted to verify it? Yes, probably not a very good idea, but I think it is synthesizable with LUTRAM and enough duplication, so this can in principle be encountered in a real world design."},"comment":{"url":"https://api.github.com/repos/YosysHQ/yosys/issues/comments/449742695","html_url":"https://github.com/YosysHQ/yosys/issues/764#issuecomment-449742695","issue_url":"https://api.github.com/repos/YosysHQ/yosys/issues/764","id":449742695,"node_id":"MDEyOklzc3VlQ29tbWVudDQ0OTc0MjY5NQ==","user":{"login":"daveshah1","id":5521177,"node_id":"MDQ6VXNlcjU1MjExNzc=","avatar_url":"https://avatars1.githubusercontent.com/u/5521177?v=4","gravatar_id":"","url":"https://api.github.com/users/daveshah1","html_url":"https://github.com/daveshah1","followers_url":"https://api.github.com/users/daveshah1/followers","following_url":"https://api.github.com/users/daveshah1/following{/other_user}","gists_url":"https://api.github.com/users/daveshah1/gists{/gist_id}","starred_url":"https://api.github.com/users/daveshah1/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/daveshah1/subscriptions","organizations_url":"https://api.github.com/users/daveshah1/orgs","repos_url":"https://api.github.com/users/daveshah1/repos","events_url":"https://api.github.com/users/daveshah1/events{/privacy}","received_events_url":"https://api.github.com/users/daveshah1/received_events","type":"User","site_admin":false},"created_at":"2018-12-24T14:50:59Z","updated_at":"2018-12-24T14:50:59Z","author_association":"MEMBER","body":"I understand this is due to the nature of the `$mem` cell, it appears as a logic loop - feedback from the output of the `$mem` to an input - at the word level, even though no loop exists at the bit level. This is vaguely similar to https://stackoverflow.com/questions/44828776/yosys-logic-loop-falsely-detected.\r\n\r\nRunning the `memory` command to explode the RAM to registers and logic removes the logic loop error, but will increase the cost of verification for larger designs."}}
{"actor":{"display_login":"daveshah1"}}