uh_fifo

Author: Pavel Simecek

VHDL source list from CVS: liberouter/vhdl_design/units/uh_fifo/ (date: 2004-02-22 01:00)

uh_fifo.vhd (vhdl)

Preconditions

pre1: G (HFE_RDY -> F ~HFE_REQ) After enabling of HFE_READY, HFE_REQ will be disabled

pre3: G (LUP_SR_VALID -> F LUP_SR_CLEAN ) There comes LUP_SR_CLEAN=1 after LUP_SR_VALID=1

pre4: G F (HFE_REQ) HFE_REQ=1 infinitely-times

pre5: RESET & X G (~RESET) There is reset in the first cycle and then there is not.

pre6: G ( (F HFE_CLK) & (F ~ HFE_CLK) ) HFE_CLK=1 infinitely-times and also HFE_CLK=0 infinitely-times

pre7: G ( (F LUP_CLK) & (F ~ LUP_CLK) ) LUP_CLK=1 infinitely-times and also LUP_CLK=0 infinitely-times

pre8: G F (LUP_SR_CLEAN) LUP_SR_CLEAN=1 infinitely-times

pre_change_then_clean: G ( ( (LUP_ADDR[5] ^ (X LUP_ADDR[5])) | (LUP_ADDR[6] ^ (X LUP_ADDR[6])) | (LUP_ADDR[7] ^ (X LUP_ADDR[7])) | (LUP_ADDR[8] ^ (X LUP_ADDR[8])) ) -> ( (X ~LUP_SR_CLEAN) & X ( (~( (LUP_ADDR[5] ^ (X LUP_ADDR[5])) | (LUP_ADDR[6] ^ (X LUP_ADDR[6])) | (LUP_ADDR[7] ^ (X LUP_ADDR[7])) | (LUP_ADDR[8] ^ (X LUP_ADDR[8])) )) U LUP_SR_CLEAN ) ) ) After change of LUP_ADDR there is no further change of LUP_ADDR until LUP_SR_CLEAN=1.

pre_always_sometimes_change: G F ( (LUP_ADDR[5] ^ (X LUP_ADDR[5])) | (LUP_ADDR[6] ^ (X LUP_ADDR[6])) | (LUP_ADDR[7] ^ (X LUP_ADDR[7])) | (LUP_ADDR[8] ^ (X LUP_ADDR[8])) ) LUP_ADDR[8..5] is not constant.

pre9: (LUP_ADDR[8..5]=0) LUP_ADDR[8..5] is initialized to zero.

pre10: ((hfe_block_0_=0)&(hfe_block_1_=0)&(hfe_block_2_=0)&(hfe_block_3_=0)) hfe_block is initialized to zero.

pre_inc_1: G ((LUP_ADDR[8..5]=0) -> X( (LUP_ADDR[8..5]=0) | (LUP_ADDR[8..5]=1) ) ) Together with pre_inc_[1-9][ 0-6] says, that LUP_ADDR[8..5] can only be the same or it can increase.

pre_inc_2: G ((LUP_ADDR[8..5])=1 -> X( (LUP_ADDR[8..5]=1) | (LUP_ADDR[8..5]=2) ) )

pre_inc_3: G ((LUP_ADDR[8..5])=2 -> X( (LUP_ADDR[8..5]=2) | (LUP_ADDR[8..5]=3) ) )

pre_inc_4: G ((LUP_ADDR[8..5])=3 -> X( (LUP_ADDR[8..5]=3) | (LUP_ADDR[8..5]=4) ) )

pre_inc_5: G ((LUP_ADDR[8..5])=4 -> X( (LUP_ADDR[8..5]=4) | (LUP_ADDR[8..5]=5) ) )

pre_inc_6: G ((LUP_ADDR[8..5])=5 -> X( (LUP_ADDR[8..5]=5) | (LUP_ADDR[8..5]=6) ) )

pre_inc_7: G ((LUP_ADDR[8..5])=6 -> X( (LUP_ADDR[8..5]=6) | (LUP_ADDR[8..5]=7) ) )

