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