FSM misbehaves.

Bram, My coleague had as debugging output a "one-hot" encoded signal that we exported to debugging leds. Those simply indicated a state that was valid, but we also exported the input signals and by hand verified that it was supposed to continue.

I then took over the project, and I used binary encoding to indicate the state. (I just defined a set of extra outputs with values that simply correspond to a binary encoding of the state. In reality behind the scenes Quartus was still using a one-hot encoding for the states).

This binary encoding is of course much less likely to indicate "bad state" than the one-hot encoding that my colleague used before. (but even then his one-hot output that should've been just led_out = NOT state_idle etc did not indicate an illegal state...)

I did not inconclusively prove that the state-machine got into an impossible state. I just synchronized the external inputs and it started working.

If you really need to prove it to be in an invalid state then I would suggest trying to use SignalTap to monitor the situation. There you can tap the internal signals: 'state_is_idle', 'state_is_start_write' etc etc.

I had never used SignalTap when I solved this problem. Now I have. :-)