stu_length

Author: Pavel Simecek

VHDL source list from CVS: liberouter/vhdl_design/projects/scampi_ph1/comp/stu (date: 2004-05-20 01:00)

../lb/local_bus.vhd (vhdl)
../lb/lbconn_mem.vhd (vhdl)
stu_length.vhd (vhdl)

Preconditions

pre_clk: (G F CLK) & (G F !CLK)

pre_reset: RESET & (X G ! RESET)

pre_infinitelytimes_ready: G F READY

Formulas

lemma_phase_1_not_const_0

! F G (stul.reg_phase_1_ = 0)

Together with all lemma_phase_[1-4]_not_const_0 says, that any phase register bit cannot be constantly 0 (inactive) from any point of the run of the system.

Preconditions:
pre_clk, pre_reset, pre_infinitelytimes_ready

Verified in 0.77 s.

lemma_phase_2_not_const_0

! F G (stul.reg_phase_2_ = 0)

Preconditions:
pre_clk, pre_reset, pre_infinitelytimes_ready

Verified in 0.77 s.

lemma_phase_3_not_const_0

! F G (stul.reg_phase_3_ = 0)

Preconditions:
pre_clk, pre_reset, pre_infinitelytimes_ready

Verified in 0.81 s.

lemma_phase_4_not_const_0

! F G (stul.reg_phase_4_ = 0)

Preconditions:
pre_clk, pre_reset, pre_infinitelytimes_ready

Verified in 0.8 s.

lemma_banks_are_consistent

G (((!stul.en_reg_5)&(stul.reg_phase_1_|stul.reg_phase_2_|stul.reg_phase_3_|stul.reg_phase_4_))-> ((!stul.reg_addr_out_8_) <-> stul.br_addr_lb_9_))

reg_addr_out_8_ is always opposite to br_addr_lb_9_, when we are not loading new flag register value from local bus (i. e. en_reg_5 is not enabled) and at least one bit of the phase register is enabled.

Preconditions:
pre_clk, pre_reset

Verified in 1.03 s.

lemma_banks_are_consistent_easy_to_verify

G ((!stul.en_reg_5) -> (stul.reg_flag_1_ <-> !stul.br_addr_lb_9_))

reg_flag_1_ is always opposite to br_addr_lb_9_, when we are not loading new flag register value from local bus (i. e. en_reg_5 is not enabled).

Preconditions:
pre_clk, pre_reset

Verified in 0.82 s.

lemma_false

G 0

This is a false assertions. It is used to prove, that preconditions and not in the contradiction

Preconditions:
pre_clk, pre_reset