search

YosysHQ / yosys

Yosys Open SYnthesis Suite
https://yosyshq.net/yosys/
ISC License
3.37k stars 874 forks source link

$assert cells should be ignored during synthesis #177

Closed whitequark closed 8 years ago

whitequark commented 8 years ago

This was triaged from openfpga, so please see the discussion over at https://github.com/azonenberg/openfpga/issues/11.

cliffordwolf commented 8 years ago

The usual approach is to enclose all code for formal verification with ifdef FORMAL ...endif and only set the define FORMAL when doing formal verification (done by default by read_verilog -formal).

It would be possible, as @azonenberg suggested, to add an option to synth_greenpak4 that simply runs a command such as delete t:$assert for convenience, but that would be very unconventional. I'd accept such a patch for synth_greenpak4 from @azonenberg, but I would not add it to "my" synthesis flows such as synth_ice40 or synth_xilinx.