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