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