pre_inc_8: G ((LUP_ADDR[8..5])=7 -> X( (LUP_ADDR[8..5]=7) | (LUP_ADDR[8..5]=8) ) )

pre_inc_9: G ((LUP_ADDR[8..5])=8 -> X( (LUP_ADDR[8..5]=8) | (LUP_ADDR[8..5]=9) ) )

pre_inc_10: G ((LUP_ADDR[8..5])=9 -> X( (LUP_ADDR[8..5]=9) | (LUP_ADDR[8..5]=10) ) )

pre_inc_11: G ((LUP_ADDR[8..5])=10 -> X( (LUP_ADDR[8..5]=10) | (LUP_ADDR[8..5]=11) ) )

pre_inc_12: G ((LUP_ADDR[8..5])=11 -> X( (LUP_ADDR[8..5]=11) | (LUP_ADDR[8..5]=12) ) )

pre_inc_13: G ((LUP_ADDR[8..5])=12 -> X( (LUP_ADDR[8..5]=12) | (LUP_ADDR[8..5]=13) ) )

pre_inc_14: G ((LUP_ADDR[8..5])=13 -> X( (LUP_ADDR[8..5]=13) | (LUP_ADDR[8..5]=14) ) )

pre_inc_15: G ((LUP_ADDR[8..5])=14 -> X( (LUP_ADDR[8..5]=14) | (LUP_ADDR[8..5]=15) ) )

pre_inc_16: G ((LUP_ADDR[8..5])=15 -> X( (LUP_ADDR[8..5]=15) | (LUP_ADDR[8..5]=0) ) )

pre_clk_hfe_req: G (((X HFE_CLK) -> HFE_CLK)->((HFE_REQ->X HFE_REQ)&((~HFE_REQ) -> (X ~HFE_REQ)))) HFE_REQ is synchronized with clocks of HFE.

pre_clk_lup_sr_clean: G (((X LUP_CLK) -> LUP_CLK)->((LUP_SR_CLEAN->X LUP_SR_CLEAN)&((~LUP_SR_CLEAN) -> (X ~LUP_SR_CLEAN)))) LUP_SR_CLEAN is synchronized with clocks of LUP.

Formulas

lemma1aa

  X G ((HFE_RDY & hfe_block_0_)->((hfe_block_0_ U hfe_is_producing)|(G hfe_block_0_)))

Together with all formulas lemma1[a-d][a-b] says, that hfe_block doesn't change after HFE_RDY=1 until hfe_is_producing=1

Preconditions:
pre5

lemma1ab

  X G ((HFE_RDY & ~hfe_block_0_)->(((~hfe_block_0_) U hfe_is_producing)|(G (~hfe_block_0_))))

Preconditions:
pre5

lemma1ba

  X G ((HFE_RDY & hfe_block_1_)->((hfe_block_1_ U hfe_is_producing)|(G hfe_block_1_)))

Preconditions:
pre5

lemma1bb

  X G ((HFE_RDY & ~hfe_block_1_)->(((~hfe_block_1_) U hfe_is_producing)|(G (~hfe_block_1_))))

Preconditions:
pre5

lemma1ca

  X G ((HFE_RDY & hfe_block_2_)->((hfe_block_2_ U hfe_is_producing)|(G hfe_block_2_)))

Preconditions:
pre5

lemma1cb

  X G ((HFE_RDY & ~hfe_block_2_)->(((~hfe_block_2_) U hfe_is_producing)|(G (~hfe_block_2_))))

Preconditions:
pre5

lemma1da

  X G ((HFE_RDY & hfe_block_3_)->((hfe_block_3_ U hfe_is_producing)|(G hfe_block_3_)))

Preconditions:
pre5

lemma1db

  X G ((HFE_RDY & ~hfe_block_3_)->(((~hfe_block_3_) U hfe_is_producing)|(G (~hfe_block_3_))))

Preconditions:
pre5

