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 *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 set "baseuri" "cic:/matita/freescale/multivm/".
29 (*include "/media/VIRTUOSO/freescale/load_write.ma".*)
30 include "freescale/load_write.ma".
32 (* ************************************************ *)
33 (* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *)
34 (* ************************************************ *)
36 (* NB: dentro il codice i commenti cercano di spiegare la logica
37 secondo quanto riportato dalle specifiche delle mcu *)
39 (* NB: notare che tranne nei casi in cui PC viene modificato esplicitamente
40 il suo avanzamento viene delegato totalmente agli strati inferiori
41 I) avanzamento dovuto al decode degli op (fetch)
42 II) avanzamento dovuto al caricamento degli argomenti (multi_mode_load/write)
43 la modifica effettiva avviene poi centralizzata in tick *)
45 (* A = [true] fAMC(A,M,C), [false] A *)
46 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
47 (* fAMC e' la logica da applicare: somma con/senza carry *)
48 definition execute_ADC_ADD_aux ≝
49 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
50 λfAMC:byte8 → byte8 → bool → ProdT byte8 bool.
51 opt_map ?? (multi_mode_load true m t s cur_pc i)
52 (λS_M_PC.match S_M_PC with
53 [ tripleT s_tmp1 M_op new_pc ⇒
54 let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
55 match fAMC A_op M_op (get_c_flag m t s_tmp1) with
57 let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
58 let A3 ≝ MSB_ex (b8l A_op) in let M3 ≝ MSB_ex (b8l M_op) in let R3 ≝ MSB_ex (b8l R_op) in
59 (* A = [true] fAMC(A,M,C), [false] A *)
60 let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
61 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
62 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
63 (* C = A7&M7 | M7&nR7 | nR7&A7 *)
64 let s_tmp4 ≝ set_c_flag m t s_tmp3 ((A7⊗M7) ⊕ (M7⊗(⊖R7)) ⊕ ((⊖R7)⊗A7)) in
66 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 R7 in
67 (* H = A3&M3 | M3&nR3 | nR3&A3 *)
68 let s_tmp6 ≝ setweak_h_flag m t s_tmp5 ((A3⊗M3) ⊕ (M3⊗(⊖R3)) ⊕ ((⊖R3)⊗A3)) in
69 (* V = A7&M7&nR7 | nA7&nM7&R7 *)
70 let s_tmp7 ≝ setweak_v_flag m t s_tmp6 ((A7⊗M7⊗(⊖R7)) ⊕ ((⊖A7)⊗(⊖M7)⊗R7)) in
72 Some ? (pairT ?? s_tmp7 new_pc) ]]).
74 (* A = [true] fAM(A,M), [false] A *)
75 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
76 (* fAM e' la logica da applicare: and/xor/or *)
77 definition execute_AND_BIT_EOR_ORA_aux ≝
78 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
79 λfAM:byte8 → byte8 → byte8.
80 opt_map ?? (multi_mode_load true m t s cur_pc i)
81 (λS_M_PC.match S_M_PC with
82 [ tripleT s_tmp1 M_op new_pc ⇒
83 let R_op ≝ fAM (get_acc_8_low_reg m t s_tmp1) M_op in
84 (* A = [true] fAM(A,M), [false] A *)
85 let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
86 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
87 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
89 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
91 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
93 Some ? (pairT ?? s_tmp5 new_pc) ]).
96 (* fMC e' la logica da applicare: rc_/ro_/sh_ *)
97 definition execute_ASL_ASR_LSR_ROL_ROR_aux ≝
98 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
99 λfMC:byte8 → bool → ProdT byte8 bool.
100 opt_map ?? (multi_mode_load true m t s cur_pc i)
101 (λS_M_PC.match S_M_PC with
102 [ tripleT s_tmp1 M_op _ ⇒
103 match fMC M_op (get_c_flag m t s_tmp1) with [ pairT R_op carry ⇒
105 opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
106 (λS_PC.match S_PC with
107 [ pairT s_tmp2 new_pc ⇒
109 let s_tmp3 ≝ set_c_flag m t s_tmp2 carry in
110 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
111 let s_tmp4 ≝ set_z_flag m t s_tmp3 (eq_b8 R_op 〈x0,x0〉) in
113 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 (MSB_b8 R_op) in
115 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((MSB_b8 R_op) ⊙ carry) in
117 Some ? (pairT ?? s_tmp6 new_pc) ])]]).
119 (* estensione del segno byte → word *)
120 definition byte_extension ≝
121 λb:byte8.〈match MSB_b8 b with [ true ⇒ 〈xF,xF〉 | false ⇒ 〈x0,x0〉 ]:b〉.
123 (* branch con byte+estensione segno *)
124 definition branched_pc ≝
125 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λb:byte8.
126 get_pc_reg m t (set_pc_reg m t s (plus_w16nc cur_pc (byte_extension b))).
128 (* if COND=1 branch *)
129 (* tutti i branch calcoleranno la condizione e la passeranno qui *)
130 definition execute_any_BRANCH ≝
131 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:bool.
132 opt_map ?? (multi_mode_load true m t s cur_pc i)
133 (λS_M_PC.match S_M_PC with
134 [ tripleT s_tmp1 M_op new_pc ⇒
135 (* if true, branch *)
137 (* newpc = nextpc + rel *)
138 [ true ⇒ Some ? (pairT ?? s_tmp1 (branched_pc m t s_tmp1 new_pc M_op))
140 | false ⇒ Some ? (pairT ?? s_tmp1 new_pc) ]]).
142 (* Mn = filtered optval *)
143 (* il chiamante passa 0x00 per azzerare, 0xFF per impostare il bit di M *)
144 definition execute_BCLRn_BSETn_aux ≝
145 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λoptval:byte8.
146 (* Mn = filtered optval *)
147 opt_map ?? (multi_mode_write true m t s cur_pc i optval)
148 (λS_PC.match S_PC with
150 [ pairT s_tmp1 new_pc ⇒ Some ? (pairT ?? s_tmp1 new_pc) ]).
152 (* if COND(Mn) branch *)
153 (* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
154 definition execute_BRCLRn_BRSETn_aux ≝
155 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:byte8 → bool.
156 opt_map ?? (multi_mode_load false m t s cur_pc i)
157 (λS_M_PC.match S_M_PC with
158 [ tripleT s_tmp1 M_op new_pc ⇒ match M_op with
159 [ mk_word16 MH_op ML_op ⇒
160 (* if COND(Mn) branch *)
161 match fCOND MH_op with
162 (* newpc = nextpc + rel *)
163 [ true ⇒ Some ? (pairT ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
165 | false ⇒ Some ? (pairT ?? s_tmp1 new_pc) ]]]).
168 (* fM e' la logica da applicare: not/neg/++/-- *)
169 definition execute_COM_DEC_INC_NEG_aux ≝
170 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
171 λfM:byte8 → byte8.λfV:bool → bool → bool.λfC:bool → byte8 → bool.
172 opt_map ?? (multi_mode_load true m t s cur_pc i)
173 (λS_M_PC.match S_M_PC with
174 [ tripleT s_tmp1 M_op _ ⇒
175 let R_op ≝ fM M_op in
177 opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
178 (λS_PC.match S_PC with
179 [ pairT s_tmp2 new_pc ⇒
181 let s_tmp3 ≝ set_c_flag m t s_tmp2 (fC (get_c_flag m t s_tmp2) R_op) in
182 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
183 let s_tmp4 ≝ set_z_flag m t s_tmp3 (eq_b8 R_op 〈x0,x0〉) in
185 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 (MSB_b8 R_op) in
187 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (fV (MSB_b8 M_op) (MSB_b8 R_op)) in
189 Some ? (pairT ?? s_tmp6 new_pc) ])]).
191 (* A = [true] fAMC(A,M,C), [false] A *)
192 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
193 (* fAMC e' la logica da applicare: sottrazione con/senza carry *)
194 definition execute_SBC_SUB_aux ≝
195 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
196 λfAMC:byte8 → byte8 → bool → ProdT byte8 bool.
197 opt_map ?? (multi_mode_load true m t s cur_pc i)
198 (λS_M_PC.match S_M_PC with
199 [ tripleT s_tmp1 M_op new_pc ⇒
200 let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
201 match fAMC A_op M_op (get_c_flag m t s_tmp1) with
203 let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
204 (* A = [true] fAMC(A,M,C), [false] A *)
205 let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
206 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
207 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
208 (* C = nA7&M7 | M7&R7 | R7&nA7 *)
209 let s_tmp4 ≝ set_c_flag m t s_tmp3 (((⊖A7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖A7))) in
211 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 R7 in
212 (* V = A7&nM7&nR7 | nA7&M7&R7 *)
213 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((A7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖A7)⊗M7⊗R7)) in
215 Some ? (pairT ?? s_tmp6 new_pc) ]]).
217 (* il classico push *)
218 definition aux_push ≝
219 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
220 opt_map ?? (get_sp_reg m t s)
222 (λSP_op.opt_map ?? (memory_filter_write m t s SP_op val)
224 (λs_tmp1.opt_map ?? (set_sp_reg m t s_tmp1 (pred_w16 SP_op))
225 (λs_tmp2.Some ? s_tmp2))).
227 (* il classico pop *)
228 (* NB: l'incremento di SP deve essere filtrato dalla ALU, quindi get(set(SP)) *)
230 λm:mcu_type.λt:memory_impl.λs:any_status m t.
231 opt_map ?? (get_sp_reg m t s)
233 (λSP_op.opt_map ?? (set_sp_reg m t s (succ_w16 SP_op))
234 (λs_tmp1.opt_map ?? (get_sp_reg m t s_tmp1)
236 (λSP_op'.opt_map ?? (memory_filter_read m t s_tmp1 SP_op')
237 (λval.Some ? (pairT ?? s_tmp1 val))))).
239 (* CCR corrisponde a V11HINZC e cmq 1 se un flag non esiste *)
240 (* i flag mantengono posizione costante nelle varie ALU, e se non sono
241 implementati corrispondono a 1 *)
242 definition aux_get_CCR ≝
243 λm:mcu_type.λt:memory_impl.λs:any_status m t.
244 let V_comp ≝ match get_v_flag m t s with
245 [ None ⇒ 〈x8,x0〉 | Some V_val ⇒ match V_val with [ true ⇒ 〈x8,x0〉 | false ⇒ 〈x0,x0〉 ]] in
246 let H_comp ≝ match get_h_flag m t s with
247 [ None ⇒ 〈x1,x0〉 | Some H_val ⇒ match H_val with [ true ⇒ 〈x1,x0〉 | false ⇒ 〈x0,x0〉 ]] in
248 let I_comp ≝ match get_i_flag m t s with
249 [ None ⇒ 〈x0,x8〉 | Some I_val ⇒ match I_val with [ true ⇒ 〈x0,x8〉 | false ⇒ 〈x0,x0〉 ]] in
250 let N_comp ≝ match get_n_flag m t s with
251 [ None ⇒ 〈x0,x4〉 | Some N_val ⇒ match N_val with [ true ⇒ 〈x0,x4〉 | false ⇒ 〈x0,x0〉 ]] in
252 let Z_comp ≝ match get_z_flag m t s with
253 [ true ⇒ 〈x0,x2〉 | false ⇒ 〈x0,x0〉 ] in
254 let C_comp ≝ match get_c_flag m t s with
255 [ true ⇒ 〈x0,x1〉 | false ⇒ 〈x0,x0〉 ] in
256 or_b8 〈x6,x0〉 (or_b8 V_comp (or_b8 H_comp (or_b8 I_comp (or_b8 N_comp (or_b8 Z_comp C_comp))))).
258 (* CCR corrisponde a V11HINZC *)
259 (* i flag mantengono posizione costante nelle varie ALU, e se non sono
260 implementati si puo' usare tranquillamente setweak *)
261 definition aux_set_CCR ≝
262 λm:mcu_type.λt:memory_impl.λs:any_status m t.λCCR:byte8.
263 let s_tmp1 ≝ set_c_flag m t s (eq_b8 〈x0,x1〉 (and_b8 〈x0,x1〉 CCR)) in
264 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 〈x0,x2〉 (and_b8 〈x0,x2〉 CCR)) in
265 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (eq_b8 〈x0,x4〉 (and_b8 〈x0,x4〉 CCR)) in
266 let s_tmp4 ≝ setweak_i_flag m t s_tmp3 (eq_b8 〈x0,x8〉 (and_b8 〈x0,x8〉 CCR)) in
267 let s_tmp5 ≝ setweak_h_flag m t s_tmp4 (eq_b8 〈x1,x0〉 (and_b8 〈x1,x0〉 CCR)) in
268 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (eq_b8 〈x8,x0〉 (and_b8 〈x8,x0〉 CCR)) in
271 (* **************** *)
272 (* LOGICA DELLA ALU *)
273 (* **************** *)
276 definition execute_ADC ≝
277 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
278 execute_ADC_ADD_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8 A_op M_op C_op).
281 definition execute_ADD ≝
282 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
283 execute_ADC_ADD_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8 A_op M_op false).
285 (* SP += extended M *)
286 definition execute_AIS ≝
287 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
288 opt_map ?? (multi_mode_load true m t s cur_pc i)
289 (λS_M_PC.match S_M_PC with
290 [ tripleT s_tmp1 M_op new_pc ⇒
291 opt_map ?? (get_sp_reg m t s_tmp1)
292 (* SP += extended M *)
293 (λSP_op.opt_map ?? (set_sp_reg m t s_tmp1 (plus_w16nc SP_op (byte_extension M_op)))
294 (λs_tmp2.Some ? (pairT ?? s_tmp2 new_pc))) ]).
296 (* H:X += extended M *)
297 definition execute_AIX ≝
298 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
299 opt_map ?? (multi_mode_load true m t s cur_pc i)
300 (λS_M_PC.match S_M_PC with
301 [ tripleT s_tmp1 M_op new_pc ⇒
302 opt_map ?? (get_indX_16_reg m t s_tmp1)
303 (* H:X += extended M *)
304 (λHX_op.opt_map ?? (set_indX_16_reg m t s_tmp1 (plus_w16nc HX_op (byte_extension M_op)))
305 (λs_tmp2.Some ? (pairT ?? s_tmp2 new_pc))) ]).
308 definition execute_AND ≝
309 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
310 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true and_b8.
312 (* M = C' <- rcl M <- 0 *)
313 definition execute_ASL ≝
314 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
315 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcl_b8 M_op false).
317 (* M = M7 -> rcr M -> C' *)
318 definition execute_ASR ≝
319 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
320 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op (MSB_b8 M_op)).
323 definition execute_BCC ≝
324 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
325 execute_any_BRANCH m t s i cur_pc (⊖(get_c_flag m t s)).
328 definition execute_BCLRn ≝
329 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
330 execute_BCLRn_BSETn_aux m t s i cur_pc 〈x0,x0〉.
333 definition execute_BCS ≝
334 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
335 execute_any_BRANCH m t s i cur_pc (get_c_flag m t s).
338 definition execute_BEQ ≝
339 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
340 execute_any_BRANCH m t s i cur_pc (get_z_flag m t s).
342 (* if N⊙V=0, branch *)
343 definition execute_BGE ≝
344 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
345 opt_map ?? (get_n_flag m t s)
346 (λN_op.opt_map ?? (get_v_flag m t s)
347 (λV_op.execute_any_BRANCH m t s i cur_pc (⊖(N_op ⊙ V_op)))).
350 definition execute_BGND ≝
351 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
352 Some ? (pairT ?? s cur_pc).
354 (* if Z|N⊙V=0, branch *)
355 definition execute_BGT ≝
356 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
357 opt_map ?? (get_n_flag m t s)
358 (λN_op.opt_map ?? (get_v_flag m t s)
359 (λV_op.execute_any_BRANCH m t s i cur_pc (⊖((get_z_flag m t s) ⊕ (N_op ⊙ V_op))))).
362 definition execute_BHCC ≝
363 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
364 opt_map ?? (get_h_flag m t s)
365 (λH_op.execute_any_BRANCH m t s i cur_pc (⊖H_op)).
368 definition execute_BHCS ≝
369 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
370 opt_map ?? (get_h_flag m t s)
371 (λH_op.execute_any_BRANCH m t s i cur_pc H_op).
373 (* if C|Z=0, branch *)
374 definition execute_BHI ≝
375 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
376 execute_any_BRANCH m t s i cur_pc (⊖((get_c_flag m t s) ⊕ (get_z_flag m t s))).
378 (* if nIRQ=1, branch NB: irqflag e' un negato del pin *)
379 definition execute_BIH ≝
380 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
381 opt_map ?? (get_irq_flag m t s)
382 (λIRQ_op.execute_any_BRANCH m t s i cur_pc (⊖IRQ_op)).
384 (* if nIRQ=0, branch NB: irqflag e' un negato del pin *)
385 definition execute_BIL ≝
386 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
387 opt_map ?? (get_irq_flag m t s)
388 (λIRQ_op.execute_any_BRANCH m t s i cur_pc IRQ_op).
391 definition execute_BIT ≝
392 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
393 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc false and_b8.
395 (* if Z|N⊙V=1, branch *)
396 definition execute_BLE ≝
397 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
398 opt_map ?? (get_n_flag m t s)
399 (λN_op.opt_map ?? (get_v_flag m t s)
400 (λV_op.execute_any_BRANCH m t s i cur_pc ((get_z_flag m t s) ⊕ (N_op ⊙ V_op)))).
402 (* if C|Z=1, branch *)
403 definition execute_BLS ≝
404 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
405 execute_any_BRANCH m t s i cur_pc ((get_c_flag m t s) ⊕ (get_z_flag m t s)).
407 (* if N⊙V=1, branch *)
408 definition execute_BLT ≝
409 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
410 opt_map ?? (get_n_flag m t s)
411 (λN_op.opt_map ?? (get_v_flag m t s)
412 (λV_op.execute_any_BRANCH m t s i cur_pc (N_op ⊙ V_op))).
415 definition execute_BMC ≝
416 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
417 opt_map ?? (get_i_flag m t s)
418 (λI_op.execute_any_BRANCH m t s i cur_pc (⊖I_op)).
421 definition execute_BMI ≝
422 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
423 opt_map ?? (get_n_flag m t s)
424 (λN_op.execute_any_BRANCH m t s i cur_pc N_op).
427 definition execute_BMS ≝
428 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
429 opt_map ?? (get_i_flag m t s)
430 (λI_op.execute_any_BRANCH m t s i cur_pc I_op).
433 definition execute_BNE ≝
434 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
435 execute_any_BRANCH m t s i cur_pc (⊖(get_z_flag m t s)).
438 definition execute_BPL ≝
439 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
440 opt_map ?? (get_n_flag m t s)
441 (λN_op.execute_any_BRANCH m t s i cur_pc (⊖N_op)).
444 definition execute_BRA ≝
445 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
446 execute_any_BRANCH m t s i cur_pc true.
449 definition execute_BRCLRn ≝
450 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
451 execute_BRCLRn_BRSETn_aux m t s i cur_pc
452 (λMn_op.eq_b8 Mn_op 〈x0,x0〉).
454 (* branch never... come se fosse un nop da 2 byte *)
455 definition execute_BRN ≝
456 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
457 execute_any_BRANCH m t s i cur_pc false.
460 definition execute_BRSETn ≝
461 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
462 execute_BRCLRn_BRSETn_aux m t s i cur_pc
463 (λMn_op.⊖(eq_b8 Mn_op 〈x0,x0〉)).
466 definition execute_BSETn ≝
467 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
468 execute_BCLRn_BSETn_aux m t s i cur_pc 〈xF,xF〉.
470 (* branch to subroutine *)
471 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
472 definition execute_BSR ≝
473 λm:mcu_type.λt:memory_impl.λs:any_status m t .λi:instr_mode.λcur_pc:word16.
474 opt_map ?? (multi_mode_load true m t s cur_pc i)
475 (λS_M_PC.match S_M_PC with
476 [ tripleT s_tmp1 M_op new_pc ⇒ let aux ≝
477 (* push (new_pc low) *)
478 opt_map ?? (aux_push m t s_tmp1 (w16l new_pc))
479 (* push (new_pc high) *)
480 (λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
481 (* new_pc = new_pc + rel *)
482 (λs_tmp3.Some ? (pairT ?? s_tmp3 (branched_pc m t s_tmp3 new_pc M_op))))
484 [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
487 opt_map ?? (set_spc_reg m t s_tmp1 new_pc)
488 (* new_pc = new_pc + rel *)
489 (λs_tmp2.Some ? (pairT ?? s_tmp2 (branched_pc m t s_tmp2 new_pc M_op)))
493 definition execute_CBEQA ≝
494 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
495 opt_map ?? (multi_mode_load false m t s cur_pc i)
496 (λS_M_PC.match S_M_PC with
497 [ tripleT s_tmp1 M_op new_pc ⇒
499 [ mk_word16 MH_op ML_op ⇒
501 match eq_b8 (get_acc_8_low_reg m t s_tmp1) MH_op with
502 (* new_pc = new_pc + rel *)
503 [ true ⇒ Some ? (pairT ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
504 (* new_pc = new_pc *)
505 | false ⇒ Some ? (pairT ?? s_tmp1 new_pc)
509 definition execute_CBEQX ≝
510 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
511 opt_map ?? (multi_mode_load false m t s cur_pc i)
512 (λS_M_PC.match S_M_PC with
513 [ tripleT s_tmp1 M_op new_pc ⇒
515 [ mk_word16 MH_op ML_op ⇒
516 opt_map ?? (get_indX_8_low_reg m t s_tmp1)
518 (λX_op.match eq_b8 X_op MH_op with
519 (* new_pc = new_pc + rel *)
520 [ true ⇒ Some ? (pairT ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
521 (* new_pc = new_pc *)
522 | false ⇒ Some ? (pairT ?? s_tmp1 new_pc)
526 definition execute_CLC ≝
527 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
528 Some ? (pairT ?? (set_c_flag m t s false) cur_pc).
531 definition execute_CLI ≝
532 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
533 opt_map ?? (set_i_flag m t s false)
534 (λs_tmp.Some ? (pairT ?? s_tmp cur_pc)).
537 definition execute_CLR ≝
538 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
540 opt_map ?? (multi_mode_write true m t s cur_pc i 〈x0,x0〉)
541 (λS_PC.match S_PC with
542 [ pairT s_tmp1 new_pc ⇒
544 let s_tmp2 ≝ set_z_flag m t s_tmp1 true in
546 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 false in
548 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
550 Some ? (pairT ?? s_tmp4 new_pc) ]).
553 definition execute_CMP ≝
554 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
555 execute_SBC_SUB_aux m t s i cur_pc false (λA_op.λM_op.λC_op.plus_b8 A_op (compl_b8 M_op) false).
558 definition execute_COM ≝
559 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
560 execute_COM_DEC_INC_NEG_aux m t s i cur_pc not_b8
566 (* flags = H:X - M *)
567 definition execute_CPHX ≝
568 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
569 opt_map ?? (multi_mode_load false m t s cur_pc i)
570 (λS_M_PC.match S_M_PC with
571 [ tripleT s_tmp1 M_op new_pc ⇒
572 opt_map ?? (get_indX_16_reg m t s_tmp1)
574 match plus_w16 X_op (compl_w16 M_op) false with
576 let X15 ≝ MSB_w16 X_op in let M15 ≝ MSB_w16 M_op in let R15 ≝ MSB_w16 R_op in
577 (* Z = nR15&nR14&nR13&nR12&nR11&nR10&nR9&nR8&nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
578 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 R_op 〈〈x0,x0〉:〈x0,x0〉〉) in
579 (* C = nX15&M15 | M15&R15 | R15&nX15 *)
580 let s_tmp3 ≝ set_c_flag m t s_tmp2 (((⊖X15)⊗M15) ⊕ (M15⊗R15) ⊕ (R15⊗(⊖X15))) in
582 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 R15 in
583 (* V = X15&nM15&nR15 | nX15&M15&R15 *)
584 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X15⊗(⊖M15)⊗(⊖R15)) ⊕ ((⊖X15)⊗M15⊗R15)) in
586 Some ? (pairT ?? s_tmp5 new_pc) ] ) ]).
589 definition execute_CPX ≝
590 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
591 opt_map ?? (multi_mode_load true m t s cur_pc i)
592 (λS_M_PC.match S_M_PC with
593 [ tripleT s_tmp1 M_op new_pc ⇒
594 opt_map ?? (get_indX_8_low_reg m t s_tmp1)
596 match plus_b8 X_op (compl_b8 M_op) false with
598 let X7 ≝ MSB_b8 X_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
599 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
600 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 R_op 〈x0,x0〉) in
601 (* C = nX7&M7 | M7&R7 | R7&nX7 *)
602 let s_tmp3 ≝ set_c_flag m t s_tmp2 (((⊖X7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖X7))) in
604 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 R7 in
605 (* V = X7&nM7&nR7 | nX7&M7&R7 *)
606 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖X7)⊗M7⊗R7)) in
608 Some ? (pairT ?? s_tmp5 new_pc) ] ) ]).
610 (* decimal adjiust A *)
611 (* per i dettagli vedere daa_b8 (modulo byte8) *)
612 definition execute_DAA ≝
613 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
614 opt_map ?? (get_h_flag m t s)
616 let M_op ≝ get_acc_8_low_reg m t s in
617 match daa_b8 H (get_c_flag m t s) M_op with
620 let s_tmp1 ≝ set_acc_8_low_reg m t s R_op in
621 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
622 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 R_op 〈x0,x0〉) in
624 let s_tmp3 ≝ set_c_flag m t s_tmp2 carry in
626 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
628 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((MSB_b8 M_op) ⊙ (MSB_b8 R_op)) in
630 Some ? (pairT ?? s_tmp5 cur_pc) ]).
632 (* if (--M)≠0, branch *)
633 definition execute_DBNZ ≝
634 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
635 opt_map ?? (multi_mode_load false m t s cur_pc i)
636 (λS_M_PC.match S_M_PC with
637 [ tripleT s_tmp1 M_op new_pc ⇒
639 [ mk_word16 MH_op ML_op ⇒
641 let MH_op' ≝ pred_b8 MH_op in
642 opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i MH_op')
643 (λS_PC.match S_PC with
645 (* if (--M)≠0, branch *)
646 match eq_b8 MH_op' 〈x0,x0〉 with
647 (* new_pc = new_pc *)
648 [ true ⇒ Some ? (pairT ?? s_tmp2 new_pc)
649 (* new_pc = new_pc + rel *)
650 | false ⇒ Some ? (pairT ?? s_tmp2 (branched_pc m t s_tmp2 new_pc ML_op)) ]])]]).
653 definition execute_DEC ≝
654 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
655 execute_COM_DEC_INC_NEG_aux m t s i cur_pc pred_b8
661 (* A = H:A/X, H = H:AmodX se non c'e' overflow, altrimenti invariati *)
662 (* per i dettagli vedere div_b8 (modulo word16) *)
663 definition execute_DIV ≝
664 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
665 opt_map ?? (get_indX_8_high_reg m t s)
666 (λH_op.opt_map ?? (get_indX_8_low_reg m t s)
667 (λX_op.match div_b8 〈H_op:(get_acc_8_low_reg m t s)〉 X_op with
668 [ tripleT quoz rest overflow ⇒
670 let s_tmp1 ≝ set_c_flag m t s overflow in
672 let s_tmp2 ≝ match overflow with
674 | false ⇒ set_acc_8_low_reg m t s_tmp1 quoz ] in
675 (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
676 (* NB: che A sia cambiato o no, lo testa *)
677 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 (get_acc_8_low_reg m t s_tmp2) 〈x0,x0〉) in
678 (* H = H o H:AmodX *)
679 opt_map ?? (match overflow with
680 [ true ⇒ Some ? s_tmp3
681 | false ⇒ set_indX_8_high_reg m t s_tmp3 rest])
682 (λs_tmp4.Some ? (pairT ?? s_tmp4 cur_pc)) ])).
685 definition execute_EOR ≝
686 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
687 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true xor_b8.
690 definition execute_INC ≝
691 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
692 execute_COM_DEC_INC_NEG_aux m t s i cur_pc succ_b8
698 (* jmp, il nuovo indirizzo e' una WORD *)
699 definition execute_JMP ≝
700 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
701 opt_map ?? (multi_mode_load false m t s cur_pc i)
704 Some ? (pairT ?? (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
706 (* jump to subroutine *)
707 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
708 definition execute_JSR ≝
709 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
710 opt_map ?? (multi_mode_load false m t s cur_pc i)
711 (λS_M_PC.match S_M_PC with
712 [ tripleT s_tmp1 M_op new_pc ⇒ let aux ≝
713 (* push (new_pc low) *)
714 opt_map ?? (aux_push m t s_tmp1 (w16l new_pc))
715 (* push (new_pc high) *)
716 (λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
718 (λs_tmp3.Some ? (pairT ?? s_tmp3 M_op)))
720 [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
723 opt_map ?? (set_spc_reg m t s_tmp1 new_pc)
725 (λs_tmp2.Some ? (pairT ?? s_tmp2 M_op))
729 definition execute_LDA ≝
730 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
731 opt_map ?? (multi_mode_load true m t s cur_pc i)
732 (λS_M_PC.match S_M_PC with
733 [ tripleT s_tmp1 M_op new_pc ⇒
735 let s_tmp2 ≝ set_acc_8_low_reg m t s_tmp1 M_op in
736 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
737 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 M_op 〈x0,x0〉) in
739 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 M_op) in
741 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
743 Some ? (pairT ?? s_tmp5 new_pc) ]).
746 definition execute_LDHX ≝
747 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
748 opt_map ?? (multi_mode_load false m t s cur_pc i)
749 (λS_M_PC.match S_M_PC with
750 [ tripleT s_tmp1 M_op new_pc ⇒
751 opt_map ?? (set_indX_16_reg m t s_tmp1 M_op)
753 (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
754 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_w16 M_op 〈〈x0,x0〉:〈x0,x0〉〉) in
756 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_w16 M_op) in
758 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
760 Some ? (pairT ?? s_tmp5 new_pc)) ]).
763 definition execute_LDX ≝
764 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
765 opt_map ?? (multi_mode_load true m t s cur_pc i)
766 (λS_M_PC.match S_M_PC with
767 [ tripleT s_tmp1 M_op new_pc ⇒
768 opt_map ?? (set_indX_8_low_reg m t s_tmp1 M_op)
770 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
771 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 M_op 〈x0,x0〉) in
773 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 M_op) in
775 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
777 Some ? (pairT ?? s_tmp5 new_pc)) ]).
779 (* M = 0 -> rcr M -> C' *)
780 definition execute_LSR ≝
781 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
782 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op false).
785 definition execute_MOV ≝
786 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
788 opt_map ?? (multi_mode_load true m t s cur_pc i)
789 (λS_R_PC.match S_R_PC with
790 [ tripleT s_tmp1 R_op tmp_pc ⇒
792 opt_map ?? (multi_mode_write true m t s_tmp1 tmp_pc i R_op)
793 (λS_PC.match S_PC with
794 [ pairT s_tmp2 new_pc ⇒
795 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
796 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
798 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
800 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
802 Some ? (pairT ?? s_tmp5 new_pc)])]).
805 definition execute_MUL ≝
806 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
807 opt_map ?? (get_indX_8_low_reg m t s)
808 (λX_op.let R_op ≝ mul_b8 X_op (get_acc_8_low_reg m t s) in
809 opt_map ?? (set_indX_8_low_reg m t s (w16h R_op))
810 (λs_tmp.Some ? (pairT ?? (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
813 definition execute_NEG ≝
814 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
815 execute_COM_DEC_INC_NEG_aux m t s i cur_pc compl_b8
818 (* fC = R7|R6|R5|R4|R3|R2|R1|R0 *)
819 (λC_op.λR_op.⊖(eq_b8 R_op 〈x0,x0〉)).
822 definition execute_NOP ≝
823 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
824 Some ? (pairT ?? s cur_pc).
826 (* A = (mk_byte8 (b8l A) (b8h A)) *)
827 (* cioe' swap del nibble alto/nibble basso di A *)
828 definition execute_NSA ≝
829 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
830 match get_acc_8_low_reg m t s with [ mk_byte8 ah al ⇒
831 (* A = (mk_byte8 (b8l A) (b8h A)) *)
832 Some ? (pairT ?? (set_acc_8_low_reg m t s 〈al,ah〉) cur_pc) ].
835 definition execute_ORA ≝
836 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
837 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true or_b8.
840 definition execute_PSHA ≝
841 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
842 opt_map ?? (aux_push m t s (get_acc_8_low_reg m t s))
843 (λs_tmp1.Some ? (pairT ?? s_tmp1 cur_pc)).
846 definition execute_PSHH ≝
847 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
848 opt_map ?? (get_indX_8_high_reg m t s)
849 (λH_op.opt_map ?? (aux_push m t s H_op)
850 (λs_tmp1.Some ? (pairT ?? s_tmp1 cur_pc))).
853 definition execute_PSHX ≝
854 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
855 opt_map ?? (get_indX_8_low_reg m t s)
856 (λH_op.opt_map ?? (aux_push m t s H_op)
857 (λs_tmp1.Some ? (pairT ?? s_tmp1 cur_pc))).
860 definition execute_PULA ≝
861 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
862 opt_map ?? (aux_pop m t s)
863 (λS_and_A.match S_and_A with [ pairT s_tmp1 A_op ⇒
864 Some ? (pairT ?? (set_acc_8_low_reg m t s_tmp1 A_op) cur_pc) ]).
867 definition execute_PULH ≝
868 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
869 opt_map ?? (aux_pop m t s)
870 (λS_and_H.match S_and_H with [ pairT s_tmp1 H_op ⇒
871 opt_map ?? (set_indX_8_high_reg m t s_tmp1 H_op)
872 (λs_tmp2.Some ? (pairT ?? s_tmp2 cur_pc))]).
875 definition execute_PULX ≝
876 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
877 opt_map ?? (aux_pop m t s)
878 (λS_and_X.match S_and_X with [ pairT s_tmp1 X_op ⇒
879 opt_map ?? (set_indX_8_low_reg m t s_tmp1 X_op)
880 (λs_tmp2.Some ? (pairT ?? s_tmp2 cur_pc))]).
882 (* M = C' <- rcl M <- C *)
883 definition execute_ROL ≝
884 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
885 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcl_b8 M_op C_op).
887 (* M = C -> rcr M -> C' *)
888 definition execute_ROR ≝
889 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
890 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op C_op).
893 (* lascia inalterato il byte superiore di SP *)
894 definition execute_RSP ≝
895 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
896 opt_map ?? (get_sp_reg m t s)
897 (λSP_op.match SP_op with [ mk_word16 sph spl ⇒
898 opt_map ?? (set_sp_reg m t s 〈sph:〈xF,xF〉〉)
899 (λs_tmp.Some ? (pairT ?? s_tmp cur_pc))]).
901 (* return from interrupt *)
902 definition execute_RTI ≝
903 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
905 opt_map ?? (aux_pop m t s)
906 (λS_and_CCR.match S_and_CCR with [ pairT s_tmp1 CCR_op ⇒
907 let s_tmp2 ≝ aux_set_CCR m t s_tmp1 CCR_op in
909 opt_map ?? (aux_pop m t s_tmp2)
910 (λS_and_A.match S_and_A with [ pairT s_tmp3 A_op ⇒
911 let s_tmp4 ≝ set_acc_8_low_reg m t s_tmp3 A_op in
913 opt_map ?? (aux_pop m t s_tmp4)
914 (λS_and_X.match S_and_X with [ pairT s_tmp5 X_op ⇒
915 opt_map ?? (set_indX_8_low_reg m t s_tmp5 X_op)
917 (λs_tmp6.opt_map ?? (aux_pop m t s_tmp6)
918 (λS_and_PCH.match S_and_PCH with [ pairT s_tmp7 PCH_op ⇒
920 opt_map ?? (aux_pop m t s_tmp7)
921 (λS_and_PCL.match S_and_PCL with [ pairT s_tmp8 PCL_op ⇒
922 Some ? (pairT ?? s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
924 (* return from subroutine *)
925 (* HC05/HC08/HCS08 si appoggia allo stack, RS08 si appoggia a SPC *)
926 definition execute_RTS ≝
927 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
930 opt_map ?? (aux_pop m t s)
931 (λS_and_PCH.match S_and_PCH with [ pairT s_tmp1 PCH_op ⇒
933 opt_map ?? (aux_pop m t s_tmp1)
934 (λS_and_PCL.match S_and_PCL with [ pairT s_tmp2 PCL_op ⇒
935 Some ? (pairT ?? s_tmp2 〈PCH_op:PCL_op〉)])])
937 [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
940 opt_map ?? (get_spc_reg m t s)
941 (λSPC_op.Some ? (pairT ?? s SPC_op))
945 definition execute_SBC ≝
946 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
947 execute_SBC_SUB_aux m t s i cur_pc true
948 (λA_op.λM_op.λC_op.match plus_b8 A_op (compl_b8 M_op) false with
949 [ pairT resb resc ⇒ match C_op with
950 [ true ⇒ plus_b8 resb 〈xF,xF〉 resc
951 | false ⇒ pairT ?? resb resc ]]).
954 definition execute_SEC ≝
955 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
956 Some ? (pairT ?? (set_c_flag m t s true) cur_pc).
959 definition execute_SEI ≝
960 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
961 opt_map ?? (set_i_flag m t s true)
962 (λs_tmp.Some ? (pairT ?? s_tmp cur_pc)).
965 (* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
966 fare subroutine annidate se RA (return address) e' salvato sempre in SPC?
967 occore accedere a SPC e salvarne il contenuto *)
968 definition execute_SHA ≝
969 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
970 opt_map ?? (get_spc_reg m t s)
971 (λSPC_op.opt_map ?? (set_spc_reg m t s 〈(get_acc_8_low_reg m t s):(w16l SPC_op)〉)
972 (λs_tmp1.Some ? (pairT ?? (set_acc_8_low_reg m t s_tmp1 (w16h SPC_op)) cur_pc))).
975 (* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
976 fare subroutine annidate se RA (return address) e' salvato sempre in SPC?
977 occore accedere a SPC e salvarne il contenuto *)
978 definition execute_SLA ≝
979 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
980 opt_map ?? (get_spc_reg m t s)
981 (λSPC_op.opt_map ?? (set_spc_reg m t s 〈(w16h SPC_op):(get_acc_8_low_reg m t s)〉)
982 (λs_tmp1.Some ? (pairT ?? (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
985 definition execute_STA ≝
986 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
988 let A_op ≝ (get_acc_8_low_reg m t s) in
989 opt_map ?? (multi_mode_write true m t s cur_pc i A_op)
990 (λS_op_and_PC.match S_op_and_PC with
991 [ pairT s_tmp1 new_pc ⇒
992 (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
993 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 A_op 〈x0,x0〉) in
995 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 A_op) in
997 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
999 Some ? (pairT ?? s_tmp4 new_pc) ]).
1002 definition execute_STHX ≝
1003 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1005 opt_map ?? (get_indX_16_reg m t s)
1006 (λX_op.opt_map ?? (multi_mode_write false m t s cur_pc i X_op)
1007 (λS_op_and_PC.match S_op_and_PC with
1008 [ pairT s_tmp1 new_pc ⇒
1009 (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1010 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 X_op 〈〈x0,x0〉:〈x0,x0〉〉) in
1012 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_w16 X_op) in
1014 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
1015 (* newpc = nextpc *)
1016 Some ? (pairT ?? s_tmp4 new_pc) ])).
1019 definition execute_STOP ≝
1020 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1021 Some ? (pairT ?? (setweak_i_flag m t s false) cur_pc).
1024 definition execute_STX ≝
1025 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1027 opt_map ?? (get_indX_8_low_reg m t s)
1028 (λX_op.opt_map ?? (multi_mode_write true m t s cur_pc i X_op)
1029 (λS_op_and_PC.match S_op_and_PC with
1030 [ pairT s_tmp1 new_pc ⇒
1031 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1032 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 X_op 〈x0,x0〉) in
1034 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 X_op) in
1036 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
1037 (* newpc = nextpc *)
1038 Some ? (pairT ?? s_tmp4 new_pc) ])).
1041 definition execute_SUB ≝
1042 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1043 execute_SBC_SUB_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8 A_op (compl_b8 M_op) false).
1045 (* software interrupt *)
1046 definition execute_SWI ≝
1047 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1048 (* indirizzo da cui caricare il nuovo pc *)
1049 let vector ≝ get_pc_reg m t (set_pc_reg m t s 〈〈xF,xF〉:〈xF,xC〉〉) in
1050 (* push (cur_pc low) *)
1051 opt_map ?? (aux_push m t s (w16l cur_pc))
1052 (* push (cur_pc high *)
1053 (λs_tmp1.opt_map ?? (aux_push m t s_tmp1 (w16h cur_pc))
1054 (λs_tmp2.opt_map ?? (get_indX_8_low_reg m t s_tmp2)
1056 (λX_op.opt_map ?? (aux_push m t s_tmp2 X_op)
1058 (λs_tmp3.opt_map ?? (aux_push m t s_tmp3 (get_acc_8_low_reg m t s_tmp3))
1060 (λs_tmp4.opt_map ?? (aux_push m t s_tmp4 (aux_get_CCR m t s_tmp4))
1062 (λs_tmp5.opt_map ?? (set_i_flag m t s_tmp5 true)
1063 (* load from vector high *)
1064 (λs_tmp6.opt_map ?? (memory_filter_read m t s_tmp6 vector)
1065 (* load from vector low *)
1066 (λaddrh.opt_map ?? (memory_filter_read m t s_tmp6 (succ_w16 vector))
1067 (* newpc = [vector] *)
1068 (λaddrl.Some ? (pairT ?? s_tmp6 〈addrh:addrl〉)))))))))).
1071 definition execute_TAP ≝
1072 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1073 Some ? (pairT ?? (aux_set_CCR m t s (get_acc_8_low_reg m t s)) cur_pc).
1076 definition execute_TAX ≝
1077 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1078 opt_map ?? (set_indX_8_low_reg m t s (get_acc_8_low_reg m t s))
1079 (λs_tmp.Some ? (pairT ?? s_tmp cur_pc)).
1082 definition execute_TPA ≝
1083 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1084 Some ? (pairT ?? (set_acc_8_low_reg m t s (aux_get_CCR m t s)) cur_pc).
1087 (* implementata senza richiamare la sottrazione, la modifica dei flag
1089 definition execute_TST ≝
1090 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1091 opt_map ?? (multi_mode_load true m t s cur_pc i)
1092 (λS_M_PC.match S_M_PC with
1093 [ tripleT s_tmp1 M_op new_pc ⇒
1094 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1095 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 M_op 〈x0,x0〉) in
1097 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 M_op) in
1099 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
1100 (* newpc = nextpc *)
1101 Some ? (pairT ?? s_tmp4 new_pc) ]).
1104 definition execute_TSX ≝
1105 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1106 opt_map ?? (get_sp_reg m t s )
1107 (λSP_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 SP_op))
1109 (λs_tmp.Some ? (pairT ?? s_tmp cur_pc))).
1112 definition execute_TXA ≝
1113 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1114 opt_map ?? (get_indX_8_low_reg m t s)
1115 (λX_op.Some ? (pairT ?? (set_acc_8_low_reg m t s X_op) cur_pc)).
1118 definition execute_TXS ≝
1119 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1120 opt_map ?? (get_indX_16_reg m t s )
1121 (λX_op.opt_map ?? (set_sp_reg m t s (pred_w16 X_op))
1123 (λs_tmp.Some ? (pairT ?? s_tmp cur_pc))).
1126 definition execute_WAIT ≝
1127 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1128 Some ? (pairT ?? (setweak_i_flag m t s false) cur_pc).
1134 (* enumerazione delle possibili modalita' di sospensione *)
1135 inductive susp_type : Type ≝
1136 BGND_MODE: susp_type
1137 | STOP_MODE: susp_type
1138 | WAIT_MODE: susp_type.
1140 (* un tipo opzione ad hoc
1141 - errore: errore+stato (seguira' reset o ??, cmq lo stato non va buttato)
1142 - sospensione: sospensione+stato (seguira' resume o ??)
1145 inductive tick_result (A:Type) : Type ≝
1146 TickERR : A → error_type → tick_result A
1147 | TickSUSP : A → susp_type → tick_result A
1148 | TickOK : A → tick_result A.
1150 (* sostanazialmente simula
1151 - fetch/decode/execute
1152 - l'esecuzione e' considerata atomica quindi nel caso di un'instruzione
1153 da 3 cicli la successione sara'
1154 ([fetch/decode] s,clk:None) →
1155 ( s,clk:Some 1,pseudo,mode,3,cur_pc) →
1156 ( s,clk:Some 2,pseudo,mode,3,cur_pc) →
1157 ([execute] s',clk:None) *)
1159 definition tick_execute ≝
1160 λm:mcu_type.λt:memory_impl.λs:any_status m t.
1161 λpseudo:any_opcode m.λmode:instr_mode.λcur_pc:word16.
1162 let abs_pseudo ≝ match pseudo with [ anyOP pseudo' ⇒ pseudo' ] in
1163 let a_status_and_fetch ≝ match abs_pseudo with
1164 [ ADC ⇒ execute_ADC m t s mode cur_pc (* add with carry *)
1165 | ADD ⇒ execute_ADD m t s mode cur_pc (* add *)
1166 | AIS ⇒ execute_AIS m t s mode cur_pc (* add immediate to SP *)
1167 | AIX ⇒ execute_AIX m t s mode cur_pc (* add immediate to X *)
1168 | AND ⇒ execute_AND m t s mode cur_pc (* and *)
1169 | ASL ⇒ execute_ASL m t s mode cur_pc (* aritmetic shift left *)
1170 | ASR ⇒ execute_ASR m t s mode cur_pc (* aritmetic shift right *)
1171 | BCC ⇒ execute_BCC m t s mode cur_pc (* branch if C=0 *)
1172 | BCLRn ⇒ execute_BCLRn m t s mode cur_pc (* clear bit n *)
1173 | BCS ⇒ execute_BCS m t s mode cur_pc (* branch if C=1 *)
1174 | BEQ ⇒ execute_BEQ m t s mode cur_pc (* branch if Z=1 *)
1175 | BGE ⇒ execute_BGE m t s mode cur_pc (* branch if N⊙V=0 (great or equal) *)
1176 | BGND ⇒ execute_BGND m t s mode cur_pc (* !!background mode!!*)
1177 | BGT ⇒ execute_BGT m t s mode cur_pc (* branch if Z|N⊙V=0 clear (great) *)
1178 | BHCC ⇒ execute_BHCC m t s mode cur_pc (* branch if H=0 *)
1179 | BHCS ⇒ execute_BHCS m t s mode cur_pc (* branch if H=1 *)
1180 | BHI ⇒ execute_BHI m t s mode cur_pc (* branch if C|Z=0, (higher) *)
1181 | BIH ⇒ execute_BIH m t s mode cur_pc (* branch if nIRQ=1 *)
1182 | BIL ⇒ execute_BIL m t s mode cur_pc (* branch if nIRQ=0 *)
1183 | BIT ⇒ execute_BIT m t s mode cur_pc (* flag = and (bit test) *)
1184 | BLE ⇒ execute_BLE m t s mode cur_pc (* branch if Z|N⊙V=1 (less or equal) *)
1185 | BLS ⇒ execute_BLS m t s mode cur_pc (* branch if C|Z=1 (lower or same) *)
1186 | BLT ⇒ execute_BLT m t s mode cur_pc (* branch if N⊙1=1 (less) *)
1187 | BMC ⇒ execute_BMC m t s mode cur_pc (* branch if I=0 (interrupt mask clear) *)
1188 | BMI ⇒ execute_BMI m t s mode cur_pc (* branch if N=1 (minus) *)
1189 | BMS ⇒ execute_BMS m t s mode cur_pc (* branch if I=1 (interrupt mask set) *)
1190 | BNE ⇒ execute_BNE m t s mode cur_pc (* branch if Z=0 *)
1191 | BPL ⇒ execute_BPL m t s mode cur_pc (* branch if N=0 (plus) *)
1192 | BRA ⇒ execute_BRA m t s mode cur_pc (* branch always *)
1193 | BRCLRn ⇒ execute_BRCLRn m t s mode cur_pc (* branch if bit n clear *)
1194 | BRN ⇒ execute_BRN m t s mode cur_pc (* branch never (nop) *)
1195 | BRSETn ⇒ execute_BRSETn m t s mode cur_pc (* branch if bit n set *)
1196 | BSETn ⇒ execute_BSETn m t s mode cur_pc (* set bit n *)
1197 | BSR ⇒ execute_BSR m t s mode cur_pc (* branch to subroutine *)
1198 | CBEQA ⇒ execute_CBEQA m t s mode cur_pc (* compare (A) and BEQ *)
1199 | CBEQX ⇒ execute_CBEQX m t s mode cur_pc (* compare (X) and BEQ *)
1200 | CLC ⇒ execute_CLC m t s mode cur_pc (* C=0 *)
1201 | CLI ⇒ execute_CLI m t s mode cur_pc (* I=0 *)
1202 | CLR ⇒ execute_CLR m t s mode cur_pc (* operand=0 *)
1203 | CMP ⇒ execute_CMP m t s mode cur_pc (* flag = sub (compare A) *)
1204 | COM ⇒ execute_COM m t s mode cur_pc (* not (1 complement) *)
1205 | CPHX ⇒ execute_CPHX m t s mode cur_pc (* flag = sub (compare H:X) *)
1206 | CPX ⇒ execute_CPX m t s mode cur_pc (* flag = sub (compare X) *)
1207 | DAA ⇒ execute_DAA m t s mode cur_pc (* decimal adjust A *)
1208 | DBNZ ⇒ execute_DBNZ m t s mode cur_pc (* dec and BNE *)
1209 | DEC ⇒ execute_DEC m t s mode cur_pc (* operand=operand-1 (decrement) *)
1210 | DIV ⇒ execute_DIV m t s mode cur_pc (* div *)
1211 | EOR ⇒ execute_EOR m t s mode cur_pc (* xor *)
1212 | INC ⇒ execute_INC m t s mode cur_pc (* operand=operand+1 (increment) *)
1213 | JMP ⇒ execute_JMP m t s mode cur_pc (* jmp word [operand] *)
1214 | JSR ⇒ execute_JSR m t s mode cur_pc (* jmp to subroutine *)
1215 | LDA ⇒ execute_LDA m t s mode cur_pc (* load in A *)
1216 | LDHX ⇒ execute_LDHX m t s mode cur_pc (* load in H:X *)
1217 | LDX ⇒ execute_LDX m t s mode cur_pc (* load in X *)
1218 | LSR ⇒ execute_LSR m t s mode cur_pc (* logical shift right *)
1219 | MOV ⇒ execute_MOV m t s mode cur_pc (* move *)
1220 | MUL ⇒ execute_MUL m t s mode cur_pc (* mul *)
1221 | NEG ⇒ execute_NEG m t s mode cur_pc (* neg (2 complement) *)
1222 | NOP ⇒ execute_NOP m t s mode cur_pc (* nop *)
1223 | NSA ⇒ execute_NSA m t s mode cur_pc (* nibble swap A (al:ah <- ah:al) *)
1224 | ORA ⇒ execute_ORA m t s mode cur_pc (* or *)
1225 | PSHA ⇒ execute_PSHA m t s mode cur_pc (* push A *)
1226 | PSHH ⇒ execute_PSHH m t s mode cur_pc (* push H *)
1227 | PSHX ⇒ execute_PSHX m t s mode cur_pc (* push X *)
1228 | PULA ⇒ execute_PULA m t s mode cur_pc (* pop A *)
1229 | PULH ⇒ execute_PULH m t s mode cur_pc (* pop H *)
1230 | PULX ⇒ execute_PULX m t s mode cur_pc (* pop X *)
1231 | ROL ⇒ execute_ROL m t s mode cur_pc (* rotate left *)
1232 | ROR ⇒ execute_ROR m t s mode cur_pc (* rotate right *)
1233 | RSP ⇒ execute_RSP m t s mode cur_pc (* reset SP (0x00FF) *)
1234 | RTI ⇒ execute_RTI m t s mode cur_pc (* return from interrupt *)
1235 | RTS ⇒ execute_RTS m t s mode cur_pc (* return from subroutine *)
1236 | SBC ⇒ execute_SBC m t s mode cur_pc (* sub with carry*)
1237 | SEC ⇒ execute_SEC m t s mode cur_pc (* C=1 *)
1238 | SEI ⇒ execute_SEI m t s mode cur_pc (* I=1 *)
1239 | SHA ⇒ execute_SHA m t s mode cur_pc (* swap spc_high,A *)
1240 | SLA ⇒ execute_SLA m t s mode cur_pc (* swap spc_low,A *)
1241 | STA ⇒ execute_STA m t s mode cur_pc (* store from A *)
1242 | STHX ⇒ execute_STHX m t s mode cur_pc (* store from H:X *)
1243 | STOP ⇒ execute_STOP m t s mode cur_pc (* !!stop mode!! *)
1244 | STX ⇒ execute_STX m t s mode cur_pc (* store from X *)
1245 | SUB ⇒ execute_SUB m t s mode cur_pc (* sub *)
1246 | SWI ⇒ execute_SWI m t s mode cur_pc (* software interrupt *)
1247 | TAP ⇒ execute_TAP m t s mode cur_pc (* flag=A (transfer A to process status byte *)
1248 | TAX ⇒ execute_TAX m t s mode cur_pc (* X=A (transfer A to X) *)
1249 | TPA ⇒ execute_TPA m t s mode cur_pc (* A=flag (transfer process status byte to A) *)
1250 | TST ⇒ execute_TST m t s mode cur_pc (* flag = sub (test) *)
1251 | TSX ⇒ execute_TSX m t s mode cur_pc (* X:H=SP (transfer SP to H:X) *)
1252 | TXA ⇒ execute_TXA m t s mode cur_pc (* A=X (transfer X to A) *)
1253 | TXS ⇒ execute_TXS m t s mode cur_pc (* SP=X:H (transfer H:X to SP) *)
1254 | WAIT ⇒ execute_WAIT m t s mode cur_pc (* !!wait mode!!*)
1255 ] in match a_status_and_fetch with
1256 (* errore nell'execute (=caricamento argomenti)? riportato in output *)
1257 (* nessun avanzamento e clk a None *)
1258 [ None ⇒ TickERR ? (set_clk_desc m t s (None ?)) ILL_EX_AD
1259 | Some status_and_newpc ⇒
1260 (* aggiornamento centralizzato di pc e clk *)
1261 match status_and_newpc with
1262 [ pairT s_tmp1 new_pc ⇒
1263 let s_tmp2 ≝ set_pc_reg m t s_tmp1 new_pc in
1264 let s_tmp3 ≝ set_clk_desc m t s_tmp2 (None ?) in
1265 let abs_magic ≝ magic_of_opcode abs_pseudo in
1266 (* distinzione fra le 4 modalita' possibili, normale/BGND/STOP/WAIT *)
1267 match eq_b8 abs_magic (magic_of_opcode BGND) with
1268 [ true ⇒ TickSUSP ? s_tmp3 BGND_MODE
1269 | false ⇒ match eq_b8 abs_magic (magic_of_opcode STOP) with
1270 [ true ⇒ TickSUSP ? s_tmp3 STOP_MODE
1271 | false ⇒ match eq_b8 abs_magic (magic_of_opcode WAIT) with
1272 [ true ⇒ TickSUSP ? s_tmp3 WAIT_MODE
1273 | false ⇒ TickOK ? s_tmp3
1277 λm:mcu_type.λt:memory_impl.λs:any_status m t.
1278 let opt_info ≝ get_clk_desc m t s in
1280 (* e' il momento del fetch *)
1281 [ None ⇒ match fetch m t s with
1282 (* errore nel fetch/decode? riportato in output, nessun avanzamento *)
1283 [ FetchERR err ⇒ TickERR ? s err
1284 (* nessun errore nel fetch *)
1285 | FetchOK fetch_info cur_pc ⇒ match fetch_info with
1286 [ quadrupleT pseudo mode _ tot_clk ⇒
1287 match eq_b8 〈x0,x1〉 tot_clk with
1288 (* un solo clk, execute subito *)
1289 [ true ⇒ tick_execute m t s pseudo mode cur_pc
1290 (* piu' clk, execute rimandata *)
1291 | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintupleT ????? 〈x0,x1〉 pseudo mode tot_clk cur_pc)))
1295 (* il fetch e' gia' stato eseguito, e' il turno di execute? *)
1296 | Some info ⇒ match info with [ quintupleT cur_clk pseudo mode tot_clk cur_pc ⇒
1297 match eq_b8 (succ_b8 cur_clk) tot_clk with
1299 [ true ⇒ tick_execute m t s pseudo mode cur_pc
1300 (* no, avanzamento cur_clk *)
1301 | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintupleT ????? (succ_b8 cur_clk) pseudo mode tot_clk cur_pc)))
1310 let rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
1312 [ TickERR s' error ⇒ TickERR ? s' error
1313 | TickSUSP s' susp ⇒ TickSUSP ? s' susp
1314 | TickOK s' ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ]
1318 ∀m,u,s,n1,n2. execute m u s (n1 + n2) = execute m u (execute m u s n1) n2.
1320 generalize in match s; clear s;