avm_master2.psl

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

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


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

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


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

} -- vunit i_avm_master2(avm_master2(synthesis))