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/read_write_base.ma".
24 include "emulator/status/status_setter.ma".
26 ndefinition IP2022_ADDRSEL_loc ≝ 〈〈x0,x0〉:〈x0,x2〉〉.
27 ndefinition IP2022_ADDRX_loc ≝ 〈〈x0,x0〉:〈x0,x3〉〉.
28 ndefinition IP2022_IPH_loc ≝ 〈〈x0,x0〉:〈x0,x4〉〉.
29 ndefinition IP2022_IPL_loc ≝ 〈〈x0,x0〉:〈x0,x5〉〉.
30 ndefinition IP2022_SPH_loc ≝ 〈〈x0,x0〉:〈x0,x6〉〉.
31 ndefinition IP2022_SPL_loc ≝ 〈〈x0,x0〉:〈x0,x7〉〉.
32 ndefinition IP2022_PCH_loc ≝ 〈〈x0,x0〉:〈x0,x8〉〉.
33 ndefinition IP2022_PCL_loc ≝ 〈〈x0,x0〉:〈x0,x9〉〉.
34 ndefinition IP2022_W_loc ≝ 〈〈x0,x0〉:〈x0,xA〉〉.
35 ndefinition IP2022_STATUS_loc ≝ 〈〈x0,x0〉:〈x0,xB〉〉.
36 ndefinition IP2022_DPH_loc ≝ 〈〈x0,x0〉:〈x0,xC〉〉.
37 ndefinition IP2022_DPL_loc ≝ 〈〈x0,x0〉:〈x0,xD〉〉.
38 ndefinition IP2022_SPEED_loc ≝ 〈〈x0,x0〉:〈x0,xE〉〉.
39 ndefinition IP2022_MULH_loc ≝ 〈〈x0,x0〉:〈x0,xF〉〉.
40 ndefinition IP2022_ADDRH_loc ≝ 〈〈x0,x0〉:〈x1,x0〉〉.
41 ndefinition IP2022_ADDRL_loc ≝ 〈〈x0,x0〉:〈x1,x1〉〉.
42 ndefinition IP2022_DATAH_loc ≝ 〈〈x0,x0〉:〈x1,x2〉〉.
43 ndefinition IP2022_DATAL_loc ≝ 〈〈x0,x0〉:〈x1,x3〉〉.
44 ndefinition IP2022_CALLH_loc ≝ 〈〈x0,x0〉:〈x1,x4〉〉.
45 ndefinition IP2022_CALLL_loc ≝ 〈〈x0,x0〉:〈x1,x5〉〉.
51 (* NB: non ci sono strane indirezioni, solo registri memory mapped da intercettare *)
52 ndefinition IP2022_memory_filter_read_aux ≝
53 λt:memory_impl.λs:any_status IP2022 t.λaddr:word16.
54 λT:Type.λfREG:byte8 → option T.λfMEM:word16 → option T.
55 (* intercettare le locazioni memory mapped *)
56 match eqc ? addr IP2022_ADDRSEL_loc with
57 [ true ⇒ fREG (addrsel_reg_IP2022 (alu … s))
59 match eqc ? addr IP2022_ADDRX_loc with
60 [ true ⇒ fREG (w24x (get_addrarray (addrsel_reg_IP2022 (alu … s))
61 (addr_array_IP2022 (alu … s))))
63 match eqc ? addr IP2022_IPH_loc with
64 [ true ⇒ fREG (cnH ? (ip_reg_IP2022 (alu … s)))
66 match eqc ? addr IP2022_IPL_loc with
67 [ true ⇒ fREG (cnL ? (ip_reg_IP2022 (alu … s)))
69 match eqc ? addr IP2022_SPH_loc with
70 [ true ⇒ fREG (cnH ? (sp_reg_IP2022 (alu … s)))
72 match eqc ? addr IP2022_SPL_loc with
73 [ true ⇒ fREG (cnL ? (sp_reg_IP2022 (alu … s)))
75 match eqc ? addr IP2022_PCH_loc with
76 [ true ⇒ fREG (cnH ? (pc_reg_IP2022 (alu … s)))
78 match eqc ? addr IP2022_PCL_loc with
79 [ true ⇒ fREG (cnL ? (pc_reg_IP2022 (alu … s)))
81 match eqc ? addr IP2022_W_loc with
82 [ true ⇒ fREG (acc_low_reg_IP2022 (alu … s))
84 (* PAGE[7:5] Z[2] H[1] C [0] *)
85 match eqc ? addr IP2022_STATUS_loc with
86 [ true ⇒ fREG 〈(rolc ? (ex_of_oct (page_reg_IP2022 (alu … s)))),
87 (orc ? (orc ? (match z_flag_IP2022 (alu … s) with
88 [ true ⇒ x4 | false ⇒ x0 ])
89 (match h_flag_IP2022 (alu … s) with
90 [ true ⇒ x2 | false ⇒ x0 ]))
91 (match c_flag_IP2022 (alu … s) with
92 [ true ⇒ x1 | false ⇒ x0 ]))〉
94 match eqc ? addr IP2022_DPH_loc with
95 [ true ⇒ fREG (cnH ? (dp_reg_IP2022 (alu … s)))
97 match eqc ? addr IP2022_DPL_loc with
98 [ true ⇒ fREG (cnL ? (dp_reg_IP2022 (alu … s)))
101 match eqc ? addr IP2022_SPEED_loc with
102 [ true ⇒ fREG (extu_b8 (speed_reg_IP2022 (alu … s)))
104 match eqc ? addr IP2022_MULH_loc with
105 [ true ⇒ fREG (mulh_reg_IP2022 (alu … s))
107 match eqc ? addr IP2022_ADDRH_loc with
108 [ true ⇒ fREG (w24h (get_addrarray (addrsel_reg_IP2022 (alu … s))
109 (addr_array_IP2022 (alu … s))))
111 match eqc ? addr IP2022_ADDRL_loc with
112 [ true ⇒ fREG (w24l (get_addrarray (addrsel_reg_IP2022 (alu … s))
113 (addr_array_IP2022 (alu … s))))
115 match eqc ? addr IP2022_DATAH_loc with
116 [ true ⇒ fREG (cnH ? (data_reg_IP2022 (alu … s)))
118 match eqc ? addr IP2022_DATAL_loc with
119 [ true ⇒ fREG (cnL ? (data_reg_IP2022 (alu … s)))
121 match eqc ? addr IP2022_CALLH_loc with
122 [ true ⇒ fREG (cnH ? (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
124 match eqc ? addr IP2022_CALLL_loc with
125 [ true ⇒ fREG (cnL ? (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
126 (* accesso normale *)
128 ]]]]]]]]]]]]]]]]]]]].
130 (* lettura IP2022 di un byte *)
131 ndefinition IP2022_memory_filter_read ≝
132 λt:memory_impl.λs:any_status IP2022 t.λaddr:word16.
133 IP2022_memory_filter_read_aux t s addr byte8
135 (mem_read t (mem_desc … s) (chk_desc … s) o0).
137 (* lettura IP2022 di un bit *)
138 ndefinition IP2022_memory_filter_read_bit ≝
139 λt:memory_impl.λs:any_status IP2022 t.λaddr:word16.λsub:oct.
140 IP2022_memory_filter_read_aux t s addr bool
141 (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
142 (λa.mem_read_bit t (mem_desc … s) (chk_desc … s) o0 a sub).
148 ndefinition high_write_aux_w16 ≝
149 λf:byte8 → byte8.λw:word16.〈(f (cnH ? w)):(cnL ? w)〉.
151 ndefinition lowc_write_aux_w16 ≝
152 λf:byte8 → byte8.λw:word16.λflag:aux_mod_type.
155 | auxMode_inc ⇒ succc ?
156 | auxMode_dec ⇒ predc ? ]) (cnH ? w)):
159 ndefinition lownc_write_aux_w16 ≝
160 λf:byte8 → byte8.λw:word16.〈(cnH ? w):(f (cnL ? w))〉.
162 ndefinition ext_write_aux_w24 ≝
163 λf:byte8 → byte8.λw:word24.〈(f (w24x w));(w24h w);(w24l w)〉.
165 ndefinition high_write_aux_w24 ≝
166 λf:byte8 → byte8.λw:word24.〈(w24x w);(f (w24h w));(w24l w)〉.
168 ndefinition low_write_aux_w24 ≝
169 λf:byte8 → byte8.λw:word24.λflag:aux_mod_type.
170 match (match flag with
172 | auxMode_inc ⇒ succc ?
173 | auxMode_dec ⇒ predc ? ]) 〈(w24x w):(w24h w)〉 with
174 [ mk_comp_num wx' wh' ⇒ 〈wx';wh';(w24l w)〉 ].
176 (* flag di carry: riportare il carry al byte logicamente superiore *)
177 (* modifica di pc: non inserita nella stato ma postposta *)
178 ndefinition IP2022_memory_filter_write_aux ≝
179 λt:memory_impl.λs:any_status IP2022 t.λaddr:word16.λflag:aux_mod_type.
180 λfREG:byte8 → byte8.λfMEM:word16 → option (aux_mem_type t).
181 (* intercettare le locazioni memory mapped *)
182 match eqc ? addr IP2022_ADDRSEL_loc with
183 [ true ⇒ set_addrsel_reg … s (fREG (addrsel_reg_IP2022 (alu … s)))
185 match eqc ? addr IP2022_ADDRX_loc with
186 [ true ⇒ set_addr_reg … s (ext_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
187 (addr_array_IP2022 (alu … s))))
189 match eqc ? addr IP2022_IPH_loc with
190 [ true ⇒ set_ip_reg … s (high_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)))
192 match eqc ? addr IP2022_IPL_loc with
193 [ true ⇒ set_ip_reg … s (lowc_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)) flag)
195 match eqc ? addr IP2022_SPH_loc with
196 [ true ⇒ set_sp_reg … s (high_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)))
198 match eqc ? addr IP2022_SPL_loc with
199 [ true ⇒ set_sp_reg … s (lowc_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)) flag)
201 match eqc ? addr IP2022_PCL_loc with
202 [ true ⇒ Some ? (set_pc_reg … s (lowc_write_aux_w16 fREG (pc_reg_IP2022 (alu … s)) flag))
204 match eqc ? addr IP2022_W_loc with
205 [ true ⇒ Some ? (set_acc_8_low_reg … s (fREG (acc_low_reg_IP2022 (alu … s))))
207 match eqc ? addr IP2022_DPH_loc with
208 [ true ⇒ set_dp_reg … s (high_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)))
210 match eqc ? addr IP2022_DPL_loc with
211 [ true ⇒ set_dp_reg … s (lowc_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)) flag)
213 match eqc ? addr IP2022_MULH_loc with
214 [ true ⇒ set_mulh_reg … s (fREG (mulh_reg_IP2022 (alu … s)))
216 match eqc ? addr IP2022_ADDRH_loc with
217 [ true ⇒ set_addr_reg … s (high_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
218 (addr_array_IP2022 (alu … s))))
220 match eqc ? addr IP2022_ADDRL_loc with
221 [ true ⇒ set_addr_reg … s (low_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
222 (addr_array_IP2022 (alu … s))) flag)
224 match eqc ? addr IP2022_DATAH_loc with
225 [ true ⇒ set_data_reg … s (high_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
227 (* nessun riporto automatico *)
228 match eqc ? addr IP2022_DATAL_loc with
229 [ true ⇒ set_data_reg … s (lownc_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
231 match eqc ? addr IP2022_CALLH_loc with
232 [ true ⇒ set_call_reg … s (high_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
234 (* nessun riporto automatico *)
235 match eqc ? addr IP2022_CALLL_loc with
236 [ true ⇒ set_call_reg … s (lownc_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
237 (* accesso normale *)
238 | false ⇒ opt_map … (fMEM addr)
239 (λmem'.Some ? (set_mem_desc … s mem'))
242 (* scrittura IP2022 di un byte *)
243 ndefinition IP2022_memory_filter_write ≝
244 λt:memory_impl.λs:any_status IP2022 t.
245 λaddr:word16.λflag:aux_mod_type.λval:byte8.
246 (* PAGE[7:5] Z[2] H[1] C [0] *)
247 match eqc ? addr IP2022_STATUS_loc with
253 (set_c_flag_IP2022 (alu … s)
254 (getn_array8T o7 ? (bits_of_byte8 val)))
255 (getn_array8T o6 ? (bits_of_byte8 val)))
256 (getn_array8T o5 ? (bits_of_byte8 val)))
257 (oct_of_exH (cnH ? val))))
258 (* accesso a registro_non_spezzato/normale *)
259 | false ⇒ IP2022_memory_filter_write_aux t s addr flag
261 (λa.mem_update t (mem_desc … s) (chk_desc … s) o0 a val) ].
263 (* scrittura IP2022 di un bit *)
264 ndefinition IP2022_memory_filter_write_bit ≝
265 λt:memory_impl.λs:any_status IP2022 t.
266 λaddr:word16.λsub:oct.λval:bool.
267 (* PAGE[7:5] Z[2] H[1] C [0] *)
268 match eqc ? addr IP2022_STATUS_loc with
269 [ true ⇒ Some ? (set_alu … s
271 [ o0 ⇒ set_page_reg_IP2022 (alu … s)
272 ((match val with [ true ⇒ or_oct o4 | false ⇒ and_oct o3 ])
273 (page_reg_IP2022 (alu … s)))
274 | o1 ⇒ set_page_reg_IP2022 (alu … s)
275 ((match val with [ true ⇒ or_oct o2 | false ⇒ and_oct o5 ])
276 (page_reg_IP2022 (alu … s)))
277 | o2 ⇒ set_page_reg_IP2022 (alu … s)
278 ((match val with [ true ⇒ or_oct o1 | false ⇒ and_oct o6 ])
279 (page_reg_IP2022 (alu … s)))
280 | o5 ⇒ set_z_flag_IP2022 (alu … s) val
281 | o6 ⇒ set_h_flag_IP2022 (alu … s) val
282 | o7 ⇒ set_c_flag_IP2022 (alu … s) val
284 (* accesso a registro_non_spezzato/normale *)
285 | false ⇒ IP2022_memory_filter_write_aux t s addr auxMode_ok
286 (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
287 (λa.mem_update_bit t (mem_desc … s) (chk_desc … s) o0 a sub val) ].