Closed antonblanchard closed 4 years ago
Duplicate of #177.
Thanks, I guess the SystemVerilog reproducer was a bit of a red herring. Should GHDL not emit Assert entries at all, or have an option to not emit them? It seems a bit strange to be doing it there, vs yosys or nextpnr.
It wouldn't be too problematic to drop these cells in the nextpnr frontend, if that is the consensus then I'm happy to do that. But I don't know what would happen with synth_xilinx and the EDIF backend, or xilinx/ice40 going into VPR or arachne-pnr via BLIF.
Should we perhaps just delete formal cells at the end of every device-specific flow? I'm not sure what the downsides to that are.
Hypothetically I suppose some kind of post-synthesis verification might need them?
Is there any movement on this? I retested with the latest docker images in ghdl/synth:nextpnr-ecp5 and we are still hitting this. FWIW https://github.com/antonblanchard/microwatt/issues/172 is blocked on this.
This was rejected in #177.
@whitequark I'm a bit confused, these are runtime asserts in the VHDL, and GHDL is passing them through to yosys. Should we get GHDL to strip them all out?
The Verilog backend also passes the asserts through to Yosys. The solution offered in #177 was to use the Verilog preprocessor to strip asserts for synthesis. Does VHDL have one?
@tgingold @eine is this something we could do in ghdl-synth?
1) You can use the chformal -remove
yosys command to remove all the formal cells. That's an immediate workaround.
2) We could add a -no-assert
or -no-formal
options to the ghdl front-end to disable all the assertions.
@tgingold IMHO a -no-assert
would be nicer for microwatt as then we wouldn't need to change our code specifically for ghdl-synth/yosys. We don't use formal at all currently.
Wait, you don't use formal? Why do you get assertions in the input netlist then?
@whitequark we just use asserts. An example that's causing us problems is here. Happy to take pointers if we are doing this the wrong way.
@whitequark The possibility to use assertions in VHDL exists since the first standard (1987) and is not exactly considered as formal methods.
It is now possible to use the --no-formal
option for synthesis with ghdl.
@tgingold this works with microwatt. Thanks.
FWIW, the equivalent flag for read_verilog
is -noassert
I'm hitting an issue building microwatt with ghdl/yosys/nextpnr where nextpnr complains about an assertion. I'm not sure if yosys shouldn't emit them, if nextpnr should ignore them, or if they are unsupported and ghdl shouldn't emit them.
A simple example: