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/status/status_getter.ma".
24 include "emulator/read_write/load_write_base.ma".
26 (* lettura da [OLD PC<<1 + 1] : argomento non caricato dal fetch word-aligned *)
27 ndefinition mode_IMM1_load ≝
28 λt:memory_impl.λs:any_status IP2022 t.
29 mem_read_s … s (rol_w32 〈〈〈x8,x1〉:〈x0,x0〉〉.(get_pc_reg … s)〉).
32 ADDRX=0x00 [ADDRH|ADDRL] 16Kb PROGRAM RAM
33 ADDRX=0x01 [ADDRH|ADDRL] 64Kb FLASH
34 ADDRX=0x80 [ADDRH|ADDRL] 64Kb EXTERNAL RAM
35 ADDRX=0x81 [ADDRH|ADDRL] 64Kb EXTERNAL RAM *)
37 (* lettura da [ADDR] *)
38 ndefinition mode_ADDR_load ≝
39 λt:memory_impl.λs:any_status IP2022 t.
40 opt_map … (get_addr_reg … s)
41 (λaddr.match (eq_b8 (w24x addr) 〈x0,x1〉) ⊗ (le_w16 (pred_w16 (get_pc_reg … s)) 〈〈x1,xF〉:〈xF,xF〉〉) with
42 (* lettura della FLASH da codice in RAM : operazione non bloccante non implementata! *)
44 | false ⇒ opt_map … (memory_filter_read … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(clrLSB_b8 (w24l addr))〉〉)
45 (λbh.opt_map … (memory_filter_read … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(setLSB_b8 (w24l addr))〉〉)
46 (λbl.Some ? 〈bh:bl〉))]).
48 (* scrittura su [ADDR] *)
49 ndefinition mode_ADDR_write ≝
50 λt:memory_impl.λs:any_status IP2022 t.λval:word16.
51 opt_map … (get_addr_reg … s)
52 (λaddr.opt_map … (memory_filter_write … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(clrLSB_b8 (w24l addr))〉〉 auxMode_ok (cnH ? val))
53 (λs'.memory_filter_write … s' 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(setLSB_b8 (w24l addr))〉〉 auxMode_ok (cnL ? val))).
55 (* IMM1 > 0 : lettura/scrittura da [IMM1] *)
56 (* else : lettura/scrittura da [IP] : IP ≥ 0x20 *)
57 ndefinition mode_DIR1IP_aux ≝
58 λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T.
59 opt_map … (mode_IMM1_load t s)
60 (λaddr.match eq_b8 addr 〈x0,x0〉 with
61 (* xxxxxxx0 00000000 → [IP] *)
62 [ true ⇒ opt_map … (get_ip_reg … s)
63 (λip.match ge_w16 ip 〈〈x0,x0〉:〈x2,x0〉〉 with
65 [ true ⇒ f (extu_w32 ip)
67 (* xxxxxxx0 nnnnnnnn → [IMM1] *)
68 | false ⇒ f (extu2_w32 addr)
71 (* IMM1 < 0x80 : lettura/scrittura da [DP+IMM1] : DP+IMM1 ≥ 0x20 *)
72 (* else : lettura/scrittura da [SP+IMM1] : SP+IMM1 ≥ 0x20 *)
73 ndefinition mode_DPSP_aux ≝
74 λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T.
75 opt_map … (mode_IMM1_load t s)
76 (λaddr.opt_map … (match getMSB_b8 addr with
77 (* xxxxxxx1 1nnnnnnn → [SP+IMM1] *)
78 [ true ⇒ get_sp_reg … s
79 (* xxxxxxx1 0nnnnnnn → [DP+IMM1] *)
80 | false ⇒ get_dp_reg … s ])
81 (λreg.match ge_w16 (plus_w16_d_d reg (extu_w16 (clrMSB_b8 addr))) 〈〈x0,x0〉:〈x2,x0〉〉 with
83 [ true ⇒ f (extu_w32 (plus_w16_d_d reg (extu_w16 (clrMSB_b8 addr))))
87 ndefinition mode_FR0_load ≝
88 λt:memory_impl.λs:any_status IP2022 t.
89 mode_DIR1IP_aux t s byte8 (memory_filter_read … s).
91 ndefinition mode_FR0n_load ≝
92 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
93 mode_DIR1IP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
95 ndefinition mode_FR0_write ≝
96 λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
97 mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
99 ndefinition mode_FR0n_write ≝
100 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
101 mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
104 ndefinition mode_FR1_load ≝
105 λt:memory_impl.λs:any_status IP2022 t.
106 mode_DPSP_aux t s byte8 (memory_filter_read … s).
108 ndefinition mode_FR1n_load ≝
109 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
110 mode_DPSP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
112 ndefinition mode_FR1_write ≝
113 λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
114 mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
116 ndefinition mode_FR1n_write ≝
117 λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
118 mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
120 (* ************************************** *)
121 (* raccordo di tutte le possibili letture *)
122 (* ************************************** *)
125 ndefinition aux_inc_addr2 ≝
126 λt:memory_impl.λs:any_status IP2022 t.
127 set_addr_reg_sIP2022 t s (succ_w24 (succ_w24 (get_addr_reg_IP2022 (alu … s)))).
129 ndefinition IP2022_multi_mode_load_auxb ≝
130 λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.match i with
131 (* NO: non ci sono indicazioni *)
134 | MODE_INHADDR ⇒ None ?
136 | MODE_INHADDRpp ⇒ None ?
139 | MODE_IMM3 o ⇒ Some ? (triple … s (extu_b8 (ex_of_oct o)) cur_pc)
141 | MODE_IMM8 ⇒ opt_map … (mode_IMM1_load t s)
142 (λb.Some ? (triple … s b cur_pc))
143 (* NO: solo lettura word *)
144 | MODE_IMM13 _ ⇒ None ?
147 | MODE_FR0_and_W ⇒ None ?
149 | MODE_FR1_and_W ⇒ None ?
151 | MODE_W_and_FR0 ⇒ None ?
153 | MODE_W_and_FR1 ⇒ None ?
156 | MODE_FR0n o ⇒ opt_map … (mode_FR0n_load t s o)
157 (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc))
159 | MODE_FR1n o ⇒ opt_map … (mode_FR1n_load t s o)
160 (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc))
163 ndefinition IP2022_multi_mode_load_auxw ≝
164 λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.match i with
165 (* NO: non ci sono indicazioni *)
168 | MODE_INHADDR ⇒ opt_map … (mode_ADDR_load t s)
169 (λw.Some ? (triple … s w cur_pc))
170 (* [ADDR], ADDR+=2 *)
171 | MODE_INHADDRpp ⇒ opt_map … (mode_ADDR_load t s)
172 (λw.Some ? (triple … (aux_inc_addr2 t s) w cur_pc))
174 (* NO: solo lettura byte *)
175 | MODE_IMM3 _ ⇒ None ?
176 (* NO: solo lettura byte *)
179 | MODE_IMM13 bt ⇒ opt_map … (mode_IMM1_load t s)
180 (λb.Some ? (triple … s 〈(b8_of_bit bt):b〉 cur_pc))
183 | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_load t s)
184 (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc))
186 | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_load t s)
187 (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc))
189 | MODE_W_and_FR0 ⇒ opt_map … (mode_FR0_load t s)
190 (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc))
192 | MODE_W_and_FR1 ⇒ opt_map … (mode_FR1_load t s)
193 (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc))
196 | MODE_FR0n _ ⇒ None ?
198 | MODE_FR1n _ ⇒ None ?
201 (* **************************************** *)
202 (* raccordo di tutte le possibili scritture *)
203 (* **************************************** *)
205 ndefinition IP2022_multi_mode_write_auxb ≝
206 λt.λs:any_status IP2022 t.λcur_pc:word16.λflag:aux_mod_type.λi:IP2022_instr_mode.λwriteb:byte8.match i with
207 (* NO: non ci sono indicazioni *)
210 | MODE_INHADDR ⇒ None ?
212 | MODE_INHADDRpp ⇒ None ?
214 (* NO: solo lettura byte *)
215 | MODE_IMM3 _ ⇒ None ?
216 (* NO: solo lettura byte *)
218 (* NO: solo lettura word *)
219 | MODE_IMM13 _ ⇒ None ?
222 | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_write t s flag writeb)
223 (λs'.Some ? (pair … s' cur_pc))
225 | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_write t s flag writeb)
226 (λs'.Some ? (pair … s' cur_pc))
228 | MODE_W_and_FR0 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
230 | MODE_W_and_FR1 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
233 | MODE_FR0n o ⇒ opt_map … (mode_FR0n_write t s o (getn_array8T o ? (bits_of_byte8 writeb)))
234 (λs'.Some ? (pair … s' cur_pc))
236 | MODE_FR1n o ⇒ opt_map … (mode_FR1n_write t s o (getn_array8T o ? (bits_of_byte8 writeb)))
237 (λs'.Some ? (pair … s' cur_pc))
240 ndefinition IP2022_multi_mode_write_auxw ≝
241 λt.λs:any_status IP2022 t.λcur_pc:word16.λi:IP2022_instr_mode.λwritew:word16.match i with
242 (* NO: non ci sono indicazioni *)
245 | MODE_INHADDR ⇒ opt_map … (mode_ADDR_write t s writew)
246 (λs'.Some ? (pair … s' cur_pc))
247 (* [ADDR], ADDR+=2 *)
248 | MODE_INHADDRpp ⇒ opt_map … (mode_ADDR_write t s writew)
249 (λs'.Some ? (pair … (aux_inc_addr2 t s') cur_pc))
251 (* NO: solo lettura byte *)
252 | MODE_IMM3 _ ⇒ None ?
253 (* NO: solo lettura byte *)
255 (* NO: solo lettura word *)
256 | MODE_IMM13 _ ⇒ None ?
259 | MODE_FR0_and_W ⇒ None ?
261 | MODE_FR1_and_W ⇒ None ?
263 | MODE_W_and_FR0 ⇒ None ?
265 | MODE_W_and_FR1 ⇒ None ?
268 | MODE_FR0n _ ⇒ None ?
270 | MODE_FR1n _ ⇒ None ?