hfe_core

Author: Pavel Simecek

VHDL source list from CVS: liberouter/vhdl_design/units/hfe/ (date: 2004-03-11 01:00)

hfe_core.vhd (vhdl)
hfe_types.vhd (vhdl)
hfe_control.vhd (vhdl)
hfe_alu.vhd (vhdl)
hfe_stack.vhd (vhdl)
hfe_muxs.vhd (vhdl)
hfe_reg_file.vhd (vhdl)

Preconditions

pre1: RESET & X G (~RESET) Reset is set only at the beginning

pre2: G (( F CLK ) & ( F ~CLK )) Clocks are alive

pre3: (~CLK) Clock is initiated to 0

pre5: G ( \dwait_en -> (F ( \dwait_en & DIN_VAL))) This precondition implies that

pre_sometimes_repi: G F (((INSTR_IN1[17..10] = 30) & (!reg_pc_sel)) | ((INSTR_IN2[17..10] = 30) & reg_pc_sel)) From time to time there appears an instruction REPI

pre_clk_0_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[0]->X INSTR_IN1[0])&((~INSTR_IN1[0]) -> (X ~INSTR_IN1[0])))) INSTR_IN1[0] is synchronized with clocks

pre_clk_1_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[1]->X INSTR_IN1[1])&((~INSTR_IN1[1]) -> (X ~INSTR_IN1[1])))) INSTR_IN1[1] is synchronized with clocks

pre_clk_2_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[2]->X INSTR_IN1[2])&((~INSTR_IN1[2]) -> (X ~INSTR_IN1[2])))) INSTR_IN1[2] is synchronized with clocks

pre_clk_3_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[3]->X INSTR_IN1[3])&((~INSTR_IN1[3]) -> (X ~INSTR_IN1[3])))) INSTR_IN1[3] is synchronized with clocks

pre_clk_4_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[4]->X INSTR_IN1[4])&((~INSTR_IN1[4]) -> (X ~INSTR_IN1[4])))) INSTR_IN1[4] is synchronized with clocks

pre_clk_5_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[5]->X INSTR_IN1[5])&((~INSTR_IN1[5]) -> (X ~INSTR_IN1[5])))) INSTR_IN1[5] is synchronized with clocks

pre_clk_6_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[6]->X INSTR_IN1[6])&((~INSTR_IN1[6]) -> (X ~INSTR_IN1[6])))) INSTR_IN1[6] is synchronized with clocks

pre_clk_7_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[7]->X INSTR_IN1[7])&((~INSTR_IN1[7]) -> (X ~INSTR_IN1[7])))) INSTR_IN1[7] is synchronized with clocks

pre_clk_8_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[8]->X INSTR_IN1[8])&((~INSTR_IN1[8]) -> (X ~INSTR_IN1[8])))) INSTR_IN1[8] is synchronized with clocks

pre_clk_9_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[9]->X INSTR_IN1[9])&((~INSTR_IN1[9]) -> (X ~INSTR_IN1[9])))) INSTR_IN1[9] is synchronized with clocks

pre_clk_10_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[10]->X INSTR_IN1[10])&((~INSTR_IN1[10]) -> (X ~INSTR_IN1[10])))) INSTR_IN1[10] is synchronized with clocks

pre_clk_11_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[11]->X INSTR_IN1[11])&((~INSTR_IN1[11]) -> (X ~INSTR_IN1[11])))) INSTR_IN1[11] is synchronized with clocks

pre_clk_12_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[12]->X INSTR_IN1[12])&((~INSTR_IN1[12]) -> (X ~INSTR_IN1[12])))) INSTR_IN1[12] is synchronized with clocks

pre_clk_13_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[13]->X INSTR_IN1[13])&((~INSTR_IN1[13]) -> (X ~INSTR_IN1[13])))) INSTR_IN1[13] is synchronized with clocks

pre_clk_14_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[14]->X INSTR_IN1[14])&((~INSTR_IN1[14]) -> (X ~INSTR_IN1[14])))) INSTR_IN1[14] is synchronized with clocks

pre_clk_15_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[15]->X INSTR_IN1[15])&((~INSTR_IN1[15]) -> (X ~INSTR_IN1[15])))) INSTR_IN1[15] is synchronized with clocks

pre_clk_16_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[16]->X INSTR_IN1[16])&((~INSTR_IN1[16]) -> (X ~INSTR_IN1[16])))) INSTR_IN1[16] is synchronized with clocks

