disp

Author: Pavel Simecek
In this verification I only proved for single bits of input vector FIFO_DO, that if the bit should be copied (according the control signals), then it finally shows on the corresponding output signal. In the beginning we made a mistake: we forgot to verify if output is also enabled by DRAM_WE signal. Now it is fixed. Verification is done separately for each bit of FIFO_DO (and DRAM_DO) and its value (0 or 1).

VHDL source list from CVS: liberouter/vhdl_design/ (date: 2004-05-25 18:00)

units/common/fifo/fifo.vhd (vhdl)
units/lb/lbconn_mem.vhd (vhdl)
projects/scampi_ph1/comp/disp/disp_fsm.vhd (vhdl)
units/lb/local_bus.vhd (vhdl)
projects/scampi_ph1/comp/disp/disp_ent.vhd (vhdl)
units/lb/local_bus.vhd (vhdl)
projects/scampi_ph1/comp/disp/disp_ent.vhd (vhdl)
projects/scampi_ph1/comp/disp/disp.vhd (vhdl)

Preconditions

pre_clk: (G F CLK) & (G F !CLK)Clock will be never blocked

pre_reset: RESET & (X G ! RESET)Reset is at he beginning and then it is not

pre_clk_fifo_do_0: G (((X CLK) -> CLK)->(FIFO_DO[0] <-> X FIFO_DO[0]))FIFO_DO[0] is synchronized with CLK

pre_clk_fifo_do_1: G (((X CLK) -> CLK)->(FIFO_DO[1] <-> X FIFO_DO[1]))FIFO_DO[1] is synchronized with CLK

pre_clk_fifo_do_2: G (((X CLK) -> CLK)->(FIFO_DO[2] <-> X FIFO_DO[2]))FIFO_DO[2] is synchronized with CLK

pre_clk_fifo_do_3: G (((X CLK) -> CLK)->(FIFO_DO[3] <-> X FIFO_DO[3]))FIFO_DO[3] is synchronized with CLK

pre_clk_fifo_do_4: G (((X CLK) -> CLK)->(FIFO_DO[4] <-> X FIFO_DO[4]))FIFO_DO[4] is synchronized with CLK

pre_clk_fifo_do_5: G (((X CLK) -> CLK)->(FIFO_DO[5] <-> X FIFO_DO[5]))FIFO_DO[5] is synchronized with CLK

pre_clk_fifo_do_6: G (((X CLK) -> CLK)->(FIFO_DO[6] <-> X FIFO_DO[6]))FIFO_DO[6] is synchronized with CLK

pre_clk_fifo_do_7: G (((X CLK) -> CLK)->(FIFO_DO[7] <-> X FIFO_DO[7]))FIFO_DO[7] is synchronized with CLK

pre_clk_fifo_do_8: G (((X CLK) -> CLK)->(FIFO_DO[8] <-> X FIFO_DO[8]))FIFO_DO[8] is synchronized with CLK

pre_clk_fifo_do_9: G (((X CLK) -> CLK)->(FIFO_DO[9] <-> X FIFO_DO[9]))FIFO_DO[9] is synchronized with CLK

pre_clk_fifo_do_10: G (((X CLK) -> CLK)->(FIFO_DO[10] <-> X FIFO_DO[10]))FIFO_DO[10] is synchronized with CLK

pre_clk_fifo_do_11: G (((X CLK) -> CLK)->(FIFO_DO[11] <-> X FIFO_DO[11]))FIFO_DO[11] is synchronized with CLK

pre_clk_fifo_do_12: G (((X CLK) -> CLK)->(FIFO_DO[12] <-> X FIFO_DO[12]))FIFO_DO[12] is synchronized with CLK

pre_clk_fifo_do_13: G (((X CLK) -> CLK)->(FIFO_DO[13] <-> X FIFO_DO[13]))FIFO_DO[13] is synchronized with CLK

pre_clk_fifo_do_14: G (((X CLK) -> CLK)->(FIFO_DO[14] <-> X FIFO_DO[14]))FIFO_DO[14] is synchronized with CLK

pre_clk_fifo_do_15: G (((X CLK) -> CLK)->(FIFO_DO[15] <-> X FIFO_DO[15]))FIFO_DO[15] is synchronized with CLK

pre_clk_fifo_do_16: G (((X CLK) -> CLK)->(FIFO_DO[16] <-> X FIFO_DO[16]))FIFO_DO[16] is synchronized with CLK

pre_clk_sau_fifo_do_0: G (((X CLK) -> CLK)->(FIFO_U.DATA_OUT[0] <-> X FIFO_U.DATA_OUT[0]))Bit 0 of FIFO_U.DATA_OUT is synchronized with CLK

pre_clk_fifo_dv: G (((X CLK) -> CLK)->(FIFO_DV <-> X FIFO_DV))FIFO_DV is synchronized with CLK

Formulas

