tx_buff

Author: Pavel Simecek

This is a verification of TX_BUFFER and its subcomponents. Behavior of tx_fsm is abstacted to arbitrary outputs.

There is one more verification "2005-05-05 15:00" including more formulas and verification with tx_fsm.

VHDL source list from CVS: liberouter/vhdl_design/projects/liberouter/comp/tx_buffer/ (date: 2005-05-05 10:00)

projects/liberouter/comp/tx_buffer/comp/tx_databuf.vhd (vhdl)
projects/liberouter/comp/tx_buffer/comp/hwbuff_fsm.vhd (vhdl)
projects/liberouter/comp/tx_buffer/comp/tx_arbiter.vhd (vhdl)
projects/liberouter/comp/tx_buffer/tx_buff.vhd (vhdl)
units/common/pkg/math_pack.vhd (vhdl)
projects/nic_card/comp/ni/crc.vhd (vhdl)
projects/nic_card/comp/ni/tx_buffer.vhd (vhdl)
projects/nic_card/comp/ni/reg_flags_4.vhd (vhdl)
projects/nic_card/comp/ni/reg_len_arr.vhd (vhdl)
projects/nic_card/comp/ni/tx_fsm.vhd (vhdl)

Preconditions

pre_reset: RESET & (X G ! RESET); Reset is only is the first state of the run.

pre_txd_clk: (G F TXD_CLK) & (G F !TXD_CLK) Infinitely-times TXD_CLK is one and infinitely-times TXD_CLK is zero.

pre_data_valid_clk: G (((X TXD_CLK) -> TXD_CLK)->((hw_tx_dv<->X hw_tx_dv))) hw_tx_dv is synchronized with TXD_CLK.

pre_data_valid_at_least_two_ticks: G (((~hw_tx_dv) & X hw_tx_dv) -> X ( hw_tx_dv U (((~TXD_CLK) & hw_tx_dv) & X (TXD_CLK & hw_tx_dv) ) ) ) hw_tx_dv=1 for at least 2 ticks of TXD_CLK

pre_data_valid_at_least_three_ticks: G (((~hw_tx_dv) & X hw_tx_dv) -> X ( hw_tx_dv U (((~TXD_CLK) & hw_tx_dv) & X (TXD_CLK & hw_tx_dv & (hw_tx_dv U (((~TXD_CLK) & hw_tx_dv) & X (TXD_CLK & hw_tx_dv) ) ) ) ) ) ) hw_tx_dv=1 for at least 3 ticks of TXD_CLK

pre_not_data_valid_at_least_three_ticks: G ((hw_tx_dv & X (~hw_tx_dv)) -> X ( (~hw_tx_dv) U (((~TXD_CLK) & (~hw_tx_dv)) & X (TXD_CLK & (~hw_tx_dv) & ((~hw_tx_dv) U (((~TXD_CLK) & (~hw_tx_dv)) & X (TXD_CLK & (~hw_tx_dv)) ) ) ) ) ) ) hw_tx_dv=0 for at least 3 ticks of TXD_CLK

pre_not_data_valid_at_least_four_ticks: G ((hw_tx_dv & X (~hw_tx_dv)) -> X ( (~hw_tx_dv) U (((~TXD_CLK) & (~hw_tx_dv)) & X (TXD_CLK & (~hw_tx_dv) & ((~hw_tx_dv) U (((~TXD_CLK) & (~hw_tx_dv)) & X (TXD_CLK & (~hw_tx_dv) & ((~hw_tx_dv) U (((~TXD_CLK) & (~hw_tx_dv)) & X (TXD_CLK & (~hw_tx_dv))) ) ) ) ) ) ) ) ) hw_tx_dv=0 for at least 4 ticks of TXD_CLK

pre_TX_CLK_at_least_as_fast_as_TXD_CLK: G ( ((~TXD_CLK) & X TXD_CLK) -> X ( (!((~TXD_CLK) & X TXD_CLK)) U ((~TX_CLK) & X TX_CLK) ) ); TX_CLK has a frequency same as or higher than TXD_CLK

pre_TXD_CLK_at_least_as_fast_as_TX_CLK: G ( ((~TX_CLK) & X TX_CLK) -> X ( (!((~TX_CLK) & X TX_CLK)) U ((~TXD_CLK) & X TXD_CLK) ) ); TXD_CLK has a frequency same as or higher than TX_CLK

