• fifo_bram_status_small - (2007-02-22 12:00)
• fifo_bram_status_small - (2007-03-13 12:00)
• fifo_bram_status_small - (2007-04-21 18:00)

fifo_bram_status_small

Author: Vojtech Rehak

Specification of the VHDL unit is as follows: "BRAM FIFO component is an implementation of FIFO component composed of internal Virtex2 BRAM Memories. Number of items is given via generic parameter ITEMS (where number of BRAMs is computed during translation). Any data width can be reached by setting DATA_WIDTH and BRAM_TYPE generic parameters. Next, this Fifo component allows detection of a "Last Free Block" (via generic parameter BLOCK_SIZE) and the number of free items in the fifo (STATUS signal).

Write operation, EMPTY and FULL signals have the same behavioral as in the standard fifo component. Different bevavioral is registered during the Read operation and LSTBLK and STATUS signals. During the Read operation the output data are available on the DO port 2-3 clock cycles after read request (RD port). This delay is caused by registered BRAM memory and additional register "reg_data_out" behind the multiplex. Due to this delay, it's usefull to utilize the "DV" port, which is set, as soon as the valid output data are available on the "DO" port.

It can be very useful to detect a situation, when last N items are available in the FIFO space. For this reason, the LSTBLK signal is generated. So the LSTBLK signal is asserted, when FIFO contains N or less then N free items. Moreover, the STATUS signal report actual number of free items in the fifo."

In addition to the fifo_bram component, there is modelled a verification environment. This environment generates all possible input for the input signals CLK, RESET, WR, and RD. The "data in" input signal is unassigned because we do not care about data values. In our verification we focuse only on the control signals EMPTY, FULL, LSTBLK, and STATUS. To be able to do this, in the environment variable counter saves actual number of assigned items in the FIFO.

As was mentioned above, the VHDL design has two parameters ITEMS and BLOCK_SIZE. The verification was performed for the FIFOs with every parameters found in every Liberouter project exept of one with ITEMS=2048 and BLOCK_SIZE=256. For this parameter the verification exeeds the 3 GB of memory. The verification was performed also for all 1<=ITEMS<=58 and all reasonable combinations of BLOCK_SIZE (i.e. 0<=BLOCK_SIZE<=ITEMS). The presented results are common for all the verified possibilities (if not stated otherwise) and the listed duration of verification correspond to the case where ITEMS was defined as 512 and BLOCK_SIZE was defined as 8. And according the fifo_bram.vhd the BRAM_TYPE was defined as 36 and DATA_WIDTH was defined as 72.

This verification has shown that the design is incorrect for the values of BLOCK_SIZE = 0, when the STATUS signal is out of order. Otherwise the component follows the verified part of its specification.

The vhdl designers were asked to add this very important notice into the vhdl code, or fix the bug.

VHDL source list from CVS: liberouter/vhdl_design/units/common/fifo_bram/ (date: 2007-02-22 12:00)

fifo_bram_status.vhd (vhdl)

Preconditions

nonzero_block_size: BLOCK_SIZE > 0 When BLOCK_SIZE is equal to zero the last free block properties are disabled.

Formulas

Strong_write

      AG( ! ( counter = ITEMS + 1 ))
        

The counter does not overflow.

Verified in 5927.03 s.

Strong_read

      AG( ! ( counter = -1 ))
        

The counter does not underflow.

Verified in 5953.13 s.

Check_full

		AG( full <-> ( counter = ITEMS ) )
	

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

Verified in 10538.6 s.

Check_empty

		AG( empty <-> ( counter = 0 ) )
	

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

Verified in 5081.07 s.

Check_lstblk

		AG(
 	           ( ( ITEMS - counter ) <=  BLOCK_SIZE  )
		     <->
                   fifo.LSTBLK
                  )
		

The LSTBLK signal is up iff the number of empty items is less or equal than the size of the blocks.

Preconditions:
nonzero_block_size

Verified in 8334.23 s.

Reach_lstblk

		AG EF ( fifo.LSTBLK )
		

The LSTBLK signal is sometimes up. The formula is false if LSTB_ADDR==0 (and so the relevant vhdl code is not synthesized).

Preconditions:
nonzero_block_size

Verified in 70.53 s.

Reach_full

		AG EF ( counter = ITEMS )
		

The fifo is sometimes full.

Verified in 43.84 s.

Reach_empty

		AG EF ( counter = 0 )
		

The fifo is sometimes empty.

Verified in 25.64 s.

Status

		AG ( (ITEMS - counter) = status )
		

Status is equal to the number of free items in the fifo.

