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 lowc_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 lownc_write_aux_w16 ≝
161 λf:byte8 → byte8.λw:word16.〈(cnH ? w):(f (cnL ? w))〉.
163 ndefinition ext_write_aux_w24 ≝
164 λf:byte8 → byte8.λw:word24.〈(f (w24x w));(w24h w);(w24l w)〉.
166 ndefinition high_write_aux_w24 ≝
167 λf:byte8 → byte8.λw:word24.〈(w24x w);(f (w24h w));(w24l w)〉.
169 ndefinition low_write_aux_w24 ≝
170 λf:byte8 → byte8.λw:word24.λflag:aux_mod_type.
171 match (match flag with
173 | auxMode_inc ⇒ succ_w16
174 | auxMode_dec ⇒ pred_w16 ]) 〈(w24x w):(w24h w)〉 with
175 [ mk_comp_num wx' wh' ⇒ 〈wx';wh';(w24l w)〉 ].
177 (* flag di carry: riportare il carry al byte logicamente superiore *)
178 (* modifica di pc: non inserita nella stato ma postposta *)
179 ndefinition IP2022_memory_filter_write_aux ≝
180 λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.λflag:aux_mod_type.
181 λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option (aux_mem_type t).
182 (* intercettare le locazioni memory mapped *)
183 match eq_w32 addr IP2022_ADDRSEL_loc with
184 [ true ⇒ set_addrsel_reg … s (fREG (addrsel_reg_IP2022 (alu … s)))
186 match eq_w32 addr IP2022_ADDRX_loc with
187 [ true ⇒ set_addr_reg … s (ext_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
188 (addr_array_IP2022 (alu … s))))
190 match eq_w32 addr IP2022_IPH_loc with
191 [ true ⇒ set_ip_reg … s (high_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)))
193 match eq_w32 addr IP2022_IPL_loc with
194 [ true ⇒ set_ip_reg … s (lowc_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)) flag)
196 match eq_w32 addr IP2022_SPH_loc with
197 [ true ⇒ set_sp_reg … s (high_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)))
199 match eq_w32 addr IP2022_SPL_loc with
200 [ true ⇒ set_sp_reg … s (lowc_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)) flag)
202 match eq_w32 addr IP2022_PCL_loc with
203 [ true ⇒ Some ? (set_pc_reg … s (lowc_write_aux_w16 fREG (pc_reg_IP2022 (alu … s)) flag))
205 match eq_w32 addr IP2022_W_loc with
206 [ true ⇒ Some ? (set_acc_8_low_reg … s (fREG (acc_low_reg_IP2022 (alu … s))))
208 match eq_w32 addr IP2022_DPH_loc with
209 [ true ⇒ set_dp_reg … s (high_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)))
211 match eq_w32 addr IP2022_DPL_loc with
212 [ true ⇒ set_dp_reg … s (lowc_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)) flag)
214 match eq_w32 addr IP2022_MULH_loc with
215 [ true ⇒ set_mulh_reg … s (fREG (mulh_reg_IP2022 (alu … s)))
217 match eq_w32 addr IP2022_ADDRH_loc with
218 [ true ⇒ set_addr_reg … s (high_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
219 (addr_array_IP2022 (alu … s))))
221 match eq_w32 addr IP2022_ADDRL_loc with
222 [ true ⇒ set_addr_reg … s (low_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
223 (addr_array_IP2022 (alu … s))) flag)
225 match eq_w32 addr IP2022_DATAH_loc with
226 [ true ⇒ set_data_reg … s (high_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
228 (* nessun riporto automatico *)
229 match eq_w32 addr IP2022_DATAL_loc with
230 [ true ⇒ set_data_reg … s (lownc_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
232 match eq_w32 addr IP2022_CALLH_loc with
233 [ true ⇒ set_call_reg … s (high_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
235 (* nessun riporto automatico *)
236 match eq_w32 addr IP2022_CALLL_loc with
237 [ true ⇒ set_call_reg … s (lownc_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
238 (* accesso normale *)
239 | false ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr)
240 (λmem'.Some ? (set_mem_desc … s mem'))
243 (* scrittura IP2022 di un byte *)
244 ndefinition IP2022_memory_filter_write ≝
245 λt:memory_impl.λs:any_status IP2022 t.
246 λaddr:word32.λflag:aux_mod_type.λval:byte8.
247 (* PAGE[7:5] Z[2] H[1] C [0] *)
248 match eq_w32 addr IP2022_STATUS_loc with
254 (set_c_flag_IP2022 (alu … s)
255 (getn_array8T o7 ? (bits_of_byte8 val)))
256 (getn_array8T o6 ? (bits_of_byte8 val)))
257 (getn_array8T o5 ? (bits_of_byte8 val)))
258 (oct_of_exH (cnH ? val))))
259 (* accesso a registro_non_spezzato/normale *)
260 | false ⇒ IP2022_memory_filter_write_aux t s addr flag
262 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update t m c a val) ].
264 (* scrittura IP2022 di un bit *)
265 ndefinition IP2022_memory_filter_write_bit ≝
266 λt:memory_impl.λs:any_status IP2022 t.
267 λaddr:word32.λsub:oct.λval:bool.
268 (* PAGE[7:5] Z[2] H[1] C [0] *)
269 match eq_w32 addr IP2022_STATUS_loc with
270 [ true ⇒ Some ? (set_alu … s
272 [ o0 ⇒ set_page_reg_IP2022 (alu … s)
273 ((match val with [ true ⇒ or_oct o4 | false ⇒ and_oct o3 ])
274 (page_reg_IP2022 (alu … s)))
275 | o1 ⇒ set_page_reg_IP2022 (alu … s)
276 ((match val with [ true ⇒ or_oct o2 | false ⇒ and_oct o5 ])
277 (page_reg_IP2022 (alu … s)))
278 | o2 ⇒ set_page_reg_IP2022 (alu … s)
279 ((match val with [ true ⇒ or_oct o1 | false ⇒ and_oct o6 ])
280 (page_reg_IP2022 (alu … s)))
281 | o5 ⇒ set_z_flag_IP2022 (alu … s) val
282 | o6 ⇒ set_h_flag_IP2022 (alu … s) val
283 | o7 ⇒ set_c_flag_IP2022 (alu … s) val
285 (* accesso a registro_non_spezzato/normale *)
286 | false ⇒ IP2022_memory_filter_write_aux t s addr auxMode_ok
287 (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
288 (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update_bit t m c a sub val) ].