helm/software/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  (mk_alu_HC05 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  (mk_alu_HC08 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  (mk_alu_RS08 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  (mk_any_status 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'.
 401  mk_any_status m t alu' (get_mem_desc m t s) (get_chk_desc m t s) (get_clk_desc m t s).
 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.
 406  mk_any_status m t (get_alu m t s) mem' (get_chk_desc m t s) (get_clk_desc m t s).
 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.
 411  mk_any_status m t (get_alu m t s) (get_mem_desc m t s) chk' (get_clk_desc m t s).
 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).
 417  mk_any_status m t (get_alu m t s) (get_mem_desc m t s) (get_chk_desc m t s) clk'.
 418
 419 (* REGISTRO A *)
 420
 421 (* setter specifico HC05 di A *)
 422 definition set_acc_8_low_reg_HC05 ≝
 423 λalu.λacclow':byte8.
 424  mk_alu_HC05
 425   acclow'
 426   (indX_low_reg_HC05 alu)
 427   (sp_reg_HC05 alu)
 428   (sp_mask_HC05 alu)
 429   (sp_fix_HC05 alu)
 430   (pc_reg_HC05 alu)
 431   (pc_mask_HC05 alu)
 432   (h_flag_HC05 alu)
 433   (i_flag_HC05 alu)
 434   (n_flag_HC05 alu)
 435   (z_flag_HC05 alu)
 436   (c_flag_HC05 alu)
 437   (irq_flag_HC05 alu).
 438
 439 (* setter specifico HC08/HCS08 di A *)
 440 definition set_acc_8_low_reg_HC08 ≝
 441 λalu.λacclow':byte8.
 442  mk_alu_HC08
 443   acclow'
 444   (indX_low_reg_HC08 alu)
 445   (indX_high_reg_HC08 alu)
 446   (sp_reg_HC08 alu)
 447   (pc_reg_HC08 alu)
 448   (v_flag_HC08 alu)
 449   (h_flag_HC08 alu)
 450   (i_flag_HC08 alu)
 451   (n_flag_HC08 alu)
 452   (z_flag_HC08 alu)
 453   (c_flag_HC08 alu)
 454   (irq_flag_HC08 alu).
 455
 456 (* setter specifico RS08 di A *)
 457 definition set_acc_8_low_reg_RS08 ≝
 458 λalu.λacclow':byte8.
 459  mk_alu_RS08
 460   acclow'
 461   (pc_reg_RS08 alu)
 462   (pc_mask_RS08 alu)
 463   (spc_reg_RS08 alu)
 464   (x_map_RS08 alu)
 465   (ps_map_RS08 alu)
 466   (z_flag_RS08 alu)
 467   (c_flag_RS08 alu).
 468
 469 (* setter forte di A *)
 470 definition set_acc_8_low_reg ≝
 471 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
 472  set_alu m t s
 473  (match m return aux_set_typing byte8 with
 474   [ HC05 ⇒ set_acc_8_low_reg_HC05
 475   | HC08 ⇒ set_acc_8_low_reg_HC08
 476   | HCS08 ⇒ set_acc_8_low_reg_HC08
 477   | RS08 ⇒ set_acc_8_low_reg_RS08
 478   ] (alu m t s) acclow').
 479
 480 (* REGISTRO X *)
 481
 482 (* setter specifico HC05 di X *)
 483 definition set_indX_8_low_reg_HC05 ≝
 484 λalu.λindxlow':byte8.
 485  mk_alu_HC05
 486   (acc_low_reg_HC05 alu)
 487   indxlow'
 488   (sp_reg_HC05 alu)
 489   (sp_mask_HC05 alu)
 490   (sp_fix_HC05 alu)
 491   (pc_reg_HC05 alu)
 492   (pc_mask_HC05 alu)
 493   (h_flag_HC05 alu)
 494   (i_flag_HC05 alu)
 495   (n_flag_HC05 alu)
 496   (z_flag_HC05 alu)
 497   (c_flag_HC05 alu)
 498   (irq_flag_HC05 alu).
 499
 500 (* setter specifico HC08/HCS08 di X *)
 501 definition set_indX_8_low_reg_HC08 ≝
 502 λalu.λindxlow':byte8.
 503  mk_alu_HC08
 504   (acc_low_reg_HC08 alu)
 505   indxlow'
 506   (indX_high_reg_HC08 alu)
 507   (sp_reg_HC08 alu)
 508   (pc_reg_HC08 alu)
 509   (v_flag_HC08 alu)
 510   (h_flag_HC08 alu)
 511   (i_flag_HC08 alu)
 512   (n_flag_HC08 alu)
 513   (z_flag_HC08 alu)
 514   (c_flag_HC08 alu)
 515   (irq_flag_HC08 alu).
 516
 517 (* setter forte di X *)
 518 definition set_indX_8_low_reg ≝
 519 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
 520  opt_map ?? (match m return aux_set_typing_opt byte8 with
 521              [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
 522              | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
 523              | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
 524              | RS08 ⇒ None ? ])
 525  (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
 526
 527 (* setter debole di X *)
 528 definition setweak_indX_8_low_reg ≝
 529 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
 530  match set_indX_8_low_reg m t s indxlow' with
 531   [ None ⇒ s | Some s' ⇒ s' ].
 532
 533 (* REGISTRO H *)
 534
 535 (* setter specifico HC08/HCS08 di H *)
 536 definition set_indX_8_high_reg_HC08 ≝
 537 λalu.λindxhigh':byte8.
 538  mk_alu_HC08
 539   (acc_low_reg_HC08 alu)
 540   (indX_low_reg_HC08 alu)
 541   indxhigh'
 542   (sp_reg_HC08 alu)
 543   (pc_reg_HC08 alu)
 544   (v_flag_HC08 alu)
 545   (h_flag_HC08 alu)
 546   (i_flag_HC08 alu)
 547   (n_flag_HC08 alu)
 548   (z_flag_HC08 alu)
 549   (c_flag_HC08 alu)
 550   (irq_flag_HC08 alu).
 551
 552 (* setter forte di H *)
 553 definition set_indX_8_high_reg ≝
 554 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
 555  opt_map ?? (match m return aux_set_typing_opt byte8 with
 556              [ HC05 ⇒ None ?
 557              | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
 558              | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
 559              | RS08 ⇒ None ? ])
 560  (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
 561
 562 (* setter debole di H *)
 563 definition setweak_indX_8_high_reg ≝
 564 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
 565  match set_indX_8_high_reg m t s indxhigh' with
 566   [ None ⇒ s | Some s' ⇒ s' ].
 567
 568 (* REGISTRO H:X *)
 569
 570 (* setter specifico HC08/HCS08 di H:X *)
 571 definition set_indX_16_reg_HC08 ≝
 572 λalu.λindx16:word16.
 573  mk_alu_HC08
 574   (acc_low_reg_HC08 alu)
 575   (w16l indx16)
 576   (w16h indx16)
 577   (sp_reg_HC08 alu)
 578   (pc_reg_HC08 alu)
 579   (v_flag_HC08 alu)
 580   (h_flag_HC08 alu)
 581   (i_flag_HC08 alu)
 582   (n_flag_HC08 alu)
 583   (z_flag_HC08 alu)
 584   (c_flag_HC08 alu)
 585   (irq_flag_HC08 alu).
 586
 587 (* setter forte di H:X *)
 588 definition set_indX_16_reg ≝
 589 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
 590  opt_map ?? (match m return aux_set_typing_opt word16 with
 591              [ HC05 ⇒ None ?
 592              | HC08 ⇒ Some ? set_indX_16_reg_HC08
 593              | HCS08 ⇒ Some ? set_indX_16_reg_HC08
 594              | RS08 ⇒ None ? ])
 595  (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
 596
 597 (* setter debole di H:X *)
 598 definition setweak_indX_16_reg ≝
 599 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
 600  match set_indX_16_reg m t s indx16 with
 601   [ None ⇒ s | Some s' ⇒ s' ].
 602
 603 (* REGISTRO SP *)
 604
 605 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
 606 definition set_sp_reg_HC05 ≝
 607 λalu.λsp':word16.
 608  mk_alu_HC05
 609   (acc_low_reg_HC05 alu)
 610   (indX_low_reg_HC05 alu)
 611   (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
 612   (sp_mask_HC05 alu)
 613   (sp_fix_HC05 alu)
 614   (pc_reg_HC05 alu)
 615   (pc_mask_HC05 alu)
 616   (h_flag_HC05 alu)
 617   (i_flag_HC05 alu)
 618   (n_flag_HC05 alu)
 619   (z_flag_HC05 alu)
 620   (c_flag_HC05 alu)
 621   (irq_flag_HC05 alu).
 622
 623 (* setter specifico HC08/HCS08 di SP *)
 624 definition set_sp_reg_HC08 ≝
 625 λalu.λsp':word16.
 626  mk_alu_HC08
 627   (acc_low_reg_HC08 alu)
 628   (indX_low_reg_HC08 alu)
 629   (indX_high_reg_HC08 alu)
 630   sp'
 631   (pc_reg_HC08 alu)
 632   (v_flag_HC08 alu)
 633   (h_flag_HC08 alu)
 634   (i_flag_HC08 alu)
 635   (n_flag_HC08 alu)
 636   (z_flag_HC08 alu)
 637   (c_flag_HC08 alu)
 638   (irq_flag_HC08 alu).
 639
 640 (* setter forte di SP *)
 641 definition set_sp_reg ≝
 642 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
 643  opt_map ?? (match m return aux_set_typing_opt word16 with
 644              [ HC05 ⇒ Some ? set_sp_reg_HC05
 645              | HC08 ⇒ Some ? set_sp_reg_HC08
 646              | HCS08 ⇒ Some ? set_sp_reg_HC08
 647              | RS08 ⇒ None ? ])
 648  (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
 649
 650 (* setter debole di SP *)
 651 definition setweak_sp_reg ≝
 652 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
 653  match set_sp_reg m t s sp' with
 654   [ None ⇒ s | Some s' ⇒ s' ].
 655
 656 (* REGISTRO PC *)
 657
 658 (* setter specifico HC05 di PC, effettua PC∧mask *)
 659 definition set_pc_reg_HC05 ≝
 660 λalu.λpc':word16.
 661  mk_alu_HC05
 662   (acc_low_reg_HC05 alu)
 663   (indX_low_reg_HC05 alu)
 664   (sp_reg_HC05 alu)
 665   (sp_mask_HC05 alu)
 666   (sp_fix_HC05 alu)
 667   (and_w16 pc' (pc_mask_HC05 alu))
 668   (pc_mask_HC05 alu)
 669   (h_flag_HC05 alu)
 670   (i_flag_HC05 alu)
 671   (n_flag_HC05 alu)
 672   (z_flag_HC05 alu)
 673   (c_flag_HC05 alu)
 674   (irq_flag_HC05 alu).
 675
 676 (* setter specifico HC08/HCS08 di PC *)
 677 definition set_pc_reg_HC08 ≝
 678 λalu.λpc':word16.
 679  mk_alu_HC08
 680   (acc_low_reg_HC08 alu)
 681   (indX_low_reg_HC08 alu)
 682   (indX_high_reg_HC08 alu)
 683   (sp_reg_HC08 alu)
 684   pc'
 685   (v_flag_HC08 alu)
 686   (h_flag_HC08 alu)
 687   (i_flag_HC08 alu)
 688   (n_flag_HC08 alu)
 689   (z_flag_HC08 alu)
 690   (c_flag_HC08 alu)
 691   (irq_flag_HC08 alu).
 692
 693 (* setter specifico RS08 di PC, effettua PC∧mask *)
 694 definition set_pc_reg_RS08 ≝
 695 λalu.λpc':word16.
 696  mk_alu_RS08
 697   (acc_low_reg_RS08 alu)
 698   (and_w16 pc' (pc_mask_RS08 alu))
 699   (pc_mask_RS08 alu)
 700   (spc_reg_RS08 alu)
 701   (x_map_RS08 alu)
 702   (ps_map_RS08 alu)
 703   (z_flag_RS08 alu)
 704   (c_flag_RS08 alu).
 705
 706 (* setter forte di PC *)
 707 definition set_pc_reg ≝
 708 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
 709  set_alu m t s
 710  (match m return aux_set_typing word16 with
 711   [ HC05 ⇒ set_pc_reg_HC05
 712   | HC08 ⇒ set_pc_reg_HC08
 713   | HCS08 ⇒ set_pc_reg_HC08
 714   | RS08 ⇒ set_pc_reg_RS08
 715   ] (alu m t s) pc').
 716
 717 (* REGISTRO SPC *)
 718
 719 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
 720 definition set_spc_reg_RS08 ≝
 721 λalu.λspc':word16.
 722  mk_alu_RS08
 723   (acc_low_reg_RS08 alu)
 724   (pc_reg_RS08 alu)
 725   (pc_mask_RS08 alu)
 726   (and_w16 spc' (pc_mask_RS08 alu))
 727   (x_map_RS08 alu)
 728   (ps_map_RS08 alu)
 729   (z_flag_RS08 alu)
 730   (c_flag_RS08 alu).
 731
 732 (* setter forte di SPC *)
 733 definition set_spc_reg ≝
 734 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
 735  opt_map ?? (match m return aux_set_typing_opt word16 with
 736              [ HC05 ⇒ None ?
 737              | HC08 ⇒ None ?
 738              | HCS08 ⇒ None ?
 739              | RS08 ⇒ Some ? set_spc_reg_RS08 ])
 740  (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
 741
 742 (* setter debole di SPC *)
 743 definition setweak_spc_reg ≝
 744 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
 745  match set_spc_reg m t s spc' with
 746   [ None ⇒ s | Some s' ⇒ s' ].
 747
 748 (* REGISTRO MEMORY MAPPED X *)
 749
 750 (* setter specifico RS08 di memory mapped X *)
 751 definition set_x_map_RS08 ≝
 752 λalu.λxm':byte8.
 753  mk_alu_RS08
 754   (acc_low_reg_RS08 alu)
 755   (pc_reg_RS08 alu)
 756   (pc_mask_RS08 alu)
 757   (spc_reg_RS08 alu)
 758   xm'
 759   (ps_map_RS08 alu)
 760   (z_flag_RS08 alu)
 761   (c_flag_RS08 alu).
 762
 763 (* setter forte di memory mapped X *)
 764 definition set_x_map ≝
 765 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
 766  opt_map ?? (match m return aux_set_typing_opt byte8 with
 767              [ HC05 ⇒ None ?
 768              | HC08 ⇒ None ?
 769              | HCS08 ⇒ None ?
 770              | RS08 ⇒ Some ? set_x_map_RS08 ])
 771  (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
 772
 773 (* setter debole di memory mapped X *)
 774 definition setweak_x_map ≝
 775 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
 776  match set_x_map m t s xm' with
 777   [ None ⇒ s | Some s' ⇒ s' ].
 778
 779 (* REGISTRO MEMORY MAPPED PS *)
 780
 781 (* setter specifico RS08 di memory mapped PS *)
 782 definition set_ps_map_RS08 ≝
 783 λalu.λpsm':byte8.
 784  mk_alu_RS08
 785   (acc_low_reg_RS08 alu)
 786   (pc_reg_RS08 alu)
 787   (pc_mask_RS08 alu)
 788   (spc_reg_RS08 alu)
 789   (x_map_RS08 alu)
 790   psm'
 791   (z_flag_RS08 alu)
 792   (c_flag_RS08 alu).
 793
 794 (* setter forte di memory mapped PS *)
 795 definition set_ps_map ≝
 796 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
 797  opt_map ?? (match m return aux_set_typing_opt byte8 with
 798              [ HC05 ⇒ None ?
 799              | HC08 ⇒ None ?
 800              | HCS08 ⇒ None ?
 801              | RS08 ⇒ Some ? set_ps_map_RS08 ])
 802  (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
 803
 804 (* setter debole di memory mapped PS *)
 805 definition setweak_ps_map ≝
 806 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
 807  match set_ps_map m t s psm' with
 808   [ None ⇒ s | Some s' ⇒ s' ].
 809
 810 (* FLAG V *)
 811
 812 (* setter specifico HC08/HCS08 di V *)
 813 definition set_v_flag_HC08 ≝
 814 λalu.λvfl':bool.
 815  mk_alu_HC08
 816   (acc_low_reg_HC08 alu)
 817   (indX_low_reg_HC08 alu)
 818   (indX_high_reg_HC08 alu)
 819   (sp_reg_HC08 alu)
 820   (pc_reg_HC08 alu)
 821   vfl'
 822   (h_flag_HC08 alu)
 823   (i_flag_HC08 alu)
 824   (n_flag_HC08 alu)
 825   (z_flag_HC08 alu)
 826   (c_flag_HC08 alu)
 827   (irq_flag_HC08 alu).
 828
 829 (* setter forte di V *)
 830 definition set_v_flag ≝
 831 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
 832  opt_map ?? (match m return aux_set_typing_opt bool with
 833              [ HC05 ⇒ None ?
 834              | HC08 ⇒ Some ? set_v_flag_HC08
 835              | HCS08 ⇒ Some ? set_v_flag_HC08
 836              | RS08 ⇒ None ? ])
 837  (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
 838
 839 (* setter debole  di V *)
 840 definition setweak_v_flag ≝
 841 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
 842  match set_v_flag m t s vfl' with
 843   [ None ⇒ s | Some s' ⇒ s' ].
 844
 845 (* FLAG H *)
 846
 847 (* setter specifico HC05 di H *)
 848 definition set_h_flag_HC05 ≝
 849 λalu.λhfl':bool.
 850  mk_alu_HC05
 851   (acc_low_reg_HC05 alu)
 852   (indX_low_reg_HC05 alu)
 853   (sp_reg_HC05 alu)
 854   (sp_mask_HC05 alu)
 855   (sp_fix_HC05 alu)
 856   (pc_reg_HC05 alu)
 857   (pc_mask_HC05 alu)
 858   hfl'
 859   (i_flag_HC05 alu)
 860   (n_flag_HC05 alu)
 861   (z_flag_HC05 alu)
 862   (c_flag_HC05 alu)
 863   (irq_flag_HC05 alu).
 864
 865 (* setter specifico HC08/HCS08 di H *)
 866 definition set_h_flag_HC08 ≝
 867 λalu.λhfl':bool.
 868  mk_alu_HC08
 869   (acc_low_reg_HC08 alu)
 870   (indX_low_reg_HC08 alu)
 871   (indX_high_reg_HC08 alu)
 872   (sp_reg_HC08 alu)
 873   (pc_reg_HC08 alu)
 874   (v_flag_HC08 alu)
 875   hfl'
 876   (i_flag_HC08 alu)
 877   (n_flag_HC08 alu)
 878   (z_flag_HC08 alu)
 879   (c_flag_HC08 alu)
 880   (irq_flag_HC08 alu).
 881
 882 (* setter forte di H *)
 883 definition set_h_flag ≝
 884 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
 885  opt_map ?? (match m return aux_set_typing_opt bool with
 886              [ HC05 ⇒ Some ? set_h_flag_HC05
 887              | HC08 ⇒ Some ? set_h_flag_HC08
 888              | HCS08 ⇒ Some ? set_h_flag_HC08
 889              | RS08 ⇒ None ? ])
 890  (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
 891
 892 (* setter debole di H *)
 893 definition setweak_h_flag ≝
 894 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
 895  match set_h_flag m t s hfl' with
 896   [ None ⇒ s | Some s' ⇒ s' ].
 897
 898 (* FLAG I *)
 899
 900 (* setter specifico HC05 di I *)
 901 definition set_i_flag_HC05 ≝
 902 λalu.λifl':bool.
 903  mk_alu_HC05
 904   (acc_low_reg_HC05 alu)
 905   (indX_low_reg_HC05 alu)
 906   (sp_reg_HC05 alu)
 907   (sp_mask_HC05 alu)
 908   (sp_fix_HC05 alu)
 909   (pc_reg_HC05 alu)
 910   (pc_mask_HC05 alu)
 911   (h_flag_HC05 alu)
 912   ifl'
 913   (n_flag_HC05 alu)
 914   (z_flag_HC05 alu)
 915   (c_flag_HC05 alu)
 916   (irq_flag_HC05 alu).
 917
 918 (* setter specifico HC08/HCS08 di I *)
 919 definition set_i_flag_HC08 ≝
 920 λalu.λifl':bool.
 921  mk_alu_HC08
 922   (acc_low_reg_HC08 alu)
 923   (indX_low_reg_HC08 alu)
 924   (indX_high_reg_HC08 alu)
 925   (sp_reg_HC08 alu)
 926   (pc_reg_HC08 alu)
 927   (v_flag_HC08 alu)
 928   (h_flag_HC08 alu)
 929   ifl'
 930   (n_flag_HC08 alu)
 931   (z_flag_HC08 alu)
 932   (c_flag_HC08 alu)
 933   (irq_flag_HC08 alu).
 934
 935 (* setter forte di I *)
 936 definition set_i_flag ≝
 937 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
 938  opt_map ?? (match m return aux_set_typing_opt bool with
 939              [ HC05 ⇒ Some ? set_i_flag_HC05
 940              | HC08 ⇒ Some ? set_i_flag_HC08
 941              | HCS08 ⇒ Some ? set_i_flag_HC08
 942              | RS08 ⇒ None ? ])
 943  (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
 944
 945 (* setter debole di I *)
 946 definition setweak_i_flag ≝
 947 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
 948  match set_i_flag m t s ifl' with
 949   [ None ⇒ s | Some s' ⇒ s' ].
 950
 951 (* FLAG N *)
 952
 953 (* setter specifico HC05 di N *)
 954 definition set_n_flag_HC05 ≝
 955 λalu.λnfl':bool.
 956  mk_alu_HC05
 957   (acc_low_reg_HC05 alu)
 958   (indX_low_reg_HC05 alu)
 959   (sp_reg_HC05 alu)
 960   (sp_mask_HC05 alu)
 961   (sp_fix_HC05 alu)
 962   (pc_reg_HC05 alu)
 963   (pc_mask_HC05 alu)
 964   (h_flag_HC05 alu)
 965   (i_flag_HC05 alu)
 966   nfl'
 967   (z_flag_HC05 alu)
 968   (c_flag_HC05 alu)
 969   (irq_flag_HC05 alu).
 970
 971 (* setter specifico HC08/HCS08 di N *)
 972 definition set_n_flag_HC08 ≝
 973 λalu.λnfl':bool.
 974  mk_alu_HC08
 975   (acc_low_reg_HC08 alu)
 976   (indX_low_reg_HC08 alu)
 977   (indX_high_reg_HC08 alu)
 978   (sp_reg_HC08 alu)
 979   (pc_reg_HC08 alu)
 980   (v_flag_HC08 alu)
 981   (h_flag_HC08 alu)
 982   (i_flag_HC08 alu)
 983   nfl'
 984   (z_flag_HC08 alu)
 985   (c_flag_HC08 alu)
 986   (irq_flag_HC08 alu).
 987
 988 (* setter forte di N *)
 989 definition set_n_flag ≝
 990 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
 991  opt_map ?? (match m return aux_set_typing_opt bool with
 992              [ HC05 ⇒ Some ? set_n_flag_HC05
 993              | HC08 ⇒ Some ? set_n_flag_HC08
 994              | HCS08 ⇒ Some ? set_n_flag_HC08
 995              | RS08 ⇒ None ? ])
 996  (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
 997
 998 (* setter debole di N *)
 999 definition setweak_n_flag ≝
1000 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
1001  match set_n_flag m t s nfl' with
1002   [ None ⇒ s | Some s' ⇒ s' ].
1003
1004 (* FLAG Z *)
1005
1006 (* setter specifico HC05 di Z *)
1007 definition set_z_flag_HC05 ≝
1008 λalu.λzfl':bool.
1009  mk_alu_HC05
1010   (acc_low_reg_HC05 alu)
1011   (indX_low_reg_HC05 alu)
1012   (sp_reg_HC05 alu)
1013   (sp_mask_HC05 alu)
1014   (sp_fix_HC05 alu)
1015   (pc_reg_HC05 alu)
1016   (pc_mask_HC05 alu)
1017   (h_flag_HC05 alu)
1018   (i_flag_HC05 alu)
1019   (n_flag_HC05 alu)
1020   zfl'
1021   (c_flag_HC05 alu)
1022   (irq_flag_HC05 alu).
1023
1024 (* setter specifico HC08/HCS08 di Z *)
1025 definition set_z_flag_HC08 ≝
1026 λalu.λzfl':bool.
1027  mk_alu_HC08
1028   (acc_low_reg_HC08 alu)
1029   (indX_low_reg_HC08 alu)
1030   (indX_high_reg_HC08 alu)
1031   (sp_reg_HC08 alu)
1032   (pc_reg_HC08 alu)
1033   (v_flag_HC08 alu)
1034   (h_flag_HC08 alu)
1035   (i_flag_HC08 alu)
1036   (n_flag_HC08 alu)
1037   zfl'
1038   (c_flag_HC08 alu)
1039   (irq_flag_HC08 alu).
1040
1041 (* setter sprcifico RS08 di Z *)
1042 definition set_z_flag_RS08 ≝
1043 λalu.λzfl':bool.
1044  mk_alu_RS08
1045   (acc_low_reg_RS08 alu)
1046   (pc_reg_RS08 alu)
1047   (pc_mask_RS08 alu)
1048   (spc_reg_RS08 alu)
1049   (x_map_RS08 alu)
1050   (ps_map_RS08 alu)
1051   zfl'
1052   (c_flag_RS08 alu).
1053
1054 (* setter forte di Z *)
1055 definition set_z_flag ≝
1056 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
1057  set_alu m t s
1058  (match m return aux_set_typing bool with
1059   [ HC05 ⇒ set_z_flag_HC05
1060   | HC08 ⇒ set_z_flag_HC08
1061   | HCS08 ⇒ set_z_flag_HC08
1062   | RS08 ⇒ set_z_flag_RS08
1063   ] (alu m t s) zfl').
1064
1065 (* FLAG C *)
1066
1067 (* setter specifico HC05 di C *)
1068 definition set_c_flag_HC05 ≝
1069 λalu.λcfl':bool.
1070  mk_alu_HC05
1071   (acc_low_reg_HC05 alu)
1072   (indX_low_reg_HC05 alu)
1073   (sp_reg_HC05 alu)
1074   (sp_mask_HC05 alu)
1075   (sp_fix_HC05 alu)
1076   (pc_reg_HC05 alu)
1077   (pc_mask_HC05 alu)
1078   (h_flag_HC05 alu)
1079   (i_flag_HC05 alu)
1080   (n_flag_HC05 alu)
1081   (z_flag_HC05 alu)
1082   cfl'
1083   (irq_flag_HC05 alu).
1084
1085 (* setter specifico HC08/HCS08 di C *)
1086 definition set_c_flag_HC08 ≝
1087 λalu.λcfl':bool.
1088  mk_alu_HC08
1089   (acc_low_reg_HC08 alu)
1090   (indX_low_reg_HC08 alu)
1091   (indX_high_reg_HC08 alu)
1092   (sp_reg_HC08 alu)
1093   (pc_reg_HC08 alu)
1094   (v_flag_HC08 alu)
1095   (h_flag_HC08 alu)
1096   (i_flag_HC08 alu)
1097   (n_flag_HC08 alu)
1098   (z_flag_HC08 alu)
1099   cfl'
1100   (irq_flag_HC08 alu).
1101
1102 (* setter specifico RS08 di C *)
1103 definition set_c_flag_RS08 ≝
1104 λalu.λcfl':bool.
1105  mk_alu_RS08
1106   (acc_low_reg_RS08 alu)
1107   (pc_reg_RS08 alu)
1108   (pc_mask_RS08 alu)
1109   (spc_reg_RS08 alu)
1110   (x_map_RS08 alu)
1111   (ps_map_RS08 alu)
1112   (z_flag_RS08 alu)
1113   cfl'.
1114
1115 (* setter forte di C *)
1116 definition set_c_flag ≝
1117 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
1118  set_alu m t s
1119  (match m return aux_set_typing bool with
1120   [ HC05 ⇒ set_c_flag_HC05
1121   | HC08 ⇒ set_c_flag_HC08
1122   | HCS08 ⇒ set_c_flag_HC08
1123   | RS08 ⇒ set_c_flag_RS08
1124   ] (alu m t s) cfl').
1125
1126 (* FLAG IRQ *)
1127
1128 (* setter specifico HC05 di IRQ *)
1129 definition set_irq_flag_HC05 ≝
1130 λalu.λirqfl':bool.
1131  mk_alu_HC05
1132   (acc_low_reg_HC05 alu)
1133   (indX_low_reg_HC05 alu)
1134   (sp_reg_HC05 alu)
1135   (sp_mask_HC05 alu)
1136   (sp_fix_HC05 alu)
1137   (pc_reg_HC05 alu)
1138   (pc_mask_HC05 alu)
1139   (h_flag_HC05 alu)
1140   (i_flag_HC05 alu)
1141   (n_flag_HC05 alu)
1142   (z_flag_HC05 alu)
1143   (c_flag_HC05 alu)
1144   irqfl'.
1145
1146 (* setter specifico HC08/HCS08 di IRQ *)
1147 definition set_irq_flag_HC08 ≝
1148 λalu.λirqfl':bool.
1149  mk_alu_HC08
1150   (acc_low_reg_HC08 alu)
1151   (indX_low_reg_HC08 alu)
1152   (indX_high_reg_HC08 alu)
1153   (sp_reg_HC08 alu)
1154   (pc_reg_HC08 alu)
1155   (v_flag_HC08 alu)
1156   (h_flag_HC08 alu)
1157   (i_flag_HC08 alu)
1158   (n_flag_HC08 alu)
1159   (z_flag_HC08 alu)
1160   (c_flag_HC08 alu)
1161   irqfl'.
1162
1163 (* setter forte di IRQ *)
1164 definition set_irq_flag ≝
1165 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1166  opt_map ?? (match m return aux_set_typing_opt bool with
1167              [ HC05 ⇒ Some ? set_irq_flag_HC05
1168              | HC08 ⇒ Some ? set_irq_flag_HC08
1169              | HCS08 ⇒ Some ? set_irq_flag_HC08
1170              | RS08 ⇒ None ? ])
1171  (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
1172
1173 (* setter debole di IRQ *)
1174 definition setweak_irq_flag ≝
1175 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1176  match set_irq_flag m t s irqfl' with
1177   [ None ⇒ s | Some s' ⇒ s' ].
1178
1179 (* ***************** *)
1180 (* CONFRONTO FRA ALU *)
1181 (* ***************** *)
1182
1183 (* confronto registro per registro dell'HC05 *)
1184 definition eq_alu_HC05 ≝
1185 λalu1,alu2:alu_HC05.
1186  match alu1 with
1187   [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1188  match alu2 with
1189   [ mk_alu_HC05 acclow2 indxlow2 sp2 spm2 spf2 pc2 pcm2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1190    (eq_b8 acclow1 acclow2) ⊗
1191    (eq_b8 indxlow1 indxlow2) ⊗
1192    (eq_w16 sp1 sp2) ⊗
1193    (eq_w16 spm1 spm2) ⊗
1194    (eq_w16 spf1 spf2) ⊗
1195    (eq_w16 pc1 pc2) ⊗
1196    (eq_w16 pcm1 pcm2) ⊗
1197    (eq_bool hfl1 hfl2) ⊗
1198    (eq_bool ifl1 ifl2) ⊗
1199    (eq_bool nfl1 nfl2) ⊗
1200    (eq_bool zfl1 zfl2) ⊗
1201    (eq_bool cfl1 cfl2) ⊗
1202    (eq_bool irqfl1 irqfl2) ]].
1203
1204 (* confronto registro per registro dell'HC08 *)
1205 definition eq_alu_HC08 ≝
1206 λalu1,alu2:alu_HC08.
1207  match alu1 with
1208   [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1209  match alu2 with
1210   [ mk_alu_HC08 acclow2 indxlow2 indxhigh2 sp2 pc2 vfl2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1211    (eq_b8 acclow1 acclow2) ⊗
1212    (eq_b8 indxlow1 indxlow2) ⊗
1213    (eq_b8 indxhigh1 indxhigh2) ⊗
1214    (eq_w16 sp1 sp2) ⊗
1215    (eq_w16 pc1 pc2) ⊗
1216    (eq_bool vfl1 vfl2) ⊗
1217    (eq_bool hfl1 hfl2) ⊗
1218    (eq_bool ifl1 ifl2) ⊗
1219    (eq_bool nfl1 nfl2) ⊗
1220    (eq_bool zfl1 zfl2) ⊗
1221    (eq_bool cfl1 cfl2) ⊗
1222    (eq_bool irqfl1 irqfl2) ]].
1223
1224 (* confronto registro per registro dell'RS08 *)
1225 definition eq_alu_RS08 ≝
1226 λalu1,alu2:alu_RS08.
1227  match alu1 with
1228   [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
1229  match alu2 with
1230   [ mk_alu_RS08 acclow2 pc2 pcm2 spc2 xm2 psm2 zfl2 cfl2 ⇒
1231    (eq_b8 acclow1 acclow2) ⊗
1232    (eq_w16 pc1 pc2) ⊗
1233    (eq_w16 pcm1 pcm2) ⊗
1234    (eq_w16 spc1 spc2) ⊗
1235    (eq_b8 xm1 xm2) ⊗
1236    (eq_b8 psm1 psm2) ⊗
1237    (eq_bool zfl1 zfl2) ⊗
1238    (eq_bool cfl1 cfl2) ]].
1239
1240 (* ******************** *)
1241 (* CONFRONTO FRA STATUS *)
1242 (* ******************** *)
1243
1244 (* la lettura da memoria ritorna un option byte8, quindi bisogna poterli confrontare *)
1245 definition eq_b8_opt ≝
1246 λb1,b2:option byte8.
1247  match b1 with
1248   [ None ⇒ match b2 with
1249    [ None ⇒ true | Some _ ⇒ false ]
1250   | Some b1' ⇒ match b2 with
1251    [ None ⇒ false | Some b2' ⇒ eq_b8 b1' b2' ]
1252   ].
1253
1254 (* confronto di una regione di memoria [inf,inf+n] *)
1255 let rec forall_memory_ranged
1256  (t:memory_impl)
1257  (chk1:aux_chk_type t) (chk2:aux_chk_type t)
1258  (mem1:aux_mem_type t) (mem2:aux_mem_type t)
1259  (inf:word16) (n:nat) on n ≝
1260  match n return λ_.bool with
1261   [ O ⇒ eq_b8_opt (mem_read t mem1 chk1 inf) (mem_read t mem2 chk2 inf)
1262   | S n' ⇒ (eq_b8_opt (mem_read t mem1 chk1 (plus_w16nc inf (word16_of_nat n)))
1263                       (mem_read t mem2 chk2 (plus_w16nc inf (word16_of_nat n)))) ⊗
1264            (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n')
1265   ].
1266
1267 (* il clk e' option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16) *)
1268 definition eq_clk ≝
1269 λm:mcu_type.λc1,c2:option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
1270  match c1 with
1271   [ None ⇒ match c2 with
1272    [ None ⇒ true | Some _ ⇒ false ]
1273   | Some c1' ⇒ match c2 with
1274    [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T ????? c1') (fst5T ????? c2')) ⊗
1275                                (eqop m (snd5T ????? c1') (snd5T ????? c2')) ⊗
1276                                (eqim (thd5T ????? c1') (thd5T ????? c2')) ⊗
1277                                (eq_b8 (frth5T ????? c1') (frth5T ????? c2')) ⊗
1278                                (eq_w16 (ffth5T ????? c1') (ffth5T ????? c2')) ]
1279   ].
1280
1281 (* generalizzazione del confronto fra stati *)
1282 definition eq_status ≝
1283 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λinf:word16.λn:nat.
1284  match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
1285  match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
1286
1287  (* 1) confronto della ALU *)
1288  (match m return λm:mcu_type.
1289    match m with
1290     [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1291    match m with
1292     [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1293    bool with
1294   [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ]
1295  alu1 alu2) ⊗
1296
1297  (* 2) confronto della memoria in [inf,inf+n] *)
1298  (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n) ⊗
1299
1300  (* 3) confronto del clik *)
1301  (eq_clk m clk1 clk2)
1302  ]].
1303
1304 (* assioma da applicare per l'uguaglianza degli stati *)
1305 axiom eq_status_axiom :
1306 ∀inf:word16.∀n:nat.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1307  (eq_status m t s1 s2 inf n = true) →
1308  s1 = s2.