VHDL: la ecuación característica reducida del mapa K falla

Tengo este circuito (D-latch) :

y puedo escribir directamente la ecuación lógica solo mirando las puertas:

Si quiero minimizar esto, primero escribo un estado anterior - siguiente tabla de estado:

Y usa la reducción de K así:

Obtuve la ecuación reducida:

Escribí este ejemplo de VHDL y D-latch funciona perfectamente cuando uso la ecuación no minimizada E:. Sin embargo, no funciona como se esperaba para la ecuación minimizada F:.

-- A:
library ieee;
use ieee.std_logic_1164.all;

-- B:
entity d_latch is
    port(
        d: in std_ulogic; -- Input (DATA)
        c: in std_ulogic; -- Input (CONTROL)
        q: inout std_ulogic -- Input/output (OUTPUT)
    );
end d_latch;

-- C:
architecture logic_001 of d_latch is
begin

    -- E:
    --q <= ((d and c) nor q) nor (c and not d);

    -- F:
    q <= ((not c) and q) or (c and d);

end architecture logic_001;

Cuando exporto los .dotarchivos de ambos .vhdlarchivos para verificar qué tipo de hardware se creó, ¡observo una diferencia!

Aquí está el hardware creado que funciona:

Aquí está el hardware creado que no:

¿Está mal mi reducción de K-map? ¿O qué diablos está pasando con VHDL?

Simulaciones

También escribí el banco de pruebas VHDL:

-- A:
library ieee;
use ieee.std_logic_1164.all;

-- B:
entity d_latch_tb is
end d_latch_tb;

-- C:
architecture test_001 of d_latch_tb is
    
    -- D:
    component d_latch
        port(
            d: in std_ulogic; -- Input (DATA)
            c: in std_ulogic; -- Input (CONTROL)
            q: inout std_ulogic -- Input/output (OUTPUT)
        );
    end component;

    -- E:
    signal dx: std_ulogic; -- Input (SET)
    signal cx: std_ulogic; -- Input (RESET)
    signal qx: std_ulogic; -- Input/output (OUTPUT)

begin

    -- F:
    -- c1: d_latch port map (dx, cx);
    -- c1: d_latch port map (dx, cx, qx);
    c1: d_latch port map (d => dx, c => cx, q => qx);

    -- G:
    process begin
        
        -- H:
        cx <= '0';
        dx <= '0';
        wait for 1 ns;
        cx <= '0';
        dx <= '1';
        wait for 1 ns;
        cx <= '0';
        dx <= '0';
        wait for 1 ns;
        cx <= '1';
        dx <= '0';
        wait for 1 ns;
        cx <= '1';
        dx <= '1';
        wait for 1 ns;
        cx <= '0';
        dx <= '1';
        wait for 1 ns;
        cx <= '0';
        dx <= '0';
        wait for 1 ns;

        -- I:
        assert false report "END OF TEST!";
        
        -- J:
        wait;

    end process;

end architecture test_001;

Usé este banco de pruebas para producir formas de onda como se sugiere en los comentarios. ¡Para mi sorpresa, también las formas de onda se ven idénticas! Pero producen resultados diferentes en el hardware.

Esta es la forma de onda simulada para la ecuación original:

Esta es la forma de onda simulada para la ecuación reducida de K-map:

Entonces... La simulación se ve igual pero el hardware da resultados diferentes. En el hardware, la ecuación reducida de K-map se comporta exactamente como una puerta AND simple. La salida es alta solo cuando ambos son altos. Y el estado de salida no se almacena.

Makefile:

Es posible que se trate de algún tipo de problema de compilación. ¡Porque VHDL se traduce primero a Verilog y luego se usa la cadena de herramientas de código abierto para compilar verilog!

Aquí está el archivo MAKE:

