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 nlemma callstack_is_comparable : comparable.
59 @ (aux_callstack_type)
60 ##[ napply (zeroc (ar16_is_comparable word16_is_comparable))
61 ##| napply (forallc (ar16_is_comparable word16_is_comparable))
62 ##| napply (eqc (ar16_is_comparable word16_is_comparable))
63 ##| napply (eqc_to_eq (ar16_is_comparable word16_is_comparable))
64 ##| napply (eq_to_eqc (ar16_is_comparable word16_is_comparable))
65 ##| napply (neqc_to_neq (ar16_is_comparable word16_is_comparable))
66 ##| napply (neq_to_neqc (ar16_is_comparable word16_is_comparable))
67 ##| napply (decidable_c (ar16_is_comparable word16_is_comparable))
68 ##| napply (symmetric_eqc (ar16_is_comparable word16_is_comparable))
72 unification hint 0 ≔ ⊢ carr callstack_is_comparable ≡ aux_callstack_type.
74 (* array ad accesso diretto di 8 registri ADDR a 24bit *)
75 (* selezione con registro ADDRSEL, solo i primi 3bit validi *)
76 ndefinition aux_addrarray_type ≝ Array8T word24.
78 (* tutti a 0x000000 on reset *)
79 ndefinition new_addrarray : aux_addrarray_type ≝
80 mk_Array8T ? (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
81 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?).
83 ndefinition get_addrarray ≝
84 λaddrsel:byte8.λaa:aux_addrarray_type.
85 getn_array8T (oct_of_exL (cnL ? addrsel)) ? aa.
87 ndefinition set_addrarray ≝
88 λaddrsel:byte8.λaa:aux_addrarray_type.λv.
89 setn_array8T (oct_of_exL (cnL ? addrsel)) ? aa v.
91 nlemma addrarray_is_comparable : comparable.
92 @ (aux_addrarray_type)
93 ##[ napply (zeroc (ar8_is_comparable word24_is_comparable))
94 ##| napply (forallc (ar8_is_comparable word24_is_comparable))
95 ##| napply (eqc (ar8_is_comparable word24_is_comparable))
96 ##| napply (eqc_to_eq (ar8_is_comparable word24_is_comparable))
97 ##| napply (eq_to_eqc (ar8_is_comparable word24_is_comparable))
98 ##| napply (neqc_to_neq (ar8_is_comparable word24_is_comparable))
99 ##| napply (neq_to_neqc (ar8_is_comparable word24_is_comparable))
100 ##| napply (decidable_c (ar8_is_comparable word24_is_comparable))
101 ##| napply (symmetric_eqc (ar8_is_comparable word24_is_comparable))
105 unification hint 0 ≔ ⊢ carr addrarray_is_comparable ≡ aux_addrarray_type.
107 (* *********************************** *)
108 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
109 (* *********************************** *)
111 (* ALU dell'IP2022 *)
112 nrecord alu_IP2022: Type ≝
114 (* W: accumulatore *)
115 acc_low_reg_IP2022 : byte8;
116 (* MULH: parte alta moltiplicazione *)
117 mulh_reg_IP2022 : byte8;
119 (* ADDRSEL: selettore di indirizzo *)
120 addrsel_reg_IP2022 : byte8;
121 (* ADDR [ADDRX|ADDRH|ADDRL] : array indirizzi indicizzati da ADDRSEL *)
122 addr_array_IP2022 : aux_addrarray_type;
124 (* CALL [CALLH|CALLL] : stack indirizzi di ritorno *)
125 call_stack_IP2022 : aux_callstack_type;
127 (* IP [IPH|IPL] : indirect pointer *)
128 ip_reg_IP2022 : word16;
129 (* DP [DPH|DPL] : data pointer *)
130 dp_reg_IP2022 : word16;
131 (* DATA [DATAH|DATAL] : data value *)
132 data_reg_IP2022 : word16;
133 (* SP [SPH|SPL] : stack pointer *)
134 sp_reg_IP2022 : word16;
135 (* PC [PCH|PCL] : program counter *)
136 pc_reg_IP2022 : word16;
138 (* SPEED[xxxxSSSS] : divisore del clock *)
139 speed_reg_IP2022 : exadecim;
140 (* PAGE [PPPxxxxx] : selettore pagina *)
141 page_reg_IP2022 : oct;
143 (* H: flag semi-carry (somma nibble basso) *)
144 h_flag_IP2022 : bool;
146 z_flag_IP2022 : bool;
148 c_flag_IP2022 : bool;
150 (* skip mode : effettua fetch-decode, no execute *)
151 skip_mode_IP2022 : bool
154 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)}"
155 non associative with precedence 80 for
156 @{ 'mk_alu_IP2022 $w $mulh $addrsel $addr $call $ip $dp $data $sp $pc $speed $page $hfl $zfl $cfl $skipmode }.
157 interpretation "mk_alu_IP2022" 'mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode =
158 (mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode).
164 (* setter specifico IP2022 di A *)
165 ndefinition set_acc_8_low_reg_IP2022 ≝
169 (mulh_reg_IP2022 alu)
170 (addrsel_reg_IP2022 alu)
171 (addr_array_IP2022 alu)
172 (call_stack_IP2022 alu)
175 (data_reg_IP2022 alu)
178 (speed_reg_IP2022 alu)
179 (page_reg_IP2022 alu)
183 (skip_mode_IP2022 alu).
185 (* setter specifico IP2022 di MULH *)
186 ndefinition set_mulh_reg_IP2022 ≝
189 (acc_low_reg_IP2022 alu)
191 (addrsel_reg_IP2022 alu)
192 (addr_array_IP2022 alu)
193 (call_stack_IP2022 alu)
196 (data_reg_IP2022 alu)
199 (speed_reg_IP2022 alu)
200 (page_reg_IP2022 alu)
204 (skip_mode_IP2022 alu).
206 (* setter specifico IP2022 di ADDRSEL *)
207 ndefinition set_addrsel_reg_IP2022 ≝
208 λalu.λaddrsel':byte8.
210 (acc_low_reg_IP2022 alu)
211 (mulh_reg_IP2022 alu)
213 (addr_array_IP2022 alu)
214 (call_stack_IP2022 alu)
217 (data_reg_IP2022 alu)
220 (speed_reg_IP2022 alu)
221 (page_reg_IP2022 alu)
225 (skip_mode_IP2022 alu).
227 (* setter specifico IP2022 di ADDR *)
228 ndefinition set_addr_reg_IP2022 ≝
231 (acc_low_reg_IP2022 alu)
232 (mulh_reg_IP2022 alu)
233 (addrsel_reg_IP2022 alu)
234 (set_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu) addr')
235 (call_stack_IP2022 alu)
238 (data_reg_IP2022 alu)
241 (speed_reg_IP2022 alu)
242 (page_reg_IP2022 alu)
246 (skip_mode_IP2022 alu).
248 ndefinition get_addr_reg_IP2022 ≝
249 λalu.get_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu).
251 (* setter specifico IP2022 di CALL *)
252 ndefinition set_call_reg_IP2022 ≝
255 (acc_low_reg_IP2022 alu)
256 (mulh_reg_IP2022 alu)
257 (addrsel_reg_IP2022 alu)
258 (addr_array_IP2022 alu)
259 (setn_array16T x0 ? (call_stack_IP2022 alu) call')
262 (data_reg_IP2022 alu)
265 (speed_reg_IP2022 alu)
266 (page_reg_IP2022 alu)
270 (skip_mode_IP2022 alu).
272 ndefinition get_call_reg_IP2022 ≝
273 λalu.getn_array16T x0 ? (call_stack_IP2022 alu).
275 ndefinition set_call_stack_IP2022 ≝
276 λalu.λcall':aux_callstack_type.
278 (acc_low_reg_IP2022 alu)
279 (mulh_reg_IP2022 alu)
280 (addrsel_reg_IP2022 alu)
281 (addr_array_IP2022 alu)
285 (data_reg_IP2022 alu)
288 (speed_reg_IP2022 alu)
289 (page_reg_IP2022 alu)
293 (skip_mode_IP2022 alu).
295 ndefinition push_call_reg_IP2022 ≝
298 (acc_low_reg_IP2022 alu)
299 (mulh_reg_IP2022 alu)
300 (addrsel_reg_IP2022 alu)
301 (addr_array_IP2022 alu)
302 (push_callstack (call_stack_IP2022 alu) call')
305 (data_reg_IP2022 alu)
308 (speed_reg_IP2022 alu)
309 (page_reg_IP2022 alu)
313 (skip_mode_IP2022 alu).
315 ndefinition pop_call_reg_IP2022 ≝
316 λalu.match pop_callstack (call_stack_IP2022 alu) with
317 [ pair val call' ⇒ pair … val (set_call_stack_IP2022 alu call') ].
319 (* setter specifico IP2022 di IP *)
320 ndefinition set_ip_reg_IP2022 ≝
323 (acc_low_reg_IP2022 alu)
324 (mulh_reg_IP2022 alu)
325 (addrsel_reg_IP2022 alu)
326 (addr_array_IP2022 alu)
327 (call_stack_IP2022 alu)
330 (data_reg_IP2022 alu)
333 (speed_reg_IP2022 alu)
334 (page_reg_IP2022 alu)
338 (skip_mode_IP2022 alu).
340 (* setter specifico IP2022 di DP *)
341 ndefinition set_dp_reg_IP2022 ≝
344 (acc_low_reg_IP2022 alu)
345 (mulh_reg_IP2022 alu)
346 (addrsel_reg_IP2022 alu)
347 (addr_array_IP2022 alu)
348 (call_stack_IP2022 alu)
351 (data_reg_IP2022 alu)
354 (speed_reg_IP2022 alu)
355 (page_reg_IP2022 alu)
359 (skip_mode_IP2022 alu).
361 (* setter specifico IP2022 di DATA *)
362 ndefinition set_data_reg_IP2022 ≝
365 (acc_low_reg_IP2022 alu)
366 (mulh_reg_IP2022 alu)
367 (addrsel_reg_IP2022 alu)
368 (addr_array_IP2022 alu)
369 (call_stack_IP2022 alu)
375 (speed_reg_IP2022 alu)
376 (page_reg_IP2022 alu)
380 (skip_mode_IP2022 alu).
382 (* setter specifico IP2022 di SP *)
383 ndefinition set_sp_reg_IP2022 ≝
386 (acc_low_reg_IP2022 alu)
387 (mulh_reg_IP2022 alu)
388 (addrsel_reg_IP2022 alu)
389 (addr_array_IP2022 alu)
390 (call_stack_IP2022 alu)
393 (data_reg_IP2022 alu)
396 (speed_reg_IP2022 alu)
397 (page_reg_IP2022 alu)
401 (skip_mode_IP2022 alu).
403 (* setter specifico IP2022 di PC *)
404 ndefinition set_pc_reg_IP2022 ≝
407 (acc_low_reg_IP2022 alu)
408 (mulh_reg_IP2022 alu)
409 (addrsel_reg_IP2022 alu)
410 (addr_array_IP2022 alu)
411 (call_stack_IP2022 alu)
414 (data_reg_IP2022 alu)
417 (speed_reg_IP2022 alu)
418 (page_reg_IP2022 alu)
422 (skip_mode_IP2022 alu).
424 (* setter specifico IP2022 di SPEED *)
425 ndefinition set_speed_reg_IP2022 ≝
426 λalu.λspeed':exadecim.
428 (acc_low_reg_IP2022 alu)
429 (mulh_reg_IP2022 alu)
430 (addrsel_reg_IP2022 alu)
431 (addr_array_IP2022 alu)
432 (call_stack_IP2022 alu)
435 (data_reg_IP2022 alu)
439 (page_reg_IP2022 alu)
443 (skip_mode_IP2022 alu).
445 (* setter specifico IP2022 di PAGE *)
446 ndefinition set_page_reg_IP2022 ≝
449 (acc_low_reg_IP2022 alu)
450 (mulh_reg_IP2022 alu)
451 (addrsel_reg_IP2022 alu)
452 (addr_array_IP2022 alu)
453 (call_stack_IP2022 alu)
456 (data_reg_IP2022 alu)
459 (speed_reg_IP2022 alu)
464 (skip_mode_IP2022 alu).
466 (* setter specifico IP2022 di H *)
467 ndefinition set_h_flag_IP2022 ≝
470 (acc_low_reg_IP2022 alu)
471 (mulh_reg_IP2022 alu)
472 (addrsel_reg_IP2022 alu)
473 (addr_array_IP2022 alu)
474 (call_stack_IP2022 alu)
477 (data_reg_IP2022 alu)
480 (speed_reg_IP2022 alu)
481 (page_reg_IP2022 alu)
485 (skip_mode_IP2022 alu).
487 (* setter specifico IP2022 di Z *)
488 ndefinition set_z_flag_IP2022 ≝
491 (acc_low_reg_IP2022 alu)
492 (mulh_reg_IP2022 alu)
493 (addrsel_reg_IP2022 alu)
494 (addr_array_IP2022 alu)
495 (call_stack_IP2022 alu)
498 (data_reg_IP2022 alu)
501 (speed_reg_IP2022 alu)
502 (page_reg_IP2022 alu)
506 (skip_mode_IP2022 alu).
508 (* setter specifico IP2022 di C *)
509 ndefinition set_c_flag_IP2022 ≝
512 (acc_low_reg_IP2022 alu)
513 (mulh_reg_IP2022 alu)
514 (addrsel_reg_IP2022 alu)
515 (addr_array_IP2022 alu)
516 (call_stack_IP2022 alu)
519 (data_reg_IP2022 alu)
522 (speed_reg_IP2022 alu)
523 (page_reg_IP2022 alu)
527 (skip_mode_IP2022 alu).
529 (* setter specifico IP2022 di SKIP *)
530 ndefinition set_skip_mode_IP2022 ≝
531 λalu.λskipmode':bool.
533 (acc_low_reg_IP2022 alu)
534 (mulh_reg_IP2022 alu)
535 (addrsel_reg_IP2022 alu)
536 (addr_array_IP2022 alu)
537 (call_stack_IP2022 alu)
540 (data_reg_IP2022 alu)
543 (speed_reg_IP2022 alu)
544 (page_reg_IP2022 alu)
550 (* ***************** *)
551 (* CONFRONTO FRA ALU *)
552 (* ***************** *)
554 (* confronto registro per registro dell'IP2022 *)
555 ndefinition eq_IP2022_alu ≝
556 λalu1,alu2:alu_IP2022.
557 (eqc ? (acc_low_reg_IP2022 alu1) (acc_low_reg_IP2022 alu2)) ⊗
558 (eqc ? (mulh_reg_IP2022 alu1) (mulh_reg_IP2022 alu2)) ⊗
559 (eqc ? (addrsel_reg_IP2022 alu1) (addrsel_reg_IP2022 alu2)) ⊗
560 (eqc ? (addr_array_IP2022 alu1) (addr_array_IP2022 alu2)) ⊗
561 (eqc ? (call_stack_IP2022 alu1) (call_stack_IP2022 alu2)) ⊗
562 (eqc ? (ip_reg_IP2022 alu1) (ip_reg_IP2022 alu2)) ⊗
563 (eqc ? (dp_reg_IP2022 alu1) (dp_reg_IP2022 alu2)) ⊗
564 (eqc ? (data_reg_IP2022 alu1) (data_reg_IP2022 alu2)) ⊗
565 (eqc ? (sp_reg_IP2022 alu1) (sp_reg_IP2022 alu2)) ⊗
566 (eqc ? (pc_reg_IP2022 alu1) (pc_reg_IP2022 alu2)) ⊗
567 (eqc ? (speed_reg_IP2022 alu1) (speed_reg_IP2022 alu2)) ⊗
568 (eqc ? (page_reg_IP2022 alu1) (page_reg_IP2022 alu2)) ⊗
569 (eqc ? (h_flag_IP2022 alu1) (h_flag_IP2022 alu2)) ⊗
570 (eqc ? (z_flag_IP2022 alu1) (z_flag_IP2022 alu2)) ⊗
571 (eqc ? (c_flag_IP2022 alu1) (c_flag_IP2022 alu2)) ⊗
572 (eqc ? (skip_mode_IP2022 alu1) (skip_mode_IP2022 alu2)).
574 ndefinition forall_IP2022_alu ≝ λP:alu_IP2022 → bool.
575 forallc ? (λr1.forallc ? (λr2.
576 forallc ? (λr3.forallc ? (λr4.
577 forallc ? (λr5.forallc ? (λr6.
578 forallc ? (λr7.forallc ? (λr8.
579 forallc ? (λr9.forallc ? (λr10.
580 forallc ? (λr11.forallc ? (λr12.
581 forallc ? (λr13.forallc ? (λr14.
582 forallc ? (λr15.forallc ? (λr16.
583 P (mk_alu_IP2022 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14 r15 r16))))))))))))))))).