Add (non-functional yet) VAI-FIFO

README.md

@@ -20,5 +20,8 @@ A simple counter design in VHDL. The testbench contains various simple propertie
 ### fifo
 A simple synchronous FIFO with various checks for write/read pointers, data and flags.
 
+### vai_fifo
+A simple FIFO with valid-accept interface. Consists of the fifo unit and some glue logic doing fifo<->vai interface conversion.
+
 ### vai_reg
-A simple register file with VAI (valid-accept-interface) which serves as test design to try formal verification of FSMs.
+A simple register file with VAI (valid-accept-interface) which serves as test design to try formal verification of FSMs.

vai_fifo/Makefile

@@ -0,0 +1,19 @@
+DUT := vai_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: ${DUT}.vhd
+	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

vai_fifo/symbiyosys.sby

@@ -0,0 +1,26 @@
+[tasks]
+cover
+bmc
+prove
+
+[options]
+depth 25
+cover: mode cover
+bmc: mode bmc
+prove: mode prove
+
+[engines]
+cover: smtbmc z3
+bmc: smtbmc z3
+#abc bmc3
+prove: abc pdr
+
+[script]
+ghdl --std=08 -gFormal=true -gDepth=16 -gWidth=16 fifo.vhd vai_fifo.vhd -e vai_fifo
+prep -top vai_fifo
+#chformal -assume -remove vai_fifo/*
+chformal -assume -remove vai_fifo/i_fifo
+
+[files]
+../fifo/fifo.vhd
+vai_fifo.vhd

vai_fifo/vai_fifo.vhd

@@ -0,0 +1,81 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+
+
+entity vai_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
+    Valid_i      : in  std_logic;
+    Accept_o     : out std_logic;
+    Din_i        : in  std_logic_vector(Width-1 downto 0);
+    -- read
+    Valid_o      : out std_logic;
+    Accept_i     : in  std_logic;
+    Dout_o       : out std_logic_vector(Width-1 downto 0)
+  );
+end entity vai_fifo;
+
+
+architecture rtl of vai_fifo is
+
+
+  signal s_wen : std_logic;
+  signal s_ren : std_logic;
+
+  signal s_full  : std_logic;
+  signal s_empty : 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        => s_wen,
+    Din_i        => Din_i,
+    Full_o       => s_full,
+    Werror_o     => open,
+    -- read
+    Ren_i        => s_ren,
+    Dout_o       => Dout_o,
+    Empty_o      => s_empty,
+    Rerror_o     => open
+  );
+
+
+  s_wen <= Valid_i and not s_full;
+  s_ren <= Accept_i and not s_empty;
+
+  Accept_o <= not s_full;
+  Valid_o  <= not s_empty;
+
+
+
+  FormalG : if Formal generate
+
+    default clock is rising_edge(Clk_i);
+
+    -- Inputs are low during reset for simplicity
+    vai_fifo_reset_a : assume always not Reset_n_i -> not Valid_i and not Accept_i;
+
+  end generate FormalG;
+
+
+end architecture rtl;