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_setter.ma".
24 include "emulator/read_write/read_write_base.ma".
26 ndefinition IP2022_ADDRSEL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x2〉〉〉.
27 ndefinition IP2022_ADDRX_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x3〉〉〉.
28 ndefinition IP2022_IPH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x4〉〉〉.
29 ndefinition IP2022_IPL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x5〉〉〉.
30 ndefinition IP2022_SPH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x6〉〉〉.
31 ndefinition IP2022_SPL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x7〉〉〉.
32 ndefinition IP2022_PCH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x8〉〉〉.
33 ndefinition IP2022_PCL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x9〉〉〉.
34 ndefinition IP2022_W_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xA〉〉〉.
35 ndefinition IP2022_STATUS_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xB〉〉〉.
36 ndefinition IP2022_DPH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xC〉〉〉.
37 ndefinition IP2022_DPL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xD〉〉〉.
38 ndefinition IP2022_SPEED_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xE〉〉〉.
39 ndefinition IP2022_MULH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xF〉〉〉.
40 ndefinition IP2022_ADDRH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x0〉〉〉.
41 ndefinition IP2022_ADDRL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x1〉〉〉.
42 ndefinition IP2022_DATAH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x2〉〉〉.
43 ndefinition IP2022_DATAL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x3〉〉〉.
44 ndefinition IP2022_CALLH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x4〉〉〉.
45 ndefinition IP2022_CALLL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x5〉〉〉.
51 (* NB: non ci sono strane indirezioni,
52 solo registri memory mapped da intercettare *)
53 ndefinition IP2022_memory_filter_read_aux ≝
54 λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.
55 λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option T.
56 (* intercettare le locazioni memory mapped *)
57 match eq_w32 addr IP2022_ADDRSEL_loc with
58 [ true ⇒ fREG (addrsel_reg_IP2022 (alu … s))
60 match eq_w32 addr IP2022_ADDRX_loc with
61 [ true ⇒ fREG (w24x (get_addrarray (addrsel_reg_IP2022 (alu … s))
62 (addr_array_IP2022 (alu … s))))
64 match eq_w32 addr IP2022_IPH_loc with
65 [ true ⇒ fREG (cnH ? (ip_reg_IP2022 (alu … s)))
67 match eq_w32 addr IP2022_IPL_loc with
68 [ true ⇒ fREG (cnL ? (ip_reg_IP2022 (alu … s)))
70 match eq_w32 addr IP2022_SPH_loc with
71 [ true ⇒ fREG (cnH ? (sp_reg_IP2022 (alu … s)))
73 match eq_w32 addr IP2022_SPL_loc with
74 [ true ⇒ fREG (cnL ? (sp_reg_IP2022 (alu … s)))
76 match eq_w32 addr IP2022_PCH_loc with
77 [ true ⇒ fREG (cnH ? (pc_reg_IP2022 (alu … s)))
79 match eq_w32 addr IP2022_PCL_loc with
80 [ true ⇒ fREG (cnL ? (pc_reg_IP2022 (alu … s)))
82 match eq_w32 addr IP2022_W_loc with
83 [ true ⇒ fREG (acc_low_reg_IP2022 (alu … s))
85 (* PAGE[7:5] Z[2] H[1] C [0] *)
86 match eq_w32 addr IP2022_STATUS_loc with
87 [ true ⇒ fREG 〈(rol_ex (ex_of_oct (page_reg_IP2022 (alu … s)))),
88 (or_ex (or_ex (match z_flag_IP2022 (alu … s) with
89 [ true ⇒ x4 | false ⇒ x0 ])
90 (match h_flag_IP2022 (alu … s) with
91 [ true ⇒ x2 | false ⇒ x0 ]))
92 (match c_flag_IP2022 (alu … s) with
93 [ true ⇒ x1 | false ⇒ x0 ]))〉
95 match eq_w32 addr IP2022_DPH_loc with
96 [ true ⇒ fREG (cnH ? (dp_reg_IP2022 (alu … s)))
98 match eq_w32 addr IP2022_DPL_loc with
99 [ true ⇒ fREG (cnL ? (dp_reg_IP2022 (alu … s)))
102 match eq_w32 addr IP2022_SPEED_loc with
103 [ true ⇒ fREG 〈x0,(speed_reg_IP2022 (alu … s))〉
105 match eq_w32 addr IP2022_MULH_loc with
106 [ true ⇒ fREG (mulh_reg_IP2022 (alu … s))
108 match eq_w32 addr IP2022_ADDRH_loc with
109 [ true ⇒ fREG (w24h (get_addrarray (addrsel_reg_IP2022 (alu … s))
110 (addr_array_IP2022 (alu … s))))
112 match eq_w32 addr IP2022_ADDRL_loc with
113 [ true ⇒ fREG (w24l (get_addrarray (addrsel_reg_IP2022 (alu … s))
114 (addr_array_IP2022 (alu … s))))
116 match eq_w32 addr IP2022_DATAH_loc with
117 [ true ⇒ fREG (cnH ? (data_reg_IP2022 (alu … s)))
119 match eq_w32 addr IP2022_DATAL_loc with
120 [ true ⇒ fREG (cnL ? (data_reg_IP2022 (alu … s)))
122 match eq_w32 addr IP2022_CALLH_loc with
123 [ true ⇒ fREG (cnH ? (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
125 match eq_w32 addr IP2022_CALLL_loc with
126 [ true ⇒ fREG (cnL ? (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
127 (* accesso normale *)
128 | false ⇒ fMEM (mem_desc … s) (chk_desc … s) addr
129 ]]]]]]]]]]]]]]]]]]]].
131 (* lettura IP2022 di un byte *)
132 ndefinition IP2022_memory_filter_read ≝
133 λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.
134 IP2022_memory_filter_read_aux t s addr byte8
136 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read t m c a).
138 (* lettura IP2022 di un bit *)
139 ndefinition IP2022_memory_filter_read_bit ≝
140 λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.λsub:oct.
141 IP2022_memory_filter_read_aux t s addr bool
142 (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
143 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read_bit t m c a sub).
149 ndefinition high_write_aux_w16 ≝
150 λf:byte8 → byte8.λw:word16.〈(f (cnH ? w)):(cnL ? w)〉.
152 ndefinition low_write_aux_w16 ≝
153 λf:byte8 → byte8.λw:word16.λflag:aux_mod_type.
156 | auxMode_inc ⇒ succ_b8
157 | auxMode_dec ⇒ pred_b8 ]) (cnH ? w)):
160 ndefinition ext_write_aux_w24 ≝
161 λf:byte8 → byte8.λw:word24.〈(f (w24x w));(w24h w);(w24l w)〉.
163 ndefinition high_write_aux_w24 ≝
164 λf:byte8 → byte8.λw:word24.〈(w24x w);(f (w24h w));(w24l w)〉.
166 ndefinition low_write_aux_w24 ≝
167 λf:byte8 → byte8.λw:word24.λflag:aux_mod_type.
168 match (match flag with
170 | auxMode_inc ⇒ succ_w16
171 | auxMode_dec ⇒ pred_w16 ]) 〈(w24x w):(w24h w)〉 with
172 [ mk_comp_num wx' wh' ⇒ 〈wx';wh';(w24l w)〉 ].
174 (* flag di carry: riportare il carry al byte logicamente superiore *)
175 ndefinition IP2022_memory_filter_write_aux ≝
176 λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.λflag:aux_mod_type.
177 λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option (aux_mem_type t).
178 (* intercettare le locazioni memory mapped *)
179 match eq_w32 addr IP2022_ADDRSEL_loc with
180 [ true ⇒ set_addrsel_reg … s (fREG (addrsel_reg_IP2022 (alu … s)))
182 match eq_w32 addr IP2022_ADDRX_loc with
183 [ true ⇒ set_addr_reg … s (ext_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
184 (addr_array_IP2022 (alu … s))))
186 match eq_w32 addr IP2022_IPH_loc with
187 [ true ⇒ set_ip_reg … s (high_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)))
189 match eq_w32 addr IP2022_IPL_loc with
190 [ true ⇒ set_ip_reg … s (low_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)) flag)
192 match eq_w32 addr IP2022_SPH_loc with
193 [ true ⇒ set_sp_reg … s (high_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)))
195 match eq_w32 addr IP2022_SPL_loc with
196 [ true ⇒ set_sp_reg … s (low_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)) flag)
198 match eq_w32 addr IP2022_PCL_loc with
199 [ true ⇒ Some ? (set_pc_reg … s (low_write_aux_w16 fREG (pc_reg_IP2022 (alu … s)) flag))
201 match eq_w32 addr IP2022_W_loc with
202 [ true ⇒ Some ? (set_acc_8_low_reg … s (fREG (acc_low_reg_IP2022 (alu … s))))
204 match eq_w32 addr IP2022_DPH_loc with
205 [ true ⇒ set_dp_reg … s (high_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)))
207 match eq_w32 addr IP2022_DPL_loc with
208 [ true ⇒ set_dp_reg … s (low_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)) flag)
210 match eq_w32 addr IP2022_MULH_loc with
211 [ true ⇒ set_mulh_reg … s (fREG (mulh_reg_IP2022 (alu … s)))
213 match eq_w32 addr IP2022_ADDRH_loc with
214 [ true ⇒ set_addr_reg … s (high_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
215 (addr_array_IP2022 (alu … s))))
217 match eq_w32 addr IP2022_ADDRL_loc with
218 [ true ⇒ set_addr_reg … s (low_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
219 (addr_array_IP2022 (alu … s))) flag)
221 match eq_w32 addr IP2022_DATAH_loc with
222 [ true ⇒ set_data_reg … s (high_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
224 match eq_w32 addr IP2022_DATAL_loc with
225 [ true ⇒ set_data_reg … s (low_write_aux_w16 fREG (data_reg_IP2022 (alu … s)) flag)
227 match eq_w32 addr IP2022_CALLH_loc with
228 [ true ⇒ set_call_reg … s (high_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
230 match eq_w32 addr IP2022_CALLL_loc with
231 [ true ⇒ set_call_reg … s (low_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))) flag)
232 (* accesso normale *)
233 | false ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr)
234 (λmem'.Some ? (set_mem_desc … s mem')) ]]]]]]]]]]]]]]]]].
236 (* scrittura IP2022 di un byte *)
237 ndefinition IP2022_memory_filter_write ≝
238 λt:memory_impl.λs:any_status IP2022 t.
239 λaddr:word32.λflag:aux_mod_type.λval:byte8.
240 (* PAGE[7:5] Z[2] H[1] C [0] *)
241 match eq_w32 addr IP2022_STATUS_loc with
242 [ true ⇒ Some ? (set_alu … s
246 (set_c_flag_IP2022 (alu … s)
247 (getn_array8T o7 ? (bits_of_byte8 val)))
248 (getn_array8T o6 ? (bits_of_byte8 val)))
249 (getn_array8T o5 ? (bits_of_byte8 val)))
250 (oct_of_exH (cnH ? val))))
251 (* accesso a registro_non_spezzato/normale *)
252 | false ⇒ IP2022_memory_filter_write_aux t s addr flag
254 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update t m c a val) ].
256 (* scrittura IP2022 di un bit *)
257 ndefinition IP2022_memory_filter_write_bit ≝
258 λt:memory_impl.λs:any_status IP2022 t.
259 λaddr:word32.λsub:oct.λval:bool.
260 (* PAGE[7:5] Z[2] H[1] C [0] *)
261 match eq_w32 addr IP2022_STATUS_loc with
262 [ true ⇒ Some ? (set_alu … s
264 [ o0 ⇒ set_page_reg_IP2022 (alu … s)
265 ((match val with [ true ⇒ or_oct o4 | false ⇒ and_oct o3 ])
266 (page_reg_IP2022 (alu … s)))
267 | o1 ⇒ set_page_reg_IP2022 (alu … s)
268 ((match val with [ true ⇒ or_oct o2 | false ⇒ and_oct o5 ])
269 (page_reg_IP2022 (alu … s)))
270 | o2 ⇒ set_page_reg_IP2022 (alu … s)
271 ((match val with [ true ⇒ or_oct o1 | false ⇒ and_oct o6 ])
272 (page_reg_IP2022 (alu … s)))
273 | o5 ⇒ set_z_flag_IP2022 (alu … s) val
274 | o6 ⇒ set_h_flag_IP2022 (alu … s) val
275 | o7 ⇒ set_c_flag_IP2022 (alu … s) val
277 (* accesso a registro_non_spezzato/normale *)
278 | false ⇒ IP2022_memory_filter_write_aux t s addr auxMode_ok
279 (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
280 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update_bit t m c a sub val) ].