Добрый день!
Помогите, пожалуйста, разобраться с проблемой. Описываю автомат. Использую при этом связку: перечисления + unique case.
Исходный код прилагается:

module simple_fsm
(
input clk, rst,
output logic y
);
typedef enum logic [1:0] {IDLE=2'b00, WORK=2'b01, DONE=2'b10} fsm_state;
fsm_state State, Next;
always_ff @(posedge clk)
if(rst)
State<=IDLE;
else
State<=Next;
always_comb
unique case (State)
IDLE: Next=WORK;
WORK: Next=DONE;
DONE: Next=IDLE;
endcase
always_comb
y=(State==DONE);
endmodule

Далее я пытаюсь загрузить этот файл в Synopsys DC. Использую пару команд:
analyze -format sverilog simple_fsm.sv
elaborate simple_fsm
И получаю следующие предупреждение:
Warning: ./mult.sv:17: Case statement marked unique does not cover all possible conditions. (VER-504)

Поэтому у меня возникает вопрос. Как DC анализирует unique case?
Ведь я использую перечисления, разве это не должно сказать DC, что кроме перечисленных значений, других не возникнет?

Он смотрит на "logic [1:0]" и видит, что возможны 4 варианта.

То есть, если я правильно понял, DC этим предупреждением призывает еще раз проверить, так ли все задумывалось?

Не только - состояние 11 он может приравнять к любому из 3-х уже существующим и в результате может получиться не то, что предполагалось.

Теперь понял. Спасибо.