safe state machines

--- Quote Start ---

I continue this interesting post with an example I don't understand.

I simulated the following FSM

 
module FSMexampleSafe2 (clk,reset,read_write, ready, oe);
input clk,reset,read_write, ready;
output oe;
wire clk,reset,read_write, ready;
reg oe;
reg  ac_state /* synthesis syn_encoding="user,safe" */;
parameter     // One-hot coding
idle =6'b000001,      decision=6'b000010,       read  =6'b000100,
write=6'b001000,      dummy1  =6'b010000,   dummy2=6'b100000;
always @(posedge clk)  // state register and logic for next state
begin
if (reset)
 ac_state <= idle;
else
 case (ac_state)
 idle:    ac_state <= (ready)      ? decision : idle;
 decision:   ac_state <= (read_write) ? read : write;
 read:    ac_state <= (ready)      ? idle : read;
 write:    ac_state <= (ready)      ? idle : write;
   dummy1:    ac_state <= dummy2;
   dummy2:    ac_state <= dummy1;
// default: ac_state <= idle;
 endcase
end
always @(ac_state)  // Moore logic for output
begin
case (ac_state)
 idle, decision, write:    oe<=1'b0; 
 read:   oe<=1'b1;
 default:  oe<=1'b0;
endcase
end
endmodule
 

and run the Modelsim RTL simulation with the following testbench

The FSM is recognized by the synthesizer and the state machine viewer shows a FSM with 5 states.

The message windows confirms that the FSM is being implemented as 'safe'.

Following what is written in this post the synthesizer should:

1) remove dummy1 and dummy2 states that are not reachable.

2) gracefully recover from illegal states.

The RTL simulation shows, instead:

1) when forced in dummy1 state, the FSM hangs in the dummy1-dummy2 infinite cycle hence dummy1 and dummy2 have not been removed.

2) when froced in the illegal '000000' state, the FSM hangs there forever.

Can someone explain where's my error?

Please note that the default instruction in the next state block is commented.

--- Quote End ---

If i uncomment the

// default: ac_state <= idle;

line

the FSM recovers from the 000000 illegal state going to idle.

This seems to show that the 'default' instruction isnot ignored by the synthesizer. Further, the 'default' instruction, is the only one that works in producing a 'safe' (in a certain sense) FSM.

Am I worng?