lemma2

  X G (HFE_RDY -> ((G ~uh_valid) | ((~X uh_valid) U hfe_is_producing )))

Says that uh_valid=0 after HFE_RDY=1 until HFE_VALID=1 (and if HFE_VALID=0 constantly then uh_valid=0 constantly too after hfe_is_producing).

Preconditions:
pre5

lemma3

  G F HFE_RDY

HFE_RDY=1 infinitely-times.

Preconditions:
pre1, pre3, pre4, pre5, pre6, pre7, pre8, pre9, pre10, pre_clk_hfe_req, pre_clk_lup_sr_clean, pre_inc_1, pre_inc_2, pre_inc_3, pre_inc_4, pre_inc_5, pre_inc_6, pre_inc_7, pre_inc_8, pre_inc_9, pre_inc_10, pre_inc_11, pre_inc_12, pre_inc_13, pre_inc_14, pre_inc_15, pre_inc_16, pre_clk_lup_addr_5, pre_clk_lup_addr_6, pre_clk_lup_addr_7, pre_clk_lup_addr_8, pre_change_then_clean, pre_always_sometimes_change

lemma4

  G F hfe_is_producing

hfe_is_producing=1 infinitely-times.

lemma5_0

  ~(F G ready_0_)

This formula says that 0th bit of register ready is not constantly 1. Together with formulas lemma[5-6]_[0-9][ 0-5] says that register ready is alive.

lemma5_1

  ~(F G ready_1_)

1th bit of register ready is not constantly 1

lemma5_2

  ~(F G ready_2_)

2th bit of register ready is not constantly 1

lemma5_3

  ~(F G ready_3_)

3th bit of register ready is not constantly 1

lemma5_4

  ~(F G ready_4_)

4th bit of register ready is not constantly 1

lemma5_5

  ~(F G ready_5_)

5th bit of register ready is not constantly 1

lemma5_6

  ~(F G ready_6_)

6th bit of register ready is not constantly 1

lemma5_7

  ~(F G ready_7_)

7th bit of register ready is not constantly 1

lemma5_8

  ~(F G ready_8_)

8th bit of register ready is not constantly 1

lemma5_9

  ~(F G ready_9_)

9th bit of register ready is not constantly 1

lemma5_10

  ~(F G ready_10_)

10th bit of register ready is not constantly 1

lemma5_11

  ~(F G ready_11_)

11th bit of register ready is not constantly 1

lemma5_12

  ~(F G ready_12_)

12th bit of register ready is not constantly 1

lemma5_13

  ~(F G ready_13_)

13th bit of register ready is not constantly 1

lemma5_14

  ~(F G ready_14_)

14th bit of register ready is not constantly 1

lemma5_15

  ~(F G ready_15_)

15th bit of register ready is not constantly 1

lemma6_0

  ~(F G ~ready_0_)

0th bit of register ready is not constantly 0

lemma6_1

  ~(F G ~ready_1_)

1th bit of register ready is not constantly 0

lemma6_2

  ~(F G ~ready_2_)

2th bit of register ready is not constantly 0

lemma6_3

  ~(F G ~ready_3_)

3th bit of register ready is not constantly 0

lemma6_4

  ~(F G ~ready_4_)

4th bit of register ready is not constantly 0

lemma6_5

  ~(F G ~ready_5_)

5th bit of register ready is not constantly 0

lemma6_6

  ~(F G ~ready_6_)

6th bit of register ready is not constantly 0

lemma6_7

  ~(F G ~ready_7_)

7th bit of register ready is not constantly 0

lemma6_8

  ~(F G ~ready_8_)

8th bit of register ready is not constantly 0

lemma6_9

  ~(F G ~ready_9_)

9th bit of register ready is not constantly 0

lemma6_10

  ~(F G ~ready_10_)

10th bit of register ready is not constantly 0

lemma6_11

  ~(F G ~ready_11_)

11th bit of register ready is not constantly 0

lemma6_12

  ~(F G ~ready_12_)

