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