Verified in 8421.57 s.

Read_from_and_write_to_the_same_address

           AG( ! ( MINUS & PLUS
           & ( fifo.reg_write_addr_0_ = fifo.reg_read_addr_0_ )
           & ( fifo.reg_write_addr_1_ = fifo.reg_read_addr_1_ )
           & ( fifo.reg_write_addr_2_ = fifo.reg_read_addr_2_ )
	   & ( fifo.reg_write_addr_3_ = fifo.reg_read_addr_3_ )
           #if ITEMS < 33
           & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   #elif ITEMS < 65
	   & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	   #elif ITEMS < 129
	   & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	   & ( fifo.reg_write_addr_6_ = fifo.reg_read_addr_6_ )
	   #elif ITEMS < 257
	   & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	   & ( fifo.reg_write_addr_6_ = fifo.reg_read_addr_6_ )
	   & ( fifo.reg_write_addr_7_ = fifo.reg_read_addr_7_ )
           #elif ITEMS < 513
	   & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	   & ( fifo.reg_write_addr_6_ = fifo.reg_read_addr_6_ )
	   & ( fifo.reg_write_addr_7_ = fifo.reg_read_addr_7_ )
	   & ( fifo.reg_write_addr_8_ = fifo.reg_read_addr_8_ )
           #elif ITEMS < 1025
	   & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	   & ( fifo.reg_write_addr_6_ = fifo.reg_read_addr_6_ )
	   & ( fifo.reg_write_addr_7_ = fifo.reg_read_addr_7_ )
	   & ( fifo.reg_write_addr_8_ = fifo.reg_read_addr_8_ )
	   & ( fifo.reg_write_addr_9_ = fifo.reg_read_addr_9_ )
           #elif ITEMS < 2049
	   & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	   & ( fifo.reg_write_addr_6_ = fifo.reg_read_addr_6_ )
	   & ( fifo.reg_write_addr_7_ = fifo.reg_read_addr_7_ )
	   & ( fifo.reg_write_addr_8_ = fifo.reg_read_addr_8_ )
	   & ( fifo.reg_write_addr_9_ = fifo.reg_read_addr_9_ )
	   & ( fifo.reg_write_addr_10_ = fifo.reg_read_addr_10_ )
	   #endif
	      )   )
		

It is not possible to read from and write to the same address. This formula works only for less than 1025 items.

Verified in 1899.59 s.

fifo_bram_status_small

Author: Vojtech Rehak

Specification of the VHDL unit is as follows: "BRAM FIFO component is an implementation of FIFO component composed of internal Virtex2 BRAM Memories. Number of items is given via generic parameter ITEMS (where number of BRAMs is computed during translation). Any data width can be reached by setting DATA_WIDTH and BRAM_TYPE generic parameters. Next, this Fifo component allows detection of a "Last Free Block" (via generic parameter BLOCK_SIZE) and the number of free items in the fifo (STATUS signal).

Write operation, EMPTY and FULL signals have the same behavioral as in the standard fifo component. Different bevavioral is registered during the Read operation and LSTBLK and STATUS signals. During the Read operation the output data are available on the DO port 2-3 clock cycles after read request (RD port). This delay is caused by registered BRAM memory and additional register "reg_data_out" behind the multiplex. Due to this delay, it's usefull to utilize the "DV" port, which is set, as soon as the valid output data are available on the "DO" port.

It can be very useful to detect a situation, when last N items are available in the FIFO space. For this reason, the LSTBLK signal is generated. So the LSTBLK signal is asserted, when FIFO contains N or less then N free items. Moreover, the STATUS signal report actual number of free items in the fifo."

In addition to the fifo_bram component, there is modelled a verification environment. This environment generates all possible input for the input signals CLK, RESET, WR, and RD. The "data in" input signal is unassigned because we do not care about data values. In our verification we focuse only on the control signals EMPTY, FULL, LSTBLK, and STATUS. To be able to do this, in the environment variable counter saves actual number of assigned items in the FIFO.

As was mentioned above, the VHDL design has two parameters ITEMS and BLOCK_SIZE. The verification was performed for the FIFOs with every parameters found in every Liberouter project exept of one with ITEMS=2048 and BLOCK_SIZE=256. For this parameter the verification exeeds the 3 GB of memory. The verification was performed also for all 1<ITEMS<=129 and BLOCK_SIZE was defined as 0. All the formulas were satified according to these verifications. The listed duration of verification correspond to the case where ITEMS was defined as 512 and BLOCK_SIZE was defined as 0. And according the fifo_bram.vhd the BRAM_TYPE was defined as 36 and DATA_WIDTH was defined as 72.

