Verification Reports

fifo_bram5

Author: Vojtech Rehak
The model is a smaller version (5bit long address of each Block RAM, i.e. 31 items) of the fifo_bram in CVS.

VHDL source list from CVS: liberouter/vhdl_design/units/common/fifo_bram/ (date: 2004-07-26 12:00)

fifo_bram.vhd (vhdl)

Preconditions

Formulas

Strong_write

        AG( ! ( counter=MAX ))
The counter does not overflow.

Verified in 10.59 s.

Strong_read

        AG( ! ( counter=MIN ))
The counter does not underflow.

Verified in 10.61 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 15.47 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 11.68 s.

Check_last_block_more_than_one_plus1

		AG(
 	         ( (MAX-1-counter) > 1+((MAX-MIN-2)/BLOCK_NUMBER)
		     ->
                   ~fifo.LSTBLK
                 ) )
The LSTBLK signal is down if the number of empty items is greater than the size of one block plus one.

Verified in 1.24 s.

Check_last_block_less_than_one_minus1

		AG(
		         ( (MAX-1-counter) < (((MAX-MIN-2)/BLOCK_NUMBER )-1)
			            ->
                            fifo.LSTBLK
	              ) )
The LSTBLK signal is up if the number of empty items is smaller than the size of one block minus one.

Verified in 2.01 s.

Check_last_block_before_less_than_one_minus1

            ( (MAX-1-counter) >= (((MAX-MIN-2)/BLOCK_NUMBER)-1) U fifo.LSTBLK
              ) |
            G (MAX-1-counter) >= (((MAX-MIN-2)/BLOCK_NUMBER)-1)
The LSTBLK signal is up before the number of empty items is smaller than the size of one block.

Verified in 70.55 s.

Check_last_block_more_than_two

		AG(
 	         ( (MAX-1-counter) > (2*(MAX-MIN-2)/BLOCK_NUMBER)
		     ->
                   ~fifo.LSTBLK
                 ) )
The LSTBLK signal is down if the number of empty items is greater than the size of two blocks.

Verified in 8.09 s.

Check_last_block_less_than_one

		AG(
		         ( (MAX-1-counter) < ((MAX-MIN-2)/BLOCK_NUMBER )
			            ->
                            fifo.LSTBLK
	              ) )
The LSTBLK signal is up if the number of empty items is smaller than the size of one block.

Verified in 1.98 s.

Check_last_block_before_less_than_one

             ( (MAX-1-counter) >= ((MAX-MIN-2)/BLOCK_NUMBER) U fifo.LSTBLK
                ) |
               G (MAX-1-counter) >= ((MAX-MIN-2)/BLOCK_NUMBER)
The LSTBLK signal is up before the number of empty items is smaller than the size of one block.

Verified in 57.17 s.

Reach_LSTBLK

		AG EF ( fifo.LSTBLK )
The LSTBLK signal is sometimes up.

Verified in 8.53 s.

Reach_full

		AG EF ( counter=(MAX-1) )
The fifo is sometimes full.

Verified in 14.67 s.

Reach_empty

		AG EF ( counter=(MIN+1) )
The fifo is sometimes empty.

Verified in 12.55 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_ )
	   & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	      )   )
It is not possible to read from and write to the same address.

Verified in 9.58 s.

fifo_bram5

Author: Vojtech Rehak
The model is a smaller version (5bit long address of each Block RAM, i.e. 31 items) of the fifo_bram in CVS.

VHDL source list from CVS: liberouter/vhdl_design/units/common/fifo_bram/ (date: 2004-08-12 09:00)

fifo_bram.vhd (vhdl)

Preconditions

Formulas

Strong_write

      AG( ! ( counter=MAX ))
The counter does not overflow.

Verified in 8.45 s.

Strong_read

      AG( ! ( counter=MIN ))
The counter does not underflow.

Verified in 8.44 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 15.45 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 11.42 s.

Check_last_block_more_than_one_plus1

		AG(
 	         ( (MAX-1-counter) > 1+((MAX-MIN-2)/BLOCK_NUMBER)
		     ->
                   ~fifo.LSTBLK
                 ) )
The LSTBLK signal is down if the number of empty items is greater than the size of one block plus one.

Verified in 17.94 s.

Check_last_block_less_than_one_minus1

		AG(
		         ( (MAX-1-counter) < (((MAX-MIN-2)/BLOCK_NUMBER )-1)
			            ->
                            fifo.LSTBLK
	              ) )
The LSTBLK signal is up if the number of empty items is smaller than the size of one block minus one. The formula is false if LSTB_ADDR==0 (and so the relevant vhdl code is not synthesized).

Verified in 17.92 s.

