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