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