if I haven't already highlighted this paper by Clifford Cummings then I should have....
You will hopefully be aware that I have a complete behavioural simulation of SPAM-1 in Verilog (suggested by Warren Toomey aka Dr WKT) .
The simulation is as far as I can make it also timing accurate for the chips I've used in the hardware.
This paper above was instrumental in my understanding (a bit) how timing works in Verilog and helped me decide to go for a "Transmission delay" approach because that is most aggressive in highlighting glitches if there are any. My entire model hasn't yet switched over.
Really important for folk to understand if hoping to get the most from a model.