pre_clk_17_instr_in1: G (((X CLK) -> CLK)->((INSTR_IN1[17]->X INSTR_IN1[17])&((~INSTR_IN1[17]) -> (X ~INSTR_IN1[17])))) INSTR_IN1[17] is synchronized with clocks

pre_clk_0_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[0]->X INSTR_IN2[0])&((~INSTR_IN2[0]) -> (X ~INSTR_IN2[0])))) INSTR_IN2[0] is synchronized with clocks

pre_clk_1_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[1]->X INSTR_IN2[1])&((~INSTR_IN2[1]) -> (X ~INSTR_IN2[1])))) INSTR_IN2[1] is synchronized with clocks

pre_clk_2_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[2]->X INSTR_IN2[2])&((~INSTR_IN2[2]) -> (X ~INSTR_IN2[2])))) INSTR_IN2[2] is synchronized with clocks

pre_clk_3_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[3]->X INSTR_IN2[3])&((~INSTR_IN2[3]) -> (X ~INSTR_IN2[3])))) INSTR_IN2[3] is synchronized with clocks

pre_clk_4_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[4]->X INSTR_IN2[4])&((~INSTR_IN2[4]) -> (X ~INSTR_IN2[4])))) INSTR_IN2[4] is synchronized with clocks

pre_clk_5_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[5]->X INSTR_IN2[5])&((~INSTR_IN2[5]) -> (X ~INSTR_IN2[5])))) INSTR_IN2[5] is synchronized with clocks

pre_clk_6_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[6]->X INSTR_IN2[6])&((~INSTR_IN2[6]) -> (X ~INSTR_IN2[6])))) INSTR_IN2[6] is synchronized with clocks

pre_clk_7_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[7]->X INSTR_IN2[7])&((~INSTR_IN2[7]) -> (X ~INSTR_IN2[7])))) INSTR_IN2[7] is synchronized with clocks

pre_clk_8_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[8]->X INSTR_IN2[8])&((~INSTR_IN2[8]) -> (X ~INSTR_IN2[8])))) INSTR_IN2[8] is synchronized with clocks

pre_clk_9_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[9]->X INSTR_IN2[9])&((~INSTR_IN2[9]) -> (X ~INSTR_IN2[9])))) INSTR_IN2[9] is synchronized with clocks

pre_clk_10_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[10]->X INSTR_IN2[10])&((~INSTR_IN2[10]) -> (X ~INSTR_IN2[10])))) INSTR_IN2[10] is synchronized with clocks

pre_clk_11_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[11]->X INSTR_IN2[11])&((~INSTR_IN2[11]) -> (X ~INSTR_IN2[11])))) INSTR_IN2[11] is synchronized with clocks

pre_clk_12_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[12]->X INSTR_IN2[12])&((~INSTR_IN2[12]) -> (X ~INSTR_IN2[12])))) INSTR_IN2[12] is synchronized with clocks

pre_clk_13_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[13]->X INSTR_IN2[13])&((~INSTR_IN2[13]) -> (X ~INSTR_IN2[13])))) INSTR_IN2[13] is synchronized with clocks

pre_clk_14_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[14]->X INSTR_IN2[14])&((~INSTR_IN2[14]) -> (X ~INSTR_IN2[14])))) INSTR_IN2[14] is synchronized with clocks

pre_clk_15_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[15]->X INSTR_IN2[15])&((~INSTR_IN2[15]) -> (X ~INSTR_IN2[15])))) INSTR_IN2[15] is synchronized with clocks

pre_clk_16_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[16]->X INSTR_IN2[16])&((~INSTR_IN2[16]) -> (X ~INSTR_IN2[16])))) INSTR_IN2[16] is synchronized with clocks

pre_clk_17_instr_in2: G (((X CLK) -> CLK)->((INSTR_IN2[17]->X INSTR_IN2[17])&((~INSTR_IN2[17]) -> (X ~INSTR_IN2[17])))) INSTR_IN2[17] is synchronized with clocks

pre_repi_arg_not_zero_instr_in1: G ((INSTR_IN1[17..10] = 30)->(INSTR_IN1[7..0]>=2)) REPI in INSTR_IN1 comes with argument greater than 1

