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_addrarray ≝
  70 λaddrsel:byte8.λaa:aux_addrarray_type.
  71  getn_array8T (oct_of_exL (cnL ? addrsel)) ? aa.
  72
  73 ndefinition set_addrarray ≝
  74 λaddrsel:byte8.λaa:aux_addrarray_type.λv.
  75  setn_array8T (oct_of_exL (cnL ? addrsel)) ? aa v.
  76
  77 (* *********************************** *)
  78 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  79 (* *********************************** *)
  80
  81 (* ALU dell'IP2022 *)
  82 nrecord alu_IP2022: Type ≝
  83  {
  84  (* W: accumulatore *)
  85  acc_low_reg_IP2022 : byte8;
  86  (* MULH: parte alta moltiplicazione *)
  87  mulh_reg_IP2022 : byte8;
  88
  89  (* ADDRSEL: selettore di indirizzo *)
  90  addrsel_reg_IP2022 : byte8;
  91  (* ADDR [ADDRX|ADDRH|ADDRL] : array indirizzi indicizzati da ADDRSEL *)
  92  addr_array_IP2022 : aux_addrarray_type;
  93
  94  (* CALL [CALLH|CALLL] : stack indirizzi di ritorno *)
  95  call_stack_IP2022 : aux_callstack_type;
  96
  97  (* IP [IPH|IPL] : indirect pointer *)
  98  ip_reg_IP2022 : word16;
  99  (* DP [DPH|DPL] : data pointer *)
 100  dp_reg_IP2022 : word16;
 101  (* DATA [DATAH|DATAL] : data value *)
 102  data_reg_IP2022 : word16;
 103  (* SP [SPH|SPL] : stack pointer *)
 104  sp_reg_IP2022 : word16;
 105  (* PC [PCH|PCL] : program counter *)
 106  pc_reg_IP2022 : word16;
 107
 108  (* SPEED[xxxxSSSS] : divisore del clock *)
 109  speed_reg_IP2022 : exadecim;
 110  (* PAGE [PPPxxxxx] : selettore pagina *)
 111  page_reg_IP2022 : oct;
 112
 113  (* H: flag semi-carry (somma nibble basso) *)
 114  h_flag_IP2022 : bool;
 115  (* Z: flag zero *)
 116  z_flag_IP2022 : bool;
 117  (* C: flag carry *)
 118  c_flag_IP2022 : bool;
 119
 120  (* skip mode : effettua fetch-decode, no execute *)
 121  skip_mode_IP2022 : bool
 122  }.
 123
 124 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)}"
 125  non associative with precedence 80 for
 126  @{ 'mk_alu_IP2022 $w $mulh $addrsel $addr $call $ip $dp $data $sp $pc $speed $page $hfl $zfl $cfl $skipmode }.
 127 interpretation "mk_alu_IP2022" 'mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode =
 128  (mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode).
 129
 130 (* ****** *)
 131 (* SETTER *)
 132 (* ****** *)
 133
 134 (* setter specifico IP2022 di A *)
 135 ndefinition set_acc_8_low_reg_IP2022 ≝
 136 λalu.λacclow':byte8.
 137  mk_alu_IP2022
 138   acclow'
 139   (mulh_reg_IP2022 alu)
 140   (addrsel_reg_IP2022 alu)
 141   (addr_array_IP2022 alu)
 142   (call_stack_IP2022 alu)
 143   (ip_reg_IP2022 alu)
 144   (dp_reg_IP2022 alu)
 145   (data_reg_IP2022 alu)
 146   (sp_reg_IP2022 alu)
 147   (pc_reg_IP2022 alu)
 148   (speed_reg_IP2022 alu)
 149   (page_reg_IP2022 alu)
 150   (h_flag_IP2022 alu)
 151   (z_flag_IP2022 alu)
 152   (c_flag_IP2022 alu)
 153   (skip_mode_IP2022 alu).
 154
 155 (* setter specifico IP2022 di MULH *)
 156 ndefinition set_mulh_reg_IP2022 ≝
 157 λalu.λmulh':byte8.
 158  mk_alu_IP2022
 159   (acc_low_reg_IP2022 alu)
 160   mulh'
 161   (addrsel_reg_IP2022 alu)
 162   (addr_array_IP2022 alu)
 163   (call_stack_IP2022 alu)
 164   (ip_reg_IP2022 alu)
 165   (dp_reg_IP2022 alu)
 166   (data_reg_IP2022 alu)
 167   (sp_reg_IP2022 alu)
 168   (pc_reg_IP2022 alu)
 169   (speed_reg_IP2022 alu)
 170   (page_reg_IP2022 alu)
 171   (h_flag_IP2022 alu)
 172   (z_flag_IP2022 alu)
 173   (c_flag_IP2022 alu)
 174   (skip_mode_IP2022 alu).
 175
 176 (* setter specifico IP2022 di ADDRSEL *)
 177 ndefinition set_addrsel_reg_IP2022 ≝
 178 λalu.λaddrsel':byte8.
 179  mk_alu_IP2022
 180   (acc_low_reg_IP2022 alu)
 181   (mulh_reg_IP2022 alu)
 182   addrsel'
 183   (addr_array_IP2022 alu)
 184   (call_stack_IP2022 alu)
 185   (ip_reg_IP2022 alu)
 186   (dp_reg_IP2022 alu)
 187   (data_reg_IP2022 alu)
 188   (sp_reg_IP2022 alu)
 189   (pc_reg_IP2022 alu)
 190   (speed_reg_IP2022 alu)
 191   (page_reg_IP2022 alu)
 192   (h_flag_IP2022 alu)
 193   (z_flag_IP2022 alu)
 194   (c_flag_IP2022 alu)
 195   (skip_mode_IP2022 alu).
 196
 197 (* setter specifico IP2022 di ADDR *)
 198 ndefinition set_addr_reg_IP2022 ≝
 199 λalu.λaddr':word24.
 200  mk_alu_IP2022
 201   (acc_low_reg_IP2022 alu)
 202   (mulh_reg_IP2022 alu)
 203   (addrsel_reg_IP2022 alu)
 204   (set_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu) addr')
 205   (call_stack_IP2022 alu)
 206   (ip_reg_IP2022 alu)
 207   (dp_reg_IP2022 alu)
 208   (data_reg_IP2022 alu)
 209   (sp_reg_IP2022 alu)
 210   (pc_reg_IP2022 alu)
 211   (speed_reg_IP2022 alu)
 212   (page_reg_IP2022 alu)
 213   (h_flag_IP2022 alu)
 214   (z_flag_IP2022 alu)
 215   (c_flag_IP2022 alu)
 216   (skip_mode_IP2022 alu).
 217
 218 (* setter specifico IP2022 di CALL *)
 219 ndefinition set_call_reg_IP2022 ≝
 220 λalu.λcall':word16.
 221  mk_alu_IP2022
 222   (acc_low_reg_IP2022 alu)
 223   (mulh_reg_IP2022 alu)
 224   (addrsel_reg_IP2022 alu)
 225   (addr_array_IP2022 alu)
 226   (setn_array16T x0 ? (call_stack_IP2022 alu) call')
 227   (ip_reg_IP2022 alu)
 228   (dp_reg_IP2022 alu)
 229   (data_reg_IP2022 alu)
 230   (sp_reg_IP2022 alu)
 231   (pc_reg_IP2022 alu)
 232   (speed_reg_IP2022 alu)
 233   (page_reg_IP2022 alu)
 234   (h_flag_IP2022 alu)
 235   (z_flag_IP2022 alu)
 236   (c_flag_IP2022 alu)
 237   (skip_mode_IP2022 alu).
 238
 239 ndefinition push_call_reg_IP2022 ≝
 240 λalu.λcall':word16.
 241  mk_alu_IP2022
 242   (acc_low_reg_IP2022 alu)
 243   (mulh_reg_IP2022 alu)
 244   (addrsel_reg_IP2022 alu)
 245   (addr_array_IP2022 alu)
 246   (push_callstack (call_stack_IP2022 alu) call')
 247   (ip_reg_IP2022 alu)
 248   (dp_reg_IP2022 alu)
 249   (data_reg_IP2022 alu)
 250   (sp_reg_IP2022 alu)
 251   (pc_reg_IP2022 alu)
 252   (speed_reg_IP2022 alu)
 253   (page_reg_IP2022 alu)
 254   (h_flag_IP2022 alu)
 255   (z_flag_IP2022 alu)
 256   (c_flag_IP2022 alu)
 257   (skip_mode_IP2022 alu).
 258
 259 ndefinition pop_call_reg_IP2022 ≝
 260 λalu.
 261  match pop_callstack (call_stack_IP2022 alu) with
 262   [ pair val call' ⇒
 263  pair … val
 264         (mk_alu_IP2022
 265          (acc_low_reg_IP2022 alu)
 266          (mulh_reg_IP2022 alu)
 267          (addrsel_reg_IP2022 alu)
 268          (addr_array_IP2022 alu)
 269          call'
 270          (ip_reg_IP2022 alu)
 271          (dp_reg_IP2022 alu)
 272          (data_reg_IP2022 alu)
 273          (sp_reg_IP2022 alu)
 274          (pc_reg_IP2022 alu)
 275          (speed_reg_IP2022 alu)
 276          (page_reg_IP2022 alu)
 277          (h_flag_IP2022 alu)
 278          (z_flag_IP2022 alu)
 279          (c_flag_IP2022 alu)
 280          (skip_mode_IP2022 alu)) ].
 281
 282 (* setter specifico IP2022 di IP *)
 283 ndefinition set_ip_reg_IP2022 ≝
 284 λalu.λip':word16.
 285  mk_alu_IP2022
 286   (acc_low_reg_IP2022 alu)
 287   (mulh_reg_IP2022 alu)
 288   (addrsel_reg_IP2022 alu)
 289   (addr_array_IP2022 alu)
 290   (call_stack_IP2022 alu)
 291   ip'
 292   (dp_reg_IP2022 alu)
 293   (data_reg_IP2022 alu)
 294   (sp_reg_IP2022 alu)
 295   (pc_reg_IP2022 alu)
 296   (speed_reg_IP2022 alu)
 297   (page_reg_IP2022 alu)
 298   (h_flag_IP2022 alu)
 299   (z_flag_IP2022 alu)
 300   (c_flag_IP2022 alu)
 301   (skip_mode_IP2022 alu).
 302
 303 (* setter specifico IP2022 di DP *)
 304 ndefinition set_dp_reg_IP2022 ≝
 305 λalu.λdp':word16.
 306  mk_alu_IP2022
 307   (acc_low_reg_IP2022 alu)
 308   (mulh_reg_IP2022 alu)
 309   (addrsel_reg_IP2022 alu)
 310   (addr_array_IP2022 alu)
 311   (call_stack_IP2022 alu)
 312   (ip_reg_IP2022 alu)
 313   dp'
 314   (data_reg_IP2022 alu)
 315   (sp_reg_IP2022 alu)
 316   (pc_reg_IP2022 alu)
 317   (speed_reg_IP2022 alu)
 318   (page_reg_IP2022 alu)
 319   (h_flag_IP2022 alu)
 320   (z_flag_IP2022 alu)
 321   (c_flag_IP2022 alu)
 322   (skip_mode_IP2022 alu).
 323
 324 (* setter specifico IP2022 di DATA *)
 325 ndefinition set_data_reg_IP2022 ≝
 326 λalu.λdata':word16.
 327  mk_alu_IP2022
 328   (acc_low_reg_IP2022 alu)
 329   (mulh_reg_IP2022 alu)
 330   (addrsel_reg_IP2022 alu)
 331   (addr_array_IP2022 alu)
 332   (call_stack_IP2022 alu)
 333   (ip_reg_IP2022 alu)
 334   (dp_reg_IP2022 alu)
 335   data'
 336   (sp_reg_IP2022 alu)
 337   (pc_reg_IP2022 alu)
 338   (speed_reg_IP2022 alu)
 339   (page_reg_IP2022 alu)
 340   (h_flag_IP2022 alu)
 341   (z_flag_IP2022 alu)
 342   (c_flag_IP2022 alu)
 343   (skip_mode_IP2022 alu).
 344
 345 (* setter specifico IP2022 di SP *)
 346 ndefinition set_sp_reg_IP2022 ≝
 347 λalu.λsp':word16.
 348  mk_alu_IP2022
 349   (acc_low_reg_IP2022 alu)
 350   (mulh_reg_IP2022 alu)
 351   (addrsel_reg_IP2022 alu)
 352   (addr_array_IP2022 alu)
 353   (call_stack_IP2022 alu)
 354   (ip_reg_IP2022 alu)
 355   (dp_reg_IP2022 alu)
 356   (data_reg_IP2022 alu)
 357   sp'
 358   (pc_reg_IP2022 alu)
 359   (speed_reg_IP2022 alu)
 360   (page_reg_IP2022 alu)
 361   (h_flag_IP2022 alu)
 362   (z_flag_IP2022 alu)
 363   (c_flag_IP2022 alu)
 364   (skip_mode_IP2022 alu).
 365
 366 (* setter specifico IP2022 di PC *)
 367 ndefinition set_pc_reg_IP2022 ≝
 368 λalu.λpc':word16.
 369  mk_alu_IP2022
 370   (acc_low_reg_IP2022 alu)
 371   (mulh_reg_IP2022 alu)
 372   (addrsel_reg_IP2022 alu)
 373   (addr_array_IP2022 alu)
 374   (call_stack_IP2022 alu)
 375   (ip_reg_IP2022 alu)
 376   (dp_reg_IP2022 alu)
 377   (data_reg_IP2022 alu)
 378   (sp_reg_IP2022 alu)
 379   pc'
 380   (speed_reg_IP2022 alu)
 381   (page_reg_IP2022 alu)
 382   (h_flag_IP2022 alu)
 383   (z_flag_IP2022 alu)
 384   (c_flag_IP2022 alu)
 385   (skip_mode_IP2022 alu).
 386
 387 (* setter specifico IP2022 di SPEED *)
 388 ndefinition set_speed_reg_IP2022 ≝
 389 λalu.λspeed':exadecim.
 390  mk_alu_IP2022
 391   (acc_low_reg_IP2022 alu)
 392   (mulh_reg_IP2022 alu)
 393   (addrsel_reg_IP2022 alu)
 394   (addr_array_IP2022 alu)
 395   (call_stack_IP2022 alu)
 396   (ip_reg_IP2022 alu)
 397   (dp_reg_IP2022 alu)
 398   (data_reg_IP2022 alu)
 399   (sp_reg_IP2022 alu)
 400   (pc_reg_IP2022 alu)
 401   speed'
 402   (page_reg_IP2022 alu)
 403   (h_flag_IP2022 alu)
 404   (z_flag_IP2022 alu)
 405   (c_flag_IP2022 alu)
 406   (skip_mode_IP2022 alu).
 407
 408 (* setter specifico IP2022 di PAGE *)
 409 ndefinition set_page_reg_IP2022 ≝
 410 λalu.λpage':oct.
 411  mk_alu_IP2022
 412   (acc_low_reg_IP2022 alu)
 413   (mulh_reg_IP2022 alu)
 414   (addrsel_reg_IP2022 alu)
 415   (addr_array_IP2022 alu)
 416   (call_stack_IP2022 alu)
 417   (ip_reg_IP2022 alu)
 418   (dp_reg_IP2022 alu)
 419   (data_reg_IP2022 alu)
 420   (sp_reg_IP2022 alu)
 421   (pc_reg_IP2022 alu)
 422   (speed_reg_IP2022 alu)
 423   page'
 424   (h_flag_IP2022 alu)
 425   (z_flag_IP2022 alu)
 426   (c_flag_IP2022 alu)
 427   (skip_mode_IP2022 alu).
 428
 429 (* setter specifico IP2022 di H *)
 430 ndefinition set_h_flag_IP2022 ≝
 431 λalu.λhfl':bool.
 432  mk_alu_IP2022
 433   (acc_low_reg_IP2022 alu)
 434   (mulh_reg_IP2022 alu)
 435   (addrsel_reg_IP2022 alu)
 436   (addr_array_IP2022 alu)
 437   (call_stack_IP2022 alu)
 438   (ip_reg_IP2022 alu)
 439   (dp_reg_IP2022 alu)
 440   (data_reg_IP2022 alu)
 441   (sp_reg_IP2022 alu)
 442   (pc_reg_IP2022 alu)
 443   (speed_reg_IP2022 alu)
 444   (page_reg_IP2022 alu)
 445   hfl'
 446   (z_flag_IP2022 alu)
 447   (c_flag_IP2022 alu)
 448   (skip_mode_IP2022 alu).
 449
 450 (* setter specifico IP2022 di Z *)
 451 ndefinition set_z_flag_IP2022 ≝
 452 λalu.λzfl':bool.
 453  mk_alu_IP2022
 454   (acc_low_reg_IP2022 alu)
 455   (mulh_reg_IP2022 alu)
 456   (addrsel_reg_IP2022 alu)
 457   (addr_array_IP2022 alu)
 458   (call_stack_IP2022 alu)
 459   (ip_reg_IP2022 alu)
 460   (dp_reg_IP2022 alu)
 461   (data_reg_IP2022 alu)
 462   (sp_reg_IP2022 alu)
 463   (pc_reg_IP2022 alu)
 464   (speed_reg_IP2022 alu)
 465   (page_reg_IP2022 alu)
 466   (h_flag_IP2022 alu)
 467   zfl'
 468   (c_flag_IP2022 alu)
 469   (skip_mode_IP2022 alu).
 470
 471 (* setter specifico IP2022 di C *)
 472 ndefinition set_c_flag_IP2022 ≝
 473 λalu.λcfl':bool.
 474  mk_alu_IP2022
 475   (acc_low_reg_IP2022 alu)
 476   (mulh_reg_IP2022 alu)
 477   (addrsel_reg_IP2022 alu)
 478   (addr_array_IP2022 alu)
 479   (call_stack_IP2022 alu)
 480   (ip_reg_IP2022 alu)
 481   (dp_reg_IP2022 alu)
 482   (data_reg_IP2022 alu)
 483   (sp_reg_IP2022 alu)
 484   (pc_reg_IP2022 alu)
 485   (speed_reg_IP2022 alu)
 486   (page_reg_IP2022 alu)
 487   (h_flag_IP2022 alu)
 488   (z_flag_IP2022 alu)
 489   cfl'
 490   (skip_mode_IP2022 alu).
 491
 492 (* setter specifico IP2022 di SKIP *)
 493 ndefinition set_skip_mode_IP2022 ≝
 494 λalu.λskipmode':bool.
 495  mk_alu_IP2022
 496   (acc_low_reg_IP2022 alu)
 497   (mulh_reg_IP2022 alu)
 498   (addrsel_reg_IP2022 alu)
 499   (addr_array_IP2022 alu)
 500   (call_stack_IP2022 alu)
 501   (ip_reg_IP2022 alu)
 502   (dp_reg_IP2022 alu)
 503   (data_reg_IP2022 alu)
 504   (sp_reg_IP2022 alu)
 505   (pc_reg_IP2022 alu)
 506   (speed_reg_IP2022 alu)
 507   (page_reg_IP2022 alu)
 508   (h_flag_IP2022 alu)
 509   (z_flag_IP2022 alu)
 510   (c_flag_IP2022 alu)
 511   skipmode'.
 512
 513 (* ***************** *)
 514 (* CONFRONTO FRA ALU *)
 515 (* ***************** *)
 516
 517 (* confronto registro per registro dell'IP2022 *)
 518 ndefinition eq_IP2022_alu ≝
 519 λalu1,alu2:alu_IP2022.
 520  (eq_b8 (acc_low_reg_IP2022 alu1) (acc_low_reg_IP2022 alu2)) ⊗
 521  (eq_b8 (mulh_reg_IP2022 alu1) (mulh_reg_IP2022 alu2)) ⊗
 522  (eq_b8 (addrsel_reg_IP2022 alu1) (addrsel_reg_IP2022 alu2)) ⊗
 523  (eq_ar8 ? eq_w24 (addr_array_IP2022 alu1) (addr_array_IP2022 alu2)) ⊗
 524  (eq_ar16 ? eq_w16 (call_stack_IP2022 alu1) (call_stack_IP2022 alu2)) ⊗
 525  (eq_w16 (ip_reg_IP2022 alu1) (ip_reg_IP2022 alu2)) ⊗
 526  (eq_w16 (dp_reg_IP2022 alu1) (dp_reg_IP2022 alu2)) ⊗
 527  (eq_w16 (data_reg_IP2022 alu1) (data_reg_IP2022 alu2)) ⊗
 528  (eq_w16 (sp_reg_IP2022 alu1) (sp_reg_IP2022 alu2)) ⊗
 529  (eq_w16 (pc_reg_IP2022 alu1) (pc_reg_IP2022 alu2)) ⊗
 530  (eq_ex (speed_reg_IP2022 alu1) (speed_reg_IP2022 alu2)) ⊗
 531  (eq_oct (page_reg_IP2022 alu1) (page_reg_IP2022 alu2)) ⊗
 532  (eq_bool (h_flag_IP2022 alu1) (h_flag_IP2022 alu2)) ⊗
 533  (eq_bool (z_flag_IP2022 alu1) (z_flag_IP2022 alu2)) ⊗
 534  (eq_bool (c_flag_IP2022 alu1) (c_flag_IP2022 alu2)) ⊗
 535  (eq_bool (skip_mode_IP2022 alu1) (skip_mode_IP2022 alu2)).