tgingold

Do not hesitate to give your opinion on this issue! That would be useful.

For the spurious warnings when the same file is re-analyzed, I am not sure what to do. Maybe I won't do anything, as this is not a common case. Currently,...

No, external libraries would be kept. But files that have been read from a previous ghdl command wouldn't be kept for the next commands.

Yes, but this is not spurious. This exactly what the warning is about.

Yes, but you can the same with a verilog input: module m (output v); assign v = 1'bz; endmodule autoidx 1 attribute \cells_not_processed 1 attribute \src "t.v:1.1-3.10" module \m attribute...

Ok, so that's just a bug with write_rtlil. Do not hesitate to report the issue once you have figured out it.

Well, that's expected. You are doing a synthesis and the output is a netlist.

VHDL being case insensitive, ghdl only uses lowercase names. Yosys being verilog is case sensitive and expect the same name. So, you can either use lowercase ports name in verilog...

Last time I looked at it, it seemed to me that $live semantic doesn't really match the semantic of PSL. Is it supported only by boolector ?

I am not sure this is accepted by synthesizer. Do you want it to be accepted or do you want a better error message ?