¿Cómo debo manejar los meta-valores en implementaciones de máquina de estado finito usando VHDL?

Recientemente agregué la propagación de 'X' a mis diseños VHDL de nivel RT, para detectar de manera temprana cada vez que se realizan operaciones en valores desconocidos ('X') o no inicializados ('U'). Este último puede provenir de registros, que olvidé restablecer, o de la memoria que no se puede restablecer. Los valores desconocidos pueden provenir de operaciones lógicas en valores no inicializados. No me importan los valores desconocidos o no inicializados, siempre que no conduzcan a un comportamiento indefinido, por ejemplo, cambios de estado indefinidos en una máquina de estados finitos (FSM). No distingo entre 'X', 'U' o cualquier otro meta-valor, todos son tratados como 'X'.

Estoy familiarizado con la aplicación de la propagación de 'X' a las rutas de datos, pero me cuesta aplicarlo a los FSM porque el código se está volviendo mucho más complejo y la legibilidad está disminuyendo. Aquí hay un ejemplo simplificado, cómo se ven mis FSM con la propagación 'X':

library ieee;
use ieee.std_logic_1164.all;

entity fsm is
    port (
        clock  : in std_logic;
        reset  : in std_logic;
        input  : in  std_logic_vector(1 downto 0);
        output : out std_logic); -- mealy output
end entity fsm;

architecture rtl of fsm is
    type states is (RUNNING, WAITING, UNKNOWN);
    signal state : states
        -- synthesis translate_off
        := UNKNOWN
        -- synthesis translate_on
        ;
    signal next_state : states;
begin  -- architecture rtl

    process(state, input)
    begin
        next_state <= state;
        output     <= '0';

        case state is
            when RUNNING =>
                case input(1) and not input(0) is -- some complex condition
                    when '1' => next_state <= WAITING;
                    when '0' => output     <= '1';
                    when others =>
                        next_state <= UNKNOWN;
                        output     <= 'X';
                end case;

            when WAITING =>
                next_state <= RUNNING;

            when UNKNOWN =>
                output <= 'X';
        end case;
    end process;

    process(clock)
    begin
        if rising_edge(clock) then
            case to_x01(reset) is
                when '1' =>    state <= RUNNING;
                when '0' =>    state <= next_state;
                when others => state <= UNKNOWN;
            end case;
        end if;
    end process;
end architecture rtl;

Uso las declaraciones case para verificar las entradas de alguna condición, por lo que no tengo que repetir la condición como con las declaraciones if :

if (input(1) and not input(0)) = '1' then
    next_state <= WAITING;
elsif (input(1) and not input(0)) = '0' then -- repeated condition
    output <= '1';
else
    next_state <= UNKNOWN; output <= 'X';
end if;

No encuentro la instrucción case muy legible porque sin la propagación de "X", la condición sería mucho más clara:

if input(1) = '1' and input(0) = '0' then
    next_state <= WAITING;
else
    output <= '1';
end if;

Otro problema es hacer un seguimiento cuando las salidas débiles serán desconocidas. En el ejemplo anterior, output será desconocido cuando la condición no esté determinada.

Entonces, mis preguntas son:

1. ¿Debo propagar los valores de 'X' (al estado FSM y las salidas medibles) o debo simplemente un report un error?

2. ¿Hay una plantilla de código más legible para probar condiciones complejas como en el ejemplo anterior?

3. ¿Existe un método mejor para verificar si se aplicó un reinicio correcto? (Nota: el estado aún debe ser desconocido hasta que se levante el primer borde del reloj)

Todo después de todo: el código debe ser sintetizable. (Debido a la protección de síntesis, el estado DESCONOCIDO nunca se alcanzará en HW real y, por lo tanto, se optimizará).