Check_last_block_before_less_than_one_minus1

            ( (MAX-1-counter) >= (((MAX-MIN-2)/BLOCK_NUMBER)-1) U fifo.LSTBLK
              ) |
            G (MAX-1-counter) >= (((MAX-MIN-2)/BLOCK_NUMBER)-1)
The LSTBLK signal is up before the number of empty items is smaller than the size of one block. The formula is false if LSTB_ADDR==0 (and so the relevant vhdl code is not synthesized).

Verified in 152.34 s.

Check_last_block_more_than_two

		AG(
 	         ( (MAX-1-counter) > (2*(MAX-MIN-2)/BLOCK_NUMBER)
		     ->
                   ~fifo.LSTBLK
                 ) )
The LSTBLK signal is down if the number of empty items is greater than the size of two blocks.

Verified in 17.88 s.

Check_last_block_less_than_one

		AG(
		         ( (MAX-1-counter) < ((MAX-MIN-2)/BLOCK_NUMBER )
			            ->
                            fifo.LSTBLK
	              ) )
The LSTBLK signal is up if the number of empty items is smaller than the size of one block.

Verified in 2.23 s.

Check_last_block_before_less_than_one

             ( (MAX-1-counter) >= ((MAX-MIN-2)/BLOCK_NUMBER) U fifo.LSTBLK
                ) |
               G (MAX-1-counter) >= ((MAX-MIN-2)/BLOCK_NUMBER)
The LSTBLK signal is up before the number of empty items is smaller than the size of one block.

Verified in 107.51 s.

Reach_LSTBLK

		AG EF ( fifo.LSTBLK )
The LSTBLK signal is sometimes up.

Verified in 30.63 s.

Reach_full

		AG EF ( counter=(MAX-1) )
The fifo is sometimes full.

Verified in 14.59 s.

Reach_empty

		AG EF ( counter=(MIN+1) )
The fifo is sometimes empty.

Verified in 12.52 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_ )
	   & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	      )   )
It is not possible to read from and write to the same address.

Verified in 9.62 s.

fifo_bram5

Author: Vojtech Rehak

Specification of the VHDL unit is as follows: "BRAM FIFO component is an implementation of FIFO component composed of intermal Virtex2 BRAM Memories. Number of BRAMs is given via generic parameter EXADDR (where Number_of_BRAMs = 2^EXADDR). Next, this Fifo component allows detection of a "Last Free Block" (via generic parameter LSTB_ADDR).

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 signal. 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 than N free items. In current implementation, this signal is 1 clock cycle delayed."

Our verified model is a smaller version (5bit long address of each Block RAM, i.e. 31 items) of the described fifo_bram in CVS. 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, and LSTBLK. 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 EXADDR and LSTB_ADDR. The verification was performed for all 0<=EXADDR<=2 and all reasonable combinations of LSTB_ADDR (i.e. 0<=LSTB_ADDR<=EXADDR+5). 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 EXADDR was defined as 1 and LSTB_ADDR was defined as 2.

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

fifo_bram.vhd (vhdl)

Preconditions

fair_clock: G F (clock) The clock signal will be never set to 0 forever.

fair_non_clock: G F (~clock) The clock signal will be never set to 1 forever.

Formulas

Strong_write

      AG( ! ( counter=MAX ))
The counter does not overflow.

Verified in 8.47 s.

Strong_read

      AG( ! ( counter=MIN ))
The counter does not underflow.

Verified in 8.49 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 15.42 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 11.41 s.

Check_last_block_specification_up

		G(
 	          ( (MAX-1-counter) <= ((MAX-MIN-2)/BLOCK_NUMBER) )
		     ->
                  ( fifo.CLK U ( (~fifo.CLK) U ( (fifo.LSTBLK) | fifo.RESET ) ) )
                 )
Part of fifo_bram specification file: "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 than N free items. In current implementation, this signal is 1 clock cycle delayed." MAX-1-counter is the number of free items. (MAX-MIN-2)/BLOCK_NUMBER is the block size (i.e. N). The formula express that the LSTBLK signal is up when the specification decribes to be. The model does not satisfy this formula because LSTBLK signal is set when FIFO contains strictly less than N free items (not equal). See the Check_last_block_specification_up_changed formula.

Preconditions:
fair_clock, fair_non_clock

Verified in 39.1 s.

Check_last_block_specification_down

		G(
 	          ( (MAX-1-counter) > ((MAX-MIN-2)/BLOCK_NUMBER) )
		     ->
                  ( fifo.CLK U ( (~fifo.CLK) U ( (~fifo.LSTBLK) | fifo.RESET ) ) )
                 )