12th bit of register ready is not constantly 0

lemma6_13

  ~(F G ~ready_13_)

13th bit of register ready is not constantly 0

lemma6_14

  ~(F G ~ready_14_)

14th bit of register ready is not constantly 0

lemma6_15

  ~(F G ~ready_15_)

15th bit of register ready is not constantly 0

lemma7

  G ((ready_0_&(LUP_ADDR[8..5]=0)) -> (hfe_block_0_ | hfe_block_1_ | hfe_block_2_ | hfe_block_3_ | ~(HFE_WEN & hfe_allocated)))

The original assertion was: " globally if (ready(conv_integer(unsigned(lup_block)))) then ((hfe_block != lup_block) or (not write_i))". This is an instance of this assertion for lup_block=0.

lemma8

  G ((ready_0_&(LUP_ADDR[8..5]=0)) -> (hfe_block_0_ | hfe_block_1_ | hfe_block_2_ | ~(HFE_WEN & hfe_allocated)))

This is the same formula as lemma7, but hfe_block_3_ is omitted.

uh_fifo

Author: Pavel Simecek

VHDL source list from CVS: liberouter/vhdl_design/units/uh_fifo/ (date: 2004-04-18 01:00)

uh_fifo.vhd (vhdl)
../common/dp_regflags/dp_regflags.vhd (vhdl)

Preconditions

pre1: G (HFE_RDY -> F ~HFE_REQ) After enabling of HFE_READY, HFE_REQ will be disabled

pre_lup_sr_valid_comes_first: ((~LUP_SR_CLEAN) U LUP_SR_VALID) It begins with LUP_SR_VALID

pre_lup_sr_valid_precedes_clean: G ( LUP_SR_CLEAN -> X ((~LUP_SR_CLEAN) U LUP_SR_VALID) ) LUP_SR_CLEAN alters with LUP_SR_VALID

pre3: G (LUP_SR_VALID -> F LUP_SR_CLEAN ) There comes LUP_SR_CLEAN=1 after LUP_SR_VALID=1

pre4: G F (HFE_REQ) HFE_REQ=1 infinitely-times

pre5: RESET & X G (~RESET) There is reset in the first cycle and then there is not.

pre6: G ( (F HFE_CLK) & (F ~ HFE_CLK) ) HFE_CLK=1 infinitely-times and also HFE_CLK=0 infinitely-times

pre7: G ( (F LUP_CLK) & (F ~ LUP_CLK) ) LUP_CLK=1 infinitely-times and also LUP_CLK=0 infinitely-times

pre8: G F (LUP_SR_CLEAN) LUP_SR_CLEAN=1 infinitely-times

pre_change_then_clean: G ( ( (LUP_ADDR[5] ^ (X LUP_ADDR[5])) | (LUP_ADDR[6] ^ (X LUP_ADDR[6])) | (LUP_ADDR[7] ^ (X LUP_ADDR[7])) | (LUP_ADDR[8] ^ (X LUP_ADDR[8])) ) -> ( (X ~LUP_SR_CLEAN) & X ( (~( (LUP_ADDR[5] ^ (X LUP_ADDR[5])) | (LUP_ADDR[6] ^ (X LUP_ADDR[6])) | (LUP_ADDR[7] ^ (X LUP_ADDR[7])) | (LUP_ADDR[8] ^ (X LUP_ADDR[8])) )) U LUP_SR_CLEAN ) ) ) After change of LUP_ADDR there is no further change of LUP_ADDR until LUP_SR_CLEAN=1.

pre_always_sometimes_change: G F ( (LUP_ADDR[7] ^ (X LUP_ADDR[7])) | (LUP_ADDR[8] ^ (X LUP_ADDR[8])) ) LUP_ADDR[8..7] is not constant.

pre9: (LUP_ADDR[8..7]=0) LUP_ADDR[8..7] is initialized to zero.

pre10: ((hfe_block_0_=0)&(hfe_block_1_=0)) hfe_block is initialized to zero.

