helm/software/matita/contribs/ng_assembly/emulator/read_write/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 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/status/status_getter.ma".
  24 include "emulator/read_write/load_write_base.ma".
  25
  26 (* lettura da [curpc]: IMM1 *)
  27 ndefinition mode_IMM1_load ≝
  28 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  29  opt_map … (mem_read_s … s (extu_w32 cur_pc))
  30   (λb.Some ? (triple … s b (succ_w16 cur_pc))).
  31
  32 (* lettura da [curpc]: IMM1 + estensione a word *)
  33 ndefinition mode_IMM1EXT_load ≝
  34 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  35  opt_map … (mem_read_s …  s (extu_w32 cur_pc))
  36   (λb.Some ? (triple … s (extu_w16 b) (succ_w16 cur_pc))).
  37
  38 (* lettura da [curpc]: IMM2 *)
  39 ndefinition mode_IMM2_load ≝
  40 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  41  opt_map … (mem_read_s …  s (extu_w32 cur_pc))
  42   (λbh.opt_map … (mem_read_s …  s (extu_w32 (succ_w16 cur_pc)))
  43    (λbl.Some ? (triple … s 〈bh:bl〉 (succ_w16 (succ_w16 cur_pc))))).
  44
  45 (* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
  46 ndefinition mode_DIR1_load ≝
  47 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  48  opt_map … (mem_read_s …  s (extu_w32 cur_pc))
  49   (λaddr.(aux_load m t byteflag) s (extu2_w32 addr) cur_pc x1).
  50
  51 (* lettura da [byte [curpc]]: loadbit *)
  52 ndefinition mode_DIR1n_load ≝
  53 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.
  54  opt_map … (mem_read_s …  s (extu_w32 cur_pc))
  55   (λaddr.loadbit_from … s (extu2_w32 addr) sub cur_pc x1).
  56
  57 (* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
  58 ndefinition mode_DIR1_write ≝
  59 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  60 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  61  opt_map … (mem_read_s …  s (extu_w32 cur_pc))
  62   (λaddr.(aux_write m t byteflag) s (extu2_w32 addr) auxMode_ok cur_pc x1 writebw).
  63
  64 (* scrittura su [byte [curpc]]: writebit *)
  65 ndefinition mode_DIR1n_write ≝
  66 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.λwriteb:bool.
  67  opt_map … (mem_read_s …  s (extu_w32 cur_pc))
  68   (λaddr.writebit_to … s (extu2_w32 addr) sub cur_pc x1 writeb).
  69
  70 (* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
  71 ndefinition mode_DIR2_load ≝
  72 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  73  opt_map … (mem_read_s …  s (extu_w32 cur_pc))
  74   (λaddrh.opt_map … (mem_read_s …  s (extu_w32 (succ_w16 cur_pc)))
  75    (λaddrl.(aux_load m t byteflag) s (extu_w32 〈addrh:addrl〉) cur_pc x2)).
  76
  77 (* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
  78 ndefinition mode_DIR2_write ≝
  79 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  80 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
  81  opt_map … (mem_read_s …  s (extu_w32 cur_pc))
  82   (λaddrh.opt_map … (mem_read_s …  s (extu_w32 (succ_w16 cur_pc)))
  83    (λaddrl.(aux_write m t byteflag) s (extu_w32 〈addrh:addrl〉) auxMode_ok cur_pc x2 writebw)).
  84
  85 ndefinition get_IX ≝
  86 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  87  match m with
  88   [ HC05 ⇒ opt_map … (get_indX_8_low_reg … s) (λindx.Some ? (extu_w16 indx))
  89   | HC08 ⇒ opt_map … (get_indX_16_reg … s) (λindx.Some ? indx)
  90   | HCS08 ⇒ opt_map … (get_indX_16_reg … s) (λindx.Some ? indx)
  91   | RS08 ⇒ None ?
  92   | IP2022 ⇒ None ? ].
  93
  94 (* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
  95 ndefinition mode_IX0_load ≝
  96 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
  97  opt_map … (get_IX … s)
  98   (λaddr.(aux_load m t byteflag) s (extu_w32 addr) cur_pc x0).
  99
 100 (* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
 101 ndefinition mode_IX0_write ≝
 102 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 103 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
 104  opt_map … (get_IX … s)
 105   (λaddr.(aux_write m t byteflag) s (extu_w32 addr) auxMode_ok cur_pc x0 writebw).
 106
 107 (* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
 108 ndefinition mode_IX1_load ≝
 109 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 110  opt_map … (get_IX … s)
 111   (λaddr.opt_map … (mem_read_s …  s (extu_w32 cur_pc))
 112    (λoffs.(aux_load m t byteflag) s (extu_w32 (plus_w16_d_d addr (extu_w16 offs))) cur_pc x1)).
 113
 114 (* lettura da X+[byte curpc] *)
 115 ndefinition mode_IX1ADD_load ≝
 116 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 117  opt_map … (get_IX … s)
 118   (λaddr.opt_map … (mem_read_s …  s (extu_w32 cur_pc))
 119    (λb.Some ? (triple … s (plus_w16_d_d addr (extu_w16 b)) (succ_w16 cur_pc)))).
 120
 121 (* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
 122 ndefinition mode_IX1_write ≝
 123 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 124 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
 125  opt_map … (get_IX … s)
 126   (λaddr.opt_map … (mem_read_s …  s (extu_w32 cur_pc))
 127    (λoffs.(aux_write m t byteflag) s (extu_w32 (plus_w16_d_d addr (extu_w16 offs))) auxMode_ok cur_pc x1 writebw)).
 128
 129 (* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
 130 ndefinition mode_IX2_load ≝
 131 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 132  opt_map … (get_IX … s)
 133   (λaddr.opt_map … (mem_read_s …  s (extu_w32 cur_pc))
 134    (λoffsh.opt_map … (mem_read_s …  s (extu_w32 (succ_w16 cur_pc)))
 135     (λoffsl.(aux_load m t byteflag) s (extu_w32 (plus_w16_d_d addr 〈offsh:offsl〉)) cur_pc x2))).
 136
 137 (* lettura da X+[word curpc] *)
 138 ndefinition mode_IX2ADD_load ≝
 139 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 140  opt_map … (get_IX … s)
 141   (λaddr.opt_map … (mem_read_s …  s (extu_w32 cur_pc))
 142    (λbh.opt_map … (mem_read_s …  s (extu_w32 (succ_w16 cur_pc)))
 143     (λbl.Some ? (triple … s (plus_w16_d_d addr 〈bh:bl〉) (succ_w16 (succ_w16 cur_pc)))))).
 144
 145 (* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
 146 ndefinition mode_IX2_write ≝
 147 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 148 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
 149  opt_map … (get_IX … s)
 150   (λaddr.opt_map … (mem_read_s …  s (extu_w32 cur_pc))
 151    (λoffsh.opt_map … (mem_read_s …  s (extu_w32 (succ_w16 cur_pc)))
 152     (λoffsl.(aux_write m t byteflag) s (extu_w32 (plus_w16_d_d addr 〈offsh:offsl〉)) auxMode_ok cur_pc x2 writebw))).
 153
 154 (* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
 155 ndefinition mode_SP1_load ≝
 156 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 157  opt_map … (get_sp_reg … s)
 158   (λaddr.opt_map … (mem_read_s …  s (extu_w32 cur_pc))
 159    (λoffs.(aux_load m t byteflag) s (extu_w32 (plus_w16_d_d addr (extu_w16 offs))) cur_pc x1)).
 160
 161 (* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
 162 ndefinition mode_SP1_write ≝
 163 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 164 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
 165  opt_map … (get_sp_reg … s)
 166   (λaddr.opt_map … (mem_read_s …  s (extu_w32 cur_pc))
 167    (λoffs.(aux_write m t byteflag) s (extu_w32 (plus_w16_d_d addr (extu_w16 offs))) auxMode_ok cur_pc x1 writebw)).
 168
 169 (* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
 170 ndefinition mode_SP2_load ≝
 171 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 172  opt_map … (get_sp_reg … s)
 173   (λaddr.opt_map … (mem_read_s …  s (extu_w32 cur_pc))
 174    (λoffsh.opt_map … (mem_read_s …  s (extu_w32 (succ_w16 cur_pc)))
 175     (λoffsl.(aux_load m t byteflag) s (extu_w32 (plus_w16_d_d addr 〈offsh:offsl〉)) cur_pc x2))).
 176
 177 (* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
 178 ndefinition mode_SP2_write ≝
 179 λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
 180 λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
 181  opt_map … (get_sp_reg … s)
 182   (λaddr.opt_map … (mem_read_s …  s (extu_w32 cur_pc))
 183    (λoffsh.opt_map … (mem_read_s …  s (extu_w32 (succ_w16 cur_pc)))
 184     (λoffsl.(aux_write m t byteflag) s (extu_w32 (plus_w16_d_d addr 〈offsh:offsl〉)) auxMode_ok cur_pc x2 writebw))).
 185
 186 (* ************************************** *)
 187 (* raccordo di tutte le possibili letture *)
 188 (* ************************************** *)
 189
 190 (* H:X++ *)
 191 ndefinition aux_inc_indX_16 ≝
 192 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 193  opt_map … (get_indX_16_reg m t s)
 194   (λX_op.opt_map … (set_indX_16_reg m t s (succ_w16 X_op))
 195    (λs_tmp.Some ? s_tmp)).
 196
 197 ndefinition Freescale_multi_mode_load_auxb ≝
 198 λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with
 199 (* NO: non ci sono indicazioni *)
 200    [ MODE_INH  ⇒ None ?
 201 (* restituisce A *)
 202    | MODE_INHA ⇒ Some ? (triple … s (get_acc_8_low_reg … s) cur_pc)
 203 (* restituisce X *)
 204    | MODE_INHX ⇒ opt_map … (get_indX_8_low_reg … s)
 205                   (λindx.Some ? (triple … s indx cur_pc))
 206 (* restituisce H *)
 207    | MODE_INHH ⇒ opt_map … (get_indX_8_high_reg … s)
 208                   (λindx.Some ? (triple … s indx cur_pc))
 209
 210 (* NO: solo lettura word *)
 211   | MODE_INHX0ADD ⇒ None ?
 212 (* NO: solo lettura word *)
 213   | MODE_INHX1ADD ⇒ None ?
 214 (* NO: solo lettura word *)
 215   | MODE_INHX2ADD ⇒ None ?
 216
 217 (* preleva 1 byte immediato *)
 218    | MODE_IMM1 ⇒ mode_IMM1_load … s cur_pc
 219 (* NO: solo lettura word *)
 220    | MODE_IMM1EXT ⇒ None ?
 221 (* NO: solo lettura word *)
 222    | MODE_IMM2 ⇒ None ?
 223 (* preleva 1 byte da indirizzo diretto 1 byte *)
 224    | MODE_DIR1 ⇒ mode_DIR1_load true … s cur_pc
 225 (* preleva 1 byte da indirizzo diretto 1 word *)
 226    | MODE_DIR2 ⇒ mode_DIR2_load true … s cur_pc
 227 (* preleva 1 byte da H:X *)
 228    | MODE_IX0  ⇒ mode_IX0_load true … s cur_pc
 229 (* preleva 1 byte da H:X+1 byte offset *)
 230    | MODE_IX1  ⇒ mode_IX1_load true … s cur_pc
 231 (* preleva 1 byte da H:X+1 word offset *)
 232    | MODE_IX2  ⇒ mode_IX2_load true … s cur_pc
 233 (* preleva 1 byte da SP+1 byte offset *)
 234    | MODE_SP1  ⇒ mode_SP1_load true … s cur_pc
 235 (* preleva 1 byte da SP+1 word offset *)
 236    | MODE_SP2  ⇒ mode_SP2_load true … s cur_pc
 237
 238 (* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
 239    | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true … s cur_pc
 240 (* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
 241    | MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load … s cur_pc
 242 (* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
 243    | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load true … s cur_pc
 244 (* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
 245    | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true … s cur_pc
 246
 247 (* NO: solo lettura word/scrittura byte *)
 248    | MODE_INHA_and_IMM1 ⇒ None ?
 249 (* NO: solo lettura word/scrittura byte *)
 250    | MODE_INHX_and_IMM1 ⇒ None ?
 251 (* NO: solo lettura word *)
 252    | MODE_IMM1_and_IMM1 ⇒ None ?
 253 (* NO: solo lettura word/scrittura byte *)
 254    | MODE_DIR1_and_IMM1 ⇒ None ?
 255 (* NO: solo lettura word/scrittura byte *)
 256    | MODE_IX0_and_IMM1  ⇒ None ?
 257 (* NO: solo lettura word *)
 258    | MODE_IX0p_and_IMM1 ⇒ None ?
 259 (* NO: solo lettura word/scrittura byte *)
 260    | MODE_IX1_and_IMM1  ⇒ None ?
 261 (* NO: solo lettura word *)
 262    | MODE_IX1p_and_IMM1 ⇒ None ?
 263 (* NO: solo lettura word/scrittura byte *)
 264    | MODE_SP1_and_IMM1  ⇒ None ?
 265
 266 (* NO: solo scrittura byte *)
 267    | MODE_DIRn _          ⇒ None ?
 268 (* NO: solo lettura word *)
 269    | MODE_DIRn_and_IMM1 _ ⇒ None ?
 270 (* preleva 1 byte da 0000 0000 0000 xxxxb *)
 271    | MODE_TNY e           ⇒ opt_map … (memory_filter_read … s (extu3_w32 e))
 272                              (λb.Some ? (triple … s b cur_pc))
 273 (* preleva 1 byte da 0000 0000 000x xxxxb *)
 274    | MODE_SRT e           ⇒ opt_map … (memory_filter_read … s (extu2_w32 (b8_of_bit e)))
 275                              (λb.Some ? (triple … s b cur_pc))
 276    ].
 277
 278 ndefinition Freescale_multi_mode_load_auxw ≝
 279 λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with
 280 (* NO: non ci sono indicazioni *)
 281    [ MODE_INH  ⇒ None ?
 282 (* NO: solo lettura/scrittura byte *)
 283    | MODE_INHA ⇒ None ?
 284 (* NO: solo lettura/scrittura byte *)
 285    | MODE_INHX ⇒ None ?
 286 (* NO: solo lettura/scrittura byte *)
 287    | MODE_INHH ⇒ None ?
 288
 289 (* preleva 1 word immediato *)
 290   | MODE_INHX0ADD ⇒ opt_map … (get_IX … s)
 291                      (λw.Some ? (triple … s w cur_pc))
 292 (* preleva 1 word immediato *)
 293   | MODE_INHX1ADD ⇒ mode_IX1ADD_load … s cur_pc
 294 (* preleva 1 word immediato *)
 295   | MODE_INHX2ADD ⇒ mode_IX2ADD_load … s cur_pc
 296
 297 (* NO: solo lettura byte *)
 298    | MODE_IMM1 ⇒ None ?
 299 (* preleva 1 word immediato *)
 300    | MODE_IMM1EXT ⇒ mode_IMM1EXT_load … s cur_pc
 301 (* preleva 1 word immediato *)
 302    | MODE_IMM2 ⇒ mode_IMM2_load … s cur_pc
 303 (* preleva 1 word da indirizzo diretto 1 byte *)
 304    | MODE_DIR1 ⇒ mode_DIR1_load false … s cur_pc
 305 (* preleva 1 word da indirizzo diretto 1 word *)
 306    | MODE_DIR2 ⇒ mode_DIR2_load false … s cur_pc
 307 (* preleva 1 word da H:X *)
 308    | MODE_IX0  ⇒ mode_IX0_load false … s cur_pc
 309 (* preleva 1 word da H:X+1 byte offset *)
 310    | MODE_IX1  ⇒ mode_IX1_load false … s cur_pc
 311 (* preleva 1 word da H:X+1 word offset *)
 312    | MODE_IX2  ⇒ mode_IX2_load false … s cur_pc
 313 (* preleva 1 word da SP+1 byte offset *)
 314    | MODE_SP1  ⇒ mode_SP1_load false … s cur_pc
 315 (* preleva 1 word da SP+1 word offset *)
 316    | MODE_SP2  ⇒ mode_SP2_load false … s cur_pc
 317
 318 (* NO: solo lettura/scrittura byte *)
 319    | MODE_DIR1_to_DIR1 ⇒ None ?
 320 (* NO: solo lettura/scrittura byte *)
 321    | MODE_IMM1_to_DIR1 ⇒ None ?
 322 (* NO: solo lettura/scrittura byte *)
 323    | MODE_IX0p_to_DIR1 ⇒ None ?
 324 (* NO: solo lettura/scrittura byte *)
 325    | MODE_DIR1_to_IX0p ⇒ None ?
 326
 327 (* preleva 2 byte, possibilita' modificare Io argomento *)
 328    | MODE_INHA_and_IMM1 ⇒ opt_map … (mode_IMM1_load … s cur_pc)
 329                            (λS_immb_and_PC.match S_immb_and_PC with
 330                             [ triple _ immb cur_pc' ⇒
 331                              Some ? (triple … s 〈(get_acc_8_low_reg … s):immb〉 cur_pc')])
 332 (* preleva 2 byte, possibilita' modificare Io argomento *)
 333    | MODE_INHX_and_IMM1 ⇒ opt_map … (get_indX_8_low_reg … s)
 334                            (λX_op.opt_map … (mode_IMM1_load … s cur_pc)
 335                             (λS_immb_and_PC.match S_immb_and_PC with
 336                              [ triple _ immb cur_pc' ⇒
 337                               Some ? (triple … s 〈X_op:immb〉 cur_pc')]))
 338 (* preleva 2 byte, NO possibilita' modificare Io argomento *)
 339    | MODE_IMM1_and_IMM1 ⇒ opt_map … (mode_IMM1_load … s cur_pc)
 340                            (λS_immb1_and_PC.match S_immb1_and_PC with
 341                             [ triple _ immb1 cur_pc' ⇒
 342                              opt_map … (mode_IMM1_load … s cur_pc')
 343                               (λS_immb2_and_PC.match S_immb2_and_PC with
 344                                [ triple _ immb2 cur_pc'' ⇒
 345                                 Some ? (triple … s 〈immb1:immb2〉 cur_pc'')])])
 346 (* preleva 2 byte, possibilita' modificare Io argomento *)
 347    | MODE_DIR1_and_IMM1 ⇒ opt_map … (mode_DIR1_load true … s cur_pc)
 348                            (λS_dirb_and_PC.match S_dirb_and_PC with
 349                             [ triple _ dirb cur_pc' ⇒
 350                              opt_map … (mode_IMM1_load … s cur_pc')
 351                               (λS_immb_and_PC.match S_immb_and_PC with
 352                                [ triple _ immb cur_pc'' ⇒
 353                                 Some ? (triple … s 〈dirb:immb〉 cur_pc'')])])
 354 (* preleva 2 byte, possibilita' modificare Io argomento *)
 355    | MODE_IX0_and_IMM1  ⇒ opt_map … (mode_IX0_load true … s cur_pc)
 356                            (λS_ixb_and_PC.match S_ixb_and_PC with
 357                             [ triple _ ixb cur_pc' ⇒
 358                              opt_map … (mode_IMM1_load … s cur_pc')
 359                               (λS_immb_and_PC.match S_immb_and_PC with
 360                                [ triple _ immb cur_pc'' ⇒
 361                                 Some ? (triple … s 〈ixb:immb〉 cur_pc'')])])
 362 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
 363    | MODE_IX0p_and_IMM1 ⇒ opt_map … (mode_IX0_load true … s cur_pc)
 364                            (λS_ixb_and_PC.match S_ixb_and_PC with
 365                             [ triple _ ixb cur_pc' ⇒
 366                              opt_map … (mode_IMM1_load … s cur_pc')
 367                               (λS_immb_and_PC.match S_immb_and_PC with
 368                                [ triple _ immb cur_pc'' ⇒
 369                                 (* H:X++ *)
 370                                 opt_map … (aux_inc_indX_16 … s)
 371                                  (λs'.Some ? (triple … s' 〈ixb:immb〉 cur_pc''))])])
 372 (* preleva 2 byte, possibilita' modificare Io argomento *)
 373    | MODE_IX1_and_IMM1  ⇒ opt_map … (mode_IX1_load true … s cur_pc)
 374                            (λS_ixb_and_PC.match S_ixb_and_PC with
 375                             [ triple _ ixb cur_pc' ⇒
 376                              opt_map … (mode_IMM1_load … s cur_pc')
 377                               (λS_immb_and_PC.match S_immb_and_PC with
 378                                [ triple _ immb cur_pc'' ⇒
 379                                 Some ? (triple … s 〈ixb:immb〉 cur_pc'')])])
 380 (* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
 381    | MODE_IX1p_and_IMM1 ⇒ opt_map … (mode_IX1_load true … s cur_pc)
 382                            (λS_ixb_and_PC.match S_ixb_and_PC with
 383                             [ triple _ ixb cur_pc' ⇒
 384                              opt_map … (mode_IMM1_load … s cur_pc')
 385                               (λS_immb_and_PC.match S_immb_and_PC with
 386                                [ triple _ immb cur_pc'' ⇒
 387                                 (* H:X++ *)
 388                                 opt_map … (aux_inc_indX_16 … s)
 389                                  (λs'.Some ? (triple … s' 〈ixb:immb〉 cur_pc''))])])
 390 (* preleva 2 byte, possibilita' modificare Io argomento *)
 391    | MODE_SP1_and_IMM1  ⇒ opt_map … (mode_SP1_load true … s cur_pc)
 392                            (λS_spb_and_PC.match S_spb_and_PC with
 393                             [ triple _ spb cur_pc' ⇒
 394                              opt_map … (mode_IMM1_load … s cur_pc')
 395                               (λS_immb_and_PC.match S_immb_and_PC with
 396                                [ triple _ immb cur_pc'' ⇒
 397                                 Some ? (triple … s 〈spb:immb〉 cur_pc'')])])
 398
 399 (* NO: solo scrittura byte *)
 400    | MODE_DIRn _            ⇒ None ?
 401 (* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
 402    | MODE_DIRn_and_IMM1 msk ⇒ opt_map … (mode_DIR1n_load … s cur_pc msk)
 403                                (λS_dirbn_and_PC.match S_dirbn_and_PC with
 404                                 [ triple _ dirbn cur_pc'   ⇒
 405                                  opt_map … (mode_IMM1_load … s cur_pc')
 406                                   (λS_immb_and_PC.match S_immb_and_PC with
 407                                    [ triple _ immb cur_pc'' ⇒
 408                                      Some ? (triple … s 〈〈x0,match dirbn with [ true ⇒ x1 | false ⇒ x0 ]〉:immb〉 cur_pc'') ])])
 409 (* NO: solo lettura/scrittura byte *)
 410    | MODE_TNY _             ⇒ None ?
 411 (* NO: solo lettura/scrittura byte *)
 412    | MODE_SRT _             ⇒ None ?
 413    ].
 414
 415 (* **************************************** *)
 416 (* raccordo di tutte le possibili scritture *)
 417 (* **************************************** *)
 418
 419 ndefinition Freescale_multi_mode_write_auxb ≝
 420 λm,t.λs:any_status m t.λcur_pc:word16.λflag:aux_mod_type.λi:Freescale_instr_mode.λwriteb:byte8.match i with
 421 (* NO: non ci sono indicazioni *)
 422   [ MODE_INH        ⇒ None ?
 423 (* scrive A *)
 424   | MODE_INHA       ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
 425 (* scrive X *)
 426   | MODE_INHX       ⇒ opt_map … (set_indX_8_low_reg … s writeb)
 427                       (λtmps.Some ? (pair … tmps cur_pc))
 428 (* scrive H *)
 429   | MODE_INHH       ⇒ opt_map … (set_indX_8_high_reg … s writeb)
 430                        (λtmps.Some ? (pair … tmps cur_pc))
 431
 432 (* NO: solo lettura word *)
 433   | MODE_INHX0ADD ⇒ None ?
 434 (* NO: solo lettura word *)
 435   | MODE_INHX1ADD ⇒ None ?
 436 (* NO: solo lettura word *)
 437   | MODE_INHX2ADD ⇒ None ?
 438
 439 (* NO: solo lettura byte *)
 440   | MODE_IMM1       ⇒ None ?
 441 (* NO: solo lettura word *)
 442   | MODE_IMM1EXT    ⇒ None ?
 443 (* NO: solo lettura word *)
 444   | MODE_IMM2       ⇒ None ?
 445 (* scrive 1 byte su indirizzo diretto 1 byte *)
 446   | MODE_DIR1       ⇒ mode_DIR1_write true … s cur_pc writeb
 447 (* scrive 1 byte su indirizzo diretto 1 word *)
 448   | MODE_DIR2       ⇒ mode_DIR2_write true … s cur_pc writeb
 449 (* scrive 1 byte su H:X *)
 450   | MODE_IX0        ⇒ mode_IX0_write true … s cur_pc writeb
 451 (* scrive 1 byte su H:X+1 byte offset *)
 452   | MODE_IX1        ⇒ mode_IX1_write true … s cur_pc writeb
 453 (* scrive 1 byte su H:X+1 word offset *)
 454   | MODE_IX2        ⇒ mode_IX2_write true … s cur_pc writeb
 455 (* scrive 1 byte su SP+1 byte offset *)
 456   | MODE_SP1        ⇒ mode_SP1_write true … s cur_pc writeb
 457 (* scrive 1 byte su SP+1 word offset *)
 458   | MODE_SP2        ⇒ mode_SP2_write true … s cur_pc writeb
 459
 460 (* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
 461   | MODE_DIR1_to_DIR1   ⇒ mode_DIR1_write true … s cur_pc writeb
 462 (* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
 463   | MODE_IMM1_to_DIR1   ⇒ mode_DIR1_write true … s cur_pc writeb
 464 (* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
 465   | MODE_IX0p_to_DIR1   ⇒ opt_map … (mode_DIR1_write true … s cur_pc writeb)
 466                            (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
 467                             (* H:X++ *)
 468                             opt_map … (aux_inc_indX_16 … S_op)
 469                              (λS_op'.Some ? (pair … S_op' PC_op))])
 470 (* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
 471   | MODE_DIR1_to_IX0p   ⇒ opt_map … (mode_IX0_write true … s cur_pc writeb)
 472                            (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
 473                             (* H:X++ *)
 474                             opt_map … (aux_inc_indX_16 … S_op)
 475                              (λS_op'.Some ? (pair … S_op' PC_op))])
 476
 477 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
 478   | MODE_INHA_and_IMM1 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
 479 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)
 480   | MODE_INHX_and_IMM1 ⇒ opt_map … (set_indX_8_low_reg … s writeb)
 481                            (λtmps.Some ? (pair … tmps cur_pc))
 482 (* NO: solo lettura word *)
 483   | MODE_IMM1_and_IMM1 ⇒ None ?
 484 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *)
 485   | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write true … s cur_pc writeb
 486 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
 487   | MODE_IX0_and_IMM1  ⇒ mode_IX0_write true … s cur_pc writeb
 488 (* NO: solo lettura word *)
 489   | MODE_IX0p_and_IMM1 ⇒ None ?
 490 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
 491   | MODE_IX1_and_IMM1  ⇒ mode_IX1_write true … s cur_pc writeb
 492 (* NO: solo lettura word *)
 493   | MODE_IX1p_and_IMM1 ⇒ None ?
 494 (* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
 495   | MODE_SP1_and_IMM1  ⇒ mode_SP1_write true … s cur_pc writeb
 496
 497 (* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
 498   | MODE_DIRn msk ⇒ mode_DIR1n_write … s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))
 499 (* NO: solo lettura word *)
 500   | MODE_DIRn_and_IMM1 _ ⇒ None ?
 501 (* scrive 1 byte su 0000 0000 0000 xxxxb *)
 502   | MODE_TNY e ⇒ opt_map … (memory_filter_write … s (extu3_w32 e) auxMode_ok writeb)
 503                    (λtmps.Some ? (pair … tmps cur_pc))
 504 (* scrive 1 byte su 0000 0000 000x xxxxb *)
 505   | MODE_SRT e ⇒ opt_map … (memory_filter_write … s (extu2_w32 (b8_of_bit e)) auxMode_ok writeb)
 506                       (λtmps.Some ? (pair … tmps cur_pc))
 507   ].
 508
 509 ndefinition Freescale_multi_mode_write_auxw ≝
 510 λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.λwritew:word16.match i with
 511 (* NO: non ci sono indicazioni *)
 512   [ MODE_INH        ⇒ None ?
 513 (* NO: solo lettura/scrittura byte *)
 514   | MODE_INHA       ⇒ None ?
 515 (* NO: solo lettura/scrittura byte *)
 516   | MODE_INHX       ⇒ None ?
 517 (* NO: solo lettura/scrittura byte *)
 518   | MODE_INHH       ⇒ None ?
 519
 520 (* NO: solo lettura word *)
 521   | MODE_INHX0ADD ⇒ None ?
 522 (* NO: solo lettura word *)
 523   | MODE_INHX1ADD ⇒ None ?
 524 (* NO: solo lettura word *)
 525   | MODE_INHX2ADD ⇒ None ?
 526
 527 (* NO: solo lettura byte *)
 528   | MODE_IMM1       ⇒ None ?
 529 (* NO: solo lettura word *)
 530   | MODE_IMM1EXT    ⇒ None ?
 531 (* NO: solo lettura word *)
 532   | MODE_IMM2       ⇒ None ?
 533 (* scrive 1 word su indirizzo diretto 1 byte *)
 534   | MODE_DIR1       ⇒ mode_DIR1_write false … s cur_pc writew
 535 (* scrive 1 word su indirizzo diretto 1 word *)
 536   | MODE_DIR2       ⇒ mode_DIR2_write false … s cur_pc writew
 537 (* scrive 1 word su H:X *)
 538   | MODE_IX0        ⇒ mode_IX0_write false … s cur_pc writew
 539 (* scrive 1 word su H:X+1 byte offset *)
 540   | MODE_IX1        ⇒ mode_IX1_write false … s cur_pc writew
 541 (* scrive 1 word su H:X+1 word offset *)
 542   | MODE_IX2        ⇒ mode_IX2_write false … s cur_pc writew
 543 (* scrive 1 word su SP+1 byte offset *)
 544   | MODE_SP1        ⇒ mode_SP1_write false … s cur_pc writew
 545 (* scrive 1 word su SP+1 word offset *)
 546   | MODE_SP2        ⇒ mode_SP2_write false … s cur_pc writew
 547
 548 (* NO: solo lettura/scrittura byte *)
 549   | MODE_DIR1_to_DIR1 ⇒ None ?
 550 (* NO: solo lettura/scrittura byte *)
 551   | MODE_IMM1_to_DIR1 ⇒ None ?
 552 (* NO: solo lettura/scrittura byte *)
 553   | MODE_IX0p_to_DIR1 ⇒ None ?
 554 (* NO: solo lettura/scrittura byte *)
 555   | MODE_DIR1_to_IX0p ⇒ None ?
 556
 557 (* NO: solo lettura word/scrittura byte *)
 558   | MODE_INHA_and_IMM1 ⇒ None ?
 559 (* NO: solo lettura word/scrittura byte *)
 560   | MODE_INHX_and_IMM1 ⇒ None ?
 561 (* NO: solo lettura word *)
 562   | MODE_IMM1_and_IMM1 ⇒ None ?
 563 (* NO: solo lettura word/scrittura byte *)
 564   | MODE_DIR1_and_IMM1 ⇒ None ?
 565 (* NO: solo lettura word/scrittura byte *)
 566   | MODE_IX0_and_IMM1  ⇒ None ?
 567 (* NO: solo lettura word *)
 568   | MODE_IX0p_and_IMM1 ⇒ None ?
 569 (* NO: solo lettura word/scrittura byte *)
 570   | MODE_IX1_and_IMM1  ⇒ None ?
 571 (* NO: solo lettura word *)
 572   | MODE_IX1p_and_IMM1 ⇒ None ?
 573 (* NO: solo lettura word/scrittura byte *)
 574   | MODE_SP1_and_IMM1  ⇒ None ?
 575
 576 (* NO: solo scrittura byte *)
 577   | MODE_DIRn _          ⇒ None ?
 578 (* NO: solo lettura word *)
 579   | MODE_DIRn_and_IMM1 _ ⇒ None ?
 580 (* NO: solo lettura/scrittura byte *)
 581   | MODE_TNY _           ⇒ None ?
 582 (* NO: solo lettura/scrittura byte *)
 583   | MODE_SRT _           ⇒ None ?
 584   ].