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/read_write/load_write_base.ma".
  24 include "emulator/status/status_getter.ma".
  25
  26 (* lettura da [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〉〉.(pred_w16 (get_pc_reg … s))〉).
  30
  31 (* lettura da [ADDR] *)
  32 ndefinition mode_ADDR_load ≝
  33 λt:memory_impl.λs:any_status IP2022 t.
  34  opt_map … (get_addr_reg … s)
  35   (λaddr.match (eq_b8 (w24x addr) 〈x0,x1〉) ⊗ (le_w16 (pred_w16 (get_pc_reg … s)) 〈〈x1,xF〉:〈xF,xF〉〉) with
  36    (* lettura della FLASH da codice in RAM : operazione non bloccante non implementata! *)
  37    [ true ⇒ None ?
  38    | false ⇒ opt_map … (memory_filter_read … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(w24l addr)〉〉)
  39              (λbh.opt_map … (memory_filter_read … s 〈〈〈x0,x2〉:(w24x (succ_w24 addr))〉.〈(w24h (succ_w24 addr)):(w24l (succ_w24 addr))〉〉)
  40               (λbl.Some ? 〈bh:bl〉))]).
  41
  42 (* scrittura su [ADDR] *)
  43 ndefinition mode_ADDR_write ≝
  44 λt:memory_impl.λs:any_status IP2022 t.λval:word16.
  45  opt_map … (get_addr_reg … s)
  46   (λaddr.opt_map … (memory_filter_write … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(w24l addr)〉〉 auxMode_ok (cnH ? val))
  47    (λs'.memory_filter_write … s' 〈〈〈x0,x2〉:(w24x (succ_w24 addr))〉.〈(w24h (succ_w24 addr)):(w24l (succ_w24 addr))〉〉 auxMode_ok (cnL ? val))).
  48
  49 (* IMM1 > 0 : lettura/scrittura da [IMM1] *)
  50 (* else     : lettura/scrittura da [IP] : IP ≥ 0x20 *)
  51 ndefinition mode_DIR1IP_aux ≝
  52 λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T.
  53  opt_map … (mode_IMM1_load t s)
  54   (λaddr.match eq_b8 addr 〈x0,x0〉 with
  55    (* xxxxxxx0 00000000 → [IP] *)
  56    [ true ⇒ opt_map … (get_ip_reg … s)
  57              (λip.match ge_w16 ip 〈〈x0,x0〉:〈x2,x0〉〉 with
  58               (* IP ≥ 0x20 *)
  59               [ true ⇒ f (extu_w32 ip)
  60               | false ⇒ None ? ])
  61    (* xxxxxxx0 nnnnnnnn → [IMM1] *)
  62    | false ⇒ f (extu2_w32 addr)
  63    ]).
  64
  65 (* IMM1 < 0x80 : lettura/scrittura da [DP+IMM1] : DP+IMM1 ≥ 0x20 *)
  66 (* else        : lettura/scrittura da [SP+IMM1] : SP+IMM1 ≥ 0x20 *)
  67 ndefinition mode_DPSP_aux ≝
  68 λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T.
  69  opt_map … (mode_IMM1_load t s)
  70   (λaddr.opt_map … (match getMSB_b8 addr with
  71                     (* xxxxxxx1 1nnnnnnn → [SP+IMM1] *)
  72                     [ true ⇒ get_sp_reg … s
  73                     (* xxxxxxx1 0nnnnnnn → [DP+IMM1] *)
  74                     | false ⇒ get_dp_reg … s ])
  75    (λreg.match ge_w16 (plus_w16_d_d reg (extu_w16 (clrMSB_b8 addr))) 〈〈x0,x0〉:〈x2,x0〉〉 with
  76     (* reg+IMM1 ≥ 0x20 *)
  77     [ true ⇒ f (extu_w32 (plus_w16_d_d reg (extu_w16 (clrMSB_b8 addr))))
  78     | false ⇒ None ? ])).
  79
  80 (* FR0 *)
  81 ndefinition mode_FR0_load ≝
  82 λt:memory_impl.λs:any_status IP2022 t.
  83  mode_DIR1IP_aux t s byte8 (memory_filter_read … s).
  84
  85 ndefinition mode_FR0n_load ≝
  86 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
  87  mode_DIR1IP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
  88
  89 ndefinition mode_FR0_write ≝
  90 λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
  91  mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
  92
  93 ndefinition mode_FR0n_write ≝
  94 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
  95  mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
  96
  97 (* FR1 *)
  98 ndefinition mode_FR1_load ≝
  99 λt:memory_impl.λs:any_status IP2022 t.
 100  mode_DPSP_aux t s byte8 (memory_filter_read … s).
 101
 102 ndefinition mode_FR1n_load ≝
 103 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
 104  mode_DPSP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
 105
 106 ndefinition mode_FR1_write ≝
 107 λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
 108  mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
 109
 110 ndefinition mode_FR1n_write ≝
 111 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
 112  mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).