pre_inc_1: G ((LUP_ADDR[8..7]=0) -> X( (LUP_ADDR[8..7]=0) | (LUP_ADDR[8..7]=1) ) ) Together with pre_inc_[1-9][ 0-6] says, that LUP_ADDR[8..7] can only be the same or it can increase.

pre_inc_2: G ((LUP_ADDR[8..7])=1 -> X( (LUP_ADDR[8..7]=1) | (LUP_ADDR[8..7]=2) ) )

pre_inc_3: G ((LUP_ADDR[8..7])=2 -> X( (LUP_ADDR[8..7]=2) | (LUP_ADDR[8..7]=3) ) )

pre_inc_4: G ((LUP_ADDR[8..7])=3 -> X( (LUP_ADDR[8..7]=3) | (LUP_ADDR[8..7]=0) ) )

pre_clk_hfe_req: G (((X HFE_CLK) -> HFE_CLK)->((HFE_REQ->X HFE_REQ)&((~HFE_REQ) -> (X ~HFE_REQ)))) HFE_REQ is synchronized with clocks of HFE.

pre_clk_lup_sr_clean: G (((X LUP_CLK) -> LUP_CLK)->((LUP_SR_CLEAN->X LUP_SR_CLEAN)&((~LUP_SR_CLEAN) -> (X ~LUP_SR_CLEAN)))) LUP_SR_CLEAN is synchronized with clocks of LUP.

Formulas

lemma1aa

  X G ((HFE_RDY & hfe_block_0_)->((hfe_block_0_ U hfe_is_producing)|(G hfe_block_0_)))

Together with all formulas lemma1[a-b][a-b] says, that hfe_block doesn't change after HFE_RDY=1 until hfe_is_producing=1

Preconditions:
pre5

lemma1ab

  X G ((HFE_RDY & ~hfe_block_0_)->(((~hfe_block_0_) U hfe_is_producing)|(G (~hfe_block_0_))))

Preconditions:
pre5

lemma1ba

  X G ((HFE_RDY & hfe_block_1_)->((hfe_block_1_ U hfe_is_producing)|(G hfe_block_1_)))

Preconditions:
pre5

lemma1bb

  X G ((HFE_RDY & ~hfe_block_1_)->(((~hfe_block_1_) U hfe_is_producing)|(G (~hfe_block_1_))))

Preconditions:
pre5

lemma2

  X G (HFE_RDY -> ((G ~uh_valid) | ((~X uh_valid) U hfe_is_producing )))

Says that uh_valid=0 after HFE_RDY=1 until HFE_VALID=1 (and if HFE_VALID=0 constantly then uh_valid=0 constantly too after hfe_is_producing).

Preconditions:
pre5

lemma3

  G F HFE_RDY

HFE_RDY=1 infinitely-times.

Preconditions:
pre1, pre3, pre4, pre5, pre6, pre7, pre8, pre9, pre10, pre_clk_hfe_req, pre_clk_lup_sr_clean, pre_inc_1, pre_inc_2, pre_inc_3, pre_inc_4, pre_clk_lup_addr_5, pre_clk_lup_addr_6, pre_clk_lup_addr_7, pre_clk_lup_addr_8, pre_change_then_clean, pre_always_sometimes_change

lemma4

  G F hfe_is_producing

hfe_is_producing=1 infinitely-times.

lemma5_0

  ~(F G ready_0_)

This formula says that 0th bit of register ready is not constantly 1. Together with formulas lemma[5-6]_[0-3] says that register ready is alive.

lemma5_1

  ~(F G ready_1_)

1th bit of register ready is not constantly 1

lemma5_2

  ~(F G ready_2_)

2th bit of register ready is not constantly 1

lemma5_3

  ~(F G ready_3_)

3th bit of register ready is not constantly 1

lemma6_0

  ~(F G ~ready_0_)

0th bit of register ready is not constantly 0

lemma6_1

  ~(F G ~ready_1_)

1th bit of register ready is not constantly 0

