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_base.ma".
24 include "num/word16.ma".
25 include "common/list.ma".
27 (* ************************** *)
28 (* 8 segmenti da 64Kb → 512Kb *)
29 (* ************************** *)
31 (* ********************* *)
32 (* MEMORIA E DESCRITTORE *)
33 (* ********************* *)
35 (* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
36 ndefinition mf_check_update_ranged ≝
37 λf:oct → word16 → memory_type.λsel:oct.λaddr:word16.λrange:word16.λv.
39 match (eqc ? sel x)⊗(inrangec ? y addr (plusc_d_d ? addr range)) with
43 (* tutta la memoria non installata *)
44 ndefinition mf_out_of_bound_memory ≝ λ_:oct.λ_:word16.MEM_OUT_OF_BOUND.
46 (* (mf_mem_update mem checked addr val) = scrivi controllando il tipo di memoria *)
47 ndefinition mf_mem_update ≝
48 λf:oct → word16 → byte8.λc:oct → word16 → memory_type.λsel:oct.λa:word16.λv:byte8.
50 (* ROM? ok, ma il valore viene perso *)
51 [ MEM_READ_ONLY ⇒ Some ? f
53 | MEM_READ_WRITE ⇒ Some ? (λx,y.match (eqc ? sel x)⊗(eqc ? a y) with [ true ⇒ v | false ⇒ f x y ])
54 (* NON INSTALLATA? no *)
55 | MEM_OUT_OF_BOUND ⇒ None ? ].
57 (* tutta la memoria a 0 *)
58 ndefinition mf_zero_memory ≝ λ_:oct.λ_:word16.〈x0,x0〉.
60 (* (mf_mem_read mem check addr) = leggi controllando il tipo di memoria *)
61 ndefinition mf_mem_read ≝
62 λf:oct → word16 → byte8.λc:oct → word16 → memory_type.λsel:oct.λa:word16.
64 [ MEM_READ_ONLY ⇒ Some ? (f sel a)
65 | MEM_READ_WRITE ⇒ Some ? (f sel a)
66 | MEM_OUT_OF_BOUND ⇒ None ? ].
68 (* ************************** *)
69 (* CARICAMENTO PROGRAMMA/DATI *)
70 (* ************************** *)
72 (* carica a paratire da addr, overflow se si supera 0xFFFF... *)
73 nlet rec mf_load_from_source_at (old_mem:oct → word16 → byte8) (src:list byte8) (sel:oct) (addr:word16) on src ≝
75 (* fine di source: carica da old_mem *)
77 | cons hd tl ⇒ λx,y.match (eqc ? sel x)⊗(eqc ? addr y) with
78 (* la locazione corrisponde al punto corrente di source *)
80 (* la locazione e' piu' avanti? ricorsione *)
81 | false ⇒ (mf_load_from_source_at old_mem tl sel (succc ? addr)) x y