pre_repi_arg_not_zero_instr_in2: G ((INSTR_IN2[17..10] = 30)->(INSTR_IN2[7..0]>=2)) REPI in INSTR_IN2 comes with argument greater than 1

Formulas

lemma_bits_of_loop_cntr_sometimes_active

  G F    (loop_cntr_0_ | loop_cntr_1_ | loop_cntr_2_ | loop_cntr_3_ | loop_cntr_4_ |     loop_cntr_5_ | loop_cntr_6_ | loop_cntr_7_)

It is always reachable that loop_cntr!=0

Preconditions:
pre1, pre2, pre_sometimes_repi, pre_clk_0_instr_in1, pre_clk_0_instr_in2, pre_clk_1_instr_in1, pre_clk_1_instr_in2, pre_clk_2_instr_in1, pre_clk_2_instr_in2, pre_clk_3_instr_in1, pre_clk_3_instr_in2, pre_clk_4_instr_in1, pre_clk_4_instr_in2, pre_clk_5_instr_in1, pre_clk_5_instr_in2, pre_clk_6_instr_in1, pre_clk_6_instr_in2, pre_clk_7_instr_in1, pre_clk_7_instr_in2, pre_clk_8_instr_in1, pre_clk_8_instr_in2, pre_clk_9_instr_in1, pre_clk_9_instr_in2, pre_clk_10_instr_in1, pre_clk_10_instr_in2, pre_clk_11_instr_in1, pre_clk_11_instr_in2, pre_clk_12_instr_in1, pre_clk_12_instr_in2, pre_clk_13_instr_in1, pre_clk_13_instr_in2, pre_clk_14_instr_in1, pre_clk_14_instr_in2, pre_clk_15_instr_in1, pre_clk_15_instr_in2, pre_clk_16_instr_in1, pre_clk_16_instr_in2, pre_clk_17_instr_in1, pre_clk_17_instr_in2, pre_repi_arg_not_zero_instr_in1, pre_repi_arg_not_zero_instr_in2

lemma_exclusion_indd_inc_and_indd_dec

   G ( (indd_inc -> (~indd_dec)) && (indd_dec -> (~indd_inc)))

indd_inc and indd_dec are mutually exclusive

Preconditions:
pre1, pre2

lemma_exclusion_clear_int_and_set_int

   G ( (set_int -> (~clear_int)) && (clear_int -> (~set_int)))

set_int and clear_int are mutually exclusive

Preconditions:
pre1, pre2

lemma_exclusion_shortcut_en_sel_gpr_sel_din_sel_sin_i

   ((~CLK) U G ( ~ ( ( shortcut_en & sel_gpr ) | ( shortcut_en & sel_din ) |          ( shortcut_en & sel_din_i) | ( sel_gpr & sel_din ) |	  ( sel_gpr & sel_din_i) | ( sel_din & sel_din_i )        )    ))

Preconditions:
pre1, pre2, pre3

lemma_ds_ren_alive

   G ( (ds_ren -> F (~ds_ren)) & ((~ds_ren) -> F ds_ren) )

signal ds_ren is always alive

Preconditions:
pre1, pre2, pre3, pre5, pre_clk_0_instr_in1, pre_clk_0_instr_in2, pre_clk_1_instr_in1, pre_clk_1_instr_in2, pre_clk_2_instr_in1, pre_clk_2_instr_in2, pre_clk_3_instr_in1, pre_clk_3_instr_in2, pre_clk_4_instr_in1, pre_clk_4_instr_in2, pre_clk_5_instr_in1, pre_clk_5_instr_in2, pre_clk_6_instr_in1, pre_clk_6_instr_in2, pre_clk_7_instr_in1, pre_clk_7_instr_in2, pre_clk_8_instr_in1, pre_clk_8_instr_in2, pre_clk_9_instr_in1, pre_clk_9_instr_in2, pre_clk_10_instr_in1, pre_clk_10_instr_in2, pre_clk_11_instr_in1, pre_clk_11_instr_in2, pre_clk_12_instr_in1, pre_clk_12_instr_in2, pre_clk_13_instr_in1, pre_clk_13_instr_in2, pre_clk_14_instr_in1, pre_clk_14_instr_in2, pre_clk_15_instr_in1, pre_clk_15_instr_in2, pre_clk_16_instr_in1, pre_clk_16_instr_in2, pre_clk_17_instr_in1, pre_clk_17_instr_in2

It is false, because there can exists unsuitable sequence of instructions