lemma6_2

  ~(F G ~ready_2_)

2th bit of register ready is not constantly 0

lemma6_3

  ~(F G ~ready_3_)

3th bit of register ready is not constantly 0

lemma7

  G ((ready_0_&(LUP_ADDR[8..7]=0)) -> (hfe_block_0_ | hfe_block_1_ | ~(HFE_WEN & hfe_allocated)))

The original assertion was: " globally if (ready(conv_integer(unsigned(lup_block)))) then ((hfe_block != lup_block) or (not write_i))". This is an instance of this assertion for lup_block=0.

lemma8

  G ((ready_0_&(LUP_ADDR[8..7]=0)) -> (hfe_block_0_ | ~(HFE_WEN & hfe_allocated)))

This is the same formula as lemma7, but hfe_block_3_ is omitted.

uh_fifo

Author: Pavel Simecek

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

uh_fifo/ver/2004-12-26_22_00/uh_fifo.vhd (vhdl)
common/dp_regflags/dp_regflags.vhd (vhdl)

Preconditions

Formulas

lemma1aa

  X G ((HFE_RDY & hfe_block_0_)->((hfe_block_0_ U hfe_is_producing)|(G hfe_block_0_)))

Together with all formulas lemma1[a-b][a-b] says, that hfe_block doesn't change after HFE_RDY=1 until hfe_is_producing=1

Preconditions:
pre5

lemma1ab

  X G ((HFE_RDY & ~hfe_block_0_)->(((~hfe_block_0_) U hfe_is_producing)|(G (~hfe_block_0_))))

Preconditions:
pre5

lemma1ba

  X G ((HFE_RDY & hfe_block_1_)->((hfe_block_1_ U hfe_is_producing)|(G hfe_block_1_)))

Preconditions:
pre5

lemma1bb

  X G ((HFE_RDY & ~hfe_block_1_)->(((~hfe_block_1_) U hfe_is_producing)|(G (~hfe_block_1_))))

Preconditions:
pre5

lemma2

  X G (HFE_RDY -> ((G ~uh_valid) | ((~X uh_valid) U hfe_is_producing )))

Says that uh_valid=0 after HFE_RDY=1 until HFE_VALID=1 (and if HFE_VALID=0 constantly then uh_valid=0 constantly too after hfe_is_producing).

Preconditions:
pre5

lemma3

  G F HFE_RDY

HFE_RDY=1 infinitely-times.

lemma4

  G F hfe_is_producing

hfe_is_producing=1 infinitely-times.

lemma5_0

  ~(F G ready_0_)

This formula says that 0th bit of register ready is not constantly 1. Together with formulas lemma[5-6]_[0-3] says that register ready is alive.

lemma5_1

  ~(F G ready_1_)

1th bit of register ready is not constantly 1

lemma5_2

  ~(F G ready_2_)

2th bit of register ready is not constantly 1

lemma5_3

  ~(F G ready_3_)

3th bit of register ready is not constantly 1

lemma6_0

  ~(F G ~ready_0_)

0th bit of register ready is not constantly 0

lemma6_1

  ~(F G ~ready_1_)

1th bit of register ready is not constantly 0

lemma6_2

  ~(F G ~ready_2_)

2th bit of register ready is not constantly 0

lemma6_3

  ~(F G ~ready_3_)

3th bit of register ready is not constantly 0

lemma7

  G ((ready_0_&(LUP_ADDR[8..7]=0)) -> (hfe_block_0_ | hfe_block_1_ | ~(HFE_WEN & hfe_allocated)))

The original assertion was: " globally if (ready(conv_integer(unsigned(lup_block)))) then ((hfe_block != lup_block) or (not write_i))". This is an instance of this assertion for lup_block=0.

lemma8

  G ((ready_0_&(LUP_ADDR[8..7]=0)) -> (hfe_block_0_ | ~(HFE_WEN & hfe_allocated)))

This is the same formula as lemma7, but hfe_block_3_ is omitted.