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