helm/software/matita/contribs/ng_assembly/freescale/memory_func.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_struct.ma".
  28 include "freescale/word16.ma".
  29 include "freescale/option.ma".
  30 include "freescale/theory.ma".
  31
  32 (* ********************* *)
  33 (* MEMORIA E DESCRITTORE *)
  34 (* ********************* *)
  35
  36 (* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
  37 ndefinition mf_check_update_ranged ≝
  38 λf:word16 → memory_type.λi.λs.λv.
  39  λx.match in_range x i s with
  40   [ true ⇒ v
  41   | false ⇒ f x ].
  42
  43 (* tutta la memoria non installata *)
  44 ndefinition mf_out_of_bound_memory ≝ λ_:word16.MEM_OUT_OF_BOUND.
  45
  46 ndefinition mf_chk_get ≝
  47 λc:word16 → memory_type.λa:word16.
  48  match c a with
  49   [ MEM_READ_ONLY ⇒ array_8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY
  50   | MEM_READ_WRITE ⇒ array_8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE
  51   | MEM_OUT_OF_BOUND ⇒ array_8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  52   ].
  53
  54 (* (mf_mem_update mem checked addr val) = scrivi controllando il tipo di memoria *)
  55 ndefinition mf_mem_update ≝
  56 λf:word16 → byte8.λc:Array8T memory_type.λa:word16.λv:byte8.
  57  match getn_array8T o0 ? c with
  58   (* ROM? ok, ma il valore viene perso *)
  59   [ MEM_READ_ONLY ⇒ Some ? f
  60   (* RAM? ok *)
  61   | MEM_READ_WRITE ⇒ Some ? (λx.match eq_w16 x a with [ true ⇒ v | false ⇒ f x ])
  62   (* NON INSTALLATA? no *)
  63   | MEM_OUT_OF_BOUND ⇒ None ? ].
  64
  65 (* tutta la memoria a 0 *)
  66 ndefinition mf_zero_memory ≝ λ_:word16.〈x0,x0〉.
  67
  68 (* (mf_mem_read mem check addr) = leggi controllando il tipo di memoria *)
  69 ndefinition mf_mem_read ≝
  70 λf:word16 → byte8.λc:word16 → memory_type.λa.
  71  match c a with
  72   [ MEM_READ_ONLY ⇒ Some ? (f a)
  73   | MEM_READ_WRITE ⇒ Some ? (f a)
  74   | MEM_OUT_OF_BOUND ⇒ None ? ].
  75
  76 (* ************************** *)
  77 (* CARICAMENTO PROGRAMMA/DATI *)
  78 (* ************************** *)
  79
  80 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
  81 nlet rec mf_load_from_source_at (old_mem:word16 → byte8) (source:list byte8) (addr:word16) on source ≝
  82 match source with
  83  (* fine di source: carica da old_mem *)
  84  [ nil ⇒ old_mem
  85  | cons hd tl ⇒ λx:word16.match lt_w16 x addr with
  86   (* e' prima di source: carica da old_mem *)
  87   [ true ⇒ old_mem x
  88   | false ⇒ match eq_w16 x addr with
  89    (* la locazione corrisponde al punto corrente di source *)
  90    [ true ⇒ hd
  91    (* la locazione e' piu' avanti: ricorsione *)
  92    | false ⇒ (mf_load_from_source_at old_mem tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)) x
  93    ]
  94   ]
  95  ].