This verification was focused on the instances with BLOCK_SIZE = 0, when the previous version of the fifo failed (see the previous verification report).

VHDL source list from CVS: liberouter/vhdl_design/units/common/fifo_bram/ (date: 2007-03-13 12:00)

fifo_bram_status.vhd (vhdl)

Preconditions

nonzero_block_size: BLOCK_SIZE > 0 When BLOCK_SIZE is equal to zero the last free block properties are disabled.

Formulas

Strong_write

      AG( ! ( counter = ITEMS + 1 ))
        

The counter does not overflow.

Verified in 6061.52 s.

Strong_read

      AG( ! ( counter = -1 ))
        

The counter does not underflow.

Verified in 6062.35 s.

Check_full

		AG( full <-> ( counter = ITEMS ) )
	

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

Verified in 10824.4 s.

Check_empty

		AG( empty <-> ( counter = 0 ) )
	

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

Verified in 5192.86 s.

Check_lstblk

		AG(
 	           ( ( ITEMS - counter ) <=  BLOCK_SIZE  )
		     <->
                   fifo.LSTBLK
                  )
		

The LSTBLK signal is up iff the number of empty items is less or equal than the size of the blocks.

Preconditions:
nonzero_block_size

Verified in 0.64 s.

Reach_lstblk

		AG EF ( fifo.LSTBLK )
		

The LSTBLK signal is sometimes up. The formula is false if LSTB_ADDR==0 (and so the relevant vhdl code is not synthesized).

Preconditions:
nonzero_block_size

Verified in 0.4 s.

Reach_full

		AG EF ( counter = ITEMS )
		

The fifo is sometimes full.

Reach_empty

		AG EF ( counter = 0 )
		

The fifo is sometimes empty.

Status

		AG ( (ITEMS - counter) = status )
		

Status is equal to the number of free items in the fifo.

Verified in 8562.84 s.

Read_from_and_write_to_the_same_address

           AG( ! ( MINUS & PLUS
           & ( fifo.reg_write_addr_0_ = fifo.reg_read_addr_0_ )
           #if ITEMS > 2
           & ( fifo.reg_write_addr_1_ = fifo.reg_read_addr_1_ )
	   #endif
           #if ITEMS > 4
           & ( fifo.reg_write_addr_2_ = fifo.reg_read_addr_2_ )
	   #endif
           #if ITEMS > 8
           & ( fifo.reg_write_addr_3_ = fifo.reg_read_addr_3_ )
	   #endif
           #if ITEMS > 16
           & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   #endif
	   #if ITEMS > 32
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	   #endif
	   #if ITEMS > 64
	   & ( fifo.reg_write_addr_6_ = fifo.reg_read_addr_6_ )
	   #endif
	   #if ITEMS > 128
	   & ( fifo.reg_write_addr_7_ = fifo.reg_read_addr_7_ )
	   #endif
           #if ITEMS > 256
	   & ( fifo.reg_write_addr_8_ = fifo.reg_read_addr_8_ )
	   #endif
           #if ITEMS > 512
	   & ( fifo.reg_write_addr_9_ = fifo.reg_read_addr_9_ )
	   #endif
           #if ITEMS > 1024
	   & ( fifo.reg_write_addr_10_ = fifo.reg_read_addr_10_ )
	   #endif
	      )   )
		

It is not possible to read from and write to the same address. This formula works only for less than 1025 items.

Verified in 1930.27 s.

fifo_bram_status_small

Author: Zdenek Rehak

Specification of the VHDL unit is as follows: "BRAM FIFO component is an implementation of FIFO component composed of internal Virtex2 BRAM Memories. Number of items is given via generic parameter ITEMS (where number of BRAMs is computed during translation). Any data width can be reached by setting DATA_WIDTH and BRAM_TYPE generic parameters. Next, this Fifo component allows detection of a "Last Free Block" (via generic parameter BLOCK_SIZE) and the number of free items in the fifo (STATUS signal).

Write operation, EMPTY and FULL signals have the same behavioral as in the standard fifo component. Different bevavioral is registered during the Read operation and LSTBLK and STATUS signals. During the Read operation the output data are available on the DO port 2-3 clock cycles after read request (RD port). This delay is caused by registered BRAM memory and additional register "reg_data_out" behind the multiplex. Due to this delay, it's usefull to utilize the "DV" port, which is set, as soon as the valid output data are available on the "DO" port.

