diff options
Diffstat (limited to 'testsuite/synth')
| -rw-r--r-- | testsuite/synth/issue2214/avm_cache.psl | 162 | ||||
| -rw-r--r-- | testsuite/synth/issue2214/avm_cache.sby | 18 | ||||
| -rw-r--r-- | testsuite/synth/issue2214/avm_cache.vhd | 158 | ||||
| -rwxr-xr-x | testsuite/synth/issue2214/testsuite.sh | 8 |
4 files changed, 346 insertions, 0 deletions
diff --git a/testsuite/synth/issue2214/avm_cache.psl b/testsuite/synth/issue2214/avm_cache.psl new file mode 100644 index 000000000..87c8dace2 --- /dev/null +++ b/testsuite/synth/issue2214/avm_cache.psl @@ -0,0 +1,162 @@ +vunit i_avm_cache(avm_cache(synthesis)) +{ + -- set all declarations to run on clk_i + default clock is rising_edge(clk_i); + + -- Additional signals used during formal verification + signal f_s_rd_burstcount : integer; + signal f_m_rd_burstcount : integer; + + p_s_rd_burstcount : process (clk_i) + begin + if rising_edge(clk_i) then + if s_avm_readdatavalid_o then + f_s_rd_burstcount <= f_s_rd_burstcount - 1; + end if; + if s_avm_read_i and not s_avm_waitrequest_o then + f_s_rd_burstcount <= to_integer(s_avm_burstcount_i); + end if; + if rst_i then + f_s_rd_burstcount <= 0; + end if; + end if; + end process p_s_rd_burstcount; + + p_m_rd_burstcount : process (clk_i) + begin + if rising_edge(clk_i) then + if m_avm_readdatavalid_i then + f_m_rd_burstcount <= f_m_rd_burstcount - 1; + end if; + if m_avm_read_o and not m_avm_waitrequest_i then + f_m_rd_burstcount <= to_integer(m_avm_burstcount_o); + end if; + if rst_i then + f_m_rd_burstcount <= 0; + end if; + end if; + end process p_m_rd_burstcount; + + signal f_s_written : std_logic := '0'; + signal f_s_data : std_logic_vector(G_DATA_SIZE-1 downto 0); + signal f_s_read : std_logic := '0'; + signal f_m_written : std_logic := '0'; + signal f_m_data : std_logic_vector(G_DATA_SIZE-1 downto 0); + signal f_m_read : std_logic := '0'; + signal f_addr : std_logic_vector(G_ADDRESS_SIZE-1 downto 0); + attribute anyconst : boolean; + attribute anyconst of f_addr : signal is true; + + p_s_write : process (clk_i) + begin + if rising_edge(clk_i) then + if s_avm_write_i and not s_avm_waitrequest_o then + if s_avm_address_i = f_addr then + f_s_data <= s_avm_writedata_i; + f_s_written <= '1'; + end if; + end if; + end if; + end process p_s_write; + + p_s_read : process (clk_i) + begin + if rising_edge(clk_i) then + if s_avm_read_i and not s_avm_waitrequest_o then + if s_avm_address_i = f_addr then + f_s_read <= '1'; + end if; + end if; + + if f_s_read = '1' and s_avm_readdatavalid_o = '1' then + f_s_read <= '0'; + end if; + end if; + end process p_s_read; + + p_m_write : process (clk_i) + begin + if rising_edge(clk_i) then + if m_avm_write_o and not m_avm_waitrequest_i then + if m_avm_address_o = f_addr then + f_m_data <= m_avm_writedata_o; + f_m_written <= '1'; + end if; + end if; + end if; + end process p_m_write; + + p_m_read : process (clk_i) + begin + if rising_edge(clk_i) then + if m_avm_read_o and not m_avm_waitrequest_i then + if m_avm_address_o = f_addr then + f_m_read <= '1'; + end if; + end if; + + if f_m_read = '1' and m_avm_readdatavalid_i = '1' then + f_m_read <= '0'; + end if; + end if; + end process p_m_read; + + f_slave : assert always f_s_written and f_s_read and s_avm_readdatavalid_o |-> s_avm_readdata_o = f_s_data; + + f_master : assume always f_m_written and f_m_read and m_avm_readdatavalid_i |-> m_avm_readdata_i = f_m_data; + + + + ----------------------------- + -- ASSERTIONS ABOUT OUTPUTS + ----------------------------- + + -- Master must be empty after reset + f_master_after_reset_empty : assert always {rst_i} |=> not (m_avm_write_o or m_avm_read_o); + + -- Master may not assert both write and read. + f_master_not_double: assert always rst_i or not (m_avm_write_o and m_avm_read_o); + + -- Master must be stable until accepted + f_master_stable : assert always {(m_avm_write_o or m_avm_read_o) and m_avm_waitrequest_i and not rst_i} |=> + {stable(m_avm_write_o) and stable(m_avm_read_o) and stable(m_avm_address_o) and stable(m_avm_writedata_o) and + stable(m_avm_byteenable_o) and stable(m_avm_burstcount_o)}; + + f_master_burst_valid : assert always rst_i or not (m_avm_read_o and not m_avm_waitrequest_i and nor(m_avm_burstcount_o)); + f_slave_burst_reset : assert always rst_i |=> {f_s_rd_burstcount = 0}; + f_slave_burst_range : assert always rst_i or f_s_rd_burstcount >= 0; + f_slave_burst_block : assert always rst_i or f_s_rd_burstcount = 0 or s_avm_waitrequest_o or (f_s_rd_burstcount = 1 and s_avm_readdatavalid_o = '1'); + f_slave_no_data : assert always rst_i or not (f_s_rd_burstcount = 0 and s_avm_readdatavalid_o = '1'); + + + ----------------------------- + -- ASSUMPTIONS ABOUT INPUTS + ----------------------------- + + -- Require reset at startup. + f_reset : assume {rst_i}; + + -- Slave must be empty after reset + f_slave_after_reset_empty : assume always {rst_i} |=> not (s_avm_write_i or s_avm_read_i); + + -- Slave may not assert both write and read. + f_slave_not_double: assume always not (s_avm_write_i and s_avm_read_i); + + -- Slaves must be stable until accepted + f_slave_input_stable : assume always {(s_avm_write_i or s_avm_read_i) and s_avm_waitrequest_o and not rst_i} |=> + {stable(s_avm_write_i) and stable(s_avm_read_i) and stable(s_avm_address_i) and stable(s_avm_writedata_i) and + stable(s_avm_byteenable_i) and stable(s_avm_burstcount_i)}; + + f_slave_burst_valid : assume always rst_i or not (s_avm_read_i and not s_avm_waitrequest_o and nor(s_avm_burstcount_i)); + f_master_burst_reset : assume always rst_i |=> {f_m_rd_burstcount = 0}; + f_master_burst_range : assume always rst_i or f_m_rd_burstcount >= 0; + f_master_burst_block : assume always rst_i or f_m_rd_burstcount = 0 or m_avm_waitrequest_i or (f_m_rd_burstcount = 1 and m_avm_readdatavalid_i = '1'); + f_master_no_data : assume always rst_i or not (f_m_rd_burstcount = 0 and m_avm_readdatavalid_i = '1'); + + + -------------------------------------------- + -- COVER STATEMENTS TO VERIFY REACHABILITY + -------------------------------------------- + +} -- vunit i_avm_cache(avm_cache(synthesis)) + diff --git a/testsuite/synth/issue2214/avm_cache.sby b/testsuite/synth/issue2214/avm_cache.sby new file mode 100644 index 000000000..1a5498fd7 --- /dev/null +++ b/testsuite/synth/issue2214/avm_cache.sby @@ -0,0 +1,18 @@ +[tasks] +bmc + +[options] +bmc: mode bmc +bmc: depth 6 + +[engines] +smtbmc + +[script] +ghdl --std=08 -gG_CACHE_SIZE=8 -gG_ADDRESS_SIZE=4 -gG_DATA_SIZE=8 avm_cache.vhd avm_cache.psl -e avm_cache +prep -top avm_cache + +[files] +avm_cache.psl +avm_cache.vhd + diff --git a/testsuite/synth/issue2214/avm_cache.vhd b/testsuite/synth/issue2214/avm_cache.vhd new file mode 100644 index 000000000..5e84b69ff --- /dev/null +++ b/testsuite/synth/issue2214/avm_cache.vhd @@ -0,0 +1,158 @@ +-- This module implements a very simple read cache with just one cache line. +-- +-- Created by Michael Jørgensen in 2022 (mjoergen.github.io/HyperRAM). + +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; +use ieee.numeric_std_unsigned.all; + +entity avm_cache is + generic ( + G_CACHE_SIZE : integer; + G_ADDRESS_SIZE : integer; -- Number of bits + G_DATA_SIZE : integer -- Number of bits + ); + port ( + clk_i : in std_logic; + rst_i : in std_logic; + s_avm_waitrequest_o : out std_logic; + s_avm_write_i : in std_logic; + s_avm_read_i : in std_logic; + s_avm_address_i : in std_logic_vector(G_ADDRESS_SIZE-1 downto 0); + s_avm_writedata_i : in std_logic_vector(G_DATA_SIZE-1 downto 0); + s_avm_byteenable_i : in std_logic_vector(G_DATA_SIZE/8-1 downto 0); + s_avm_burstcount_i : in std_logic_vector(7 downto 0); + s_avm_readdata_o : out std_logic_vector(G_DATA_SIZE-1 downto 0); + s_avm_readdatavalid_o : out std_logic; + m_avm_waitrequest_i : in std_logic; + m_avm_write_o : out std_logic; + m_avm_read_o : out std_logic; + m_avm_address_o : out std_logic_vector(G_ADDRESS_SIZE-1 downto 0); + m_avm_writedata_o : out std_logic_vector(G_DATA_SIZE-1 downto 0); + m_avm_byteenable_o : out std_logic_vector(G_DATA_SIZE/8-1 downto 0); + m_avm_burstcount_o : out std_logic_vector(7 downto 0); + m_avm_readdata_i : in std_logic_vector(G_DATA_SIZE-1 downto 0); + m_avm_readdatavalid_i : in std_logic + ); +end entity avm_cache; + +architecture synthesis of avm_cache is + + type mem_t is array (0 to G_CACHE_SIZE-1) of std_logic_vector(G_DATA_SIZE-1 downto 0); + type t_state is (IDLE_ST, READING_ST); + + -- Registers + signal cache_data : mem_t; + signal cache_addr : std_logic_vector(G_ADDRESS_SIZE-1 downto 0); + signal cache_valid : std_logic; + signal cache_count : natural range 0 to G_CACHE_SIZE; + signal rd_burstcount : std_logic_vector(7 downto 0); + signal state : t_state := IDLE_ST; + + -- Combinatorial + signal cache_offset_s : std_logic_vector(G_ADDRESS_SIZE-1 downto 0); + +begin + + s_avm_waitrequest_o <= m_avm_waitrequest_i when state = IDLE_ST else + '1' when rd_burstcount /= X"00" else + '0' when (cache_valid = '1' or cache_offset_s < cache_count) and s_avm_read_i = '1' and s_avm_burstcount_i = X"01" else + '1'; + + -- Two's complement, i.e. wrap-around + cache_offset_s <= std_logic_vector(unsigned(s_avm_address_i) - unsigned(cache_addr)); + + p_fsm : process (clk_i) + begin + if rising_edge(clk_i) then + s_avm_readdata_o <= (others => '0'); + s_avm_readdatavalid_o <= '0'; + + if m_avm_waitrequest_i = '0' then + m_avm_write_o <= '0'; + m_avm_read_o <= '0'; + m_avm_address_o <= (others => '0'); + m_avm_writedata_o <= (others => '0'); + m_avm_byteenable_o <= (others => '0'); + m_avm_burstcount_o <= (others => '0'); + end if; + + case state is + when IDLE_ST => + assert not (s_avm_write_i = '1' and s_avm_read_i = '1'); + + if s_avm_write_i = '1' and s_avm_waitrequest_o = '0' then + m_avm_write_o <= s_avm_write_i; + m_avm_read_o <= s_avm_read_i; + m_avm_address_o <= s_avm_address_i; + m_avm_writedata_o <= s_avm_writedata_i; + m_avm_byteenable_o <= s_avm_byteenable_i; + m_avm_burstcount_o <= s_avm_burstcount_i; + if cache_offset_s < G_CACHE_SIZE then + cache_valid <= '0'; + cache_count <= to_integer(cache_offset_s); + cache_data(to_integer(cache_offset_s)) <= s_avm_writedata_i; + end if; + state <= IDLE_ST; + end if; + + if s_avm_read_i = '1' and s_avm_waitrequest_o = '0' then + if (cache_valid = '1' or cache_offset_s < cache_count) and cache_offset_s < G_CACHE_SIZE and s_avm_burstcount_i = X"01" then + s_avm_readdata_o <= cache_data(to_integer(cache_offset_s)); + s_avm_readdatavalid_o <= '1'; + else + m_avm_write_o <= '0'; + m_avm_read_o <= '1'; + m_avm_address_o <= s_avm_address_i; + m_avm_burstcount_o <= to_stdlogicvector(G_CACHE_SIZE, 8); + rd_burstcount <= s_avm_burstcount_i; + cache_valid <= '0'; + cache_count <= 0; + cache_addr <= s_avm_address_i; + state <= READING_ST; + end if; + end if; + + -- Reading data into cache + when READING_ST => + if m_avm_readdatavalid_i = '1' then + cache_data(cache_count) <= m_avm_readdata_i; + if rd_burstcount /= 0 then + s_avm_readdata_o <= m_avm_readdata_i; + s_avm_readdatavalid_o <= '1'; + rd_burstcount <= std_logic_vector(unsigned(rd_burstcount) - 1); + end if; + + if cache_count >= G_CACHE_SIZE-1 then + cache_count <= G_CACHE_SIZE; + cache_valid <= '1'; + state <= IDLE_ST; + else + cache_count <= cache_count + 1; + end if; + end if; + + if s_avm_waitrequest_o = '0' and s_avm_read_i = '1' and s_avm_burstcount_i = X"01" then + s_avm_readdata_o <= cache_data(to_integer(cache_offset_s)); + s_avm_readdatavalid_o <= '1'; + end if; + + when others => + null; + + end case; + + if rst_i = '1' then + s_avm_readdatavalid_o <= '0'; + m_avm_write_o <= '0'; + m_avm_read_o <= '0'; + cache_valid <= '0'; + cache_count <= 0; + state <= IDLE_ST; + end if; + end if; + end process p_fsm; + +end architecture synthesis; + diff --git a/testsuite/synth/issue2214/testsuite.sh b/testsuite/synth/issue2214/testsuite.sh new file mode 100755 index 000000000..16e35475a --- /dev/null +++ b/testsuite/synth/issue2214/testsuite.sh @@ -0,0 +1,8 @@ +#! /bin/sh + +. ../../testenv.sh + +GHDL_STD_FLAGS=--std=08 +synth -gG_CACHE_SIZE=8 -gG_ADDRESS_SIZE=4 -gG_DATA_SIZE=8 avm_cache.vhd avm_cache.psl -e avm_cache > syn_avm_cache.vhdl + +echo "Test successful" |