one_stage_fifo.psl

vunit i_one_stage_fifo(one_stage_fifo(synthesis))
{
   -- Additional signals used during formal verification
   signal f_last_value : std_logic_vector(G_DATA_SIZE-1 downto 0) := (others => '0');
   signal f_count      : integer range 0 to 3 := 0;


   -- set all declarations to run on clk_i
   default clock is rising_edge(clk_i);


   -----------------------------
   -- ASSERTIONS ABOUT OUTPUTS
   -----------------------------

   -- FIFO must be empty after reset
   f_after_reset : assert always {rst_i} |=> not m_valid_o;

   -- Output must be stable until accepted
   f_output_stable : assert always {m_valid_o and not m_ready_i and not rst_i} |=> {stable(m_valid_o) and stable(m_data_o)};

   -- Ready must be stable until new data
   f_ready_stable : assert always {s_ready_o and not s_valid_i and not rst_i} |=> {stable(s_ready_o)};

   -- Keep track of amount of data flowing into and out of the FIFO
   p_count : process (clk_i)
   begin
      if rising_edge(clk_i) then
         -- Data flowing in, but not out.
         if s_valid_i and s_ready_o and not (m_valid_o and m_ready_i) then
            f_count <= f_count + 1;
         end if;

         -- Data flowing out, but not in.
         if m_valid_o and m_ready_i and not (s_valid_i and s_ready_o) then
            f_count <= f_count - 1;
         end if;

         if rst_i then
            f_count <= 0;
         end if;
      end if;
   end process p_count;

   -- Keep track of data flowing into and out of the FIFO
   p_last_value : process (clk_i)
   begin
      if rising_edge(clk_i) then
         -- Remember last value written into FIFO
         if s_valid_i and s_ready_o then
            f_last_value <= s_data_i;
         end if;
      end if;
   end process p_last_value;

   -- The FIFO size is limited to 1.
   f_size : assert always {0 <= f_count and f_count <= 1};

   -- If FIFO is full, it must always present valid data on output
   f_count_1 : assert always {f_count = 1} |-> {m_valid_o = '1' and m_data_o = f_last_value} abort rst_i;

   -- If FIFO is empty, no data present on output
   f_count_0 : assert always {f_count = 0} |-> {m_valid_o = '0'} abort rst_i;


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

   -- Require reset at startup.
   f_reset : assume {rst_i};


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

   -- Make sure FIFO can transition from full to empty.
   f_full_to_empty : cover {m_valid_o and not rst_i; not m_valid_o};

} -- vunit i_one_stage_buffer(one_stage_buffer(synthesis))