4
\$\begingroup\$

I have this circuit (D-latch):

enter image description here

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:

enter image description here

And use K-reduction like this:

enter image description here

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:

enter image description here

Here is the created hardware that does not:

enter image description here

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: enter image description here

This is the simulated waveform for the K-map reduced equation: enter image description here

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.

\$\endgroup\$
15
  • 2
    \$\begingroup\$ Can you add the simulation waveforms for both cases? \$\endgroup\$
    – Mitu Raj
    Jun 18, 2021 at 13:37
  • \$\begingroup\$ @MituRaj I added the waveforms. \$\endgroup\$
    – 71GA
    Jun 21, 2021 at 10:13
  • 2
    \$\begingroup\$ I'm more amazed that the first works consistently given you have the same race condition and the logic chains don't seem to be balanced per se. \$\endgroup\$
    – DonFusili
    Jun 21, 2021 at 10:36
  • 1
    \$\begingroup\$ I was able to bypass the DRC error and interestingly observed the same behavior on board as you described. I think I figured out the problem/solution. I will post the answer later. \$\endgroup\$
    – Mitu Raj
    Jun 21, 2021 at 13:39
  • 1
    \$\begingroup\$ @MituRaj Is it possible that this is due to glitches!? My K-map has two groups of 1s, but groups are not connected! So there is a possibility of a glitch! And that is exactly what happens on hardware! But it does not happen in software simulation because simulation does not account for the D-latche's setup time and hold time! I added another image to the topic that describes posibillity of a glitch! Well anyway... Please post an answer if you figure this one out! \$\endgroup\$
    – 71GA
    Jun 21, 2021 at 13:47

2 Answers 2

5
\$\begingroup\$

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): enter image description here

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.

\$\endgroup\$
4
  • 1
    \$\begingroup\$ I just wrote the same answer heheheh! \$\endgroup\$
    – 71GA
    Jun 21, 2021 at 14:18
  • 1
    \$\begingroup\$ Oh haha. Yea good you figured out the same. \$\endgroup\$
    – Mitu Raj
    Jun 21, 2021 at 14:19
  • 1
    \$\begingroup\$ Very Interesting indeed. And I solved my first glitch! :) \$\endgroup\$
    – 71GA
    Jun 21, 2021 at 14:22
  • 1
    \$\begingroup\$ Not to say that this is an example from the book! Bad book it looks like... \$\endgroup\$
    – 71GA
    Jun 21, 2021 at 14:28
3
\$\begingroup\$

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:

enter image description here

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:

enter image description here

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.

\$\endgroup\$
1
  • \$\begingroup\$ Look up'Earle latch' \$\endgroup\$ Jul 22, 2022 at 5:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.