fgc.psl

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


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

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

   -- Fox and Goat can not be alone
   f_fox_goat : assume always {bank_f_o = bank_g_o} |-> bank_m_o = bank_f_o;

   -- Goat and cabbage can not be alone
   f_goat_cabbage : assume always {bank_g_o = bank_c_o} |-> bank_m_o = bank_c_o;


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

   -- Attempt to have everything on bank 1
   cover {bank_m_o and bank_f_o and bank_g_o and bank_c_o};

} -- vunit i_fgc(fgc(synthesis))