VHDL -- K-map reduced characteristic equation fails

Question

I have this circuit (D-latch):

and I can directly write the logical equation by only watching the gates:

$$ Q = \overline{(\overline{(D \cdot C) + Q}) + (C \cdot \overline{D})} $$

If I want to minimize this I first write a previous state - next state table:

And use K-reduction like this:

I got the reduced equation:

$$ Q = (\overline{C}\cdot Q) + (C \cdot D) $$

I wrote this VHDL example and D-latch works flawlesly when I use the non-minimized equation E:. However, it is not working as expected for minimized equation 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;

When I export the .dot files for both .vhdl files to check what kind of hardware was created, I notice a difference!

Here is the created hardware that works:

Here is the created hardware that does not:

Is my K-map reduction wrong? Or what the heck is going on with VHDL?

---

Simulations

I also wrote the VHDL testbench:

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

I used this testbanch to produce waveforms as suggested in the comments. In my surprise also the waveforms look identical! But they produce different result on hardware.

This is the simulated waveform for the original equation:

This is the simulated waveform for the K-map reduced equation:

So... Simulation looks the same but hardware gives different results. On hardware K-map reduced equation behaves exactly lika a simple AND gate. Output is high only when both are high. And output state is not stored.

Makefile:

It is possible that this is some sort of a compilation problem. Because VHDL is 1st translated to Verilog and then opensource toolchain is used to compile verilog!

Here is the 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

To compile the binaries I use target make and then make flash to upload binaries to the target FPGA.

I use make simulate in order to create .vcd waveform simulation files.

Hardware .dot preview files were generated with a goal make dot.

There are also other targets in the makefile that can be used for formal verification, but just ignore them.

Answer 1

Latches have to be properly timed on its paths to obtain the intended latching behavior. Latches have a combinatorial feedback and hence its timing cannot be correctly analysed by an FPGA synthesiser when it's synthesised naively in LUTs. This is one reason why latches or any combinatorial loops are said to be 'bad' and unpredictable to synthesise on an FPGA in HDL.

Out of curiosity, I tried both versions of your code on a Xilinx board bypassing combinatorial-loop warnings and observed the same behavior as you described. The first version of code surprisingly worked as a D-latch on board. But the second version of code (the reduced K-map) didn't. It behaved like an AND gate.

After a bit digging, I figured out the problem is that you have a static-1 hazard, (like a 'glitch', read more here) in your reduced K-map expression \$Q' = (\overline{C}\cdot Q) + (C \cdot D)\$, which may be the cause of this unpredictable behavior.

This glitch of \$0\$ at \$Q'\$ happens when there is a transition in the current state, \$[C, D, Q]: [0,1,1] \leftrightarrow [1,1,1]\$ within the \$\color{orange} {orange}\$ group shown in the K-map. ie., \$ Q'\$ momentarily changes from \$ 1 \rightarrow 0\$ and it in turns changes the 'input' \$Q\$ (because it is fed back) from \$ 1 \rightarrow 0\$, right when the clock \$ C \$ changes from \$ 1 \rightarrow 0\$. This should be causing hold violation, and the latch fails to latch the value \$1\$ which was at \$Q\$ just before the clock transition.

Wiki states: "A theorem proved by Huffman tells us that by adding a redundant loop will eliminate the hazard"

So if you add the redundant term \$Q.D\$ into the K-map expression (the group in \$\color{orange} {orange}\$ color):

The new expression will become: $$Q'=(\overline{C}\cdot Q) + (C \cdot D)\color{blue}{+ \text{(} Q.D)}$$

This should be the reduced expression without static hazards, which you should be using to model the latch in HDL. It worked for me on board as a D-latch.

However, I don't recommend modelling latches on FPGA for the reason I stated earlier.

Answer 2

I found out that in this case K-reduction produces a glitch! This glitch does not show in simulation, but it shows on the hardware, because simulation does not take in account the D-latche's setup time and hold time like shown in this image:

If D is changed near the moment C's negative edge, D latch only manages to store the input state for a short time and then it returns to the previous state. What remains is a glitch... I did not observe this glitch. I only read about it in the book.

To remove the glitch, I had to fix my K-map and connect the existing groups with a group III:

This gives me a different equation:

$$ Q = (\overline{C}\cdot Q) + (C \cdot D) + (D \cdot Q) $$

And this works in VHDL! But in this case K-map reduction does not do much for me or it can cause more harm than good. What I still do not understand is why and how glitch prevents the hardware to act like it should.

I will not accept this answer of mine if anyone can explain, how and why this glitch causes my design to act as an AND gate.