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/read_write/load_write_base.ma".
24 include "emulator/status/status_getter.ma".
25 include "emulator/read_write/IP2022_fetch.ma".
27 (* lettura da [OLD PC<<1 + 1] : argomento non caricato dal fetch word-aligned *)
28 ndefinition mode_IMM1_load ≝
29 λt:memory_impl.λs:any_status IP2022 t.
30 match IP2022_pc_translation (get_pc_reg … s) with
31 [ pair seg pc ⇒ mem_read_s … s seg (succc ? pc) ].
34 ADDRX=0x00 [ADDRH|ADDRL] 16Kb PROGRAM RAM
35 ADDRX=0x01 [ADDRH|ADDRL] 64Kb FLASH
36 ADDRX=0x80 [ADDRH|ADDRL] 64Kb EXTERNAL RAM
37 ADDRX=0x81 [ADDRH|ADDRL] 64Kb EXTERNAL RAM *)
39 (* lettura da [ADDR] *)
40 ndefinition mode_ADDR_load ≝
41 λt:memory_impl.λs:any_status IP2022 t.
42 opt_map … (get_addr_reg … s)
43 (λaddr.match eqc ? (w24x addr) 〈x0,x0〉 with
44 (* lettura della RAM, sempre non blocking *)
45 [ true ⇒ opt_map … (mem_read_s … s o1 (clrLSBc ? 〈(w24h addr):(w24l addr)〉))
46 (λbh.opt_map … (mem_read_s … s o1 (setLSBc ? 〈(w24h addr):(w24l addr)〉))
48 (* lettura della FLASH da codice in RAM : operazione non bloccante non implementata! *)
49 (* lettura da alri ADDRX, errore *)
50 | false ⇒ match (gtc ? (w24x addr) 〈x0,x1〉)⊕(⊖(IP2022_pc_flashtest (get_pc_reg … s))) with
52 | false ⇒ opt_map … (mem_read_s … s o2 (clrLSBc ? 〈(w24h addr):(w24l addr)〉))
53 (λbh.opt_map … (mem_read_s … s o2 (setLSBc ? 〈(w24h addr):(w24l addr)〉))
58 (* scrittura su [ADDR] *)
59 ndefinition mode_ADDR_write ≝
60 λt:memory_impl.λs:any_status IP2022 t.λval:word16.
61 opt_map ?? (get_addr_reg … s)
62 (λaddr.opt_map ?? (match eqc ? (w24x addr) 〈x0,x0〉 with
64 | false ⇒ match eqc ? (w24x addr) 〈x0,x1〉 with
67 (λseg.opt_map ?? (mem_write_s ?? s seg (clrLSBc ? 〈(w24h addr):(w24l addr)〉) (cnH ? val))
68 (λs'.mem_write_s ?? s' seg (setLSBc ? 〈(w24h addr):(w24l addr)〉) (cnL ? val)))).
70 (* IMM1 > 0 : lettura/scrittura da [IMM1] *)
71 (* else : lettura/scrittura da [IP] : IP ≥ 0x20 *)
72 ndefinition mode_DIR1IP_aux ≝
73 λt:memory_impl.λs:any_status IP2022 t.λT.λf:word16 → option T.
74 opt_map … (mode_IMM1_load t s)
75 (λaddr.match eqc ? addr 〈x0,x0〉 with
76 (* xxxxxxx0 00000000 → [IP] *)
77 [ true ⇒ opt_map … (get_ip_reg … s)
78 (λip.match gec ? ip 〈〈x0,x0〉:〈x2,x0〉〉 with
82 (* xxxxxxx0 nnnnnnnn → [IMM1] *)
83 | false ⇒ f (extu_w16 addr)
86 (* IMM1 < 0x80 : lettura/scrittura da [DP+IMM1] : DP+IMM1 ≥ 0x20 *)
87 (* else : lettura/scrittura da [SP+IMM1] : SP+IMM1 ≥ 0x20 *)
88 ndefinition mode_DPSP_aux ≝
89 λt:memory_impl.λs:any_status IP2022 t.λT.λf:word16 → option T.
90 opt_map … (mode_IMM1_load t s)
91 (λaddr.opt_map … (match getMSBc ? addr with
92 (* xxxxxxx1 1nnnnnnn → [SP+IMM1] *)
93 [ true ⇒ get_sp_reg … s
94 (* xxxxxxx1 0nnnnnnn → [DP+IMM1] *)
95 | false ⇒ get_dp_reg … s ])
96 (λreg.match gec ? (plusc_d_d ? reg (extu_w16 (clrMSBc ? addr))) 〈〈x0,x0〉:〈x2,x0〉〉 with
98 [ true ⇒ f (plusc_d_d ? reg (extu_w16 (clrMSBc ? addr)))
102 ndefinition mode_FR0_load ≝
103 λt:memory_impl.λs:any_status IP2022 t.
104 mode_DIR1IP_aux t s byte8 (memory_filter_read … s).
106 ndefinition mode_FR0n_load ≝
107 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
108 mode_DIR1IP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
110 ndefinition mode_FR0_write ≝
111 λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
112 mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
114 ndefinition mode_FR0n_write ≝
115 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
116 mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
119 ndefinition mode_FR1_load ≝
120 λt:memory_impl.λs:any_status IP2022 t.
121 mode_DPSP_aux t s byte8 (memory_filter_read … s).
123 ndefinition mode_FR1n_load ≝
124 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
125 mode_DPSP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
127 ndefinition mode_FR1_write ≝
128 λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
129 mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
131 ndefinition mode_FR1n_write ≝
132 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
133 mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
135 (* ************************************** *)
136 (* raccordo di tutte le possibili letture *)
137 (* ************************************** *)
140 ndefinition aux_inc_addr2 ≝
141 λt:memory_impl.λs:any_status IP2022 t.
142 set_addr_reg_sIP2022 t s (succ_w24 (succ_w24 (get_addr_reg_IP2022 (alu … s)))).
144 ndefinition IP2022_multi_mode_load_auxb ≝
145 λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.match i with
146 (* NO: non ci sono indicazioni *)
149 | MODE_INHADDR ⇒ None ?
151 | MODE_INHADDRpp ⇒ None ?
154 | MODE_IMM3 o ⇒ Some ? (triple … s (extu_b8 (ex_of_oct o)) cur_pc)
156 | MODE_IMM8 ⇒ opt_map … (mode_IMM1_load t s)
157 (λb.Some ? (triple … s b cur_pc))
158 (* NO: solo lettura word *)
159 | MODE_IMM13 _ ⇒ None ?
162 | MODE_FR0_and_W ⇒ None ?
164 | MODE_FR1_and_W ⇒ None ?
166 | MODE_W_and_FR0 ⇒ None ?
168 | MODE_W_and_FR1 ⇒ None ?
171 | MODE_FR0n o ⇒ opt_map … (mode_FR0n_load t s o)
172 (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc))
174 | MODE_FR1n o ⇒ opt_map … (mode_FR1n_load t s o)
175 (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc))
178 ndefinition IP2022_multi_mode_load_auxw ≝
179 λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.match i with
180 (* NO: non ci sono indicazioni *)
183 | MODE_INHADDR ⇒ opt_map … (mode_ADDR_load t s)
184 (λw.Some ? (triple … s w cur_pc))
185 (* [ADDR], ADDR+=2 *)
186 | MODE_INHADDRpp ⇒ opt_map … (mode_ADDR_load t s)
187 (λw.Some ? (triple … (aux_inc_addr2 t s) w cur_pc))
189 (* NO: solo lettura byte *)
190 | MODE_IMM3 _ ⇒ None ?
191 (* NO: solo lettura byte *)
194 | MODE_IMM13 bt ⇒ opt_map … (mode_IMM1_load t s)
195 (λb.Some ? (triple … s 〈(b8_of_bit bt):b〉 cur_pc))
198 | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_load t s)
199 (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc))
201 | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_load t s)
202 (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc))
204 | MODE_W_and_FR0 ⇒ opt_map … (mode_FR0_load t s)
205 (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc))
207 | MODE_W_and_FR1 ⇒ opt_map … (mode_FR1_load t s)
208 (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc))
211 | MODE_FR0n _ ⇒ None ?
213 | MODE_FR1n _ ⇒ None ?
216 (* **************************************** *)
217 (* raccordo di tutte le possibili scritture *)
218 (* **************************************** *)
220 ndefinition IP2022_multi_mode_write_auxb ≝
221 λt.λs:any_status IP2022 t.λcur_pc:word16.λflag:aux_mod_type.λi:IP2022_instr_mode.λwriteb:byte8.match i with
222 (* NO: non ci sono indicazioni *)
225 | MODE_INHADDR ⇒ None ?
227 | MODE_INHADDRpp ⇒ None ?
229 (* NO: solo lettura byte *)
230 | MODE_IMM3 _ ⇒ None ?
231 (* NO: solo lettura byte *)
233 (* NO: solo lettura word *)
234 | MODE_IMM13 _ ⇒ None ?
237 | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_write t s flag writeb)
238 (λs'.Some ? (pair … s' cur_pc))
240 | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_write t s flag writeb)
241 (λs'.Some ? (pair … s' cur_pc))
243 | MODE_W_and_FR0 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
245 | MODE_W_and_FR1 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
248 | MODE_FR0n o ⇒ opt_map … (mode_FR0n_write t s o (getn_array8T o ? (bits_of_byte8 writeb)))
249 (λs'.Some ? (pair … s' cur_pc))
251 | MODE_FR1n o ⇒ opt_map … (mode_FR1n_write t s o (getn_array8T o ? (bits_of_byte8 writeb)))
252 (λs'.Some ? (pair … s' cur_pc))
255 ndefinition IP2022_multi_mode_write_auxw ≝
256 λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.λwritew:word16.match i with
257 (* NO: non ci sono indicazioni *)
260 | MODE_INHADDR ⇒ opt_map … (mode_ADDR_write t s writew)
261 (λs'.Some ? (pair … s' cur_pc))
262 (* [ADDR], ADDR+=2 *)
263 | MODE_INHADDRpp ⇒ opt_map … (mode_ADDR_write t s writew)
264 (λs'.Some ? (pair … (aux_inc_addr2 t s') cur_pc))
266 (* NO: solo lettura byte *)
267 | MODE_IMM3 _ ⇒ None ?
268 (* NO: solo lettura byte *)
270 (* NO: solo lettura word *)
271 | MODE_IMM13 _ ⇒ None ?
274 | MODE_FR0_and_W ⇒ None ?
276 | MODE_FR1_and_W ⇒ None ?
278 | MODE_W_and_FR0 ⇒ None ?
280 | MODE_W_and_FR1 ⇒ None ?
283 | MODE_FR0n _ ⇒ None ?
285 | MODE_FR1n _ ⇒ None ?