lemma_value_1_bit_0_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[0]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[0] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[0] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[0] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[0] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_0, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_0_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[0])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[0]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[0]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[0] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[0] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_0, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_1_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[1]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[1] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[1] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[1] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[1] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_1, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_1_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[1])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[1]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[1]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[1] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[1] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_1, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_2_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[2]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[2] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[2] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[2] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[2] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_2, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_2_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[2])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[2]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[2]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[2] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[2] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_2, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_3_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[3]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[3] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[3] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[3] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[3] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_3, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_3_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[3])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[3]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[3]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[3] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[3] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_3, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_4_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[4]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[4] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[4] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[4] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[4] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_4, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_4_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[4])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[4]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[4]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[4] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[4] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_4, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_5_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[5]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[5] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[5] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[5] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[5] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_5, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_5_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[5])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[5]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[5]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[5] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[5] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_5, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_6_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[6]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[6] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[6] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[6] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[6] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_6, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_6_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[6])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[6]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[6]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[6] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[6] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_6, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_7_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[7]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[7] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[7] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[7] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[7] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_7, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_7_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[7])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[7]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[7]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[7] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[7] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_7, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_8_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[8]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[8] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[8] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[8] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[8] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_8, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_8_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[8])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[8]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[8]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[8] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[8] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_8, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_9_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[9]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[9] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[9] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[9] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[9] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_9, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_9_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[9])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[9]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[9]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[9] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[9] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_9, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_10_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[10]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[10] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[10] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[10] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[10] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_10, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_10_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[10])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[10]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[10]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[10] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[10] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_10, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_11_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[11]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[11] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[11] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[11] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[11] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_11, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_11_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[11])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[11]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[11]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[11] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[11] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_11, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_12_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[12]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[12] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[12] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[12] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[12] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_12, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_12_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[12])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[12]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[12]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[12] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[12] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_12, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_13_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[13]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[13] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[13] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[13] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[13] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_13, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_13_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[13])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[13]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[13]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[13] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[13] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_13, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_14_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[14]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[14] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[14] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[14] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[14] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_14, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_14_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[14])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[14]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[14]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[14] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[14] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_14, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_15_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[15]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[15] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[15] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[15] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[15] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_15, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_15_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[15])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[15]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[15]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[15] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[15] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_15, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

disp

VHDL source list from CVS: liberouter/vhdl_design/ (date: 2004-10-23 20:00)

Preconditions

Formulas

lemma_value_1_bit_0_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[0]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[0] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[0] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[0] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[0] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_0, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_0_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[0])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[0]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[0]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[0] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[0] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_0, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_1_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[1]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[1] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[1] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[1] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[1] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_1, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_1_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[1])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[1]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[1]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[1] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[1] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_1, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_2_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[2]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[2] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[2] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[2] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[2] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_2, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_2_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[2])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[2]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[2]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[2] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[2] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_2, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_3_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[3]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[3] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[3] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[3] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[3] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_3, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_3_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[3])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[3]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[3]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[3] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[3] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_3, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_4_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[4]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[4] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[4] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[4] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[4] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_4, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_4_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[4])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[4]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[4]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[4] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[4] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_4, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_5_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[5]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[5] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[5] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[5] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[5] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_5, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_5_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[5])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[5]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[5]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[5] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[5] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_5, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_6_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[6]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[6] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[6] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[6] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[6] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_6, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_6_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[6])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[6]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[6]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[6] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[6] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_6, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_7_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[7]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[7] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[7] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[7] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[7] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_7, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_7_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[7])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[7]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[7]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[7] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[7] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_7, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_8_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[8]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[8] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[8] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[8] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[8] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_8, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_8_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[8])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[8]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[8]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[8] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[8] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_8, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_9_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[9]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[9] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[9] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[9] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[9] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_9, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_9_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[9])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[9]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[9]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[9] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[9] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_9, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_10_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[10]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[10] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[10] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[10] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[10] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_10, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_10_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[10])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[10]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[10]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[10] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[10] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_10, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_11_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[11]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[11] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[11] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[11] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[11] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_11, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_11_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[11])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[11]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[11]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[11] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[11] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_11, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_12_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[12]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[12] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[12] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[12] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[12] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_12, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_12_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[12])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[12]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[12]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[12] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[12] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_12, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_13_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[13]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[13] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[13] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[13] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[13] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_13, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_13_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[13])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[13]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[13]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[13] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[13] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_13, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_14_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[14]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[14] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[14] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[14] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[14] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_14, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_14_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[14])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[14]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[14]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[14] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[14] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_14, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_1_bit_15_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[15]) U
			      (FIFO_DV & (~FIFO_DO[16]) & FIFO_DO[15] & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F (DRAM_DO[15] & DRAM_WE)
			  )
		        )

If 1 comes to FIFO_DO[15] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 1 comes finally to DRAM_DO[15] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_15, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv

lemma_value_0_bit_15_in_future_out

G (
		          (
			    ( (~FSM_U.FSM_SETREG) & (~FSM_U.FSM_DO_CMD) & (~FSM_U.FSM_DRAM_REQ) &
			      (~FSM_U.FSM_COPY) ) &
		            ( (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[15])) U
			      (FIFO_DV & (~FIFO_DO[16]) & (~FIFO_DO[15]) & FIFO_RD) ) &
			    ( ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0]) U
			      ((~FIFO_U.EMPTY) & FIFO_U.DATA_OUT[0] & FIFO_U.READ_REQ) )
			  ) ->
			  (
			    F ((~DRAM_DO[15]) & DRAM_WE)
			  )
		        )

If 0 comes to FIFO_DO[15] and data on both FIFOs are valid and FIFO_U tells dispatcher to copy the packet and dispatcher reads these values from both FIFOs then 0 comes finally to DRAM_DO[15] too

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_15, pre_clk_fifo_do_16, pre_clk_sau_fifo_do_0, pre_clk_fifo_dv