Add fwft-fifo & use that for vai-fifo; minor fixes

fwft_fifo/Makefile

@@ -0,0 +1,19 @@
+DUT := fwft_fifo
+SRC := ../fifo/fifo.vhd ${DUT}.vhd
+
+.PHONY: cover bmc prove synth all clean
+
+all: cover bmc prove
+
+cover bmc prove: ${DUT}.vhd symbiyosys.sby
+	sby --yosys "yosys -m ghdl" -f -d work/${DUT}-$@ symbiyosys.sby $@
+
+${DUT}_synth.vhd: ${SRC}
+	ghdl --synth --std=08 --no-formal -gDepth=16 -gWidth=16 ${SRC} -e ${DUT} > $@
+
+synth: ${DUT}.json
+${DUT}.json: ${DUT}_synth.vhd
+	yosys -m ghdl -p 'ghdl --std=08 --no-formal -gDepth=16 -gWidth=16 ${SRC} -e ${DUT}; synth_ice40 -top ${DUT} -json $@'
+
+clean:
+	rm -rf work ${DUT}.json ${DUT}_synth.vhd

fwft_fifo/fwft_fifo.vhd

@@ -0,0 +1,98 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+
+
+entity fwft_fifo is
+  generic (
+    Formal : boolean := true;
+    Depth  : positive := 16;
+    Width  : positive := 16
+  );
+  port (
+    Reset_n_i    : in  std_logic;
+    Clk_i        : in  std_logic;
+    -- write
+    Wen_i        : in  std_logic;
+    Din_i        : in  std_logic_vector(Width-1 downto 0);
+    Full_o       : out std_logic;
+    Werror_o     : out std_logic;
+    -- read
+    Ren_i        : in  std_logic;
+    Dout_o       : out std_logic_vector(Width-1 downto 0);
+    Empty_o      : out std_logic;
+    Rerror_o     : out std_logic
+  );
+end entity fwft_fifo;
+
+
+architecture rtl of fwft_fifo is
+
+
+  signal s_empty : std_logic;
+  signal s_ren   : std_logic;
+
+
+begin
+
+
+  i_fifo : entity work.fifo
+  generic map (
+    Formal => Formal,
+    Depth  => Depth,
+    Width  => Width
+  )
+  port map (
+    Reset_n_i    => Reset_n_i,
+    Clk_i        => Clk_i,
+    -- write
+    Wen_i        => Wen_i,
+    Din_i        => Din_i,
+    Full_o       => Full_o,
+    Werror_o     => Werror_o,
+    -- read
+    Ren_i        => s_ren,
+    Dout_o       => Dout_o,
+    Empty_o      => s_empty,
+    Rerror_o     => open
+  );
+
+
+
+  s_ren <= not s_empty and (Empty_o or Ren_i);
+
+
+  ReadFlagsP : process (Reset_n_i, Clk_i) is
+  begin
+    if (Reset_n_i = '0') then
+      Empty_o  <= '1';
+      Rerror_o <= '0';
+    elsif (rising_edge(Clk_i)) then
+      Rerror_o <= Ren_i and Empty_o;
+      if (s_ren = '1') then
+        Empty_o <= '0';
+      elsif (Ren_i = '1') then
+        Empty_o <= '1';
+      end if;
+    end if;
+  end process ReadFlagsP;
+
+
+  FormalG : if Formal generate
+
+    default clock is rising_edge(Clk_i);
+
+    -- Initial reset
+    RESTRICT_RESET : restrict
+      {not Reset_n_i[*3]; Reset_n_i[+]}[*1];
+
+    -- Inputs are low during reset for simplicity
+    ASSUME_INPUTS_DURING_RESET : assume always
+      not Reset_n_i ->
+      not Wen_i and not Ren_i;
+
+  end generate FormalG;
+
+
+end architecture rtl;

fwft_fifo/symbiyosys.sby

@@ -0,0 +1,30 @@
+[tasks]
+cover
+bmc
+prove
+
+[options]
+depth 25
+cover: mode cover
+bmc: mode bmc
+prove: mode prove
+
+[engines]
+cover: smtbmc z3
+bmc: abc bmc3
+prove: abc pdr
+
+[script]
+ghdl --std=08 -gFormal=true -gDepth=16 -gWidth=16 fifo.vhd fwft_fifo.vhd -e fwft_fifo
+prep -top fwft_fifo
+
+# Convert all assumes to asserts in sub-units
+chformal -assume2assert fwft_fifo/* %M
+
+# Remove selected covers in i_fifo sub-unit as they cannot be reached
+chformal -cover -remove */formalg.read_pnt_stable_when_empty.cover
+chformal -cover -remove */formalg.rerror.cover
+
+[files]
+../fifo/fifo.vhd
+fwft_fifo.vhd

tests.txt

@@ -1,5 +1,6 @@
 alu
 counter
 fifo
+fwft_fifo
 vai_fifo
 vai_reg

vai_fifo/Makefile

@@ -1,5 +1,5 @@
 DUT := vai_fifo
-SRC := ../fifo/fifo.vhd ${DUT}.vhd
+SRC := ../fifo/fifo.vhd ../fwft_fifo/fwft_fifo.vhd ${DUT}.vhd
 
 .PHONY: cover bmc prove synth all clean
 
@@ -8,7 +8,7 @@ all: cover bmc prove
 cover bmc prove: ${DUT}.vhd symbiyosys.sby
 	sby --yosys "yosys -m ghdl" -f -d work/${DUT}-$@ symbiyosys.sby $@
 
-${DUT}_synth.vhd: ${DUT}.vhd
+${DUT}_synth.vhd: ${SRC}
 	ghdl --synth --std=08 --no-formal -gDepth=16 -gWidth=16 ${SRC} -e ${DUT} > $@
 
 synth: ${DUT}.json

vai_fifo/symbiyosys.sby

@@ -15,10 +15,12 @@ bmc: abc bmc3
 prove: abc pdr
 
 [script]
-ghdl --std=08 -gFormal=true -gDepth=16 -gWidth=16 fifo.vhd vai_fifo.vhd -e vai_fifo
+ghdl --std=08 -gFormal=true -gDepth=16 -gWidth=16 fifo.vhd fwft_fifo.vhd vai_fifo.vhd -e vai_fifo
 prep -top vai_fifo
-# Convert all assumes to asserts in sub-unit i_fifo
-chformal -assume2assert vai_fifo/i_fifo %M
+
+# Convert all assumes to asserts in sub-units
+chformal -assume2assert vai_fifo/* %M
+
 # Remove selected covers in i_fifo sub-unit as they cannot be reached
 chformal -cover -remove */formalg.read_pnt_stable_when_empty.cover
 chformal -cover -remove */formalg.rerror.cover
@@ -27,4 +29,5 @@ chformal -cover -remove */formalg.write_pnt_stable_when_full.cover
 
 [files]
 ../fifo/fifo.vhd
+../fwft_fifo/fwft_fifo.vhd
 vai_fifo.vhd

vai_fifo/vai_fifo.vhd

@@ -38,7 +38,7 @@ architecture rtl of vai_fifo is
 begin
 
 
-  i_fifo : entity work.fifo
+  i_fwft_fifo : entity work.fwft_fifo
   generic map (
     Formal => Formal,
     Depth  => Depth,