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: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/memory_abs.ma".
24 include "freescale/opcode_base.ma".
25 include "freescale/prod.ma".
27 (* *********************************** *)
28 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
29 (* *********************************** *)
32 nrecord alu_HC05: Type ≝
34 (* A: registo accumulatore *)
35 acc_low_reg_HC05 : byte8;
36 (* X: registro indice *)
37 indX_low_reg_HC05 : byte8;
38 (* SP: registo stack pointer *)
40 (* modificatori di SP: per esempio e' definito come 0000000011xxxxxxb *)
41 (* la logica della sua costruzione e' quindi (SP∧mask)∨fix *)
42 (* totalmente racchiusa nella ALU, bastera' fare get(set(SP)) *)
43 sp_mask_HC05 : word16;
45 (* PC: registro program counter *)
47 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
48 (* la logica della sua costruzione e' quindi (PC∧mask) *)
49 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
50 pc_mask_HC05 : word16;
52 (* H: flag semi-carry (somma nibble basso) *)
54 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
56 (* N: flag segno/negativita' *)
63 (* IRQ: flag che simula il pin esterno IRQ *)
67 notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg' ≝ sp ; break 'Sp_Mask' ≝ spm ; break 'Sp_Fix' ≝ spf ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
68 non associative with precedence 80 for
69 @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
70 interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
71 (mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
73 (* ALU dell'HC08/HCS08 *)
74 nrecord alu_HC08: Type ≝
76 (* A: registo accumulatore *)
77 acc_low_reg_HC08 : byte8;
78 (* X: registro indice parte bassa *)
79 indX_low_reg_HC08 : byte8;
80 (* H: registro indice parte alta *)
81 indX_high_reg_HC08 : byte8;
82 (* SP: registo stack pointer *)
84 (* PC: registro program counter *)
87 (* V: flag overflow *)
89 (* H: flag semi-carry (somma nibble basso) *)
91 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
93 (* N: flag segno/negativita' *)
100 (* IRQ: flag che simula il pin esterno IRQ *)
104 notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg' ≝ indxhigh ; break 'Sp_Reg' ≝ sp ; break 'Pc_Reg' ≝ pc ; break 'V_Flag' ≝ vfl ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
105 non associative with precedence 80 for
106 @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
107 interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
108 (mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
111 nrecord alu_RS08: Type ≝
113 (* A: registo accumulatore *)
114 acc_low_reg_RS08 : byte8;
115 (* PC: registro program counter *)
116 pc_reg_RS08 : word16;
117 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
118 (* la logica della sua costruzione e' quindi (PC∧mask) *)
119 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
120 pc_mask_RS08 : word16;
121 (* SPC: registro shadow program counter *)
122 (* NB: il suo modificatore e' lo stesso di PC *)
123 spc_reg_RS08 : word16;
125 (* X: registro indice parte bassa *)
126 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
127 (* la lettura/scrittura avviene tramite la locazione [0x000F] *)
128 (* la funzione memory_filter_read/write si occupera' di intercettare *)
129 (* e deviare sul registro le letture/scritture (modulo load_write) *)
131 (* PS: registro selezione di pagina *)
132 (* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *)
133 (* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *)
134 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
135 (* la lettura/scrittura avviene tramite la locazione [0x001F] *)
136 (* la funzione memory_filter_read/write si occupera' di intercettare *)
137 (* e deviare sul registro le letture/scritture (modulo load_write) *)
146 notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'Spc_Reg' ≝ spc ; break 'X_Map' ≝ xm ; break 'Ps_Map' ≝ psm ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl)}"
147 non associative with precedence 80 for
148 @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
149 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
150 (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
152 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
153 nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
156 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ];
158 (* descritore della memoria *)
159 mem_desc : aux_mem_type t;
160 (* descrittore del tipo di memoria installata *)
161 chk_desc : aux_chk_type t;
162 (* descrittore del click = stato di avanzamento dell'esecuzione+cur_pc conseguente a fetch *)
163 (* 1) None = istruzione eseguita, attesa del fetch *)
164 (* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito, countup a esecuzione *)
165 clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16)
168 ndefinition any_status_ind :
169 Πmcu.Πt.ΠP:any_status mcu t → Prop.
170 (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
171 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
172 λmcu.λt.λP:any_status mcu t → Prop.
173 λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
174 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
175 match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
177 ndefinition any_status_rec :
178 Πmcu.Πt.ΠP:any_status mcu t → Set.
179 (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
180 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
181 λmcu.λt.λP:any_status mcu t → Set.
182 λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
183 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
184 match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
186 ndefinition any_status_rect :
187 Πmcu.Πt.ΠP:any_status mcu t → Type.
188 (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
189 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
190 λmcu.λt.λP:any_status mcu t → Type.
191 λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
192 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
193 match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
195 ndefinition alu ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status (x:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]) _ _ _ ⇒ x ].
196 ndefinition mem_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ x _ _ ⇒ x ].
197 ndefinition chk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ x _ ⇒ x ].
198 ndefinition clk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ _ x ⇒ x ].
200 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
201 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
202 for @{ 'mk_any_status $alu $mem $chk $clk }.
203 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
204 (mk_any_status alu mem chk clk).
206 (* **************** *)
207 (* GETTER SPECIFICI *)
208 (* **************** *)
210 (* funzione ausiliaria per il tipaggio dei getter *)
211 ndefinition aux_get_typing ≝ λx:Type.λm:mcu_type.match m with
212 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] → x.
216 (* getter di A, esiste sempre *)
217 ndefinition get_acc_8_low_reg ≝
218 λm:mcu_type.λt:memory_impl.λs:any_status m t.
220 return aux_get_typing byte8 with
221 [ HC05 ⇒ acc_low_reg_HC05
222 | HC08 ⇒ acc_low_reg_HC08
223 | HCS08 ⇒ acc_low_reg_HC08
224 | RS08 ⇒ acc_low_reg_RS08 ]
227 (* getter di X, non esiste sempre *)
228 ndefinition get_indX_8_low_reg ≝
229 λm:mcu_type.λt:memory_impl.λs:any_status m t.
231 return aux_get_typing (option byte8) with
232 [ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
233 | HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
234 | HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
235 | RS08 ⇒ λalu.None ? ]
238 (* getter di H, non esiste sempre *)
239 ndefinition get_indX_8_high_reg ≝
240 λm:mcu_type.λt:memory_impl.λs:any_status m t.
242 return aux_get_typing (option byte8) with
244 | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
245 | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
246 | RS08 ⇒ λalu.None ? ]
249 (* getter di H:X, non esiste sempre *)
250 ndefinition get_indX_16_reg ≝
251 λm:mcu_type.λt:memory_impl.λs:any_status m t.
253 return aux_get_typing (option word16) with
255 | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
256 | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
257 | RS08 ⇒ λalu.None ? ]
260 (* getter di SP, non esiste sempre *)
261 ndefinition get_sp_reg ≝
262 λm:mcu_type.λt:memory_impl.λs:any_status m t.
264 return aux_get_typing (option word16) with
265 [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
266 | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
267 | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
268 | RS08 ⇒ λalu.None ? ]
271 (* getter di PC, esiste sempre *)
272 ndefinition get_pc_reg ≝
273 λm:mcu_type.λt:memory_impl.λs:any_status m t.
275 return aux_get_typing word16 with
278 | HCS08 ⇒ pc_reg_HC08
279 | RS08 ⇒ pc_reg_RS08 ]
282 (* getter di SPC, non esiste sempre *)
283 ndefinition get_spc_reg ≝
284 λm:mcu_type.λt:memory_impl.λs:any_status m t.
286 return aux_get_typing (option word16) with
289 | HCS08 ⇒ λalu.None ?
290 | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu) ]
293 (* REGISTRI MEMORY MAPPED *)
295 (* getter di memory mapped X, non esiste sempre *)
296 ndefinition get_x_map ≝
297 λm:mcu_type.λt:memory_impl.λs:any_status m t.
299 return aux_get_typing (option byte8) with
302 | HCS08 ⇒ λalu.None ?
303 | RS08 ⇒ λalu.Some ? (x_map_RS08 alu) ]
306 (* getter di memory mapped PS, non esiste sempre *)
307 ndefinition get_ps_map ≝
308 λm:mcu_type.λt:memory_impl.λs:any_status m t.
310 return aux_get_typing (option byte8) with
313 | HCS08 ⇒ λalu.None ?
314 | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu) ]
319 (* getter di V, non esiste sempre *)
320 ndefinition get_v_flag ≝
321 λm:mcu_type.λt:memory_impl.λs:any_status m t.
323 return aux_get_typing (option bool) with
325 | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
326 | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
327 | RS08 ⇒ λalu.None ? ]
330 (* getter di H, non esiste sempre *)
331 ndefinition get_h_flag ≝
332 λm:mcu_type.λt:memory_impl.λs:any_status m t.
334 return aux_get_typing (option bool) with
335 [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
336 | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
337 | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
338 | RS08 ⇒ λalu.None ? ]
341 (* getter di I, non esiste sempre *)
342 ndefinition get_i_flag ≝
343 λm:mcu_type.λt:memory_impl.λs:any_status m t.
345 return aux_get_typing (option bool) with
346 [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
347 | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
348 | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
349 | RS08 ⇒ λalu.None ? ]
352 (* getter di N, non esiste sempre *)
353 ndefinition get_n_flag ≝
354 λm:mcu_type.λt:memory_impl.λs:any_status m t.
356 return aux_get_typing (option bool) with
357 [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
358 | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
359 | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
360 | RS08 ⇒ λalu.None ? ]
363 (* getter di Z, esiste sempre *)
364 ndefinition get_z_flag ≝
365 λm:mcu_type.λt:memory_impl.λs:any_status m t.
367 return aux_get_typing bool with
370 | HCS08 ⇒ z_flag_HC08
371 | RS08 ⇒ z_flag_RS08 ]
374 (* getter di C, esiste sempre *)
375 ndefinition get_c_flag ≝
376 λm:mcu_type.λt:memory_impl.λs:any_status m t.
378 return aux_get_typing bool with
381 | HCS08 ⇒ c_flag_HC08
382 | RS08 ⇒ c_flag_RS08 ]
385 (* getter di IRQ, non esiste sempre *)
386 ndefinition get_irq_flag ≝
387 λm:mcu_type.λt:memory_impl.λs:any_status m t.
389 return aux_get_typing (option bool) with
390 [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
391 | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
392 | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
393 | RS08 ⇒ λalu.None ? ]
396 (* DESCRITTORI ESTERNI ALLA ALU *)
398 (* getter della ALU, esiste sempre *)
399 ndefinition get_alu ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.alu m t s.
401 (* getter della memoria, esiste sempre *)
402 ndefinition get_mem_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.mem_desc m t s.
404 (* getter del descrittore, esiste sempre *)
405 ndefinition get_chk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.chk_desc m t s.
407 (* getter del clik, esiste sempre *)
408 ndefinition get_clk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.clk_desc m t s.
410 (* ***************************** *)
411 (* SETTER SPECIFICI FORTI/DEBOLI *)
412 (* ***************************** *)
414 (* funzione ausiliaria per il tipaggio dei setter forti *)
415 ndefinition aux_set_typing ≝ λx:Type.λm:mcu_type.
416 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
418 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
420 (* funzione ausiliaria per il tipaggio dei setter deboli *)
421 ndefinition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option
422 (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
424 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]).
426 (* DESCRITTORI ESTERNI ALLA ALU *)
428 (* setter forte della ALU *)
429 ndefinition set_alu ≝
430 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
431 mk_any_status m t alu' (get_mem_desc m t s) (get_chk_desc m t s) (get_clk_desc m t s).
433 (* setter forte della memoria *)
434 ndefinition set_mem_desc ≝
435 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
436 mk_any_status m t (get_alu m t s) mem' (get_chk_desc m t s) (get_clk_desc m t s).
438 (* setter forte del descrittore *)
439 ndefinition set_chk_desc ≝
440 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
441 mk_any_status m t (get_alu m t s) (get_mem_desc m t s) chk' (get_clk_desc m t s).
443 (* setter forte del clik *)
444 ndefinition set_clk_desc ≝
445 λm:mcu_type.λt:memory_impl.λs:any_status m t.
446 λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
447 mk_any_status m t (get_alu m t s) (get_mem_desc m t s) (get_chk_desc m t s) clk'.
451 (* setter specifico HC05 di A *)
452 ndefinition set_acc_8_low_reg_HC05 ≝
456 (indX_low_reg_HC05 alu)
469 (* setter specifico HC08/HCS08 di A *)
470 ndefinition set_acc_8_low_reg_HC08 ≝
474 (indX_low_reg_HC08 alu)
475 (indX_high_reg_HC08 alu)
486 (* setter specifico RS08 di A *)
487 ndefinition set_acc_8_low_reg_RS08 ≝
499 (* setter forte di A *)
500 ndefinition set_acc_8_low_reg ≝
501 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
503 (match m return aux_set_typing byte8 with
504 [ HC05 ⇒ set_acc_8_low_reg_HC05
505 | HC08 ⇒ set_acc_8_low_reg_HC08
506 | HCS08 ⇒ set_acc_8_low_reg_HC08
507 | RS08 ⇒ set_acc_8_low_reg_RS08
508 ] (alu m t s) acclow').
512 (* setter specifico HC05 di X *)
513 ndefinition set_indX_8_low_reg_HC05 ≝
514 λalu.λindxlow':byte8.
516 (acc_low_reg_HC05 alu)
530 (* setter specifico HC08/HCS08 di X *)
531 ndefinition set_indX_8_low_reg_HC08 ≝
532 λalu.λindxlow':byte8.
534 (acc_low_reg_HC08 alu)
536 (indX_high_reg_HC08 alu)
547 (* setter forte di X *)
548 ndefinition set_indX_8_low_reg ≝
549 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
550 opt_map ?? (match m return aux_set_typing_opt byte8 with
551 [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
552 | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
553 | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
555 (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
557 (* setter debole di X *)
558 ndefinition setweak_indX_8_low_reg ≝
559 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
560 match set_indX_8_low_reg m t s indxlow' with
561 [ None ⇒ s | Some s' ⇒ s' ].
565 (* setter specifico HC08/HCS08 di H *)
566 ndefinition set_indX_8_high_reg_HC08 ≝
567 λalu.λindxhigh':byte8.
569 (acc_low_reg_HC08 alu)
570 (indX_low_reg_HC08 alu)
582 (* setter forte di H *)
583 ndefinition set_indX_8_high_reg ≝
584 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
585 opt_map ?? (match m return aux_set_typing_opt byte8 with
587 | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
588 | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
590 (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
592 (* setter debole di H *)
593 ndefinition setweak_indX_8_high_reg ≝
594 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
595 match set_indX_8_high_reg m t s indxhigh' with
596 [ None ⇒ s | Some s' ⇒ s' ].
600 (* setter specifico HC08/HCS08 di H:X *)
601 ndefinition set_indX_16_reg_HC08 ≝
604 (acc_low_reg_HC08 alu)
617 (* setter forte di H:X *)
618 ndefinition set_indX_16_reg ≝
619 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
620 opt_map ?? (match m return aux_set_typing_opt word16 with
622 | HC08 ⇒ Some ? set_indX_16_reg_HC08
623 | HCS08 ⇒ Some ? set_indX_16_reg_HC08
625 (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
627 (* setter debole di H:X *)
628 ndefinition setweak_indX_16_reg ≝
629 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
630 match set_indX_16_reg m t s indx16 with
631 [ None ⇒ s | Some s' ⇒ s' ].
635 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
636 ndefinition set_sp_reg_HC05 ≝
639 (acc_low_reg_HC05 alu)
640 (indX_low_reg_HC05 alu)
641 (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
653 (* setter specifico HC08/HCS08 di SP *)
654 ndefinition set_sp_reg_HC08 ≝
657 (acc_low_reg_HC08 alu)
658 (indX_low_reg_HC08 alu)
659 (indX_high_reg_HC08 alu)
670 (* setter forte di SP *)
671 ndefinition set_sp_reg ≝
672 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
673 opt_map ?? (match m return aux_set_typing_opt word16 with
674 [ HC05 ⇒ Some ? set_sp_reg_HC05
675 | HC08 ⇒ Some ? set_sp_reg_HC08
676 | HCS08 ⇒ Some ? set_sp_reg_HC08
678 (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
680 (* setter debole di SP *)
681 ndefinition setweak_sp_reg ≝
682 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
683 match set_sp_reg m t s sp' with
684 [ None ⇒ s | Some s' ⇒ s' ].
688 (* setter specifico HC05 di PC, effettua PC∧mask *)
689 ndefinition set_pc_reg_HC05 ≝
692 (acc_low_reg_HC05 alu)
693 (indX_low_reg_HC05 alu)
697 (and_w16 pc' (pc_mask_HC05 alu))
706 (* setter specifico HC08/HCS08 di PC *)
707 ndefinition set_pc_reg_HC08 ≝
710 (acc_low_reg_HC08 alu)
711 (indX_low_reg_HC08 alu)
712 (indX_high_reg_HC08 alu)
723 (* setter specifico RS08 di PC, effettua PC∧mask *)
724 ndefinition set_pc_reg_RS08 ≝
727 (acc_low_reg_RS08 alu)
728 (and_w16 pc' (pc_mask_RS08 alu))
736 (* setter forte di PC *)
737 ndefinition set_pc_reg ≝
738 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
740 (match m return aux_set_typing word16 with
741 [ HC05 ⇒ set_pc_reg_HC05
742 | HC08 ⇒ set_pc_reg_HC08
743 | HCS08 ⇒ set_pc_reg_HC08
744 | RS08 ⇒ set_pc_reg_RS08
749 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
750 ndefinition set_spc_reg_RS08 ≝
753 (acc_low_reg_RS08 alu)
756 (and_w16 spc' (pc_mask_RS08 alu))
762 (* setter forte di SPC *)
763 ndefinition set_spc_reg ≝
764 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
765 opt_map ?? (match m return aux_set_typing_opt word16 with
769 | RS08 ⇒ Some ? set_spc_reg_RS08 ])
770 (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
772 (* setter debole di SPC *)
773 ndefinition setweak_spc_reg ≝
774 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
775 match set_spc_reg m t s spc' with
776 [ None ⇒ s | Some s' ⇒ s' ].
778 (* REGISTRO MEMORY MAPPED X *)
780 (* setter specifico RS08 di memory mapped X *)
781 ndefinition set_x_map_RS08 ≝
784 (acc_low_reg_RS08 alu)
793 (* setter forte di memory mapped X *)
794 ndefinition set_x_map ≝
795 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
796 opt_map ?? (match m return aux_set_typing_opt byte8 with
800 | RS08 ⇒ Some ? set_x_map_RS08 ])
801 (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
803 (* setter debole di memory mapped X *)
804 ndefinition setweak_x_map ≝
805 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
806 match set_x_map m t s xm' with
807 [ None ⇒ s | Some s' ⇒ s' ].
809 (* REGISTRO MEMORY MAPPED PS *)
811 (* setter specifico RS08 di memory mapped PS *)
812 ndefinition set_ps_map_RS08 ≝
815 (acc_low_reg_RS08 alu)
824 (* setter forte di memory mapped PS *)
825 ndefinition set_ps_map ≝
826 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
827 opt_map ?? (match m return aux_set_typing_opt byte8 with
831 | RS08 ⇒ Some ? set_ps_map_RS08 ])
832 (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
834 (* setter debole di memory mapped PS *)
835 ndefinition setweak_ps_map ≝
836 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
837 match set_ps_map m t s psm' with
838 [ None ⇒ s | Some s' ⇒ s' ].
842 (* setter specifico HC08/HCS08 di V *)
843 ndefinition set_v_flag_HC08 ≝
846 (acc_low_reg_HC08 alu)
847 (indX_low_reg_HC08 alu)
848 (indX_high_reg_HC08 alu)
859 (* setter forte di V *)
860 ndefinition set_v_flag ≝
861 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
862 opt_map ?? (match m return aux_set_typing_opt bool with
864 | HC08 ⇒ Some ? set_v_flag_HC08
865 | HCS08 ⇒ Some ? set_v_flag_HC08
867 (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
869 (* setter debole di V *)
870 ndefinition setweak_v_flag ≝
871 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
872 match set_v_flag m t s vfl' with
873 [ None ⇒ s | Some s' ⇒ s' ].
877 (* setter specifico HC05 di H *)
878 ndefinition set_h_flag_HC05 ≝
881 (acc_low_reg_HC05 alu)
882 (indX_low_reg_HC05 alu)
895 (* setter specifico HC08/HCS08 di H *)
896 ndefinition set_h_flag_HC08 ≝
899 (acc_low_reg_HC08 alu)
900 (indX_low_reg_HC08 alu)
901 (indX_high_reg_HC08 alu)
912 (* setter forte di H *)
913 ndefinition set_h_flag ≝
914 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
915 opt_map ?? (match m return aux_set_typing_opt bool with
916 [ HC05 ⇒ Some ? set_h_flag_HC05
917 | HC08 ⇒ Some ? set_h_flag_HC08
918 | HCS08 ⇒ Some ? set_h_flag_HC08
920 (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
922 (* setter debole di H *)
923 ndefinition setweak_h_flag ≝
924 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
925 match set_h_flag m t s hfl' with
926 [ None ⇒ s | Some s' ⇒ s' ].
930 (* setter specifico HC05 di I *)
931 ndefinition set_i_flag_HC05 ≝
934 (acc_low_reg_HC05 alu)
935 (indX_low_reg_HC05 alu)
948 (* setter specifico HC08/HCS08 di I *)
949 ndefinition set_i_flag_HC08 ≝
952 (acc_low_reg_HC08 alu)
953 (indX_low_reg_HC08 alu)
954 (indX_high_reg_HC08 alu)
965 (* setter forte di I *)
966 ndefinition set_i_flag ≝
967 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
968 opt_map ?? (match m return aux_set_typing_opt bool with
969 [ HC05 ⇒ Some ? set_i_flag_HC05
970 | HC08 ⇒ Some ? set_i_flag_HC08
971 | HCS08 ⇒ Some ? set_i_flag_HC08
973 (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
975 (* setter debole di I *)
976 ndefinition setweak_i_flag ≝
977 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
978 match set_i_flag m t s ifl' with
979 [ None ⇒ s | Some s' ⇒ s' ].
983 (* setter specifico HC05 di N *)
984 ndefinition set_n_flag_HC05 ≝
987 (acc_low_reg_HC05 alu)
988 (indX_low_reg_HC05 alu)
1001 (* setter specifico HC08/HCS08 di N *)
1002 ndefinition set_n_flag_HC08 ≝
1005 (acc_low_reg_HC08 alu)
1006 (indX_low_reg_HC08 alu)
1007 (indX_high_reg_HC08 alu)
1016 (irq_flag_HC08 alu).
1018 (* setter forte di N *)
1019 ndefinition set_n_flag ≝
1020 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
1021 opt_map ?? (match m return aux_set_typing_opt bool with
1022 [ HC05 ⇒ Some ? set_n_flag_HC05
1023 | HC08 ⇒ Some ? set_n_flag_HC08
1024 | HCS08 ⇒ Some ? set_n_flag_HC08
1026 (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
1028 (* setter debole di N *)
1029 ndefinition setweak_n_flag ≝
1030 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
1031 match set_n_flag m t s nfl' with
1032 [ None ⇒ s | Some s' ⇒ s' ].
1036 (* setter specifico HC05 di Z *)
1037 ndefinition set_z_flag_HC05 ≝
1040 (acc_low_reg_HC05 alu)
1041 (indX_low_reg_HC05 alu)
1052 (irq_flag_HC05 alu).
1054 (* setter specifico HC08/HCS08 di Z *)
1055 ndefinition set_z_flag_HC08 ≝
1058 (acc_low_reg_HC08 alu)
1059 (indX_low_reg_HC08 alu)
1060 (indX_high_reg_HC08 alu)
1069 (irq_flag_HC08 alu).
1071 (* setter sprcifico RS08 di Z *)
1072 ndefinition set_z_flag_RS08 ≝
1075 (acc_low_reg_RS08 alu)
1084 (* setter forte di Z *)
1085 ndefinition set_z_flag ≝
1086 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
1088 (match m return aux_set_typing bool with
1089 [ HC05 ⇒ set_z_flag_HC05
1090 | HC08 ⇒ set_z_flag_HC08
1091 | HCS08 ⇒ set_z_flag_HC08
1092 | RS08 ⇒ set_z_flag_RS08
1093 ] (alu m t s) zfl').
1097 (* setter specifico HC05 di C *)
1098 ndefinition set_c_flag_HC05 ≝
1101 (acc_low_reg_HC05 alu)
1102 (indX_low_reg_HC05 alu)
1113 (irq_flag_HC05 alu).
1115 (* setter specifico HC08/HCS08 di C *)
1116 ndefinition set_c_flag_HC08 ≝
1119 (acc_low_reg_HC08 alu)
1120 (indX_low_reg_HC08 alu)
1121 (indX_high_reg_HC08 alu)
1130 (irq_flag_HC08 alu).
1132 (* setter specifico RS08 di C *)
1133 ndefinition set_c_flag_RS08 ≝
1136 (acc_low_reg_RS08 alu)
1145 (* setter forte di C *)
1146 ndefinition set_c_flag ≝
1147 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
1149 (match m return aux_set_typing bool with
1150 [ HC05 ⇒ set_c_flag_HC05
1151 | HC08 ⇒ set_c_flag_HC08
1152 | HCS08 ⇒ set_c_flag_HC08
1153 | RS08 ⇒ set_c_flag_RS08
1154 ] (alu m t s) cfl').
1158 (* setter specifico HC05 di IRQ *)
1159 ndefinition set_irq_flag_HC05 ≝
1162 (acc_low_reg_HC05 alu)
1163 (indX_low_reg_HC05 alu)
1176 (* setter specifico HC08/HCS08 di IRQ *)
1177 ndefinition set_irq_flag_HC08 ≝
1180 (acc_low_reg_HC08 alu)
1181 (indX_low_reg_HC08 alu)
1182 (indX_high_reg_HC08 alu)
1193 (* setter forte di IRQ *)
1194 ndefinition set_irq_flag ≝
1195 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1196 opt_map ?? (match m return aux_set_typing_opt bool with
1197 [ HC05 ⇒ Some ? set_irq_flag_HC05
1198 | HC08 ⇒ Some ? set_irq_flag_HC08
1199 | HCS08 ⇒ Some ? set_irq_flag_HC08
1201 (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
1203 (* setter debole di IRQ *)
1204 ndefinition setweak_irq_flag ≝
1205 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1206 match set_irq_flag m t s irqfl' with
1207 [ None ⇒ s | Some s' ⇒ s' ].
1209 (* ***************** *)
1210 (* CONFRONTO FRA ALU *)
1211 (* ***************** *)
1213 (* confronto registro per registro dell'HC05 *)
1214 ndefinition eq_alu_HC05 ≝
1215 λalu1,alu2:alu_HC05.
1217 [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1219 [ mk_alu_HC05 acclow2 indxlow2 sp2 spm2 spf2 pc2 pcm2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1220 (eq_b8 acclow1 acclow2) ⊗
1221 (eq_b8 indxlow1 indxlow2) ⊗
1223 (eq_w16 spm1 spm2) ⊗
1224 (eq_w16 spf1 spf2) ⊗
1226 (eq_w16 pcm1 pcm2) ⊗
1227 (eq_bool hfl1 hfl2) ⊗
1228 (eq_bool ifl1 ifl2) ⊗
1229 (eq_bool nfl1 nfl2) ⊗
1230 (eq_bool zfl1 zfl2) ⊗
1231 (eq_bool cfl1 cfl2) ⊗
1232 (eq_bool irqfl1 irqfl2) ]].
1234 (* confronto registro per registro dell'HC08 *)
1235 ndefinition eq_alu_HC08 ≝
1236 λalu1,alu2:alu_HC08.
1238 [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1240 [ mk_alu_HC08 acclow2 indxlow2 indxhigh2 sp2 pc2 vfl2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1241 (eq_b8 acclow1 acclow2) ⊗
1242 (eq_b8 indxlow1 indxlow2) ⊗
1243 (eq_b8 indxhigh1 indxhigh2) ⊗
1246 (eq_bool vfl1 vfl2) ⊗
1247 (eq_bool hfl1 hfl2) ⊗
1248 (eq_bool ifl1 ifl2) ⊗
1249 (eq_bool nfl1 nfl2) ⊗
1250 (eq_bool zfl1 zfl2) ⊗
1251 (eq_bool cfl1 cfl2) ⊗
1252 (eq_bool irqfl1 irqfl2) ]].
1254 (* confronto registro per registro dell'RS08 *)
1255 ndefinition eq_alu_RS08 ≝
1256 λalu1,alu2:alu_RS08.
1258 [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
1260 [ mk_alu_RS08 acclow2 pc2 pcm2 spc2 xm2 psm2 zfl2 cfl2 ⇒
1261 (eq_b8 acclow1 acclow2) ⊗
1263 (eq_w16 pcm1 pcm2) ⊗
1264 (eq_w16 spc1 spc2) ⊗
1267 (eq_bool zfl1 zfl2) ⊗
1268 (eq_bool cfl1 cfl2) ]].
1270 (* ******************** *)
1271 (* CONFRONTO FRA STATUS *)
1272 (* ******************** *)
1274 (* confronto di una regione di memoria [addr1 ; ... ; addrn] *)
1275 nlet rec forall_memory_ranged
1277 (chk1:aux_chk_type t) (chk2:aux_chk_type t)
1278 (mem1:aux_mem_type t) (mem2:aux_mem_type t)
1279 (addrl:list word16) on addrl ≝
1280 match addrl return λ_.bool with
1282 | cons hd tl ⇒ (eq_option byte8 (mem_read t mem1 chk1 hd)
1283 (mem_read t mem2 chk2 hd) eq_b8) ⊗
1284 (forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
1287 (* il clk e' option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16) *)
1288 ndefinition eq_clk ≝
1289 λm:mcu_type.λc1,c2:option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
1291 [ None ⇒ match c2 with
1292 [ None ⇒ true | Some _ ⇒ false ]
1293 | Some c1' ⇒ match c2 with
1294 [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T ????? c1') (fst5T ????? c2')) ⊗
1295 (eq_anyop m (snd5T ????? c1') (snd5T ????? c2')) ⊗
1296 (eq_instrmode (thd5T ????? c1') (thd5T ????? c2')) ⊗
1297 (eq_b8 (frth5T ????? c1') (frth5T ????? c2')) ⊗
1298 (eq_w16 (ffth5T ????? c1') (ffth5T ????? c2')) ]
1301 (* generalizzazione del confronto fra stati *)
1302 ndefinition eq_status ≝
1303 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word16.
1304 match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
1305 match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
1307 (* 1) confronto della ALU *)
1308 (match m return λm:mcu_type.
1310 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1312 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1314 [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ]
1317 (* 2) confronto della memoria in [inf,inf+n] *)
1318 (forall_memory_ranged t chk1 chk2 mem1 mem2 addrl) ⊗
1320 (* 3) confronto del clik *)
1321 (eq_clk m clk1 clk2)