• Edit Engine - (2004-11-14 23:30)

Edit Engine

Author: Tomas Kratochvila

VHDL source list from CVS: liberouter/vhdl_design/units/ee/comp/ee_unit/ (date: 2004-11-14 23:30)

comp/dram_unit/dram_u_fsm_mem.vhd (vhdl)
comp/dram_unit/dram_u_fsm.vhd (vhdl)
comp/dram_unit/dram_u.vhd (vhdl)
comp/send_unit/send_u.vhd (vhdl)
comp/control_unit/control_u_fsm_mem.vhd (vhdl)
comp/control_unit/control_u_fsm.vhd (vhdl)
comp/control_unit/control_u.vhd (vhdl)
comp/output_unit/output_u_fifo.vhd (vhdl)
comp/output_unit/output_u.vhd (vhdl)
comp/alu/alu.vhd (vhdl)
pd_block.vhd (vhdl)
ep_block.vhd (vhdl)
pp_block.vhd (vhdl)
im_block.vhd (vhdl)
addr_dc_pc.vhd (vhdl)
ee.vhd (vhdl)

Preconditions

preCLK_RUNNING: G ( F (CLK) & F (!CLK) ) Precondition that clock CLK is ticking.

Formulas

RW_mutual_exclusion

  G (! ( plx_wr && plx_rd ) )

Simple read-write mutual exclusion formula.

Preconditions:
preCLK_RUNNING

Verified in 0.66 s.

DRAM_communication_WR

  G ( ( !DRAM_COM_U.RESET && DRAM_COM_U.START ) -> ( X DRAM_WR_REQ ) )

DRAM scheduler communication for WR REQ FSM (Write Request Finite State Machine)

Preconditions:
preCLK_RUNNING

DRAM_COM_U.START .. DRAM_WR_REQ .. DRAM_ACK

Verified in 0.68 s.

DRAM_communication_ACK

  G ( ( !DRAM_COM_U.RESET && DRAM_COM_U.START ) -> ( X DRAM_ACK ) )

DRAM scheduler communication for WR REQ FSM (Write Request Finite State Machine)

Preconditions:
preCLK_RUNNING

DRAM_COM_U.START .. DRAM_WR_REQ .. DRAM_ACK

Verified in 0.72 s.

DRAM_communication_RD

  G ( ( !DRAM_COM_U.RESET && DRAM_COM_U.START ) -> ( X DRAM_RD_REQ ) )

DRAM scheduler communication for RD REQ FSM (Read Request Finite State Machine)

Preconditions:
preCLK_RUNNING

DRAM_COM_U.START .. DRAM_RD_REQ .. DRAM_ACK

Verified in 1.08 s.

DRAM_communication_DEC

  G ( ( !DRAM_COM_U.RESET && DRAM_COM_U.START ) -> ( X DRAM_DEC_REQ ) )

DRAM scheduler communication for DEC REQ FSM (Decrement Request Finite State Machine)

Preconditions:
preCLK_RUNNING

DRAM_COM_U.START .. DRAM_DEC_REQ .. DRAM_ACK .. CTRL_U.DRAM_FINISH

Verified in 0.71 s.

DRAM_communication_FINISH

  G ( ( !DRAM_COM_U.RESET && DRAM_COM_U.START ) -> (X CTRL_U.DRAM_FINISH) )

DRAM scheduler communication for DEC REQ FSM (Decrement Request Finite State Machine)

Preconditions:
preCLK_RUNNING

DRAM_COM_U.START .. DRAM_DEC_REQ .. DRAM_ACK .. CTRL_U.DRAM_FINISH

Verified in 0.74 s.

DRAM_coordination

  G ( !DRAM_COM_U.RESET && !( (DRAM_COM_U.INP_PTR + 1) = DRAM_COM_U.OUT_PTR) )

DRAM scheduler coordination of data transfare into PD block using CNT CE FSM (Counter Clock Enable Finite State Machine). If the condition "(InputPointer + 1) = OutputPointer" is satisfied, than the data that was still not processed will be rewriten.

Preconditions:
preCLK_RUNNING