It is good design practice to not only verify Verilog designs with regular pre-synthesis (behavioral) simulation, but also using post-synthesis simulation. This is practically mandatory when debugging mismatches between simulation and hardware. How can this be achieved with the open source IceStorm flow for iCE40 FPGAs?
See https://github.com/cliffordwolf/icestorm/tree/master/examples/icestick for an example. The "rs232demo" project comes with a test bench and the Makefile contains rules for pre- and post-synthesis simulation:
make rs232demo_tb.vcd # pre-synthesis simulation
make rs232demo_syntb.vcd # post-synthesis simulation
Use a VCD viewer like gtkwave to view the VCD files generated by this two commands.
In order to run post-synthesis simulation one must first convert the BLIF netlist (synthesis output) to a Verilog netlist: yosys -p 'read_blif -wideports example.blif; write_verilog example_syn.v'
This netlist will instantiate iCE40 device primitives. Yosys comes with simulation models for those primitives. Run the command yosys-config --datdir/ice40/cells_sim.v to print the full path name of that simulation library. Use this Verilog file when compiling your simulation.
Edit: Two additional FAQs regarding post-synthesis simulation:
(1) The clock should not have a clock edge at timestamp 0 as this can result in a race condition between clocked register updates and register initialization. I.e. the following test bench code for generating the clock is problematic:
reg clk = 1;
always #5 clk = ~clk;
Instead you should use something like the following, that leaves the clock signal undefined for an initial period:
reg clk;
always #5 clk = (clk === 1'b0);
(2) Some signals (or individual bits of a vector) can be optimized away during synthesis. This bits may be set to a constant value (usually x) or left floating by the tool. This can be confusing when trying to inspect post-synthesis simulation results. Set the keep attribute on nets that you want the tool to preserve:
(* keep *) reg [31:0] foobar;