wb_mem.psl

vunit i_wb_mem(wb_mem(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);


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

   -- When wb_ack_o is de-asserted, then wb_data_o is all zeros.
   f_data_zero : assert always {not wb_ack_o} |-> {or(wb_data_o) = '0'};

   -- When writing to memory, the data output is unchanged.
   f_data_stable : assert always {wb_cyc_i and wb_stb_i and wb_we_i and not rst_i} |=> {stable(wb_data_o)};

   -- The response always appears on the exact following clock cycle, i.e. a fixed latency of 1.
   f_ack_next : assert always {wb_cyc_i and wb_stb_i and wb_we_i and not rst_i} |=> {wb_ack_o};

   -- No ACKs allowed when the bus is idle.
   f_ack_idle : assert always {not (wb_cyc_i and wb_stb_i)} |=> {not wb_ack_o};

   -- Keep track of outstanding requests
   p_count : process (clk_i)
   begin
      if rising_edge(clk_i) then
         -- Request without response
         if wb_cyc_i and wb_stb_i and not (wb_ack_o) then
            f_count <= f_count + 1;
         end if;

         -- Reponse without request
         if not(wb_cyc_i and wb_stb_i) and wb_ack_o then
            f_count <= f_count - 1;
         end if;

         if rst_i or not wb_cyc_i then
            f_count <= 0;
         end if;
      end if;
   end process p_count;

   -- At most one outstanding request
   f_outstanding : assert always {0 <= f_count and f_count <= 1};

   -- No ACK without outstanding request
   f_count_0 : assert always {f_count = 0} |-> {not wb_ack_o};

   -- ACK always comes immediately after an outstanding request
   f_count_1 : assert always {f_count = 1} |-> {wb_ack_o};

   -- Low CYC aborts all transactions
   f_idle : assert always {not wb_cyc_i} |=> {f_count = 0};


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

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


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

   -- Make sure memory can respond to a request
   f_full_to_empty : cover {f_count = 1; f_count = 0};

} -- vunit i_wb_mem(wb_mem(synthesis))