Formulas

lemma_FULL_implies_not_WEN

        G (~RESET -> ((HW_TX_BUFFERS.STATUS[3] & HW_TX_BUFFERS.STATUS[2] &
                HW_TX_BUFFERS.STATUS[1] & HW_TX_BUFFERS.STATUS[0])->
                (~ HWBUFF_CONTROL.WEN ) ))

If the buffer is full, write cannot be enabled at the same time.

Preconditions:
pre_reset, pre_data_valid_clk, pre_not_data_valid_at_least_four_ticks, pre_TX_CLK_at_least_as_fast_as_TXD_CLK

Important note: The formula is not valid, if the precondition pre_not_data_valid_at_least_four_ticks is substituted for example by pre_not_data_valid_at_least_three_ticks - THUS THE LIMIT OF AT LEAST 4 TICKS IS CRUICIAL

Verified in up to 2 hours.

lemma_exclusive_FULL_and_DV

        G (~RESET -> ~(HW_TX_BUFFERS.STATUS[3] & HW_TX_BUFFERS.STATUS[2] &
                HW_TX_BUFFERS.STATUS[1] & HW_TX_BUFFERS.STATUS[0] &
                HW_TX_BUFFERS.D_VAL_IN))

If the buffer cannot be full at the same time as HW_TX_BUFFERS.D_VAL_IN=1

Preconditions:
pre_reset, pre_data_valid_clk, pre_not_data_valid_at_least_four_ticks, pre_TX_CLK_at_least_as_fast_as_TXD_CLK

Verified in up to 2 hours.

tx_buff

Author: Pavel Simecek

This is a verification of TX_BUFFER and its subcomponents.

There is one more verification "2005-05-05 10:00" including more formulas and abstracted tx_fsm.

VHDL source list from CVS: liberouter/vhdl_design/projects/liberouter/comp/tx_buffer/ (date: 2005-05-05 15:00)

Preconditions

pre_reset: RESET & (X G ! RESET); Reset is only is the first state of the run.

Formulas

lemma_STATUS_0_stays_1_until_hwbuff_freebuf

        G ( ((~HW_TX_BUFFERS.STATUS[0]) & X HW_TX_BUFFERS.STATUS[0]) ->
            X ( ( HW_TX_BUFFERS.STATUS[0] U hwbuff_free_buff) |
                ( G HW_TX_BUFFERS.STATUS[0]) )
          )

If STATUS[0] is set to 1, then it stays being one until hwbuff_free_buff=1.

Preconditions:
pre_reset

Verified in approx. 46 hours .

lemma_STATUS_1_stays_1_until_hwbuff_freebuf

        G ( ((~HW_TX_BUFFERS.STATUS[1]) & X HW_TX_BUFFERS.STATUS[1]) ->
            X ( ( HW_TX_BUFFERS.STATUS[1] U hwbuff_free_buff) |
                ( G HW_TX_BUFFERS.STATUS[1]) )
          )

If STATUS[1] is set to 1, then it stays being one until hwbuff_free_buff=1.

Preconditions:
pre_reset

Verified in approx. 46 hours .

lemma_STATUS_2_stays_1_until_hwbuff_freebuf

        G ( ((~HW_TX_BUFFERS.STATUS[2]) & X HW_TX_BUFFERS.STATUS[2]) ->
            X ( ( HW_TX_BUFFERS.STATUS[2] U hwbuff_free_buff) |
                ( G HW_TX_BUFFERS.STATUS[2]) )
          )

If STATUS[2] is set to 1, then it stays being one until hwbuff_free_buff=1.

Preconditions:
pre_reset

Verified in approx. 46 hours .

lemma_STATUS_3_stays_1_until_hwbuff_freebuf

        G ( ((~HW_TX_BUFFERS.STATUS[3]) & X HW_TX_BUFFERS.STATUS[3]) ->
            X ( ( HW_TX_BUFFERS.STATUS[3] U hwbuff_free_buff) |
                ( G HW_TX_BUFFERS.STATUS[3]) )
          )

If STATUS[3] is set to 1, then it stays being one until hwbuff_free_buff=1.

Preconditions:
pre_reset

Verified in approx. 46 hours .