Part of fifo_bram specification file: "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 than N free items. In current implementation, this signal is 1 clock cycle delayed." MAX-1-counter is the number of free items. (MAX-MIN-2)/BLOCK_NUMBER is the block size (i.e. N). The formula express that the LSTBLK signal is down when the specification decribes to be. This formula is weaker than the the one that the model really satisfies. See the Check_last_block_specification_down_changed formula.

Preconditions:
fair_clock, fair_non_clock

Verified in 35.87 s.

Check_last_block_specification_up_changed

		G(
 	          ( (MAX-1-counter) < ((MAX-MIN-2)/BLOCK_NUMBER) )
		     ->
                  ( fifo.CLK U ( (~fifo.CLK) U ( (fifo.LSTBLK) | fifo.RESET ) ) )
                 )
Changed fifo_bram specification: "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 less than N free items. In current implementation, this signal is 1 clock cycle delayed." MAX-1-counter is the number of free items. (MAX-MIN-2)/BLOCK_NUMBER is the block size (i.e. N). The formula express that the LSTBLK signal is up when the changed specification decribes to be. The formula is false if LSTB_ADDR==0 (and so the relevant vhdl code is not synthesized).

Preconditions:
fair_clock, fair_non_clock

Verified in 38.01 s.

Check_last_block_specification_down_changed

		G(
 	          ( (MAX-1-counter) >= ((MAX-MIN-2)/BLOCK_NUMBER) )
		     ->
                  ( fifo.CLK U ( (~fifo.CLK) U ( (~fifo.LSTBLK) | fifo.RESET ) ) )
                 )
Changed fifo_bram specification: "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 less than N free items. In current implementation, this signal is 1 clock cycle delayed." MAX-1-counter is the number of free items. (MAX-MIN-2)/BLOCK_NUMBER is the block size (i.e. N). The formula express that the LSTBLK signal is down when the changed specification decribes to be.

Preconditions:
fair_clock, fair_non_clock

Verified in 35.63 s.

Check_last_block_more_than_two

		AG(
 	         ( (MAX-1-counter) > (2*(MAX-MIN-2)/BLOCK_NUMBER)
		     ->
                   ~fifo.LSTBLK
                 ) )
The LSTBLK signal is down if the number of empty items is greater than the size of two blocks.

Verified in 17.9 s.

Check_last_block_less_than_one

		AG(
		         ( (MAX-1-counter) < ((MAX-MIN-2)/BLOCK_NUMBER )
			            ->
                            fifo.LSTBLK
	              ) )
The LSTBLK signal is up if the number of empty items is smaller than the size of one block.

Verified in 2.2 s.

Check_last_block_before_less_than_one

             ( (MAX-1-counter) >= ((MAX-MIN-2)/BLOCK_NUMBER) U fifo.LSTBLK
                ) |
               G (MAX-1-counter) >= ((MAX-MIN-2)/BLOCK_NUMBER)
The LSTBLK signal is up before the number of empty items is smaller than the size of one block.

Verified in 107.13 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).

Verified in 30.78 s.

Reach_full

		AG EF ( counter=(MAX-1) )
The fifo is sometimes full.

Verified in 14.63 s.

Reach_empty

		AG EF ( counter=(MIN+1) )
The fifo is sometimes empty.

Verified in 12.51 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_ )
	   & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	      )   )
It is not possible to read from and write to the same address.

Verified in 9.62 s.

fifo_bram5

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). Next, this Fifo component allows detection of a "Last Free Block" (via generic parameter BLOCK_SIZE).

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 signal. 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."

Our verified model is a smaller version (5bit long address of each Block RAM, i.e. 31 items) of the described fifo_bram in CVS. 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, and LSTBLK. 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 presented results and the listed durations of verification correspond to the case where ITEMS was defined as 57 and BLOCK_SIZE was defined as 13. We find out that this VHDL design cannot be synthetized for ITEMS<=31. Hence, the verification was performed for no other combination of ITEMS and BLOCK_SIZE.

VHDL source list from CVS: liberouter/vhdl_design/units/common/fifo_bram/ (date: 2005-02-06 20:00)

fifo_bram.vhd (vhdl)

Preconditions

fair_clock: G F (clock) The clock signal will be never set to 0 forever.

fair_non_clock: G F (~clock) The clock signal will be never set to 1 forever.

Formulas

Strong_write

      AG( ! ( counter = ITEMS + 1 ))
The counter does not overflow.

Verified in 8.17 s.

Strong_read

      AG( ! ( counter = -1 ))
The counter does not underflow.

Verified in 8.18 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 21.15 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 7.64 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.

Verified in 11.82 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).

Verified in 24.98 s.

Reach_full

		AG EF ( counter = ITEMS )
The fifo is sometimes full.

Verified in 21.72 s.

Reach_empty

		AG EF ( counter = 0 )
