matita/contribs/assembly/freescale/memory_bits.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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/memory_trees.ma".
  28
  29 (* ********************* *)
  30 (* MEMORIA E DESCRITTORE *)
  31 (* ********************* *)
  32
  33 (* tutta la memoria non installata *)
  34 definition mb_out_of_bound_memory ≝
  35 let base ≝ array_8T memory_type MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  36                                 MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND in
  37 let lev4 ≝ array_16T ?
  38            base base base base base base base base
  39            base base base base base base base base
  40            in
  41 let lev3 ≝ array_16T ?
  42            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  43            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  44            in
  45 let lev2 ≝ array_16T ?
  46            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  47            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  48            in
  49 let lev1 ≝ array_16T ?
  50            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  51            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  52            in
  53 lev1.
  54
  55 (* tutta la memoria a 0 *)
  56 definition mb_zero_memory ≝
  57 let base ≝ array_8T bool false false false false false false false false in
  58 let lev4 ≝ array_16T ?
  59            base base base base base base base base
  60            base base base base base base base base
  61            in
  62 let lev3 ≝ array_16T ?
  63            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  64            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  65            in
  66 let lev2 ≝ array_16T ?
  67            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  68            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  69            in
  70 let lev1 ≝ array_16T ?
  71            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  72            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  73            in
  74 lev1.
  75
  76 (* scrivi bit controllando il tipo di memoria *)
  77 definition mb_mem_update_bit ≝
  78 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
  79 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
  80 λaddr:word16.λsub:oct.λv:bool.
  81  match getn_array8T sub memory_type (mt_visit (Prod8T memory_type) chk addr) with
  82   (* ROM? ok, ma il valore viene perso *)
  83   [ MEM_READ_ONLY ⇒ Some ? mem
  84   (* RAM? ok *)
  85   | MEM_READ_WRITE ⇒ Some ? (mt_update (Prod8T bool) mem addr (setn_array8T sub bool (mt_visit (Prod8T bool) mem addr) v))
  86   (* NON INSTALLATA? no *)
  87   | MEM_OUT_OF_BOUND ⇒ None ? ].
  88
  89 (* scrivi tipo di bit *)
  90 definition mb_chk_update_bit ≝
  91 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
  92 λaddr:word16.λsub:oct.λv:memory_type.
  93  mt_update (Prod8T memory_type) chk addr (setn_array8T sub memory_type (mt_visit (Prod8T memory_type) chk addr) v).
  94
  95 (* leggi bit controllando il tipo di memoria *)
  96 definition mb_mem_read_bit ≝
  97 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
  98 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
  99 λaddr:word16.λsub:oct.
 100  match getn_array8T sub memory_type (mt_visit (Prod8T memory_type) chk addr) with
 101   (* ROM? ok, ma il valore viene perso *)
 102   [ MEM_READ_ONLY ⇒ Some ? (getn_array8T sub bool (mt_visit (Prod8T bool) mem addr))
 103   (* RAM? ok *)
 104   | MEM_READ_WRITE ⇒ Some ? (getn_array8T sub bool (mt_visit (Prod8T bool) mem addr))
 105   (* NON INSTALLATA? no *)
 106   | MEM_OUT_OF_BOUND ⇒ None ? ].
 107
 108 definition mb_chk_get ≝
 109 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).λaddr:word16.
 110 let c ≝ mt_visit (Prod8T memory_type) chk addr in
 111 array_8T ? (getn_array8T o7 ? c) (getn_array8T o6 ? c)
 112            (getn_array8T o5 ? c) (getn_array8T o4 ? c)
 113            (getn_array8T o3 ? c) (getn_array8T o2 ? c)
 114            (getn_array8T o1 ? c) (getn_array8T o0 ? c).
 115
 116 (* scrivi controllando il tipo di memoria *)
 117 (* NB: devono esistere tutti i bit *)
 118 definition mb_mem_update ≝
 119 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
 120 λchk:Prod8T memory_type.
 121 λaddr:word16.λv:byte8.
 122 let old_value ≝ mt_visit (Prod8T bool) mem addr in
 123 let new_value ≝ bits_of_byte8 v in
 124 let newbit0 ≝ match getn_array8T o0 memory_type chk with
 125  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool old_value)
 126  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool new_value)
 127  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 128 let newbit1 ≝ match getn_array8T o1 memory_type chk with
 129  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool old_value)
 130  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool new_value)
 131  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 132 let newbit2 ≝ match getn_array8T o2 memory_type chk with
 133  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool old_value)
 134  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool new_value)
 135  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 136 let newbit3 ≝ match getn_array8T o3 memory_type chk with
 137  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool old_value)
 138  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool new_value)
 139  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 140 let newbit4 ≝ match getn_array8T o4 memory_type chk with
 141  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool old_value)
 142  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool new_value)
 143  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 144 let newbit5 ≝ match getn_array8T o5 memory_type chk with
 145  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool old_value)
 146  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool new_value)
 147  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 148 let newbit6 ≝ match getn_array8T o6 memory_type chk with
 149  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool old_value)
 150  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool new_value)
 151  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 152 let newbit7 ≝ match getn_array8T o7 memory_type chk with
 153  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool old_value)
 154  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool new_value)
 155  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 156        opt_map ?? newbit0
 157  (λnb0.opt_map ?? newbit1
 158  (λnb1.opt_map ?? newbit2
 159  (λnb2.opt_map ?? newbit3
 160  (λnb3.opt_map ?? newbit4
 161  (λnb4.opt_map ?? newbit5
 162  (λnb5.opt_map ?? newbit6
 163  (λnb6.opt_map ?? newbit7
 164  (λnb7.Some ? (mt_update (Prod8T bool) mem addr (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
 165
 166 (* leggi controllando il tipo di memoria *)
 167 (* NB: devono esistere tutti i bit *)
 168 definition mb_mem_read ≝
 169 λmem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))).
 170 λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).
 171 λaddr:word16.
 172 let bit_types ≝ mt_visit (Prod8T memory_type) chk addr in
 173 let value ≝ mt_visit (Prod8T bool) mem addr in
 174 let newbit0 ≝ match getn_array8T o0 memory_type bit_types with
 175  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool value)
 176  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool value)
 177  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 178 let newbit1 ≝ match getn_array8T o1 memory_type bit_types with
 179  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool value)
 180  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool value)
 181  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 182 let newbit2 ≝ match getn_array8T o2 memory_type bit_types with
 183  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool value)
 184  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool value)
 185  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 186 let newbit3 ≝ match getn_array8T o3 memory_type bit_types with
 187  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool value)
 188  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool value)
 189  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 190 let newbit4 ≝ match getn_array8T o4 memory_type bit_types with
 191  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool value)
 192  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool value)
 193  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 194 let newbit5 ≝ match getn_array8T o5 memory_type bit_types with
 195  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool value)
 196  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool value)
 197  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 198 let newbit6 ≝ match getn_array8T o6 memory_type bit_types with
 199  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool value)
 200  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool value)
 201  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 202 let newbit7 ≝ match getn_array8T o7 memory_type bit_types with
 203  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool value)
 204  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool value)
 205  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 206        opt_map ?? newbit0
 207  (λnb0.opt_map ?? newbit1
 208  (λnb1.opt_map ?? newbit2
 209  (λnb2.opt_map ?? newbit3
 210  (λnb3.opt_map ?? newbit4
 211  (λnb4.opt_map ?? newbit5
 212  (λnb5.opt_map ?? newbit6
 213  (λnb6.opt_map ?? newbit7
 214  (λnb7.Some ? (byte8_of_bits (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
 215
 216 (* ************************** *)
 217 (* CARICAMENTO PROGRAMMA/DATI *)
 218 (* ************************** *)
 219
 220 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
 221 let rec mb_load_from_source_at (old_mem:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool)))))
 222                                (source:list byte8) (addr:word16) on source ≝
 223 match source with
 224  (* fine di source: carica da old_mem *)
 225  [ nil ⇒ old_mem
 226  | cons hd tl ⇒ match lt_w16 addr 〈〈xF,xF〉:〈xF,xF〉〉 with
 227   (* non supera 0xFFFF, ricorsione *)
 228   [ true ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16nc addr 〈〈x0,x0〉:〈x0,x1〉〉)
 229   (* supera 0xFFFF, niente ricorsione *)
 230   | false ⇒ mt_update ? old_mem addr (bits_of_byte8 hd)
 231   ]].