• Sampling unit - development
• Sampling Unit - Development - (2005-05-01 21:00)

Sampling unit - development

Author: Tomas Kratochvila

VHDL source list (date: Thu Apr 8 07:12:23 2004)

disp_empty.vhd (vhdl)
disp_ent.vhd (vhdl)
disp_saudebug.vhd (vhdl)
lup_empty.vhd (vhdl)
lup_ent.vhd (vhdl)
lup_saudebug.vhd (vhdl)
top_level.vhd (vhdl)

Preconditions

preRESET: F ( SAU_INS_notri.RESET );

preLRESET: F ( LRESET );

preCLK2X_RUNNING: G ( F (SAU_INS_notri.LBCLK) & F (!SAU_INS_notri.LBCLK) );

Formulas

control_data_flag

   G ( ! (
      (!SAU_INS_notri.RESET) &
      (!LRESET) &
      SAU_INS_notri.NOT_control_flag &
      SAU_INS_notri.NOT_data_flag
     )  );

Mutual exclusion of NOT_control_flag and NOT_data_flag.

mutex_mode_wr_init_wr_vec00, 01, .., 15

   G ( ! ( (SAU_INS_notri.nx72) & (SAU_INS_notri.nx57, 58, .., 71, 73) ) );

Mutual exclusion of mode_wr and init_wr_vec. Settings: pre G ( ! ( (!(mode_wr=0)) & (!(init_wr_vec=0)) ) )

mode_wr is synthetized into nx72. init_wr_vec is synthetized into nx57, nx58, .., nx71, nx73.

control_a_d

   G ( !( SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_A &
      SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_B ) );

Mutual exclusion of CONTROL_A .. CONTROL_D

Preconditions:
preRESET, preCLK2X_RUNNING

Sampling Unit - Development

Author: Tomas Kratochvila

VHDL source list (date: Thu Apr 8 07:12:23 2004)

disp_empty.vhd (vhdl)
disp_ent.vhd (vhdl)
disp_saudebug.vhd (vhdl)
lup_empty.vhd (vhdl)
lup_ent.vhd (vhdl)
lup_saudebug.vhd (vhdl)
top_level.vhd (vhdl)

Preconditions

preRESET: F ( SAU_INS_notri.RESET );

preLRESET: F ( LRESET );

preCLK2X_RUNNING: G ( F (SAU_INS_notri.LBCLK) & F (!SAU_INS_notri.LBCLK) );

Formulas

control_data_flag

G !(
     ! SAU_INS_notri.RESET &
     ! LRESET &
     SAU_INS_notri.NOT_control_flag &
     SAU_INS_notri.NOT_data_flag
   );

Mutual exclusion of NOT_control_flag and NOT_data_flag.

Verified in 3.95 s.

mutex_mode_wr_init_wr_vec

 G (
     ! (
         SAU_INS_notri.nx57 & SAU_INS_notri.nx58 & SAU_INS_notri.nx59 &
         SAU_INS_notri.nx60 & SAU_INS_notri.nx61 & SAU_INS_notri.nx62 &
	 SAU_INS_notri.nx63 & SAU_INS_notri.nx64 & SAU_INS_notri.nx65 &
         SAU_INS_notri.nx66 & SAU_INS_notri.nx67 & SAU_INS_notri.nx68 &
         SAU_INS_notri.nx69 & SAU_INS_notri.nx70 & SAU_INS_notri.nx71 &
	 SAU_INS_notri.nx72 & SAU_INS_notri.nx73
       )
   )
      

Mutual exclusion of mode_wr and init_wr_vec. Settings: G ! ( ! mode_wr & ! init_wr_vec ) Signal mode_wr is synthetized into signal nx72. Vector init_wr_vec is synthetized into signals nx57, nx58, .., nx71, nx73.

Verified in 4.14 s.

control_abcd

G !(
     ! LRESET &
     (
       ( SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_A &
         SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_B )
       |
       ( SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_A &
         SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_C )
       |
       ( SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_A &
         SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_D )
       |
       ( SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_B &
         SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_C )
       |
       ( SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_B &
         SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_D )
       |
       ( SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_C &
         SAU_INS_notri.sau_cores_0_U_SAU_CORE.CONTROL_D )
     )
   );
      

Mutual exclusion of signals: CONTROL_A, CONTROL_B, CONTROL_C, and CONTROL_D.

Preconditions:
preRESET, preLRESET, preCLK2X_RUNNING

Verified in 7.47.