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