Fail to detect FSM with specific writing style

[KelvinChung2000]

Version

Yosys 0.48+45 (git sha1 8acc77c, g++ 11.4.0-1ubuntu1~22.04 -fPIC -O3)

On which OS did this happen?

Linux

Reproduction Steps

The test.v:

module fsm_main_def (
    input  logic clk,
    input  logic reset,
    input  logic fsm_start_out,
    input  logic invoke0_done_out,
    input  logic invoke1_done_out,
    output logic s0_out,
    output logic s1_out,
    output logic s2_out,
    output logic s3_out
);

  localparam logic [1:0] S0 = 2'd0;
  localparam logic [1:0] S1 = 2'd1;
  localparam logic [1:0] S2 = 2'd2;
  localparam logic [1:0] S3 = 2'd3;

  (* fsm_encoding="auto" *)logic [3:0] current_state;
  logic [3:0] next_state;

  assign {s3_out, s2_out, s1_out, s0_out} = current_state;
  always_ff @(posedge clk) begin
    if (reset) begin
      current_state <= 'b1;
    end else begin
      current_state <= next_state;
    end
  end

  always_comb begin
    next_state = 'b0;
    case (1'b1)
      current_state[S0]: begin
          next_state[S1] = 1'b1;
      end
      current_state[S1]: begin
          next_state[S2] = 1'b1;
      end
      current_state[S2]: begin
          next_state[S3] = 1'b1;
        end
      current_state[S3]: begin
        next_state[S0] = 1'b1;
      end
      default begin
        next_state = 'b1;
      end
    endcase
  end
endmodule

With the following synthesis step:

read_verilog -sv test.v
hierarchy -auto-top
proc -noopt;
opt -nosdff -nodffe -fine -purge;
fsm

Expected Behavior

It should be able to detect the FSM

Actual Behavior

5.2. Executing FSM_EXTRACT pass (extracting FSM from design).
Extracting FSM `\current_state' from module `\fsm_main_def'.
  found $dff cell for state register: $procdff$36
  root of input selection tree: $0\current_state[3:0]
  found reset state: 4'0001 (guessed from mux tree)
  found ctrl input: \reset
  found 4 combined drivers for state signal \next_state.
  fsm extraction failed: state selection tree is not closed.

However, if modify the assignment to:

    case (1'b1)
      current_state[S0]: begin
          next_state = 4'b0010;
      end
      current_state[S1]: begin
          next_state = 4'b0100;
      end
      current_state[S2]: begin
          next_state = 4'b1000;
        end
      current_state[S3]: begin
        next_state = 4'b0001;
      end
      default begin
        next_state = 'b1;
      end
    endcase

Yosys will be able to detect the FSM.

[KelvinChung2000]

As ref: https://yosyshq.slack.com/archives/C01ML659DFD/p1737037008591969

[KrystalDelusion]

This works fine with the verific frontend, so it's probably something in read_verilog.