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_low3bits ≝
71 match cnL ? addrsel with
72 [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7
73 | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ].
75 ndefinition get_addrarray ≝
76 λaddrsel:byte8.λaa:aux_addrarray_type.
77 getn_array8T (get_low3bits addrsel) ? aa.
79 ndefinition set_addrarray ≝
80 λaddrsel:byte8.λaa:aux_addrarray_type.λv.
81 setn_array8T (get_low3bits addrsel) ? aa v.
83 (* *********************************** *)
84 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
85 (* *********************************** *)
88 nrecord alu_IP2022: Type ≝
91 acc_low_reg_IP2022 : byte8;
92 (* MULH: parte alta moltiplicazione *)
93 mulh_reg_IP2022 : byte8;
95 (* ADDRSEL: selettore di indirizzo *)
96 addrsel_reg_IP2022 : byte8;
97 (* ADDR [ADDRX|ADDRH|ADDRL] : array indirizzi indicizzati da ADDRSEL *)
98 addr_array_IP2022 : aux_addrarray_type;
100 (* CALL [CALLH|CALLL] : stack indirizzi di ritorno *)
101 call_stack_IP2022 : aux_callstack_type;
103 (* IP [IPH|IPL] : indirect pointer *)
104 ip_reg_IP2022 : word16;
105 (* DP [DPH|DPL] : data pointer *)
106 dp_reg_IP2022 : word16;
107 (* DATA [DATAH|DATAL] : data value *)
108 data_reg_IP2022 : word16;
109 (* SP [SPH|SPL] : stack pointer *)
110 sp_reg_IP2022 : word16;
111 (* PC [PCH|PCL] : program counter *)
112 pc_reg_IP2022 : word16;
114 (* SPEED[xxxxSSSS] : divisore del clock *)
115 speed_reg_IP2022 : exadecim;
116 (* PAGE [PPPxxxxx] : selettore pagina *)
117 page_reg_IP2022 : oct;
119 (* H: flag semi-carry (somma nibble basso) *)
120 h_flag_IP2022 : bool;
122 z_flag_IP2022 : bool;
124 c_flag_IP2022 : bool;
126 (* skip mode : effettua fetch-decode, no execute *)
127 skip_mode_IP2022 : bool
130 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)}"
131 non associative with precedence 80 for
132 @{ 'mk_alu_IP2022 $w $mulh $addrsel $addr $call $ip $dp $data $sp $pc $speed $page $hfl $zfl $cfl $skipmode }.
133 interpretation "mk_alu_IP2022" 'mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode =
134 (mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode).
140 (* setter specifico IP2022 di A *)
141 ndefinition set_acc_8_low_reg_IP2022 ≝
145 (mulh_reg_IP2022 alu)
146 (addrsel_reg_IP2022 alu)
147 (addr_array_IP2022 alu)
148 (call_stack_IP2022 alu)
151 (data_reg_IP2022 alu)
154 (speed_reg_IP2022 alu)
155 (page_reg_IP2022 alu)
159 (skip_mode_IP2022 alu).
161 (* setter specifico IP2022 di MULH *)
162 ndefinition set_mulh_reg_IP2022 ≝
165 (acc_low_reg_IP2022 alu)
167 (addrsel_reg_IP2022 alu)
168 (addr_array_IP2022 alu)
169 (call_stack_IP2022 alu)
172 (data_reg_IP2022 alu)
175 (speed_reg_IP2022 alu)
176 (page_reg_IP2022 alu)
180 (skip_mode_IP2022 alu).
182 (* setter specifico IP2022 di ADDRSEL *)
183 ndefinition set_addrsel_reg_IP2022 ≝
184 λalu.λaddrsel':byte8.
186 (acc_low_reg_IP2022 alu)
187 (mulh_reg_IP2022 alu)
189 (addr_array_IP2022 alu)
190 (call_stack_IP2022 alu)
193 (data_reg_IP2022 alu)
196 (speed_reg_IP2022 alu)
197 (page_reg_IP2022 alu)
201 (skip_mode_IP2022 alu).
203 (* setter specifico IP2022 di ADDR *)
204 ndefinition set_addr_reg_IP2022 ≝
207 (acc_low_reg_IP2022 alu)
208 (mulh_reg_IP2022 alu)
209 (addrsel_reg_IP2022 alu)
210 (set_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu) addr')
211 (call_stack_IP2022 alu)
214 (data_reg_IP2022 alu)
217 (speed_reg_IP2022 alu)
218 (page_reg_IP2022 alu)
222 (skip_mode_IP2022 alu).
224 (* setter specifico IP2022 di CALL *)
225 ndefinition set_call_reg_IP2022 ≝
228 (acc_low_reg_IP2022 alu)
229 (mulh_reg_IP2022 alu)
230 (addrsel_reg_IP2022 alu)
231 (addr_array_IP2022 alu)
232 (setn_array16T x0 ? (call_stack_IP2022 alu) call')
235 (data_reg_IP2022 alu)
238 (speed_reg_IP2022 alu)
239 (page_reg_IP2022 alu)
243 (skip_mode_IP2022 alu).
245 ndefinition push_call_reg_IP2022 ≝
248 (acc_low_reg_IP2022 alu)
249 (mulh_reg_IP2022 alu)
250 (addrsel_reg_IP2022 alu)
251 (addr_array_IP2022 alu)
252 (push_callstack (call_stack_IP2022 alu) call')
255 (data_reg_IP2022 alu)
258 (speed_reg_IP2022 alu)
259 (page_reg_IP2022 alu)
263 (skip_mode_IP2022 alu).
265 (* setter specifico IP2022 di IP *)
266 ndefinition set_ip_reg_IP2022 ≝
269 (acc_low_reg_IP2022 alu)
270 (mulh_reg_IP2022 alu)
271 (addrsel_reg_IP2022 alu)
272 (addr_array_IP2022 alu)
273 (call_stack_IP2022 alu)
276 (data_reg_IP2022 alu)
279 (speed_reg_IP2022 alu)
280 (page_reg_IP2022 alu)
284 (skip_mode_IP2022 alu).
286 (* setter specifico IP2022 di DP *)
287 ndefinition set_dp_reg_IP2022 ≝
290 (acc_low_reg_IP2022 alu)
291 (mulh_reg_IP2022 alu)
292 (addrsel_reg_IP2022 alu)
293 (addr_array_IP2022 alu)
294 (call_stack_IP2022 alu)
297 (data_reg_IP2022 alu)
300 (speed_reg_IP2022 alu)
301 (page_reg_IP2022 alu)
305 (skip_mode_IP2022 alu).
307 (* setter specifico IP2022 di DATA *)
308 ndefinition set_data_reg_IP2022 ≝
311 (acc_low_reg_IP2022 alu)
312 (mulh_reg_IP2022 alu)
313 (addrsel_reg_IP2022 alu)
314 (addr_array_IP2022 alu)
315 (call_stack_IP2022 alu)
321 (speed_reg_IP2022 alu)
322 (page_reg_IP2022 alu)
326 (skip_mode_IP2022 alu).
328 (* setter specifico IP2022 di SP *)
329 ndefinition set_sp_reg_IP2022 ≝
332 (acc_low_reg_IP2022 alu)
333 (mulh_reg_IP2022 alu)
334 (addrsel_reg_IP2022 alu)
335 (addr_array_IP2022 alu)
336 (call_stack_IP2022 alu)
339 (data_reg_IP2022 alu)
342 (speed_reg_IP2022 alu)
343 (page_reg_IP2022 alu)
347 (skip_mode_IP2022 alu).
349 (* setter specifico IP2022 di PC *)
350 ndefinition set_pc_reg_IP2022 ≝
353 (acc_low_reg_IP2022 alu)
354 (mulh_reg_IP2022 alu)
355 (addrsel_reg_IP2022 alu)
356 (addr_array_IP2022 alu)
357 (call_stack_IP2022 alu)
360 (data_reg_IP2022 alu)
363 (speed_reg_IP2022 alu)
364 (page_reg_IP2022 alu)
368 (skip_mode_IP2022 alu).
370 (* setter specifico IP2022 di SPEED *)
371 ndefinition set_speed_reg_IP2022 ≝
372 λalu.λspeed':exadecim.
374 (acc_low_reg_IP2022 alu)
375 (mulh_reg_IP2022 alu)
376 (addrsel_reg_IP2022 alu)
377 (addr_array_IP2022 alu)
378 (call_stack_IP2022 alu)
381 (data_reg_IP2022 alu)
385 (page_reg_IP2022 alu)
389 (skip_mode_IP2022 alu).
391 (* setter specifico IP2022 di PAGE *)
392 ndefinition set_page_reg_IP2022 ≝
395 (acc_low_reg_IP2022 alu)
396 (mulh_reg_IP2022 alu)
397 (addrsel_reg_IP2022 alu)
398 (addr_array_IP2022 alu)
399 (call_stack_IP2022 alu)
402 (data_reg_IP2022 alu)
405 (speed_reg_IP2022 alu)
410 (skip_mode_IP2022 alu).
412 (* setter specifico IP2022 di H *)
413 ndefinition set_h_flag_IP2022 ≝
416 (acc_low_reg_IP2022 alu)
417 (mulh_reg_IP2022 alu)
418 (addrsel_reg_IP2022 alu)
419 (addr_array_IP2022 alu)
420 (call_stack_IP2022 alu)
423 (data_reg_IP2022 alu)
426 (speed_reg_IP2022 alu)
427 (page_reg_IP2022 alu)
431 (skip_mode_IP2022 alu).
433 (* setter specifico IP2022 di Z *)
434 ndefinition set_z_flag_IP2022 ≝
437 (acc_low_reg_IP2022 alu)
438 (mulh_reg_IP2022 alu)
439 (addrsel_reg_IP2022 alu)
440 (addr_array_IP2022 alu)
441 (call_stack_IP2022 alu)
444 (data_reg_IP2022 alu)
447 (speed_reg_IP2022 alu)
448 (page_reg_IP2022 alu)
452 (skip_mode_IP2022 alu).
454 (* setter specifico IP2022 di C *)
455 ndefinition set_c_flag_IP2022 ≝
458 (acc_low_reg_IP2022 alu)
459 (mulh_reg_IP2022 alu)
460 (addrsel_reg_IP2022 alu)
461 (addr_array_IP2022 alu)
462 (call_stack_IP2022 alu)
465 (data_reg_IP2022 alu)
468 (speed_reg_IP2022 alu)
469 (page_reg_IP2022 alu)
473 (skip_mode_IP2022 alu).
475 (* setter specifico IP2022 di SKIP *)
476 ndefinition set_skip_mode_IP2022 ≝
477 λalu.λskipmode':bool.
479 (acc_low_reg_IP2022 alu)
480 (mulh_reg_IP2022 alu)
481 (addrsel_reg_IP2022 alu)
482 (addr_array_IP2022 alu)
483 (call_stack_IP2022 alu)
486 (data_reg_IP2022 alu)
489 (speed_reg_IP2022 alu)
490 (page_reg_IP2022 alu)
496 (* ***************** *)
497 (* CONFRONTO FRA ALU *)
498 (* ***************** *)
500 (* confronto registro per registro dell'IP2022 *)
501 ndefinition eq_IP2022_alu ≝
502 λalu1,alu2:alu_IP2022.
503 (eq_b8 (acc_low_reg_IP2022 alu1) (acc_low_reg_IP2022 alu2)) ⊗
504 (eq_b8 (mulh_reg_IP2022 alu1) (mulh_reg_IP2022 alu2)) ⊗
505 (eq_b8 (addrsel_reg_IP2022 alu1) (addrsel_reg_IP2022 alu2)) ⊗
506 (eq_ar8 ? eq_w24 (addr_array_IP2022 alu1) (addr_array_IP2022 alu2)) ⊗
507 (eq_ar16 ? eq_w16 (call_stack_IP2022 alu1) (call_stack_IP2022 alu2)) ⊗
508 (eq_w16 (ip_reg_IP2022 alu1) (ip_reg_IP2022 alu2)) ⊗
509 (eq_w16 (dp_reg_IP2022 alu1) (dp_reg_IP2022 alu2)) ⊗
510 (eq_w16 (data_reg_IP2022 alu1) (data_reg_IP2022 alu2)) ⊗
511 (eq_w16 (sp_reg_IP2022 alu1) (sp_reg_IP2022 alu2)) ⊗
512 (eq_w16 (pc_reg_IP2022 alu1) (pc_reg_IP2022 alu2)) ⊗
513 (eq_ex (speed_reg_IP2022 alu1) (speed_reg_IP2022 alu2)) ⊗
514 (eq_oct (page_reg_IP2022 alu1) (page_reg_IP2022 alu2)) ⊗
515 (eq_bool (h_flag_IP2022 alu1) (h_flag_IP2022 alu2)) ⊗
516 (eq_bool (z_flag_IP2022 alu1) (z_flag_IP2022 alu2)) ⊗
517 (eq_bool (c_flag_IP2022 alu1) (c_flag_IP2022 alu2)) ⊗
518 (eq_bool (skip_mode_IP2022 alu1) (skip_mode_IP2022 alu2)).