avm_master3.psl

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


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

   -- 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 only issue 1-word burst
   f_master_no_burst : assert always {(m_avm_write_o or m_avm_read_o) and not rst_i}
                                 |-> {m_avm_burstcount_o = 1};

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


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

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

} -- vunit i_avm_pipe(avm_pipe(synthesis))