No puedo obtener una salida significativa de un circuito en el ejercicio 2.7 de Thomas & Moorby.

Estoy resolviendo los ejercicios en "El lenguaje de descripción de hardware de Verilog" para aprender Verilog. Actualmente estoy atascado en el ejercicio 2.7, y como no pude encontrar nada en la web al respecto, pensé en preguntar aquí.

Estoy implementando esto en Vivado y tratando de simularlo, pero creo que el resultado siempre es cero. El ejercicio pide una descripción utilizando diferentes técnicas de la FSM representada por este circuito:

Este es mi código actual para el circuito, que estoy probando con un banco de pruebas que simula correctamente un reloj con un período de 20 unidades de tiempo.

timescale 1ns / 1ps

module reference(
input Ain,
input Bin,
input Cin,
input rst,
input clk,
output reg Y
);

reg Q0, Q1;
wire theORW, AandW, BandW;

or #1
    theORG (theORW, AandW, BandW);

and #1
    AandG (AandW, Ain, Q1),
    BandG (BandW, Bin, Q0), 
    YandG (YandW, Cin, theORW);

always @(posedge clk, negedge rst)
begin
    if(~rst)
    begin
        Q0 <= 0;
        Q1 <= 0;
        Y <= 0;
    end
    else begin
        Q0 <= AandW;
        Q1 <= theORW;
        Y <= YandW;
    end
end

endmodule

Cuando simulo, el código Y siempre es 0, sin importar qué combinación de entradas intento y mantengo alto durante muchos relojes. Estoy emitiendo un reinicio primero. Vivado actualmente crea esta representación RTL que se parece al diagrama del libro:

¿Estoy malinterpretando algo? ¿Es este el comportamiento correcto del circuito?

Texto del ejercicio:

2.7 Escriba una descripción para la FSM que se muestra en la figura 2.7 con entradas Ain, Bin, Cin, clock y reset, y salida Y.

A. Un solo bloque siempre

B. Dos siempre bloques; uno para la lógica combinacional y otro para la secuencial.

C. Vaya, este circuito es demasiado lento. No podemos tener tres retardos de puerta entre las salidas y entradas del flip flop; mas bien solo dos. Cambie la parte B para que Y sea una salida combinacional, es decir, mueva la puerta que genera d2 al otro lado de los flip flops.

D. Simule todo lo anterior para demostrar que todos son funcionalmente equivalentes.