testsuite/synth: add a test for #2214

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"