-
Notifications
You must be signed in to change notification settings - Fork 871
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Internal module wires are not accessible using dot notation #647
Comments
This syntax is also very convenient for temporarily hooking internal signals up to an integrated logic analyzer without routing them all the way through your design. I wrote a demo for how to do this in TinyFPGA at https://hackaday.io/project/165639-sump2-tinyfpga-demo , but it only works with iCEcube2 right now. |
I think this would be a nice enhancement to use in riscv-formal's wrapper. I'm looking forward to it. |
Yeah, this is the single most annoying issue and the one that just drives me away from formal ... I tend to subdivide my code in small modules and so having to exports tons of signals through several layers of hierarchy is way too much "pollution" in the code for me to be worth it. |
Now that fbb346e is in, I might be able to fix this soon. |
The main implementation complexity is that it introduces a new constraint on elaboration ordering - the size of the wire in the target module must be known before elaborating the module containing the reference. |
Oh, yeah, I missed that. |
I have experimented locally with addressing this by piggybacking on the |
I think that the elaboration ordering constraint isn't actually all that difficult to handle. I've just pushed up PR #2998 (in draft, because it touches some lines in common with another PR in flight and I'm going for the "optimistic" rebasing strategy!). This should force elaboration to run in the right order, which will allow us to delve into the guts of child modules. |
While I haven't looked at #2998 yet, if it works, it would simplify what I have already sketched out in #2716. My PR implements the key module lookup logic in simplify and is a clear stepping stone toward automatic hierarchical references, but currently relies on unfortunate repeated elaboration, which #2998 would theoretically obviate. |
This is a bug, not an enhancement. Standard or not, everyone else's tools support this in synthesizable code. Hence, it's a showstopper, not a 'nice to have'. Worse, defaults scripts for things like synth_ice40 don't even assert the check, so there's no error that would hint that anything is wrong: Consequently, this issue is certainly frustrating engineers new to yosys, coming from commercial tools. Builds appear good (perhaps a little too good: they're quick, have incredibly low resource utilization, and very fast max frequency), but simply don't work, as almost the whole design can get quietly optimized to oblivion. |
I agree that silently generating incorrect netlists is a bug. At least these should be rejected in the frontend if they're not planned to be supported. |
It's a fairly common in soft-core CPU designs where datapath goes through the ports, but control lines are just connected by the dot notation between modules. Probably enabling the 'check -assert' option in the default synth_ice40 script will at least tend to spit the dummy when this happens, leading to it being dealt with or at least noticed. There is a warning line, 'Reported problems...' or so, but it gets treated as a warning, not an error, and it gets lost in the default info. Being least charitable, this is a failure to parse the verilog in a manner interoperable with other tools. Vivado for instance fails to connect at elaboration, but picks up the connection before synthesis, so it works there. I can also confirm that it works in Gowin's synthesis tool. |
My understanding is that this isn't a part of synth flows because Verilog does specify what happens with
I don't think there is anything uncharitable about it--it is a statement of fact. I agree that it is a serious issue, especially if you use dot notation to reach into an inner module in only a few places and it isn't immediately visible. |
Steps to reproduce the issue
The following code...
...when read with yosys...
...generates with the following warning:
Expected behavior
This code should read cleanly.
Background
This issue was prompted by the method described @ZipCPU 's article: https://zipcpu.com/blog/2018/07/06/afifo.html .
The article explains how to use formal methods to verify an asychronous FIFO described in this artcle: http://www.sunburst-design.com/papers/CummingsSNUG2002SJ_FIFO1.pdf
The FIFO design uses a sub-modules to wrap up address generation RTL that is repeated twice: once for the read-side, and once for the write-side.
Unfortunately, because the yosys verilog front-end can't access internal wires, @ZipCPU had to unroll the sub-modules into the parent module so that he could access these hidden signals.
An alternative would be to expose these wires as ports on the sub-module. However, for more complex deeply nested modules this may become rather impractical.
The text was updated successfully, but these errors were encountered: