• disp_inst - (2004-11-16 12:00)

disp_inst

Author: Pavel Simecek
In this verification I only proved for single bits of input vector PFIFO_DO, that if the bit should be copied (according the control signals), then it finally shows on the corresponding output signal. Verification is done separately for each bit and its value (0 or 1).

VHDL source list from CVS: liberouter/vhdl_design/ (date: 2004-11-16 12:00)

units/common/pkg/math_pack.vhd (vhdl)
projects/scampi_ph2/pkg/commands.vhd (vhdl)
units/common/cmd_dec/cmd_dec_cmp.vhd (vhdl)
units/common/cmd_dec/cmd_dec.vhd (vhdl)
units/common/fifo/fifo.vhd (vhdl)
units/disp/disp_fsm.vhd (vhdl)
units/disp/disp_ent.vhd (vhdl)
units/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)->(PFIFO_DO[0] <-> X PFIFO_DO[0]))PFIFO_DO[0] is synchronized with CLK

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

pre_clk_fifo_do_17: G (((X CLK) -> CLK)->(PFIFO_DO[17] <-> X PFIFO_DO[17]))PFIFO_DO[17] is synchronized with CLK

pre_clk_fifo_do_18: G (((X CLK) -> CLK)->(PFIFO_DO[18] <-> X PFIFO_DO[18]))PFIFO_DO[18] is synchronized with CLK

pre_clk_fifo_do_19: G (((X CLK) -> CLK)->(PFIFO_DO[19] <-> X PFIFO_DO[19]))PFIFO_DO[19] is synchronized with CLK

pre_clk_fifo_do_20: G (((X CLK) -> CLK)->(PFIFO_DO[20] <-> X PFIFO_DO[20]))PFIFO_DO[20] is synchronized with CLK

pre_clk_fifo_do_21: G (((X CLK) -> CLK)->(PFIFO_DO[21] <-> X PFIFO_DO[21]))PFIFO_DO[21] is synchronized with CLK

pre_clk_fifo_do_22: G (((X CLK) -> CLK)->(PFIFO_DO[22] <-> X PFIFO_DO[22]))PFIFO_DO[22] is synchronized with CLK

pre_clk_fifo_do_23: G (((X CLK) -> CLK)->(PFIFO_DO[23] <-> X PFIFO_DO[23]))PFIFO_DO[23] is synchronized with CLK

pre_clk_fifo_do_24: G (((X CLK) -> CLK)->(PFIFO_DO[24] <-> X PFIFO_DO[24]))PFIFO_DO[24] is synchronized with CLK

pre_clk_fifo_do_25: G (((X CLK) -> CLK)->(PFIFO_DO[25] <-> X PFIFO_DO[25]))PFIFO_DO[25] is synchronized with CLK

pre_clk_fifo_do_26: G (((X CLK) -> CLK)->(PFIFO_DO[26] <-> X PFIFO_DO[26]))PFIFO_DO[26] is synchronized with CLK

pre_clk_fifo_do_27: G (((X CLK) -> CLK)->(PFIFO_DO[27] <-> X PFIFO_DO[27]))PFIFO_DO[27] is synchronized with CLK

pre_clk_fifo_do_28: G (((X CLK) -> CLK)->(PFIFO_DO[28] <-> X PFIFO_DO[28]))PFIFO_DO[28] is synchronized with CLK

pre_clk_fifo_do_29: G (((X CLK) -> CLK)->(PFIFO_DO[29] <-> X PFIFO_DO[29]))PFIFO_DO[29] is synchronized with CLK

pre_clk_fifo_do_30: G (((X CLK) -> CLK)->(PFIFO_DO[30] <-> X PFIFO_DO[30]))PFIFO_DO[30] is synchronized with CLK

pre_clk_fifo_do_31: G (((X CLK) -> CLK)->(PFIFO_DO[31] <-> X PFIFO_DO[31]))PFIFO_DO[31] is synchronized with CLK

pre_clk_cmd_term_pfifo_do: G (((X CLK) -> CLK)->(cmd_term_pfifo_do <-> X cmd_term_pfifo_do))cmd_term_pfifo_do is synchronized with CLK

pre_clk_cmd_soc_pfifo_do: G (((X CLK) -> CLK)->(cmd_soc_pfifo_do <-> X cmd_soc_pfifo_do))cmd_soc_pfifo_do is synchronized with CLK

pre_clk_cmd_pckrec_pfifo_do: G (((X CLK) -> CLK)->(cmd_pckrec_pfifo_do <-> X cmd_pckrec_pfifo_do))cmd_pckrec_pfifo_do is synchronized with CLK

pre_clk_do_rdy: G (((X CLK) -> CLK)->(DO_RDY <-> X DO_RDY))DO_RDY is synchronized with CLK

pre_do_rdy_inf_times_1: G F DO_RDYDO_RDY is infinitely times 1

Formulas

lemma_value_1_bit_0_in_future_out

G (
		          (PFIFO_DO[0] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [0] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[0] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[0] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_0, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_0_in_future_out

G (
		          ((~PFIFO_DO[0]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [0]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[0] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[0] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_0, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_1_in_future_out

G (
		          (PFIFO_DO[1] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [1] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[1] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[1] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_1, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_1_in_future_out

G (
		          ((~PFIFO_DO[1]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [1]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[1] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[1] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_1, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_2_in_future_out

G (
		          (PFIFO_DO[2] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [2] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[2] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[2] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_2, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_2_in_future_out

G (
		          ((~PFIFO_DO[2]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [2]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[2] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[2] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_2, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_3_in_future_out

G (
		          (PFIFO_DO[3] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [3] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[3] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[3] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_3, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_3_in_future_out

G (
		          ((~PFIFO_DO[3]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [3]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[3] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[3] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_3, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_4_in_future_out

G (
		          (PFIFO_DO[4] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [4] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[4] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[4] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_4, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_4_in_future_out

G (
		          ((~PFIFO_DO[4]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [4]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[4] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[4] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_4, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_5_in_future_out

G (
		          (PFIFO_DO[5] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [5] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[5] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[5] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_5, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_5_in_future_out

G (
		          ((~PFIFO_DO[5]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [5]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[5] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[5] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_5, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_6_in_future_out

G (
		          (PFIFO_DO[6] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [6] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[6] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[6] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_6, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_6_in_future_out

G (
		          ((~PFIFO_DO[6]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [6]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[6] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[6] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_6, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_7_in_future_out

G (
		          (PFIFO_DO[7] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [7] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[7] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[7] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_7, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_7_in_future_out

G (
		          ((~PFIFO_DO[7]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [7]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[7] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[7] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_7, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_8_in_future_out

G (
		          (PFIFO_DO[8] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [8] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[8] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[8] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_8, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_8_in_future_out

G (
		          ((~PFIFO_DO[8]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [8]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[8] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[8] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_8, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_9_in_future_out

G (
		          (PFIFO_DO[9] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [9] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[9] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[9] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_9, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_9_in_future_out

G (
		          ((~PFIFO_DO[9]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [9]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[9] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[9] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_9, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_10_in_future_out

G (
		          (PFIFO_DO[10] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [10] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[10] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[10] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_10, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_10_in_future_out

G (
		          ((~PFIFO_DO[10]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [10]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[10] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[10] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_10, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_11_in_future_out

G (
		          (PFIFO_DO[11] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [11] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[11] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[11] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_11, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_11_in_future_out

G (
		          ((~PFIFO_DO[11]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [11]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[11] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[11] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_11, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_12_in_future_out

G (
		          (PFIFO_DO[12] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [12] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[12] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[12] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_12, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_12_in_future_out

G (
		          ((~PFIFO_DO[12]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [12]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[12] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[12] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_12, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_13_in_future_out

G (
		          (PFIFO_DO[13] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [13] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[13] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[13] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_13, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_13_in_future_out

G (
		          ((~PFIFO_DO[13]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [13]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[13] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[13] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_13, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_14_in_future_out

G (
		          (PFIFO_DO[14] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [14] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[14] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[14] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_14, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_14_in_future_out

G (
		          ((~PFIFO_DO[14]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [14]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[14] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[14] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_14, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_15_in_future_out

G (
		          (PFIFO_DO[15] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [15] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[15] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[15] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_15, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_15_in_future_out

G (
		          ((~PFIFO_DO[15]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [15]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[15] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[15] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_15, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_16_in_future_out

G (
		          (PFIFO_DO[16] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [16] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[16] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[16] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_16, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_16_in_future_out

G (
		          ((~PFIFO_DO[16]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [16]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[16] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[16] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_16, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_17_in_future_out

G (
		          (PFIFO_DO[17] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [17] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[17] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[17] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_17, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_17_in_future_out

G (
		          ((~PFIFO_DO[17]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [17]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[17] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[17] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_17, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_18_in_future_out

G (
		          (PFIFO_DO[18] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [18] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[18] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[18] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_18, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_18_in_future_out

G (
		          ((~PFIFO_DO[18]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [18]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[18] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[18] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_18, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_19_in_future_out

G (
		          (PFIFO_DO[19] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [19] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[19] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[19] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_19, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_19_in_future_out

G (
		          ((~PFIFO_DO[19]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [19]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[19] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[19] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_19, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_20_in_future_out

G (
		          (PFIFO_DO[20] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [20] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[20] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[20] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_20, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_20_in_future_out

G (
		          ((~PFIFO_DO[20]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [20]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[20] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[20] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_20, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_21_in_future_out

G (
		          (PFIFO_DO[21] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [21] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[21] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[21] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_21, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_21_in_future_out

G (
		          ((~PFIFO_DO[21]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [21]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[21] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[21] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_21, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_22_in_future_out

G (
		          (PFIFO_DO[22] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [22] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[22] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[22] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_22, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_22_in_future_out

G (
		          ((~PFIFO_DO[22]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [22]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[22] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[22] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_22, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_23_in_future_out

G (
		          (PFIFO_DO[23] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [23] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[23] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[23] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_23, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_23_in_future_out

G (
		          ((~PFIFO_DO[23]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [23]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[23] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[23] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_23, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_24_in_future_out

G (
		          (PFIFO_DO[24] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [24] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[24] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[24] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_24, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_24_in_future_out

G (
		          ((~PFIFO_DO[24]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [24]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[24] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[24] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_24, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_25_in_future_out

G (
		          (PFIFO_DO[25] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [25] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[25] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[25] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_25, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_25_in_future_out

G (
		          ((~PFIFO_DO[25]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [25]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[25] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[25] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_25, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_26_in_future_out

G (
		          (PFIFO_DO[26] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [26] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[26] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[26] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_26, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_26_in_future_out

G (
		          ((~PFIFO_DO[26]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [26]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[26] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[26] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_26, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_27_in_future_out

G (
		          (PFIFO_DO[27] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [27] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[27] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[27] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_27, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_27_in_future_out

G (
		          ((~PFIFO_DO[27]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [27]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[27] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[27] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_27, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_28_in_future_out

G (
		          (PFIFO_DO[28] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [28] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[28] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[28] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_28, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_28_in_future_out

G (
		          ((~PFIFO_DO[28]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [28]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[28] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[28] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_28, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_29_in_future_out

G (
		          (PFIFO_DO[29] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [29] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[29] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[29] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_29, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_29_in_future_out

G (
		          ((~PFIFO_DO[29]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [29]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[29] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[29] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_29, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_30_in_future_out

G (
		          (PFIFO_DO[30] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [30] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[30] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[30] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_30, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_30_in_future_out

G (
		          ((~PFIFO_DO[30]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [30]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[30] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[30] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_30, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_1_bit_31_in_future_out

G (
		          (PFIFO_DO[31] & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F (\DO [31] & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 1 comes to PFIFO_DO[31] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 1 comes finally to DO[31] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_31, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do

lemma_value_0_bit_31_in_future_out

G (
		          ((~PFIFO_DO[31]) & PFIFO_RD & (!cmd_term_pfifo_do) & (!cmd_soc_pfifo_do) & (!cmd_pckrec_pfifo_do))
			   -> (F ((~\DO [31]) & (!cmd_term_do) & (!cmd_soc_do) & (!cmd_pckrec_do) ))
		        )

If 0 comes to PFIFO_DO[31] (as a data, not a command) and dispatcher is ready for receiving and command for termination is not comming, then 0 comes finally to DO[31] too (sent as a data, not as any command)

Preconditions:
pre_clk, pre_reset, pre_clk_fifo_do_31, pre_clk_do_rdy, pre_do_rdy_inf_times_1, pre_clk_cmd_term_pfifo_do, pre_clk_cmd_soc_pfifo_do, pre_clk_cmd_pckrec_pfifo_do