• fifo - (2005-01-16 19:00)

fifo

Author: Tomas Kratochvila

Generic FIFO with synchronous write and read. Resizeable width (in steps by 1 bit) and resizeable deep (=16, 32 or 64). Distributed RAM is used for FIFO implementation. Component was tested up to 180MHz.

VHDL source list from CVS: liberouter/vhdl_design/units/common/fifo/ (date: 2005-01-16 19:00)

fifo.vhd (vhdl)
../dp_distmem/dp_distmem.vhd (vhdl)

Preconditions

Formulas

Strong_write

	   AG( ! ( counter=MAX ))
        

The counter does not overflow.

Verified in 0.03 s.

Strong_read

          AG( ! ( counter=MIN ))
        

The counter does not underflow.

Verified in 0.03 s.

Check_full

          AG( ( full <-> counter=MAX-1 ))
        

FULL signal checking. The fifo is full if and only if the FULL signal is up.

Verified in 0.03 s.

Check_empty

          AG( ( empty <-> counter=MIN+1 ))
        

EMPTY signal checking. The fifo is empty if and only if the EMPTY signal is up.

Verified in 0.03 s.

Reach_full

          AG EF ( counter=(MAX-1) )
	

The fifo is sometimes full.

Verified in 0.03 s.

Reach_epmty

          AG EF ( counter=(MIN+1) )
	

The fifo is sometimes empty.

Verified in 0.03 s.

Read_from_and_write_to_the_same_address

   	  AG( ! ( MINUS & PLUS
           & ( fifo.write_address_0_ = fifo.read_address_0_ )
           & ( fifo.write_address_1_ = fifo.read_address_1_ )
           & ( fifo.write_address_2_ = fifo.read_address_2_ )
	   & ( fifo.write_address_3_ = fifo.read_address_3_ )
	   & ( fifo.reg_write_address_4_ = fifo.reg_read_address_4_ )
	      )   )
	

It is not possible to read from and write to the same address.

Verified in 0.03 s.

Reach_LSTBLK

		AG EF ( fifo.LSTBLK )
		

The LSTBLK signal is sometimes up.

Verified in 0.02 s.