From e9b4035e8d36cd7d5b8b23f23db81703727e1005 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Thu, 4 Feb 2021 00:55:04 +0100 Subject: [PATCH] Add fwft-fifo & use that for vai-fifo; minor fixes --- fwft_fifo/Makefile | 19 ++++++++ fwft_fifo/fwft_fifo.vhd | 98 ++++++++++++++++++++++++++++++++++++++++ fwft_fifo/symbiyosys.sby | 30 ++++++++++++ tests.txt | 1 + vai_fifo/Makefile | 4 +- vai_fifo/symbiyosys.sby | 9 ++-- vai_fifo/vai_fifo.vhd | 2 +- 7 files changed, 157 insertions(+), 6 deletions(-) create mode 100644 fwft_fifo/Makefile create mode 100644 fwft_fifo/fwft_fifo.vhd create mode 100644 fwft_fifo/symbiyosys.sby diff --git a/fwft_fifo/Makefile b/fwft_fifo/Makefile new file mode 100644 index 0000000..d29c14a --- /dev/null +++ b/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 diff --git a/fwft_fifo/fwft_fifo.vhd b/fwft_fifo/fwft_fifo.vhd new file mode 100644 index 0000000..9660584 --- /dev/null +++ b/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; diff --git a/fwft_fifo/symbiyosys.sby b/fwft_fifo/symbiyosys.sby new file mode 100644 index 0000000..6bf70c4 --- /dev/null +++ b/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 diff --git a/tests.txt b/tests.txt index 14b17e3..15d64e0 100644 --- a/tests.txt +++ b/tests.txt @@ -1,5 +1,6 @@ alu counter fifo +fwft_fifo vai_fifo vai_reg \ No newline at end of file diff --git a/vai_fifo/Makefile b/vai_fifo/Makefile index 71e4d4c..4046d8b 100644 --- a/vai_fifo/Makefile +++ b/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 diff --git a/vai_fifo/symbiyosys.sby b/vai_fifo/symbiyosys.sby index ec6019f..dcfbaeb 100644 --- a/vai_fifo/symbiyosys.sby +++ b/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 diff --git a/vai_fifo/vai_fifo.vhd b/vai_fifo/vai_fifo.vhd index dde4459..27497b9 100644 --- a/vai_fifo/vai_fifo.vhd +++ b/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,