matita/contribs/assembly/freescale/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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/memory_abs.ma".
  28
  29 (* *********************************** *)
  30 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  31 (* *********************************** *)
  32
  33 (* ALU dell'HC05 *)
  34 record alu_HC05: Type ≝
  35  {
  36  (* A: registo accumulatore *)
  37  acc_low_reg_HC05 : byte8;
  38  (* X: registro indice *)
  39  indX_low_reg_HC05 : byte8;
  40  (* SP: registo stack pointer *)
  41  sp_reg_HC05 : word16;
  42  (* modificatori di SP: per esempio e' definito come 0000000011xxxxxxb *)
  43  (* la logica della sua costruzione e' quindi (SP∧mask)∨fix *)
  44  (* totalmente racchiusa nella ALU, bastera' fare get(set(SP)) *)
  45  sp_mask_HC05 : word16;
  46  sp_fix_HC05 : word16;
  47  (* PC: registro program counter *)
  48  pc_reg_HC05 : word16;
  49  (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
  50  (* la logica della sua costruzione e' quindi (PC∧mask) *)
  51  (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
  52  pc_mask_HC05 : word16;
  53
  54  (* H: flag semi-carry (somma nibble basso) *)
  55  h_flag_HC05 : bool;
  56  (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
  57  i_flag_HC05 : bool;
  58  (* N: flag segno/negativita' *)
  59  n_flag_HC05 : bool;
  60  (* Z: flag zero *)
  61  z_flag_HC05 : bool;
  62  (* C: flag carry *)
  63  c_flag_HC05 : bool;
  64
  65  (* IRQ: flag che simula il pin esterno IRQ *)
  66  irq_flag_HC05 : bool
  67  }.
  68
  69 notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg' ≝ sp ; break 'Sp_Mask' ≝ spm ; break 'Sp_Fix' ≝ spf ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
  70  non associative with precedence 80 for
  71  @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
  72 interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
  73  (cic:/matita/freescale/status/alu_HC05.ind#xpointer(1/1/1) acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
  74
  75 (* ALU dell'HC08/HCS08 *)
  76 record alu_HC08: Type ≝
  77  {
  78  (* A: registo accumulatore *)
  79  acc_low_reg_HC08 : byte8;
  80  (* X: registro indice parte bassa *)
  81  indX_low_reg_HC08 : byte8;
  82  (* H: registro indice parte alta *)
  83  indX_high_reg_HC08 : byte8;
  84  (* SP: registo stack pointer *)
  85  sp_reg_HC08 : word16;
  86  (* PC: registro program counter *)
  87  pc_reg_HC08 : word16;
  88
  89  (* V: flag overflow *)
  90  v_flag_HC08 : bool;
  91  (* H: flag semi-carry (somma nibble basso) *)
  92  h_flag_HC08 : bool;
  93  (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
  94  i_flag_HC08 : bool;
  95  (* N: flag segno/negativita' *)
  96  n_flag_HC08 : bool;
  97  (* Z: flag zero *)
  98  z_flag_HC08 : bool;
  99  (* C: flag carry *)
 100  c_flag_HC08 : bool;
 101
 102  (* IRQ: flag che simula il pin esterno IRQ *)
 103  irq_flag_HC08 : bool
 104  }.
 105
 106 notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg' ≝ indxhigh ; break 'Sp_Reg' ≝ sp ; break 'Pc_Reg' ≝ pc ; break 'V_Flag' ≝ vfl ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
 107  non associative with precedence 80 for
 108  @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
 109 interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
 110  (cic:/matita/freescale/status/alu_HC08.ind#xpointer(1/1/1) acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
 111
 112 (* ALU dell'RS08 *)
 113 record alu_RS08: Type ≝
 114  {
 115  (* A: registo accumulatore *)
 116  acc_low_reg_RS08 : byte8;
 117  (* PC: registro program counter *)
 118  pc_reg_RS08 : word16;
 119  (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
 120  (* la logica della sua costruzione e' quindi (PC∧mask) *)
 121  (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
 122  pc_mask_RS08 : word16;
 123  (* SPC: registro shadow program counter *)
 124  (* NB: il suo modificatore e' lo stesso di PC *)
 125  spc_reg_RS08 : word16;
 126
 127  (* X: registro indice parte bassa *)
 128  (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
 129  (* la lettura/scrittura avviene tramite la locazione [0x000F] *)
 130  (* la funzione memory_filter_read/write si occupera' di intercettare *)
 131  (* e deviare sul registro le letture/scritture (modulo load_write) *)
 132  x_map_RS08 : byte8;
 133  (* PS: registro selezione di pagina *)
 134  (* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *)
 135  (* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *)
 136  (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
 137  (* la lettura/scrittura avviene tramite la locazione [0x001F] *)
 138  (* la funzione memory_filter_read/write si occupera' di intercettare *)
 139  (* e deviare sul registro le letture/scritture (modulo load_write) *)
 140  ps_map_RS08 : byte8;
 141
 142  (* Z: flag zero *)
 143  z_flag_RS08 : bool;
 144  (* C: flag carry *)
 145  c_flag_RS08 : bool
 146  }.
 147
 148 notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'Spc_Reg' ≝ spc ; break 'X_Map' ≝ xm ; break 'Ps_Map' ≝ psm ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl)}"
 149  non associative with precedence 80 for
 150  @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
 151 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
 152  (cic:/matita/freescale/status/alu_RS08.ind#xpointer(1/1/1) acclow pc pcm spc xm psm zfl cfl).
 153
 154 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
 155 record any_status (mcu:mcu_type) (t:memory_impl): Type ≝
 156  {
 157  alu : match mcu with
 158   [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ];
 159
 160  (* descritore della memoria *)
 161  mem_desc : aux_mem_type t;
 162  (* descrittore del tipo di memoria installata *)
 163  chk_desc : aux_chk_type t;
 164  (* descrittore del click = stato di avanzamento dell'esecuzione+cur_pc conseguente a fetch *)
 165  (* 1) None = istruzione eseguita, attesa del fetch *)
 166  (* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito, countup a esecuzione *)
 167  clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16)
 168  }.
 169
 170 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
 171 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
 172  for @{ 'mk_any_status $alu $mem $chk $clk }.
 173 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
 174  (cic:/matita/freescale/status/any_status.ind#xpointer(1/1/1) alu mem chk clk).
 175
 176 (* **************** *)
 177 (* GETTER SPECIFICI *)
 178 (* **************** *)
 179
 180 (* funzione ausiliaria per il tipaggio dei getter *)
 181 definition aux_get_typing ≝ λx:Type.λm:mcu_type.match m with
 182  [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] → x.
 183
 184 (* REGISTRI *)
 185
 186 (* getter di A, esiste sempre *)
 187 definition get_acc_8_low_reg ≝
 188 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 189  match m
 190   return aux_get_typing byte8 with
 191  [ HC05 ⇒ acc_low_reg_HC05
 192  | HC08 ⇒ acc_low_reg_HC08
 193  | HCS08 ⇒ acc_low_reg_HC08
 194  | RS08 ⇒ acc_low_reg_RS08 ]
 195  (alu m t s).
 196
 197 (* getter di X, non esiste sempre *)
 198 definition get_indX_8_low_reg ≝
 199 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 200  match m
 201   return aux_get_typing (option byte8) with
 202  [ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
 203  | HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
 204  | HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
 205  | RS08 ⇒ λalu.None ? ]
 206  (alu m t s).
 207
 208 (* getter di H, non esiste sempre *)
 209 definition get_indX_8_high_reg ≝
 210 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 211  match m
 212   return aux_get_typing (option byte8) with
 213  [ HC05 ⇒ λalu.None ?
 214  | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
 215  | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
 216  | RS08 ⇒ λalu.None ? ]
 217  (alu m t s).
 218
 219 (* getter di H:X, non esiste sempre *)
 220 definition get_indX_16_reg ≝
 221 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 222  match m
 223   return aux_get_typing (option word16) with
 224  [ HC05 ⇒ λalu.None ?
 225  | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
 226  | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
 227  | RS08 ⇒ λalu.None ? ]
 228  (alu m t s).
 229
 230 (* getter di SP, non esiste sempre *)
 231 definition get_sp_reg ≝
 232 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 233  match m
 234   return aux_get_typing (option word16) with
 235  [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
 236  | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
 237  | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
 238  | RS08 ⇒ λalu.None ? ]
 239  (alu m t s).
 240
 241 (* getter di PC, esiste sempre *)
 242 definition get_pc_reg ≝
 243 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 244  match m
 245   return aux_get_typing word16 with
 246  [ HC05 ⇒ pc_reg_HC05
 247  | HC08 ⇒ pc_reg_HC08
 248  | HCS08 ⇒ pc_reg_HC08
 249  | RS08 ⇒ pc_reg_RS08 ]
 250  (alu m t s).
 251
 252 (* getter di SPC, non esiste sempre *)
 253 definition get_spc_reg ≝
 254 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 255  match m
 256   return aux_get_typing (option word16) with
 257  [ HC05 ⇒ λalu.None ?
 258  | HC08 ⇒ λalu.None ?
 259  | HCS08 ⇒ λalu.None ?
 260  | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu) ]
 261  (alu m t s).
 262
 263 (* REGISTRI MEMORY MAPPED *)
 264
 265 (* getter di memory mapped X, non esiste sempre *)
 266 definition get_x_map ≝
 267 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 268  match m
 269   return aux_get_typing (option byte8) with
 270  [ HC05 ⇒ λalu.None ?
 271  | HC08 ⇒ λalu.None ?
 272  | HCS08 ⇒ λalu.None ?
 273  | RS08 ⇒ λalu.Some ? (x_map_RS08 alu) ]
 274  (alu m t s).
 275
 276 (* getter di memory mapped PS, non esiste sempre *)
 277 definition get_ps_map ≝
 278 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 279  match m
 280   return aux_get_typing (option byte8) with
 281  [ HC05 ⇒ λalu.None ?
 282  | HC08 ⇒ λalu.None ?
 283  | HCS08 ⇒ λalu.None ?
 284  | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu) ]
 285  (alu m t s).
 286
 287 (* FLAG *)
 288
 289 (* getter di V, non esiste sempre *)
 290 definition get_v_flag ≝
 291 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 292  match m
 293   return aux_get_typing (option bool) with
 294  [ HC05 ⇒ λalu.None ?
 295  | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
 296  | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
 297  | RS08 ⇒ λalu.None ? ]
 298  (alu m t s).
 299
 300 (* getter di H, non esiste sempre *)
 301 definition get_h_flag ≝
 302 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 303  match m
 304   return aux_get_typing (option bool) with
 305  [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
 306  | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
 307  | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
 308  | RS08 ⇒ λalu.None ? ]
 309  (alu m t s).
 310
 311 (* getter di I, non esiste sempre *)
 312 definition get_i_flag ≝
 313 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 314  match m
 315   return aux_get_typing (option bool) with
 316  [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
 317  | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
 318  | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
 319  | RS08 ⇒ λalu.None ? ]
 320  (alu m t s).
 321
 322 (* getter di N, non esiste sempre *)
 323 definition get_n_flag ≝
 324 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 325  match m
 326   return aux_get_typing (option bool) with
 327  [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
 328  | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
 329  | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
 330  | RS08 ⇒ λalu.None ? ]
 331  (alu m t s).
 332
 333 (* getter di Z, esiste sempre *)
 334 definition get_z_flag ≝
 335 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 336  match m
 337   return aux_get_typing bool with
 338  [ HC05 ⇒ z_flag_HC05
 339  | HC08 ⇒ z_flag_HC08
 340  | HCS08 ⇒ z_flag_HC08
 341  | RS08 ⇒ z_flag_RS08 ]
 342  (alu m t s).
 343
 344 (* getter di C, esiste sempre *)
 345 definition get_c_flag ≝
 346 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 347  match m
 348   return aux_get_typing bool with
 349  [ HC05 ⇒ c_flag_HC05
 350  | HC08 ⇒ c_flag_HC08
 351  | HCS08 ⇒ c_flag_HC08
 352  | RS08 ⇒ c_flag_RS08 ]
 353  (alu m t s).
 354
 355 (* getter di IRQ, non esiste sempre *)
 356 definition get_irq_flag ≝
 357 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 358  match m
 359   return aux_get_typing (option bool) with
 360  [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
 361  | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
 362  | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
 363  | RS08 ⇒ λalu.None ? ]
 364  (alu m t s).
 365
 366 (* DESCRITTORI ESTERNI ALLA ALU *)
 367
 368 (* getter della ALU, esiste sempre *)
 369 definition get_alu ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.alu m t s.
 370
 371 (* getter della memoria, esiste sempre *)
 372 definition get_mem_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.mem_desc m t s.
 373
 374 (* getter del descrittore, esiste sempre *)
 375 definition get_chk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.chk_desc m t s.
 376
 377 (* getter del clik, esiste sempre *)
 378 definition get_clk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.clk_desc m t s.
 379
 380 (* ***************************** *)
 381 (* SETTER SPECIFICI FORTI/DEBOLI *)
 382 (* ***************************** *)
 383
 384 (* funzione ausiliaria per il tipaggio dei setter forti *)
 385 definition aux_set_typing ≝ λx:Type.λm:mcu_type.
 386   match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
 387   → x →
 388   match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
 389
 390 (* funzione ausiliaria per il tipaggio dei setter deboli *)
 391 definition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option
 392  (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
 393   → x →
 394   match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]).
 395
 396 (* DESCRITTORI ESTERNI ALLA ALU *)
 397
 398 (* setter forte della ALU *)
 399 definition set_alu ≝
 400 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.match s with
 401  [ mk_any_status _ mem chk clk ⇒ mk_any_status m t alu' mem chk clk ].
 402
 403 (* setter forte della memoria *)
 404 definition set_mem_desc ≝
 405 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.match s with
 406  [ mk_any_status alu _ chk clk ⇒ mk_any_status m t alu mem' chk clk ].
 407
 408 (* setter forte del descrittore *)
 409 definition set_chk_desc ≝
 410 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.match s with
 411  [ mk_any_status alu mem _ clk ⇒ mk_any_status m t alu mem chk' clk ].
 412
 413 (* setter forte del clik *)
 414 definition set_clk_desc ≝
 415 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 416 λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).match s with
 417  [ mk_any_status alu mem chk _ ⇒ mk_any_status m t alu mem chk clk' ].
 418
 419 (* REGISTRO A *)
 420
 421 (* setter specifico HC05 di A *)
 422 definition set_acc_8_low_reg_HC05 ≝
 423 λalu.λacclow':byte8.match alu with
 424  [ mk_alu_HC05 _ indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
 425   mk_alu_HC05 acclow' indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
 426
 427 (* setter specifico HC08/HCS08 di A *)
 428 definition set_acc_8_low_reg_HC08 ≝
 429 λalu.λacclow':byte8.match alu with
 430  [ mk_alu_HC08 _ indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
 431   mk_alu_HC08 acclow' indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ].
 432
 433 (* setter specifico RS08 di A *)
 434 definition set_acc_8_low_reg_RS08 ≝
 435 λalu.λacclow':byte8.match alu with
 436  [ mk_alu_RS08 _ pc pcm spc xm psm zfl cfl ⇒
 437   mk_alu_RS08 acclow' pc pcm spc xm psm zfl cfl ].
 438
 439 (* setter forte di A *)
 440 definition set_acc_8_low_reg ≝
 441 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
 442  set_alu m t s
 443  (match m return aux_set_typing byte8 with
 444   [ HC05 ⇒ set_acc_8_low_reg_HC05
 445   | HC08 ⇒ set_acc_8_low_reg_HC08
 446   | HCS08 ⇒ set_acc_8_low_reg_HC08
 447   | RS08 ⇒ set_acc_8_low_reg_RS08
 448   ] (alu m t s) acclow').
 449
 450 (* REGISTRO X *)
 451
 452 (* setter specifico HC05 di X *)
 453 definition set_indX_8_low_reg_HC05 ≝
 454 λalu.λindxlow':byte8.match alu with
 455  [ mk_alu_HC05 acclow _ sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
 456   mk_alu_HC05 acclow indxlow' sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
 457
 458 (* setter specifico HC08/HCS08 di X *)
 459 definition set_indX_8_low_reg_HC08 ≝
 460 λalu.λindxlow':byte8.match alu with
 461  [ mk_alu_HC08 acclow _ indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
 462   mk_alu_HC08 acclow indxlow' indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ].
 463
 464 (* setter forte di X *)
 465 definition set_indX_8_low_reg ≝
 466 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
 467  opt_map ?? (match m return aux_set_typing_opt byte8 with
 468              [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
 469              | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
 470              | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
 471              | RS08 ⇒ None ? ])
 472  (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
 473
 474 (* setter debole di X *)
 475 definition setweak_indX_8_low_reg ≝
 476 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
 477  match set_indX_8_low_reg m t s indxlow' with
 478   [ None ⇒ s | Some s' ⇒ s' ].
 479
 480 (* REGISTRO H *)
 481
 482 (* setter specifico HC08/HCS08 di H *)
 483 definition set_indX_8_high_reg_HC08 ≝
 484 λalu.λindxhigh':byte8.match alu with
 485  [ mk_alu_HC08 acclow indxlow _ sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
 486   mk_alu_HC08 acclow indxlow indxhigh' sp pc vfl hfl ifl nfl zfl cfl irqfl ].
 487
 488 (* setter forte di H *)
 489 definition set_indX_8_high_reg ≝
 490 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
 491  opt_map ?? (match m return aux_set_typing_opt byte8 with
 492              [ HC05 ⇒ None ?
 493              | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
 494              | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
 495              | RS08 ⇒ None ? ])
 496  (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
 497
 498 (* setter debole di H *)
 499 definition setweak_indX_8_high_reg ≝
 500 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
 501  match set_indX_8_high_reg m t s indxhigh' with
 502   [ None ⇒ s | Some s' ⇒ s' ].
 503
 504 (* REGISTRO H:X *)
 505
 506 (* setter specifico HC08/HCS08 di H:X *)
 507 definition set_indX_16_reg_HC08 ≝
 508 λalu.λindx16:word16.match alu with
 509  [ mk_alu_HC08 acclow _ _ sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
 510   mk_alu_HC08 acclow (w16l indx16) (w16h indx16) sp pc vfl hfl ifl nfl zfl cfl irqfl ].
 511
 512 (* setter forte di H:X *)
 513 definition set_indX_16_reg ≝
 514 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
 515  opt_map ?? (match m return aux_set_typing_opt word16 with
 516              [ HC05 ⇒ None ?
 517              | HC08 ⇒ Some ? set_indX_16_reg_HC08
 518              | HCS08 ⇒ Some ? set_indX_16_reg_HC08
 519              | RS08 ⇒ None ? ])
 520  (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
 521
 522 (* setter debole di H:X *)
 523 definition setweak_indX_16_reg ≝
 524 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
 525  match set_indX_16_reg m t s indx16 with
 526   [ None ⇒ s | Some s' ⇒ s' ].
 527
 528 (* REGISTRO SP *)
 529
 530 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
 531 definition set_sp_reg_HC05 ≝
 532 λalu.λsp':word16.match alu with
 533  [ mk_alu_HC05 acclow indxlow _ spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
 534   mk_alu_HC05 acclow indxlow (or_w16 (and_w16 sp' spm) spf) spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
 535
 536 (* setter specifico HC08/HCS08 di SP *)
 537 definition set_sp_reg_HC08 ≝
 538 λalu.λsp':word16.match alu with
 539  [ mk_alu_HC08 acclow indxlow indxhigh _ pc vfl hfl ifl nfl zfl cfl irqfl ⇒
 540   mk_alu_HC08 acclow indxlow indxhigh sp' pc vfl hfl ifl nfl zfl cfl irqfl ].
 541
 542 (* setter forte di SP *)
 543 definition set_sp_reg ≝
 544 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
 545  opt_map ?? (match m return aux_set_typing_opt word16 with
 546              [ HC05 ⇒ Some ? set_sp_reg_HC05
 547              | HC08 ⇒ Some ? set_sp_reg_HC08
 548              | HCS08 ⇒ Some ? set_sp_reg_HC08
 549              | RS08 ⇒ None ? ])
 550  (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
 551
 552 (* setter debole di SP *)
 553 definition setweak_sp_reg ≝
 554 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
 555  match set_sp_reg m t s sp' with
 556   [ None ⇒ s | Some s' ⇒ s' ].
 557
 558 (* REGISTRO PC *)
 559
 560 (* setter specifico HC05 di PC, effettua PC∧mask *)
 561 definition set_pc_reg_HC05 ≝
 562 λalu.λpc':word16.match alu with
 563  [ mk_alu_HC05 acclow indxlow sp spm spf _ pcm hfl ifl nfl zfl cfl irqfl ⇒
 564   mk_alu_HC05 acclow indxlow sp spm spf (and_w16 pc' pcm) pcm hfl ifl nfl zfl cfl irqfl ].
 565
 566 (* setter specifico HC08/HCS08 di PC *)
 567 definition set_pc_reg_HC08 ≝
 568 λalu.λpc':word16.match alu with
 569  [ mk_alu_HC08 acclow indxlow indxhigh sp _ vfl hfl ifl nfl zfl cfl irqfl ⇒
 570   mk_alu_HC08 acclow indxlow indxhigh sp pc' vfl hfl ifl nfl zfl cfl irqfl ].
 571
 572 (* setter specifico RS08 di PC, effettua PC∧mask *)
 573 definition set_pc_reg_RS08 ≝
 574 λalu.λpc':word16.match alu with
 575  [ mk_alu_RS08 acclow _ pcm spc xm psm zfl cfl ⇒
 576   mk_alu_RS08 acclow (and_w16 pc' pcm) pcm spc xm psm zfl cfl ].
 577
 578 (* setter forte di PC *)
 579 definition set_pc_reg ≝
 580 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
 581  set_alu m t s
 582  (match m return aux_set_typing word16 with
 583   [ HC05 ⇒ set_pc_reg_HC05
 584   | HC08 ⇒ set_pc_reg_HC08
 585   | HCS08 ⇒ set_pc_reg_HC08
 586   | RS08 ⇒ set_pc_reg_RS08
 587   ] (alu m t s) pc').
 588
 589 (* REGISTRO SPC *)
 590
 591 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
 592 definition set_spc_reg_RS08 ≝
 593 λalu.λspc':word16.match alu with
 594  [ mk_alu_RS08 acclow pc pcm _ xm psm zfl cfl ⇒
 595   mk_alu_RS08 acclow pc pcm (and_w16 spc' pcm) xm psm zfl cfl ].
 596
 597 (* setter forte di SPC *)
 598 definition set_spc_reg ≝
 599 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
 600  opt_map ?? (match m return aux_set_typing_opt word16 with
 601              [ HC05 ⇒ None ?
 602              | HC08 ⇒ None ?
 603              | HCS08 ⇒ None ?
 604              | RS08 ⇒ Some ? set_spc_reg_RS08 ])
 605  (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
 606
 607 (* setter debole di SPC *)
 608 definition setweak_spc_reg ≝
 609 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
 610  match set_spc_reg m t s spc' with
 611   [ None ⇒ s | Some s' ⇒ s' ].
 612
 613 (* REGISTRO MEMORY MAPPED X *)
 614
 615 (* setter specifico RS08 di memory mapped X *)
 616 definition set_x_map_RS08 ≝
 617 λalu.λxm':byte8.match alu with
 618  [ mk_alu_RS08 acclow pc pcm spc _ psm zfl cfl ⇒
 619   mk_alu_RS08 acclow pc pcm spc xm' psm zfl cfl ].
 620
 621 (* setter forte di memory mapped X *)
 622 definition set_x_map ≝
 623 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
 624  opt_map ?? (match m return aux_set_typing_opt byte8 with
 625              [ HC05 ⇒ None ?
 626              | HC08 ⇒ None ?
 627              | HCS08 ⇒ None ?
 628              | RS08 ⇒ Some ? set_x_map_RS08 ])
 629  (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
 630
 631 (* setter debole di memory mapped X *)
 632 definition setweak_x_map ≝
 633 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
 634  match set_x_map m t s xm' with
 635   [ None ⇒ s | Some s' ⇒ s' ].
 636
 637 (* REGISTRO MEMORY MAPPED PS *)
 638
 639 (* setter specifico RS08 di memory mapped PS *)
 640 definition set_ps_map_RS08 ≝
 641 λalu.λpsm':byte8.match alu with
 642  [ mk_alu_RS08 acclow pc pcm spc xm _ zfl cfl ⇒
 643   mk_alu_RS08 acclow pc pcm spc xm psm' zfl cfl ].
 644
 645 (* setter forte di memory mapped PS *)
 646 definition set_ps_map ≝
 647 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
 648  opt_map ?? (match m return aux_set_typing_opt byte8 with
 649              [ HC05 ⇒ None ?
 650              | HC08 ⇒ None ?
 651              | HCS08 ⇒ None ?
 652              | RS08 ⇒ Some ? set_ps_map_RS08 ])
 653  (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
 654
 655 (* setter debole di memory mapped PS *)
 656 definition setweak_ps_map ≝
 657 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
 658  match set_ps_map m t s psm' with
 659   [ None ⇒ s | Some s' ⇒ s' ].
 660
 661 (* FLAG V *)
 662
 663 (* setter specifico HC08/HCS08 di V *)
 664 definition set_v_flag_HC08 ≝
 665 λalu.λvfl':bool.match alu with
 666  [ mk_alu_HC08 acclow indxlow indxhigh sp pc _ hfl ifl nfl zfl cfl irqfl ⇒
 667   mk_alu_HC08 acclow indxlow indxhigh sp pc vfl' hfl ifl nfl zfl cfl irqfl ].
 668
 669 (* setter forte di V *)
 670 definition set_v_flag ≝
 671 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
 672  opt_map ?? (match m return aux_set_typing_opt bool with
 673              [ HC05 ⇒ None ?
 674              | HC08 ⇒ Some ? set_v_flag_HC08
 675              | HCS08 ⇒ Some ? set_v_flag_HC08
 676              | RS08 ⇒ None ? ])
 677  (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
 678
 679 (* setter debole  di V *)
 680 definition setweak_v_flag ≝
 681 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
 682  match set_v_flag m t s vfl' with
 683   [ None ⇒ s | Some s' ⇒ s' ].
 684
 685 (* FLAG H *)
 686
 687 (* setter specifico HC05 di H *)
 688 definition set_h_flag_HC05 ≝
 689 λalu.λhfl':bool.match alu with
 690  [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm _ ifl nfl zfl cfl irqfl ⇒
 691   mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl' ifl nfl zfl cfl irqfl ].
 692
 693 (* setter specifico HC08/HCS08 di H *)
 694 definition set_h_flag_HC08 ≝
 695 λalu.λhfl':bool.match alu with
 696  [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl _ ifl nfl zfl cfl irqfl ⇒
 697   mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl' ifl nfl zfl cfl irqfl ].
 698
 699 (* setter forte di H *)
 700 definition set_h_flag ≝
 701 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
 702  opt_map ?? (match m return aux_set_typing_opt bool with
 703              [ HC05 ⇒ Some ? set_h_flag_HC05
 704              | HC08 ⇒ Some ? set_h_flag_HC08
 705              | HCS08 ⇒ Some ? set_h_flag_HC08
 706              | RS08 ⇒ None ? ])
 707  (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
 708
 709 (* setter debole di H *)
 710 definition setweak_h_flag ≝
 711 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
 712  match set_h_flag m t s hfl' with
 713   [ None ⇒ s | Some s' ⇒ s' ].
 714
 715 (* FLAG I *)
 716
 717 (* setter specifico HC05 di I *)
 718 definition set_i_flag_HC05 ≝
 719 λalu.λifl':bool.match alu with
 720  [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl _ nfl zfl cfl irqfl ⇒
 721   mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl' nfl zfl cfl irqfl ].
 722
 723 (* setter specifico HC08/HCS08 di I *)
 724 definition set_i_flag_HC08 ≝
 725 λalu.λifl':bool.match alu with
 726  [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl _ nfl zfl cfl irqfl ⇒
 727   mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl' nfl zfl cfl irqfl ].
 728
 729 (* setter forte di I *)
 730 definition set_i_flag ≝
 731 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
 732  opt_map ?? (match m return aux_set_typing_opt bool with
 733              [ HC05 ⇒ Some ? set_i_flag_HC05
 734              | HC08 ⇒ Some ? set_i_flag_HC08
 735              | HCS08 ⇒ Some ? set_i_flag_HC08
 736              | RS08 ⇒ None ? ])
 737  (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
 738
 739 (* setter debole di I *)
 740 definition setweak_i_flag ≝
 741 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
 742  match set_i_flag m t s ifl' with
 743   [ None ⇒ s | Some s' ⇒ s' ].
 744
 745 (* FLAG N *)
 746
 747 (* setter specifico HC05 di N *)
 748 definition set_n_flag_HC05 ≝
 749 λalu.λnfl':bool.match alu with
 750  [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl _ zfl cfl irqfl ⇒
 751   mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl' zfl cfl irqfl ].
 752
 753 (* setter specifico HC08/HCS08 di N *)
 754 definition set_n_flag_HC08 ≝
 755 λalu.λnfl':bool.match alu with
 756  [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl _ zfl cfl irqfl ⇒
 757   mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl' zfl cfl irqfl ].
 758
 759 (* setter forte di N *)
 760 definition set_n_flag ≝
 761 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
 762  opt_map ?? (match m return aux_set_typing_opt bool with
 763              [ HC05 ⇒ Some ? set_n_flag_HC05
 764              | HC08 ⇒ Some ? set_n_flag_HC08
 765              | HCS08 ⇒ Some ? set_n_flag_HC08
 766              | RS08 ⇒ None ? ])
 767  (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
 768
 769 (* setter debole di N *)
 770 definition setweak_n_flag ≝
 771 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
 772  match set_n_flag m t s nfl' with
 773   [ None ⇒ s | Some s' ⇒ s' ].
 774
 775 (* FLAG Z *)
 776
 777 (* setter specifico HC05 di Z *)
 778 definition set_z_flag_HC05 ≝
 779 λalu.λzfl':bool.match alu with
 780  [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl _ cfl irqfl ⇒
 781   mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl' cfl irqfl ].
 782
 783 (* setter specifico HC08/HCS08 di Z *)
 784 definition set_z_flag_HC08 ≝
 785 λalu.λzfl':bool.match alu with
 786  [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl _ cfl irqfl ⇒
 787   mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl' cfl irqfl ].
 788
 789 (* setter sprcifico RS08 di Z *)
 790 definition set_z_flag_RS08 ≝
 791 λalu.λzfl':bool.match alu with
 792  [ mk_alu_RS08 acclow pc pcm spc xm psm _ cfl ⇒
 793   mk_alu_RS08 acclow pc pcm spc xm psm zfl' cfl ].
 794
 795 (* setter forte di Z *)
 796 definition set_z_flag ≝
 797 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
 798  set_alu m t s
 799  (match m return aux_set_typing bool with
 800   [ HC05 ⇒ set_z_flag_HC05
 801   | HC08 ⇒ set_z_flag_HC08
 802   | HCS08 ⇒ set_z_flag_HC08
 803   | RS08 ⇒ set_z_flag_RS08
 804   ] (alu m t s) zfl').
 805
 806 (* FLAG C *)
 807
 808 (* setter specifico HC05 di C *)
 809 definition set_c_flag_HC05 ≝
 810 λalu.λcfl':bool.match alu with
 811  [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl _ irqfl ⇒
 812   mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl' irqfl ].
 813
 814 (* setter specifico HC08/HCS08 di C *)
 815 definition set_c_flag_HC08 ≝
 816 λalu.λcfl':bool.match alu with
 817  [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl _ irqfl ⇒
 818   mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl' irqfl ].
 819
 820 (* setter specifico RS08 di C *)
 821 definition set_c_flag_RS08 ≝
 822 λalu.λcfl':bool.match alu with
 823  [ mk_alu_RS08 acclow pc pcm spc xm psm zfl _ ⇒
 824   mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl' ].
 825
 826 (* setter forte di C *)
 827 definition set_c_flag ≝
 828 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
 829  set_alu m t s
 830  (match m return aux_set_typing bool with
 831   [ HC05 ⇒ set_c_flag_HC05
 832   | HC08 ⇒ set_c_flag_HC08
 833   | HCS08 ⇒ set_c_flag_HC08
 834   | RS08 ⇒ set_c_flag_RS08
 835   ] (alu m t s) cfl').
 836
 837 (* FLAG IRQ *)
 838
 839 (* setter specifico HC05 di IRQ *)
 840 definition set_irq_flag_HC05 ≝
 841 λalu.λirqfl':bool.match alu with
 842  [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl _ ⇒
 843   mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl' ].
 844
 845 (* setter specifico HC08/HCS08 di IRQ *)
 846 definition set_irq_flag_HC08 ≝
 847 λalu.λirqfl':bool.match alu with
 848  [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl _ ⇒
 849   mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl' ].
 850
 851 (* setter forte di IRQ *)
 852 definition set_irq_flag ≝
 853 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
 854  opt_map ?? (match m return aux_set_typing_opt bool with
 855              [ HC05 ⇒ Some ? set_irq_flag_HC05
 856              | HC08 ⇒ Some ? set_irq_flag_HC08
 857              | HCS08 ⇒ Some ? set_irq_flag_HC08
 858              | RS08 ⇒ None ? ])
 859  (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
 860
 861 (* setter debole di IRQ *)
 862 definition setweak_irq_flag ≝
 863 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
 864  match set_irq_flag m t s irqfl' with
 865   [ None ⇒ s | Some s' ⇒ s' ].
 866
 867 (* ***************** *)
 868 (* CONFRONTO FRA ALU *)
 869 (* ***************** *)
 870
 871 (* confronto registro per registro dell'HC05 *)
 872 definition eq_alu_HC05 ≝
 873 λalu1,alu2:alu_HC05.
 874  match alu1 with
 875   [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
 876  match alu2 with
 877   [ mk_alu_HC05 acclow2 indxlow2 sp2 spm2 spf2 pc2 pcm2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
 878    (eq_b8 acclow1 acclow2) ⊗
 879    (eq_b8 indxlow1 indxlow2) ⊗
 880    (eq_w16 sp1 sp2) ⊗
 881    (eq_w16 spm1 spm2) ⊗
 882    (eq_w16 spf1 spf2) ⊗
 883    (eq_w16 pc1 pc2) ⊗
 884    (eq_w16 pcm1 pcm2) ⊗
 885    (eq_bool hfl1 hfl2) ⊗
 886    (eq_bool ifl1 ifl2) ⊗
 887    (eq_bool nfl1 nfl2) ⊗
 888    (eq_bool zfl1 zfl2) ⊗
 889    (eq_bool cfl1 cfl2) ⊗
 890    (eq_bool irqfl1 irqfl2) ]].
 891
 892 (* confronto registro per registro dell'HC08 *)
 893 definition eq_alu_HC08 ≝
 894 λalu1,alu2:alu_HC08.
 895  match alu1 with
 896   [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
 897  match alu2 with
 898   [ mk_alu_HC08 acclow2 indxlow2 indxhigh2 sp2 pc2 vfl2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
 899    (eq_b8 acclow1 acclow2) ⊗
 900    (eq_b8 indxlow1 indxlow2) ⊗
 901    (eq_b8 indxhigh1 indxhigh2) ⊗
 902    (eq_w16 sp1 sp2) ⊗
 903    (eq_w16 pc1 pc2) ⊗
 904    (eq_bool vfl1 vfl2) ⊗
 905    (eq_bool hfl1 hfl2) ⊗
 906    (eq_bool ifl1 ifl2) ⊗
 907    (eq_bool nfl1 nfl2) ⊗
 908    (eq_bool zfl1 zfl2) ⊗
 909    (eq_bool cfl1 cfl2) ⊗
 910    (eq_bool irqfl1 irqfl2) ]].
 911
 912 (* confronto registro per registro dell'RS08 *)
 913 definition eq_alu_RS08 ≝
 914 λalu1,alu2:alu_RS08.
 915  match alu1 with
 916   [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
 917  match alu2 with
 918   [ mk_alu_RS08 acclow2 pc2 pcm2 spc2 xm2 psm2 zfl2 cfl2 ⇒
 919    (eq_b8 acclow1 acclow2) ⊗
 920    (eq_w16 pc1 pc2) ⊗
 921    (eq_w16 pcm1 pcm2) ⊗
 922    (eq_w16 spc1 spc2) ⊗
 923    (eq_b8 xm1 xm2) ⊗
 924    (eq_b8 psm1 psm2) ⊗
 925    (eq_bool zfl1 zfl2) ⊗
 926    (eq_bool cfl1 cfl2) ]].
 927
 928 (* ******************** *)
 929 (* CONFRONTO FRA STATUS *)
 930 (* ******************** *)
 931
 932 (* la lettura da memoria ritorna un option byte8, quindi bisogna poterli confrontare *)
 933 definition eq_b8_opt ≝
 934 λb1,b2:option byte8.
 935  match b1 with
 936   [ None ⇒ match b2 with
 937    [ None ⇒ true | Some _ ⇒ false ]
 938   | Some b1' ⇒ match b2 with
 939    [ None ⇒ false | Some b2' ⇒ eq_b8 b1' b2' ]
 940   ].
 941
 942 (* confronto di una regione di memoria [inf,inf+n] *)
 943 let rec forall_memory_ranged
 944  (t:memory_impl)
 945  (chk1:aux_chk_type t) (chk2:aux_chk_type t)
 946  (mem1:aux_mem_type t) (mem2:aux_mem_type t)
 947  (inf:word16) (n:nat) on n ≝
 948  match n return λ_.bool with
 949   [ O ⇒ eq_b8_opt (mem_read t mem1 chk1 inf) (mem_read t mem2 chk2 inf)
 950   | S n' ⇒ (eq_b8_opt (mem_read t mem1 chk1 (plus_w16nc inf (word16_of_nat n)))
 951                       (mem_read t mem2 chk2 (plus_w16nc inf (word16_of_nat n)))) ⊗
 952            (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n')
 953   ].
 954
 955 (* il clk e' option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16) *)
 956 definition eq_clk ≝
 957 λm:mcu_type.λc1,c2:option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
 958  match c1 with
 959   [ None ⇒ match c2 with
 960    [ None ⇒ true | Some _ ⇒ false ]
 961   | Some c1' ⇒ match c2 with
 962    [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T ????? c1') (fst5T ????? c2')) ⊗
 963                                (eqop m (snd5T ????? c1') (snd5T ????? c2')) ⊗
 964                                (eqim (thd5T ????? c1') (thd5T ????? c2')) ⊗
 965                                (eq_b8 (frth5T ????? c1') (frth5T ????? c2')) ⊗
 966                                (eq_w16 (ffth5T ????? c1') (ffth5T ????? c2')) ]
 967   ].
 968
 969 (* generalizzazione del confronto fra stati *)
 970 definition eq_status ≝
 971 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λinf:word16.λn:nat.
 972  match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
 973  match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
 974
 975  (* 1) confronto della ALU *)
 976  (match m return λm:mcu_type.
 977    match m with
 978     [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
 979    match m with
 980     [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
 981    bool with
 982   [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ]
 983  alu1 alu2) ⊗
 984
 985  (* 2) confronto della memoria in [inf,inf+n] *)
 986  (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n) ⊗
 987
 988  (* 3) confronto del clik *)
 989  (eq_clk m clk1 clk2)
 990  ]].
 991
 992 (* assioma da applicare per l'uguaglianza degli stati *)
 993 axiom eq_status_axiom :
 994 ∀inf:word16.∀n:nat.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
 995  (eq_status m t s1 s2 inf n = true) →
 996  s1 = s2.