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 "emulator/memory/memory_struct.ma".
25 include "num/word32.ma".
26 include "common/list.ma".
28 (* ************************** *)
29 (* 8 segmenti da 64Kb → 512Kb *)
30 (* 4 + 16 bit indirizzo *)
31 (* ************************** *)
33 (* ********************* *)
34 (* MEMORIA E DESCRITTORE *)
35 (* ********************* *)
37 ndefinition aux_20B_filler ≝
39 let lev4 ≝ mk_Array16T T el el el el el el el el el el el el el el el el in
40 let lev3 ≝ mk_Array16T ?
41 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
42 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 in
43 let lev2 ≝ mk_Array16T ?
44 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
45 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 in
46 let lev1 ≝ mk_Array16T ?
47 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
48 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 in
49 let lev0 ≝ mk_Array8T ?
50 lev1 lev1 lev1 lev1 lev1 lev1 lev1 lev1
54 ndefinition aux_20B_type ≝
55 λT:Type.Array8T (Array16T (Array16T (Array16T (Array16T T)))).
57 (* tutta la memoria non installata *)
58 ndefinition mt_out_of_bound_memory ≝ aux_20B_filler ? MEM_OUT_OF_BOUND.
60 (* tutta la memoria a 0 *)
61 ndefinition mt_zero_memory ≝ aux_20B_filler ? 〈x0,x0〉.
63 (* visita di un albero da 512Kb di elementi: ln16(512Kb)=5 passaggi *)
64 ndefinition mt_visit ≝
65 λT:Type.λdata:aux_20B_type T.λsel:oct.λaddr:word16.
66 getn_array16T (cnL ? (cnL ? addr)) ?
67 (getn_array16T (cnH ? (cnL ? addr)) ?
68 (getn_array16T (cnL ? (cnH ? addr)) ?
69 (getn_array16T (cnH ? (cnH ? addr)) ?
70 (getn_array8T sel ? data)))).
72 (* scrittura di un elemento in un albero da 512Kb *)
73 ndefinition mt_update ≝
74 λT:Type.λdata:aux_20B_type T.λsel:oct.λaddr:word16.λv:T.
75 let lev1 ≝ getn_array8T sel ? data in
76 let lev2 ≝ getn_array16T (cnH ? (cnH ? addr)) ? lev1 in
77 let lev3 ≝ getn_array16T (cnL ? (cnH ? addr)) ? lev2 in
78 let lev4 ≝ getn_array16T (cnH ? (cnL ? addr)) ? lev3 in
79 setn_array8T sel ? data
80 (setn_array16T (cnH ? (cnH ? addr)) ? lev1
81 (setn_array16T (cnL ? (cnH ? addr)) ? lev2
82 (setn_array16T (cnH ? (cnL ? addr)) ? lev3
83 (setn_array16T (cnL ? (cnL ? addr)) T lev4 v)))).
85 (* scrittura di un segmento (max 64Kb) degli otto disponibili *)
86 nlet rec mt_update_ranged (T:Type) (data:aux_20B_type T) (sel:oct) (addr:word16) (w:word16) (rw:rec_word16 w) (v:T) on rw ≝
89 | w16_S w' rw' ⇒ mt_update_ranged T (mt_update T data sel addr v)
90 sel (succc ? addr) w' rw' v
93 (* scrivi controllando il tipo di memoria *)
94 ndefinition mt_mem_update ≝
95 λmem:aux_20B_type byte8.
96 λchk:aux_20B_type memory_type.
97 λsel:oct.λaddr:word16.λv:byte8.
98 match mt_visit ? chk sel addr with
99 (* ROM? ok, ma il valore viene perso *)
100 [ MEM_READ_ONLY ⇒ Some ? mem
102 | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem sel addr v)
103 (* NON INSTALLATA? no *)
104 | MEM_OUT_OF_BOUND ⇒ None ? ].
106 (* leggi controllando il tipo di memoria *)
107 ndefinition mt_mem_read ≝
108 λmem:aux_20B_type byte8.
109 λchk:aux_20B_type memory_type.
110 λsel:oct.λaddr:word16.
111 match mt_visit ? chk sel addr with
112 [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem sel addr)
113 | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem sel addr)
114 | MEM_OUT_OF_BOUND ⇒ None ? ].
116 (* ************************** *)
117 (* CARICAMENTO PROGRAMMA/DATI *)
118 (* ************************** *)
120 (* carica a paratire da addr, overflow se si supera 0xFFFF... *)
121 nlet rec mt_load_from_source_at (old_mem:aux_20B_type byte8)
122 (src:list byte8) (sel:oct) (addr:word16) on src ≝
124 (* fine di source: carica da old_mem *)
126 | cons hd tl ⇒ mt_load_from_source_at (mt_update ? old_mem sel addr hd)
127 tl sel (succc ? addr)