helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_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 [OLD PC<<1 + 1] : argomento non caricato dal fetch word-aligned *)
  27 ndefinition mode_IMM1_load ≝
  28 λt:memory_impl.λs:any_status IP2022 t.
  29  mem_read_s … s (rol_w32 〈〈〈x8,x1〉:〈x0,x0〉〉.(get_pc_reg … s)〉).
  30
  31 (* SCHEMA:
  32    ADDRX=0x00 [ADDRH|ADDRL] 16Kb PROGRAM RAM
  33    ADDRX=0x01 [ADDRH|ADDRL] 64Kb FLASH
  34    ADDRX=0x80 [ADDRH|ADDRL] 64Kb EXTERNAL RAM
  35    ADDRX=0x81 [ADDRH|ADDRL] 64Kb EXTERNAL RAM *)
  36
  37 (* lettura da [ADDR] *)
  38 ndefinition mode_ADDR_load ≝
  39 λt:memory_impl.λs:any_status IP2022 t.
  40  opt_map … (get_addr_reg … s)
  41   (λaddr.match (eq_b8 (w24x addr) 〈x0,x1〉) ⊗ (le_w16 (pred_w16 (get_pc_reg … s)) 〈〈x1,xF〉:〈xF,xF〉〉) with
  42    (* lettura della FLASH da codice in RAM : operazione non bloccante non implementata! *)
  43    [ true ⇒ None ?
  44    | false ⇒ opt_map … (memory_filter_read … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(clrLSB_b8 (w24l addr))〉〉)
  45              (λbh.opt_map … (memory_filter_read … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(setLSB_b8 (w24l addr))〉〉)
  46               (λbl.Some ? 〈bh:bl〉))]).
  47
  48 (* scrittura su [ADDR] *)
  49 ndefinition mode_ADDR_write ≝
  50 λt:memory_impl.λs:any_status IP2022 t.λval:word16.
  51  opt_map … (get_addr_reg … s)
  52   (λaddr.opt_map … (memory_filter_write … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(clrLSB_b8 (w24l addr))〉〉 auxMode_ok (cnH ? val))
  53    (λs'.memory_filter_write … s' 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(setLSB_b8 (w24l addr))〉〉 auxMode_ok (cnL ? val))).
  54
  55 (* IMM1 > 0 : lettura/scrittura da [IMM1] *)
  56 (* else     : lettura/scrittura da [IP] : IP ≥ 0x20 *)
  57 ndefinition mode_DIR1IP_aux ≝
  58 λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T.
  59  opt_map … (mode_IMM1_load t s)
  60   (λaddr.match eq_b8 addr 〈x0,x0〉 with
  61    (* xxxxxxx0 00000000 → [IP] *)
  62    [ true ⇒ opt_map … (get_ip_reg … s)
  63              (λip.match ge_w16 ip 〈〈x0,x0〉:〈x2,x0〉〉 with
  64               (* IP ≥ 0x20 *)
  65               [ true ⇒ f (extu_w32 ip)
  66               | false ⇒ None ? ])
  67    (* xxxxxxx0 nnnnnnnn → [IMM1] *)
  68    | false ⇒ f (extu2_w32 addr)
  69    ]).
  70
  71 (* IMM1 < 0x80 : lettura/scrittura da [DP+IMM1] : DP+IMM1 ≥ 0x20 *)
  72 (* else        : lettura/scrittura da [SP+IMM1] : SP+IMM1 ≥ 0x20 *)
  73 ndefinition mode_DPSP_aux ≝
  74 λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T.
  75  opt_map … (mode_IMM1_load t s)
  76   (λaddr.opt_map … (match getMSB_b8 addr with
  77                     (* xxxxxxx1 1nnnnnnn → [SP+IMM1] *)
  78                     [ true ⇒ get_sp_reg … s
  79                     (* xxxxxxx1 0nnnnnnn → [DP+IMM1] *)
  80                     | false ⇒ get_dp_reg … s ])
  81    (λreg.match ge_w16 (plus_w16_d_d reg (extu_w16 (clrMSB_b8 addr))) 〈〈x0,x0〉:〈x2,x0〉〉 with
  82     (* reg+IMM1 ≥ 0x20 *)
  83     [ true ⇒ f (extu_w32 (plus_w16_d_d reg (extu_w16 (clrMSB_b8 addr))))
  84     | false ⇒ None ? ])).
  85
  86 (* FR0 *)
  87 ndefinition mode_FR0_load ≝
  88 λt:memory_impl.λs:any_status IP2022 t.
  89  mode_DIR1IP_aux t s byte8 (memory_filter_read … s).
  90
  91 ndefinition mode_FR0n_load ≝
  92 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
  93  mode_DIR1IP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
  94
  95 ndefinition mode_FR0_write ≝
  96 λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
  97  mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
  98
  99 ndefinition mode_FR0n_write ≝
 100 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
 101  mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
 102
 103 (* FR1 *)
 104 ndefinition mode_FR1_load ≝
 105 λt:memory_impl.λs:any_status IP2022 t.
 106  mode_DPSP_aux t s byte8 (memory_filter_read … s).
 107
 108 ndefinition mode_FR1n_load ≝
 109 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
 110  mode_DPSP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
 111
 112 ndefinition mode_FR1_write ≝
 113 λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
 114  mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
 115
 116 ndefinition mode_FR1n_write ≝
 117 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
 118  mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
 119
 120 (* ************************************** *)
 121 (* raccordo di tutte le possibili letture *)
 122 (* ************************************** *)
 123
 124 (* addr+=2 *)
 125 ndefinition aux_inc_addr2 ≝
 126 λt:memory_impl.λs:any_status IP2022 t.
 127  set_addr_reg_sIP2022 t s (succ_w24 (succ_w24 (get_addr_reg_IP2022 (alu … s)))).
 128
 129 ndefinition IP2022_multi_mode_load_auxb ≝
 130 λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.match i with
 131 (* NO: non ci sono indicazioni *)
 132    [ MODE_INH ⇒ None ?
 133 (* NO: solo word *)
 134    | MODE_INHADDR ⇒ None ?
 135 (* NO: solo word *)
 136    | MODE_INHADDRpp ⇒ None ?
 137
 138 (* IMM3 *)
 139    | MODE_IMM3 o ⇒ Some ? (triple … s (extu_b8 (ex_of_oct o)) cur_pc)
 140 (* IMM8 *)
 141    | MODE_IMM8 ⇒ opt_map … (mode_IMM1_load t s)
 142                   (λb.Some ? (triple … s b cur_pc))
 143 (* NO: solo lettura word *)
 144    | MODE_IMM13 _ ⇒ None ?
 145
 146 (* NO: solo word *)
 147    | MODE_FR0_and_W ⇒ None ?
 148 (* NO: solo word *)
 149    | MODE_FR1_and_W ⇒ None ?
 150 (* NO: solo word *)
 151    | MODE_W_and_FR0 ⇒ None ?
 152 (* NO: solo word *)
 153    | MODE_W_and_FR1 ⇒ None ?
 154
 155 (* [FRn] *)
 156    | MODE_FR0n o ⇒ opt_map … (mode_FR0n_load t s o)
 157                     (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc))
 158 (* [FRn] *)
 159    | MODE_FR1n o ⇒ opt_map … (mode_FR1n_load t s o)
 160                     (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc))
 161    ].
 162
 163 ndefinition IP2022_multi_mode_load_auxw ≝
 164 λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.match i with
 165 (* NO: non ci sono indicazioni *)
 166    [ MODE_INH ⇒ None ?
 167 (* [ADDR] *)
 168    | MODE_INHADDR ⇒ opt_map … (mode_ADDR_load t s)
 169                      (λw.Some ? (triple … s w cur_pc))
 170 (* [ADDR], ADDR+=2 *)
 171    | MODE_INHADDRpp ⇒ opt_map … (mode_ADDR_load t s)
 172                        (λw.Some ? (triple … (aux_inc_addr2 t s) w cur_pc))
 173
 174 (* NO: solo lettura byte *)
 175    | MODE_IMM3 _ ⇒ None ?
 176 (* NO: solo lettura byte *)
 177    | MODE_IMM8 ⇒ None ?
 178 (* IMM13 *)
 179    | MODE_IMM13 bt ⇒ opt_map … (mode_IMM1_load t s)
 180                       (λb.Some ? (triple … s 〈(b8_of_bit bt):b〉 cur_pc))
 181
 182 (* FR, W → FR *)
 183    | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_load t s)
 184                        (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc))
 185 (* FR, W → FR *)
 186    | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_load t s)
 187                        (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc))
 188 (* W, FR → W *)
 189    | MODE_W_and_FR0 ⇒ opt_map … (mode_FR0_load t s)
 190                        (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc))
 191 (* W, FR → W *)
 192    | MODE_W_and_FR1 ⇒ opt_map … (mode_FR1_load t s)
 193                        (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc))
 194
 195 (* NO: solo byte *)
 196    | MODE_FR0n _ ⇒ None ?
 197 (* NO: solo byte *)
 198    | MODE_FR1n _ ⇒ None ?
 199    ].
 200
 201 (* **************************************** *)
 202 (* raccordo di tutte le possibili scritture *)
 203 (* **************************************** *)
 204
 205 ndefinition IP2022_multi_mode_write_auxb ≝
 206 λt.λs:any_status IP2022 t.λcur_pc:word16.λflag:aux_mod_type.λi:IP2022_instr_mode.λwriteb:byte8.match i with
 207 (* NO: non ci sono indicazioni *)
 208    [ MODE_INH ⇒ None ?
 209 (* NO: solo word *)
 210    | MODE_INHADDR ⇒ None ?
 211 (* NO: solo word *)
 212    | MODE_INHADDRpp ⇒ None ?
 213
 214 (* NO: solo lettura byte *)
 215    | MODE_IMM3 _ ⇒ None ?
 216 (* NO: solo lettura byte *)
 217    | MODE_IMM8 ⇒ None ?
 218 (* NO: solo lettura word *)
 219    | MODE_IMM13 _ ⇒ None ?
 220
 221 (* FR, W → FR *)
 222    | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_write t s flag writeb)
 223                        (λs'.Some ? (pair … s' cur_pc))
 224 (* FR, W → FR *)
 225    | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_write t s flag writeb)
 226                        (λs'.Some ? (pair … s' cur_pc))
 227 (* W, FR → W *)
 228    | MODE_W_and_FR0 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
 229 (* W, FR → W *)
 230    | MODE_W_and_FR1 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
 231
 232 (* [FRn] *)
 233    | MODE_FR0n o ⇒ opt_map … (mode_FR0n_write t s o (getn_array8T o ? (bits_of_byte8 writeb)))
 234                     (λs'.Some ? (pair … s' cur_pc))
 235 (* [FRn] *)
 236    | MODE_FR1n o ⇒ opt_map … (mode_FR1n_write t s o (getn_array8T o ? (bits_of_byte8 writeb)))
 237                     (λs'.Some ? (pair … s' cur_pc))
 238    ].
 239
 240 ndefinition IP2022_multi_mode_write_auxw ≝
 241 λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.λwritew:word16.match i with
 242 (* NO: non ci sono indicazioni *)
 243    [ MODE_INH ⇒ None ?
 244 (* [ADDR] *)
 245    | MODE_INHADDR ⇒ opt_map … (mode_ADDR_write t s writew)
 246                      (λs'.Some ? (pair … s' cur_pc))
 247 (* [ADDR], ADDR+=2 *)
 248    | MODE_INHADDRpp ⇒ opt_map … (mode_ADDR_write t s writew)
 249                        (λs'.Some ? (pair … (aux_inc_addr2 t s') cur_pc))
 250
 251 (* NO: solo lettura byte *)
 252    | MODE_IMM3 _ ⇒ None ?
 253 (* NO: solo lettura byte *)
 254    | MODE_IMM8 ⇒ None ?
 255 (* NO: solo lettura word *)
 256    | MODE_IMM13 _ ⇒ None ?
 257
 258 (* NO: solo byte *)
 259    | MODE_FR0_and_W ⇒ None ?
 260 (* NO: solo byte *)
 261    | MODE_FR1_and_W ⇒ None ?
 262 (* NO: solo byte *)
 263    | MODE_W_and_FR0 ⇒ None ?
 264 (* NO: solo byte *)
 265    | MODE_W_and_FR1 ⇒ None ?
 266
 267 (* NO: solo byte *)
 268    | MODE_FR0n _ ⇒ None ?
 269 (* NO: solo byte *)
 270    | MODE_FR1n _ ⇒ None ?
 271    ].