1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/load_write.ma".
24 include "freescale/nat_lemmas.ma".
26 (* ************************************************ *)
27 (* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *)
28 (* ************************************************ *)
30 (* NB: dentro il codice i commenti cercano di spiegare la logica
31 secondo quanto riportato dalle specifiche delle mcu *)
33 (* NB: notare che tranne nei casi in cui PC viene modificato esplicitamente
34 il suo avanzamento viene delegato totalmente agli strati inferiori
35 I) avanzamento dovuto al decode degli op (fetch)
36 II) avanzamento dovuto al caricamento degli argomenti (multi_mode_load/write)
37 la modifica effettiva avviene poi centralizzata in tick *)
39 (* A = [true] fAMC(A,M,C), [false] A *)
40 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
41 (* fAMC e' la logica da applicare: somma con/senza carry *)
42 ndefinition execute_ADC_ADD_aux ≝
43 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
44 λfAMC:byte8 → byte8 → bool → ProdT byte8 bool.
45 opt_map ?? (multi_mode_load true m t s cur_pc i)
46 (λS_M_PC.match S_M_PC with
47 [ triple s_tmp1 M_op new_pc ⇒
48 let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
49 match fAMC A_op M_op (get_c_flag m t s_tmp1) with
51 let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
52 let A3 ≝ MSB_ex (b8l A_op) in let M3 ≝ MSB_ex (b8l M_op) in let R3 ≝ MSB_ex (b8l R_op) in
53 (* A = [true] fAMC(A,M,C), [false] A *)
54 let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
55 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
56 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
57 (* C = A7&M7 | M7&nR7 | nR7&A7 *)
58 let s_tmp4 ≝ set_c_flag m t s_tmp3 ((A7⊗M7) ⊕ (M7⊗(⊖R7)) ⊕ ((⊖R7)⊗A7)) in
60 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 R7 in
61 (* H = A3&M3 | M3&nR3 | nR3&A3 *)
62 let s_tmp6 ≝ setweak_h_flag m t s_tmp5 ((A3⊗M3) ⊕ (M3⊗(⊖R3)) ⊕ ((⊖R3)⊗A3)) in
63 (* V = A7&M7&nR7 | nA7&nM7&R7 *)
64 let s_tmp7 ≝ setweak_v_flag m t s_tmp6 ((A7⊗M7⊗(⊖R7)) ⊕ ((⊖A7)⊗(⊖M7)⊗R7)) in
66 Some ? (pair ?? s_tmp7 new_pc) ]]).
68 (* A = [true] fAM(A,M), [false] A *)
69 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
70 (* fAM e' la logica da applicare: and/xor/or *)
71 ndefinition execute_AND_BIT_EOR_ORA_aux ≝
72 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
73 λfAM:byte8 → byte8 → byte8.
74 opt_map ?? (multi_mode_load true m t s cur_pc i)
75 (λS_M_PC.match S_M_PC with
76 [ triple s_tmp1 M_op new_pc ⇒
77 let R_op ≝ fAM (get_acc_8_low_reg m t s_tmp1) M_op in
78 (* A = [true] fAM(A,M), [false] A *)
79 let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
80 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
81 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
83 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
85 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
87 Some ? (pair ?? s_tmp5 new_pc) ]).
90 (* fMC e' la logica da applicare: rc_/ro_/sh_ *)
91 ndefinition execute_ASL_ASR_LSR_ROL_ROR_aux ≝
92 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
93 λfMC:byte8 → bool → ProdT byte8 bool.
94 opt_map ?? (multi_mode_load true m t s cur_pc i)
95 (λS_M_PC.match S_M_PC with
96 [ triple s_tmp1 M_op _ ⇒
97 match fMC M_op (get_c_flag m t s_tmp1) with [ pair R_op carry ⇒
99 opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
100 (λS_PC.match S_PC with
101 [ pair s_tmp2 new_pc ⇒
103 let s_tmp3 ≝ set_c_flag m t s_tmp2 carry in
104 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
105 let s_tmp4 ≝ set_z_flag m t s_tmp3 (eq_b8 R_op 〈x0,x0〉) in
107 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 (MSB_b8 R_op) in
109 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((MSB_b8 R_op) ⊙ carry) in
111 Some ? (pair ?? s_tmp6 new_pc) ])]]).
113 (* estensione del segno byte → word *)
114 ndefinition byte_extension ≝
115 λb:byte8.〈match MSB_b8 b with [ true ⇒ 〈xF,xF〉 | false ⇒ 〈x0,x0〉 ]:b〉.
117 (* branch con byte+estensione segno *)
118 ndefinition branched_pc ≝
119 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λb:byte8.
120 get_pc_reg m t (set_pc_reg m t s (plus_w16_d_d cur_pc (byte_extension b))).
122 (* if COND=1 branch *)
123 (* tutti i branch calcoleranno la condizione e la passeranno qui *)
124 ndefinition execute_any_BRANCH ≝
125 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:bool.
126 opt_map ?? (multi_mode_load true m t s cur_pc i)
127 (λS_M_PC.match S_M_PC with
128 [ triple s_tmp1 M_op new_pc ⇒
129 (* if true, branch *)
131 (* newpc = nextpc + rel *)
132 [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc M_op))
134 | false ⇒ Some ? (pair ?? s_tmp1 new_pc) ]]).
136 (* Mn = filtered optval *)
137 (* il chiamante passa 0x00 per azzerare, 0xFF per impostare il bit di M *)
138 ndefinition execute_BCLRn_BSETn_aux ≝
139 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λoptval:byte8.
140 (* Mn = filtered optval *)
141 opt_map ?? (multi_mode_write true m t s cur_pc i optval)
142 (λS_PC.match S_PC with
144 [ pair s_tmp1 new_pc ⇒ Some ? (pair ?? s_tmp1 new_pc) ]).
146 (* if COND(Mn) branch *)
147 (* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
148 ndefinition execute_BRCLRn_BRSETn_aux ≝
149 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:byte8 → bool.
150 opt_map ?? (multi_mode_load false m t s cur_pc i)
151 (λS_M_PC.match S_M_PC with
152 [ triple s_tmp1 M_op new_pc ⇒ match M_op with
153 [ mk_word16 MH_op ML_op ⇒
154 (* if COND(Mn) branch *)
155 match fCOND MH_op with
156 (* newpc = nextpc + rel *)
157 [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
159 | false ⇒ Some ? (pair ?? s_tmp1 new_pc) ]]]).
162 (* fM e' la logica da applicare: not/neg/++/-- *)
163 ndefinition execute_COM_DEC_INC_NEG_aux ≝
164 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
165 λfM:byte8 → byte8.λfV:bool → bool → bool.λfC:bool → byte8 → bool.
166 opt_map ?? (multi_mode_load true m t s cur_pc i)
167 (λS_M_PC.match S_M_PC with
168 [ triple s_tmp1 M_op _ ⇒
169 let R_op ≝ fM M_op in
171 opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
172 (λS_PC.match S_PC with
173 [ pair s_tmp2 new_pc ⇒
175 let s_tmp3 ≝ set_c_flag m t s_tmp2 (fC (get_c_flag m t s_tmp2) R_op) in
176 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
177 let s_tmp4 ≝ set_z_flag m t s_tmp3 (eq_b8 R_op 〈x0,x0〉) in
179 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 (MSB_b8 R_op) in
181 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (fV (MSB_b8 M_op) (MSB_b8 R_op)) in
183 Some ? (pair ?? s_tmp6 new_pc) ])]).
185 (* A = [true] fAMC(A,M,C), [false] A *)
186 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
187 (* fAMC e' la logica da applicare: sottrazione con/senza carry *)
188 ndefinition execute_SBC_SUB_aux ≝
189 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
190 λfAMC:byte8 → byte8 → bool → ProdT byte8 bool.
191 opt_map ?? (multi_mode_load true m t s cur_pc i)
192 (λS_M_PC.match S_M_PC with
193 [ triple s_tmp1 M_op new_pc ⇒
194 let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
195 match fAMC A_op M_op (get_c_flag m t s_tmp1) with
197 let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
198 (* A = [true] fAMC(A,M,C), [false] A *)
199 let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
200 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
201 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
202 (* C = nA7&M7 | M7&R7 | R7&nA7 *)
203 let s_tmp4 ≝ set_c_flag m t s_tmp3 (((⊖A7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖A7))) in
205 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 R7 in
206 (* V = A7&nM7&nR7 | nA7&M7&R7 *)
207 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((A7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖A7)⊗M7⊗R7)) in
209 Some ? (pair ?? s_tmp6 new_pc) ]]).
211 (* il classico push *)
212 ndefinition aux_push ≝
213 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
214 opt_map ?? (get_sp_reg m t s)
216 (λSP_op.opt_map ?? (memory_filter_write m t s SP_op val)
218 (λs_tmp1.opt_map ?? (set_sp_reg m t s_tmp1 (pred_w16 SP_op))
219 (λs_tmp2.Some ? s_tmp2))).
221 (* il classico pop *)
222 (* NB: l'incremento di SP deve essere filtrato dalla ALU, quindi get(set(SP)) *)
223 ndefinition aux_pop ≝
224 λm:mcu_type.λt:memory_impl.λs:any_status m t.
225 opt_map ?? (get_sp_reg m t s)
227 (λSP_op.opt_map ?? (set_sp_reg m t s (succ_w16 SP_op))
228 (λs_tmp1.opt_map ?? (get_sp_reg m t s_tmp1)
230 (λSP_op'.opt_map ?? (memory_filter_read m t s_tmp1 SP_op')
231 (λval.Some ? (pair ?? s_tmp1 val))))).
233 (* CCR corrisponde a V11HINZC e cmq 1 se un flag non esiste *)
234 (* i flag mantengono posizione costante nelle varie ALU, e se non sono
235 implementati corrispondono a 1 *)
236 ndefinition aux_get_CCR ≝
237 λm:mcu_type.λt:memory_impl.λs:any_status m t.
238 let V_comp ≝ match get_v_flag m t s with
239 [ None ⇒ 〈x8,x0〉 | Some V_val ⇒ match V_val with [ true ⇒ 〈x8,x0〉 | false ⇒ 〈x0,x0〉 ]] in
240 let H_comp ≝ match get_h_flag m t s with
241 [ None ⇒ 〈x1,x0〉 | Some H_val ⇒ match H_val with [ true ⇒ 〈x1,x0〉 | false ⇒ 〈x0,x0〉 ]] in
242 let I_comp ≝ match get_i_flag m t s with
243 [ None ⇒ 〈x0,x8〉 | Some I_val ⇒ match I_val with [ true ⇒ 〈x0,x8〉 | false ⇒ 〈x0,x0〉 ]] in
244 let N_comp ≝ match get_n_flag m t s with
245 [ None ⇒ 〈x0,x4〉 | Some N_val ⇒ match N_val with [ true ⇒ 〈x0,x4〉 | false ⇒ 〈x0,x0〉 ]] in
246 let Z_comp ≝ match get_z_flag m t s with
247 [ true ⇒ 〈x0,x2〉 | false ⇒ 〈x0,x0〉 ] in
248 let C_comp ≝ match get_c_flag m t s with
249 [ true ⇒ 〈x0,x1〉 | false ⇒ 〈x0,x0〉 ] in
250 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))))).
252 (* CCR corrisponde a V11HINZC *)
253 (* i flag mantengono posizione costante nelle varie ALU, e se non sono
254 implementati si puo' usare tranquillamente setweak *)
255 ndefinition aux_set_CCR ≝
256 λm:mcu_type.λt:memory_impl.λs:any_status m t.λCCR:byte8.
257 let s_tmp1 ≝ set_c_flag m t s (eq_b8 〈x0,x1〉 (and_b8 〈x0,x1〉 CCR)) in
258 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 〈x0,x2〉 (and_b8 〈x0,x2〉 CCR)) in
259 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (eq_b8 〈x0,x4〉 (and_b8 〈x0,x4〉 CCR)) in
260 let s_tmp4 ≝ setweak_i_flag m t s_tmp3 (eq_b8 〈x0,x8〉 (and_b8 〈x0,x8〉 CCR)) in
261 let s_tmp5 ≝ setweak_h_flag m t s_tmp4 (eq_b8 〈x1,x0〉 (and_b8 〈x1,x0〉 CCR)) in
262 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (eq_b8 〈x8,x0〉 (and_b8 〈x8,x0〉 CCR)) in
265 (* **************** *)
266 (* LOGICA DELLA ALU *)
267 (* **************** *)
270 ndefinition execute_ADC ≝
271 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
272 execute_ADC_ADD_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8_dc_dc A_op M_op C_op).
275 ndefinition execute_ADD ≝
276 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
277 execute_ADC_ADD_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8_dc_dc A_op M_op false).
279 (* SP += extended M *)
280 ndefinition execute_AIS ≝
281 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
282 opt_map ?? (multi_mode_load true m t s cur_pc i)
283 (λS_M_PC.match S_M_PC with
284 [ triple s_tmp1 M_op new_pc ⇒
285 opt_map ?? (get_sp_reg m t s_tmp1)
286 (* SP += extended M *)
287 (λSP_op.opt_map ?? (set_sp_reg m t s_tmp1 (plus_w16_d_d SP_op (byte_extension M_op)))
288 (λs_tmp2.Some ? (pair ?? s_tmp2 new_pc))) ]).
290 (* H:X += extended M *)
291 ndefinition execute_AIX ≝
292 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
293 opt_map ?? (multi_mode_load true m t s cur_pc i)
294 (λS_M_PC.match S_M_PC with
295 [ triple s_tmp1 M_op new_pc ⇒
296 opt_map ?? (get_indX_16_reg m t s_tmp1)
297 (* H:X += extended M *)
298 (λHX_op.opt_map ?? (set_indX_16_reg m t s_tmp1 (plus_w16_d_d HX_op (byte_extension M_op)))
299 (λs_tmp2.Some ? (pair ?? s_tmp2 new_pc))) ]).
302 ndefinition execute_AND ≝
303 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
304 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true and_b8.
306 (* M = C' <- rcl M <- 0 *)
307 ndefinition execute_ASL ≝
308 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
309 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcl_b8 M_op false).
311 (* M = M7 -> rcr M -> C' *)
312 ndefinition execute_ASR ≝
313 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
314 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)).
317 ndefinition execute_BCC ≝
318 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
319 execute_any_BRANCH m t s i cur_pc (⊖(get_c_flag m t s)).
322 ndefinition execute_BCLRn ≝
323 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
324 execute_BCLRn_BSETn_aux m t s i cur_pc 〈x0,x0〉.
327 ndefinition execute_BCS ≝
328 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
329 execute_any_BRANCH m t s i cur_pc (get_c_flag m t s).
332 ndefinition execute_BEQ ≝
333 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
334 execute_any_BRANCH m t s i cur_pc (get_z_flag m t s).
336 (* if N⊙V=0, branch *)
337 ndefinition execute_BGE ≝
338 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
339 opt_map ?? (get_n_flag m t s)
340 (λN_op.opt_map ?? (get_v_flag m t s)
341 (λV_op.execute_any_BRANCH m t s i cur_pc (⊖(N_op ⊙ V_op)))).
344 ndefinition execute_BGND ≝
345 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
346 Some ? (pair ?? s cur_pc).
348 (* if Z|N⊙V=0, branch *)
349 ndefinition execute_BGT ≝
350 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
351 opt_map ?? (get_n_flag m t s)
352 (λN_op.opt_map ?? (get_v_flag m t s)
353 (λV_op.execute_any_BRANCH m t s i cur_pc (⊖((get_z_flag m t s) ⊕ (N_op ⊙ V_op))))).
356 ndefinition execute_BHCC ≝
357 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
358 opt_map ?? (get_h_flag m t s)
359 (λH_op.execute_any_BRANCH m t s i cur_pc (⊖H_op)).
362 ndefinition execute_BHCS ≝
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).
367 (* if C|Z=0, branch *)
368 ndefinition execute_BHI ≝
369 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
370 execute_any_BRANCH m t s i cur_pc (⊖((get_c_flag m t s) ⊕ (get_z_flag m t s))).
372 (* if nIRQ=1, branch NB: irqflag e' un negato del pin *)
373 ndefinition execute_BIH ≝
374 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
375 opt_map ?? (get_irq_flag m t s)
376 (λIRQ_op.execute_any_BRANCH m t s i cur_pc (⊖IRQ_op)).
378 (* if nIRQ=0, branch NB: irqflag e' un negato del pin *)
379 ndefinition execute_BIL ≝
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).
385 ndefinition execute_BIT ≝
386 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
387 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc false and_b8.
389 (* if Z|N⊙V=1, branch *)
390 ndefinition execute_BLE ≝
391 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
392 opt_map ?? (get_n_flag m t s)
393 (λN_op.opt_map ?? (get_v_flag m t s)
394 (λV_op.execute_any_BRANCH m t s i cur_pc ((get_z_flag m t s) ⊕ (N_op ⊙ V_op)))).
396 (* if C|Z=1, branch *)
397 ndefinition execute_BLS ≝
398 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
399 execute_any_BRANCH m t s i cur_pc ((get_c_flag m t s) ⊕ (get_z_flag m t s)).
401 (* if N⊙V=1, branch *)
402 ndefinition execute_BLT ≝
403 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
404 opt_map ?? (get_n_flag m t s)
405 (λN_op.opt_map ?? (get_v_flag m t s)
406 (λV_op.execute_any_BRANCH m t s i cur_pc (N_op ⊙ V_op))).
409 ndefinition execute_BMC ≝
410 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
411 opt_map ?? (get_i_flag m t s)
412 (λI_op.execute_any_BRANCH m t s i cur_pc (⊖I_op)).
415 ndefinition execute_BMI ≝
416 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
417 opt_map ?? (get_n_flag m t s)
418 (λN_op.execute_any_BRANCH m t s i cur_pc N_op).
421 ndefinition execute_BMS ≝
422 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
423 opt_map ?? (get_i_flag m t s)
424 (λI_op.execute_any_BRANCH m t s i cur_pc I_op).
427 ndefinition execute_BNE ≝
428 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
429 execute_any_BRANCH m t s i cur_pc (⊖(get_z_flag m t s)).
432 ndefinition execute_BPL ≝
433 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
434 opt_map ?? (get_n_flag m t s)
435 (λN_op.execute_any_BRANCH m t s i cur_pc (⊖N_op)).
438 ndefinition execute_BRA ≝
439 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
440 execute_any_BRANCH m t s i cur_pc true.
443 ndefinition execute_BRCLRn ≝
444 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
445 execute_BRCLRn_BRSETn_aux m t s i cur_pc
446 (λMn_op.eq_b8 Mn_op 〈x0,x0〉).
448 (* branch never... come se fosse un nop da 2 byte *)
449 ndefinition execute_BRN ≝
450 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
451 execute_any_BRANCH m t s i cur_pc false.
454 ndefinition execute_BRSETn ≝
455 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
456 execute_BRCLRn_BRSETn_aux m t s i cur_pc
457 (λMn_op.⊖(eq_b8 Mn_op 〈x0,x0〉)).
460 ndefinition execute_BSETn ≝
461 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
462 execute_BCLRn_BSETn_aux m t s i cur_pc 〈xF,xF〉.
464 (* branch to subroutine *)
465 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
466 ndefinition execute_BSR ≝
467 λm:mcu_type.λt:memory_impl.λs:any_status m t .λi:instr_mode.λcur_pc:word16.
468 opt_map ?? (multi_mode_load true m t s cur_pc i)
469 (λS_M_PC.match S_M_PC with
470 [ triple s_tmp1 M_op new_pc ⇒ let aux ≝
471 (* push (new_pc low) *)
472 opt_map ?? (aux_push m t s_tmp1 (w16l new_pc))
473 (* push (new_pc high) *)
474 (λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
475 (* new_pc = new_pc + rel *)
476 (λs_tmp3.Some ? (pair ?? s_tmp3 (branched_pc m t s_tmp3 new_pc M_op))))
478 [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
481 opt_map ?? (set_spc_reg m t s_tmp1 new_pc)
482 (* new_pc = new_pc + rel *)
483 (λs_tmp2.Some ? (pair ?? s_tmp2 (branched_pc m t s_tmp2 new_pc M_op)))
487 ndefinition execute_CBEQA ≝
488 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
489 opt_map ?? (multi_mode_load false m t s cur_pc i)
490 (λS_M_PC.match S_M_PC with
491 [ triple s_tmp1 M_op new_pc ⇒
493 [ mk_word16 MH_op ML_op ⇒
495 match eq_b8 (get_acc_8_low_reg m t s_tmp1) MH_op with
496 (* new_pc = new_pc + rel *)
497 [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
498 (* new_pc = new_pc *)
499 | false ⇒ Some ? (pair ?? s_tmp1 new_pc)
503 ndefinition execute_CBEQX ≝
504 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
505 opt_map ?? (multi_mode_load false m t s cur_pc i)
506 (λS_M_PC.match S_M_PC with
507 [ triple s_tmp1 M_op new_pc ⇒
509 [ mk_word16 MH_op ML_op ⇒
510 opt_map ?? (get_indX_8_low_reg m t s_tmp1)
512 (λX_op.match eq_b8 X_op MH_op with
513 (* new_pc = new_pc + rel *)
514 [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
515 (* new_pc = new_pc *)
516 | false ⇒ Some ? (pair ?? s_tmp1 new_pc)
520 ndefinition execute_CLC ≝
521 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
522 Some ? (pair ?? (set_c_flag m t s false) cur_pc).
525 ndefinition execute_CLI ≝
526 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
527 opt_map ?? (set_i_flag m t s false)
528 (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
531 ndefinition execute_CLR ≝
532 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
534 opt_map ?? (multi_mode_write true m t s cur_pc i 〈x0,x0〉)
535 (λS_PC.match S_PC with
536 [ pair s_tmp1 new_pc ⇒
538 let s_tmp2 ≝ set_z_flag m t s_tmp1 true in
540 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 false in
542 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
544 Some ? (pair ?? s_tmp4 new_pc) ]).
547 ndefinition execute_CMP ≝
548 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
549 execute_SBC_SUB_aux m t s i cur_pc false (λA_op.λM_op.λC_op.plus_b8_dc_dc A_op (compl_b8 M_op) false).
552 ndefinition execute_COM ≝
553 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
554 execute_COM_DEC_INC_NEG_aux m t s i cur_pc not_b8
560 (* flags = H:X - M *)
561 ndefinition execute_CPHX ≝
562 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
563 opt_map ?? (multi_mode_load false m t s cur_pc i)
564 (λS_M_PC.match S_M_PC with
565 [ triple s_tmp1 M_op new_pc ⇒
566 opt_map ?? (get_indX_16_reg m t s_tmp1)
568 match plus_w16_dc_dc X_op (compl_w16 M_op) false with
570 let X15 ≝ MSB_w16 X_op in let M15 ≝ MSB_w16 M_op in let R15 ≝ MSB_w16 R_op in
571 (* Z = nR15&nR14&nR13&nR12&nR11&nR10&nR9&nR8&nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
572 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 R_op 〈〈x0,x0〉:〈x0,x0〉〉) in
573 (* C = nX15&M15 | M15&R15 | R15&nX15 *)
574 let s_tmp3 ≝ set_c_flag m t s_tmp2 (((⊖X15)⊗M15) ⊕ (M15⊗R15) ⊕ (R15⊗(⊖X15))) in
576 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 R15 in
577 (* V = X15&nM15&nR15 | nX15&M15&R15 *)
578 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X15⊗(⊖M15)⊗(⊖R15)) ⊕ ((⊖X15)⊗M15⊗R15)) in
580 Some ? (pair ?? s_tmp5 new_pc) ] ) ]).
583 ndefinition execute_CPX ≝
584 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
585 opt_map ?? (multi_mode_load true m t s cur_pc i)
586 (λS_M_PC.match S_M_PC with
587 [ triple s_tmp1 M_op new_pc ⇒
588 opt_map ?? (get_indX_8_low_reg m t s_tmp1)
590 match plus_b8_dc_dc X_op (compl_b8 M_op) false with
592 let X7 ≝ MSB_b8 X_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
593 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
594 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 R_op 〈x0,x0〉) in
595 (* C = nX7&M7 | M7&R7 | R7&nX7 *)
596 let s_tmp3 ≝ set_c_flag m t s_tmp2 (((⊖X7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖X7))) in
598 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 R7 in
599 (* V = X7&nM7&nR7 | nX7&M7&R7 *)
600 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖X7)⊗M7⊗R7)) in
602 Some ? (pair ?? s_tmp5 new_pc) ] ) ]).
604 (* decimal adjiust A *)
605 (* per i dettagli vedere daa_b8 (modulo byte8) *)
606 ndefinition execute_DAA ≝
607 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
608 opt_map ?? (get_h_flag m t s)
610 let M_op ≝ get_acc_8_low_reg m t s in
611 match daa_b8 H (get_c_flag m t s) M_op with
614 let s_tmp1 ≝ set_acc_8_low_reg m t s R_op in
615 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
616 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 R_op 〈x0,x0〉) in
618 let s_tmp3 ≝ set_c_flag m t s_tmp2 carry in
620 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
622 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((MSB_b8 M_op) ⊙ (MSB_b8 R_op)) in
624 Some ? (pair ?? s_tmp5 cur_pc) ]).
626 (* if (--M)≠0, branch *)
627 ndefinition execute_DBNZ ≝
628 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
629 opt_map ?? (multi_mode_load false m t s cur_pc i)
630 (λS_M_PC.match S_M_PC with
631 [ triple s_tmp1 M_op new_pc ⇒
633 [ mk_word16 MH_op ML_op ⇒
635 let MH_op' ≝ pred_b8 MH_op in
636 opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i MH_op')
637 (λS_PC.match S_PC with
639 (* if (--M)≠0, branch *)
640 match eq_b8 MH_op' 〈x0,x0〉 with
641 (* new_pc = new_pc *)
642 [ true ⇒ Some ? (pair ?? s_tmp2 new_pc)
643 (* new_pc = new_pc + rel *)
644 | false ⇒ Some ? (pair ?? s_tmp2 (branched_pc m t s_tmp2 new_pc ML_op)) ]])]]).
647 ndefinition execute_DEC ≝
648 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
649 execute_COM_DEC_INC_NEG_aux m t s i cur_pc pred_b8
655 (* A = H:A/X, H = H:AmodX se non c'e' overflow, altrimenti invariati *)
656 (* per i dettagli vedere div_b8 (modulo word16) *)
657 ndefinition execute_DIV ≝
658 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
659 opt_map ?? (get_indX_8_high_reg m t s)
660 (λH_op.opt_map ?? (get_indX_8_low_reg m t s)
661 (λX_op.match div_b8 〈H_op:(get_acc_8_low_reg m t s)〉 X_op with
662 [ triple quoz rest overflow ⇒
664 let s_tmp1 ≝ set_c_flag m t s overflow in
666 let s_tmp2 ≝ match overflow with
668 | false ⇒ set_acc_8_low_reg m t s_tmp1 quoz ] in
669 (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
670 (* NB: che A sia cambiato o no, lo testa *)
671 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 (get_acc_8_low_reg m t s_tmp2) 〈x0,x0〉) in
672 (* H = H o H:AmodX *)
673 opt_map ?? (match overflow with
674 [ true ⇒ Some ? s_tmp3
675 | false ⇒ set_indX_8_high_reg m t s_tmp3 rest])
676 (λs_tmp4.Some ? (pair ?? s_tmp4 cur_pc)) ])).
679 ndefinition execute_EOR ≝
680 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
681 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true xor_b8.
684 ndefinition execute_INC ≝
685 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
686 execute_COM_DEC_INC_NEG_aux m t s i cur_pc succ_b8
692 (* jmp, il nuovo indirizzo e' una WORD *)
693 ndefinition execute_JMP ≝
694 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
695 opt_map ?? (multi_mode_load false m t s cur_pc i)
698 Some ? (pair ?? (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
700 (* jump to subroutine *)
701 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
702 ndefinition execute_JSR ≝
703 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
704 opt_map ?? (multi_mode_load false m t s cur_pc i)
705 (λS_M_PC.match S_M_PC with
706 [ triple s_tmp1 M_op new_pc ⇒ let aux ≝
707 (* push (new_pc low) *)
708 opt_map ?? (aux_push m t s_tmp1 (w16l new_pc))
709 (* push (new_pc high) *)
710 (λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
712 (λs_tmp3.Some ? (pair ?? s_tmp3 M_op)))
714 [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
717 opt_map ?? (set_spc_reg m t s_tmp1 new_pc)
719 (λs_tmp2.Some ? (pair ?? s_tmp2 M_op))
723 ndefinition execute_LDA ≝
724 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
725 opt_map ?? (multi_mode_load true m t s cur_pc i)
726 (λS_M_PC.match S_M_PC with
727 [ triple s_tmp1 M_op new_pc ⇒
729 let s_tmp2 ≝ set_acc_8_low_reg m t s_tmp1 M_op in
730 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
731 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 M_op 〈x0,x0〉) in
733 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 M_op) in
735 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
737 Some ? (pair ?? s_tmp5 new_pc) ]).
740 ndefinition execute_LDHX ≝
741 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
742 opt_map ?? (multi_mode_load false m t s cur_pc i)
743 (λS_M_PC.match S_M_PC with
744 [ triple s_tmp1 M_op new_pc ⇒
745 opt_map ?? (set_indX_16_reg m t s_tmp1 M_op)
747 (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
748 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_w16 M_op 〈〈x0,x0〉:〈x0,x0〉〉) in
750 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_w16 M_op) in
752 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
754 Some ? (pair ?? s_tmp5 new_pc)) ]).
757 ndefinition execute_LDX ≝
758 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
759 opt_map ?? (multi_mode_load true m t s cur_pc i)
760 (λS_M_PC.match S_M_PC with
761 [ triple s_tmp1 M_op new_pc ⇒
762 opt_map ?? (set_indX_8_low_reg m t s_tmp1 M_op)
764 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
765 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 M_op 〈x0,x0〉) in
767 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 M_op) in
769 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
771 Some ? (pair ?? s_tmp5 new_pc)) ]).
773 (* M = 0 -> rcr M -> C' *)
774 ndefinition execute_LSR ≝
775 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
776 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op false).
779 ndefinition execute_MOV ≝
780 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
782 opt_map ?? (multi_mode_load true m t s cur_pc i)
783 (λS_R_PC.match S_R_PC with
784 [ triple s_tmp1 R_op tmp_pc ⇒
786 opt_map ?? (multi_mode_write true m t s_tmp1 tmp_pc i R_op)
787 (λS_PC.match S_PC with
788 [ pair s_tmp2 new_pc ⇒
789 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
790 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
792 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
794 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
796 Some ? (pair ?? s_tmp5 new_pc)])]).
799 ndefinition execute_MUL ≝
800 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
801 opt_map ?? (get_indX_8_low_reg m t s)
802 (λX_op.let R_op ≝ mul_b8 X_op (get_acc_8_low_reg m t s) in
803 opt_map ?? (set_indX_8_low_reg m t s (w16h R_op))
804 (λs_tmp.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
807 ndefinition execute_NEG ≝
808 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
809 execute_COM_DEC_INC_NEG_aux m t s i cur_pc compl_b8
812 (* fC = R7|R6|R5|R4|R3|R2|R1|R0 *)
813 (λC_op.λR_op.⊖(eq_b8 R_op 〈x0,x0〉)).
816 ndefinition execute_NOP ≝
817 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
818 Some ? (pair ?? s cur_pc).
820 (* A = (mk_byte8 (b8l A) (b8h A)) *)
821 (* cioe' swap del nibble alto/nibble basso di A *)
822 ndefinition execute_NSA ≝
823 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
824 match get_acc_8_low_reg m t s with [ mk_byte8 ah al ⇒
825 (* A = (mk_byte8 (b8l A) (b8h A)) *)
826 Some ? (pair ?? (set_acc_8_low_reg m t s 〈al,ah〉) cur_pc) ].
829 ndefinition execute_ORA ≝
830 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
831 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true or_b8.
834 ndefinition execute_PSHA ≝
835 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
836 opt_map ?? (aux_push m t s (get_acc_8_low_reg m t s))
837 (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc)).
840 ndefinition execute_PSHH ≝
841 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
842 opt_map ?? (get_indX_8_high_reg m t s)
843 (λH_op.opt_map ?? (aux_push m t s H_op)
844 (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc))).
847 ndefinition execute_PSHX ≝
848 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
849 opt_map ?? (get_indX_8_low_reg m t s)
850 (λH_op.opt_map ?? (aux_push m t s H_op)
851 (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc))).
854 ndefinition execute_PULA ≝
855 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
856 opt_map ?? (aux_pop m t s)
857 (λS_and_A.match S_and_A with [ pair s_tmp1 A_op ⇒
858 Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 A_op) cur_pc) ]).
861 ndefinition execute_PULH ≝
862 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
863 opt_map ?? (aux_pop m t s)
864 (λS_and_H.match S_and_H with [ pair s_tmp1 H_op ⇒
865 opt_map ?? (set_indX_8_high_reg m t s_tmp1 H_op)
866 (λs_tmp2.Some ? (pair ?? s_tmp2 cur_pc))]).
869 ndefinition execute_PULX ≝
870 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
871 opt_map ?? (aux_pop m t s)
872 (λS_and_X.match S_and_X with [ pair s_tmp1 X_op ⇒
873 opt_map ?? (set_indX_8_low_reg m t s_tmp1 X_op)
874 (λs_tmp2.Some ? (pair ?? s_tmp2 cur_pc))]).
876 (* M = C' <- rcl M <- C *)
877 ndefinition execute_ROL ≝
878 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
879 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcl_b8 M_op C_op).
881 (* M = C -> rcr M -> C' *)
882 ndefinition execute_ROR ≝
883 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
884 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op C_op).
887 (* lascia inalterato il byte superiore di SP *)
888 ndefinition execute_RSP ≝
889 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
890 opt_map ?? (get_sp_reg m t s)
891 (λSP_op.match SP_op with [ mk_word16 sph spl ⇒
892 opt_map ?? (set_sp_reg m t s 〈sph:〈xF,xF〉〉)
893 (λs_tmp.Some ? (pair ?? s_tmp cur_pc))]).
895 (* return from interrupt *)
896 ndefinition execute_RTI ≝
897 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
899 opt_map ?? (aux_pop m t s)
900 (λS_and_CCR.match S_and_CCR with [ pair s_tmp1 CCR_op ⇒
901 let s_tmp2 ≝ aux_set_CCR m t s_tmp1 CCR_op in
903 opt_map ?? (aux_pop m t s_tmp2)
904 (λS_and_A.match S_and_A with [ pair s_tmp3 A_op ⇒
905 let s_tmp4 ≝ set_acc_8_low_reg m t s_tmp3 A_op in
907 opt_map ?? (aux_pop m t s_tmp4)
908 (λS_and_X.match S_and_X with [ pair s_tmp5 X_op ⇒
909 opt_map ?? (set_indX_8_low_reg m t s_tmp5 X_op)
911 (λs_tmp6.opt_map ?? (aux_pop m t s_tmp6)
912 (λS_and_PCH.match S_and_PCH with [ pair s_tmp7 PCH_op ⇒
914 opt_map ?? (aux_pop m t s_tmp7)
915 (λS_and_PCL.match S_and_PCL with [ pair s_tmp8 PCL_op ⇒
916 Some ? (pair ?? s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
918 (* return from subroutine *)
919 (* HC05/HC08/HCS08 si appoggia allo stack, RS08 si appoggia a SPC *)
920 ndefinition execute_RTS ≝
921 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
924 opt_map ?? (aux_pop m t s)
925 (λS_and_PCH.match S_and_PCH with [ pair s_tmp1 PCH_op ⇒
927 opt_map ?? (aux_pop m t s_tmp1)
928 (λS_and_PCL.match S_and_PCL with [ pair s_tmp2 PCL_op ⇒
929 Some ? (pair ?? s_tmp2 〈PCH_op:PCL_op〉)])])
931 [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
934 opt_map ?? (get_spc_reg m t s)
935 (λSPC_op.Some ? (pair ?? s SPC_op))
939 ndefinition execute_SBC ≝
940 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
941 execute_SBC_SUB_aux m t s i cur_pc true
942 (λA_op.λM_op.λC_op.match plus_b8_dc_dc A_op (compl_b8 M_op) false with
943 [ pair resb resc ⇒ match C_op with
944 [ true ⇒ plus_b8_dc_dc resb 〈xF,xF〉 false
945 | false ⇒ pair ?? resb resc ]]).
948 ndefinition execute_SEC ≝
949 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
950 Some ? (pair ?? (set_c_flag m t s true) cur_pc).
953 ndefinition execute_SEI ≝
954 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
955 opt_map ?? (set_i_flag m t s true)
956 (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
959 (* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
960 fare subroutine annidate se RA (return address) e' salvato sempre in SPC?
961 occore accedere a SPC e salvarne il contenuto *)
962 ndefinition execute_SHA ≝
963 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
964 opt_map ?? (get_spc_reg m t s)
965 (λSPC_op.opt_map ?? (set_spc_reg m t s 〈(get_acc_8_low_reg m t s):(w16l SPC_op)〉)
966 (λs_tmp1.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 (w16h SPC_op)) cur_pc))).
969 (* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
970 fare subroutine annidate se RA (return address) e' salvato sempre in SPC?
971 occore accedere a SPC e salvarne il contenuto *)
972 ndefinition execute_SLA ≝
973 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
974 opt_map ?? (get_spc_reg m t s)
975 (λSPC_op.opt_map ?? (set_spc_reg m t s 〈(w16h SPC_op):(get_acc_8_low_reg m t s)〉)
976 (λs_tmp1.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
979 ndefinition execute_STA ≝
980 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
982 let A_op ≝ (get_acc_8_low_reg m t s) in
983 opt_map ?? (multi_mode_write true m t s cur_pc i A_op)
984 (λS_op_and_PC.match S_op_and_PC with
985 [ pair s_tmp1 new_pc ⇒
986 (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
987 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 A_op 〈x0,x0〉) in
989 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 A_op) in
991 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
993 Some ? (pair ?? s_tmp4 new_pc) ]).
996 ndefinition execute_STHX ≝
997 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
999 opt_map ?? (get_indX_16_reg m t s)
1000 (λX_op.opt_map ?? (multi_mode_write false m t s cur_pc i X_op)
1001 (λS_op_and_PC.match S_op_and_PC with
1002 [ pair s_tmp1 new_pc ⇒
1003 (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1004 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 X_op 〈〈x0,x0〉:〈x0,x0〉〉) in
1006 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_w16 X_op) in
1008 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
1009 (* newpc = nextpc *)
1010 Some ? (pair ?? s_tmp4 new_pc) ])).
1013 ndefinition execute_STOP ≝
1014 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1015 Some ? (pair ?? (setweak_i_flag m t s false) cur_pc).
1018 ndefinition execute_STX ≝
1019 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1021 opt_map ?? (get_indX_8_low_reg m t s)
1022 (λX_op.opt_map ?? (multi_mode_write true m t s cur_pc i X_op)
1023 (λS_op_and_PC.match S_op_and_PC with
1024 [ pair s_tmp1 new_pc ⇒
1025 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1026 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 X_op 〈x0,x0〉) in
1028 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 X_op) in
1030 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
1031 (* newpc = nextpc *)
1032 Some ? (pair ?? s_tmp4 new_pc) ])).
1035 ndefinition execute_SUB ≝
1036 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1037 execute_SBC_SUB_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8_dc_dc A_op (compl_b8 M_op) false).
1039 (* software interrupt *)
1040 ndefinition execute_SWI ≝
1041 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1042 (* indirizzo da cui caricare il nuovo pc *)
1043 let vector ≝ get_pc_reg m t (set_pc_reg m t s 〈〈xF,xF〉:〈xF,xC〉〉) in
1044 (* push (cur_pc low) *)
1045 opt_map ?? (aux_push m t s (w16l cur_pc))
1046 (* push (cur_pc high *)
1047 (λs_tmp1.opt_map ?? (aux_push m t s_tmp1 (w16h cur_pc))
1048 (λs_tmp2.opt_map ?? (get_indX_8_low_reg m t s_tmp2)
1050 (λX_op.opt_map ?? (aux_push m t s_tmp2 X_op)
1052 (λs_tmp3.opt_map ?? (aux_push m t s_tmp3 (get_acc_8_low_reg m t s_tmp3))
1054 (λs_tmp4.opt_map ?? (aux_push m t s_tmp4 (aux_get_CCR m t s_tmp4))
1056 (λs_tmp5.opt_map ?? (set_i_flag m t s_tmp5 true)
1057 (* load from vector high *)
1058 (λs_tmp6.opt_map ?? (memory_filter_read m t s_tmp6 vector)
1059 (* load from vector low *)
1060 (λaddrh.opt_map ?? (memory_filter_read m t s_tmp6 (succ_w16 vector))
1061 (* newpc = [vector] *)
1062 (λaddrl.Some ? (pair ?? s_tmp6 〈addrh:addrl〉)))))))))).
1065 ndefinition execute_TAP ≝
1066 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1067 Some ? (pair ?? (aux_set_CCR m t s (get_acc_8_low_reg m t s)) cur_pc).
1070 ndefinition execute_TAX ≝
1071 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1072 opt_map ?? (set_indX_8_low_reg m t s (get_acc_8_low_reg m t s))
1073 (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
1076 ndefinition execute_TPA ≝
1077 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1078 Some ? (pair ?? (set_acc_8_low_reg m t s (aux_get_CCR m t s)) cur_pc).
1081 (* implementata senza richiamare la sottrazione, la modifica dei flag
1083 ndefinition execute_TST ≝
1084 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1085 opt_map ?? (multi_mode_load true m t s cur_pc i)
1086 (λS_M_PC.match S_M_PC with
1087 [ triple s_tmp1 M_op new_pc ⇒
1088 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1089 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 M_op 〈x0,x0〉) in
1091 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 M_op) in
1093 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
1094 (* newpc = nextpc *)
1095 Some ? (pair ?? s_tmp4 new_pc) ]).
1098 ndefinition execute_TSX ≝
1099 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1100 opt_map ?? (get_sp_reg m t s )
1101 (λSP_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 SP_op))
1103 (λs_tmp.Some ? (pair ?? s_tmp cur_pc))).
1106 ndefinition execute_TXA ≝
1107 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1108 opt_map ?? (get_indX_8_low_reg m t s)
1109 (λX_op.Some ? (pair ?? (set_acc_8_low_reg m t s X_op) cur_pc)).
1112 ndefinition execute_TXS ≝
1113 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1114 opt_map ?? (get_indX_16_reg m t s )
1115 (λX_op.opt_map ?? (set_sp_reg m t s (pred_w16 X_op))
1117 (λs_tmp.Some ? (pair ?? s_tmp cur_pc))).
1120 ndefinition execute_WAIT ≝
1121 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1122 Some ? (pair ?? (setweak_i_flag m t s false) cur_pc).
1128 (* enumerazione delle possibili modalita' di sospensione *)
1129 ninductive susp_type : Type ≝
1130 BGND_MODE: susp_type
1131 | STOP_MODE: susp_type
1132 | WAIT_MODE: susp_type.
1134 (* un tipo opzione ad hoc
1135 - errore: errore+stato (seguira' reset o ??, cmq lo stato non va buttato)
1136 - sospensione: sospensione+stato (seguira' resume o ??)
1139 ninductive tick_result (A:Type) : Type ≝
1140 TickERR : A → error_type → tick_result A
1141 | TickSUSP : A → susp_type → tick_result A
1142 | TickOK : A → tick_result A.
1144 (* sostanazialmente simula
1145 - fetch/decode/execute
1146 - l'esecuzione e' considerata atomica quindi nel caso di un'instruzione
1147 da 3 cicli la successione sara'
1148 ([fetch/decode] s,clk:None) →
1149 ( s,clk:Some 1,pseudo,mode,3,cur_pc) →
1150 ( s,clk:Some 2,pseudo,mode,3,cur_pc) →
1151 ([execute] s',clk:None) *)
1153 ndefinition tick_execute ≝
1154 λm:mcu_type.λt:memory_impl.λs:any_status m t.
1155 λpseudo:any_opcode m.λmode:instr_mode.λcur_pc:word16.
1156 let abs_pseudo ≝ match pseudo with [ anyOP pseudo' ⇒ pseudo' ] in
1157 let a_status_and_fetch ≝ match abs_pseudo with
1158 [ ADC ⇒ execute_ADC m t s mode cur_pc (* add with carry *)
1159 | ADD ⇒ execute_ADD m t s mode cur_pc (* add *)
1160 | AIS ⇒ execute_AIS m t s mode cur_pc (* add immediate to SP *)
1161 | AIX ⇒ execute_AIX m t s mode cur_pc (* add immediate to X *)
1162 | AND ⇒ execute_AND m t s mode cur_pc (* and *)
1163 | ASL ⇒ execute_ASL m t s mode cur_pc (* aritmetic shift left *)
1164 | ASR ⇒ execute_ASR m t s mode cur_pc (* aritmetic shift right *)
1165 | BCC ⇒ execute_BCC m t s mode cur_pc (* branch if C=0 *)
1166 | BCLRn ⇒ execute_BCLRn m t s mode cur_pc (* clear bit n *)
1167 | BCS ⇒ execute_BCS m t s mode cur_pc (* branch if C=1 *)
1168 | BEQ ⇒ execute_BEQ m t s mode cur_pc (* branch if Z=1 *)
1169 | BGE ⇒ execute_BGE m t s mode cur_pc (* branch if N⊙V=0 (great or equal) *)
1170 | BGND ⇒ execute_BGND m t s mode cur_pc (* !!background mode!!*)
1171 | BGT ⇒ execute_BGT m t s mode cur_pc (* branch if Z|N⊙V=0 clear (great) *)
1172 | BHCC ⇒ execute_BHCC m t s mode cur_pc (* branch if H=0 *)
1173 | BHCS ⇒ execute_BHCS m t s mode cur_pc (* branch if H=1 *)
1174 | BHI ⇒ execute_BHI m t s mode cur_pc (* branch if C|Z=0, (higher) *)
1175 | BIH ⇒ execute_BIH m t s mode cur_pc (* branch if nIRQ=1 *)
1176 | BIL ⇒ execute_BIL m t s mode cur_pc (* branch if nIRQ=0 *)
1177 | BIT ⇒ execute_BIT m t s mode cur_pc (* flag = and (bit test) *)
1178 | BLE ⇒ execute_BLE m t s mode cur_pc (* branch if Z|N⊙V=1 (less or equal) *)
1179 | BLS ⇒ execute_BLS m t s mode cur_pc (* branch if C|Z=1 (lower or same) *)
1180 | BLT ⇒ execute_BLT m t s mode cur_pc (* branch if N⊙1=1 (less) *)
1181 | BMC ⇒ execute_BMC m t s mode cur_pc (* branch if I=0 (interrupt mask clear) *)
1182 | BMI ⇒ execute_BMI m t s mode cur_pc (* branch if N=1 (minus) *)
1183 | BMS ⇒ execute_BMS m t s mode cur_pc (* branch if I=1 (interrupt mask set) *)
1184 | BNE ⇒ execute_BNE m t s mode cur_pc (* branch if Z=0 *)
1185 | BPL ⇒ execute_BPL m t s mode cur_pc (* branch if N=0 (plus) *)
1186 | BRA ⇒ execute_BRA m t s mode cur_pc (* branch always *)
1187 | BRCLRn ⇒ execute_BRCLRn m t s mode cur_pc (* branch if bit n clear *)
1188 | BRN ⇒ execute_BRN m t s mode cur_pc (* branch never (nop) *)
1189 | BRSETn ⇒ execute_BRSETn m t s mode cur_pc (* branch if bit n set *)
1190 | BSETn ⇒ execute_BSETn m t s mode cur_pc (* set bit n *)
1191 | BSR ⇒ execute_BSR m t s mode cur_pc (* branch to subroutine *)
1192 | CBEQA ⇒ execute_CBEQA m t s mode cur_pc (* compare (A) and BEQ *)
1193 | CBEQX ⇒ execute_CBEQX m t s mode cur_pc (* compare (X) and BEQ *)
1194 | CLC ⇒ execute_CLC m t s mode cur_pc (* C=0 *)
1195 | CLI ⇒ execute_CLI m t s mode cur_pc (* I=0 *)
1196 | CLR ⇒ execute_CLR m t s mode cur_pc (* operand=0 *)
1197 | CMP ⇒ execute_CMP m t s mode cur_pc (* flag = sub (compare A) *)
1198 | COM ⇒ execute_COM m t s mode cur_pc (* not (1 complement) *)
1199 | CPHX ⇒ execute_CPHX m t s mode cur_pc (* flag = sub (compare H:X) *)
1200 | CPX ⇒ execute_CPX m t s mode cur_pc (* flag = sub (compare X) *)
1201 | DAA ⇒ execute_DAA m t s mode cur_pc (* decimal adjust A *)
1202 | DBNZ ⇒ execute_DBNZ m t s mode cur_pc (* dec and BNE *)
1203 | DEC ⇒ execute_DEC m t s mode cur_pc (* operand=operand-1 (decrement) *)
1204 | DIV ⇒ execute_DIV m t s mode cur_pc (* div *)
1205 | EOR ⇒ execute_EOR m t s mode cur_pc (* xor *)
1206 | INC ⇒ execute_INC m t s mode cur_pc (* operand=operand+1 (increment) *)
1207 | JMP ⇒ execute_JMP m t s mode cur_pc (* jmp word [operand] *)
1208 | JSR ⇒ execute_JSR m t s mode cur_pc (* jmp to subroutine *)
1209 | LDA ⇒ execute_LDA m t s mode cur_pc (* load in A *)
1210 | LDHX ⇒ execute_LDHX m t s mode cur_pc (* load in H:X *)
1211 | LDX ⇒ execute_LDX m t s mode cur_pc (* load in X *)
1212 | LSR ⇒ execute_LSR m t s mode cur_pc (* logical shift right *)
1213 | MOV ⇒ execute_MOV m t s mode cur_pc (* move *)
1214 | MUL ⇒ execute_MUL m t s mode cur_pc (* mul *)
1215 | NEG ⇒ execute_NEG m t s mode cur_pc (* neg (2 complement) *)
1216 | NOP ⇒ execute_NOP m t s mode cur_pc (* nop *)
1217 | NSA ⇒ execute_NSA m t s mode cur_pc (* nibble swap A (al:ah <- ah:al) *)
1218 | ORA ⇒ execute_ORA m t s mode cur_pc (* or *)
1219 | PSHA ⇒ execute_PSHA m t s mode cur_pc (* push A *)
1220 | PSHH ⇒ execute_PSHH m t s mode cur_pc (* push H *)
1221 | PSHX ⇒ execute_PSHX m t s mode cur_pc (* push X *)
1222 | PULA ⇒ execute_PULA m t s mode cur_pc (* pop A *)
1223 | PULH ⇒ execute_PULH m t s mode cur_pc (* pop H *)
1224 | PULX ⇒ execute_PULX m t s mode cur_pc (* pop X *)
1225 | ROL ⇒ execute_ROL m t s mode cur_pc (* rotate left *)
1226 | ROR ⇒ execute_ROR m t s mode cur_pc (* rotate right *)
1227 | RSP ⇒ execute_RSP m t s mode cur_pc (* reset SP (0x00FF) *)
1228 | RTI ⇒ execute_RTI m t s mode cur_pc (* return from interrupt *)
1229 | RTS ⇒ execute_RTS m t s mode cur_pc (* return from subroutine *)
1230 | SBC ⇒ execute_SBC m t s mode cur_pc (* sub with carry*)
1231 | SEC ⇒ execute_SEC m t s mode cur_pc (* C=1 *)
1232 | SEI ⇒ execute_SEI m t s mode cur_pc (* I=1 *)
1233 | SHA ⇒ execute_SHA m t s mode cur_pc (* swap spc_high,A *)
1234 | SLA ⇒ execute_SLA m t s mode cur_pc (* swap spc_low,A *)
1235 | STA ⇒ execute_STA m t s mode cur_pc (* store from A *)
1236 | STHX ⇒ execute_STHX m t s mode cur_pc (* store from H:X *)
1237 | STOP ⇒ execute_STOP m t s mode cur_pc (* !!stop mode!! *)
1238 | STX ⇒ execute_STX m t s mode cur_pc (* store from X *)
1239 | SUB ⇒ execute_SUB m t s mode cur_pc (* sub *)
1240 | SWI ⇒ execute_SWI m t s mode cur_pc (* software interrupt *)
1241 | TAP ⇒ execute_TAP m t s mode cur_pc (* flag=A (transfer A to process status byte *)
1242 | TAX ⇒ execute_TAX m t s mode cur_pc (* X=A (transfer A to X) *)
1243 | TPA ⇒ execute_TPA m t s mode cur_pc (* A=flag (transfer process status byte to A) *)
1244 | TST ⇒ execute_TST m t s mode cur_pc (* flag = sub (test) *)
1245 | TSX ⇒ execute_TSX m t s mode cur_pc (* X:H=SP (transfer SP to H:X) *)
1246 | TXA ⇒ execute_TXA m t s mode cur_pc (* A=X (transfer X to A) *)
1247 | TXS ⇒ execute_TXS m t s mode cur_pc (* SP=X:H (transfer H:X to SP) *)
1248 | WAIT ⇒ execute_WAIT m t s mode cur_pc (* !!wait mode!!*)
1249 ] in match a_status_and_fetch with
1250 (* errore nell'execute (=caricamento argomenti)? riportato in output *)
1251 (* nessun avanzamento e clk a None *)
1252 [ None ⇒ TickERR ? (set_clk_desc m t s (None ?)) ILL_EX_AD
1253 | Some status_and_newpc ⇒
1254 (* aggiornamento centralizzato di pc e clk *)
1255 match status_and_newpc with
1256 [ pair s_tmp1 new_pc ⇒
1257 let s_tmp2 ≝ set_pc_reg m t s_tmp1 new_pc in
1258 let s_tmp3 ≝ set_clk_desc m t s_tmp2 (None ?) in
1259 (* distinzione fra le 4 modalita' possibili, normale/BGND/STOP/WAIT *)
1260 match eq_op abs_pseudo BGND with
1261 [ true ⇒ TickSUSP ? s_tmp3 BGND_MODE
1262 | false ⇒ match eq_op abs_pseudo STOP with
1263 [ true ⇒ TickSUSP ? s_tmp3 STOP_MODE
1264 | false ⇒ match eq_op abs_pseudo WAIT with
1265 [ true ⇒ TickSUSP ? s_tmp3 WAIT_MODE
1266 | false ⇒ TickOK ? s_tmp3
1270 λm:mcu_type.λt:memory_impl.λs:any_status m t.
1271 let opt_info ≝ get_clk_desc m t s in
1273 (* e' il momento del fetch *)
1274 [ None ⇒ match fetch m t s with
1275 (* errore nel fetch/decode? riportato in output, nessun avanzamento *)
1276 [ FetchERR err ⇒ TickERR ? s err
1277 (* nessun errore nel fetch *)
1278 | FetchOK fetch_info cur_pc ⇒ match fetch_info with
1279 [ quadruple pseudo mode _ tot_clk ⇒
1280 match eq_b8 〈x0,x1〉 tot_clk with
1281 (* un solo clk, execute subito *)
1282 [ true ⇒ tick_execute m t s pseudo mode cur_pc
1283 (* piu' clk, execute rimandata *)
1284 | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple ????? 〈x0,x1〉 pseudo mode tot_clk cur_pc)))
1288 (* il fetch e' gia' stato eseguito, e' il turno di execute? *)
1289 | Some info ⇒ match info with [ quintuple cur_clk pseudo mode tot_clk cur_pc ⇒
1290 match eq_b8 (succ_b8 cur_clk) tot_clk with
1292 [ true ⇒ tick_execute m t s pseudo mode cur_pc
1293 (* no, avanzamento cur_clk *)
1294 | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple ????? (succ_b8 cur_clk) pseudo mode tot_clk cur_pc)))
1303 nlet rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
1305 [ TickERR s' error ⇒ TickERR ? s' error
1306 | TickSUSP s' susp ⇒ TickSUSP ? s' susp
1307 | TickOK s' ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ]
1310 nlemma breakpoint_err : ∀m,t,s,err,n.execute m t (TickERR ? s err) n = TickERR ? s err.
1311 #m; #t; #s; #err; #n;
1315 napply (refl_eq ??).
1318 nlemma breakpoint_susp : ∀m,t,s,susp,n.execute m t (TickSUSP ? s susp) n = TickSUSP ? s susp.
1319 #m; #t; #s; #susp; #n;
1323 napply (refl_eq ??).
1327 ∀m,t,n1,n2,s. execute m t s (n1 + n2) = execute m t (execute m t s n1) n2.
1330 ##[ ##1: nnormalize; #n2; #s; ncases s; nnormalize; ##[ ##1,2: #x ##] #y; napply (refl_eq ??)
1331 ##| ##2: #n3; #H; #n2; #s; ncases s;
1332 ##[ ##1: #x; #y; nnormalize; nrewrite > (breakpoint_err m t x y n2); napply (refl_eq ??)
1333 ##| ##2: #x; #y; nnormalize; nrewrite > (breakpoint_susp m t x y n2); napply (refl_eq ??)
1334 ##| ##3: #x; nrewrite > (Sn_p_n_to_S_npn n3 n2);
1335 nchange with ((execute m t (tick m t x) (n3+n2)) =
1336 (execute m t (execute m t (tick m t x) n3) n2));
1337 nrewrite > (H n2 (tick m t x));