avm_cache.psl

vunit i_avm_cache(avm_cache(synthesis))
{
   -- set all declarations to run on clk_i
   default clock is rising_edge(clk_i);


   -----------------------------------------------
   -- Keep track of burst write and read on slave
   -----------------------------------------------

   signal f_s_wr_burstcount  : integer;   -- Remaining amount of write data
   signal f_s_rd_burstcount  : integer;   -- Remaining amount of read data
   signal f_s_avm_address    : std_logic_vector(G_ADDRESS_SIZE-1 downto 0);
   signal f_s_avm_burstcount : std_logic_vector(7 downto 0);

   p_s_wr_burstcount : process (clk_i)
   begin
      if rising_edge(clk_i) then
         if s_avm_write_i and not s_avm_waitrequest_o then
            if f_s_wr_burstcount = 0 then
               f_s_wr_burstcount <= to_integer(s_avm_burstcount_i) - 1;
            else
               f_s_wr_burstcount <= f_s_wr_burstcount - 1;
            end if;
         end if;
         if rst_i then
            f_s_wr_burstcount <= 0;
         end if;
      end if;
   end process p_s_wr_burstcount;

   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_s_avm : process (clk_i)
   begin
      if rising_edge(clk_i) then
         if f_s_wr_burstcount = 0 and
            f_s_rd_burstcount = 0 and
            rst_i = '0' and
            (s_avm_write_i or s_avm_read_i) = '1' and
            s_avm_burstcount_i > X"01" then
            f_s_avm_burstcount <= s_avm_burstcount_i;
            f_s_avm_address    <= s_avm_address_i;
         end if;
      end if;
   end process p_s_avm;


   ------------------------------------------------
   -- Keep track of burst write and read on master
   ------------------------------------------------

   signal f_m_wr_burstcount  : integer;   -- Remaining amount of write data
   signal f_m_rd_burstcount  : integer;   -- Remaining amount of read data
   signal f_m_avm_address    : std_logic_vector(G_ADDRESS_SIZE-1 downto 0);
   signal f_m_avm_burstcount : std_logic_vector(7 downto 0);

   p_m_wr_burstcount : process (clk_i)
   begin
      if rising_edge(clk_i) then
         if m_avm_write_o and not m_avm_waitrequest_i then
            if f_m_wr_burstcount = 0 then
               f_m_wr_burstcount <= to_integer(m_avm_burstcount_o) - 1;
            else
               f_m_wr_burstcount <= f_m_wr_burstcount - 1;
            end if;
         end if;
         if rst_i then
            f_m_wr_burstcount <= 0;
         end if;
      end if;
   end process p_m_wr_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;

   p_m_avm : process (clk_i)
   begin
      if rising_edge(clk_i) then
         if f_m_wr_burstcount = 0 and
            f_m_rd_burstcount = 0 and
            rst_i = '0' and
            (m_avm_write_o or m_avm_read_o) = '1' and
            m_avm_burstcount_o > X"01" then
            f_m_avm_burstcount <= m_avm_burstcount_o;
            f_m_avm_address    <= m_avm_address_o;
         end if;
      end if;
   end process p_m_avm;


   ------------------------------------------------------
   -- Additional signals used during formal verification
   ------------------------------------------------------

   signal f_s_wr_burstcount_s : integer;
   signal f_s_wr_address      : std_logic_vector(G_ADDRESS_SIZE-1 downto 0);
   signal f_s_written         : std_logic_vector(G_DATA_SIZE/8-1 downto 0) := (others => '0');
   signal f_s_read            : std_logic := '0';
   signal f_s_data            : std_logic_vector(G_DATA_SIZE-1 downto 0);
   signal f_addr              : std_logic_vector(G_ADDRESS_SIZE-1 downto 0);

   attribute anyconst : boolean;
   attribute anyconst of f_addr : signal is true;

   f_s_wr_burstcount_s <= 0 when f_s_wr_burstcount = 0 else
                          to_integer(s_avm_burstcount_i);

   -- Current address being written to
   f_s_wr_address <= std_logic_vector(unsigned(s_avm_address_i) + f_s_wr_burstcount_s - f_s_wr_burstcount);

   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 f_s_wr_address = f_addr then
               for i in 0 to G_DATA_SIZE/8-1 loop
                  if s_avm_byteenable_i(i) then
                     f_s_data(8*i+7 downto 8*i) <= s_avm_writedata_i(8*i+7 downto 8*i);
                     f_s_written(i) <= '1';
                  end if;
               end loop;
            end if;
         end if;
         if rst_i = '1' then
            f_s_written <= (others => '0');
         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 and s_avm_readdatavalid_o then
             f_s_read <= '0';
         end if;
         if rst_i = '1' then
            f_s_read <= '0';
         end if;
      end if;
   end process p_s_read;


   -----------------------------
   -- 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 must not assert both write and read.
   f_master_not_double: assert always {not rst_i} |-> not (m_avm_write_o and m_avm_read_o);

   -- Master request 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)};

   -- Master must not issue any new request during a read burst transfer
   f_master_no_new_burst : assert always {f_m_rd_burstcount /= 0 and rst_i = '0'}
                                      |-> not (m_avm_write_o or m_avm_read_o);

   -- Master must not issue new read request during a write burst transfer
   f_master_no_new_read : assert always {f_m_wr_burstcount /= 0 and rst_i = '0'}
                                     |-> not (m_avm_read_o);

   -- Master must not have both read and write burst simultaneously ongoing
   f_master_only_one_burst : assert always f_m_rd_burstcount = 0 or f_m_wr_burstcount = 0 or rst_i = '1';

   -- Master must keep burstcount and address stable during burst transfer
   f_master_burst_stable : assert always {(f_m_rd_burstcount /= 0 or f_m_wr_burstcount /= 0) and
                                          rst_i = '0' and
                                          (m_avm_write_o or m_avm_read_o) = '1'}
                                     |-> {m_avm_burstcount_o = f_m_avm_burstcount and
                                          m_avm_address_o = f_m_avm_address};


   -- Master must not issue zero burst
   f_master_burst_valid : assert always rst_i or not ((m_avm_write_o or m_avm_read_o) and nor(m_avm_burstcount_o));

   -- Slave must block requests during a read burst
   f_slave_wait : assert always (f_s_rd_burstcount > 1 or (f_s_rd_burstcount = 1 and s_avm_readdatavalid_o = '0')) and rst_i = '0'
                             |-> s_avm_waitrequest_o = '1';

   -- Slave must only respond with data to an ongoing request
   f_slave_read_data : assert always s_avm_readdatavalid_o and not rst_i |-> f_s_rd_burstcount > 0;

   -- Slave must read back data correctly
   f_slave : assert always (unsigned(f_s_written)+1 = 0) and f_s_read = '1' and s_avm_readdatavalid_o = '1'
                        |-> s_avm_readdata_o = f_s_data;


   -----------------------------
   -- ASSUMPTIONS ABOUT INPUTS
   -----------------------------

   -- There may be reset at startup.
   f_reset : assume {rst_i};

   -- Slave may not assert both write and read.
   f_slave_request_not_double : assume always not (s_avm_write_i and s_avm_read_i);

   -- Slave request may be stable until accepted
   f_slave_request_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)};

   -- Slave may not issue any new request during a read burst transfer
   f_slave_no_new_burst : assume always {f_s_rd_burstcount /= 0 and rst_i = '0'}
                                     |-> not (s_avm_write_i or s_avm_read_i);

   -- Slave may not issue new read request during a write burst transfer
   f_slave_no_new_read : assume always {f_s_wr_burstcount /= 0 and rst_i = '0'}
                                    |-> not (s_avm_read_i);

   -- Slave may not have both read and write burst simultaneously ongoing
   f_slave_only_one_burst : assume always f_s_rd_burstcount = 0 or f_s_wr_burstcount = 0 or rst_i = '1';

   -- Slave may keep burstcount and address stable during burst transfer
   f_slave_burst_stable : assume always {(f_s_rd_burstcount /= 0 or f_s_wr_burstcount /= 0) and
                                         rst_i = '0' and
                                         (s_avm_write_i or s_avm_read_i) = '1'}
                                    |-> {s_avm_burstcount_i = f_s_avm_burstcount and
                                         s_avm_address_i = f_s_avm_address};

   -- Slave may not issue zero burst
   f_slave_burst_valid  : assume always rst_i or not ((s_avm_write_i or s_avm_read_i) and nor(s_avm_burstcount_i));


   ---------------------
   -- Simulate a memory
   ---------------------

   type f_mem_t is array (0 to 2**G_ADDRESS_SIZE-1) of std_logic_vector(G_DATA_SIZE-1 downto 0);
   signal f_mem_data               : f_mem_t;
   signal f_mem_write_next_address : std_logic_vector(G_ADDRESS_SIZE-1 downto 0);
   signal f_mem_write_words_left   : std_logic_vector(7 downto 0);
   signal f_mem_read_next_address  : std_logic_vector(G_ADDRESS_SIZE-1 downto 0);
   signal f_mem_read_words_left    : std_logic_vector(7 downto 0);

   -- Block requests during a read burst
   f_mem_wait : assume always f_mem_read_words_left /= 0 |-> m_avm_waitrequest_i = '1';

   -- Handle read from memory
   f_mem_read : assume always m_avm_readdatavalid_i |-> m_avm_readdata_i = f_mem_data(to_integer(f_mem_read_next_address));

   -- Only respond with data to an ongoing request
   f_mem_read_data : assume always m_avm_readdatavalid_i |-> f_mem_read_words_left > 0;

   p_mem : process (clk_i)
   begin
      if rising_edge(clk_i) then
         if m_avm_write_o = '1' and m_avm_waitrequest_i = '0' then
            if f_mem_write_words_left = X"00" then
               f_mem_write_next_address <= std_logic_vector(unsigned(m_avm_address_o) + 1);
               f_mem_write_words_left   <= std_logic_vector(unsigned(m_avm_burstcount_o) - 1);
               for i in 0 to G_DATA_SIZE/8-1 loop
                  if m_avm_byteenable_o(i) then
                     f_mem_data(to_integer(m_avm_address_o))(8*i+7 downto 8*i) <= m_avm_writedata_o(8*i+7 downto 8*i);
                  end if;
               end loop;
            else
               f_mem_write_next_address <= std_logic_vector(unsigned(f_mem_write_next_address) + 1);
               f_mem_write_words_left   <= std_logic_vector(unsigned(f_mem_write_words_left) - 1);
               for i in 0 to G_DATA_SIZE/8-1 loop
                  if m_avm_byteenable_o(i) then
                     f_mem_data(to_integer(f_mem_write_next_address))(8*i+7 downto 8*i) <= m_avm_writedata_o(8*i+7 downto 8*i);
                  end if;
               end loop;
            end if;
         end if;

         if m_avm_readdatavalid_i = '1' then
            f_mem_read_next_address <= std_logic_vector(unsigned(f_mem_read_next_address) + 1);
            f_mem_read_words_left   <= std_logic_vector(unsigned(f_mem_read_words_left) - 1);
         end if;

         if m_avm_read_o = '1' and m_avm_waitrequest_i = '0' then
            f_mem_read_next_address <= std_logic_vector(unsigned(m_avm_address_o));
            f_mem_read_words_left   <= std_logic_vector(unsigned(m_avm_burstcount_o));
         end if;

         if rst_i = '1' then
            f_mem_write_words_left <= (others => '0');
            f_mem_read_words_left  <= (others => '0');
         end if;
      end if;
   end process p_mem;


   --------------------------------------------
   -- COVER STATEMENTS TO VERIFY REACHABILITY
   --------------------------------------------

   f_full : cover {
                   -- First issue a write
                   s_avm_write_i = '1' and
                   s_avm_waitrequest_o = '0' and
                   rst_i = '0';

                   [*];

                   -- Then read from the same cache line
                   s_avm_read_i = '1' and
                   s_avm_waitrequest_o = '0' and
                   cache_offset_s < cache_count;

                   [*];

                   -- Then wait for result to arrive
                   s_avm_readdatavalid_o = '1'
                   };

} -- vunit i_avm_cache(avm_cache(synthesis))