The fifo is sometimes empty.

Verified in 12.58 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_ )
	   & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	      )   )
It is not possible to read from and write to the same address.

Verified in 6.77 s.

fifo_bram5

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). Next, this Fifo component allows detection of a "Last Free Block" (via generic parameter BLOCK_SIZE).

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 signal. 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."

Our verified model is a smaller version (5bit long address of each Block RAM, i.e. 31 items) of the described fifo_bram in CVS. 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, and LSTBLK. 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 all 0<=ITEMS<=? 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 57 and BLOCK_SIZE was defined as 13.

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

fifo_bram.vhd (vhdl)

Preconditions

fair_clock: G F (clock) The clock signal will be never set to 0 forever.

fair_non_clock: G F (~clock) The clock signal will be never set to 1 forever.

Formulas

Strong_write

      AG( ! ( counter = ITEMS + 1 ))
The counter does not overflow.

Verified in 8.24 s.

Strong_read

      AG( ! ( counter = -1 ))
The counter does not underflow.

Verified in 8.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 21.3 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 7.63 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.

Verified in 15.72 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).

Verified in 25.43 s.

Reach_full

		AG EF ( counter = ITEMS )
The fifo is sometimes full.

Verified in 21.77 s.

Reach_empty

		AG EF ( counter = 0 )
The fifo is sometimes empty.

Verified in 12.65 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_ )
	   & ( fifo.reg_write_addr_4_ = fifo.reg_read_addr_4_ )
	   & ( fifo.reg_write_addr_5_ = fifo.reg_read_addr_5_ )
	      )   )
It is not possible to read from and write to the same address.

Verified in 6.72 s.

fifo_bram5

Author: Tomas Kratochvila, 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).

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 signal. 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."

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, and LSTBLK. 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 2<=ITEMS<=128 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 57 and BLOCK_SIZE was defined as 13. And according the fifo_bram.vhd the BRAM_TYPE was defined as 18 and DATA_WIDTH was defined as 36.

This version changes the way how to initialize the memory. This version initialize memory using the dp_bmem common component.

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

fifo_bram.vhd (vhdl)

Preconditions

fair_clock: G F (clock) The clock signal will be never set to 0 forever.

fair_non_clock: G F (~clock) The clock signal will be never set to 1 forever.

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 32.66 s.

Strong_read

      AG( ! ( counter = -1 ))
The counter does not underflow.

Verified in 32.63 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 23.48 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 28.31 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 44.11 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 77.26 s.

Reach_full

		AG EF ( counter = ITEMS )
The fifo is sometimes full.

Verified in 81.47 s.

Reach_empty

		AG EF ( counter = 0 )
The fifo is sometimes empty.

Verified in 49.6 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.

Verified in 26.53 s.

fifo_bram5

Author: Tomas Kratochvila, 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).

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 signal. 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."

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, and LSTBLK. 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 2<=ITEMS<=128 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 57 and BLOCK_SIZE was defined as 13. And according the fifo_bram.vhd the BRAM_TYPE was defined as 18 and DATA_WIDTH was defined as 36.

This version changes only the ITEMS, BLOCK_SIZE, BRAM_TYPE and DATA_WIDTH initial values.

VHDL source list from CVS: liberouter/vhdl_design/units/common/fifo_bram/ (date: 2005-03-01 09:00)

fifo_bram.vhd (vhdl)

Preconditions

fair_clock: G F (clock) The clock signal will be never set to 0 forever.

fair_non_clock: G F (~clock) The clock signal will be never set to 1 forever.

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 16.42 s.

Strong_read

      AG( ! ( counter = -1 ))
The counter does not underflow.

Verified in 14.99 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 19.25 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 14.14 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 18.88 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.

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 9.31 s.

fifo_bram5

Author: Tomas Kratochvila, 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).

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 signal. 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."

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, and LSTBLK. 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 2<=ITEMS<=128 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 57 and BLOCK_SIZE was defined as 13. And according the fifo_bram.vhd the BRAM_TYPE was defined as 18 and DATA_WIDTH was defined as 36.

This version changes only the ITEMS, BLOCK_SIZE, BRAM_TYPE and DATA_WIDTH initial values.

VHDL source list from CVS: liberouter/vhdl_design/units/common/fifo_bram/ (date: 2005-03-21 15:00)

fifo_bram.vhd (vhdl)

Preconditions

fair_clock: G F (clock) The clock signal will be never set to 0 forever.

fair_non_clock: G F (~clock) The clock signal will be never set to 1 forever.

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 16.42 s.

Strong_read

      AG( ! ( counter = -1 ))
The counter does not underflow.

Verified in 14.99 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 19.25 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 14.14 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 18.88 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.

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 9.31 s.