helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/memory/memory_struct.ma".
  24 include "num/word16.ma".
  25 include "num/word24.ma".
  26
  27 (* ******************************** *)
  28 (* IP2022 REGISTER SPECIAL HARDWARE *)
  29 (* ******************************** *)
  30
  31 (* (Top Of Stack) : CALLH/CALL ↑ CALLH/CALL ↓ *)
  32 (* Pos2-15        : ...        ↑ ...        ↓ *)
  33 (* Pos16          : 0xFFFF     ↑ ...        ↓ *)
  34 ndefinition aux_callstack_type ≝ Array16T word16.
  35
  36 (* Top Of Stack : 0xFFFF on reset *)
  37 ndefinition new_callstack ≝
  38  mk_Array16T ? (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉)
  39                (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉)
  40                (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉)
  41                (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉).
  42
  43 ndefinition pop_callstack ≝
  44 λcs:aux_callstack_type.
  45  pair ?? (a16_1 ? cs)
  46          (mk_Array16T ? (a16_2 ? cs)  (a16_3 ? cs)  (a16_4 ? cs)  (a16_5 ? cs)
  47                         (a16_6 ? cs)  (a16_7 ? cs)  (a16_8 ? cs)  (a16_9 ? cs)
  48                         (a16_10 ? cs) (a16_11 ? cs) (a16_12 ? cs) (a16_13 ? cs)
  49                         (a16_14 ? cs) (a16_15 ? cs) (a16_16 ? cs) 〈〈xF,xF〉:〈xF,xF〉〉).
  50
  51 ndefinition push_callstack ≝
  52 λcs:aux_callstack_type.λtop.
  53  mk_Array16T ? top           (a16_1 ? cs)  (a16_2 ? cs)  (a16_3 ? cs)
  54                (a16_4 ? cs)  (a16_5 ? cs)  (a16_6 ? cs)  (a16_7 ? cs)
  55                (a16_8 ? cs)  (a16_9 ? cs)  (a16_10 ? cs) (a16_11 ? cs)
  56                (a16_12 ? cs) (a16_13 ? cs) (a16_14 ? cs) (a16_15 ? cs).
  57
  58 (* array ad accesso diretto di 8 registri ADDR a 24bit *)
  59 (* selezione con registro ADDRSEL, solo i primi 3bit validi *)
  60 ndefinition aux_addrarray_type ≝ Array8T word24.
  61
  62 (* tutti a 0x000000 on reset *)
  63 ndefinition new_addrarray ≝
  64  mk_Array8T ? (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
  65               (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
  66               (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
  67               (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉).
  68
  69 ndefinition get_low3bits ≝
  70 λaddrsel:byte8.
  71  match cnL ? addrsel with
  72   [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7
  73   | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ].
  74
  75 ndefinition get_addrarray ≝
  76 λaddrsel:byte8.λaa:aux_addrarray_type.
  77  getn_array8T (get_low3bits addrsel) ? aa.
  78
  79 ndefinition set_addrarray ≝
  80 λaddrsel:byte8.λaa:aux_addrarray_type.λv.
  81  setn_array8T (get_low3bits addrsel) ? aa v.
  82
  83 (* *********************************** *)
  84 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  85 (* *********************************** *)
  86
  87 (* ALU dell'IP2022 *)
  88 nrecord alu_IP2022: Type ≝
  89  {
  90  (* W: accumulatore *)
  91  acc_low_reg_IP2022 : byte8;
  92  (* MULH: parte alta moltiplicazione *)
  93  mulh_reg_IP2022 : byte8;
  94
  95  (* ADDRSEL: selettore di indirizzo *)
  96  addrsel_reg_IP2022 : byte8;
  97  (* ADDR [ADDRX|ADDRH|ADDRL] : array indirizzi indicizzati da ADDRSEL *)
  98  addr_array_IP2022 : aux_addrarray_type;
  99
 100  (* CALL [CALLH|CALLL] : stack indirizzi di ritorno *)
 101  call_stack_IP2022 : aux_callstack_type;
 102
 103  (* IP [IPH|IPL] : indirect pointer *)
 104  ip_reg_IP2022 : word16;
 105  (* DP [DPH|DPL] : data pointer *)
 106  dp_reg_IP2022 : word16;
 107  (* DATA [DATAH|DATAL] : data value *)
 108  data_reg_IP2022 : word16;
 109  (* SP [SPH|SPL] : stack pointer *)
 110  sp_reg_IP2022 : word16;
 111  (* PC [PCH|PCL] : program counter *)
 112  pc_reg_IP2022 : word16;
 113
 114  (* SPEED[xxxxSSSS] : divisore del clock *)
 115  speed_reg_IP2022 : exadecim;
 116  (* PAGE [PPPxxxxx] : selettore pagina *)
 117  page_reg_IP2022 : oct;
 118
 119  (* H: flag semi-carry (somma nibble basso) *)
 120  h_flag_IP2022 : bool;
 121  (* Z: flag zero *)
 122  z_flag_IP2022 : bool;
 123  (* C: flag carry *)
 124  c_flag_IP2022 : bool;
 125
 126  (* skip mode : effettua fetch-decode, no execute *)
 127  skip_mode_IP2022 : bool
 128  }.
 129
 130 notation "{hvbox('W_Reg' ≝ w ; break 'MulH_Reg' ≝ mulh ; break 'Addrsel_Reg' ≝ addrsel ; break 'Addr_Array' ≝ addr ; break 'Call_Stack' ≝ call ; break 'Ip_Reg' ≝ ip ; break 'Dp_Reg' ≝ dp ; break 'Data_Reg' ≝ data ; break 'Sp_Reg' ≝ sp ; break 'Pc_Reg' ≝ pc ; break 'Speed_Reg' ≝ speed ; break 'Page_Reg' ≝ page ; break 'H_Flag' ≝ hfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'Skip_Mode' ≝ skipmode)}"
 131  non associative with precedence 80 for
 132  @{ 'mk_alu_IP2022 $w $mulh $addrsel $addr $call $ip $dp $data $sp $pc $speed $page $hfl $zfl $cfl $skipmode }.
 133 interpretation "mk_alu_IP2022" 'mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode =
 134  (mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode).
 135
 136 (* ****** *)
 137 (* SETTER *)
 138 (* ****** *)
 139
 140 (* setter specifico IP2022 di A *)
 141 ndefinition set_acc_8_low_reg_IP2022 ≝
 142 λalu.λacclow':byte8.
 143  mk_alu_IP2022
 144   acclow'
 145   (mulh_reg_IP2022 alu)
 146   (addrsel_reg_IP2022 alu)
 147   (addr_array_IP2022 alu)
 148   (call_stack_IP2022 alu)
 149   (ip_reg_IP2022 alu)
 150   (dp_reg_IP2022 alu)
 151   (data_reg_IP2022 alu)
 152   (sp_reg_IP2022 alu)
 153   (pc_reg_IP2022 alu)
 154   (speed_reg_IP2022 alu)
 155   (page_reg_IP2022 alu)
 156   (h_flag_IP2022 alu)
 157   (z_flag_IP2022 alu)
 158   (c_flag_IP2022 alu)
 159   (skip_mode_IP2022 alu).
 160
 161 (* setter specifico IP2022 di MULH *)
 162 ndefinition set_mulh_reg_IP2022 ≝
 163 λalu.λmulh':byte8.
 164  mk_alu_IP2022
 165   (acc_low_reg_IP2022 alu)
 166   mulh'
 167   (addrsel_reg_IP2022 alu)
 168   (addr_array_IP2022 alu)
 169   (call_stack_IP2022 alu)
 170   (ip_reg_IP2022 alu)
 171   (dp_reg_IP2022 alu)
 172   (data_reg_IP2022 alu)
 173   (sp_reg_IP2022 alu)
 174   (pc_reg_IP2022 alu)
 175   (speed_reg_IP2022 alu)
 176   (page_reg_IP2022 alu)
 177   (h_flag_IP2022 alu)
 178   (z_flag_IP2022 alu)
 179   (c_flag_IP2022 alu)
 180   (skip_mode_IP2022 alu).
 181
 182 (* setter specifico IP2022 di ADDRSEL *)
 183 ndefinition set_addrsel_reg_IP2022 ≝
 184 λalu.λaddrsel':byte8.
 185  mk_alu_IP2022
 186   (acc_low_reg_IP2022 alu)
 187   (mulh_reg_IP2022 alu)
 188   addrsel'
 189   (addr_array_IP2022 alu)
 190   (call_stack_IP2022 alu)
 191   (ip_reg_IP2022 alu)
 192   (dp_reg_IP2022 alu)
 193   (data_reg_IP2022 alu)
 194   (sp_reg_IP2022 alu)
 195   (pc_reg_IP2022 alu)
 196   (speed_reg_IP2022 alu)
 197   (page_reg_IP2022 alu)
 198   (h_flag_IP2022 alu)
 199   (z_flag_IP2022 alu)
 200   (c_flag_IP2022 alu)
 201   (skip_mode_IP2022 alu).
 202
 203 (* setter specifico IP2022 di ADDR *)
 204 ndefinition set_addr_reg_IP2022 ≝
 205 λalu.λaddr':word24.
 206  mk_alu_IP2022
 207   (acc_low_reg_IP2022 alu)
 208   (mulh_reg_IP2022 alu)
 209   (addrsel_reg_IP2022 alu)
 210   (set_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu) addr')
 211   (call_stack_IP2022 alu)
 212   (ip_reg_IP2022 alu)
 213   (dp_reg_IP2022 alu)
 214   (data_reg_IP2022 alu)
 215   (sp_reg_IP2022 alu)
 216   (pc_reg_IP2022 alu)
 217   (speed_reg_IP2022 alu)
 218   (page_reg_IP2022 alu)
 219   (h_flag_IP2022 alu)
 220   (z_flag_IP2022 alu)
 221   (c_flag_IP2022 alu)
 222   (skip_mode_IP2022 alu).
 223
 224 (* setter specifico IP2022 di CALL *)
 225 ndefinition set_call_reg_IP2022 ≝
 226 λalu.λcall':word16.
 227  mk_alu_IP2022
 228   (acc_low_reg_IP2022 alu)
 229   (mulh_reg_IP2022 alu)
 230   (addrsel_reg_IP2022 alu)
 231   (addr_array_IP2022 alu)
 232   (setn_array16T x0 ? (call_stack_IP2022 alu) call')
 233   (ip_reg_IP2022 alu)
 234   (dp_reg_IP2022 alu)
 235   (data_reg_IP2022 alu)
 236   (sp_reg_IP2022 alu)
 237   (pc_reg_IP2022 alu)
 238   (speed_reg_IP2022 alu)
 239   (page_reg_IP2022 alu)
 240   (h_flag_IP2022 alu)
 241   (z_flag_IP2022 alu)
 242   (c_flag_IP2022 alu)
 243   (skip_mode_IP2022 alu).
 244
 245 ndefinition push_call_reg_IP2022 ≝
 246 λalu.λcall':word16.
 247  mk_alu_IP2022
 248   (acc_low_reg_IP2022 alu)
 249   (mulh_reg_IP2022 alu)
 250   (addrsel_reg_IP2022 alu)
 251   (addr_array_IP2022 alu)
 252   (push_callstack (call_stack_IP2022 alu) call')
 253   (ip_reg_IP2022 alu)
 254   (dp_reg_IP2022 alu)
 255   (data_reg_IP2022 alu)
 256   (sp_reg_IP2022 alu)
 257   (pc_reg_IP2022 alu)
 258   (speed_reg_IP2022 alu)
 259   (page_reg_IP2022 alu)
 260   (h_flag_IP2022 alu)
 261   (z_flag_IP2022 alu)
 262   (c_flag_IP2022 alu)
 263   (skip_mode_IP2022 alu).
 264
 265 (* setter specifico IP2022 di IP *)
 266 ndefinition set_ip_reg_IP2022 ≝
 267 λalu.λip':word16.
 268  mk_alu_IP2022
 269   (acc_low_reg_IP2022 alu)
 270   (mulh_reg_IP2022 alu)
 271   (addrsel_reg_IP2022 alu)
 272   (addr_array_IP2022 alu)
 273   (call_stack_IP2022 alu)
 274   ip'
 275   (dp_reg_IP2022 alu)
 276   (data_reg_IP2022 alu)
 277   (sp_reg_IP2022 alu)
 278   (pc_reg_IP2022 alu)
 279   (speed_reg_IP2022 alu)
 280   (page_reg_IP2022 alu)
 281   (h_flag_IP2022 alu)
 282   (z_flag_IP2022 alu)
 283   (c_flag_IP2022 alu)
 284   (skip_mode_IP2022 alu).
 285
 286 (* setter specifico IP2022 di DP *)
 287 ndefinition set_dp_reg_IP2022 ≝
 288 λalu.λdp':word16.
 289  mk_alu_IP2022
 290   (acc_low_reg_IP2022 alu)
 291   (mulh_reg_IP2022 alu)
 292   (addrsel_reg_IP2022 alu)
 293   (addr_array_IP2022 alu)
 294   (call_stack_IP2022 alu)
 295   (ip_reg_IP2022 alu)
 296   dp'
 297   (data_reg_IP2022 alu)
 298   (sp_reg_IP2022 alu)
 299   (pc_reg_IP2022 alu)
 300   (speed_reg_IP2022 alu)
 301   (page_reg_IP2022 alu)
 302   (h_flag_IP2022 alu)
 303   (z_flag_IP2022 alu)
 304   (c_flag_IP2022 alu)
 305   (skip_mode_IP2022 alu).
 306
 307 (* setter specifico IP2022 di DATA *)
 308 ndefinition set_data_reg_IP2022 ≝
 309 λalu.λdata':word16.
 310  mk_alu_IP2022
 311   (acc_low_reg_IP2022 alu)
 312   (mulh_reg_IP2022 alu)
 313   (addrsel_reg_IP2022 alu)
 314   (addr_array_IP2022 alu)
 315   (call_stack_IP2022 alu)
 316   (ip_reg_IP2022 alu)
 317   (dp_reg_IP2022 alu)
 318   data'
 319   (sp_reg_IP2022 alu)
 320   (pc_reg_IP2022 alu)
 321   (speed_reg_IP2022 alu)
 322   (page_reg_IP2022 alu)
 323   (h_flag_IP2022 alu)
 324   (z_flag_IP2022 alu)
 325   (c_flag_IP2022 alu)
 326   (skip_mode_IP2022 alu).
 327
 328 (* setter specifico IP2022 di SP *)
 329 ndefinition set_sp_reg_IP2022 ≝
 330 λalu.λsp':word16.
 331  mk_alu_IP2022
 332   (acc_low_reg_IP2022 alu)
 333   (mulh_reg_IP2022 alu)
 334   (addrsel_reg_IP2022 alu)
 335   (addr_array_IP2022 alu)
 336   (call_stack_IP2022 alu)
 337   (ip_reg_IP2022 alu)
 338   (dp_reg_IP2022 alu)
 339   (data_reg_IP2022 alu)
 340   sp'
 341   (pc_reg_IP2022 alu)
 342   (speed_reg_IP2022 alu)
 343   (page_reg_IP2022 alu)
 344   (h_flag_IP2022 alu)
 345   (z_flag_IP2022 alu)
 346   (c_flag_IP2022 alu)
 347   (skip_mode_IP2022 alu).
 348
 349 (* setter specifico IP2022 di PC *)
 350 ndefinition set_pc_reg_IP2022 ≝
 351 λalu.λpc':word16.
 352  mk_alu_IP2022
 353   (acc_low_reg_IP2022 alu)
 354   (mulh_reg_IP2022 alu)
 355   (addrsel_reg_IP2022 alu)
 356   (addr_array_IP2022 alu)
 357   (call_stack_IP2022 alu)
 358   (ip_reg_IP2022 alu)
 359   (dp_reg_IP2022 alu)
 360   (data_reg_IP2022 alu)
 361   (sp_reg_IP2022 alu)
 362   pc'
 363   (speed_reg_IP2022 alu)
 364   (page_reg_IP2022 alu)
 365   (h_flag_IP2022 alu)
 366   (z_flag_IP2022 alu)
 367   (c_flag_IP2022 alu)
 368   (skip_mode_IP2022 alu).
 369
 370 (* setter specifico IP2022 di SPEED *)
 371 ndefinition set_speed_reg_IP2022 ≝
 372 λalu.λspeed':exadecim.
 373  mk_alu_IP2022
 374   (acc_low_reg_IP2022 alu)
 375   (mulh_reg_IP2022 alu)
 376   (addrsel_reg_IP2022 alu)
 377   (addr_array_IP2022 alu)
 378   (call_stack_IP2022 alu)
 379   (ip_reg_IP2022 alu)
 380   (dp_reg_IP2022 alu)
 381   (data_reg_IP2022 alu)
 382   (sp_reg_IP2022 alu)
 383   (pc_reg_IP2022 alu)
 384   speed'
 385   (page_reg_IP2022 alu)
 386   (h_flag_IP2022 alu)
 387   (z_flag_IP2022 alu)
 388   (c_flag_IP2022 alu)
 389   (skip_mode_IP2022 alu).
 390
 391 (* setter specifico IP2022 di PAGE *)
 392 ndefinition set_page_reg_IP2022 ≝
 393 λalu.λpage':oct.
 394  mk_alu_IP2022
 395   (acc_low_reg_IP2022 alu)
 396   (mulh_reg_IP2022 alu)
 397   (addrsel_reg_IP2022 alu)
 398   (addr_array_IP2022 alu)
 399   (call_stack_IP2022 alu)
 400   (ip_reg_IP2022 alu)
 401   (dp_reg_IP2022 alu)
 402   (data_reg_IP2022 alu)
 403   (sp_reg_IP2022 alu)
 404   (pc_reg_IP2022 alu)
 405   (speed_reg_IP2022 alu)
 406   page'
 407   (h_flag_IP2022 alu)
 408   (z_flag_IP2022 alu)
 409   (c_flag_IP2022 alu)
 410   (skip_mode_IP2022 alu).
 411
 412 (* setter specifico IP2022 di H *)
 413 ndefinition set_h_flag_IP2022 ≝
 414 λalu.λhfl':bool.
 415  mk_alu_IP2022
 416   (acc_low_reg_IP2022 alu)
 417   (mulh_reg_IP2022 alu)
 418   (addrsel_reg_IP2022 alu)
 419   (addr_array_IP2022 alu)
 420   (call_stack_IP2022 alu)
 421   (ip_reg_IP2022 alu)
 422   (dp_reg_IP2022 alu)
 423   (data_reg_IP2022 alu)
 424   (sp_reg_IP2022 alu)
 425   (pc_reg_IP2022 alu)
 426   (speed_reg_IP2022 alu)
 427   (page_reg_IP2022 alu)
 428   hfl'
 429   (z_flag_IP2022 alu)
 430   (c_flag_IP2022 alu)
 431   (skip_mode_IP2022 alu).
 432
 433 (* setter specifico IP2022 di Z *)
 434 ndefinition set_z_flag_IP2022 ≝
 435 λalu.λzfl':bool.
 436  mk_alu_IP2022
 437   (acc_low_reg_IP2022 alu)
 438   (mulh_reg_IP2022 alu)
 439   (addrsel_reg_IP2022 alu)
 440   (addr_array_IP2022 alu)
 441   (call_stack_IP2022 alu)
 442   (ip_reg_IP2022 alu)
 443   (dp_reg_IP2022 alu)
 444   (data_reg_IP2022 alu)
 445   (sp_reg_IP2022 alu)
 446   (pc_reg_IP2022 alu)
 447   (speed_reg_IP2022 alu)
 448   (page_reg_IP2022 alu)
 449   (h_flag_IP2022 alu)
 450   zfl'
 451   (c_flag_IP2022 alu)
 452   (skip_mode_IP2022 alu).
 453
 454 (* setter specifico IP2022 di C *)
 455 ndefinition set_c_flag_IP2022 ≝
 456 λalu.λcfl':bool.
 457  mk_alu_IP2022
 458   (acc_low_reg_IP2022 alu)
 459   (mulh_reg_IP2022 alu)
 460   (addrsel_reg_IP2022 alu)
 461   (addr_array_IP2022 alu)
 462   (call_stack_IP2022 alu)
 463   (ip_reg_IP2022 alu)
 464   (dp_reg_IP2022 alu)
 465   (data_reg_IP2022 alu)
 466   (sp_reg_IP2022 alu)
 467   (pc_reg_IP2022 alu)
 468   (speed_reg_IP2022 alu)
 469   (page_reg_IP2022 alu)
 470   (h_flag_IP2022 alu)
 471   (z_flag_IP2022 alu)
 472   cfl'
 473   (skip_mode_IP2022 alu).
 474
 475 (* setter specifico IP2022 di SKIP *)
 476 ndefinition set_skip_mode_IP2022 ≝
 477 λalu.λskipmode':bool.
 478  mk_alu_IP2022
 479   (acc_low_reg_IP2022 alu)
 480   (mulh_reg_IP2022 alu)
 481   (addrsel_reg_IP2022 alu)
 482   (addr_array_IP2022 alu)
 483   (call_stack_IP2022 alu)
 484   (ip_reg_IP2022 alu)
 485   (dp_reg_IP2022 alu)
 486   (data_reg_IP2022 alu)
 487   (sp_reg_IP2022 alu)
 488   (pc_reg_IP2022 alu)
 489   (speed_reg_IP2022 alu)
 490   (page_reg_IP2022 alu)
 491   (h_flag_IP2022 alu)
 492   (z_flag_IP2022 alu)
 493   (c_flag_IP2022 alu)
 494   skipmode'.
 495
 496 (* ***************** *)
 497 (* CONFRONTO FRA ALU *)
 498 (* ***************** *)
 499
 500 (* confronto registro per registro dell'IP2022 *)
 501 ndefinition eq_IP2022_alu ≝
 502 λalu1,alu2:alu_IP2022.
 503  (eq_b8 (acc_low_reg_IP2022 alu1) (acc_low_reg_IP2022 alu2)) ⊗
 504  (eq_b8 (mulh_reg_IP2022 alu1) (mulh_reg_IP2022 alu2)) ⊗
 505  (eq_b8 (addrsel_reg_IP2022 alu1) (addrsel_reg_IP2022 alu2)) ⊗
 506  (eq_ar8 ? eq_w24 (addr_array_IP2022 alu1) (addr_array_IP2022 alu2)) ⊗
 507  (eq_ar16 ? eq_w16 (call_stack_IP2022 alu1) (call_stack_IP2022 alu2)) ⊗
 508  (eq_w16 (ip_reg_IP2022 alu1) (ip_reg_IP2022 alu2)) ⊗
 509  (eq_w16 (dp_reg_IP2022 alu1) (dp_reg_IP2022 alu2)) ⊗
 510  (eq_w16 (data_reg_IP2022 alu1) (data_reg_IP2022 alu2)) ⊗
 511  (eq_w16 (sp_reg_IP2022 alu1) (sp_reg_IP2022 alu2)) ⊗
 512  (eq_w16 (pc_reg_IP2022 alu1) (pc_reg_IP2022 alu2)) ⊗
 513  (eq_ex (speed_reg_IP2022 alu1) (speed_reg_IP2022 alu2)) ⊗
 514  (eq_oct (page_reg_IP2022 alu1) (page_reg_IP2022 alu2)) ⊗
 515  (eq_bool (h_flag_IP2022 alu1) (h_flag_IP2022 alu2)) ⊗
 516  (eq_bool (z_flag_IP2022 alu1) (z_flag_IP2022 alu2)) ⊗
 517  (eq_bool (c_flag_IP2022 alu1) (c_flag_IP2022 alu2)) ⊗
 518  (eq_bool (skip_mode_IP2022 alu1) (skip_mode_IP2022 alu2)).