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 ndefinition alu_HC05_ind :
68 ΠP:alu_HC05 → Prop.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝
69 λP:alu_HC05 → Prop.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05.
70 match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ].
72 ndefinition alu_HC05_rec :
73 ΠP:alu_HC05 → Set.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝
74 λP:alu_HC05 → Set.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05.
75 match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ].
77 ndefinition alu_HC05_rect :
78 ΠP:alu_HC05 → Type.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝
79 λP:alu_HC05 → Type.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05.
80 match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ].
82 ndefinition acc_low_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 x _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x ].
83 ndefinition indX_low_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ x _ _ _ _ _ _ _ _ _ _ _ ⇒ x ].
84 ndefinition sp_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ x _ _ _ _ _ _ _ _ _ _ ⇒ x ].
85 ndefinition sp_mask_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ x _ _ _ _ _ _ _ _ _ ⇒ x ].
86 ndefinition sp_fix_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ x _ _ _ _ _ _ _ _ ⇒ x ].
87 ndefinition pc_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ x _ _ _ _ _ _ _ ⇒ x ].
88 ndefinition pc_mask_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ x _ _ _ _ _ _ ⇒ x ].
89 ndefinition h_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ x _ _ _ _ _ ⇒ x ].
90 ndefinition i_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ x _ _ _ _ ⇒ x ].
91 ndefinition n_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ x _ _ _ ⇒ x ].
92 ndefinition z_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ x _ _ ⇒ x ].
93 ndefinition c_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ x _ ⇒ x ].
94 ndefinition irq_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ x ⇒ x ].
96 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)}"
97 non associative with precedence 80 for
98 @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
99 interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
100 (mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
102 (* ALU dell'HC08/HCS08 *)
103 nrecord alu_HC08: Type ≝
105 (* A: registo accumulatore *)
106 acc_low_reg_HC08 : byte8;
107 (* X: registro indice parte bassa *)
108 indX_low_reg_HC08 : byte8;
109 (* H: registro indice parte alta *)
110 indX_high_reg_HC08 : byte8;
111 (* SP: registo stack pointer *)
112 sp_reg_HC08 : word16;
113 (* PC: registro program counter *)
114 pc_reg_HC08 : word16;
116 (* V: flag overflow *)
118 (* H: flag semi-carry (somma nibble basso) *)
120 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
122 (* N: flag segno/negativita' *)
129 (* IRQ: flag che simula il pin esterno IRQ *)
133 ndefinition alu_HC08_ind :
134 ΠP:alu_HC08 → Prop.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝
135 λP:alu_HC08 → Prop.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08.
136 match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ].
138 ndefinition alu_HC08_rec :
139 ΠP:alu_HC08 → Set.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝
140 λP:alu_HC08 → Set.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08.
141 match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ].
143 ndefinition alu_HC08_rect :
144 ΠP:alu_HC08 → Type.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝
145 λP:alu_HC08 → Type.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08.
146 match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ].
148 ndefinition acc_low_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 x _ _ _ _ _ _ _ _ _ _ _ ⇒ x ].
149 ndefinition indX_low_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ x _ _ _ _ _ _ _ _ _ _ ⇒ x ].
150 ndefinition indX_high_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ x _ _ _ _ _ _ _ _ _ ⇒ x ].
151 ndefinition sp_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ x _ _ _ _ _ _ _ _ ⇒ x ].
152 ndefinition pc_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ x _ _ _ _ _ _ _ ⇒ x ].
153 ndefinition v_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ x _ _ _ _ _ _ ⇒ x ].
154 ndefinition h_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ x _ _ _ _ _ ⇒ x ].
155 ndefinition i_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ x _ _ _ _ ⇒ x ].
156 ndefinition n_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ x _ _ _ ⇒ x ].
157 ndefinition z_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ x _ _ ⇒ x ].
158 ndefinition c_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ x _ ⇒ x ].
159 ndefinition irq_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ x ⇒ x ].
161 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)}"
162 non associative with precedence 80 for
163 @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
164 interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
165 (mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
168 nrecord alu_RS08: Type ≝
170 (* A: registo accumulatore *)
171 acc_low_reg_RS08 : byte8;
172 (* PC: registro program counter *)
173 pc_reg_RS08 : word16;
174 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
175 (* la logica della sua costruzione e' quindi (PC∧mask) *)
176 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
177 pc_mask_RS08 : word16;
178 (* SPC: registro shadow program counter *)
179 (* NB: il suo modificatore e' lo stesso di PC *)
180 spc_reg_RS08 : word16;
182 (* X: registro indice parte bassa *)
183 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
184 (* la lettura/scrittura avviene tramite la locazione [0x000F] *)
185 (* la funzione memory_filter_read/write si occupera' di intercettare *)
186 (* e deviare sul registro le letture/scritture (modulo load_write) *)
188 (* PS: registro selezione di pagina *)
189 (* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *)
190 (* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *)
191 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
192 (* la lettura/scrittura avviene tramite la locazione [0x001F] *)
193 (* la funzione memory_filter_read/write si occupera' di intercettare *)
194 (* e deviare sul registro le letture/scritture (modulo load_write) *)
203 ndefinition alu_RS08_ind :
204 ΠP:alu_RS08 → Prop.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝
205 λP:alu_RS08 → Prop.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08.
206 match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ].
208 ndefinition alu_RS08_rec :
209 ΠP:alu_RS08 → Set.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝
210 λP:alu_RS08 → Set.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08.
211 match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ].
213 ndefinition alu_RS08_rect :
214 ΠP:alu_RS08 → Type.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝
215 λP:alu_RS08 → Type.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08.
216 match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ].
218 ndefinition acc_low_reg_RS08 ≝ λalu.match alu with [ mk_alu_RS08 x _ _ _ _ _ _ _ ⇒ x ].
219 ndefinition pc_reg_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ x _ _ _ _ _ _ ⇒ x ].
220 ndefinition pc_mask_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ x _ _ _ _ _ ⇒ x ].
221 ndefinition spc_reg_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ x _ _ _ _ ⇒ x ].
222 ndefinition x_map_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ x _ _ _ ⇒ x ].
223 ndefinition ps_map_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ x _ _ ⇒ x ].
224 ndefinition z_flag_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ _ x _ ⇒ x ].
225 ndefinition c_flag_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ _ _ x ⇒ x ].
227 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)}"
228 non associative with precedence 80 for
229 @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
230 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
231 (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
233 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
234 nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
237 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ];
239 (* descritore della memoria *)
240 mem_desc : aux_mem_type t;
241 (* descrittore del tipo di memoria installata *)
242 chk_desc : aux_chk_type t;
243 (* descrittore del click = stato di avanzamento dell'esecuzione+cur_pc conseguente a fetch *)
244 (* 1) None = istruzione eseguita, attesa del fetch *)
245 (* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito, countup a esecuzione *)
246 clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16)
249 ndefinition any_status_ind :
250 Πmcu.Πt.ΠP:any_status mcu t → Prop.
251 (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
252 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
253 λmcu.λt.λP:any_status mcu t → Prop.
254 λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
255 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
256 match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
258 ndefinition any_status_rec :
259 Πmcu.Πt.ΠP:any_status mcu t → Set.
260 (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
261 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
262 λmcu.λt.λP:any_status mcu t → Set.
263 λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
264 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
265 match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
267 ndefinition any_status_rect :
268 Πmcu.Πt.ΠP:any_status mcu t → Type.
269 (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
270 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
271 λmcu.λt.λP:any_status mcu t → Type.
272 λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
273 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
274 match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
276 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 ].
277 ndefinition mem_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ x _ _ ⇒ x ].
278 ndefinition chk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ x _ ⇒ x ].
279 ndefinition clk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ _ x ⇒ x ].
281 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
282 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
283 for @{ 'mk_any_status $alu $mem $chk $clk }.
284 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
285 (mk_any_status alu mem chk clk).
287 (* **************** *)
288 (* GETTER SPECIFICI *)
289 (* **************** *)
291 (* funzione ausiliaria per il tipaggio dei getter *)
292 ndefinition aux_get_typing ≝ λx:Type.λm:mcu_type.match m with
293 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] → x.
297 (* getter di A, esiste sempre *)
298 ndefinition get_acc_8_low_reg ≝
299 λm:mcu_type.λt:memory_impl.λs:any_status m t.
301 return aux_get_typing byte8 with
302 [ HC05 ⇒ acc_low_reg_HC05
303 | HC08 ⇒ acc_low_reg_HC08
304 | HCS08 ⇒ acc_low_reg_HC08
305 | RS08 ⇒ acc_low_reg_RS08 ]
308 (* getter di X, non esiste sempre *)
309 ndefinition get_indX_8_low_reg ≝
310 λm:mcu_type.λt:memory_impl.λs:any_status m t.
312 return aux_get_typing (option byte8) with
313 [ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
314 | HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
315 | HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
316 | RS08 ⇒ λalu.None ? ]
319 (* getter di H, non esiste sempre *)
320 ndefinition get_indX_8_high_reg ≝
321 λm:mcu_type.λt:memory_impl.λs:any_status m t.
323 return aux_get_typing (option byte8) with
325 | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
326 | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
327 | RS08 ⇒ λalu.None ? ]
330 (* getter di H:X, non esiste sempre *)
331 ndefinition get_indX_16_reg ≝
332 λm:mcu_type.λt:memory_impl.λs:any_status m t.
334 return aux_get_typing (option word16) with
336 | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
337 | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
338 | RS08 ⇒ λalu.None ? ]
341 (* getter di SP, non esiste sempre *)
342 ndefinition get_sp_reg ≝
343 λm:mcu_type.λt:memory_impl.λs:any_status m t.
345 return aux_get_typing (option word16) with
346 [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
347 | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
348 | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
349 | RS08 ⇒ λalu.None ? ]
352 (* getter di PC, esiste sempre *)
353 ndefinition get_pc_reg ≝
354 λm:mcu_type.λt:memory_impl.λs:any_status m t.
356 return aux_get_typing word16 with
359 | HCS08 ⇒ pc_reg_HC08
360 | RS08 ⇒ pc_reg_RS08 ]
363 (* getter di SPC, non esiste sempre *)
364 ndefinition get_spc_reg ≝
365 λm:mcu_type.λt:memory_impl.λs:any_status m t.
367 return aux_get_typing (option word16) with
370 | HCS08 ⇒ λalu.None ?
371 | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu) ]
374 (* REGISTRI MEMORY MAPPED *)
376 (* getter di memory mapped X, non esiste sempre *)
377 ndefinition get_x_map ≝
378 λm:mcu_type.λt:memory_impl.λs:any_status m t.
380 return aux_get_typing (option byte8) with
383 | HCS08 ⇒ λalu.None ?
384 | RS08 ⇒ λalu.Some ? (x_map_RS08 alu) ]
387 (* getter di memory mapped PS, non esiste sempre *)
388 ndefinition get_ps_map ≝
389 λm:mcu_type.λt:memory_impl.λs:any_status m t.
391 return aux_get_typing (option byte8) with
394 | HCS08 ⇒ λalu.None ?
395 | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu) ]
400 (* getter di V, non esiste sempre *)
401 ndefinition get_v_flag ≝
402 λm:mcu_type.λt:memory_impl.λs:any_status m t.
404 return aux_get_typing (option bool) with
406 | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
407 | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
408 | RS08 ⇒ λalu.None ? ]
411 (* getter di H, non esiste sempre *)
412 ndefinition get_h_flag ≝
413 λm:mcu_type.λt:memory_impl.λs:any_status m t.
415 return aux_get_typing (option bool) with
416 [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
417 | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
418 | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
419 | RS08 ⇒ λalu.None ? ]
422 (* getter di I, non esiste sempre *)
423 ndefinition get_i_flag ≝
424 λm:mcu_type.λt:memory_impl.λs:any_status m t.
426 return aux_get_typing (option bool) with
427 [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
428 | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
429 | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
430 | RS08 ⇒ λalu.None ? ]
433 (* getter di N, non esiste sempre *)
434 ndefinition get_n_flag ≝
435 λm:mcu_type.λt:memory_impl.λs:any_status m t.
437 return aux_get_typing (option bool) with
438 [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
439 | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
440 | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
441 | RS08 ⇒ λalu.None ? ]
444 (* getter di Z, esiste sempre *)
445 ndefinition get_z_flag ≝
446 λm:mcu_type.λt:memory_impl.λs:any_status m t.
448 return aux_get_typing bool with
451 | HCS08 ⇒ z_flag_HC08
452 | RS08 ⇒ z_flag_RS08 ]
455 (* getter di C, esiste sempre *)
456 ndefinition get_c_flag ≝
457 λm:mcu_type.λt:memory_impl.λs:any_status m t.
459 return aux_get_typing bool with
462 | HCS08 ⇒ c_flag_HC08
463 | RS08 ⇒ c_flag_RS08 ]
466 (* getter di IRQ, non esiste sempre *)
467 ndefinition get_irq_flag ≝
468 λm:mcu_type.λt:memory_impl.λs:any_status m t.
470 return aux_get_typing (option bool) with
471 [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
472 | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
473 | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
474 | RS08 ⇒ λalu.None ? ]
477 (* DESCRITTORI ESTERNI ALLA ALU *)
479 (* getter della ALU, esiste sempre *)
480 ndefinition get_alu ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.alu m t s.
482 (* getter della memoria, esiste sempre *)
483 ndefinition get_mem_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.mem_desc m t s.
485 (* getter del descrittore, esiste sempre *)
486 ndefinition get_chk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.chk_desc m t s.
488 (* getter del clik, esiste sempre *)
489 ndefinition get_clk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.clk_desc m t s.
491 (* ***************************** *)
492 (* SETTER SPECIFICI FORTI/DEBOLI *)
493 (* ***************************** *)
495 (* funzione ausiliaria per il tipaggio dei setter forti *)
496 ndefinition aux_set_typing ≝ λx:Type.λm:mcu_type.
497 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
499 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
501 (* funzione ausiliaria per il tipaggio dei setter deboli *)
502 ndefinition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option
503 (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
505 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]).
507 (* DESCRITTORI ESTERNI ALLA ALU *)
509 (* setter forte della ALU *)
510 ndefinition set_alu ≝
511 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
512 mk_any_status m t alu' (get_mem_desc m t s) (get_chk_desc m t s) (get_clk_desc m t s).
514 (* setter forte della memoria *)
515 ndefinition set_mem_desc ≝
516 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
517 mk_any_status m t (get_alu m t s) mem' (get_chk_desc m t s) (get_clk_desc m t s).
519 (* setter forte del descrittore *)
520 ndefinition set_chk_desc ≝
521 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
522 mk_any_status m t (get_alu m t s) (get_mem_desc m t s) chk' (get_clk_desc m t s).
524 (* setter forte del clik *)
525 ndefinition set_clk_desc ≝
526 λm:mcu_type.λt:memory_impl.λs:any_status m t.
527 λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
528 mk_any_status m t (get_alu m t s) (get_mem_desc m t s) (get_chk_desc m t s) clk'.
532 (* setter specifico HC05 di A *)
533 ndefinition set_acc_8_low_reg_HC05 ≝
537 (indX_low_reg_HC05 alu)
550 (* setter specifico HC08/HCS08 di A *)
551 ndefinition set_acc_8_low_reg_HC08 ≝
555 (indX_low_reg_HC08 alu)
556 (indX_high_reg_HC08 alu)
567 (* setter specifico RS08 di A *)
568 ndefinition set_acc_8_low_reg_RS08 ≝
580 (* setter forte di A *)
581 ndefinition set_acc_8_low_reg ≝
582 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
584 (match m return aux_set_typing byte8 with
585 [ HC05 ⇒ set_acc_8_low_reg_HC05
586 | HC08 ⇒ set_acc_8_low_reg_HC08
587 | HCS08 ⇒ set_acc_8_low_reg_HC08
588 | RS08 ⇒ set_acc_8_low_reg_RS08
589 ] (alu m t s) acclow').
593 (* setter specifico HC05 di X *)
594 ndefinition set_indX_8_low_reg_HC05 ≝
595 λalu.λindxlow':byte8.
597 (acc_low_reg_HC05 alu)
611 (* setter specifico HC08/HCS08 di X *)
612 ndefinition set_indX_8_low_reg_HC08 ≝
613 λalu.λindxlow':byte8.
615 (acc_low_reg_HC08 alu)
617 (indX_high_reg_HC08 alu)
628 (* setter forte di X *)
629 ndefinition set_indX_8_low_reg ≝
630 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
631 opt_map ?? (match m return aux_set_typing_opt byte8 with
632 [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
633 | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
634 | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
636 (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
638 (* setter debole di X *)
639 ndefinition setweak_indX_8_low_reg ≝
640 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
641 match set_indX_8_low_reg m t s indxlow' with
642 [ None ⇒ s | Some s' ⇒ s' ].
646 (* setter specifico HC08/HCS08 di H *)
647 ndefinition set_indX_8_high_reg_HC08 ≝
648 λalu.λindxhigh':byte8.
650 (acc_low_reg_HC08 alu)
651 (indX_low_reg_HC08 alu)
663 (* setter forte di H *)
664 ndefinition set_indX_8_high_reg ≝
665 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
666 opt_map ?? (match m return aux_set_typing_opt byte8 with
668 | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
669 | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
671 (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
673 (* setter debole di H *)
674 ndefinition setweak_indX_8_high_reg ≝
675 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
676 match set_indX_8_high_reg m t s indxhigh' with
677 [ None ⇒ s | Some s' ⇒ s' ].
681 (* setter specifico HC08/HCS08 di H:X *)
682 ndefinition set_indX_16_reg_HC08 ≝
685 (acc_low_reg_HC08 alu)
698 (* setter forte di H:X *)
699 ndefinition set_indX_16_reg ≝
700 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
701 opt_map ?? (match m return aux_set_typing_opt word16 with
703 | HC08 ⇒ Some ? set_indX_16_reg_HC08
704 | HCS08 ⇒ Some ? set_indX_16_reg_HC08
706 (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
708 (* setter debole di H:X *)
709 ndefinition setweak_indX_16_reg ≝
710 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
711 match set_indX_16_reg m t s indx16 with
712 [ None ⇒ s | Some s' ⇒ s' ].
716 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
717 ndefinition set_sp_reg_HC05 ≝
720 (acc_low_reg_HC05 alu)
721 (indX_low_reg_HC05 alu)
722 (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
734 (* setter specifico HC08/HCS08 di SP *)
735 ndefinition set_sp_reg_HC08 ≝
738 (acc_low_reg_HC08 alu)
739 (indX_low_reg_HC08 alu)
740 (indX_high_reg_HC08 alu)
751 (* setter forte di SP *)
752 ndefinition set_sp_reg ≝
753 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
754 opt_map ?? (match m return aux_set_typing_opt word16 with
755 [ HC05 ⇒ Some ? set_sp_reg_HC05
756 | HC08 ⇒ Some ? set_sp_reg_HC08
757 | HCS08 ⇒ Some ? set_sp_reg_HC08
759 (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
761 (* setter debole di SP *)
762 ndefinition setweak_sp_reg ≝
763 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
764 match set_sp_reg m t s sp' with
765 [ None ⇒ s | Some s' ⇒ s' ].
769 (* setter specifico HC05 di PC, effettua PC∧mask *)
770 ndefinition set_pc_reg_HC05 ≝
773 (acc_low_reg_HC05 alu)
774 (indX_low_reg_HC05 alu)
778 (and_w16 pc' (pc_mask_HC05 alu))
787 (* setter specifico HC08/HCS08 di PC *)
788 ndefinition set_pc_reg_HC08 ≝
791 (acc_low_reg_HC08 alu)
792 (indX_low_reg_HC08 alu)
793 (indX_high_reg_HC08 alu)
804 (* setter specifico RS08 di PC, effettua PC∧mask *)
805 ndefinition set_pc_reg_RS08 ≝
808 (acc_low_reg_RS08 alu)
809 (and_w16 pc' (pc_mask_RS08 alu))
817 (* setter forte di PC *)
818 ndefinition set_pc_reg ≝
819 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
821 (match m return aux_set_typing word16 with
822 [ HC05 ⇒ set_pc_reg_HC05
823 | HC08 ⇒ set_pc_reg_HC08
824 | HCS08 ⇒ set_pc_reg_HC08
825 | RS08 ⇒ set_pc_reg_RS08
830 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
831 ndefinition set_spc_reg_RS08 ≝
834 (acc_low_reg_RS08 alu)
837 (and_w16 spc' (pc_mask_RS08 alu))
843 (* setter forte di SPC *)
844 ndefinition set_spc_reg ≝
845 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
846 opt_map ?? (match m return aux_set_typing_opt word16 with
850 | RS08 ⇒ Some ? set_spc_reg_RS08 ])
851 (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
853 (* setter debole di SPC *)
854 ndefinition setweak_spc_reg ≝
855 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
856 match set_spc_reg m t s spc' with
857 [ None ⇒ s | Some s' ⇒ s' ].
859 (* REGISTRO MEMORY MAPPED X *)
861 (* setter specifico RS08 di memory mapped X *)
862 ndefinition set_x_map_RS08 ≝
865 (acc_low_reg_RS08 alu)
874 (* setter forte di memory mapped X *)
875 ndefinition set_x_map ≝
876 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
877 opt_map ?? (match m return aux_set_typing_opt byte8 with
881 | RS08 ⇒ Some ? set_x_map_RS08 ])
882 (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
884 (* setter debole di memory mapped X *)
885 ndefinition setweak_x_map ≝
886 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
887 match set_x_map m t s xm' with
888 [ None ⇒ s | Some s' ⇒ s' ].
890 (* REGISTRO MEMORY MAPPED PS *)
892 (* setter specifico RS08 di memory mapped PS *)
893 ndefinition set_ps_map_RS08 ≝
896 (acc_low_reg_RS08 alu)
905 (* setter forte di memory mapped PS *)
906 ndefinition set_ps_map ≝
907 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
908 opt_map ?? (match m return aux_set_typing_opt byte8 with
912 | RS08 ⇒ Some ? set_ps_map_RS08 ])
913 (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
915 (* setter debole di memory mapped PS *)
916 ndefinition setweak_ps_map ≝
917 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
918 match set_ps_map m t s psm' with
919 [ None ⇒ s | Some s' ⇒ s' ].
923 (* setter specifico HC08/HCS08 di V *)
924 ndefinition set_v_flag_HC08 ≝
927 (acc_low_reg_HC08 alu)
928 (indX_low_reg_HC08 alu)
929 (indX_high_reg_HC08 alu)
940 (* setter forte di V *)
941 ndefinition set_v_flag ≝
942 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
943 opt_map ?? (match m return aux_set_typing_opt bool with
945 | HC08 ⇒ Some ? set_v_flag_HC08
946 | HCS08 ⇒ Some ? set_v_flag_HC08
948 (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
950 (* setter debole di V *)
951 ndefinition setweak_v_flag ≝
952 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
953 match set_v_flag m t s vfl' with
954 [ None ⇒ s | Some s' ⇒ s' ].
958 (* setter specifico HC05 di H *)
959 ndefinition set_h_flag_HC05 ≝
962 (acc_low_reg_HC05 alu)
963 (indX_low_reg_HC05 alu)
976 (* setter specifico HC08/HCS08 di H *)
977 ndefinition set_h_flag_HC08 ≝
980 (acc_low_reg_HC08 alu)
981 (indX_low_reg_HC08 alu)
982 (indX_high_reg_HC08 alu)
993 (* setter forte di H *)
994 ndefinition set_h_flag ≝
995 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
996 opt_map ?? (match m return aux_set_typing_opt bool with
997 [ HC05 ⇒ Some ? set_h_flag_HC05
998 | HC08 ⇒ Some ? set_h_flag_HC08
999 | HCS08 ⇒ Some ? set_h_flag_HC08
1001 (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
1003 (* setter debole di H *)
1004 ndefinition setweak_h_flag ≝
1005 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
1006 match set_h_flag m t s hfl' with
1007 [ None ⇒ s | Some s' ⇒ s' ].
1011 (* setter specifico HC05 di I *)
1012 ndefinition set_i_flag_HC05 ≝
1015 (acc_low_reg_HC05 alu)
1016 (indX_low_reg_HC05 alu)
1027 (irq_flag_HC05 alu).
1029 (* setter specifico HC08/HCS08 di I *)
1030 ndefinition set_i_flag_HC08 ≝
1033 (acc_low_reg_HC08 alu)
1034 (indX_low_reg_HC08 alu)
1035 (indX_high_reg_HC08 alu)
1044 (irq_flag_HC08 alu).
1046 (* setter forte di I *)
1047 ndefinition set_i_flag ≝
1048 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
1049 opt_map ?? (match m return aux_set_typing_opt bool with
1050 [ HC05 ⇒ Some ? set_i_flag_HC05
1051 | HC08 ⇒ Some ? set_i_flag_HC08
1052 | HCS08 ⇒ Some ? set_i_flag_HC08
1054 (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
1056 (* setter debole di I *)
1057 ndefinition setweak_i_flag ≝
1058 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
1059 match set_i_flag m t s ifl' with
1060 [ None ⇒ s | Some s' ⇒ s' ].
1064 (* setter specifico HC05 di N *)
1065 ndefinition set_n_flag_HC05 ≝
1068 (acc_low_reg_HC05 alu)
1069 (indX_low_reg_HC05 alu)
1080 (irq_flag_HC05 alu).
1082 (* setter specifico HC08/HCS08 di N *)
1083 ndefinition set_n_flag_HC08 ≝
1086 (acc_low_reg_HC08 alu)
1087 (indX_low_reg_HC08 alu)
1088 (indX_high_reg_HC08 alu)
1097 (irq_flag_HC08 alu).
1099 (* setter forte di N *)
1100 ndefinition set_n_flag ≝
1101 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
1102 opt_map ?? (match m return aux_set_typing_opt bool with
1103 [ HC05 ⇒ Some ? set_n_flag_HC05
1104 | HC08 ⇒ Some ? set_n_flag_HC08
1105 | HCS08 ⇒ Some ? set_n_flag_HC08
1107 (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
1109 (* setter debole di N *)
1110 ndefinition setweak_n_flag ≝
1111 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
1112 match set_n_flag m t s nfl' with
1113 [ None ⇒ s | Some s' ⇒ s' ].
1117 (* setter specifico HC05 di Z *)
1118 ndefinition set_z_flag_HC05 ≝
1121 (acc_low_reg_HC05 alu)
1122 (indX_low_reg_HC05 alu)
1133 (irq_flag_HC05 alu).
1135 (* setter specifico HC08/HCS08 di Z *)
1136 ndefinition set_z_flag_HC08 ≝
1139 (acc_low_reg_HC08 alu)
1140 (indX_low_reg_HC08 alu)
1141 (indX_high_reg_HC08 alu)
1150 (irq_flag_HC08 alu).
1152 (* setter sprcifico RS08 di Z *)
1153 ndefinition set_z_flag_RS08 ≝
1156 (acc_low_reg_RS08 alu)
1165 (* setter forte di Z *)
1166 ndefinition set_z_flag ≝
1167 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
1169 (match m return aux_set_typing bool with
1170 [ HC05 ⇒ set_z_flag_HC05
1171 | HC08 ⇒ set_z_flag_HC08
1172 | HCS08 ⇒ set_z_flag_HC08
1173 | RS08 ⇒ set_z_flag_RS08
1174 ] (alu m t s) zfl').
1178 (* setter specifico HC05 di C *)
1179 ndefinition set_c_flag_HC05 ≝
1182 (acc_low_reg_HC05 alu)
1183 (indX_low_reg_HC05 alu)
1194 (irq_flag_HC05 alu).
1196 (* setter specifico HC08/HCS08 di C *)
1197 ndefinition set_c_flag_HC08 ≝
1200 (acc_low_reg_HC08 alu)
1201 (indX_low_reg_HC08 alu)
1202 (indX_high_reg_HC08 alu)
1211 (irq_flag_HC08 alu).
1213 (* setter specifico RS08 di C *)
1214 ndefinition set_c_flag_RS08 ≝
1217 (acc_low_reg_RS08 alu)
1226 (* setter forte di C *)
1227 ndefinition set_c_flag ≝
1228 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
1230 (match m return aux_set_typing bool with
1231 [ HC05 ⇒ set_c_flag_HC05
1232 | HC08 ⇒ set_c_flag_HC08
1233 | HCS08 ⇒ set_c_flag_HC08
1234 | RS08 ⇒ set_c_flag_RS08
1235 ] (alu m t s) cfl').
1239 (* setter specifico HC05 di IRQ *)
1240 ndefinition set_irq_flag_HC05 ≝
1243 (acc_low_reg_HC05 alu)
1244 (indX_low_reg_HC05 alu)
1257 (* setter specifico HC08/HCS08 di IRQ *)
1258 ndefinition set_irq_flag_HC08 ≝
1261 (acc_low_reg_HC08 alu)
1262 (indX_low_reg_HC08 alu)
1263 (indX_high_reg_HC08 alu)
1274 (* setter forte di IRQ *)
1275 ndefinition set_irq_flag ≝
1276 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1277 opt_map ?? (match m return aux_set_typing_opt bool with
1278 [ HC05 ⇒ Some ? set_irq_flag_HC05
1279 | HC08 ⇒ Some ? set_irq_flag_HC08
1280 | HCS08 ⇒ Some ? set_irq_flag_HC08
1282 (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
1284 (* setter debole di IRQ *)
1285 ndefinition setweak_irq_flag ≝
1286 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1287 match set_irq_flag m t s irqfl' with
1288 [ None ⇒ s | Some s' ⇒ s' ].
1290 (* ***************** *)
1291 (* CONFRONTO FRA ALU *)
1292 (* ***************** *)
1294 (* confronto registro per registro dell'HC05 *)
1295 ndefinition eq_alu_HC05 ≝
1296 λalu1,alu2:alu_HC05.
1298 [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1300 [ mk_alu_HC05 acclow2 indxlow2 sp2 spm2 spf2 pc2 pcm2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1301 (eq_b8 acclow1 acclow2) ⊗
1302 (eq_b8 indxlow1 indxlow2) ⊗
1304 (eq_w16 spm1 spm2) ⊗
1305 (eq_w16 spf1 spf2) ⊗
1307 (eq_w16 pcm1 pcm2) ⊗
1308 (eq_bool hfl1 hfl2) ⊗
1309 (eq_bool ifl1 ifl2) ⊗
1310 (eq_bool nfl1 nfl2) ⊗
1311 (eq_bool zfl1 zfl2) ⊗
1312 (eq_bool cfl1 cfl2) ⊗
1313 (eq_bool irqfl1 irqfl2) ]].
1315 (* confronto registro per registro dell'HC08 *)
1316 ndefinition eq_alu_HC08 ≝
1317 λalu1,alu2:alu_HC08.
1319 [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1321 [ mk_alu_HC08 acclow2 indxlow2 indxhigh2 sp2 pc2 vfl2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1322 (eq_b8 acclow1 acclow2) ⊗
1323 (eq_b8 indxlow1 indxlow2) ⊗
1324 (eq_b8 indxhigh1 indxhigh2) ⊗
1327 (eq_bool vfl1 vfl2) ⊗
1328 (eq_bool hfl1 hfl2) ⊗
1329 (eq_bool ifl1 ifl2) ⊗
1330 (eq_bool nfl1 nfl2) ⊗
1331 (eq_bool zfl1 zfl2) ⊗
1332 (eq_bool cfl1 cfl2) ⊗
1333 (eq_bool irqfl1 irqfl2) ]].
1335 (* confronto registro per registro dell'RS08 *)
1336 ndefinition eq_alu_RS08 ≝
1337 λalu1,alu2:alu_RS08.
1339 [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
1341 [ mk_alu_RS08 acclow2 pc2 pcm2 spc2 xm2 psm2 zfl2 cfl2 ⇒
1342 (eq_b8 acclow1 acclow2) ⊗
1344 (eq_w16 pcm1 pcm2) ⊗
1345 (eq_w16 spc1 spc2) ⊗
1348 (eq_bool zfl1 zfl2) ⊗
1349 (eq_bool cfl1 cfl2) ]].
1351 (* ******************** *)
1352 (* CONFRONTO FRA STATUS *)
1353 (* ******************** *)
1355 (* confronto di una regione di memoria [addr1 ; ... ; addrn] *)
1356 nlet rec forall_memory_ranged
1358 (chk1:aux_chk_type t) (chk2:aux_chk_type t)
1359 (mem1:aux_mem_type t) (mem2:aux_mem_type t)
1360 (addrl:list word16) on addrl ≝
1361 match addrl return λ_.bool with
1363 | cons hd tl ⇒ (eq_option byte8 (mem_read t mem1 chk1 hd)
1364 (mem_read t mem2 chk2 hd) eq_b8) ⊗
1365 (forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
1368 (* il clk e' option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16) *)
1369 ndefinition eq_clk ≝
1370 λm:mcu_type.λc1,c2:option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
1372 [ None ⇒ match c2 with
1373 [ None ⇒ true | Some _ ⇒ false ]
1374 | Some c1' ⇒ match c2 with
1375 [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T ????? c1') (fst5T ????? c2')) ⊗
1376 (eq_anyop m (snd5T ????? c1') (snd5T ????? c2')) ⊗
1377 (eq_instrmode (thd5T ????? c1') (thd5T ????? c2')) ⊗
1378 (eq_b8 (frth5T ????? c1') (frth5T ????? c2')) ⊗
1379 (eq_w16 (ffth5T ????? c1') (ffth5T ????? c2')) ]
1382 (* generalizzazione del confronto fra stati *)
1383 ndefinition eq_status ≝
1384 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word16.
1385 match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
1386 match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
1388 (* 1) confronto della ALU *)
1389 (match m return λm:mcu_type.
1391 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1393 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1395 [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ]
1398 (* 2) confronto della memoria in [inf,inf+n] *)
1399 (forall_memory_ranged t chk1 chk2 mem1 mem2 addrl) ⊗
1401 (* 3) confronto del clik *)
1402 (eq_clk m clk1 clk2)