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