GHDL assertions end up in json, nextpnr complains

[antonblanchard]

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:

module test(zot);
input zot;
always @* assert(zot);
endmodule

yosys -p "read_verilog -sv test.v; synth_ecp5 -json test.json"
nextpnr-ecp5 --um5g-85k --freq 12 --json test.json

ERROR: cell type '$assert' is unsupported (instantiated as 'zot_$assert_A')

[whitequark]

Duplicate of #177.

[antonblanchard]

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.

[daveshah1]

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.

[whitequark]

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.

[daveshah1]

Hypothetically I suppose some kind of post-synthesis verification might need them?

[mikey]

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 antonblanchard/microwatt#172 is blocked on this.

[whitequark]

This was rejected in #177.

[antonblanchard]

@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?

[whitequark]

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?

[mikey]

@tgingold @eine is this something we could do in ghdl-synth?

[tgingold]

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.

[mikey]

@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.

[whitequark]

Wait, you don't use formal? Why do you get assertions in the input netlist then?

[mikey]

@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.

[tgingold]

@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.

[mikey]

@tgingold this works with microwatt. Thanks.

[mcejp]

FWIW, the equivalent flag for read_verilog is -noassert