Initialization values in EBMC

[Alexander Gnusin]

To comply with synthesizable designs in FPGA, it would be desirable to avoid "initial" statements in Verilog and initialize all synchronous design elements to 0 (usually this is a case in FPGA when global reset is de-asserted). Is it possible to implement with feature in EBMC by default (still, being able to use "initial" to override these default values).

Thanks,

-Alex   

[Daniel Kroening]

May I first ask whether you are absolutely sure that your synthesis tool chain guarantees that all state holding elements are zero initialised? In particular, I have seen cases where "bigger" (meaning exceeding some configurable threshold) pieces of state got mapped onto target-specific SRAM, and those weren't initialised.

Assuming this is actually guaranteed, then my key concern is that this is obviously specific to a particular synthesis flow, and hence can't be a default.

Would you feel comfortable to tell EBMC about this in some programmatic way, e.g., using a Python API? How are you dealing with this when doing simulation?

With best regards,

Daniel