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