asfifo_bram
Author: Vojtech RehakSpecification 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.
Write operation, EMPTY and FULL signals have the same behavioral as in the standard asynchronous fifo component. Such behaviour is very well described the XAPP258 Xilinx application note concerning an asynchronous fifo fifoctlr_ic_v2. During the Read operation the output data are delayed. This delay is caused by registered BRAM memory. 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.
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 and FULL. 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 three parameters ITEMS, DATA_WIDTH, and BRAM_TYPE. The verification was performed only for the following parameter settings:
ITEMS = 15
BRAM_TYPE = 9
DATA_WIDTH = 18
The reason for this is that we realised that synthesis does not work for ITEMS = 512, BRAM_TYPE = 36, and DATA_WIDTH = 72.
The next version is repaird.VHDL source list from CVS: liberouter/vhdl_design/units/common/asfifo_bram/ (date: 2005-04-14 15:00)
asfifo_bram.vhd (vhdl)
Preconditions
long_gsr: (X gsr) & ( G ((~gsr & X gsr)-> X X gsr )) Each gsr reset is at least two states long.fair_non_gsr: G F (~gsr) The gsr reset signal will be never activated forever.
fair_reader_clk: G F (reader_clk) The reader_clk clock signal will be never set to 0 forever.
fair_non_reader_clk: G F (~reader_clk) The reader_clk clock signal will be never set to 1 forever.
fair_writer_clk: G F (writer_clk) The writer_clk clock signal will be never set to 0 forever.
fair_non_writer_clk: G F (~writer_clk) The writer_clk clock signal will be never set to 1 forever.
Formulas
Strong_write
G( ! ( counter=ITEMS+1 ))
The counter does not overflow.
Preconditions:
long_gsr
Verified in 3.91 s.
Strong_read
G( ! ( counter=-1 ))
The counter does not underflow.
Preconditions:
long_gsr
Verified in 3.86 s.
Reach_full
AG EF ( counter = ITEMS )
The fifo is sometimes full.
Preconditions:
long_gsr
Verified in 9.29 s.
Reach_empty
AG EF ( counter = 0 )
The fifo is sometimes empty.
Preconditions:
long_gsr
Verified in 4.78 s.
Strong_write_false
G( ! ( counter=ITEMS+1 ))
It shows that long_gsr precondition is necessary.
Counterexample:
\fifo_gsr_in is 1 only in the first state and clk has a posedge
between the first and the second state.
Differences from the original design code:
The long_gsr precondition is omitted.
Verified in 2.2 s.
Strong_read_false
G( ! ( counter=-1 ))
It shows that long_gsr precondition is necessary.
Counterexample:
\fifo_gsr_in is 1 only in the first state and clk has a posedge
between the first and the second state.
Differences from the original design code:
The long_gsr precondition is omitted.
Verified in 0.21 s.
Weak_write_false
G( (counter <= (ITEMS-1)) & full & ~writer_clk & X writer_clk
-> X ( gsr | X (~full | gsr)))
If the fifo is not full, the full signal is set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_writer_clk, fair_non_writer_clk
Verified in 7.98 s.
Weak_write_more_than_one
G( (counter < (ITEMS-1)) & full & ~writer_clk & X writer_clk
-> X ( gsr | X (~full | gsr)))
If there are more than only one free item, the full signal is
set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_writer_clk, fair_non_writer_clk
Verified in 6.02 s.
Weak_write_just_one
G( (
(counter = (ITEMS-1)) & full & ~writer_clk & ( X writer_clk )
)
->
( X ( ( X ~full )
| ( writer_clk U
( (~writer_clk) U
( writer_clk U ( ~full | gsr ) )
)
)
)
)
)
If there is just one free item, the full signal is set to 0 by
at least the next one write_clk posedge.
Preconditions:
long_gsr, fair_non_gsr, fair_writer_clk, fair_non_writer_clk
Verified in 21.81 s.
Weak_read_false
G( (counter >= 1) & empty & ~reader_clk & X reader_clk
-> X ( gsr | X (~empty | gsr)))
If the fifo is not empty, the empty signal is set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_reader_clk, fair_non_reader_clk
Verified in 9.09 s.
Weak_read_more_than_one
G( (counter > 1) & empty & ~reader_clk & X reader_clk
-> X ( gsr | X (~empty | gsr)))
If there are more than only one item to read, the empty signal is
set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_reader_clk, fair_non_reader_clk
Verified in 8.09 s.
Weak_read_just_one
G( (
(counter = 1) & empty & ~reader_clk & ( X reader_clk )
)
->
( X ( ( X ~empty )
| ( reader_clk U
( (~reader_clk) U
( reader_clk U ( ~empty | gsr ) )
)
)
)
)
)
If there is just one item to read, the empty signal is set to 0
by at least the next one read_clk posedge.
Preconditions:
long_gsr, fair_non_gsr, fair_reader_clk, fair_non_reader_clk
Verified in 26.73 s.
asfifo_bram
Author: Vojtech RehakSpecification 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.
Write operation, EMPTY and FULL signals have the same behavioral as in the standard asynchronous fifo component. Such behaviour is very well described the XAPP258 Xilinx application note concerning an asynchronous fifo fifoctlr_ic_v2. During the Read operation the output data are delayed. This delay is caused by registered BRAM memory. 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.
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 and FULL. 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 three parameters ITEMS, DATA_WIDTH, and BRAM_TYPE. The verification was performed for the parameter ITEMS = 15 and all possible (correct values) of BRAM_TYPE and DATA_WIDTH according to the specification. Afther that both values BRAM_TYPE and DATA_WIDTH were fixed to 1 and ITEMS was set to all values from 1 to 33. This verification has shown that the design is correct only for the values of ITEMS = (2^n)-1, where n>=2, for the other cases the design was wrong.
The vhdl designers were asked to add this very important notice into the vhdl code, or fix the bug.
The described durations are for the paremeters ITEMS = 15, BRAM_TYPE = 9, and DATA_WIDTH = 18.
VHDL source list from CVS: liberouter/vhdl_design/units/common/asfifo_bram/ (date: 2005-04-29 15:00)
asfifo_bram.vhd (vhdl)
Preconditions
long_gsr: (X gsr) & ( G ((~gsr & X gsr)-> X X gsr )) Each gsr reset is at least two states long.fair_non_gsr: G F (~gsr) The gsr reset signal will be never activated forever.
fair_reader_clk: G F (reader_clk) The reader_clk clock signal will be never set to 0 forever.
fair_non_reader_clk: G F (~reader_clk) The reader_clk clock signal will be never set to 1 forever.
fair_writer_clk: G F (writer_clk) The writer_clk clock signal will be never set to 0 forever.
fair_non_writer_clk: G F (~writer_clk) The writer_clk clock signal will be never set to 1 forever.
Formulas
Strong_write
G( ! ( counter=ITEMS+1 ))
The counter does not overflow.
Preconditions:
long_gsr
Verified in 3.88 s.
Strong_read
G( ! ( counter=-1 ))
The counter does not underflow.
Preconditions:
long_gsr
Verified in 3.87 s.
Reach_full
AG EF ( counter = ITEMS )
The fifo is sometimes full.
Preconditions:
long_gsr
Verified in 9.29 s.
Reach_empty
AG EF ( counter = 0 )
The fifo is sometimes empty.
Preconditions:
long_gsr
Verified in 4.82 s.
Strong_write_false
G( ! ( counter=ITEMS+1 ))
It shows that long_gsr precondition is necessary.
Counterexample:
\fifo_gsr_in is 1 only in the first state and clk has a posedge
between the first and the second state.
Differences from the original design code:
The long_gsr precondition is omitted.
Verified in 2.19 s.
Strong_read_false
G( ! ( counter=-1 ))
It shows that long_gsr precondition is necessary.
Counterexample:
\fifo_gsr_in is 1 only in the first state and clk has a posedge
between the first and the second state.
Differences from the original design code:
The long_gsr precondition is omitted.
Verified in 0.21 s.
Weak_write_false
G( (counter <= (ITEMS-1)) & full & ~writer_clk & X writer_clk
-> X ( gsr | X (~full | gsr)))
If the fifo is not full, the full signal is set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_writer_clk, fair_non_writer_clk
Verified in 8 s.
Weak_write_more_than_one
G( (counter < (ITEMS-1)) & full & ~writer_clk & X writer_clk
-> X ( gsr | X (~full | gsr)))
If there are more than only one free item, the full signal is
set to 0. KRAVOVINA
Preconditions:
long_gsr, fair_non_gsr, fair_writer_clk, fair_non_writer_clk
Verified in 6.01 s.
Weak_write_just_one
G( (
(counter = (ITEMS-1)) & full & ~writer_clk & ( X writer_clk )
)
->
( X ( ( X ~full )
| ( writer_clk U
( (~writer_clk) U
( writer_clk U ( ~full | gsr ) )
)
)
)
)
)
If there is just one free item, the full signal is set to 0 by
at least the next one write_clk posedge.
Preconditions:
long_gsr, fair_non_gsr, fair_writer_clk, fair_non_writer_clk
Verified in 21.91 s.
Weak_read_false
G( (counter >= 1) & empty & ~reader_clk & X reader_clk
-> X ( gsr | X (~empty | gsr)))
If the fifo is not empty, the empty signal is set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_reader_clk, fair_non_reader_clk
Verified in 9.09 s.
Weak_read_more_than_one
G( (counter > 1) & empty & ~reader_clk & X reader_clk
-> X ( gsr | X (~empty | gsr)))
If there are more than only one item to read, the empty signal is
set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_reader_clk, fair_non_reader_clk
Verified in 8.05 s.
Weak_read_just_one
G( (
(counter = 1) & empty & ~reader_clk & ( X reader_clk )
)
->
( X ( ( X ~empty )
| ( reader_clk U
( (~reader_clk) U
( reader_clk U ( ~empty | gsr ) )
)
)
)
)
)
If there is just one item to read, the empty signal is set to 0
by at least the next one read_clk posedge.
Preconditions:
long_gsr, fair_non_gsr, fair_reader_clk, fair_non_reader_clk
Verified in 26.51 s.
asfifo_bram
Author: Vojtech RehakSpecification 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.
Write operation, EMPTY and FULL signals have the same behavioral as in the standard asynchronous fifo component. Such behaviour is very well described the XAPP258 Xilinx application note concerning an asynchronous fifo fifoctlr_ic_v2. During the Read operation the output data are delayed. This delay is caused by registered BRAM memory. 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.
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 and FULL. 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 three parameters ITEMS, DATA_WIDTH, and BRAM_TYPE. The verification was performed for the parameter ITEMS = 15 and all possible (correct values) of BRAM_TYPE and DATA_WIDTH according to the specification. Afther that both values BRAM_TYPE and DATA_WIDTH were fixed to 1 and ITEMS was set to all values from 1 to 33. This verification has shown that the design is correct only for the values of ITEMS = (2^n)-1, where n>=2, for the other cases the design was wrong.
The vhdl designers were asked to add this very important notice into the vhdl code, or fix the bug.
The described durations are for the paremeters ITEMS = 15, BRAM_TYPE = 9, and DATA_WIDTH = 18.
VHDL source list from CVS: liberouter/vhdl_design/units/common/asfifo_bram/ (date: 2005-10-19 12:00)
asfifo_bram.vhd (vhdl)
Preconditions
long_gsr: (X gsr) & ( G ((~gsr & X gsr)-> X X gsr )) Each gsr reset is at least two states long.fair_non_gsr: G F (~gsr) The gsr reset signal will be never activated forever.
fair_reader_clk: G F (reader_clk) The reader_clk clock signal will be never set to 0 forever.
fair_non_reader_clk: G F (~reader_clk) The reader_clk clock signal will be never set to 1 forever.
fair_writer_clk: G F (writer_clk) The writer_clk clock signal will be never set to 0 forever.
fair_non_writer_clk: G F (~writer_clk) The writer_clk clock signal will be never set to 1 forever.
Formulas
Strong_write
G( ! ( counter=ITEMS+1 ))
The counter does not overflow.
Preconditions:
long_gsr
Verified in 0.08 s.
Strong_read
G( ! ( counter=-1 ))
The counter does not underflow.
Preconditions:
long_gsr
Verified in 3.84 s.
Reach_full
AG EF ( counter = ITEMS )
The fifo is sometimes full.
Preconditions:
long_gsr
Verified in 9.23 s.
Reach_empty
AG EF ( counter = 0 )
The fifo is sometimes empty.
Preconditions:
long_gsr
Verified in 4.8 s.
Strong_write_false
G( ! ( counter=ITEMS+1 ))
It shows that long_gsr precondition is necessary.
Counterexample:
\fifo_gsr_in is 1 only in the first state and clk has a posedge
between the first and the second state.
Differences from the original design code:
The long_gsr precondition is omitted.
Verified in 2.2 s.
Strong_read_false
G( ! ( counter=-1 ))
It shows that long_gsr precondition is necessary.
Counterexample:
\fifo_gsr_in is 1 only in the first state and clk has a posedge
between the first and the second state.
Differences from the original design code:
The long_gsr precondition is omitted.
Verified in 0.22 s.
Weak_write_false
G( (counter <= (ITEMS-1)) & full & ~writer_clk & X writer_clk
-> X ( gsr | X (~full | gsr)))
If the fifo is not full, the full signal is set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_writer_clk, fair_non_writer_clk
Verified in 7.97 s.
Weak_write_more_than_one
G( (counter < (ITEMS-1)) & full & ~writer_clk & X writer_clk
-> X ( gsr | X (~full | gsr)))
If there are more than only one free item, the full signal is
set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_writer_clk, fair_non_writer_clk
Verified in 5.94 s.
Weak_write_just_one
G( (
(counter = (ITEMS-1)) & full & ~writer_clk & ( X writer_clk )
)
->
( X ( ( X ~full )
| ( writer_clk U
( (~writer_clk) U
( writer_clk U ( ~full | gsr ) )
)
)
)
)
)
If there is just one free item, the full signal is set to 0 by
at least the next one write_clk posedge.
Preconditions:
long_gsr, fair_non_gsr, fair_writer_clk, fair_non_writer_clk
Verified in 21.71 s.
Weak_read_false
G( (counter >= 1) & empty & ~reader_clk & X reader_clk
-> X ( gsr | X (~empty | gsr)))
If the fifo is not empty, the empty signal is set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_reader_clk, fair_non_reader_clk
Verified in 8.99 s.
Weak_read_more_than_one
G( (counter > 1) & empty & ~reader_clk & X reader_clk
-> X ( gsr | X (~empty | gsr)))
If there are more than only one item to read, the empty signal is
set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_reader_clk, fair_non_reader_clk
Verified in 8.05 s.
Weak_read_just_one
G( (
(counter = 1) & empty & ~reader_clk & ( X reader_clk )
)
->
( X ( ( X ~empty )
| ( reader_clk U
( (~reader_clk) U
( reader_clk U ( ~empty | gsr ) )
)
)
)
)
)
If there is just one item to read, the empty signal is set to 0
by at least the next one read_clk posedge.
Preconditions:
long_gsr, fair_non_gsr, fair_reader_clk, fair_non_reader_clk
Verified in 26.57 s.
asfifo_bram
Author: Vojtech RehakSpecification 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.
Write operation, EMPTY and FULL signals have the same behavioral as in the standard asynchronous fifo component. Such behaviour is very well described the XAPP258 Xilinx application note concerning an asynchronous fifo fifoctlr_ic_v2. During the Read operation the output data are delayed. This delay is caused by registered BRAM memory. 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.
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 and FULL. 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 three parameters ITEMS, DATA_WIDTH, and BRAM_TYPE. The verification was performed for the parameter ITEMS = 3, 7, 15, and 31. BRAM_TYPE was set to 0, 1, 2, 4, 9, 18, and 36 and DATA_WIDTH was set to 36.
The described durations are for the paremeters ITEMS = 15, BRAM_TYPE = 0, and DATA_WIDTH = 18.
VHDL source list from CVS: liberouter/vhdl_design/units/common/asfifo_bram/ (date: 2005-11-09 12:00)
asfifo_bram.vhd (vhdl)
Preconditions
long_gsr: (X gsr) & ( G ((~gsr & X gsr)-> X X gsr )) Each gsr reset is at least two states long.fair_non_gsr: G F (~gsr) The gsr reset signal will be never activated forever.
fair_reader_clk: G F (reader_clk) The reader_clk clock signal will be never set to 0 forever.
fair_non_reader_clk: G F (~reader_clk) The reader_clk clock signal will be never set to 1 forever.
fair_writer_clk: G F (writer_clk) The writer_clk clock signal will be never set to 0 forever.
fair_non_writer_clk: G F (~writer_clk) The writer_clk clock signal will be never set to 1 forever.
Formulas
Strong_write
G( ! ( counter=ITEMS+1 ))
The counter does not overflow.
Preconditions:
long_gsr
Verified in 0.11 s.
Strong_read
G( ! ( counter=-1 ))
The counter does not underflow.
Preconditions:
long_gsr
Verified in 0.11 s.
Reach_full
AG EF ( counter = ITEMS )
The fifo is sometimes full.
Preconditions:
long_gsr
Verified in 0.11 s.
Reach_empty
AG EF ( counter = 0 )
The fifo is sometimes empty.
Preconditions:
long_gsr
Verified in 0.11 s.
Strong_write_false
G( ! ( counter=ITEMS+1 ))
It shows that long_gsr precondition is necessary.
Counterexample:
\fifo_gsr_in is 1 only in the first state and clk has a posedge
between the first and the second state.
Differences from the original design code:
The long_gsr precondition is omitted.
Verified in 5.17 s.
Strong_read_false
G( ! ( counter=-1 ))
It shows that long_gsr precondition is necessary.
Counterexample:
\fifo_gsr_in is 1 only in the first state and clk has a posedge
between the first and the second state.
Differences from the original design code:
The long_gsr precondition is omitted.
Verified in 0.27 s.
Weak_write_false
G( (counter <= (ITEMS-1)) & full & ~writer_clk & X writer_clk
-> X ( gsr | X (~full | gsr)))
If the fifo is not full, the full signal is set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_writer_clk, fair_non_writer_clk
Verified in 9.09 s.
Weak_write_more_than_one
G( (counter < (ITEMS-1)) & full & ~writer_clk & X writer_clk
-> X ( gsr | X (~full | gsr)))
If there are more than only one free item, the full signal is
set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_writer_clk, fair_non_writer_clk
Verified in 6.72 s.
Weak_write_just_one
G( (
(counter = (ITEMS-1)) & full & ~writer_clk & ( X writer_clk )
)
->
( X ( ( X ~full )
| ( writer_clk U
( (~writer_clk) U
( writer_clk U ( ~full | gsr ) )
)
)
)
)
)
If there is just one free item, the full signal is set to 0 by
at least the next one write_clk posedge.
Preconditions:
long_gsr, fair_non_gsr, fair_writer_clk, fair_non_writer_clk
Verified in 18.61 s.
Weak_read_false
G( (counter >= 1) & empty & ~reader_clk & X reader_clk
-> X ( gsr | X (~empty | gsr)))
If the fifo is not empty, the empty signal is set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_reader_clk, fair_non_reader_clk
Verified in 9.85 s.
Weak_read_more_than_one
G( (counter > 1) & empty & ~reader_clk & X reader_clk
-> X ( gsr | X (~empty | gsr)))
If there are more than only one item to read, the empty signal is
set to 0.
Preconditions:
long_gsr, fair_non_gsr, fair_reader_clk, fair_non_reader_clk
Verified in 8.57 s.
Weak_read_just_one
G( (
(counter = 1) & empty & ~reader_clk & ( X reader_clk )
)
->
( X ( ( X ~empty )
| ( reader_clk U
( (~reader_clk) U
( reader_clk U ( ~empty | gsr ) )
)
)
)
)
)
If there is just one item to read, the empty signal is set to 0
by at least the next one read_clk posedge.
Preconditions:
long_gsr, fair_non_gsr, fair_reader_clk, fair_non_reader_clk
Verified in 29.88 s.