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 ≝
80 mk_Array8T ? (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
81 (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
82 (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
83 (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉).
85 ndefinition get_addrarray ≝
86 λaddrsel:byte8.λaa:aux_addrarray_type.
87 getn_array8T (oct_of_exL (cnL ? addrsel)) ? aa.
89 ndefinition set_addrarray ≝
90 λaddrsel:byte8.λaa:aux_addrarray_type.λv.
91 setn_array8T (oct_of_exL (cnL ? addrsel)) ? aa v.
93 nlemma addrarray_is_comparable : comparable.
94 @ (aux_addrarray_type)
95 ##[ napply (zeroc (ar8_is_comparable word24_is_comparable))
96 ##| napply (forallc (ar8_is_comparable word24_is_comparable))
97 ##| napply (eqc (ar8_is_comparable word24_is_comparable))
98 ##| napply (eqc_to_eq (ar8_is_comparable word24_is_comparable))
99 ##| napply (eq_to_eqc (ar8_is_comparable word24_is_comparable))
100 ##| napply (neqc_to_neq (ar8_is_comparable word24_is_comparable))
101 ##| napply (neq_to_neqc (ar8_is_comparable word24_is_comparable))
102 ##| napply (decidable_c (ar8_is_comparable word24_is_comparable))
103 ##| napply (symmetric_eqc (ar8_is_comparable word24_is_comparable))
107 unification hint 0 ≔ ⊢ carr addrarray_is_comparable ≡ aux_addrarray_type.
109 (* *********************************** *)
110 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
111 (* *********************************** *)
113 (* ALU dell'IP2022 *)
114 nrecord alu_IP2022: Type ≝
116 (* W: accumulatore *)
117 acc_low_reg_IP2022 : byte8;
118 (* MULH: parte alta moltiplicazione *)
119 mulh_reg_IP2022 : byte8;
121 (* ADDRSEL: selettore di indirizzo *)
122 addrsel_reg_IP2022 : byte8;
123 (* ADDR [ADDRX|ADDRH|ADDRL] : array indirizzi indicizzati da ADDRSEL *)
124 addr_array_IP2022 : aux_addrarray_type;
126 (* CALL [CALLH|CALLL] : stack indirizzi di ritorno *)
127 call_stack_IP2022 : aux_callstack_type;
129 (* IP [IPH|IPL] : indirect pointer *)
130 ip_reg_IP2022 : word16;
131 (* DP [DPH|DPL] : data pointer *)
132 dp_reg_IP2022 : word16;
133 (* DATA [DATAH|DATAL] : data value *)
134 data_reg_IP2022 : word16;
135 (* SP [SPH|SPL] : stack pointer *)
136 sp_reg_IP2022 : word16;
137 (* PC [PCH|PCL] : program counter *)
138 pc_reg_IP2022 : word16;
140 (* SPEED[xxxxSSSS] : divisore del clock *)
141 speed_reg_IP2022 : exadecim;
142 (* PAGE [PPPxxxxx] : selettore pagina *)
143 page_reg_IP2022 : oct;
145 (* H: flag semi-carry (somma nibble basso) *)
146 h_flag_IP2022 : bool;
148 z_flag_IP2022 : bool;
150 c_flag_IP2022 : bool;
152 (* skip mode : effettua fetch-decode, no execute *)
153 skip_mode_IP2022 : bool
156 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)}"
157 non associative with precedence 80 for
158 @{ 'mk_alu_IP2022 $w $mulh $addrsel $addr $call $ip $dp $data $sp $pc $speed $page $hfl $zfl $cfl $skipmode }.
159 interpretation "mk_alu_IP2022" 'mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode =
160 (mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode).
166 (* setter specifico IP2022 di A *)
167 ndefinition set_acc_8_low_reg_IP2022 ≝
171 (mulh_reg_IP2022 alu)
172 (addrsel_reg_IP2022 alu)
173 (addr_array_IP2022 alu)
174 (call_stack_IP2022 alu)
177 (data_reg_IP2022 alu)
180 (speed_reg_IP2022 alu)
181 (page_reg_IP2022 alu)
185 (skip_mode_IP2022 alu).
187 (* setter specifico IP2022 di MULH *)
188 ndefinition set_mulh_reg_IP2022 ≝
191 (acc_low_reg_IP2022 alu)
193 (addrsel_reg_IP2022 alu)
194 (addr_array_IP2022 alu)
195 (call_stack_IP2022 alu)
198 (data_reg_IP2022 alu)
201 (speed_reg_IP2022 alu)
202 (page_reg_IP2022 alu)
206 (skip_mode_IP2022 alu).
208 (* setter specifico IP2022 di ADDRSEL *)
209 ndefinition set_addrsel_reg_IP2022 ≝
210 λalu.λaddrsel':byte8.
212 (acc_low_reg_IP2022 alu)
213 (mulh_reg_IP2022 alu)
215 (addr_array_IP2022 alu)
216 (call_stack_IP2022 alu)
219 (data_reg_IP2022 alu)
222 (speed_reg_IP2022 alu)
223 (page_reg_IP2022 alu)
227 (skip_mode_IP2022 alu).
229 (* setter specifico IP2022 di ADDR *)
230 ndefinition set_addr_reg_IP2022 ≝
233 (acc_low_reg_IP2022 alu)
234 (mulh_reg_IP2022 alu)
235 (addrsel_reg_IP2022 alu)
236 (set_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu) addr')
237 (call_stack_IP2022 alu)
240 (data_reg_IP2022 alu)
243 (speed_reg_IP2022 alu)
244 (page_reg_IP2022 alu)
248 (skip_mode_IP2022 alu).
250 ndefinition get_addr_reg_IP2022 ≝
251 λalu.get_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu).
253 (* setter specifico IP2022 di CALL *)
254 ndefinition set_call_reg_IP2022 ≝
257 (acc_low_reg_IP2022 alu)
258 (mulh_reg_IP2022 alu)
259 (addrsel_reg_IP2022 alu)
260 (addr_array_IP2022 alu)
261 (setn_array16T x0 ? (call_stack_IP2022 alu) call')
264 (data_reg_IP2022 alu)
267 (speed_reg_IP2022 alu)
268 (page_reg_IP2022 alu)
272 (skip_mode_IP2022 alu).
274 ndefinition get_call_reg_IP2022 ≝
275 λalu.getn_array16T x0 ? (call_stack_IP2022 alu).
277 ndefinition set_call_stack_IP2022 ≝
278 λalu.λcall':aux_callstack_type.
280 (acc_low_reg_IP2022 alu)
281 (mulh_reg_IP2022 alu)
282 (addrsel_reg_IP2022 alu)
283 (addr_array_IP2022 alu)
287 (data_reg_IP2022 alu)
290 (speed_reg_IP2022 alu)
291 (page_reg_IP2022 alu)
295 (skip_mode_IP2022 alu).
297 ndefinition push_call_reg_IP2022 ≝
300 (acc_low_reg_IP2022 alu)
301 (mulh_reg_IP2022 alu)
302 (addrsel_reg_IP2022 alu)
303 (addr_array_IP2022 alu)
304 (push_callstack (call_stack_IP2022 alu) call')
307 (data_reg_IP2022 alu)
310 (speed_reg_IP2022 alu)
311 (page_reg_IP2022 alu)
315 (skip_mode_IP2022 alu).
317 ndefinition pop_call_reg_IP2022 ≝
318 λalu.match pop_callstack (call_stack_IP2022 alu) with
319 [ pair val call' ⇒ pair … val (set_call_stack_IP2022 alu call') ].
321 (* setter specifico IP2022 di IP *)
322 ndefinition set_ip_reg_IP2022 ≝
325 (acc_low_reg_IP2022 alu)
326 (mulh_reg_IP2022 alu)
327 (addrsel_reg_IP2022 alu)
328 (addr_array_IP2022 alu)
329 (call_stack_IP2022 alu)
332 (data_reg_IP2022 alu)
335 (speed_reg_IP2022 alu)
336 (page_reg_IP2022 alu)
340 (skip_mode_IP2022 alu).
342 (* setter specifico IP2022 di DP *)
343 ndefinition set_dp_reg_IP2022 ≝
346 (acc_low_reg_IP2022 alu)
347 (mulh_reg_IP2022 alu)
348 (addrsel_reg_IP2022 alu)
349 (addr_array_IP2022 alu)
350 (call_stack_IP2022 alu)
353 (data_reg_IP2022 alu)
356 (speed_reg_IP2022 alu)
357 (page_reg_IP2022 alu)
361 (skip_mode_IP2022 alu).
363 (* setter specifico IP2022 di DATA *)
364 ndefinition set_data_reg_IP2022 ≝
367 (acc_low_reg_IP2022 alu)
368 (mulh_reg_IP2022 alu)
369 (addrsel_reg_IP2022 alu)
370 (addr_array_IP2022 alu)
371 (call_stack_IP2022 alu)
377 (speed_reg_IP2022 alu)
378 (page_reg_IP2022 alu)
382 (skip_mode_IP2022 alu).
384 (* setter specifico IP2022 di SP *)
385 ndefinition set_sp_reg_IP2022 ≝
388 (acc_low_reg_IP2022 alu)
389 (mulh_reg_IP2022 alu)
390 (addrsel_reg_IP2022 alu)
391 (addr_array_IP2022 alu)
392 (call_stack_IP2022 alu)
395 (data_reg_IP2022 alu)
398 (speed_reg_IP2022 alu)
399 (page_reg_IP2022 alu)
403 (skip_mode_IP2022 alu).
405 (* setter specifico IP2022 di PC *)
406 ndefinition set_pc_reg_IP2022 ≝
409 (acc_low_reg_IP2022 alu)
410 (mulh_reg_IP2022 alu)
411 (addrsel_reg_IP2022 alu)
412 (addr_array_IP2022 alu)
413 (call_stack_IP2022 alu)
416 (data_reg_IP2022 alu)
419 (speed_reg_IP2022 alu)
420 (page_reg_IP2022 alu)
424 (skip_mode_IP2022 alu).
426 (* setter specifico IP2022 di SPEED *)
427 ndefinition set_speed_reg_IP2022 ≝
428 λalu.λspeed':exadecim.
430 (acc_low_reg_IP2022 alu)
431 (mulh_reg_IP2022 alu)
432 (addrsel_reg_IP2022 alu)
433 (addr_array_IP2022 alu)
434 (call_stack_IP2022 alu)
437 (data_reg_IP2022 alu)
441 (page_reg_IP2022 alu)
445 (skip_mode_IP2022 alu).
447 (* setter specifico IP2022 di PAGE *)
448 ndefinition set_page_reg_IP2022 ≝
451 (acc_low_reg_IP2022 alu)
452 (mulh_reg_IP2022 alu)
453 (addrsel_reg_IP2022 alu)
454 (addr_array_IP2022 alu)
455 (call_stack_IP2022 alu)
458 (data_reg_IP2022 alu)
461 (speed_reg_IP2022 alu)
466 (skip_mode_IP2022 alu).
468 (* setter specifico IP2022 di H *)
469 ndefinition set_h_flag_IP2022 ≝
472 (acc_low_reg_IP2022 alu)
473 (mulh_reg_IP2022 alu)
474 (addrsel_reg_IP2022 alu)
475 (addr_array_IP2022 alu)
476 (call_stack_IP2022 alu)
479 (data_reg_IP2022 alu)
482 (speed_reg_IP2022 alu)
483 (page_reg_IP2022 alu)
487 (skip_mode_IP2022 alu).
489 (* setter specifico IP2022 di Z *)
490 ndefinition set_z_flag_IP2022 ≝
493 (acc_low_reg_IP2022 alu)
494 (mulh_reg_IP2022 alu)
495 (addrsel_reg_IP2022 alu)
496 (addr_array_IP2022 alu)
497 (call_stack_IP2022 alu)
500 (data_reg_IP2022 alu)
503 (speed_reg_IP2022 alu)
504 (page_reg_IP2022 alu)
508 (skip_mode_IP2022 alu).
510 (* setter specifico IP2022 di C *)
511 ndefinition set_c_flag_IP2022 ≝
514 (acc_low_reg_IP2022 alu)
515 (mulh_reg_IP2022 alu)
516 (addrsel_reg_IP2022 alu)
517 (addr_array_IP2022 alu)
518 (call_stack_IP2022 alu)
521 (data_reg_IP2022 alu)
524 (speed_reg_IP2022 alu)
525 (page_reg_IP2022 alu)
529 (skip_mode_IP2022 alu).
531 (* setter specifico IP2022 di SKIP *)
532 ndefinition set_skip_mode_IP2022 ≝
533 λalu.λskipmode':bool.
535 (acc_low_reg_IP2022 alu)
536 (mulh_reg_IP2022 alu)
537 (addrsel_reg_IP2022 alu)
538 (addr_array_IP2022 alu)
539 (call_stack_IP2022 alu)
542 (data_reg_IP2022 alu)
545 (speed_reg_IP2022 alu)
546 (page_reg_IP2022 alu)
552 (* ***************** *)
553 (* CONFRONTO FRA ALU *)
554 (* ***************** *)
556 (* confronto registro per registro dell'IP2022 *)
557 ndefinition eq_IP2022_alu ≝
558 λalu1,alu2:alu_IP2022.
559 (eqc ? (acc_low_reg_IP2022 alu1) (acc_low_reg_IP2022 alu2)) ⊗
560 (eqc ? (mulh_reg_IP2022 alu1) (mulh_reg_IP2022 alu2)) ⊗
561 (eqc ? (addrsel_reg_IP2022 alu1) (addrsel_reg_IP2022 alu2)) ⊗
562 (eqc ? (addr_array_IP2022 alu1) (addr_array_IP2022 alu2)) ⊗
563 (eqc ? (call_stack_IP2022 alu1) (call_stack_IP2022 alu2)) ⊗
564 (eqc ? (ip_reg_IP2022 alu1) (ip_reg_IP2022 alu2)) ⊗
565 (eqc ? (dp_reg_IP2022 alu1) (dp_reg_IP2022 alu2)) ⊗
566 (eqc ? (data_reg_IP2022 alu1) (data_reg_IP2022 alu2)) ⊗
567 (eqc ? (sp_reg_IP2022 alu1) (sp_reg_IP2022 alu2)) ⊗
568 (eqc ? (pc_reg_IP2022 alu1) (pc_reg_IP2022 alu2)) ⊗
569 (eqc ? (speed_reg_IP2022 alu1) (speed_reg_IP2022 alu2)) ⊗
570 (eqc ? (page_reg_IP2022 alu1) (page_reg_IP2022 alu2)) ⊗
571 (eqc ? (h_flag_IP2022 alu1) (h_flag_IP2022 alu2)) ⊗
572 (eqc ? (z_flag_IP2022 alu1) (z_flag_IP2022 alu2)) ⊗
573 (eqc ? (c_flag_IP2022 alu1) (c_flag_IP2022 alu2)) ⊗
574 (eqc ? (skip_mode_IP2022 alu1) (skip_mode_IP2022 alu2)).
576 ndefinition forall_IP2022_alu ≝ λP:alu_IP2022 → bool.
577 forallc ? (λr1.forallc ? (λr2.
578 forallc ? (λr3.forallc ? (λr4.
579 forallc ? (λr5.forallc ? (λr6.
580 forallc ? (λr7.forallc ? (λr8.
581 forallc ? (λr9.forallc ? (λr10.
582 forallc ? (λr11.forallc ? (λr12.
583 forallc ? (λr13.forallc ? (λr14.
584 forallc ? (λr15.forallc ? (λr16.
585 P (mk_alu_IP2022 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14 r15 r16))))))))))))))))).