matitaB/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 ndefinition get_addr_reg_IP2022 ≝
 219 λalu.get_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu).
 220
 221 (* setter specifico IP2022 di CALL *)
 222 ndefinition set_call_reg_IP2022 ≝
 223 λalu.λcall':word16.
 224  mk_alu_IP2022
 225   (acc_low_reg_IP2022 alu)
 226   (mulh_reg_IP2022 alu)
 227   (addrsel_reg_IP2022 alu)
 228   (addr_array_IP2022 alu)
 229   (setn_array16T x0 ? (call_stack_IP2022 alu) call')
 230   (ip_reg_IP2022 alu)
 231   (dp_reg_IP2022 alu)
 232   (data_reg_IP2022 alu)
 233   (sp_reg_IP2022 alu)
 234   (pc_reg_IP2022 alu)
 235   (speed_reg_IP2022 alu)
 236   (page_reg_IP2022 alu)
 237   (h_flag_IP2022 alu)
 238   (z_flag_IP2022 alu)
 239   (c_flag_IP2022 alu)
 240   (skip_mode_IP2022 alu).
 241
 242 ndefinition get_call_reg_IP2022 ≝
 243 λalu.getn_array16T x0 ? (call_stack_IP2022 alu).
 244
 245 ndefinition set_call_stack_IP2022 ≝
 246 λalu.λcall':aux_callstack_type.
 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   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 ndefinition push_call_reg_IP2022 ≝
 266 λalu.λcall':word16.
 267  mk_alu_IP2022
 268   (acc_low_reg_IP2022 alu)
 269   (mulh_reg_IP2022 alu)
 270   (addrsel_reg_IP2022 alu)
 271   (addr_array_IP2022 alu)
 272   (push_callstack (call_stack_IP2022 alu) call')
 273   (ip_reg_IP2022 alu)
 274   (dp_reg_IP2022 alu)
 275   (data_reg_IP2022 alu)
 276   (sp_reg_IP2022 alu)
 277   (pc_reg_IP2022 alu)
 278   (speed_reg_IP2022 alu)
 279   (page_reg_IP2022 alu)
 280   (h_flag_IP2022 alu)
 281   (z_flag_IP2022 alu)
 282   (c_flag_IP2022 alu)
 283   (skip_mode_IP2022 alu).
 284
 285 ndefinition pop_call_reg_IP2022 ≝
 286 λalu.match pop_callstack (call_stack_IP2022 alu) with
 287       [ pair val call' ⇒ pair … val (set_call_stack_IP2022 alu call') ].
 288
 289 (* setter specifico IP2022 di IP *)
 290 ndefinition set_ip_reg_IP2022 ≝
 291 λalu.λip':word16.
 292  mk_alu_IP2022
 293   (acc_low_reg_IP2022 alu)
 294   (mulh_reg_IP2022 alu)
 295   (addrsel_reg_IP2022 alu)
 296   (addr_array_IP2022 alu)
 297   (call_stack_IP2022 alu)
 298   ip'
 299   (dp_reg_IP2022 alu)
 300   (data_reg_IP2022 alu)
 301   (sp_reg_IP2022 alu)
 302   (pc_reg_IP2022 alu)
 303   (speed_reg_IP2022 alu)
 304   (page_reg_IP2022 alu)
 305   (h_flag_IP2022 alu)
 306   (z_flag_IP2022 alu)
 307   (c_flag_IP2022 alu)
 308   (skip_mode_IP2022 alu).
 309
 310 (* setter specifico IP2022 di DP *)
 311 ndefinition set_dp_reg_IP2022 ≝
 312 λalu.λdp':word16.
 313  mk_alu_IP2022
 314   (acc_low_reg_IP2022 alu)
 315   (mulh_reg_IP2022 alu)
 316   (addrsel_reg_IP2022 alu)
 317   (addr_array_IP2022 alu)
 318   (call_stack_IP2022 alu)
 319   (ip_reg_IP2022 alu)
 320   dp'
 321   (data_reg_IP2022 alu)
 322   (sp_reg_IP2022 alu)
 323   (pc_reg_IP2022 alu)
 324   (speed_reg_IP2022 alu)
 325   (page_reg_IP2022 alu)
 326   (h_flag_IP2022 alu)
 327   (z_flag_IP2022 alu)
 328   (c_flag_IP2022 alu)
 329   (skip_mode_IP2022 alu).
 330
 331 (* setter specifico IP2022 di DATA *)
 332 ndefinition set_data_reg_IP2022 ≝
 333 λalu.λdata':word16.
 334  mk_alu_IP2022
 335   (acc_low_reg_IP2022 alu)
 336   (mulh_reg_IP2022 alu)
 337   (addrsel_reg_IP2022 alu)
 338   (addr_array_IP2022 alu)
 339   (call_stack_IP2022 alu)
 340   (ip_reg_IP2022 alu)
 341   (dp_reg_IP2022 alu)
 342   data'
 343   (sp_reg_IP2022 alu)
 344   (pc_reg_IP2022 alu)
 345   (speed_reg_IP2022 alu)
 346   (page_reg_IP2022 alu)
 347   (h_flag_IP2022 alu)
 348   (z_flag_IP2022 alu)
 349   (c_flag_IP2022 alu)
 350   (skip_mode_IP2022 alu).
 351
 352 (* setter specifico IP2022 di SP *)
 353 ndefinition set_sp_reg_IP2022 ≝
 354 λalu.λsp':word16.
 355  mk_alu_IP2022
 356   (acc_low_reg_IP2022 alu)
 357   (mulh_reg_IP2022 alu)
 358   (addrsel_reg_IP2022 alu)
 359   (addr_array_IP2022 alu)
 360   (call_stack_IP2022 alu)
 361   (ip_reg_IP2022 alu)
 362   (dp_reg_IP2022 alu)
 363   (data_reg_IP2022 alu)
 364   sp'
 365   (pc_reg_IP2022 alu)
 366   (speed_reg_IP2022 alu)
 367   (page_reg_IP2022 alu)
 368   (h_flag_IP2022 alu)
 369   (z_flag_IP2022 alu)
 370   (c_flag_IP2022 alu)
 371   (skip_mode_IP2022 alu).
 372
 373 (* setter specifico IP2022 di PC *)
 374 ndefinition set_pc_reg_IP2022 ≝
 375 λalu.λpc':word16.
 376  mk_alu_IP2022
 377   (acc_low_reg_IP2022 alu)
 378   (mulh_reg_IP2022 alu)
 379   (addrsel_reg_IP2022 alu)
 380   (addr_array_IP2022 alu)
 381   (call_stack_IP2022 alu)
 382   (ip_reg_IP2022 alu)
 383   (dp_reg_IP2022 alu)
 384   (data_reg_IP2022 alu)
 385   (sp_reg_IP2022 alu)
 386   pc'
 387   (speed_reg_IP2022 alu)
 388   (page_reg_IP2022 alu)
 389   (h_flag_IP2022 alu)
 390   (z_flag_IP2022 alu)
 391   (c_flag_IP2022 alu)
 392   (skip_mode_IP2022 alu).
 393
 394 (* setter specifico IP2022 di SPEED *)
 395 ndefinition set_speed_reg_IP2022 ≝
 396 λalu.λspeed':exadecim.
 397  mk_alu_IP2022
 398   (acc_low_reg_IP2022 alu)
 399   (mulh_reg_IP2022 alu)
 400   (addrsel_reg_IP2022 alu)
 401   (addr_array_IP2022 alu)
 402   (call_stack_IP2022 alu)
 403   (ip_reg_IP2022 alu)
 404   (dp_reg_IP2022 alu)
 405   (data_reg_IP2022 alu)
 406   (sp_reg_IP2022 alu)
 407   (pc_reg_IP2022 alu)
 408   speed'
 409   (page_reg_IP2022 alu)
 410   (h_flag_IP2022 alu)
 411   (z_flag_IP2022 alu)
 412   (c_flag_IP2022 alu)
 413   (skip_mode_IP2022 alu).
 414
 415 (* setter specifico IP2022 di PAGE *)
 416 ndefinition set_page_reg_IP2022 ≝
 417 λalu.λpage':oct.
 418  mk_alu_IP2022
 419   (acc_low_reg_IP2022 alu)
 420   (mulh_reg_IP2022 alu)
 421   (addrsel_reg_IP2022 alu)
 422   (addr_array_IP2022 alu)
 423   (call_stack_IP2022 alu)
 424   (ip_reg_IP2022 alu)
 425   (dp_reg_IP2022 alu)
 426   (data_reg_IP2022 alu)
 427   (sp_reg_IP2022 alu)
 428   (pc_reg_IP2022 alu)
 429   (speed_reg_IP2022 alu)
 430   page'
 431   (h_flag_IP2022 alu)
 432   (z_flag_IP2022 alu)
 433   (c_flag_IP2022 alu)
 434   (skip_mode_IP2022 alu).
 435
 436 (* setter specifico IP2022 di H *)
 437 ndefinition set_h_flag_IP2022 ≝
 438 λalu.λhfl':bool.
 439  mk_alu_IP2022
 440   (acc_low_reg_IP2022 alu)
 441   (mulh_reg_IP2022 alu)
 442   (addrsel_reg_IP2022 alu)
 443   (addr_array_IP2022 alu)
 444   (call_stack_IP2022 alu)
 445   (ip_reg_IP2022 alu)
 446   (dp_reg_IP2022 alu)
 447   (data_reg_IP2022 alu)
 448   (sp_reg_IP2022 alu)
 449   (pc_reg_IP2022 alu)
 450   (speed_reg_IP2022 alu)
 451   (page_reg_IP2022 alu)
 452   hfl'
 453   (z_flag_IP2022 alu)
 454   (c_flag_IP2022 alu)
 455   (skip_mode_IP2022 alu).
 456
 457 (* setter specifico IP2022 di Z *)
 458 ndefinition set_z_flag_IP2022 ≝
 459 λalu.λzfl':bool.
 460  mk_alu_IP2022
 461   (acc_low_reg_IP2022 alu)
 462   (mulh_reg_IP2022 alu)
 463   (addrsel_reg_IP2022 alu)
 464   (addr_array_IP2022 alu)
 465   (call_stack_IP2022 alu)
 466   (ip_reg_IP2022 alu)
 467   (dp_reg_IP2022 alu)
 468   (data_reg_IP2022 alu)
 469   (sp_reg_IP2022 alu)
 470   (pc_reg_IP2022 alu)
 471   (speed_reg_IP2022 alu)
 472   (page_reg_IP2022 alu)
 473   (h_flag_IP2022 alu)
 474   zfl'
 475   (c_flag_IP2022 alu)
 476   (skip_mode_IP2022 alu).
 477
 478 (* setter specifico IP2022 di C *)
 479 ndefinition set_c_flag_IP2022 ≝
 480 λalu.λcfl':bool.
 481  mk_alu_IP2022
 482   (acc_low_reg_IP2022 alu)
 483   (mulh_reg_IP2022 alu)
 484   (addrsel_reg_IP2022 alu)
 485   (addr_array_IP2022 alu)
 486   (call_stack_IP2022 alu)
 487   (ip_reg_IP2022 alu)
 488   (dp_reg_IP2022 alu)
 489   (data_reg_IP2022 alu)
 490   (sp_reg_IP2022 alu)
 491   (pc_reg_IP2022 alu)
 492   (speed_reg_IP2022 alu)
 493   (page_reg_IP2022 alu)
 494   (h_flag_IP2022 alu)
 495   (z_flag_IP2022 alu)
 496   cfl'
 497   (skip_mode_IP2022 alu).
 498
 499 (* setter specifico IP2022 di SKIP *)
 500 ndefinition set_skip_mode_IP2022 ≝
 501 λalu.λskipmode':bool.
 502  mk_alu_IP2022
 503   (acc_low_reg_IP2022 alu)
 504   (mulh_reg_IP2022 alu)
 505   (addrsel_reg_IP2022 alu)
 506   (addr_array_IP2022 alu)
 507   (call_stack_IP2022 alu)
 508   (ip_reg_IP2022 alu)
 509   (dp_reg_IP2022 alu)
 510   (data_reg_IP2022 alu)
 511   (sp_reg_IP2022 alu)
 512   (pc_reg_IP2022 alu)
 513   (speed_reg_IP2022 alu)
 514   (page_reg_IP2022 alu)
 515   (h_flag_IP2022 alu)
 516   (z_flag_IP2022 alu)
 517   (c_flag_IP2022 alu)
 518   skipmode'.
 519
 520 (* ***************** *)
 521 (* CONFRONTO FRA ALU *)
 522 (* ***************** *)
 523
 524 (* confronto registro per registro dell'IP2022 *)
 525 ndefinition eq_IP2022_alu ≝
 526 λalu1,alu2:alu_IP2022.
 527  (eq_b8 (acc_low_reg_IP2022 alu1) (acc_low_reg_IP2022 alu2)) ⊗
 528  (eq_b8 (mulh_reg_IP2022 alu1) (mulh_reg_IP2022 alu2)) ⊗
 529  (eq_b8 (addrsel_reg_IP2022 alu1) (addrsel_reg_IP2022 alu2)) ⊗
 530  (eq_ar8 ? eq_w24 (addr_array_IP2022 alu1) (addr_array_IP2022 alu2)) ⊗
 531  (eq_ar16 ? eq_w16 (call_stack_IP2022 alu1) (call_stack_IP2022 alu2)) ⊗
 532  (eq_w16 (ip_reg_IP2022 alu1) (ip_reg_IP2022 alu2)) ⊗
 533  (eq_w16 (dp_reg_IP2022 alu1) (dp_reg_IP2022 alu2)) ⊗
 534  (eq_w16 (data_reg_IP2022 alu1) (data_reg_IP2022 alu2)) ⊗
 535  (eq_w16 (sp_reg_IP2022 alu1) (sp_reg_IP2022 alu2)) ⊗
 536  (eq_w16 (pc_reg_IP2022 alu1) (pc_reg_IP2022 alu2)) ⊗
 537  (eq_ex (speed_reg_IP2022 alu1) (speed_reg_IP2022 alu2)) ⊗
 538  (eq_oct (page_reg_IP2022 alu1) (page_reg_IP2022 alu2)) ⊗
 539  (eq_bool (h_flag_IP2022 alu1) (h_flag_IP2022 alu2)) ⊗
 540  (eq_bool (z_flag_IP2022 alu1) (z_flag_IP2022 alu2)) ⊗
 541  (eq_bool (c_flag_IP2022 alu1) (c_flag_IP2022 alu2)) ⊗
 542  (eq_bool (skip_mode_IP2022 alu1) (skip_mode_IP2022 alu2)).