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/memory/memory_struct.ma".
24 include "num/word16.ma".
25 include "num/word24.ma".
27 (* ******************************** *)
28 (* IP2022 REGISTER SPECIAL HARDWARE *)
29 (* ******************************** *)
31 (* (Top Of Stack) : CALLH/CALL ↑ CALLH/CALL ↓ *)
32 (* Pos2-15 : ... ↑ ... ↓ *)
33 (* Pos16 : 0xFFFF ↑ ... ↓ *)
34 ndefinition aux_callstack_type ≝ Array16T word16.
36 (* Top Of Stack : 0xFFFF on reset *)
37 ndefinition new_callstack ≝
38 mk_Array16T ? (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉)
39 (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉)
40 (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉)
41 (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉).
43 ndefinition pop_callstack ≝
44 λcs:aux_callstack_type.
46 (mk_Array16T ? (a16_2 ? cs) (a16_3 ? cs) (a16_4 ? cs) (a16_5 ? cs)
47 (a16_6 ? cs) (a16_7 ? cs) (a16_8 ? cs) (a16_9 ? cs)
48 (a16_10 ? cs) (a16_11 ? cs) (a16_12 ? cs) (a16_13 ? cs)
49 (a16_14 ? cs) (a16_15 ? cs) (a16_16 ? cs) 〈〈xF,xF〉:〈xF,xF〉〉).
51 ndefinition push_callstack ≝
52 λcs:aux_callstack_type.λtop.
53 mk_Array16T ? top (a16_1 ? cs) (a16_2 ? cs) (a16_3 ? cs)
54 (a16_4 ? cs) (a16_5 ? cs) (a16_6 ? cs) (a16_7 ? cs)
55 (a16_8 ? cs) (a16_9 ? cs) (a16_10 ? cs) (a16_11 ? cs)
56 (a16_12 ? cs) (a16_13 ? cs) (a16_14 ? cs) (a16_15 ? cs).
58 (* array ad accesso diretto di 8 registri ADDR a 24bit *)
59 (* selezione con registro ADDRSEL, solo i primi 3bit validi *)
60 ndefinition aux_addrarray_type ≝ Array8T word24.
62 (* tutti a 0x000000 on reset *)
63 ndefinition new_addrarray ≝
64 mk_Array8T ? (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
65 (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
66 (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
67 (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉).
69 ndefinition get_addrarray ≝
70 λaddrsel:byte8.λaa:aux_addrarray_type.
71 getn_array8T (oct_of_exL (cnL ? addrsel)) ? aa.
73 ndefinition set_addrarray ≝
74 λaddrsel:byte8.λaa:aux_addrarray_type.λv.
75 setn_array8T (oct_of_exL (cnL ? addrsel)) ? aa v.
77 (* *********************************** *)
78 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
79 (* *********************************** *)
82 nrecord alu_IP2022: Type ≝
85 acc_low_reg_IP2022 : byte8;
86 (* MULH: parte alta moltiplicazione *)
87 mulh_reg_IP2022 : byte8;
89 (* ADDRSEL: selettore di indirizzo *)
90 addrsel_reg_IP2022 : byte8;
91 (* ADDR [ADDRX|ADDRH|ADDRL] : array indirizzi indicizzati da ADDRSEL *)
92 addr_array_IP2022 : aux_addrarray_type;
94 (* CALL [CALLH|CALLL] : stack indirizzi di ritorno *)
95 call_stack_IP2022 : aux_callstack_type;
97 (* IP [IPH|IPL] : indirect pointer *)
98 ip_reg_IP2022 : word16;
99 (* DP [DPH|DPL] : data pointer *)
100 dp_reg_IP2022 : word16;
101 (* DATA [DATAH|DATAL] : data value *)
102 data_reg_IP2022 : word16;
103 (* SP [SPH|SPL] : stack pointer *)
104 sp_reg_IP2022 : word16;
105 (* PC [PCH|PCL] : program counter *)
106 pc_reg_IP2022 : word16;
108 (* SPEED[xxxxSSSS] : divisore del clock *)
109 speed_reg_IP2022 : exadecim;
110 (* PAGE [PPPxxxxx] : selettore pagina *)
111 page_reg_IP2022 : oct;
113 (* H: flag semi-carry (somma nibble basso) *)
114 h_flag_IP2022 : bool;
116 z_flag_IP2022 : bool;
118 c_flag_IP2022 : bool;
120 (* skip mode : effettua fetch-decode, no execute *)
121 skip_mode_IP2022 : bool
124 notation "{hvbox('W_Reg' ≝ w ; break 'MulH_Reg' ≝ mulh ; break 'Addrsel_Reg' ≝ addrsel ; break 'Addr_Array' ≝ addr ; break 'Call_Stack' ≝ call ; break 'Ip_Reg' ≝ ip ; break 'Dp_Reg' ≝ dp ; break 'Data_Reg' ≝ data ; break 'Sp_Reg' ≝ sp ; break 'Pc_Reg' ≝ pc ; break 'Speed_Reg' ≝ speed ; break 'Page_Reg' ≝ page ; break 'H_Flag' ≝ hfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'Skip_Mode' ≝ skipmode)}"
125 non associative with precedence 80 for
126 @{ 'mk_alu_IP2022 $w $mulh $addrsel $addr $call $ip $dp $data $sp $pc $speed $page $hfl $zfl $cfl $skipmode }.
127 interpretation "mk_alu_IP2022" 'mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode =
128 (mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode).
134 (* setter specifico IP2022 di A *)
135 ndefinition set_acc_8_low_reg_IP2022 ≝
139 (mulh_reg_IP2022 alu)
140 (addrsel_reg_IP2022 alu)
141 (addr_array_IP2022 alu)
142 (call_stack_IP2022 alu)
145 (data_reg_IP2022 alu)
148 (speed_reg_IP2022 alu)
149 (page_reg_IP2022 alu)
153 (skip_mode_IP2022 alu).
155 (* setter specifico IP2022 di MULH *)
156 ndefinition set_mulh_reg_IP2022 ≝
159 (acc_low_reg_IP2022 alu)
161 (addrsel_reg_IP2022 alu)
162 (addr_array_IP2022 alu)
163 (call_stack_IP2022 alu)
166 (data_reg_IP2022 alu)
169 (speed_reg_IP2022 alu)
170 (page_reg_IP2022 alu)
174 (skip_mode_IP2022 alu).
176 (* setter specifico IP2022 di ADDRSEL *)
177 ndefinition set_addrsel_reg_IP2022 ≝
178 λalu.λaddrsel':byte8.
180 (acc_low_reg_IP2022 alu)
181 (mulh_reg_IP2022 alu)
183 (addr_array_IP2022 alu)
184 (call_stack_IP2022 alu)
187 (data_reg_IP2022 alu)
190 (speed_reg_IP2022 alu)
191 (page_reg_IP2022 alu)
195 (skip_mode_IP2022 alu).
197 (* setter specifico IP2022 di ADDR *)
198 ndefinition set_addr_reg_IP2022 ≝
201 (acc_low_reg_IP2022 alu)
202 (mulh_reg_IP2022 alu)
203 (addrsel_reg_IP2022 alu)
204 (set_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu) addr')
205 (call_stack_IP2022 alu)
208 (data_reg_IP2022 alu)
211 (speed_reg_IP2022 alu)
212 (page_reg_IP2022 alu)
216 (skip_mode_IP2022 alu).
218 ndefinition get_addr_reg_IP2022 ≝
219 λalu.get_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu).
221 (* setter specifico IP2022 di CALL *)
222 ndefinition set_call_reg_IP2022 ≝
225 (acc_low_reg_IP2022 alu)
226 (mulh_reg_IP2022 alu)
227 (addrsel_reg_IP2022 alu)
228 (addr_array_IP2022 alu)
229 (setn_array16T x0 ? (call_stack_IP2022 alu) call')
232 (data_reg_IP2022 alu)
235 (speed_reg_IP2022 alu)
236 (page_reg_IP2022 alu)
240 (skip_mode_IP2022 alu).
242 ndefinition get_call_reg_IP2022 ≝
243 λalu.getn_array16T x0 ? (call_stack_IP2022 alu).
245 ndefinition set_call_stack_IP2022 ≝
246 λalu.λcall':aux_callstack_type.
248 (acc_low_reg_IP2022 alu)
249 (mulh_reg_IP2022 alu)
250 (addrsel_reg_IP2022 alu)
251 (addr_array_IP2022 alu)
255 (data_reg_IP2022 alu)
258 (speed_reg_IP2022 alu)
259 (page_reg_IP2022 alu)
263 (skip_mode_IP2022 alu).
265 ndefinition push_call_reg_IP2022 ≝
268 (acc_low_reg_IP2022 alu)
269 (mulh_reg_IP2022 alu)
270 (addrsel_reg_IP2022 alu)
271 (addr_array_IP2022 alu)
272 (push_callstack (call_stack_IP2022 alu) call')
275 (data_reg_IP2022 alu)
278 (speed_reg_IP2022 alu)
279 (page_reg_IP2022 alu)
283 (skip_mode_IP2022 alu).
285 ndefinition pop_call_reg_IP2022 ≝
286 λalu.match pop_callstack (call_stack_IP2022 alu) with
287 [ pair val call' ⇒ pair … val (set_call_stack_IP2022 alu call') ].
289 (* setter specifico IP2022 di IP *)
290 ndefinition set_ip_reg_IP2022 ≝
293 (acc_low_reg_IP2022 alu)
294 (mulh_reg_IP2022 alu)
295 (addrsel_reg_IP2022 alu)
296 (addr_array_IP2022 alu)
297 (call_stack_IP2022 alu)
300 (data_reg_IP2022 alu)
303 (speed_reg_IP2022 alu)
304 (page_reg_IP2022 alu)
308 (skip_mode_IP2022 alu).
310 (* setter specifico IP2022 di DP *)
311 ndefinition set_dp_reg_IP2022 ≝
314 (acc_low_reg_IP2022 alu)
315 (mulh_reg_IP2022 alu)
316 (addrsel_reg_IP2022 alu)
317 (addr_array_IP2022 alu)
318 (call_stack_IP2022 alu)
321 (data_reg_IP2022 alu)
324 (speed_reg_IP2022 alu)
325 (page_reg_IP2022 alu)
329 (skip_mode_IP2022 alu).
331 (* setter specifico IP2022 di DATA *)
332 ndefinition set_data_reg_IP2022 ≝
335 (acc_low_reg_IP2022 alu)
336 (mulh_reg_IP2022 alu)
337 (addrsel_reg_IP2022 alu)
338 (addr_array_IP2022 alu)
339 (call_stack_IP2022 alu)
345 (speed_reg_IP2022 alu)
346 (page_reg_IP2022 alu)
350 (skip_mode_IP2022 alu).
352 (* setter specifico IP2022 di SP *)
353 ndefinition set_sp_reg_IP2022 ≝
356 (acc_low_reg_IP2022 alu)
357 (mulh_reg_IP2022 alu)
358 (addrsel_reg_IP2022 alu)
359 (addr_array_IP2022 alu)
360 (call_stack_IP2022 alu)
363 (data_reg_IP2022 alu)
366 (speed_reg_IP2022 alu)
367 (page_reg_IP2022 alu)
371 (skip_mode_IP2022 alu).
373 (* setter specifico IP2022 di PC *)
374 ndefinition set_pc_reg_IP2022 ≝
377 (acc_low_reg_IP2022 alu)
378 (mulh_reg_IP2022 alu)
379 (addrsel_reg_IP2022 alu)
380 (addr_array_IP2022 alu)
381 (call_stack_IP2022 alu)
384 (data_reg_IP2022 alu)
387 (speed_reg_IP2022 alu)
388 (page_reg_IP2022 alu)
392 (skip_mode_IP2022 alu).
394 (* setter specifico IP2022 di SPEED *)
395 ndefinition set_speed_reg_IP2022 ≝
396 λalu.λspeed':exadecim.
398 (acc_low_reg_IP2022 alu)
399 (mulh_reg_IP2022 alu)
400 (addrsel_reg_IP2022 alu)
401 (addr_array_IP2022 alu)
402 (call_stack_IP2022 alu)
405 (data_reg_IP2022 alu)
409 (page_reg_IP2022 alu)
413 (skip_mode_IP2022 alu).
415 (* setter specifico IP2022 di PAGE *)
416 ndefinition set_page_reg_IP2022 ≝
419 (acc_low_reg_IP2022 alu)
420 (mulh_reg_IP2022 alu)
421 (addrsel_reg_IP2022 alu)
422 (addr_array_IP2022 alu)
423 (call_stack_IP2022 alu)
426 (data_reg_IP2022 alu)
429 (speed_reg_IP2022 alu)
434 (skip_mode_IP2022 alu).
436 (* setter specifico IP2022 di H *)
437 ndefinition set_h_flag_IP2022 ≝
440 (acc_low_reg_IP2022 alu)
441 (mulh_reg_IP2022 alu)
442 (addrsel_reg_IP2022 alu)
443 (addr_array_IP2022 alu)
444 (call_stack_IP2022 alu)
447 (data_reg_IP2022 alu)
450 (speed_reg_IP2022 alu)
451 (page_reg_IP2022 alu)
455 (skip_mode_IP2022 alu).
457 (* setter specifico IP2022 di Z *)
458 ndefinition set_z_flag_IP2022 ≝
461 (acc_low_reg_IP2022 alu)
462 (mulh_reg_IP2022 alu)
463 (addrsel_reg_IP2022 alu)
464 (addr_array_IP2022 alu)
465 (call_stack_IP2022 alu)
468 (data_reg_IP2022 alu)
471 (speed_reg_IP2022 alu)
472 (page_reg_IP2022 alu)
476 (skip_mode_IP2022 alu).
478 (* setter specifico IP2022 di C *)
479 ndefinition set_c_flag_IP2022 ≝
482 (acc_low_reg_IP2022 alu)
483 (mulh_reg_IP2022 alu)
484 (addrsel_reg_IP2022 alu)
485 (addr_array_IP2022 alu)
486 (call_stack_IP2022 alu)
489 (data_reg_IP2022 alu)
492 (speed_reg_IP2022 alu)
493 (page_reg_IP2022 alu)
497 (skip_mode_IP2022 alu).
499 (* setter specifico IP2022 di SKIP *)
500 ndefinition set_skip_mode_IP2022 ≝
501 λalu.λskipmode':bool.
503 (acc_low_reg_IP2022 alu)
504 (mulh_reg_IP2022 alu)
505 (addrsel_reg_IP2022 alu)
506 (addr_array_IP2022 alu)
507 (call_stack_IP2022 alu)
510 (data_reg_IP2022 alu)
513 (speed_reg_IP2022 alu)
514 (page_reg_IP2022 alu)
520 (* ***************** *)
521 (* CONFRONTO FRA ALU *)
522 (* ***************** *)
524 (* confronto registro per registro dell'IP2022 *)
525 ndefinition eq_IP2022_alu ≝
526 λalu1,alu2:alu_IP2022.
527 (eq_b8 (acc_low_reg_IP2022 alu1) (acc_low_reg_IP2022 alu2)) ⊗
528 (eq_b8 (mulh_reg_IP2022 alu1) (mulh_reg_IP2022 alu2)) ⊗
529 (eq_b8 (addrsel_reg_IP2022 alu1) (addrsel_reg_IP2022 alu2)) ⊗
530 (eq_ar8 ? eq_w24 (addr_array_IP2022 alu1) (addr_array_IP2022 alu2)) ⊗
531 (eq_ar16 ? eq_w16 (call_stack_IP2022 alu1) (call_stack_IP2022 alu2)) ⊗
532 (eq_w16 (ip_reg_IP2022 alu1) (ip_reg_IP2022 alu2)) ⊗
533 (eq_w16 (dp_reg_IP2022 alu1) (dp_reg_IP2022 alu2)) ⊗
534 (eq_w16 (data_reg_IP2022 alu1) (data_reg_IP2022 alu2)) ⊗
535 (eq_w16 (sp_reg_IP2022 alu1) (sp_reg_IP2022 alu2)) ⊗
536 (eq_w16 (pc_reg_IP2022 alu1) (pc_reg_IP2022 alu2)) ⊗
537 (eq_ex (speed_reg_IP2022 alu1) (speed_reg_IP2022 alu2)) ⊗
538 (eq_oct (page_reg_IP2022 alu1) (page_reg_IP2022 alu2)) ⊗
539 (eq_bool (h_flag_IP2022 alu1) (h_flag_IP2022 alu2)) ⊗
540 (eq_bool (z_flag_IP2022 alu1) (z_flag_IP2022 alu2)) ⊗
541 (eq_bool (c_flag_IP2022 alu1) (c_flag_IP2022 alu2)) ⊗
542 (eq_bool (skip_mode_IP2022 alu1) (skip_mode_IP2022 alu2)).