1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "emulator/memory/memory_struct.ma".
24 include "num/word32.ma".
25 include "common/option.ma".
26 include "common/list.ma".
28 (* ********************* *)
29 (* MEMORIA E DESCRITTORE *)
30 (* ********************* *)
32 (* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
33 ndefinition mf_check_update_ranged ≝
34 λf:word32 → memory_type.λaddr:word32.λrange:word16.λv.
35 λx.match inrange_w32 x addr (plus_w32_d_d addr (ext_word32 range)) with
39 (* tutta la memoria non installata *)
40 ndefinition mf_out_of_bound_memory ≝ λ_:word32.MEM_OUT_OF_BOUND.
42 (* (mf_mem_update mem checked addr val) = scrivi controllando il tipo di memoria *)
43 ndefinition mf_mem_update ≝
44 λf:word32 → byte8.λc:word32 → memory_type.λa:word32.λv:byte8.
46 (* ROM? ok, ma il valore viene perso *)
47 [ MEM_READ_ONLY ⇒ Some ? f
49 | MEM_READ_WRITE ⇒ Some ? (λx.match eq_w32 x a with [ true ⇒ v | false ⇒ f x ])
50 (* NON INSTALLATA? no *)
51 | MEM_OUT_OF_BOUND ⇒ None ? ].
53 (* tutta la memoria a 0 *)
54 ndefinition mf_zero_memory ≝ λ_:word32.〈x0,x0〉.
56 (* (mf_mem_read mem check addr) = leggi controllando il tipo di memoria *)
57 ndefinition mf_mem_read ≝
58 λf:word32 → byte8.λc:word32 → memory_type.λa.
60 [ MEM_READ_ONLY ⇒ Some ? (f a)
61 | MEM_READ_WRITE ⇒ Some ? (f a)
62 | MEM_OUT_OF_BOUND ⇒ None ? ].
64 (* ************************** *)
65 (* CARICAMENTO PROGRAMMA/DATI *)
66 (* ************************** *)
68 (* carica a paratire da addr, overflow se si supera 0xFFFF... *)
69 nlet rec mf_load_from_source_at (old_mem:word32 → byte8) (src:list byte8) (addr:word32) on src ≝
71 (* fine di source: carica da old_mem *)
73 | cons hd tl ⇒ λx:word32.match eq_w32 addr x with
74 (* la locazione corrisponde al punto corrente di source *)
76 (* la locazione e' piu' avanti? ricorsione *)
77 | false ⇒ (mf_load_from_source_at old_mem tl (succ_w32 addr)) x