Retrascope

Автомат b11 был бы проще, если бы в качестве переменной состояния извлекалась только STATO. Например, код
when s_spazio=>
if r_in=0 or r_in=63 then
if cont<25 then
cont:=cont+1;
else
cont:=0;
end if;
cont1:=r_in;
stato:=s_dataout;
elsif r_in<=26 then
stato:=s_mul;
else
stato:=s_datain;
end if;

сейчас преобразуется в два состояния:
(AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25))
(AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (NOT (LESS CONT 25)))

и десять переходов: {source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25)); destination state: (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8)) (NOT (LESS CONT1 0))); guarded action: {{posedge of CLOCK}: {predicate: (AND (OR (EQ R_IN 0) (EQ R_IN 63)) (NOT (LESS R_IN 0)) (NOT (EQ RESET 1)))}->{{assignment: CONT := (ADD CONT 1); assignment: CONT1 := R_IN; assignment: STATO := 8}}}} {source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (NOT (LESS CONT 25))); destination state: (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8)) (NOT (LESS CONT1 0))); guarded action: {{posedge of CLOCK}: {predicate: (AND (OR (EQ R_IN 0) (EQ R_IN 63)) (NOT (LESS R_IN 0)) (NOT (EQ RESET 1)))}->{{assignment: CONT := 0; assignment: CONT1 := R_IN; assignment: STATO := 8}}}}

{source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25)); destination state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (EQ STATO 3)); guarded action: {{posedge of CLOCK}: {predicate: (AND (NOT (EQ RESET 1)) (NOT (OR (EQ R_IN 0) (EQ R_IN 63))) (OR (LESS R_IN 26) (EQ R_IN 26)))}->{{assignment: STATO := 3}}}} {source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (NOT (LESS CONT 25))); destination state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (EQ STATO 3)); guarded action: {{posedge of CLOCK}: {predicate: (AND (NOT (EQ RESET 1)) (NOT (OR (EQ R_IN 0) (EQ R_IN 63))) (OR (LESS R_IN 26) (EQ R_IN 26)))}->{{assignment: STATO := 3}}}}

{source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25)); destination state: (AND (NOT (EQ STATO 0)) (EQ STATO 1)); guarded action: {{posedge of CLOCK}: {predicate: (AND (NOT (EQ RESET 1)) (NOT (OR (EQ R_IN 0) (EQ R_IN 63))) (NOT (OR (LESS R_IN 26) (EQ R_IN 26))))}->{{assignment: STATO := 1}}}} {source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (NOT (LESS CONT 25))); destination state: (AND (NOT (EQ STATO 0)) (EQ STATO 1)); guarded action: {{posedge of CLOCK}: {predicate: (AND (NOT (EQ RESET 1)) (NOT (OR (EQ R_IN 0) (EQ R_IN 63))) (NOT (OR (LESS R_IN 26) (EQ R_IN 26))))}->{{assignment: STATO := 1}}}}

{source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25)); state: (EQ STATO 0); guarded action: {{CLOCK,RESET}: {predicate: (EQ RESET 1)}->{{assignment: STATO := 0; assignment: R_IN := 0; assignment: CONT := 0; assignment: CONT1 := 0; assignment: X_OUT := 0}}}} {source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (NOT (LESS CONT 25))); destination state: (EQ STATO 0); guarded action: {{CLOCK,RESET}: {predicate: (EQ RESET 1)}->{{assignment: STATO := 0; assignment: R_IN := 0; assignment: CONT := 0; assignment: CONT1 := 0; assignment: X_OUT := 0}}}}

{source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (NOT (LESS CONT 25))); destination state: (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8)) (LESS CONT1 0)); guarded action: {{posedge of CLOCK}: {predicate: (AND (OR (EQ R_IN 0) (EQ R_IN 63)) (LESS R_IN 0) (NOT (EQ RESET 1)))}->{{assignment: CONT := 0; assignment: CONT1 := R_IN; assignment: STATO := 8}}}} {source state: (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)) (LESS CONT 25)); destination state: (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8)) (LESS CONT1 0)); guarded action: {{posedge of CLOCK}: {predicate: (AND (OR (EQ R_IN 0) (EQ R_IN 63)) (LESS R_IN 0) (NOT (EQ RESET 1)))}->{{assignment: CONT := (ADD CONT 1); assignment: CONT1 := R_IN; assignment: STATO := 8}}}}

При этом среди них есть три пары переходов с совпадающими GA и конечными состояниями. То есть исключение переменной CONT из числа переменных состояния позволило бы сократить количество переходов в данном случае с десяти до семи без потери информации и с сопутствующим упрощением обхода. Ещё два перехода можно было бы убрать, исключив CONT1
Я не знаю, какая эвристика используется для определения переменных состояния, поэтому конкретных предложений дать не могу. Возможно, стоит попробовать повысить минимальный порог по количеству вхождений переменной-кандидата в охранные выражения: кажется, для отсечения переменной cont этого будет достаточно (она встречается только в двух условиях).