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