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 include "freescale/load_write.ma".
29 (* ************************************************ *)
30 (* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *)
31 (* ************************************************ *)
33 (* NB: dentro il codice i commenti cercano di spiegare la logica
34 secondo quanto riportato dalle specifiche delle mcu *)
36 (* NB: notare che tranne nei casi in cui PC viene modificato esplicitamente
37 il suo avanzamento viene delegato totalmente agli strati inferiori
38 I) avanzamento dovuto al decode degli op (fetch)
39 II) avanzamento dovuto al caricamento degli argomenti (multi_mode_load/write)
40 la modifica effettiva avviene poi centralizzata in tick *)
42 (* A = [true] fAMC(A,M,C), [false] A *)
43 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
44 (* fAMC e' la logica da applicare: somma con/senza carry *)
45 definition execute_ADC_ADD_aux ≝
46 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
47 λfAMC:byte8 → byte8 → bool → Prod byte8 bool.
48 opt_map ?? (multi_mode_load m t true s cur_pc i)
49 (λS_M_PC.match S_M_PC with
50 [ tripleT s_tmp1 M_op new_pc ⇒
51 let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
52 match fAMC A_op M_op (get_c_flag m t s_tmp1) with
54 let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
55 let A3 ≝ MSB_ex (b8l A_op) in let M3 ≝ MSB_ex (b8l M_op) in let R3 ≝ MSB_ex (b8l R_op) in
56 (* A = [true] fAMC(A,M,C), [false] A *)
57 let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
58 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
59 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
60 (* C = A7&M7 | M7&nR7 | nR7&A7 *)
61 let s_tmp4 ≝ set_c_flag m t s_tmp3 ((A7⊗M7) ⊕ (M7⊗(⊖R7)) ⊕ ((⊖R7)⊗A7)) in
63 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 R7 in
64 (* H = A3&M3 | M3&nR3 | nR3&A3 *)
65 let s_tmp6 ≝ setweak_h_flag m t s_tmp5 ((A3⊗M3) ⊕ (M3⊗(⊖R3)) ⊕ ((⊖R3)⊗A3)) in
66 (* V = A7&M7&nR7 | nA7&nM7&R7 *)
67 let s_tmp7 ≝ setweak_v_flag m t s_tmp6 ((A7⊗M7⊗(⊖R7)) ⊕ ((⊖A7)⊗(⊖M7)⊗R7)) in
69 Some ? (pair ?? s_tmp7 new_pc) ]]).
71 (* A = [true] fAM(A,M), [false] A *)
72 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
73 (* fAM e' la logica da applicare: and/xor/or *)
74 definition execute_AND_BIT_EOR_ORA_aux ≝
75 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
76 λfAM:byte8 → byte8 → byte8.
77 opt_map ?? (multi_mode_load m t true s cur_pc i)
78 (λS_M_PC.match S_M_PC with
79 [ tripleT s_tmp1 M_op new_pc ⇒
80 let R_op ≝ fAM (get_acc_8_low_reg m t s_tmp1) M_op in
81 (* A = [true] fAM(A,M), [false] A *)
82 let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
83 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
84 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
86 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
88 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
90 Some ? (pair ?? s_tmp5 new_pc) ]).
93 (* fMC e' la logica da applicare: rc_/ro_/sh_ *)
94 definition execute_ASL_ASR_LSR_ROL_ROR_aux ≝
95 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
96 λfMC:byte8 → bool → Prod byte8 bool.
97 opt_map ?? (multi_mode_load m t true s cur_pc i)
98 (λS_M_PC.match S_M_PC with
99 [ tripleT s_tmp1 M_op _ ⇒
100 match fMC M_op (get_c_flag m t s_tmp1) with [ pair R_op carry ⇒
102 opt_map ?? (multi_mode_write m t true s_tmp1 cur_pc i R_op)
103 (λS_PC.match S_PC with
104 [ pair s_tmp2 new_pc ⇒
106 let s_tmp3 ≝ set_c_flag m t s_tmp2 carry in
107 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
108 let s_tmp4 ≝ set_z_flag m t s_tmp3 (eq_b8 R_op 〈x0,x0〉) in
110 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 (MSB_b8 R_op) in
112 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((MSB_b8 R_op) ⊙ carry) in
114 Some ? (pair ?? s_tmp6 new_pc) ])]]).
116 (* estensione del segno byte → word *)
117 definition byte_extension ≝
118 λb:byte8.〈match MSB_b8 b with [ true ⇒ 〈xF,xF〉 | false ⇒ 〈x0,x0〉 ]:b〉.
120 (* branch con byte+estensione segno *)
121 definition branched_pc ≝
122 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λb:byte8.
123 get_pc_reg m t (set_pc_reg m t s (plus_w16nc cur_pc (byte_extension b))).
125 (* if COND=1 branch *)
126 (* tutti i branch calcoleranno la condizione e la passeranno qui *)
127 definition execute_any_BRANCH ≝
128 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:bool.
129 opt_map ?? (multi_mode_load m t true s cur_pc i)
130 (λS_M_PC.match S_M_PC with
131 [ tripleT s_tmp1 M_op new_pc ⇒
132 (* if true, branch *)
134 (* newpc = nextpc + rel *)
135 [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc M_op))
137 | false ⇒ Some ? (pair ?? s_tmp1 new_pc) ]]).
139 (* Mn = filtered optval *)
140 (* il chiamante passa 0x00 per azzerare, 0xFF per impostare il bit di M *)
141 definition execute_BCLRn_BSETn_aux ≝
142 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λoptval:byte8.
143 (* Mn = filtered optval *)
144 opt_map ?? (multi_mode_write m t true s cur_pc i optval)
145 (λS_PC.match S_PC with
147 [ pair s_tmp1 new_pc ⇒ Some ? (pair ?? s_tmp1 new_pc) ]).
149 (* if COND(Mn) branch *)
150 (* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
151 definition execute_BRCLRn_BRSETn_aux ≝
152 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:byte8 → bool.
153 opt_map ?? (multi_mode_load m t false s cur_pc i)
154 (λS_M_PC.match S_M_PC with
155 [ tripleT s_tmp1 M_op new_pc ⇒ match M_op with
156 [ mk_word16 MH_op ML_op ⇒
157 (* if COND(Mn) branch *)
158 match fCOND MH_op with
159 (* newpc = nextpc + rel *)
160 [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
162 | false ⇒ Some ? (pair ?? s_tmp1 new_pc) ]]]).
165 (* fM e' la logica da applicare: not/neg/++/-- *)
166 definition execute_COM_DEC_INC_NEG_aux ≝
167 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
168 λfM:byte8 → byte8.λfV:bool → bool → bool.λfC:bool → byte8 → bool.
169 opt_map ?? (multi_mode_load m t true s cur_pc i)
170 (λS_M_PC.match S_M_PC with
171 [ tripleT s_tmp1 M_op _ ⇒
172 let R_op ≝ fM M_op in
174 opt_map ?? (multi_mode_write m t true s_tmp1 cur_pc i R_op)
175 (λS_PC.match S_PC with
176 [ pair s_tmp2 new_pc ⇒
178 let s_tmp3 ≝ set_c_flag m t s_tmp2 (fC (get_c_flag m t s_tmp2) R_op) in
179 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
180 let s_tmp4 ≝ set_z_flag m t s_tmp3 (eq_b8 R_op 〈x0,x0〉) in
182 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 (MSB_b8 R_op) in
184 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (fV (MSB_b8 M_op) (MSB_b8 R_op)) in
186 Some ? (pair ?? s_tmp6 new_pc) ])]).
188 (* A = [true] fAMC(A,M,C), [false] A *)
189 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
190 (* fAMC e' la logica da applicare: sottrazione con/senza carry *)
191 definition execute_SBC_SUB_aux ≝
192 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
193 λfAMC:byte8 → byte8 → bool → Prod byte8 bool.
194 opt_map ?? (multi_mode_load m t true s cur_pc i)
195 (λS_M_PC.match S_M_PC with
196 [ tripleT s_tmp1 M_op new_pc ⇒
197 let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
198 match fAMC A_op M_op (get_c_flag m t s_tmp1) with
200 let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
201 (* A = [true] fAMC(A,M,C), [false] A *)
202 let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
203 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
204 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
205 (* C = nA7&M7 | M7&R7 | R7&nA7 *)
206 let s_tmp4 ≝ set_c_flag m t s_tmp3 (((⊖A7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖A7))) in
208 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 R7 in
209 (* V = A7&nM7&nR7 | nA7&M7&R7 *)
210 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((A7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖A7)⊗M7⊗R7)) in
212 Some ? (pair ?? s_tmp6 new_pc) ]]).
214 (* il classico push *)
215 definition aux_push ≝
216 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
217 opt_map ?? (get_sp_reg m t s)
219 (λSP_op.opt_map ?? (memory_filter_write m t s SP_op val)
221 (λs_tmp1.opt_map ?? (set_sp_reg m t s_tmp1 (pred_w16 SP_op))
222 (λs_tmp2.Some ? s_tmp2))).
224 (* il classico pop *)
225 (* NB: l'incremento di SP deve essere filtrato dalla ALU, quindi get(set(SP)) *)
227 λm:mcu_type.λt:memory_impl.λs:any_status m t.
228 opt_map ?? (get_sp_reg m t s)
230 (λSP_op.opt_map ?? (set_sp_reg m t s (succ_w16 SP_op))
231 (λs_tmp1.opt_map ?? (get_sp_reg m t s_tmp1)
233 (λSP_op'.opt_map ?? (memory_filter_read m t s_tmp1 SP_op')
234 (λval.Some ? (pair ?? s_tmp1 val))))).
236 (* CCR corrisponde a V11HINZC e cmq 1 se un flag non esiste *)
237 (* i flag mantengono posizione costante nelle varie ALU, e se non sono
238 implementati corrispondono a 1 *)
239 definition aux_get_CCR ≝
240 λm:mcu_type.λt:memory_impl.λs:any_status m t.
241 let V_comp ≝ match get_v_flag m t s with
242 [ None ⇒ 〈x8,x0〉 | Some V_val ⇒ match V_val with [ true ⇒ 〈x8,x0〉 | false ⇒ 〈x0,x0〉 ]] in
243 let H_comp ≝ match get_h_flag m t s with
244 [ None ⇒ 〈x1,x0〉 | Some H_val ⇒ match H_val with [ true ⇒ 〈x1,x0〉 | false ⇒ 〈x0,x0〉 ]] in
245 let I_comp ≝ match get_i_flag m t s with
246 [ None ⇒ 〈x0,x8〉 | Some I_val ⇒ match I_val with [ true ⇒ 〈x0,x8〉 | false ⇒ 〈x0,x0〉 ]] in
247 let N_comp ≝ match get_n_flag m t s with
248 [ None ⇒ 〈x0,x4〉 | Some N_val ⇒ match N_val with [ true ⇒ 〈x0,x4〉 | false ⇒ 〈x0,x0〉 ]] in
249 let Z_comp ≝ match get_z_flag m t s with
250 [ true ⇒ 〈x0,x2〉 | false ⇒ 〈x0,x0〉 ] in
251 let C_comp ≝ match get_c_flag m t s with
252 [ true ⇒ 〈x0,x1〉 | false ⇒ 〈x0,x0〉 ] in
253 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))))).
255 (* CCR corrisponde a V11HINZC *)
256 (* i flag mantengono posizione costante nelle varie ALU, e se non sono
257 implementati si puo' usare tranquillamente setweak *)
258 definition aux_set_CCR ≝
259 λm:mcu_type.λt:memory_impl.λs:any_status m t.λCCR:byte8.
260 let s_tmp1 ≝ set_c_flag m t s (eq_b8 〈x0,x1〉 (and_b8 〈x0,x1〉 CCR)) in
261 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 〈x0,x2〉 (and_b8 〈x0,x2〉 CCR)) in
262 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (eq_b8 〈x0,x4〉 (and_b8 〈x0,x4〉 CCR)) in
263 let s_tmp4 ≝ setweak_i_flag m t s_tmp3 (eq_b8 〈x0,x8〉 (and_b8 〈x0,x8〉 CCR)) in
264 let s_tmp5 ≝ setweak_h_flag m t s_tmp4 (eq_b8 〈x1,x0〉 (and_b8 〈x1,x0〉 CCR)) in
265 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (eq_b8 〈x8,x0〉 (and_b8 〈x8,x0〉 CCR)) in
268 (* **************** *)
269 (* LOGICA DELLA ALU *)
270 (* **************** *)
273 definition execute_ADC ≝
274 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
275 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).
278 definition execute_ADD ≝
279 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
280 execute_ADC_ADD_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8 A_op M_op false).
282 (* SP += extended M *)
283 definition execute_AIS ≝
284 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
285 opt_map ?? (multi_mode_load m t true s cur_pc i)
286 (λS_M_PC.match S_M_PC with
287 [ tripleT s_tmp1 M_op new_pc ⇒
288 opt_map ?? (get_sp_reg m t s_tmp1)
289 (* SP += extended M *)
290 (λSP_op.opt_map ?? (set_sp_reg m t s_tmp1 (plus_w16nc SP_op (byte_extension M_op)))
291 (λs_tmp2.Some ? (pair ?? s_tmp2 new_pc))) ]).
293 (* H:X += extended M *)
294 definition execute_AIX ≝
295 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
296 opt_map ?? (multi_mode_load m t true s cur_pc i)
297 (λS_M_PC.match S_M_PC with
298 [ tripleT s_tmp1 M_op new_pc ⇒
299 opt_map ?? (get_indX_16_reg m t s_tmp1)
300 (* H:X += extended M *)
301 (λHX_op.opt_map ?? (set_indX_16_reg m t s_tmp1 (plus_w16nc HX_op (byte_extension M_op)))
302 (λs_tmp2.Some ? (pair ?? s_tmp2 new_pc))) ]).
305 definition execute_AND ≝
306 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
307 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true and_b8.
309 (* M = C' <- rcl M <- 0 *)
310 definition execute_ASL ≝
311 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
312 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcl_b8 M_op false).
314 (* M = M7 -> rcr M -> C' *)
315 definition execute_ASR ≝
316 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
317 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)).
320 definition execute_BCC ≝
321 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
322 execute_any_BRANCH m t s i cur_pc (⊖(get_c_flag m t s)).
325 definition execute_BCLRn ≝
326 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
327 execute_BCLRn_BSETn_aux m t s i cur_pc 〈x0,x0〉.
330 definition execute_BCS ≝
331 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
332 execute_any_BRANCH m t s i cur_pc (get_c_flag m t s).
335 definition execute_BEQ ≝
336 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
337 execute_any_BRANCH m t s i cur_pc (get_z_flag m t s).
339 (* if N⊙V=0, branch *)
340 definition execute_BGE ≝
341 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
342 opt_map ?? (get_n_flag m t s)
343 (λN_op.opt_map ?? (get_v_flag m t s)
344 (λV_op.execute_any_BRANCH m t s i cur_pc (⊖(N_op ⊙ V_op)))).
347 definition execute_BGND ≝
348 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
349 Some ? (pair ?? s cur_pc).
351 (* if Z|N⊙V=0, branch *)
352 definition execute_BGT ≝
353 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
354 opt_map ?? (get_n_flag m t s)
355 (λN_op.opt_map ?? (get_v_flag m t s)
356 (λV_op.execute_any_BRANCH m t s i cur_pc (⊖((get_z_flag m t s) ⊕ (N_op ⊙ V_op))))).
359 definition execute_BHCC ≝
360 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
361 opt_map ?? (get_h_flag m t s)
362 (λH_op.execute_any_BRANCH m t s i cur_pc (⊖H_op)).
365 definition execute_BHCS ≝
366 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
367 opt_map ?? (get_h_flag m t s)
368 (λH_op.execute_any_BRANCH m t s i cur_pc H_op).
370 (* if C|Z=0, branch *)
371 definition execute_BHI ≝
372 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
373 execute_any_BRANCH m t s i cur_pc (⊖((get_c_flag m t s) ⊕ (get_z_flag m t s))).
375 (* if nIRQ=1, branch NB: irqflag e' un negato del pin *)
376 definition execute_BIH ≝
377 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
378 opt_map ?? (get_irq_flag m t s)
379 (λIRQ_op.execute_any_BRANCH m t s i cur_pc (⊖IRQ_op)).
381 (* if nIRQ=0, branch NB: irqflag e' un negato del pin *)
382 definition execute_BIL ≝
383 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
384 opt_map ?? (get_irq_flag m t s)
385 (λIRQ_op.execute_any_BRANCH m t s i cur_pc IRQ_op).
388 definition execute_BIT ≝
389 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
390 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc false and_b8.
392 (* if Z|N⊙V=1, branch *)
393 definition execute_BLE ≝
394 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
395 opt_map ?? (get_n_flag m t s)
396 (λN_op.opt_map ?? (get_v_flag m t s)
397 (λV_op.execute_any_BRANCH m t s i cur_pc ((get_z_flag m t s) ⊕ (N_op ⊙ V_op)))).
399 (* if C|Z=1, branch *)
400 definition execute_BLS ≝
401 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
402 execute_any_BRANCH m t s i cur_pc ((get_c_flag m t s) ⊕ (get_z_flag m t s)).
404 (* if N⊙V=1, branch *)
405 definition execute_BLT ≝
406 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
407 opt_map ?? (get_n_flag m t s)
408 (λN_op.opt_map ?? (get_v_flag m t s)
409 (λV_op.execute_any_BRANCH m t s i cur_pc (N_op ⊙ V_op))).
412 definition execute_BMC ≝
413 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
414 opt_map ?? (get_i_flag m t s)
415 (λI_op.execute_any_BRANCH m t s i cur_pc (⊖I_op)).
418 definition execute_BMI ≝
419 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
420 opt_map ?? (get_n_flag m t s)
421 (λN_op.execute_any_BRANCH m t s i cur_pc N_op).
424 definition execute_BMS ≝
425 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
426 opt_map ?? (get_i_flag m t s)
427 (λI_op.execute_any_BRANCH m t s i cur_pc I_op).
430 definition execute_BNE ≝
431 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
432 execute_any_BRANCH m t s i cur_pc (⊖(get_z_flag m t s)).
435 definition execute_BPL ≝
436 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
437 opt_map ?? (get_n_flag m t s)
438 (λN_op.execute_any_BRANCH m t s i cur_pc (⊖N_op)).
441 definition execute_BRA ≝
442 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
443 execute_any_BRANCH m t s i cur_pc true.
446 definition execute_BRCLRn ≝
447 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
448 execute_BRCLRn_BRSETn_aux m t s i cur_pc
449 (λMn_op.eq_b8 Mn_op 〈x0,x0〉).
451 (* branch never... come se fosse un nop da 2 byte *)
452 definition execute_BRN ≝
453 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
454 execute_any_BRANCH m t s i cur_pc false.
457 definition execute_BRSETn ≝
458 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
459 execute_BRCLRn_BRSETn_aux m t s i cur_pc
460 (λMn_op.⊖(eq_b8 Mn_op 〈x0,x0〉)).
463 definition execute_BSETn ≝
464 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
465 execute_BCLRn_BSETn_aux m t s i cur_pc 〈xF,xF〉.
467 (* branch to subroutine *)
468 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
469 definition execute_BSR ≝
470 λm:mcu_type.λt:memory_impl.λs:any_status m t .λi:instr_mode.λcur_pc:word16.
471 opt_map ?? (multi_mode_load m t true s cur_pc i)
472 (λS_M_PC.match S_M_PC with
473 [ tripleT s_tmp1 M_op new_pc ⇒ let aux ≝
474 (* push (new_pc low) *)
475 opt_map ?? (aux_push m t s_tmp1 (w16l new_pc))
476 (* push (new_pc high) *)
477 (λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
478 (* new_pc = new_pc + rel *)
479 (λs_tmp3.Some ? (pair ?? s_tmp3 (branched_pc m t s_tmp3 new_pc M_op))))
481 [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
484 opt_map ?? (set_spc_reg m t s_tmp1 new_pc)
485 (* new_pc = new_pc + rel *)
486 (λs_tmp2.Some ? (pair ?? s_tmp2 (branched_pc m t s_tmp2 new_pc M_op)))
490 definition execute_CBEQA ≝
491 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
492 opt_map ?? (multi_mode_load m t false s cur_pc i)
493 (λS_M_PC.match S_M_PC with
494 [ tripleT s_tmp1 M_op new_pc ⇒
496 [ mk_word16 MH_op ML_op ⇒
498 match eq_b8 (get_acc_8_low_reg m t s_tmp1) MH_op with
499 (* new_pc = new_pc + rel *)
500 [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
501 (* new_pc = new_pc *)
502 | false ⇒ Some ? (pair ?? s_tmp1 new_pc)
506 definition execute_CBEQX ≝
507 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
508 opt_map ?? (multi_mode_load m t false s cur_pc i)
509 (λS_M_PC.match S_M_PC with
510 [ tripleT s_tmp1 M_op new_pc ⇒
512 [ mk_word16 MH_op ML_op ⇒
513 opt_map ?? (get_indX_8_low_reg m t s_tmp1)
515 (λX_op.match eq_b8 X_op MH_op with
516 (* new_pc = new_pc + rel *)
517 [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
518 (* new_pc = new_pc *)
519 | false ⇒ Some ? (pair ?? s_tmp1 new_pc)
523 definition execute_CLC ≝
524 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
525 Some ? (pair ?? (set_c_flag m t s false) cur_pc).
528 definition execute_CLI ≝
529 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
530 opt_map ?? (set_i_flag m t s false)
531 (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
534 definition execute_CLR ≝
535 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
537 opt_map ?? (multi_mode_write m t true s cur_pc i 〈x0,x0〉)
538 (λS_PC.match S_PC with
539 [ pair s_tmp1 new_pc ⇒
541 let s_tmp2 ≝ set_z_flag m t s_tmp1 true in
543 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 false in
545 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
547 Some ? (pair ?? s_tmp4 new_pc) ]).
550 definition execute_CMP ≝
551 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
552 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).
555 definition execute_COM ≝
556 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
557 execute_COM_DEC_INC_NEG_aux m t s i cur_pc not_b8
563 (* flags = H:X - M *)
564 definition execute_CPHX ≝
565 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
566 opt_map ?? (multi_mode_load m t false s cur_pc i)
567 (λS_M_PC.match S_M_PC with
568 [ tripleT s_tmp1 M_op new_pc ⇒
569 opt_map ?? (get_indX_16_reg m t s_tmp1)
571 match plus_w16 X_op (compl_w16 M_op) false with
573 let X15 ≝ MSB_w16 X_op in let M15 ≝ MSB_w16 M_op in let R15 ≝ MSB_w16 R_op in
574 (* Z = nR15&nR14&nR13&nR12&nR11&nR10&nR9&nR8&nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
575 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 R_op 〈〈x0,x0〉:〈x0,x0〉〉) in
576 (* C = nX15&M15 | M15&R15 | R15&nX15 *)
577 let s_tmp3 ≝ set_c_flag m t s_tmp2 (((⊖X15)⊗M15) ⊕ (M15⊗R15) ⊕ (R15⊗(⊖X15))) in
579 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 R15 in
580 (* V = X15&nM15&nR15 | nX15&M15&R15 *)
581 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X15⊗(⊖M15)⊗(⊖R15)) ⊕ ((⊖X15)⊗M15⊗R15)) in
583 Some ? (pair ?? s_tmp5 new_pc) ] ) ]).
586 definition execute_CPX ≝
587 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
588 opt_map ?? (multi_mode_load m t true s cur_pc i)
589 (λS_M_PC.match S_M_PC with
590 [ tripleT s_tmp1 M_op new_pc ⇒
591 opt_map ?? (get_indX_8_low_reg m t s_tmp1)
593 match plus_b8 X_op (compl_b8 M_op) false with
595 let X7 ≝ MSB_b8 X_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
596 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
597 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 R_op 〈x0,x0〉) in
598 (* C = nX7&M7 | M7&R7 | R7&nX7 *)
599 let s_tmp3 ≝ set_c_flag m t s_tmp2 (((⊖X7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖X7))) in
601 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 R7 in
602 (* V = X7&nM7&nR7 | nX7&M7&R7 *)
603 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖X7)⊗M7⊗R7)) in
605 Some ? (pair ?? s_tmp5 new_pc) ] ) ]).
607 (* decimal adjiust A *)
608 (* per i dettagli vedere daa_b8 (modulo byte8) *)
609 definition execute_DAA ≝
610 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
611 opt_map ?? (get_h_flag m t s)
613 let M_op ≝ get_acc_8_low_reg m t s in
614 match daa_b8 H (get_c_flag m t s) M_op with
617 let s_tmp1 ≝ set_acc_8_low_reg m t s R_op in
618 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
619 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 R_op 〈x0,x0〉) in
621 let s_tmp3 ≝ set_c_flag m t s_tmp2 carry in
623 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
625 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((MSB_b8 M_op) ⊙ (MSB_b8 R_op)) in
627 Some ? (pair ?? s_tmp5 cur_pc) ]).
629 (* if (--M)≠0, branch *)
630 definition execute_DBNZ ≝
631 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
632 opt_map ?? (multi_mode_load m t false s cur_pc i)
633 (λS_M_PC.match S_M_PC with
634 [ tripleT s_tmp1 M_op new_pc ⇒
636 [ mk_word16 MH_op ML_op ⇒
638 let MH_op' ≝ pred_b8 MH_op in
639 opt_map ?? (multi_mode_write m t true s_tmp1 cur_pc i MH_op')
640 (λS_PC.match S_PC with
642 (* if (--M)≠0, branch *)
643 match eq_b8 MH_op' 〈x0,x0〉 with
644 (* new_pc = new_pc *)
645 [ true ⇒ Some ? (pair ?? s_tmp2 new_pc)
646 (* new_pc = new_pc + rel *)
647 | false ⇒ Some ? (pair ?? s_tmp2 (branched_pc m t s_tmp2 new_pc ML_op)) ]])]]).
650 definition execute_DEC ≝
651 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
652 execute_COM_DEC_INC_NEG_aux m t s i cur_pc pred_b8
658 (* A = H:A/X, H = H:AmodX se non c'e' overflow, altrimenti invariati *)
659 (* per i dettagli vedere div_b8 (modulo word16) *)
660 definition execute_DIV ≝
661 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
662 opt_map ?? (get_indX_8_high_reg m t s)
663 (λH_op.opt_map ?? (get_indX_8_low_reg m t s)
664 (λX_op.match div_b8 〈H_op:(get_acc_8_low_reg m t s)〉 X_op with
665 [ tripleT quoz rest overflow ⇒
667 let s_tmp1 ≝ set_c_flag m t s overflow in
669 let s_tmp2 ≝ match overflow with
671 | false ⇒ set_acc_8_low_reg m t s_tmp1 quoz ] in
672 (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
673 (* NB: che A sia cambiato o no, lo testa *)
674 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 (get_acc_8_low_reg m t s_tmp2) 〈x0,x0〉) in
675 (* H = H o H:AmodX *)
676 opt_map ?? (match overflow with
677 [ true ⇒ Some ? s_tmp3
678 | false ⇒ set_indX_8_high_reg m t s_tmp3 rest])
679 (λs_tmp4.Some ? (pair ?? s_tmp4 cur_pc)) ])).
682 definition execute_EOR ≝
683 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
684 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true xor_b8.
687 definition execute_INC ≝
688 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
689 execute_COM_DEC_INC_NEG_aux m t s i cur_pc succ_b8
695 (* jmp, il nuovo indirizzo e' una WORD *)
696 definition execute_JMP ≝
697 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
698 opt_map ?? (multi_mode_load m t false s cur_pc i)
701 Some ? (pair ?? (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
703 (* jump to subroutine *)
704 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
705 definition execute_JSR ≝
706 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
707 opt_map ?? (multi_mode_load m t false s cur_pc i)
708 (λS_M_PC.match S_M_PC with
709 [ tripleT s_tmp1 M_op new_pc ⇒ let aux ≝
710 (* push (new_pc low) *)
711 opt_map ?? (aux_push m t s_tmp1 (w16l new_pc))
712 (* push (new_pc high) *)
713 (λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
715 (λs_tmp3.Some ? (pair ?? s_tmp3 M_op)))
717 [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
720 opt_map ?? (set_spc_reg m t s_tmp1 new_pc)
722 (λs_tmp2.Some ? (pair ?? s_tmp2 M_op))
726 definition execute_LDA ≝
727 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
728 opt_map ?? (multi_mode_load m t true s cur_pc i)
729 (λS_M_PC.match S_M_PC with
730 [ tripleT s_tmp1 M_op new_pc ⇒
732 let s_tmp2 ≝ set_acc_8_low_reg m t s_tmp1 M_op in
733 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
734 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 M_op 〈x0,x0〉) in
736 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 M_op) in
738 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
740 Some ? (pair ?? s_tmp5 new_pc) ]).
743 definition execute_LDHX ≝
744 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
745 opt_map ?? (multi_mode_load m t false s cur_pc i)
746 (λS_M_PC.match S_M_PC with
747 [ tripleT s_tmp1 M_op new_pc ⇒
748 opt_map ?? (set_indX_16_reg m t s_tmp1 M_op)
750 (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
751 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_w16 M_op 〈〈x0,x0〉:〈x0,x0〉〉) in
753 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_w16 M_op) in
755 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
757 Some ? (pair ?? s_tmp5 new_pc)) ]).
760 definition execute_LDX ≝
761 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
762 opt_map ?? (multi_mode_load m t true s cur_pc i)
763 (λS_M_PC.match S_M_PC with
764 [ tripleT s_tmp1 M_op new_pc ⇒
765 opt_map ?? (set_indX_8_low_reg m t s_tmp1 M_op)
767 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
768 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 M_op 〈x0,x0〉) in
770 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 M_op) in
772 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
774 Some ? (pair ?? s_tmp5 new_pc)) ]).
776 (* M = 0 -> rcr M -> C' *)
777 definition execute_LSR ≝
778 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
779 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op false).
782 definition execute_MOV ≝
783 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
785 opt_map ?? (multi_mode_load m t true s cur_pc i)
786 (λS_R_PC.match S_R_PC with
787 [ tripleT s_tmp1 R_op tmp_pc ⇒
789 opt_map ?? (multi_mode_write m t true s_tmp1 tmp_pc i R_op)
790 (λS_PC.match S_PC with
791 [ pair s_tmp2 new_pc ⇒
792 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
793 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
795 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
797 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
799 Some ? (pair ?? s_tmp5 new_pc)])]).
802 definition execute_MUL ≝
803 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
804 opt_map ?? (get_indX_8_low_reg m t s)
805 (λX_op.let R_op ≝ mul_b8 X_op (get_acc_8_low_reg m t s) in
806 opt_map ?? (set_indX_8_low_reg m t s (w16h R_op))
807 (λs_tmp.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
810 definition execute_NEG ≝
811 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
812 execute_COM_DEC_INC_NEG_aux m t s i cur_pc compl_b8
815 (* fC = R7|R6|R5|R4|R3|R2|R1|R0 *)
816 (λC_op.λR_op.⊖(eq_b8 R_op 〈x0,x0〉)).
819 definition execute_NOP ≝
820 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
821 Some ? (pair ?? s cur_pc).
823 (* A = (mk_byte8 (b8l A) (b8h A)) *)
824 (* cioe' swap del nibble alto/nibble basso di A *)
825 definition execute_NSA ≝
826 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
827 match get_acc_8_low_reg m t s with [ mk_byte8 ah al ⇒
828 (* A = (mk_byte8 (b8l A) (b8h A)) *)
829 Some ? (pair ?? (set_acc_8_low_reg m t s 〈al,ah〉) cur_pc) ].
832 definition execute_ORA ≝
833 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
834 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true or_b8.
837 definition execute_PSHA ≝
838 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
839 opt_map ?? (aux_push m t s (get_acc_8_low_reg m t s))
840 (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc)).
843 definition execute_PSHH ≝
844 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
845 opt_map ?? (get_indX_8_high_reg m t s)
846 (λH_op.opt_map ?? (aux_push m t s H_op)
847 (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc))).
850 definition execute_PSHX ≝
851 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
852 opt_map ?? (get_indX_8_low_reg m t s)
853 (λH_op.opt_map ?? (aux_push m t s H_op)
854 (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc))).
857 definition execute_PULA ≝
858 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
859 opt_map ?? (aux_pop m t s)
860 (λS_and_A.match S_and_A with [ pair s_tmp1 A_op ⇒
861 Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 A_op) cur_pc) ]).
864 definition execute_PULH ≝
865 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
866 opt_map ?? (aux_pop m t s)
867 (λS_and_H.match S_and_H with [ pair s_tmp1 H_op ⇒
868 opt_map ?? (set_indX_8_high_reg m t s_tmp1 H_op)
869 (λs_tmp2.Some ? (pair ?? s_tmp2 cur_pc))]).
872 definition execute_PULX ≝
873 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
874 opt_map ?? (aux_pop m t s)
875 (λS_and_X.match S_and_X with [ pair s_tmp1 X_op ⇒
876 opt_map ?? (set_indX_8_low_reg m t s_tmp1 X_op)
877 (λs_tmp2.Some ? (pair ?? s_tmp2 cur_pc))]).
879 (* M = C' <- rcl M <- C *)
880 definition execute_ROL ≝
881 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
882 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcl_b8 M_op C_op).
884 (* M = C -> rcr M -> C' *)
885 definition execute_ROR ≝
886 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
887 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op C_op).
890 (* lascia inalterato il byte superiore di SP *)
891 definition execute_RSP ≝
892 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
893 opt_map ?? (get_sp_reg m t s)
894 (λSP_op.match SP_op with [ mk_word16 sph spl ⇒
895 opt_map ?? (set_sp_reg m t s 〈sph:〈xF,xF〉〉)
896 (λs_tmp.Some ? (pair ?? s_tmp cur_pc))]).
898 (* return from interrupt *)
899 definition execute_RTI ≝
900 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
902 opt_map ?? (aux_pop m t s)
903 (λS_and_CCR.match S_and_CCR with [ pair s_tmp1 CCR_op ⇒
904 let s_tmp2 ≝ aux_set_CCR m t s_tmp1 CCR_op in
906 opt_map ?? (aux_pop m t s_tmp2)
907 (λS_and_A.match S_and_A with [ pair s_tmp3 A_op ⇒
908 let s_tmp4 ≝ set_acc_8_low_reg m t s_tmp3 A_op in
910 opt_map ?? (aux_pop m t s_tmp4)
911 (λS_and_X.match S_and_X with [ pair s_tmp5 X_op ⇒
912 opt_map ?? (set_indX_8_low_reg m t s_tmp5 X_op)
914 (λs_tmp6.opt_map ?? (aux_pop m t s_tmp6)
915 (λS_and_PCH.match S_and_PCH with [ pair s_tmp7 PCH_op ⇒
917 opt_map ?? (aux_pop m t s_tmp7)
918 (λS_and_PCL.match S_and_PCL with [ pair s_tmp8 PCL_op ⇒
919 Some ? (pair ?? s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
921 (* return from subroutine *)
922 (* HC05/HC08/HCS08 si appoggia allo stack, RS08 si appoggia a SPC *)
923 definition execute_RTS ≝
924 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
927 opt_map ?? (aux_pop m t s)
928 (λS_and_PCH.match S_and_PCH with [ pair s_tmp1 PCH_op ⇒
930 opt_map ?? (aux_pop m t s_tmp1)
931 (λS_and_PCL.match S_and_PCL with [ pair s_tmp2 PCL_op ⇒
932 Some ? (pair ?? s_tmp2 〈PCH_op:PCL_op〉)])])
934 [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
937 opt_map ?? (get_spc_reg m t s)
938 (λSPC_op.Some ? (pair ?? s SPC_op))
942 definition execute_SBC ≝
943 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
944 execute_SBC_SUB_aux m t s i cur_pc true
945 (λA_op.λM_op.λC_op.match plus_b8 A_op (compl_b8 M_op) false with
946 [ pair resb resc ⇒ match C_op with
947 [ true ⇒ plus_b8 resb 〈xF,xF〉 false
948 | false ⇒ pair ?? resb resc ]]).
951 definition execute_SEC ≝
952 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
953 Some ? (pair ?? (set_c_flag m t s true) cur_pc).
956 definition execute_SEI ≝
957 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
958 opt_map ?? (set_i_flag m t s true)
959 (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
962 (* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
963 fare subroutine annidate se RA (return address) e' salvato sempre in SPC?
964 occore accedere a SPC e salvarne il contenuto *)
965 definition execute_SHA ≝
966 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
967 opt_map ?? (get_spc_reg m t s)
968 (λSPC_op.opt_map ?? (set_spc_reg m t s 〈(get_acc_8_low_reg m t s):(w16l SPC_op)〉)
969 (λs_tmp1.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 (w16h SPC_op)) cur_pc))).
972 (* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
973 fare subroutine annidate se RA (return address) e' salvato sempre in SPC?
974 occore accedere a SPC e salvarne il contenuto *)
975 definition execute_SLA ≝
976 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
977 opt_map ?? (get_spc_reg m t s)
978 (λSPC_op.opt_map ?? (set_spc_reg m t s 〈(w16h SPC_op):(get_acc_8_low_reg m t s)〉)
979 (λs_tmp1.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
982 definition execute_STA ≝
983 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
985 let A_op ≝ (get_acc_8_low_reg m t s) in
986 opt_map ?? (multi_mode_write m t true s cur_pc i A_op)
987 (λS_op_and_PC.match S_op_and_PC with
988 [ pair s_tmp1 new_pc ⇒
989 (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
990 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 A_op 〈x0,x0〉) in
992 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 A_op) in
994 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
996 Some ? (pair ?? s_tmp4 new_pc) ]).
999 definition execute_STHX ≝
1000 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1002 opt_map ?? (get_indX_16_reg m t s)
1003 (λX_op.opt_map ?? (multi_mode_write m t false s cur_pc i X_op)
1004 (λS_op_and_PC.match S_op_and_PC with
1005 [ pair s_tmp1 new_pc ⇒
1006 (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1007 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 X_op 〈〈x0,x0〉:〈x0,x0〉〉) in
1009 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_w16 X_op) in
1011 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
1012 (* newpc = nextpc *)
1013 Some ? (pair ?? s_tmp4 new_pc) ])).
1016 definition execute_STOP ≝
1017 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1018 Some ? (pair ?? (setweak_i_flag m t s false) cur_pc).
1021 definition execute_STX ≝
1022 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1024 opt_map ?? (get_indX_8_low_reg m t s)
1025 (λX_op.opt_map ?? (multi_mode_write m t true s cur_pc i X_op)
1026 (λS_op_and_PC.match S_op_and_PC with
1027 [ pair s_tmp1 new_pc ⇒
1028 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1029 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 X_op 〈x0,x0〉) in
1031 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 X_op) in
1033 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
1034 (* newpc = nextpc *)
1035 Some ? (pair ?? s_tmp4 new_pc) ])).
1038 definition execute_SUB ≝
1039 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1040 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).
1042 (* software interrupt *)
1043 definition execute_SWI ≝
1044 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1045 (* indirizzo da cui caricare il nuovo pc *)
1046 let vector ≝ get_pc_reg m t (set_pc_reg m t s 〈〈xF,xF〉:〈xF,xC〉〉) in
1047 (* push (cur_pc low) *)
1048 opt_map ?? (aux_push m t s (w16l cur_pc))
1049 (* push (cur_pc high *)
1050 (λs_tmp1.opt_map ?? (aux_push m t s_tmp1 (w16h cur_pc))
1051 (λs_tmp2.opt_map ?? (get_indX_8_low_reg m t s_tmp2)
1053 (λX_op.opt_map ?? (aux_push m t s_tmp2 X_op)
1055 (λs_tmp3.opt_map ?? (aux_push m t s_tmp3 (get_acc_8_low_reg m t s_tmp3))
1057 (λs_tmp4.opt_map ?? (aux_push m t s_tmp4 (aux_get_CCR m t s_tmp4))
1059 (λs_tmp5.opt_map ?? (set_i_flag m t s_tmp5 true)
1060 (* load from vector high *)
1061 (λs_tmp6.opt_map ?? (memory_filter_read m t s_tmp6 vector)
1062 (* load from vector low *)
1063 (λaddrh.opt_map ?? (memory_filter_read m t s_tmp6 (succ_w16 vector))
1064 (* newpc = [vector] *)
1065 (λaddrl.Some ? (pair ?? s_tmp6 〈addrh:addrl〉)))))))))).
1068 definition execute_TAP ≝
1069 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1070 Some ? (pair ?? (aux_set_CCR m t s (get_acc_8_low_reg m t s)) cur_pc).
1073 definition execute_TAX ≝
1074 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1075 opt_map ?? (set_indX_8_low_reg m t s (get_acc_8_low_reg m t s))
1076 (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
1079 definition execute_TPA ≝
1080 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1081 Some ? (pair ?? (set_acc_8_low_reg m t s (aux_get_CCR m t s)) cur_pc).
1084 (* implementata senza richiamare la sottrazione, la modifica dei flag
1086 definition execute_TST ≝
1087 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1088 opt_map ?? (multi_mode_load m t true s cur_pc i)
1089 (λS_M_PC.match S_M_PC with
1090 [ tripleT s_tmp1 M_op new_pc ⇒
1091 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1092 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 M_op 〈x0,x0〉) in
1094 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 M_op) in
1096 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
1097 (* newpc = nextpc *)
1098 Some ? (pair ?? s_tmp4 new_pc) ]).
1101 definition execute_TSX ≝
1102 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1103 opt_map ?? (get_sp_reg m t s )
1104 (λSP_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 SP_op))
1106 (λs_tmp.Some ? (pair ?? s_tmp cur_pc))).
1109 definition execute_TXA ≝
1110 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1111 opt_map ?? (get_indX_8_low_reg m t s)
1112 (λX_op.Some ? (pair ?? (set_acc_8_low_reg m t s X_op) cur_pc)).
1115 definition execute_TXS ≝
1116 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1117 opt_map ?? (get_indX_16_reg m t s )
1118 (λX_op.opt_map ?? (set_sp_reg m t s (pred_w16 X_op))
1120 (λs_tmp.Some ? (pair ?? s_tmp cur_pc))).
1123 definition execute_WAIT ≝
1124 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1125 Some ? (pair ?? (setweak_i_flag m t s false) cur_pc).
1131 (* enumerazione delle possibili modalita' di sospensione *)
1132 inductive susp_type : Type ≝
1133 BGND_MODE: susp_type
1134 | STOP_MODE: susp_type
1135 | WAIT_MODE: susp_type.
1137 (* un tipo opzione ad hoc
1138 - errore: errore+stato (seguira' reset o ??, cmq lo stato non va buttato)
1139 - sospensione: sospensione+stato (seguira' resume o ??)
1142 inductive tick_result (A:Type) : Type ≝
1143 TickERR : A → error_type → tick_result A
1144 | TickSUSP : A → susp_type → tick_result A
1145 | TickOK : A → tick_result A.
1147 (* sostanazialmente simula
1148 - fetch/decode/execute
1149 - l'esecuzione e' considerata atomica quindi nel caso di un'instruzione
1150 da 3 cicli la successione sara'
1151 ([fetch/decode] s,clk:None) →
1152 ( s,clk:Some 1,pseudo,mode,3,cur_pc) →
1153 ( s,clk:Some 2,pseudo,mode,3,cur_pc) →
1154 ([execute] s',clk:None) *)
1156 definition tick_execute ≝
1157 λm:mcu_type.λt:memory_impl.λs:any_status m t.
1158 λpseudo:any_opcode m.λmode:instr_mode.λcur_pc:word16.
1159 let abs_pseudo ≝ match pseudo with [ anyOP pseudo' ⇒ pseudo' ] in
1160 let a_status_and_fetch ≝ match abs_pseudo with
1161 [ ADC ⇒ execute_ADC m t s mode cur_pc (* add with carry *)
1162 | ADD ⇒ execute_ADD m t s mode cur_pc (* add *)
1163 | AIS ⇒ execute_AIS m t s mode cur_pc (* add immediate to SP *)
1164 | AIX ⇒ execute_AIX m t s mode cur_pc (* add immediate to X *)
1165 | AND ⇒ execute_AND m t s mode cur_pc (* and *)
1166 | ASL ⇒ execute_ASL m t s mode cur_pc (* aritmetic shift left *)
1167 | ASR ⇒ execute_ASR m t s mode cur_pc (* aritmetic shift right *)
1168 | BCC ⇒ execute_BCC m t s mode cur_pc (* branch if C=0 *)
1169 | BCLRn ⇒ execute_BCLRn m t s mode cur_pc (* clear bit n *)
1170 | BCS ⇒ execute_BCS m t s mode cur_pc (* branch if C=1 *)
1171 | BEQ ⇒ execute_BEQ m t s mode cur_pc (* branch if Z=1 *)
1172 | BGE ⇒ execute_BGE m t s mode cur_pc (* branch if N⊙V=0 (great or equal) *)
1173 | BGND ⇒ execute_BGND m t s mode cur_pc (* !!background mode!!*)
1174 | BGT ⇒ execute_BGT m t s mode cur_pc (* branch if Z|N⊙V=0 clear (great) *)
1175 | BHCC ⇒ execute_BHCC m t s mode cur_pc (* branch if H=0 *)
1176 | BHCS ⇒ execute_BHCS m t s mode cur_pc (* branch if H=1 *)
1177 | BHI ⇒ execute_BHI m t s mode cur_pc (* branch if C|Z=0, (higher) *)
1178 | BIH ⇒ execute_BIH m t s mode cur_pc (* branch if nIRQ=1 *)
1179 | BIL ⇒ execute_BIL m t s mode cur_pc (* branch if nIRQ=0 *)
1180 | BIT ⇒ execute_BIT m t s mode cur_pc (* flag = and (bit test) *)
1181 | BLE ⇒ execute_BLE m t s mode cur_pc (* branch if Z|N⊙V=1 (less or equal) *)
1182 | BLS ⇒ execute_BLS m t s mode cur_pc (* branch if C|Z=1 (lower or same) *)
1183 | BLT ⇒ execute_BLT m t s mode cur_pc (* branch if N⊙1=1 (less) *)
1184 | BMC ⇒ execute_BMC m t s mode cur_pc (* branch if I=0 (interrupt mask clear) *)
1185 | BMI ⇒ execute_BMI m t s mode cur_pc (* branch if N=1 (minus) *)
1186 | BMS ⇒ execute_BMS m t s mode cur_pc (* branch if I=1 (interrupt mask set) *)
1187 | BNE ⇒ execute_BNE m t s mode cur_pc (* branch if Z=0 *)
1188 | BPL ⇒ execute_BPL m t s mode cur_pc (* branch if N=0 (plus) *)
1189 | BRA ⇒ execute_BRA m t s mode cur_pc (* branch always *)
1190 | BRCLRn ⇒ execute_BRCLRn m t s mode cur_pc (* branch if bit n clear *)
1191 | BRN ⇒ execute_BRN m t s mode cur_pc (* branch never (nop) *)
1192 | BRSETn ⇒ execute_BRSETn m t s mode cur_pc (* branch if bit n set *)
1193 | BSETn ⇒ execute_BSETn m t s mode cur_pc (* set bit n *)
1194 | BSR ⇒ execute_BSR m t s mode cur_pc (* branch to subroutine *)
1195 | CBEQA ⇒ execute_CBEQA m t s mode cur_pc (* compare (A) and BEQ *)
1196 | CBEQX ⇒ execute_CBEQX m t s mode cur_pc (* compare (X) and BEQ *)
1197 | CLC ⇒ execute_CLC m t s mode cur_pc (* C=0 *)
1198 | CLI ⇒ execute_CLI m t s mode cur_pc (* I=0 *)
1199 | CLR ⇒ execute_CLR m t s mode cur_pc (* operand=0 *)
1200 | CMP ⇒ execute_CMP m t s mode cur_pc (* flag = sub (compare A) *)
1201 | COM ⇒ execute_COM m t s mode cur_pc (* not (1 complement) *)
1202 | CPHX ⇒ execute_CPHX m t s mode cur_pc (* flag = sub (compare H:X) *)
1203 | CPX ⇒ execute_CPX m t s mode cur_pc (* flag = sub (compare X) *)
1204 | DAA ⇒ execute_DAA m t s mode cur_pc (* decimal adjust A *)
1205 | DBNZ ⇒ execute_DBNZ m t s mode cur_pc (* dec and BNE *)
1206 | DEC ⇒ execute_DEC m t s mode cur_pc (* operand=operand-1 (decrement) *)
1207 | DIV ⇒ execute_DIV m t s mode cur_pc (* div *)
1208 | EOR ⇒ execute_EOR m t s mode cur_pc (* xor *)
1209 | INC ⇒ execute_INC m t s mode cur_pc (* operand=operand+1 (increment) *)
1210 | JMP ⇒ execute_JMP m t s mode cur_pc (* jmp word [operand] *)
1211 | JSR ⇒ execute_JSR m t s mode cur_pc (* jmp to subroutine *)
1212 | LDA ⇒ execute_LDA m t s mode cur_pc (* load in A *)
1213 | LDHX ⇒ execute_LDHX m t s mode cur_pc (* load in H:X *)
1214 | LDX ⇒ execute_LDX m t s mode cur_pc (* load in X *)
1215 | LSR ⇒ execute_LSR m t s mode cur_pc (* logical shift right *)
1216 | MOV ⇒ execute_MOV m t s mode cur_pc (* move *)
1217 | MUL ⇒ execute_MUL m t s mode cur_pc (* mul *)
1218 | NEG ⇒ execute_NEG m t s mode cur_pc (* neg (2 complement) *)
1219 | NOP ⇒ execute_NOP m t s mode cur_pc (* nop *)
1220 | NSA ⇒ execute_NSA m t s mode cur_pc (* nibble swap A (al:ah <- ah:al) *)
1221 | ORA ⇒ execute_ORA m t s mode cur_pc (* or *)
1222 | PSHA ⇒ execute_PSHA m t s mode cur_pc (* push A *)
1223 | PSHH ⇒ execute_PSHH m t s mode cur_pc (* push H *)
1224 | PSHX ⇒ execute_PSHX m t s mode cur_pc (* push X *)
1225 | PULA ⇒ execute_PULA m t s mode cur_pc (* pop A *)
1226 | PULH ⇒ execute_PULH m t s mode cur_pc (* pop H *)
1227 | PULX ⇒ execute_PULX m t s mode cur_pc (* pop X *)
1228 | ROL ⇒ execute_ROL m t s mode cur_pc (* rotate left *)
1229 | ROR ⇒ execute_ROR m t s mode cur_pc (* rotate right *)
1230 | RSP ⇒ execute_RSP m t s mode cur_pc (* reset SP (0x00FF) *)
1231 | RTI ⇒ execute_RTI m t s mode cur_pc (* return from interrupt *)
1232 | RTS ⇒ execute_RTS m t s mode cur_pc (* return from subroutine *)
1233 | SBC ⇒ execute_SBC m t s mode cur_pc (* sub with carry*)
1234 | SEC ⇒ execute_SEC m t s mode cur_pc (* C=1 *)
1235 | SEI ⇒ execute_SEI m t s mode cur_pc (* I=1 *)
1236 | SHA ⇒ execute_SHA m t s mode cur_pc (* swap spc_high,A *)
1237 | SLA ⇒ execute_SLA m t s mode cur_pc (* swap spc_low,A *)
1238 | STA ⇒ execute_STA m t s mode cur_pc (* store from A *)
1239 | STHX ⇒ execute_STHX m t s mode cur_pc (* store from H:X *)
1240 | STOP ⇒ execute_STOP m t s mode cur_pc (* !!stop mode!! *)
1241 | STX ⇒ execute_STX m t s mode cur_pc (* store from X *)
1242 | SUB ⇒ execute_SUB m t s mode cur_pc (* sub *)
1243 | SWI ⇒ execute_SWI m t s mode cur_pc (* software interrupt *)
1244 | TAP ⇒ execute_TAP m t s mode cur_pc (* flag=A (transfer A to process status byte *)
1245 | TAX ⇒ execute_TAX m t s mode cur_pc (* X=A (transfer A to X) *)
1246 | TPA ⇒ execute_TPA m t s mode cur_pc (* A=flag (transfer process status byte to A) *)
1247 | TST ⇒ execute_TST m t s mode cur_pc (* flag = sub (test) *)
1248 | TSX ⇒ execute_TSX m t s mode cur_pc (* X:H=SP (transfer SP to H:X) *)
1249 | TXA ⇒ execute_TXA m t s mode cur_pc (* A=X (transfer X to A) *)
1250 | TXS ⇒ execute_TXS m t s mode cur_pc (* SP=X:H (transfer H:X to SP) *)
1251 | WAIT ⇒ execute_WAIT m t s mode cur_pc (* !!wait mode!!*)
1252 ] in match a_status_and_fetch with
1253 (* errore nell'execute (=caricamento argomenti)? riportato in output *)
1254 (* nessun avanzamento e clk a None *)
1255 [ None ⇒ TickERR ? (set_clk_desc m t s (None ?)) ILL_EX_AD
1256 | Some status_and_newpc ⇒
1257 (* aggiornamento centralizzato di pc e clk *)
1258 match status_and_newpc with
1259 [ pair s_tmp1 new_pc ⇒
1260 let s_tmp2 ≝ set_pc_reg m t s_tmp1 new_pc in
1261 let s_tmp3 ≝ set_clk_desc m t s_tmp2 (None ?) in
1262 let abs_magic ≝ magic_of_opcode abs_pseudo in
1263 (* distinzione fra le 4 modalita' possibili, normale/BGND/STOP/WAIT *)
1264 match eq_b8 abs_magic (magic_of_opcode BGND) with
1265 [ true ⇒ TickSUSP ? s_tmp3 BGND_MODE
1266 | false ⇒ match eq_b8 abs_magic (magic_of_opcode STOP) with
1267 [ true ⇒ TickSUSP ? s_tmp3 STOP_MODE
1268 | false ⇒ match eq_b8 abs_magic (magic_of_opcode WAIT) with
1269 [ true ⇒ TickSUSP ? s_tmp3 WAIT_MODE
1270 | false ⇒ TickOK ? s_tmp3
1274 λm:mcu_type.λt:memory_impl.λs:any_status m t.
1275 let opt_info ≝ get_clk_desc m t s in
1277 (* e' il momento del fetch *)
1278 [ None ⇒ match fetch m t s with
1279 (* errore nel fetch/decode? riportato in output, nessun avanzamento *)
1280 [ FetchERR err ⇒ TickERR ? s err
1281 (* nessun errore nel fetch *)
1282 | FetchOK fetch_info cur_pc ⇒ match fetch_info with
1283 [ quadrupleT pseudo mode _ tot_clk ⇒
1284 match eq_b8 〈x0,x1〉 tot_clk with
1285 (* un solo clk, execute subito *)
1286 [ true ⇒ tick_execute m t s pseudo mode cur_pc
1287 (* piu' clk, execute rimandata *)
1288 | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintupleT ????? 〈x0,x1〉 pseudo mode tot_clk cur_pc)))
1292 (* il fetch e' gia' stato eseguito, e' il turno di execute? *)
1293 | Some info ⇒ match info with [ quintupleT cur_clk pseudo mode tot_clk cur_pc ⇒
1294 match eq_b8 (succ_b8 cur_clk) tot_clk with
1296 [ true ⇒ tick_execute m t s pseudo mode cur_pc
1297 (* no, avanzamento cur_clk *)
1298 | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintupleT ????? (succ_b8 cur_clk) pseudo mode tot_clk cur_pc)))
1307 let rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
1309 [ TickERR s' error ⇒ TickERR ? s' error
1310 | TickSUSP s' susp ⇒ TickSUSP ? s' susp
1311 | TickOK s' ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ]
1315 ∀m,u,s,n1,n2. execute m u s (n1 + n2) = execute m u (execute m u s n1) n2.
1317 generalize in match s; clear s;