avm_arbit.psl

vunit i_avm_arbit(avm_arbit(synthesis))
{
   -- Additional signals used during formal verification
   signal f_count : integer range 0 to 3 := 0;


   -- 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_s0_wr_burstcount  : integer;   -- Remaining amount of write data
   signal f_s0_rd_burstcount  : integer;   -- Remaining amount of read data
   signal f_s0_avm_address    : std_logic_vector(G_ADDRESS_SIZE-1 downto 0);
   signal f_s0_avm_burstcount : std_logic_vector(7 downto 0);

   p_s0_wr_burstcount : process (clk_i)
   begin
      if rising_edge(clk_i) then
         if s0_avm_write_i and not s0_avm_waitrequest_o then
            if f_s0_wr_burstcount = 0 then
               f_s0_wr_burstcount <= to_integer(s0_avm_burstcount_i) - 1;
            else
               f_s0_wr_burstcount <= f_s0_wr_burstcount - 1;
            end if;
         end if;
         if rst_i then
            f_s0_wr_burstcount <= 0;
         end if;
      end if;
   end process p_s0_wr_burstcount;

   p_s0_rd_burstcount : process (clk_i)
   begin
      if rising_edge(clk_i) then
         if s0_avm_readdatavalid_o then
            f_s0_rd_burstcount <= f_s0_rd_burstcount - 1;
         end if;
         if s0_avm_read_i and not s0_avm_waitrequest_o then
            f_s0_rd_burstcount <= to_integer(s0_avm_burstcount_i);
         end if;
         if rst_i then
            f_s0_rd_burstcount <= 0;
         end if;
      end if;
   end process p_s0_rd_burstcount;

   p_s0_avm : process (clk_i)
   begin
      if rising_edge(clk_i) then
         if f_s0_wr_burstcount = 0 and
            f_s0_rd_burstcount = 0 and
            rst_i = '0' and
            (s0_avm_write_i or s0_avm_read_i) = '1' and
            s0_avm_burstcount_i > X"01" then
            f_s0_avm_burstcount <= s0_avm_burstcount_i;
            f_s0_avm_address    <= s0_avm_address_i;
         end if;
      end if;
   end process p_s0_avm;


   signal f_s1_wr_burstcount  : integer;   -- Remaining amount of write data
   signal f_s1_rd_burstcount  : integer;   -- Remaining amount of read data
   signal f_s1_avm_address    : std_logic_vector(G_ADDRESS_SIZE-1 downto 0);
   signal f_s1_avm_burstcount : std_logic_vector(7 downto 0);

   p_s1_wr_burstcount : process (clk_i)
   begin
      if rising_edge(clk_i) then
         if s1_avm_write_i and not s1_avm_waitrequest_o then
            if f_s1_wr_burstcount = 0 then
               f_s1_wr_burstcount <= to_integer(s1_avm_burstcount_i) - 1;
            else
               f_s1_wr_burstcount <= f_s1_wr_burstcount - 1;
            end if;
         end if;
         if rst_i then
            f_s1_wr_burstcount <= 0;
         end if;
      end if;
   end process p_s1_wr_burstcount;

   p_s1_rd_burstcount : process (clk_i)
   begin
      if rising_edge(clk_i) then
         if s1_avm_readdatavalid_o then
            f_s1_rd_burstcount <= f_s1_rd_burstcount - 1;
         end if;
         if s1_avm_read_i and not s1_avm_waitrequest_o then
            f_s1_rd_burstcount <= to_integer(s1_avm_burstcount_i);
         end if;
         if rst_i then
            f_s1_rd_burstcount <= 0;
         end if;
      end if;
   end process p_s1_rd_burstcount;

   p_s1_avm : process (clk_i)
   begin
      if rising_edge(clk_i) then
         if f_s1_wr_burstcount = 0 and
            f_s1_rd_burstcount = 0 and
            rst_i = '0' and
            (s1_avm_write_i or s1_avm_read_i) = '1' and
            s1_avm_burstcount_i > X"01" then
            f_s1_avm_burstcount <= s1_avm_burstcount_i;
            f_s1_avm_address    <= s1_avm_address_i;
         end if;
      end if;
   end process p_s1_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;


   -----------------------------
   -- 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 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));


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

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

   -- Slave may not assert both write and read.
   f_slave0_request_not_double: assume always not (s0_avm_write_i and s0_avm_read_i);
   f_slave1_request_not_double: assume always not (s1_avm_write_i and s1_avm_read_i);

   -- Slave request may be stable until accepted
   f_slave0_input_stable : assume always {(s0_avm_write_i or s0_avm_read_i) and
                                          s0_avm_waitrequest_o and
                                          not rst_i}
                                     |=> {stable(s0_avm_write_i) and
                                          stable(s0_avm_read_i) and
                                          stable(s0_avm_address_i) and
                                          stable(s0_avm_writedata_i) and
                                          stable(s0_avm_byteenable_i) and
                                          stable(s0_avm_burstcount_i)};

   f_slave1_input_stable : assume always {(s1_avm_write_i or s1_avm_read_i) and
                                          s1_avm_waitrequest_o and
                                          not rst_i}
                                     |=> {stable(s1_avm_write_i) and
                                          stable(s1_avm_read_i) and
                                          stable(s1_avm_address_i) and
                                          stable(s1_avm_writedata_i) and
                                          stable(s1_avm_byteenable_i) and
                                          stable(s1_avm_burstcount_i)};

   -- Slave may not issue any new request during a read burst transfer
   f_slave0_no_new_burst : assume always {f_s0_rd_burstcount /= 0 and rst_i = '0'}
                                     |-> not (s0_avm_write_i or s0_avm_read_i);
   f_slave1_no_new_burst : assume always {f_s1_rd_burstcount /= 0 and rst_i = '0'}
                                     |-> not (s1_avm_write_i or s1_avm_read_i);

   -- Slave may not issue new read request during a write burst transfer
   f_slave0_no_new_read : assume always {f_s0_wr_burstcount /= 0 and rst_i = '0'}
                                    |-> not (s0_avm_read_i);
   f_slave1_no_new_read : assume always {f_s1_wr_burstcount /= 0 and rst_i = '0'}
                                    |-> not (s1_avm_read_i);

   -- Slave may not have both read and write burst simultaneously ongoing
   f_slave0_only_one_burst : assume always f_s0_rd_burstcount = 0 or f_s0_wr_burstcount = 0 or rst_i = '1';
   f_slave1_only_one_burst : assume always f_s1_rd_burstcount = 0 or f_s1_wr_burstcount = 0 or rst_i = '1';

   -- Slave may keep burstcount and address stable during burst transfer
   f_slave0_burst_stable : assume always {(f_s0_rd_burstcount /= 0 or f_s0_wr_burstcount /= 0) and
                                         rst_i = '0' and
                                         (s0_avm_write_i or s0_avm_read_i) = '1'}
                                    |-> {s0_avm_burstcount_i = f_s0_avm_burstcount and
                                         s0_avm_address_i = f_s0_avm_address};
   f_slave1_burst_stable : assume always {(f_s1_rd_burstcount /= 0 or f_s1_wr_burstcount /= 0) and
                                         rst_i = '0' and
                                         (s1_avm_write_i or s1_avm_read_i) = '1'}
                                    |-> {s1_avm_burstcount_i = f_s1_avm_burstcount and
                                         s1_avm_address_i = f_s1_avm_address};

   -- Slave may not issue zero burst
   f_slave0_burst_valid  : assume always rst_i or not ((s0_avm_write_i or s0_avm_read_i) and nor(s0_avm_burstcount_i));
   f_slave1_burst_valid  : assume always rst_i or not ((s1_avm_write_i or s1_avm_read_i) and nor(s1_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
   --------------------------------------------

} -- vunit i_avm_arbit(avm_arbit(synthesis))