helm/software/matita/contribs/ng_assembly/freescale/load_write.ma

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