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