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