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