It can be very useful to detect a situation, when last N items are available in the FIFO space. For this reason, the LSTBLK signal is generated. So the LSTBLK signal is asserted, when FIFO contains N or less then N free items. Moreover, the STATUS signal report actual number of free items in the fifo."

In addition to the fifo_bram component, there is modelled a verification environment. This environment generates all possible input for the input signals CLK, RESET, WR, and RD. The "data in" input signal is unassigned because we do not care about data values. In our verification we focuse only on the control signals EMPTY, FULL, LSTBLK, and STATUS. To be able to do this, in the environment variable counter saves actual number of assigned items in the FIFO.

As was mentioned above, the VHDL design has two parameters ITEMS and BLOCK_SIZE. The verification was performed for the FIFOs with every parameters found in every Liberouter project exept of one with ITEMS=2048 and BLOCK_SIZE=256. For this parameter the verification exeeds the 3 GB of memory. The verification was performed also for all 1<ITEMS<=129 and BLOCK_SIZE was defined as 0. All the formulas were satified according to these verifications. The listed duration of verification correspond to the case where ITEMS was defined as 512 and BLOCK_SIZE was defined as 0. And according the fifo_bram.vhd the BRAM_TYPE was defined as 36 and DATA_WIDTH was defined as 72.

This verification was focused on new component version after problems with XST synthesis have been solved.

VHDL source list from CVS: liberouter/vhdl_design/units/common/fifo_bram/ (date: 2007-04-21 18:00)

fifo_bram_status.vhd (vhdl)

Preconditions

nonzero_block_size: BLOCK_SIZE > 0 When BLOCK_SIZE is equal to zero the last free block properties are disabled.

Formulas

Strong_write

      AG( ! ( counter = ITEMS + 1 ))
        

The counter does not overflow.

Verified in 7296.41 s.

Strong_read

      AG( ! ( counter = -1 ))
        

The counter does not underflow.

Verified in 7333.59 s.

Check_full

		AG( full <-> ( counter = ITEMS ) )
	

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

Verified in 10515.8 s.

Check_empty

		AG( empty <-> ( counter = 0 ) )
	

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

Verified in 9276.61 s.

Check_lstblk

		AG(
 	           ( ( ITEMS - counter ) <=  BLOCK_SIZE  )
		     <->
                   fifo.LSTBLK
                  )
		

The LSTBLK signal is up iff the number of empty items is less or equal than the size of the blocks.

Preconditions:
nonzero_block_size

Verified in 0.73 s.

Reach_lstblk

		AG EF ( fifo.LSTBLK )
		

The LSTBLK signal is sometimes up. The formula is false if LSTB_ADDR==0 (and so the relevant vhdl code is not synthesized).

Preconditions:
nonzero_block_size

Verified in 0.49 s.

Reach_full

		AG EF ( counter = ITEMS )
		

The fifo is sometimes full.

Reach_empty

		AG EF ( counter = 0 )
		

The fifo is sometimes empty.

Status

		AG ( (ITEMS - counter) = status )
		

Status is equal to the number of free items in the fifo.

Verified in 11946.9 s.

Read_from_and_write_to_the_same_address

           AG( ! ( MINUS & PLUS
           & ( fifo.reg_write_addr_0_ = fifo.reg_read_addr_0_ )
           #if ITEMS > 2
           & ( fifo.reg_write_addr_1_ = fifo.reg_read_addr_1_ )
	   #endif
           #if ITEMS > 4
           & ( fifo.reg_write_addr_2_ = fifo.reg_read_addr_2_ )
	   #endif
           #if ITEMS > 8
           & ( fifo.reg_write_addr_3_ = fifo.reg_read_addr_3_ )
	   #endif
           #if ITEMS > 16
           & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   #endif
	   #if ITEMS > 32
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	   #endif
	   #if ITEMS > 64
	   & ( fifo.reg_write_addr_6_ = fifo.reg_read_addr_6_ )
	   #endif
	   #if ITEMS > 128
	   & ( fifo.reg_write_addr_7_ = fifo.reg_read_addr_7_ )
	   #endif
           #if ITEMS > 256
	   & ( fifo.reg_write_addr_8_ = fifo.reg_read_addr_8_ )
	   #endif
           #if ITEMS > 512
	   & ( fifo.reg_write_addr_9_ = fifo.reg_read_addr_9_ )
	   #endif
           #if ITEMS > 1024
	   & ( fifo.reg_write_addr_10_ = fifo.reg_read_addr_10_ )
	   #endif
	      )   )
		

It is not possible to read from and write to the same address. This formula works only for less than 1025 items.

Verified in 2560.32 s.