tmeissner / formal_hw_verification Goto Github PK

Maybe the FIFO is empty after reset. If one write & read then at the same time, the FIFO don't goes out of empty state. This is caused by the condition to deassert the empty flag:

if (Wen_i = '1' and Ren_i = '0') then
  if ((s_write_pnt = s_read_pnt - 1) or
      (s_write_pnt = t_fifo_mem'high and s_read_pnt = t_fifo_mem'low)) then
    Full_o <= '1';
  end if;
  Empty_o <= '0';
end if;

At the same time, an read is ignored when FIFO is empty (and an read error is asserted). So the data is written into the FIFO memory but not read. Write pointer is incremented, read pointer not. So, the FIFO should be not empty after the first data was written into it, as the read from the empty FIFO before was ignored.

It's awful that these bug wasn't found by the formal checks. It shows that such simple low-level checks are not only tedious to write, but also often only incompletely test the design behaviour.