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