helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write_base.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/read_write.ma".
  24
  25 (* ************************ *)
  26 (* MODALITA' INDIRIZZAMENTO *)
  27 (* ************************ *)
  28
  29 (* mattoni base *)
  30 (* - incrementano l'indirizzo normalmente *)
  31 (* - incrementano PC attraverso il filtro *)
  32
  33 (* lettura byte da addr *)
  34 ndefinition loadb_from ≝
  35 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  36 λaddr:word32.λcur_pc:word16.λfetched:exadecim.
  37  opt_map … (memory_filter_read … s addr)
  38   (λb.Some ? (triple … s b (plus_w16_d_d cur_pc (extu2_w16 fetched)))).
  39
  40 (* lettura bit da addr *)
  41 ndefinition loadbit_from ≝
  42 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  43 λaddr:word32.λsub:oct.λcur_pc:word16.λfetched:exadecim.
  44  opt_map … (memory_filter_read_bit … s addr sub)
  45   (λb.Some ? (triple … s b (plus_w16_d_d cur_pc (extu2_w16 fetched)))).
  46
  47 (* lettura word da addr *)
  48 ndefinition loadw_from ≝
  49 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  50 λaddr:word32.λcur_pc:word16.λfetched:exadecim.
  51  opt_map … (memory_filter_read … s addr)
  52   (λbh.opt_map … (memory_filter_read … s (succ_w32 addr))
  53    (λbl.Some ? (triple … s 〈bh:bl〉 (plus_w16_d_d cur_pc (extu2_w16 fetched))))).
  54
  55 (* scrittura byte su addr *)
  56 ndefinition writeb_to ≝
  57 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  58 λaddr:word32.λflag:aux_mod_type.λcur_pc:word16.λfetched:exadecim.λwriteb:byte8.
  59  opt_map … (memory_filter_write … s addr flag writeb)
  60   (λtmps.Some ? (pair … tmps (plus_w16_d_d cur_pc (extu2_w16 fetched)))).
  61
  62 (* scrittura bit su addr *)
  63 ndefinition writebit_to ≝
  64 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  65 λaddr:word32.λsub:oct.λcur_pc:word16.λfetched:exadecim.λwriteb:bool.
  66  opt_map … (memory_filter_write_bit … s addr sub writeb)
  67   (λtmps.Some ? (pair … tmps (plus_w16_d_d cur_pc (extu2_w16 fetched)))).
  68
  69 (* scrittura word su addr *)
  70 ndefinition writew_to ≝
  71 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  72 λaddr:word32.λflag:aux_mod_type.λcur_pc:word16.λfetched:exadecim.λwritew:word16.
  73  opt_map … (memory_filter_write … s addr auxMode_ok (cnH ? writew))
  74   (λtmps1.opt_map … (memory_filter_write … tmps1 (succ_w32 addr) auxMode_ok (cnL ? writew))
  75     (λtmps2.Some ? (pair … tmps2 (plus_w16_d_d cur_pc (extu2_w16 fetched))))).
  76
  77 (* ausiliari per definire i tipi e la lettura/scrittura *)
  78
  79 (* ausiliaria per definire il tipo di aux_load *)
  80 ndefinition aux_load_typing ≝
  81 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
  82  any_status m t → word32 → word16 → exadecim →
  83  option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
  84
  85 (* per non dover ramificare i vari load in byte/word *)
  86 ndefinition aux_load ≝
  87 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
  88  [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
  89
  90 (* ausiliaria per definire il tipo di aux_write *)
  91 ndefinition aux_write_typing ≝
  92 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
  93  any_status m t → word32 → aux_mod_type → word16 → exadecim →
  94  match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
  95  option (ProdT (any_status m t) word16).
  96
  97 (* per non dover ramificare i vari load in byte/word *)
  98 ndefinition aux_write ≝
  99 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
 100  [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
 101
 102 ndefinition mem_read_s ≝
 103 λm,t.λs:any_status m t.mem_read t (mem_desc … s) (chk_desc … s).
 104
 105 ndefinition mem_read_bit_s ≝
 106 λm,t.λs:any_status m t.mem_read_bit t (mem_desc … s) (chk_desc … s).