VHDL – K-map reduzierte charakteristische Gleichung schlägt fehl

Ich habe diese Schaltung (D-Latch) :

und ich kann die logische Gleichung direkt schreiben, indem ich nur die Tore beobachte:

Wenn ich dies minimieren möchte, schreibe ich zuerst eine vorherige Status - nächste Statustabelle:

Und verwenden Sie die K-Reduktion wie folgt:

Ich habe die reduzierte Gleichung:

Ich habe dieses VHDL-Beispiel geschrieben und D-Latch funktioniert einwandfrei, wenn ich die nicht minimierte Formel verwende E:. Es funktioniert jedoch nicht wie erwartet für minimierte Formel 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;

Wenn ich die .dotDateien für beide .vhdlDateien exportiere, um zu überprüfen, welche Art von Hardware erstellt wurde, bemerke ich einen Unterschied!

Hier ist die erstellte Hardware, die funktioniert:

Hier ist die erstellte Hardware, die dies nicht tut:

Ist meine K-Map-Reduktion falsch? Oder was zum Teufel ist mit VHDL los?

Simulationen

Ich habe auch die VHDL-Testbench geschrieben:

-- 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;

Ich habe diese Testbank verwendet, um Wellenformen zu erzeugen, wie in den Kommentaren vorgeschlagen. Zu meiner Überraschung sehen auch die Wellenformen identisch aus! Aber sie erzeugen unterschiedliche Ergebnisse auf der Hardware.

Dies ist die simulierte Wellenform für die ursprüngliche Gleichung:

Dies ist die simulierte Wellenform für die reduzierte K-Map-Gleichung:

Also ... Die Simulation sieht gleich aus, aber die Hardware liefert unterschiedliche Ergebnisse. Auf Hardware verhält sich die reduzierte K-Map-Gleichung genau wie ein einfaches UND-Gatter. Der Ausgang ist nur dann hoch, wenn beide hoch sind. Und der Ausgangszustand wird nicht gespeichert.

Makefile:

Es ist möglich, dass dies eine Art Kompilierungsproblem ist. Weil VHDL zuerst in Verilog übersetzt wird und dann die Opensource-Toolchain verwendet wird, um Verilog zu kompilieren!

Hier ist das Makefile:

####################################################################################################
# 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

Um die Binärdateien zu kompilieren, verwende ich das Ziel makeund make flashlade dann die Binärdateien auf das Ziel-FPGA hoch.

Ich verwende make simulate, um .vcdWellenform-Simulationsdateien zu erstellen.

Hardware- .dotVorschaudateien wurden mit einem Ziel generiert make dot.

Es gibt auch andere Ziele im Makefile, die für die formale Überprüfung verwendet werden können, aber ignorieren Sie sie einfach.