####################################################################################################
# Makefile's paragraphs:
#
# A: Properly set these parameters before running any of the targets in the makefile.
#
#    Here we have to choose a solver that "yosys-stmbmc" uses. We can choose one of these:
#    z3, boolector, cvc4, yices, mathsal
#
#    NOTE: mathsal is not installed on our system...
#    NOTE: boolector is experiencing a broken pipeline error...
#
# B: This target first synthesizes VHDL file to verilog file.
#
#    Then it synthesizes verilog (.v) file to a netlist (.blif) file. Then it  place & routes
#    the netlist file and creates an ASCII bitstream file (.asc). This file is then used to create
#    an FPGA binary file (.bin) for "iCE40-UP5K-SG48".
#
# C: This flashes the binary file (.bin) to the "iCE40" device connected to our workstation.
#
# D: This creates a simulation for our design. In order to create simulation we first use ghdl with
#    parameter "-s" to check the syntax of .vhdl files. Then we use a parameter "-a" to analyze the
#    .vhdl files in order to know where to find entities... This will create a ".pc" file that is
#    also needed to write the .vcd file in the last step where we use parameter "-r" that runs the
#    simulation.
#
# E: Use design verilog file (.v) to synthesize an SMT-LIB-v2 file (.smt2) on which we use a SAT
#    solver that executes a formal verification (BMC method).
#
#    NOTE: This only produces .vcd file if formal verification fails!
#    NOTE: Usage of parameter "-formal" defines a macro "FORMAL" and in source code we use this to
#          automatically enable blocks meant exclusively for "formal verification". automatisation
#          is achieved by using "ifdef FORMAL".
#
# F: Use design verilog file (.v) to synthesize an SMT-LIB-v2 file (.smt2) on which we use a SAT
#    solver that executes a formal verification (induction method).
#
#    NOTE: This only produces .vcd file if formal verification fails!
#    NOTE: Usage of parameter "-formal" defines a macro "FORMAL" and in source code we use this to
#          automatically enable blocks meant exclusively for "formal verification". automatisation
#          is achieved by using "ifdef FORMAL".
#
# G: Use design verilog file (.v) to synthesize an SMT-LIB-v2 file (.smt2) on which we use a SAT
#    solver that executes a formal verification (cover method).
#
#    NOTE: This only produces .vcd file if formal verification fails!
#    NOTE: Usage of parameter "-formal" defines a macro "FORMAL" and in source code we use this to
#          automatically enable blocks meant exclusively for "formal verification". automatisation
#          is achieved by using "ifdef FORMAL".
#    NOTE: Target is not implemented in this design.
#
# H: Preview the generated .vcd file in gtkview.
#
# I: We first read the verilog file, then use "proc" which replaces the processes in the design with
#    multiplexers, flip-flops and latches. Then we use "show" to generate a .dot file and openm it
#    with xdot viewer.
#
#    TODO: This still does not work for multiple verilog files!!!
#
# J: Delete all the generated files.
#
####################################################################################################

# A:
file_main = d_latch
file_pcf = icebreaker
file_cpp = driver
solver = z3

module_top = d_latch
entity_top = $(module_top)
entity_top_tb = $(module_top)_tb

####################################################################################################

# B:
all:
    yosys \
        -m ghdl \
        -p "ghdl $(file_main).vhdl -e $(entity_top); write_verilog $(file_main).v"
    yosys \
        -p "synth_ice40 -top $(module_top) -blif $(file_main).blif" \
        $(file_main).v
    arachne-pnr \
        -d 5k \
        -P sg48 \
        -o $(file_main).asc \
        -p $(file_pcf).pcf $(file_main).blif
    icepack $(file_main).asc $(file_main).bin

# C:
flash:
    iceprog $(file_main).bin

# D:
simulate:
    ghdl -s $(file_main).vhdl
    ghdl -s $(file_main)_tb.vhdl
    ghdl -a $(file_main).vhdl
    ghdl -a $(file_main)_tb.vhdl
    ghdl -r $(entity_top_tb) --vcd=$(file_main).vcd

####################################################################################################

# E:
verification_bmc:
    yosys \
        -p "read_verilog -sv -formal $(file_main).v" \
        -p "hierarchy -check -top $(module_top)" \
        -p "prep -nordff -top $(module_top)" \
        -p "write_smt2 -wires $(file_main).smt2"
    yosys-smtbmc -t 100 -s $(solver) --dump-vcd $(file_main).vcd $(file_main).smt2
    
# F:
verification_induction:
    yosys \
        -p "read_verilog -sv -formal $(file_main).v" \
        -p "hierarchy -check -top $(module_top)" \
        -p "prep -nordff -top $(module_top)" \
        -p "write_smt2 -wires $(file_main).smt2"
    yosys-smtbmc -i -t 100 -s $(solver) --dump-vcd $(file_main).vcd $(file_main).smt2

# G:
verification_cover:
    yosys \
        -p "read_verilog -sv -formal $(file_main).v" \
        -p "hierarchy -check -top $(module_top)" \
        -p "prep -nordff -top $(module_top)" \
        -p "write_smt2 -wires $(file_main).smt2"
    yosys-smtbmc -c -t 100 -s $(solver) --dump-vcd $(file_main).vcd $(file_main).smt2

#################################################################################################

# H:
vcd:
    gtkwave $(file_main).vcd

# I:
dot:
    yosys \
        -p "read_verilog -sv -formal $(file_main).v" \
        -p "hierarchy -check -top $(module_top)" \
        -p "proc" \
        -p "show -prefix $(file_main) -notitle -colors 2 -width -format dot"
    xdot $(file_main).dot

#################################################################################################

# J:
.PHONY: clean
clean:
    @rm -f *.bin
    @rm -f *.blif
    @rm -f *.asc
    @rm -f -r obj_dir
    @rm -f *.elf
    @rm -f *.vcd
    @rm -f *.smt2
    @rm -f *.dot
    @rm -f *.v
    @rm -f *.cf

Para compilar los archivos binarios, uso el destino makey luego make flashsubo los archivos binarios al FPGA de destino.

Lo uso make simulatepara crear .vcdarchivos de simulación de forma de onda.

Los archivos de vista previa de hardware .dotse generaron con un objetivo make dot.

También hay otros objetivos en el archivo MAKE que se pueden usar para la verificación formal, pero simplemente ignórelos.