helm/software/matita/contribs/ng_assembly/freescale/load_write.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/model.ma".
  28 include "freescale/translation.ma".
  29
  30 (* errori possibili nel fetch *)
  31 ninductive error_type : Type ≝
  32   ILL_OP: error_type
  33 | ILL_FETCH_AD: error_type
  34 | ILL_EX_AD: error_type.
  35
  36 ndefinition error_type_ind : ΠP:error_type → Prop.P ILL_OP → P ILL_FETCH_AD → P ILL_EX_AD → Πe:error_type.P e ≝
  37 λP:error_type → Prop.λp:P ILL_OP.λp1:P ILL_FETCH_AD.λp2:P ILL_EX_AD.λe:error_type.
  38  match e with [ ILL_OP ⇒ p | ILL_FETCH_AD ⇒ p1 | ILL_EX_AD ⇒ p2 ].
  39
  40 ndefinition error_type_rec : ΠP:error_type → Set.P ILL_OP → P ILL_FETCH_AD → P ILL_EX_AD → Πe:error_type.P e ≝
  41 λP:error_type → Set.λp:P ILL_OP.λp1:P ILL_FETCH_AD.λp2:P ILL_EX_AD.λe:error_type.
  42  match e with [ ILL_OP ⇒ p | ILL_FETCH_AD ⇒ p1 | ILL_EX_AD ⇒ p2 ].
  43
  44 ndefinition error_type_rect : ΠP:error_type → Type.P ILL_OP → P ILL_FETCH_AD → P ILL_EX_AD → Πe:error_type.P e ≝
  45 λP:error_type → Type.λp:P ILL_OP.λp1:P ILL_FETCH_AD.λp2:P ILL_EX_AD.λe:error_type.
  46  match e with [ ILL_OP ⇒ p | ILL_FETCH_AD ⇒ p1 | ILL_EX_AD ⇒ p2 ].
  47
  48 (* un tipo opzione ad hoc
  49    - errore: interessa solo l'errore
  50    - ok: interessa info e il nuovo pc
  51 *)
  52 ninductive fetch_result (A:Type) : Type ≝
  53   FetchERR : error_type → fetch_result A
  54 | FetchOK  : A → word16 → fetch_result A.
  55
  56 ndefinition fetch_result_ind
  57  : ΠA:Type.ΠP:fetch_result A → Prop.(Πn:error_type.P (FetchERR A n)) →
  58    (Πa:A.Πn:word16.P (FetchOK A a n)) → Πf:fetch_result A.P f ≝
  59 λA:Type.λP:fetch_result A → Prop.λf:Πn:error_type.P (FetchERR A n).
  60 λf1:Πa:A.Πn:word16.P (FetchOK A a n).λf2:fetch_result A.
  61  match f2 with [ FetchERR n ⇒ f n | FetchOK a n ⇒ f1 a n ].
  62
  63 ndefinition fetch_result_rec
  64  : ΠA:Type.ΠP:fetch_result A → Set.(Πn:error_type.P (FetchERR A n)) →
  65    (Πa:A.Πn:word16.P (FetchOK A a n)) → Πf:fetch_result A.P f ≝
  66 λA:Type.λP:fetch_result A → Set.λf:Πn:error_type.P (FetchERR A n).
  67 λf1:Πa:A.Πn:word16.P (FetchOK A a n).λf2:fetch_result A.
  68  match f2 with [ FetchERR n ⇒ f n | FetchOK a n ⇒ f1 a n ].
  69
  70 ndefinition fetch_result_rect
  71  : ΠA:Type.ΠP:fetch_result A → Type.(Πn:error_type.P (FetchERR A n)) →
  72    (Πa:A.Πn:word16.P (FetchOK A a n)) → Πf:fetch_result A.P f ≝
  73 λA:Type.λP:fetch_result A → Type.λf:Πn:error_type.P (FetchERR A n).
  74 λf1:Πa:A.Πn:word16.P (FetchOK A a n).λf2:fetch_result A.
  75  match f2 with [ FetchERR n ⇒ f n | FetchOK a n ⇒ f1 a n ].
  76
  77 (* **************************** *)
  78 (* FETCH E ACCESSO ALLA MEMORIA *)
  79 (* **************************** *)
  80
  81 (* ausialiaria per RS08 read *)
  82 (* come anticipato in status, nell'RS08 ci sono 2 registri importanti
  83    memory mapped, quindi bisona intercettare la lettura.
  84    NB: fare molta attenzione alle note sulle combinazioni possibili perche'
  85        il comportamento della memoria nell'RS08 e' strano e ci sono
  86        precise condizioni che impediscono una semantica circolare dell'accesso
  87        (divergenza=assenza di definizione) *)
  88 ndefinition RS08_memory_filter_read_aux ≝
  89 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
  90 λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option T.
  91 match s with
  92  [ mk_any_status alu mem chk _ ⇒ match alu with
  93   [ mk_alu_RS08 _ _ _ _ xm psm _ _ ⇒
  94 (*
  95    possibili accessi al registro X
  96    1) addr=000F: diretto
  97    2) addr=000E (X =0F): indiretto
  98    3) addr=00CF (PS=00): paging
  99
 100    [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
 101    non si possono combinare due effetti contemporaneamente!
 102    per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni
 103 *)
 104   match eq_w16 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
 105         (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
 106         (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
 107    [ true ⇒ fREG xm
 108    | false ⇒
 109 (*
 110    possibili accessi al registro PS
 111    1) addr=001F: diretto
 112    2) addr=000E (X =1F): indiretto
 113    3) addr=00DF (PS=00): paging
 114 *)
 115     match eq_w16 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
 116          (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
 117          (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
 118      [ true ⇒ fREG psm
 119      | false ⇒
 120 (*
 121    accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
 122    altrimenti sarebbero 2 indirezioni
 123 *)
 124       match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
 125        [ true ⇒ fMEM mem chk 〈〈x0,x0〉:xm〉
 126        | false ⇒
 127 (*
 128    accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
 129 *)
 130         match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
 131          [ true ⇒ fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
 132                                              (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉))
 133 (*
 134    accesso normale
 135 *)
 136          | false ⇒ fMEM mem chk addr ]]]]]].
 137
 138 (* lettura RS08 di un byte *)
 139 ndefinition RS08_memory_filter_read ≝
 140 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
 141  RS08_memory_filter_read_aux t s addr byte8
 142   (λb.Some byte8 b)
 143   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_read t m c a).
 144
 145 (* lettura RS08 di un bit *)
 146 ndefinition RS08_memory_filter_read_bit ≝
 147 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.
 148  RS08_memory_filter_read_aux t s addr bool
 149   (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
 150   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_read_bit t m c a sub).
 151
 152 (* in caso di RS08 si dirotta sul filtro, altrimenti si legge direttamente *)
 153 ndefinition memory_filter_read ≝
 154 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → option byte8 with
 155  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.
 156   mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
 157  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.
 158   mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
 159  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.
 160   mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr
 161  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.
 162   RS08_memory_filter_read t s addr
 163  ].
 164
 165 ndefinition memory_filter_read_bit ≝
 166 λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → oct → option bool with
 167  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.
 168   mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
 169  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.
 170   mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
 171  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.
 172   mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub
 173  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.
 174   RS08_memory_filter_read_bit t s addr sub
 175  ].
 176
 177 (* ausialiaria per RS08 write *)
 178 (* come anticipato in status, nell'RS08 ci sono 2 registri importanti
 179    memory mapped, quindi bisona intercettare la scrittura.
 180    NB: fare molta attenzione alle note sulle combinazioni possibili perche'
 181        il comportamento della memoria nell'RS08 e' strano e ci sono
 182        precise condizioni che impediscono una semantica circolare dell'accesso
 183        (divergenza=assenza di definizione) *)
 184 ndefinition RS08_memory_filter_write_aux ≝
 185 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
 186 λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option (aux_mem_type t).
 187 match s with
 188  [ mk_any_status alu mem chk clk ⇒ match alu with
 189   [ mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl ⇒
 190 (*
 191    possibili accessi al registro X
 192    1) addr=000F: diretto
 193    2) addr=000E (X =0F): indiretto
 194    3) addr=00CF (PS=00): paging
 195
 196    [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
 197    non si possono combinare due effetti contemporaneamente!
 198    per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni
 199 *)
 200   match eq_w16 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
 201         (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
 202         (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
 203    [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc (fREG xm) psm zfl cfl) mem chk clk)
 204    | false ⇒
 205 (*
 206    possibili accessi al registro PS
 207    1) addr=001F: diretto
 208    2) addr=000E (X =1F): indiretto
 209    3) addr=00DF (PS=00): paging
 210 *)
 211     match eq_w16 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
 212          (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
 213          (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
 214      [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm (fREG psm) zfl cfl) mem chk clk)
 215      | false ⇒
 216 (*
 217    accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
 218    altrimenti sarebbero 2 indirezioni
 219 *)
 220       match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
 221        [ true ⇒ opt_map ?? (fMEM mem chk 〈〈x0,x0〉:xm〉)
 222                  (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
 223
 224        | false ⇒
 225 (*
 226    accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
 227 *)
 228         match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
 229          [ true ⇒ opt_map ?? (fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
 230                                                    (and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉)))
 231                    (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
 232 (*
 233    accesso normale
 234 *)
 235          | false ⇒ opt_map ?? (fMEM mem chk addr)
 236                     (λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk)) ]]]]]].
 237
 238 (* scrittura RS08 di un byte *)
 239 ndefinition RS08_memory_filter_write ≝
 240 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λval:byte8.
 241  RS08_memory_filter_write_aux t s addr
 242   (λb.val)
 243   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_update t m c a val).
 244
 245 (* scrittura RS08 di un bit *)
 246 ndefinition RS08_memory_filter_write_bit ≝
 247 λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
 248  RS08_memory_filter_write_aux t s addr
 249   (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
 250   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.mem_update_bit t m c a sub val).
 251
 252 (* in caso di RS08 si dirotta sul filtro, altrimenti si scrive direttamente *)
 253 ndefinition memory_filter_write ≝
 254 λm:mcu_type.λt:memory_impl.match m
 255  return λm:mcu_type.any_status m t → word16 → byte8 → option (any_status m t) with
 256  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λval:byte8.
 257   opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
 258    (λmem.Some ? (set_mem_desc ? t s mem))
 259  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λval:byte8.
 260   opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
 261    (λmem.Some ? (set_mem_desc ? t s mem))
 262  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λval:byte8.
 263   opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val)
 264    (λmem.Some ? (set_mem_desc ? t s mem))
 265  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λval:byte8.
 266   RS08_memory_filter_write t s addr val
 267  ].
 268
 269 ndefinition memory_filter_write_bit ≝
 270 λm:mcu_type.λt:memory_impl.match m
 271  return λm:mcu_type.any_status m t → word16 → oct → bool → option (any_status m t) with
 272  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.λval:bool.
 273   opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
 274    (λmem.Some ? (set_mem_desc ? t s mem))
 275  | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.λval:bool.
 276   opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
 277    (λmem.Some ? (set_mem_desc ? t s mem))
 278  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.λval:bool.
 279   opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val)
 280    (λmem.Some ? (set_mem_desc ? t s mem))
 281  | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
 282   RS08_memory_filter_write_bit t s addr sub val
 283  ].
 284
 285 (*
 286    Da utilizzarsi solo per gli aggiornamenti di PC (per il fetch),
 287    NON per il caricamento degli indiretti.
 288    - il caricamento degli immediati spetta al fetcher
 289      (incremento progressivo di PC ciclo per ciclo, e riempimento del prefetch
 290       che a questo punto DEVE poter indirizzare qualsiasi locazione puntata da PC)
 291    - il caricamento degli indiretti non spetta al fetcher
 292 *)
 293 ndefinition filtered_inc_w16 ≝
 294 λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
 295  get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
 296
 297 nlet rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
 298  match n with
 299   [ O ⇒ w
 300   | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
 301
 302 (*
 303    errore1: non esiste traduzione ILL_OP
 304    errore2: non e' riuscito a leggere ILL_FETCH_AD
 305    altrimenti OK=info+new_pc
 306 *)
 307 ndefinition fetch ≝
 308 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 309  let pc ≝ get_pc_reg m t s in
 310  let pc_next1 ≝ filtered_inc_w16 m t s pc in
 311  let pc_next2 ≝ filtered_inc_w16 m t s pc_next1 in
 312  match memory_filter_read m t s pc with
 313   [ None ⇒ FetchERR ? ILL_FETCH_AD
 314   | Some bh ⇒ match full_info_of_word16 m (Byte bh) with
 315    (* non ha trovato una traduzione con 1 byte *)
 316    [ None ⇒ match m with
 317     (* HC05 non esistono op a 2 byte *)
 318     [ HC05 ⇒ FetchERR ? ILL_OP
 319     | HC08 ⇒ match eq_b8 bh 〈x9,xE〉 with
 320      (* HC08 se il primo byte e' 0x9E il secondo puo' avere senso *)
 321      [ true ⇒ match memory_filter_read m t s pc_next1 with
 322       [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
 323       [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
 324      (* HC08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
 325      | false ⇒ FetchERR ? ILL_OP
 326      ]
 327     | HCS08 ⇒ match eq_b8 bh 〈x9,xE〉 with
 328      (* HCS08 se il primo byte e' 0x9E il secondo puo' avere senso *)
 329      [ true ⇒ match memory_filter_read m t s pc_next1 with
 330       [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
 331       [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
 332      (* HCS08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
 333      | false ⇒ FetchERR ? ILL_OP
 334      ]
 335     (* RS08 non esistono op a 2 byte *)
 336     | RS08 ⇒ FetchERR ? ILL_OP
 337     ]
 338    (* ha trovato una traduzione con 1 byte *)
 339    | Some info ⇒ FetchOK ? info pc_next1 ]].
 340
 341 (* ************************ *)
 342 (* MODALITA' INDIRIZZAMENTO *)
 343 (* ************************ *)
 344
 345 (* mattoni base *)
 346 (* - incrementano l'indirizzo normalmente *)
 347 (* - incrementano PC attraverso il filtro *)
 348
 349 (* lettura byte da addr *)
 350 ndefinition loadb_from ≝
 351 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
 352  opt_map ?? (memory_filter_read m t s addr)
 353   (λb.Some ? (triple ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
 354
 355 (* lettura bit da addr *)
 356 ndefinition loadbit_from ≝
 357 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.
 358  opt_map ?? (memory_filter_read_bit m t s addr sub)
 359   (λb.Some ? (triple ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
 360
 361 (* lettura word da addr *)
 362 ndefinition loadw_from ≝
 363 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
 364  opt_map ?? (memory_filter_read m t s addr)
 365   (λbh.opt_map ?? (memory_filter_read m t s (succ_w16 addr))
 366    (λbl.Some ? (triple ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc fetched)))).
 367
 368 (* scrittura byte su addr *)
 369 ndefinition writeb_to ≝
 370 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwriteb:byte8.
 371  opt_map ?? (memory_filter_write m t s addr writeb)
 372   (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
 373
 374 (* scrittura bit su addr *)
 375 ndefinition writebit_to ≝
 376 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.λwriteb:bool.
 377  opt_map ?? (memory_filter_write_bit m t s addr sub writeb)
 378   (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
 379
 380 (* scrittura word su addr *)
 381 ndefinition writew_to ≝
 382 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
 383  opt_map ?? (memory_filter_write m t s addr (w16h writew))
 384   (λtmps1.opt_map ?? (memory_filter_write m t tmps1 (succ_w16 addr) (w16l writew))
 385     (λtmps2.Some ? (pair ?? tmps2 (filtered_plus_w16 m t tmps2 cur_pc fetched)))).
 386
 387 (* ausiliari per definire i tipi e la lettura/scrittura *)
 388
 389 (* ausiliaria per definire il tipo di aux_load *)
 390 ndefinition aux_load_typing ≝
 391 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
 392  any_status m t → word16 → word16 → nat →
 393  option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
 394
 395 (* per non dover ramificare i vari load in byte/word *)
 396 ndefinition aux_load ≝
 397 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
 398  [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
 399
 400 (* ausiliaria per definire il tipo di aux_write *)
 401 ndefinition aux_write_typing ≝
 402 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
 403  any_status m t → word16 → word16 → nat →
 404  match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
 405  option (ProdT (any_status m t) word16).
 406
 407 (* per non dover ramificare i vari load in byte/word *)
 408 ndefinition aux_write ≝
 409 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
 410  [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
 411
 412 (* modalita' vere e proprie *)
 413
 414 (* lettura da [curpc]: IMM1 comportamento asimmetrico, quindi non si appoggia a loadb *)
 415 ndefinition mode_IMM1_load ≝
 416 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 417  opt_map ?? (memory_filter_read m t s cur_pc)
 418   (λb.Some ? (triple ??? s b (filtered_inc_w16 m t s cur_pc))).
 419
 420 (* lettura da [curpc]: IMM1 + estensione a word *)
 421 ndefinition mode_IMM1EXT_load ≝
 422 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 423  opt_map ?? (memory_filter_read m t s cur_pc)
 424   (λb.Some ? (triple ??? s 〈〈x0,x0〉:b〉 (filtered_inc_w16 m t s cur_pc))).
 425
 426 (* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
 427 ndefinition mode_IMM2_load ≝
 428 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 429  opt_map ?? (memory_filter_read m t s cur_pc)
 430   (λbh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
 431    (λbl.Some ? (triple ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc 2)))).
 432
 433 (* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
 434 ndefinition mode_DIR1_load ≝
 435 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 436  opt_map ?? (memory_filter_read m t s cur_pc)
 437   (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
 438
 439 (* lettura da [byte [curpc]]: loadbit *)
 440 ndefinition mode_DIR1n_load ≝
 441 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.
 442  opt_map ?? (memory_filter_read m t s cur_pc)
 443   (λaddr.loadbit_from m t  s 〈〈x0,x0〉:addr〉 sub cur_pc 1).
 444
 445 (* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
 446 ndefinition mode_DIR1_write ≝
 447 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 448 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
 449  opt_map ?? (memory_filter_read m t s cur_pc)
 450   (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 writebw).
 451
 452 (* scrittura su [byte [curpc]]: writebit *)
 453 ndefinition mode_DIR1n_write ≝
 454 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.λwriteb:bool.
 455  opt_map ?? (memory_filter_read m t s cur_pc)
 456   (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1 writeb).
 457
 458 (* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
 459 ndefinition mode_DIR2_load ≝
 460 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 461  opt_map ?? (memory_filter_read m t s cur_pc)
 462   (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
 463    (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc 2)).
 464
 465 (* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
 466 ndefinition mode_DIR2_write ≝
 467 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 468 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
 469  opt_map ?? (memory_filter_read m t s cur_pc)
 470   (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
 471    (λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc 2 writebw)).
 472
 473 ndefinition get_IX ≝
 474 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 475  match m with
 476   [ HC05 ⇒ opt_map ?? (get_indX_8_low_reg m t s) (λindx.Some ? 〈〈x0,x0〉:indx〉)
 477   | HC08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx)
 478   | HCS08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx)
 479   | RS08 ⇒ None ? ].
 480
 481 (* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
 482 ndefinition mode_IX0_load ≝
 483 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 484  opt_map ?? (get_IX m t s)
 485   (λaddr.(aux_load m t byteflag) s addr cur_pc 0).
 486
 487 (* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
 488 ndefinition mode_IX0_write ≝
 489 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 490 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
 491  opt_map ?? (get_IX m t s)
 492   (λaddr.(aux_write m t byteflag) s addr cur_pc 0 writebw).
 493
 494 (* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
 495 ndefinition mode_IX1_load ≝
 496 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 497  opt_map ?? (get_IX m t s)
 498   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
 499    (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
 500
 501 (* lettura da X+[byte curpc] *)
 502 ndefinition mode_IX1ADD_load ≝
 503 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 504  opt_map ?? (memory_filter_read m t s cur_pc)
 505   (λb.opt_map ?? (get_IX m t s)
 506    (λaddr.Some ? (triple ??? s (plus_w16_d_d addr 〈〈x0,x0〉:b〉) (filtered_inc_w16 m t s cur_pc)))).
 507
 508 (* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
 509 ndefinition mode_IX1_write ≝
 510 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 511 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
 512  opt_map ?? (get_IX m t s)
 513   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
 514    (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
 515
 516 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
 517 ndefinition mode_IX2_load ≝
 518 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 519  opt_map ?? (get_IX m t s)
 520   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
 521    (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
 522     (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
 523
 524 (* lettura da X+[word curpc] *)
 525 ndefinition mode_IX2ADD_load ≝
 526 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 527  opt_map ?? (memory_filter_read m t s cur_pc)
 528   (λbh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
 529    (λbl.opt_map ?? (get_IX m t s)
 530     (λaddr.Some ? (triple ??? s (plus_w16_d_d addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc 2))))).
 531
 532 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
 533 ndefinition mode_IX2_write ≝
 534 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 535 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
 536  opt_map ?? (get_IX m t s)
 537   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
 538    (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
 539     (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
 540
 541 (* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
 542 ndefinition mode_SP1_load ≝
 543 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 544  opt_map ?? (get_sp_reg m t s)
 545   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
 546    (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
 547
 548 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
 549 ndefinition mode_SP1_write ≝
 550 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 551 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
 552  opt_map ?? (get_sp_reg m t s)
 553   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
 554    (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
 555
 556 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
 557 ndefinition mode_SP2_load ≝
 558 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 559  opt_map ?? (get_sp_reg m t s)
 560   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
 561    (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
 562     (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
 563
 564 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
 565 ndefinition mode_SP2_write ≝
 566 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 567 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
 568  opt_map ?? (get_sp_reg m t s)
 569   (λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
 570    (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
 571     (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
 572
 573 (* ************************************** *)
 574 (* raccordo di tutte le possibili letture *)
 575 (* ************************************** *)
 576
 577 (* H:X++ *)
 578 ndefinition aux_inc_indX_16 ≝
 579 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 580  opt_map ?? (get_indX_16_reg m t s)
 581   (λX_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 X_op))
 582    (λs_tmp.Some ? s_tmp)).
 583
 584 (* tutte le modalita' di lettura: false=loadb true=loadw *)
 585 ndefinition multi_mode_load ≝
 586 λbyteflag:bool.λm:mcu_type.λt:memory_impl.
 587  match byteflag
 588  return λbyteflag:bool.any_status m t → word16 → instr_mode →
 589   option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16)
 590  with
 591   (* lettura di un byte *)
 592   [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
 593 (* NO: non ci sono indicazioni *)
 594    [ MODE_INH  ⇒ None ?
 595 (* restituisce A *)
 596    | MODE_INHA ⇒ Some ? (triple ??? s (get_acc_8_low_reg m t s) cur_pc)
 597 (* restituisce X *)
 598    | MODE_INHX ⇒ opt_map ?? (get_indX_8_low_reg m t s)
 599                   (λindx.Some ? (triple ??? s indx cur_pc))
 600 (* restituisce H *)
 601    | MODE_INHH ⇒ opt_map ?? (get_indX_8_high_reg m t s)
 602                   (λindx.Some ? (triple ??? s indx cur_pc))
 603
 604 (* NO: solo lettura word *)
 605   | MODE_INHX0ADD ⇒ None ?
 606 (* NO: solo lettura word *)
 607   | MODE_INHX1ADD ⇒ None ?
 608 (* NO: solo lettura word *)
 609   | MODE_INHX2ADD ⇒ None ?
 610
 611 (* preleva 1 byte immediato *)
 612    | MODE_IMM1 ⇒ mode_IMM1_load m t s cur_pc
 613 (* NO: solo lettura word *)
 614    | MODE_IMM1EXT ⇒ None ?
 615 (* NO: solo lettura word *)
 616    | MODE_IMM2 ⇒ None ?
 617 (* preleva 1 byte da indirizzo diretto 1 byte *)
 618    | MODE_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
 619 (* preleva 1 byte da indirizzo diretto 1 word *)
 620    | MODE_DIR2 ⇒ mode_DIR2_load true m t s cur_pc
 621 (* preleva 1 byte da H:X *)
 622    | MODE_IX0  ⇒ mode_IX0_load true m t s cur_pc
 623 (* preleva 1 byte da H:X+1 byte offset *)
 624    | MODE_IX1  ⇒ mode_IX1_load true m t s cur_pc
 625 (* preleva 1 byte da H:X+1 word offset *)
 626    | MODE_IX2  ⇒ mode_IX2_load true m t s cur_pc
 627 (* preleva 1 byte da SP+1 byte offset *)
 628    | MODE_SP1  ⇒ mode_SP1_load true m t s cur_pc
 629 (* preleva 1 byte da SP+1 word offset *)
 630    | MODE_SP2  ⇒ mode_SP2_load true m t s cur_pc
 631
 632 (* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
 633    | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
 634 (* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
 635    | MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load m t s cur_pc
 636 (* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
 637    | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load true m t s cur_pc
 638 (* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
 639    | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true m t s cur_pc
 640
 641 (* NO: solo lettura word/scrittura byte *)
 642    | MODE_INHA_and_IMM1 ⇒ None ?
 643 (* NO: solo lettura word/scrittura byte *)
 644    | MODE_INHX_and_IMM1 ⇒ None ?
 645 (* NO: solo lettura word *)
 646    | MODE_IMM1_and_IMM1 ⇒ None ?
 647 (* NO: solo lettura word/scrittura byte *)
 648    | MODE_DIR1_and_IMM1 ⇒ None ?
 649 (* NO: solo lettura word/scrittura byte *)
 650    | MODE_IX0_and_IMM1  ⇒ None ?
 651 (* NO: solo lettura word *)
 652    | MODE_IX0p_and_IMM1 ⇒ None ?
 653 (* NO: solo lettura word/scrittura byte *)
 654    | MODE_IX1_and_IMM1  ⇒ None ?
 655 (* NO: solo lettura word *)
 656    | MODE_IX1p_and_IMM1 ⇒ None ?
 657 (* NO: solo lettura word/scrittura byte *)
 658    | MODE_SP1_and_IMM1  ⇒ None ?
 659
 660 (* NO: solo scrittura byte *)
 661    | MODE_DIRn _          ⇒ None ?
 662 (* NO: solo lettura word *)
 663    | MODE_DIRn_and_IMM1 _ ⇒ None ?
 664 (* preleva 1 byte da 0000 0000 0000 xxxxb *)
 665    | MODE_TNY e           ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:〈x0,e〉〉)
 666                              (λb.Some ? (triple ??? s b cur_pc))
 667 (* preleva 1 byte da 0000 0000 000x xxxxb *)
 668    | MODE_SRT e           ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉)
 669                              (λb.Some ? (triple ??? s b cur_pc))
 670    ]
 671 (* lettura di una word *)
 672   | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
 673 (* NO: non ci sono indicazioni *)
 674    [ MODE_INH  ⇒ None ?
 675 (* NO: solo lettura/scrittura byte *)
 676    | MODE_INHA ⇒ None ?
 677 (* NO: solo lettura/scrittura byte *)
 678    | MODE_INHX ⇒ None ?
 679 (* NO: solo lettura/scrittura byte *)
 680    | MODE_INHH ⇒ None ?
 681
 682 (* preleva 1 word immediato *)
 683   | MODE_INHX0ADD ⇒ opt_map ?? (get_IX m t s)
 684                      (λw.Some ? (triple ??? s w cur_pc))
 685 (* preleva 1 word immediato *)
 686   | MODE_INHX1ADD ⇒ mode_IX1ADD_load m t s cur_pc
 687 (* preleva 1 word immediato *)
 688   | MODE_INHX2ADD ⇒ mode_IX2ADD_load m t s cur_pc
 689
 690 (* NO: solo lettura byte *)
 691    | MODE_IMM1 ⇒ None ?
 692 (* preleva 1 word immediato *)
 693    | MODE_IMM1EXT ⇒ mode_IMM1EXT_load m t s cur_pc
 694 (* preleva 1 word immediato *)
 695    | MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
 696 (* preleva 1 word da indirizzo diretto 1 byte *)
 697    | MODE_DIR1 ⇒ mode_DIR1_load false m t s cur_pc
 698 (* preleva 1 word da indirizzo diretto 1 word *)
 699    | MODE_DIR2 ⇒ mode_DIR2_load false m t s cur_pc
 700 (* preleva 1 word da H:X *)
 701    | MODE_IX0  ⇒ mode_IX0_load false m t s cur_pc
 702 (* preleva 1 word da H:X+1 byte offset *)
 703    | MODE_IX1  ⇒ mode_IX1_load false m t s cur_pc
 704 (* preleva 1 word da H:X+1 word offset *)
 705    | MODE_IX2  ⇒ mode_IX2_load false m t s cur_pc
 706 (* preleva 1 word da SP+1 byte offset *)
 707    | MODE_SP1  ⇒ mode_SP1_load false m t s cur_pc
 708 (* preleva 1 word da SP+1 word offset *)
 709    | MODE_SP2  ⇒ mode_SP2_load false m t s cur_pc
 710
 711 (* NO: solo lettura/scrittura byte *)
 712    | MODE_DIR1_to_DIR1 ⇒ None ?
 713 (* NO: solo lettura/scrittura byte *)
 714    | MODE_IMM1_to_DIR1 ⇒ None ?
 715 (* NO: solo lettura/scrittura byte *)
 716    | MODE_IX0p_to_DIR1 ⇒ None ?
 717 (* NO: solo lettura/scrittura byte *)
 718    | MODE_DIR1_to_IX0p ⇒ None ?
 719
 720 (* preleva 2 byte, possibilita' modificare Io argomento *)
 721    | MODE_INHA_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
 722                            (λS_immb_and_PC.match S_immb_and_PC with
 723                             [ triple _ immb cur_pc' ⇒
 724                              Some ? (triple ??? s 〈(get_acc_8_low_reg m t s):immb〉 cur_pc')])
 725 (* preleva 2 byte, possibilita' modificare Io argomento *)
 726    | MODE_INHX_and_IMM1 ⇒ opt_map ?? (get_indX_8_low_reg m t s)
 727                            (λX_op.opt_map ?? (mode_IMM1_load m t s cur_pc)
 728                             (λS_immb_and_PC.match S_immb_and_PC with
 729                              [ triple _ immb cur_pc' ⇒
 730                               Some ? (triple ??? s 〈X_op:immb〉 cur_pc')]))
 731 (* preleva 2 byte, NO possibilita' modificare Io argomento *)
 732    | MODE_IMM1_and_IMM1 ⇒ opt_map ?? (mode_IMM1_load m t s cur_pc)
 733                            (λS_immb1_and_PC.match S_immb1_and_PC with
 734                             [ triple _ immb1 cur_pc' ⇒
 735                              opt_map ?? (mode_IMM1_load m t s cur_pc')
 736                               (λS_immb2_and_PC.match S_immb2_and_PC with
 737                                [ triple _ immb2 cur_pc'' ⇒
 738                                 Some ? (triple ??? s 〈immb1:immb2〉 cur_pc'')])])
 739 (* preleva 2 byte, possibilita' modificare Io argomento *)
 740    | MODE_DIR1_and_IMM1 ⇒ opt_map ?? (mode_DIR1_load true m t s cur_pc)
 741                            (λS_dirb_and_PC.match S_dirb_and_PC with
 742                             [ triple _ dirb cur_pc' ⇒
 743                              opt_map ?? (mode_IMM1_load m t s cur_pc')
 744                               (λS_immb_and_PC.match S_immb_and_PC with
 745                                [ triple _ immb cur_pc'' ⇒
 746                                 Some ? (triple ??? s 〈dirb:immb〉 cur_pc'')])])
 747 (* preleva 2 byte, possibilita' modificare Io argomento *)
 748    | MODE_IX0_and_IMM1  ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
 749                            (λS_ixb_and_PC.match S_ixb_and_PC with
 750                             [ triple _ ixb cur_pc' ⇒
 751                              opt_map ?? (mode_IMM1_load m t s cur_pc')
 752                               (λS_immb_and_PC.match S_immb_and_PC with
 753                                [ triple _ immb cur_pc'' ⇒
 754                                 Some ? (triple ??? s 〈ixb:immb〉 cur_pc'')])])
 755 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
 756    | MODE_IX0p_and_IMM1 ⇒ opt_map ?? (mode_IX0_load true m t s cur_pc)
 757                            (λS_ixb_and_PC.match S_ixb_and_PC with
 758                             [ triple _ ixb cur_pc' ⇒
 759                              opt_map ?? (mode_IMM1_load m t s cur_pc')
 760                               (λS_immb_and_PC.match S_immb_and_PC with
 761                                [ triple _ immb cur_pc'' ⇒
 762                                 (* H:X++ *)
 763                                 opt_map ?? (aux_inc_indX_16 m t s)
 764                                  (λs'.Some ? (triple ??? s' 〈ixb:immb〉 cur_pc''))])])
 765 (* preleva 2 byte, possibilita' modificare Io argomento *)
 766    | MODE_IX1_and_IMM1  ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
 767                            (λS_ixb_and_PC.match S_ixb_and_PC with
 768                             [ triple _ ixb cur_pc' ⇒
 769                              opt_map ?? (mode_IMM1_load m t s cur_pc')
 770                               (λS_immb_and_PC.match S_immb_and_PC with
 771                                [ triple _ immb cur_pc'' ⇒
 772                                 Some ? (triple ??? s 〈ixb:immb〉 cur_pc'')])])
 773 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
 774    | MODE_IX1p_and_IMM1 ⇒ opt_map ?? (mode_IX1_load true m t s cur_pc)
 775                            (λS_ixb_and_PC.match S_ixb_and_PC with
 776                             [ triple _ ixb cur_pc' ⇒
 777                              opt_map ?? (mode_IMM1_load m t s cur_pc')
 778                               (λS_immb_and_PC.match S_immb_and_PC with
 779                                [ triple _ immb cur_pc'' ⇒
 780                                 (* H:X++ *)
 781                                 opt_map ?? (aux_inc_indX_16 m t s)
 782                                  (λs'.Some ? (triple ??? s' 〈ixb:immb〉 cur_pc''))])])
 783 (* preleva 2 byte, possibilita' modificare Io argomento *)
 784    | MODE_SP1_and_IMM1  ⇒ opt_map ?? (mode_SP1_load true m t s cur_pc)
 785                            (λS_spb_and_PC.match S_spb_and_PC with
 786                             [ triple _ spb cur_pc' ⇒
 787                              opt_map ?? (mode_IMM1_load m t s cur_pc')
 788                               (λS_immb_and_PC.match S_immb_and_PC with
 789                                [ triple _ immb cur_pc'' ⇒
 790                                 Some ? (triple ??? s 〈spb:immb〉 cur_pc'')])])
 791
 792 (* NO: solo scrittura byte *)
 793    | MODE_DIRn _            ⇒ None ?
 794 (* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
 795    | MODE_DIRn_and_IMM1 msk ⇒ opt_map ?? (mode_DIR1n_load m t s cur_pc msk)
 796                                (λS_dirbn_and_PC.match S_dirbn_and_PC with
 797                                 [ triple _ dirbn cur_pc'   ⇒
 798                                  opt_map ?? (mode_IMM1_load m t s cur_pc')
 799                                   (λS_immb_and_PC.match S_immb_and_PC with
 800                                    [ triple _ immb cur_pc'' ⇒
 801                                      Some ? (triple ??? s 〈〈x0,match dirbn with [ true ⇒ x1 | false ⇒ x0 ]〉:immb〉 cur_pc'') ])])
 802 (* NO: solo lettura/scrittura byte *)
 803    | MODE_TNY _             ⇒ None ?
 804 (* NO: solo lettura/scrittura byte *)
 805    | MODE_SRT _             ⇒ None ?
 806    ]
 807   ].
 808
 809 (* **************************************** *)
 810 (* raccordo di tutte le possibili scritture *)
 811 (* **************************************** *)
 812
 813 (* tutte le modalita' di scrittura: true=writeb, false=writew *)
 814 ndefinition multi_mode_write ≝
 815 λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
 816  return λbyteflag:bool.any_status m t → word16 → instr_mode →
 817   match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
 818   option (ProdT (any_status m t) word16) with
 819  (* scrittura di un byte *)
 820  [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwriteb:byte8.match i with
 821 (* NO: non ci sono indicazioni *)
 822   [ MODE_INH        ⇒ None ?
 823 (* scrive A *)
 824   | MODE_INHA       ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
 825 (* scrive X *)
 826   | MODE_INHX       ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
 827                       (λtmps.Some ? (pair ?? tmps cur_pc))
 828 (* scrive H *)
 829   | MODE_INHH       ⇒ opt_map ?? (set_indX_8_high_reg m t s writeb)
 830                        (λtmps.Some ? (pair ?? tmps cur_pc))
 831
 832 (* NO: solo lettura word *)
 833   | MODE_INHX0ADD ⇒ None ?
 834 (* NO: solo lettura word *)
 835   | MODE_INHX1ADD ⇒ None ?
 836 (* NO: solo lettura word *)
 837   | MODE_INHX2ADD ⇒ None ?
 838
 839 (* NO: solo lettura byte *)
 840   | MODE_IMM1       ⇒ None ?
 841 (* NO: solo lettura word *)
 842   | MODE_IMM1EXT    ⇒ None ?
 843 (* NO: solo lettura word *)
 844   | MODE_IMM2       ⇒ None ?
 845 (* scrive 1 byte su indirizzo diretto 1 byte *)
 846   | MODE_DIR1       ⇒ mode_DIR1_write true m t s cur_pc writeb
 847 (* scrive 1 byte su indirizzo diretto 1 word *)
 848   | MODE_DIR2       ⇒ mode_DIR2_write true m t s cur_pc writeb
 849 (* scrive 1 byte su H:X *)
 850   | MODE_IX0        ⇒ mode_IX0_write true m t s cur_pc writeb
 851 (* scrive 1 byte su H:X+1 byte offset *)
 852   | MODE_IX1        ⇒ mode_IX1_write true m t s cur_pc writeb
 853 (* scrive 1 byte su H:X+1 word offset *)
 854   | MODE_IX2        ⇒ mode_IX2_write true m t s cur_pc writeb
 855 (* scrive 1 byte su SP+1 byte offset *)
 856   | MODE_SP1        ⇒ mode_SP1_write true m t s cur_pc writeb
 857 (* scrive 1 byte su SP+1 word offset *)
 858   | MODE_SP2        ⇒ mode_SP2_write true m t s cur_pc writeb
 859
 860 (* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
 861   | MODE_DIR1_to_DIR1   ⇒ mode_DIR1_write true m t s cur_pc writeb
 862 (* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
 863   | MODE_IMM1_to_DIR1   ⇒ mode_DIR1_write true m t s cur_pc writeb
 864 (* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
 865   | MODE_IX0p_to_DIR1   ⇒ opt_map ?? (mode_DIR1_write true m t s cur_pc writeb)
 866                            (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
 867                             (* H:X++ *)
 868                             opt_map ?? (aux_inc_indX_16 m t S_op)
 869                              (λS_op'.Some ? (pair ?? S_op' PC_op))])
 870 (* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
 871   | MODE_DIR1_to_IX0p   ⇒ opt_map ?? (mode_IX0_write true m t s cur_pc writeb)
 872                            (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
 873                             (* H:X++ *)
 874                             opt_map ?? (aux_inc_indX_16 m t S_op)
 875                              (λS_op'.Some ? (pair ?? S_op' PC_op))])
 876
 877 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
 878   | MODE_INHA_and_IMM1 ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
 879 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)
 880   | MODE_INHX_and_IMM1 ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
 881                            (λtmps.Some ? (pair ?? tmps cur_pc))
 882 (* NO: solo lettura word *)
 883   | MODE_IMM1_and_IMM1 ⇒ None ?
 884 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *)
 885   | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write true m t s cur_pc writeb
 886 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
 887   | MODE_IX0_and_IMM1  ⇒ mode_IX0_write true m t s cur_pc writeb
 888 (* NO: solo lettura word *)
 889   | MODE_IX0p_and_IMM1 ⇒ None ?
 890 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
 891   | MODE_IX1_and_IMM1  ⇒ mode_IX1_write true m t s cur_pc writeb
 892 (* NO: solo lettura word *)
 893   | MODE_IX1p_and_IMM1 ⇒ None ?
 894 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
 895   | MODE_SP1_and_IMM1  ⇒ mode_SP1_write true m t s cur_pc writeb
 896
 897 (* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
 898   | MODE_DIRn msk ⇒ mode_DIR1n_write m t s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))
 899 (* NO: solo lettura word *)
 900   | MODE_DIRn_and_IMM1 _ ⇒ None ?
 901 (* scrive 1 byte su 0000 0000 0000 xxxxb *)
 902   | MODE_TNY e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:〈x0,e〉〉 writeb)
 903                    (λtmps.Some ? (pair ?? tmps cur_pc))
 904 (* scrive 1 byte su 0000 0000 000x xxxxb *)
 905   | MODE_SRT e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉 writeb)
 906                       (λtmps.Some ? (pair ?? tmps cur_pc)) ]
 907  (* scrittura di una word *)
 908  | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwritew:word16.match i with
 909 (* NO: non ci sono indicazioni *)
 910   [ MODE_INH        ⇒ None ?
 911 (* NO: solo lettura/scrittura byte *)
 912   | MODE_INHA       ⇒ None ?
 913 (* NO: solo lettura/scrittura byte *)
 914   | MODE_INHX       ⇒ None ?
 915 (* NO: solo lettura/scrittura byte *)
 916   | MODE_INHH       ⇒ None ?
 917
 918 (* NO: solo lettura word *)
 919   | MODE_INHX0ADD ⇒ None ?
 920 (* NO: solo lettura word *)
 921   | MODE_INHX1ADD ⇒ None ?
 922 (* NO: solo lettura word *)
 923   | MODE_INHX2ADD ⇒ None ?
 924
 925 (* NO: solo lettura byte *)
 926   | MODE_IMM1       ⇒ None ?
 927 (* NO: solo lettura word *)
 928   | MODE_IMM1EXT    ⇒ None ?
 929 (* NO: solo lettura word *)
 930   | MODE_IMM2       ⇒ None ?
 931 (* scrive 1 word su indirizzo diretto 1 byte *)
 932   | MODE_DIR1       ⇒ mode_DIR1_write false m t s cur_pc writew
 933 (* scrive 1 word su indirizzo diretto 1 word *)
 934   | MODE_DIR2       ⇒ mode_DIR2_write false m t s cur_pc writew
 935 (* scrive 1 word su H:X *)
 936   | MODE_IX0        ⇒ mode_IX0_write false m t s cur_pc writew
 937 (* scrive 1 word su H:X+1 byte offset *)
 938   | MODE_IX1        ⇒ mode_IX1_write false m t s cur_pc writew
 939 (* scrive 1 word su H:X+1 word offset *)
 940   | MODE_IX2        ⇒ mode_IX2_write false m t s cur_pc writew
 941 (* scrive 1 word su SP+1 byte offset *)
 942   | MODE_SP1        ⇒ mode_SP1_write false m t s cur_pc writew
 943 (* scrive 1 word su SP+1 word offset *)
 944   | MODE_SP2        ⇒ mode_SP2_write false m t s cur_pc writew
 945
 946 (* NO: solo lettura/scrittura byte *)
 947   | MODE_DIR1_to_DIR1 ⇒ None ?
 948 (* NO: solo lettura/scrittura byte *)
 949   | MODE_IMM1_to_DIR1 ⇒ None ?
 950 (* NO: solo lettura/scrittura byte *)
 951   | MODE_IX0p_to_DIR1 ⇒ None ?
 952 (* NO: solo lettura/scrittura byte *)
 953   | MODE_DIR1_to_IX0p ⇒ None ?
 954
 955 (* NO: solo lettura word/scrittura byte *)
 956   | MODE_INHA_and_IMM1 ⇒ None ?
 957 (* NO: solo lettura word/scrittura byte *)
 958   | MODE_INHX_and_IMM1 ⇒ None ?
 959 (* NO: solo lettura word *)
 960   | MODE_IMM1_and_IMM1 ⇒ None ?
 961 (* NO: solo lettura word/scrittura byte *)
 962   | MODE_DIR1_and_IMM1 ⇒ None ?
 963 (* NO: solo lettura word/scrittura byte *)
 964   | MODE_IX0_and_IMM1  ⇒ None ?
 965 (* NO: solo lettura word *)
 966   | MODE_IX0p_and_IMM1 ⇒ None ?
 967 (* NO: solo lettura word/scrittura byte *)
 968   | MODE_IX1_and_IMM1  ⇒ None ?
 969 (* NO: solo lettura word *)
 970   | MODE_IX1p_and_IMM1 ⇒ None ?
 971 (* NO: solo lettura word/scrittura byte *)
 972   | MODE_SP1_and_IMM1  ⇒ None ?
 973
 974 (* NO: solo scrittura byte *)
 975   | MODE_DIRn _          ⇒ None ?
 976 (* NO: solo lettura word *)
 977   | MODE_DIRn_and_IMM1 _ ⇒ None ?
 978 (* NO: solo lettura/scrittura byte *)
 979   | MODE_TNY _           ⇒ None ?
 980 (* NO: solo lettura/scrittura byte *)
 981   | MODE_SRT _           ⇒ None ?
 982   ]
 983  ].