Technically, I suppose this design would fail a bounded model check–but only if you could get the bounded model check to check over 65,000 states.

That said, I tried it myself and only got about 3,000 steps into the proof–far from the 65,000 required to get to a failure.

This illustrates one of the problems associated with bounded model checks. Where I’ve seen this problem most recently is when working on an SDRAM controller. According to the specification, this controller required a 100us reset. ).

reg	[14:0]	reset_counter;
initial	reset_counter = 0;
always @(posedge i_clk)
if (i_reset)
	reset_counter   <= 0;
	o_sdram_reset_n <= 1;
else if (reset_counter < 14'd20_000)
	reset_counter   <= reset_counter + 1;
	o_sdram_reset_n <= 1;
end else // if (reset_counter >= 14'd20_000)
	o_sdram_reset_n <= 0;

How shall this design be verified? SDRAMs have a lot of very significant timing properties that all need to be checked: the number of clocks from row activation to any column access, from row precharge to row activation, from refresh to refresh, and so on. If the design is stuck for 20k time-steps in reset, a bounded model check will not be sufficient to verify such a design. You may need to use induction in such cases. Indeed, this is one of the reasons why I tend to use induction to verify all of my designs.

Another option would be to use a parameter to describe the counter limit, and then adjust that parameter in the SymbiYosys file. You could then verify the design against a 3 clock reset for example. Since I use induction, I don’t necessarily need this to verify my SDRAM designs, however I’ve found this approach very valuable when generating cover() traces.

Another approach that I tried recently is to use abstraction, and to set the number of startup clocks only if the design is not in formal verification mode. This approach is a touch more transparent than adjusting the associated sby file. I’ll let you decide which method you like better.