• Asynchronous FIFO -- small model
• Asynchronous FIFO -- full model

Asynchronous FIFO -- small model

Author: Vojtech Rehak
The model is a smaller version (5bit long address, i.e. 31 items) of the asynchronous fifo fifoctlr_ic_v2.vhd originated form the XAPP258 Xilinx application note.

VHDL source list from CVS: liberouter/ver/models/async_fifo/ (date: 2004-05-06)

fifo5/fifo5.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=MAX ))
        

The counter does not overflow.

Preconditions:
long_gsr

Verified in 55.81 s (system 0.22 s) .

Strong_read

      G( ! ( counter=MIN ))
        

The counter does not underflow.

Preconditions:
long_gsr

Verified in 55.66 s (system 0.24 s) .

Strong_write_false

      G( ! ( counter=MAX ))
        

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 114.61 s (system 0.27 s) .

Strong_read_false

      G( ! ( counter=MIN ))
        

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.90 s (system 0.01 s) .

Weak_write_false

      G( (counter <= (MAX-2)) & 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 107.46 s (system 0.61 s) .

Weak_write_more_than_one

      G( (counter < (MAX-2)) & 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 98.64 s (system 0.48 s) .

Weak_write_just_one

      G( (
            (counter = (MAX-2)) & 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 299.26 s (system 0.89 s) .

Weak_read_false

      G( (counter >= (MIN+2)) & 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 75.29 s (system 0.35 s) .

Weak_read_more_than_one

      G( (counter > (MIN+2)) & 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 70.79 s (system 0.36 s) .

Weak_read_just_one

      G( (
            (counter = (MIN+2)) & 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 141.25 s (system 0.42 s) .

Asynchronous FIFO -- full model

Author: Vojtech Rehak
The model is a little bit modified version (some parts are in comments) of the asynchronous fifo fifoctlr_ic_v2.vhd originated form the XAPP258 Xilinx application note.

VHDL source list from CVS: liberouter/ver/models/async_fifo/ (date: 2004-05-06)

full_version/fifoctlr_ic_v2.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=MAX ))
        

The counter does not overflow.

Preconditions:
long_gsr

Verified in (unfinished) .

Strong_read

      G( ! ( counter=MIN ))
        

The counter does not underflow.

Preconditions:
long_gsr

Verified in (unfinished) .

Strong_write_false

      G( ! ( counter=MAX ))
        

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 (unfinished) .

Strong_read_false

      G( ! ( counter=MIN ))
        

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 266.06 s (system 0.91 s) .

Weak_write_false

      G( (counter <= (MAX-2)) & 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 (unfinished) .

Weak_write_more_than_one

      G( (counter < (MAX-2)) & 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 (unfinished) .

Weak_write_just_one

      G( (
            (counter = (MAX-2)) & 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 (unfinished) .

Weak_read_false

      G( (counter >= (MIN+2)) & 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 (unfinished) .

Weak_read_more_than_one

      G( (counter > (MIN+2)) & 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 (unfinished) .

Weak_read_just_one

      G( (
            (counter = (MIN+2)) & 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 (unfinished) .