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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "emulator/status/status.ma".
25 (* ***************************** *)
26 (* SETTER SPECIFICI FORTI/DEBOLI *)
27 (* ***************************** *)
29 (* funzione ausiliaria per il tipaggio dei setter forti *)
30 ndefinition aux_set_type ≝ λx:Type.λm:mcu_type.
31 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
32 | IP2022 ⇒ alu_IP2022 ]
34 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
35 | IP2022 ⇒ alu_IP2022 ].
37 (* funzione ausiliaria per il tipaggio dei setter deboli *)
38 ndefinition aux_set_type_opt ≝ λx:Type.λm:mcu_type.option
39 (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
40 | IP2022 ⇒ alu_IP2022 ]
42 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
43 | IP2022 ⇒ alu_IP2022 ]).
45 (* DESCRITTORI ESTERNI ALLA ALU *)
47 (* setter forte della ALU *)
49 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
50 mk_any_status m t alu' (mem_desc m t s) (chk_desc m t s) (clk_desc m t s).
52 (* setter forte della memoria *)
53 ndefinition set_mem_desc ≝
54 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
55 mk_any_status m t (alu m t s) mem' (chk_desc m t s) (clk_desc m t s).
57 (* setter forte del descrittore *)
58 ndefinition set_chk_desc ≝
59 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
60 mk_any_status m t (alu m t s) (mem_desc m t s) chk' (clk_desc m t s).
62 (* setter forte del clik *)
63 ndefinition set_clk_desc ≝
64 λm:mcu_type.λt:memory_impl.λs:any_status m t.
65 λclk':option (aux_clk_type m).
66 mk_any_status m t (alu m t s) (mem_desc m t s) (chk_desc m t s) clk'.
70 (* setter forte di A *)
71 ndefinition set_acc_8_low_reg ≝
72 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
74 (match m return aux_set_type byte8 with
75 [ HC05 ⇒ set_acc_8_low_reg_HC05
76 | HC08 ⇒ set_acc_8_low_reg_HC08
77 | HCS08 ⇒ set_acc_8_low_reg_HC08
78 | RS08 ⇒ set_acc_8_low_reg_RS08
79 | IP2022 ⇒ set_acc_8_low_reg_IP2022
84 ndefinition set_indX_8_low_reg_sHC05 ≝
85 λt:memory_impl.λs:any_status HC05 t.λval.
86 set_alu … s (set_indX_8_low_reg_HC05 (alu … s) val).
88 ndefinition set_indX_8_low_reg_sHC08 ≝
89 λt:memory_impl.λs:any_status HC08 t.λval.
90 set_alu … s (set_indX_8_low_reg_HC08 (alu … s) val).
92 ndefinition set_indX_8_low_reg_sHCS08 ≝
93 λt:memory_impl.λs:any_status HCS08 t.λval.
94 set_alu … s (set_indX_8_low_reg_HC08 (alu … s) val).
96 (* setter forte di X *)
97 ndefinition set_indX_8_low_reg ≝
100 return λm.any_status m t → byte8 → option (any_status m t)
102 [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHC05 t s val)
103 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHC08 t s val)
104 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHCS08 t s val)
105 | RS08 ⇒ λs:any_status ? t.λval.None ?
106 | IP2022 ⇒ λs:any_status ? t.λval.None ?
109 (* setter debole di X *)
110 ndefinition setweak_indX_8_low_reg ≝
111 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
112 match set_indX_8_low_reg m t s val with
113 [ None ⇒ s | Some s' ⇒ s' ].
117 ndefinition set_indX_8_high_reg_sHC08 ≝
118 λt:memory_impl.λs:any_status HC08 t.λval.
119 set_alu … s (set_indX_8_high_reg_HC08 (alu … s) val).
121 ndefinition set_indX_8_high_reg_sHCS08 ≝
122 λt:memory_impl.λs:any_status HCS08 t.λval.
123 set_alu … s (set_indX_8_high_reg_HC08 (alu … s) val).
125 (* setter forte di H *)
126 ndefinition set_indX_8_high_reg ≝
129 return λm.any_status m t → byte8 → option (any_status m t)
131 [ HC05 ⇒ λs:any_status ? t.λval.None ?
132 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_high_reg_sHC08 t s val)
133 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_high_reg_sHCS08 t s val)
134 | RS08 ⇒ λs:any_status ? t.λval.None ?
135 | IP2022 ⇒ λs:any_status ? t.λval.None ?
138 (* setter debole di H *)
139 ndefinition setweak_indX_8_high_reg ≝
140 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
141 match set_indX_8_high_reg m t s val with
142 [ None ⇒ s | Some s' ⇒ s' ].
146 ndefinition set_indX_16_reg_sHC08 ≝
147 λt:memory_impl.λs:any_status HC08 t.λval.
148 set_alu … s (set_indX_16_reg_HC08 (alu … s) val).
150 ndefinition set_indX_16_reg_sHCS08 ≝
151 λt:memory_impl.λs:any_status HCS08 t.λval.
152 set_alu … s (set_indX_16_reg_HC08 (alu … s) val).
154 (* setter forte di H:X *)
155 ndefinition set_indX_16_reg ≝
158 return λm.any_status m t → word16 → option (any_status m t)
160 [ HC05 ⇒ λs:any_status ? t.λval.None ?
161 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_16_reg_sHC08 t s val)
162 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_16_reg_sHCS08 t s val)
163 | RS08 ⇒ λs:any_status ? t.λval.None ?
164 | IP2022 ⇒ λs:any_status ? t.λval.None ?
167 (* setter debole di H:X *)
168 ndefinition setweak_indX_16_reg ≝
169 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
170 match set_indX_16_reg m t s val with
171 [ None ⇒ s | Some s' ⇒ s' ].
175 ndefinition set_sp_reg_sHC05 ≝
176 λt:memory_impl.λs:any_status HC05 t.λval.
177 set_alu … s (set_sp_reg_HC05 (alu … s) val).
179 ndefinition set_sp_reg_sHC08 ≝
180 λt:memory_impl.λs:any_status HC08 t.λval.
181 set_alu … s (set_sp_reg_HC08 (alu … s) val).
183 ndefinition set_sp_reg_sHCS08 ≝
184 λt:memory_impl.λs:any_status HCS08 t.λval.
185 set_alu … s (set_sp_reg_HC08 (alu … s) val).
187 ndefinition set_sp_reg_sIP2022 ≝
188 λt:memory_impl.λs:any_status IP2022 t.λval.
189 set_alu … s (set_sp_reg_IP2022 (alu … s) val).
191 (* setter forte di SP *)
192 ndefinition set_sp_reg ≝
195 return λm.any_status m t → word16 → option (any_status m t)
197 [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHC05 t s val)
198 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHC08 t s val)
199 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHCS08 t s val)
200 | RS08 ⇒ λs:any_status ? t.λval.None ?
201 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sIP2022 t s val)
204 (* setter debole di SP *)
205 ndefinition setweak_sp_reg ≝
206 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
207 match set_sp_reg m t s val with
208 [ None ⇒ s | Some s' ⇒ s' ].
212 (* setter forte di PC *)
213 ndefinition set_pc_reg ≝
214 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
216 (match m return aux_set_type word16 with
217 [ HC05 ⇒ set_pc_reg_HC05
218 | HC08 ⇒ set_pc_reg_HC08
219 | HCS08 ⇒ set_pc_reg_HC08
220 | RS08 ⇒ set_pc_reg_RS08
221 | IP2022 ⇒ set_pc_reg_IP2022
226 ndefinition set_spc_reg_sRS08 ≝
227 λt:memory_impl.λs:any_status RS08 t.λval.
228 set_alu … s (set_spc_reg_RS08 (alu … s) val).
230 (* setter forte di SPC *)
231 ndefinition set_spc_reg ≝
234 return λm.any_status m t → word16 → option (any_status m t)
236 [ HC05 ⇒ λs:any_status ? t.λval.None ?
237 | HC08 ⇒ λs:any_status ? t.λval.None ?
238 | HCS08 ⇒ λs:any_status ? t.λval.None ?
239 | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_spc_reg_sRS08 t s val)
240 | IP2022 ⇒ λs:any_status ? t.λval.None ?
243 (* setter debole di SPC *)
244 ndefinition setweak_spc_reg ≝
245 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
246 match set_spc_reg m t s val with
247 [ None ⇒ s | Some s' ⇒ s' ].
251 ndefinition set_mulh_reg_sIP2022 ≝
252 λt:memory_impl.λs:any_status IP2022 t.λval.
253 set_alu … s (set_mulh_reg_IP2022 (alu … s) val).
255 (* setter forte di MULH *)
256 ndefinition set_mulh_reg ≝
259 return λm.any_status m t → byte8 → option (any_status m t)
261 [ HC05 ⇒ λs:any_status ? t.λval.None ?
262 | HC08 ⇒ λs:any_status ? t.λval.None ?
263 | HCS08 ⇒ λs:any_status ? t.λval.None ?
264 | RS08 ⇒ λs:any_status ? t.λval.None ?
265 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_mulh_reg_sIP2022 t s val)
268 (* setter debole di MULH *)
269 ndefinition setweak_mulh_reg ≝
270 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
271 match set_mulh_reg m t s val with
272 [ None ⇒ s | Some s' ⇒ s' ].
274 (* REGISTRO ADDRSEL *)
276 ndefinition set_addrsel_reg_sIP2022 ≝
277 λt:memory_impl.λs:any_status IP2022 t.λval.
278 set_alu … s (set_addrsel_reg_IP2022 (alu … s) val).
280 (* setter forte di ADDRSEL *)
281 ndefinition set_addrsel_reg ≝
284 return λm.any_status m t → byte8 → option (any_status m t)
286 [ HC05 ⇒ λs:any_status ? t.λval.None ?
287 | HC08 ⇒ λs:any_status ? t.λval.None ?
288 | HCS08 ⇒ λs:any_status ? t.λval.None ?
289 | RS08 ⇒ λs:any_status ? t.λval.None ?
290 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_addrsel_reg_sIP2022 t s val)
293 (* setter debole di ADDRSEL *)
294 ndefinition setweak_addrsel_reg ≝
295 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
296 match set_addrsel_reg m t s val with
297 [ None ⇒ s | Some s' ⇒ s' ].
301 ndefinition set_addr_reg_sIP2022 ≝
302 λt:memory_impl.λs:any_status IP2022 t.λval.
303 set_alu … s (set_addr_reg_IP2022 (alu … s) val).
305 (* setter forte di ADDR *)
306 ndefinition set_addr_reg ≝
309 return λm.any_status m t → word24 → option (any_status m t)
311 [ HC05 ⇒ λs:any_status ? t.λval.None ?
312 | HC08 ⇒ λs:any_status ? t.λval.None ?
313 | HCS08 ⇒ λs:any_status ? t.λval.None ?
314 | RS08 ⇒ λs:any_status ? t.λval.None ?
315 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_addr_reg_sIP2022 t s val)
318 (* setter debole di ADDR *)
319 ndefinition setweak_addr_reg ≝
320 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
321 match set_addr_reg m t s val with
322 [ None ⇒ s | Some s' ⇒ s' ].
326 ndefinition set_call_reg_sIP2022 ≝
327 λt:memory_impl.λs:any_status IP2022 t.λval.
328 set_alu … s (set_call_reg_IP2022 (alu … s) val).
330 (* setter forte di CALL *)
331 ndefinition set_call_reg ≝
334 return λm.any_status m t → word16 → option (any_status m t)
336 [ HC05 ⇒ λs:any_status ? t.λval.None ?
337 | HC08 ⇒ λs:any_status ? t.λval.None ?
338 | HCS08 ⇒ λs:any_status ? t.λval.None ?
339 | RS08 ⇒ λs:any_status ? t.λval.None ?
340 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_call_reg_sIP2022 t s val)
343 (* setter debole di CALL *)
344 ndefinition setweak_call_reg ≝
345 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
346 match set_call_reg m t s val with
347 [ None ⇒ s | Some s' ⇒ s' ].
349 (* REGISTRO CALL [push] *)
351 ndefinition push_call_reg_sIP2022 ≝
352 λt:memory_impl.λs:any_status IP2022 t.λval.
353 set_alu … s (push_call_reg_IP2022 (alu … s) val).
355 (* push forte di CALL *)
356 ndefinition push_call_reg ≝
359 return λm.any_status m t → word16 → option (any_status m t)
361 [ HC05 ⇒ λs:any_status ? t.λval.None ?
362 | HC08 ⇒ λs:any_status ? t.λval.None ?
363 | HCS08 ⇒ λs:any_status ? t.λval.None ?
364 | RS08 ⇒ λs:any_status ? t.λval.None ?
365 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (push_call_reg_sIP2022 t s val)
368 (* REGISTRO CALL [pop] *)
370 ndefinition pop_call_reg_sIP2022 ≝
371 λt:memory_impl.λs:any_status IP2022 t.
372 match pop_call_reg_IP2022 (alu … s) with
373 [ pair val alu' ⇒ pair … val (set_alu … s alu') ].
375 (* pop forte di CALL *)
376 ndefinition pop_call_reg ≝
379 return λm.any_status m t → option (ProdT word16 (any_status m t))
381 [ HC05 ⇒ λs:any_status ? t.None ?
382 | HC08 ⇒ λs:any_status ? t.None ?
383 | HCS08 ⇒ λs:any_status ? t.None ?
384 | RS08 ⇒ λs:any_status ? t.None ?
385 | IP2022 ⇒ λs:any_status ? t.Some ? (pop_call_reg_sIP2022 t s)
390 ndefinition set_ip_reg_sIP2022 ≝
391 λt:memory_impl.λs:any_status IP2022 t.λval.
392 set_alu … s (set_ip_reg_IP2022 (alu … s) val).
394 (* setter forte di IP *)
395 ndefinition set_ip_reg ≝
398 return λm.any_status m t → word16 → option (any_status m t)
400 [ HC05 ⇒ λs:any_status ? t.λval.None ?
401 | HC08 ⇒ λs:any_status ? t.λval.None ?
402 | HCS08 ⇒ λs:any_status ? t.λval.None ?
403 | RS08 ⇒ λs:any_status ? t.λval.None ?
404 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_ip_reg_sIP2022 t s val)
407 (* setter debole di IP *)
408 ndefinition setweak_ip_reg ≝
409 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
410 match set_ip_reg m t s val with
411 [ None ⇒ s | Some s' ⇒ s' ].
415 ndefinition set_dp_reg_sIP2022 ≝
416 λt:memory_impl.λs:any_status IP2022 t.λval.
417 set_alu … s (set_dp_reg_IP2022 (alu … s) val).
419 (* setter forte di DP *)
420 ndefinition set_dp_reg ≝
423 return λm.any_status m t → word16 → option (any_status m t)
425 [ HC05 ⇒ λs:any_status ? t.λval.None ?
426 | HC08 ⇒ λs:any_status ? t.λval.None ?
427 | HCS08 ⇒ λs:any_status ? t.λval.None ?
428 | RS08 ⇒ λs:any_status ? t.λval.None ?
429 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_dp_reg_sIP2022 t s val)
432 (* setter debole di DP *)
433 ndefinition setweak_dp_reg ≝
434 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
435 match set_dp_reg m t s val with
436 [ None ⇒ s | Some s' ⇒ s' ].
440 ndefinition set_data_reg_sIP2022 ≝
441 λt:memory_impl.λs:any_status IP2022 t.λval.
442 set_alu … s (set_data_reg_IP2022 (alu … s) val).
444 (* setter forte di DATA *)
445 ndefinition set_data_reg ≝
448 return λm.any_status m t → word16 → option (any_status m t)
450 [ HC05 ⇒ λs:any_status ? t.λval.None ?
451 | HC08 ⇒ λs:any_status ? t.λval.None ?
452 | HCS08 ⇒ λs:any_status ? t.λval.None ?
453 | RS08 ⇒ λs:any_status ? t.λval.None ?
454 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_data_reg_sIP2022 t s val)
457 (* setter debole di DATA *)
458 ndefinition setweak_data_reg ≝
459 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
460 match set_data_reg m t s val with
461 [ None ⇒ s | Some s' ⇒ s' ].
465 ndefinition set_speed_reg_sIP2022 ≝
466 λt:memory_impl.λs:any_status IP2022 t.λval.
467 set_alu … s (set_speed_reg_IP2022 (alu … s) val).
469 (* setter forte di SPEED *)
470 ndefinition set_speed_reg ≝
473 return λm.any_status m t → exadecim → option (any_status m t)
475 [ HC05 ⇒ λs:any_status ? t.λval.None ?
476 | HC08 ⇒ λs:any_status ? t.λval.None ?
477 | HCS08 ⇒ λs:any_status ? t.λval.None ?
478 | RS08 ⇒ λs:any_status ? t.λval.None ?
479 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_speed_reg_sIP2022 t s val)
482 (* setter debole di SPEED *)
483 ndefinition setweak_speed_reg ≝
484 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
485 match set_speed_reg m t s val with
486 [ None ⇒ s | Some s' ⇒ s' ].
490 ndefinition set_page_reg_sIP2022 ≝
491 λt:memory_impl.λs:any_status IP2022 t.λval.
492 set_alu … s (set_page_reg_IP2022 (alu … s) val).
494 (* setter forte di PAGE *)
495 ndefinition set_page_reg ≝
498 return λm.any_status m t → oct → option (any_status m t)
500 [ HC05 ⇒ λs:any_status ? t.λval.None ?
501 | HC08 ⇒ λs:any_status ? t.λval.None ?
502 | HCS08 ⇒ λs:any_status ? t.λval.None ?
503 | RS08 ⇒ λs:any_status ? t.λval.None ?
504 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_page_reg_sIP2022 t s val)
507 (* setter debole di PAGE *)
508 ndefinition setweak_page_reg ≝
509 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
510 match set_page_reg m t s val with
511 [ None ⇒ s | Some s' ⇒ s' ].
513 (* REGISTRO MEMORY MAPPED X *)
515 ndefinition set_x_map_sRS08 ≝
516 λt:memory_impl.λs:any_status RS08 t.λval.
517 set_alu … s (set_x_map_RS08 (alu … s) val).
519 (* setter forte di memory mapped X *)
520 ndefinition set_x_map ≝
523 return λm.any_status m t → byte8 → option (any_status m t)
525 [ HC05 ⇒ λs:any_status ? t.λval.None ?
526 | HC08 ⇒ λs:any_status ? t.λval.None ?
527 | HCS08 ⇒ λs:any_status ? t.λval.None ?
528 | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_x_map_sRS08 t s val)
529 | IP2022 ⇒ λs:any_status ? t.λval.None ?
532 (* setter debole di memory mapped X *)
533 ndefinition setweak_x_map ≝
534 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
535 match set_x_map m t s val with
536 [ None ⇒ s | Some s' ⇒ s' ].
538 (* REGISTRO MEMORY MAPPED PS *)
540 ndefinition set_ps_map_sRS08 ≝
541 λt:memory_impl.λs:any_status RS08 t.λval.
542 set_alu … s (set_ps_map_RS08 (alu … s) val).
544 (* setter forte di memory mapped PS *)
545 ndefinition set_ps_map ≝
548 return λm.any_status m t → byte8 → option (any_status m t)
550 [ HC05 ⇒ λs:any_status ? t.λval.None ?
551 | HC08 ⇒ λs:any_status ? t.λval.None ?
552 | HCS08 ⇒ λs:any_status ? t.λval.None ?
553 | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_ps_map_sRS08 t s val)
554 | IP2022 ⇒ λs:any_status ? t.λval.None ?
557 (* setter debole di memory mapped PS *)
558 ndefinition setweak_ps_map ≝
559 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
560 match set_ps_map m t s val with
561 [ None ⇒ s | Some s' ⇒ s' ].
565 ndefinition set_skip_mode_sIP2022 ≝
566 λt:memory_impl.λs:any_status IP2022 t.λval.
567 set_alu … s (set_skip_mode_IP2022 (alu … s) val).
569 (* setter forte di modalita SKIP *)
570 ndefinition set_skip_mode ≝
573 return λm.any_status m t → bool → option (any_status m t)
575 [ HC05 ⇒ λs:any_status ? t.λval.None ?
576 | HC08 ⇒ λs:any_status ? t.λval.None ?
577 | HCS08 ⇒ λs:any_status ? t.λval.None ?
578 | RS08 ⇒ λs:any_status ? t.λval.None ?
579 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_skip_mode_sIP2022 t s val)
582 (* setter debole di SKIP *)
583 ndefinition setweak_skip_mode ≝
584 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
585 match set_skip_mode m t s val with
586 [ None ⇒ s | Some s' ⇒ s' ].
590 ndefinition set_v_flag_sHC08 ≝
591 λt:memory_impl.λs:any_status HC08 t.λval.
592 set_alu … s (set_v_flag_HC08 (alu … s) val).
594 ndefinition set_v_flag_sHCS08 ≝
595 λt:memory_impl.λs:any_status HCS08 t.λval.
596 set_alu … s (set_v_flag_HC08 (alu … s) val).
598 (* setter forte di V *)
599 ndefinition set_v_flag ≝
602 return λm.any_status m t → bool → option (any_status m t)
604 [ HC05 ⇒ λs:any_status ? t.λval.None ?
605 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_v_flag_sHC08 t s val)
606 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_v_flag_sHCS08 t s val)
607 | RS08 ⇒ λs:any_status ? t.λval.None ?
608 | IP2022 ⇒ λs:any_status ? t.λval.None ?
611 (* setter debole di V *)
612 ndefinition setweak_v_flag ≝
613 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
614 match set_v_flag m t s val with
615 [ None ⇒ s | Some s' ⇒ s' ].
619 ndefinition set_h_flag_sHC05 ≝
620 λt:memory_impl.λs:any_status HC05 t.λval.
621 set_alu … s (set_h_flag_HC05 (alu … s) val).
623 ndefinition set_h_flag_sHC08 ≝
624 λt:memory_impl.λs:any_status HC08 t.λval.
625 set_alu … s (set_h_flag_HC08 (alu … s) val).
627 ndefinition set_h_flag_sHCS08 ≝
628 λt:memory_impl.λs:any_status HCS08 t.λval.
629 set_alu … s (set_h_flag_HC08 (alu … s) val).
631 ndefinition set_h_flag_sIP2022 ≝
632 λt:memory_impl.λs:any_status IP2022 t.λval.
633 set_alu … s (set_h_flag_IP2022 (alu … s) val).
635 (* setter forte di H *)
636 ndefinition set_h_flag ≝
639 return λm.any_status m t → bool → option (any_status m t)
641 [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHC05 t s val)
642 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHC08 t s val)
643 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHCS08 t s val)
644 | RS08 ⇒ λs:any_status ? t.λval.None ?
645 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sIP2022 t s val)
648 (* setter debole di H *)
649 ndefinition setweak_h_flag ≝
650 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
651 match set_h_flag m t s val with
652 [ None ⇒ s | Some s' ⇒ s' ].
656 ndefinition set_i_flag_sHC05 ≝
657 λt:memory_impl.λs:any_status HC05 t.λval.
658 set_alu … s (set_i_flag_HC05 (alu … s) val).
660 ndefinition set_i_flag_sHC08 ≝
661 λt:memory_impl.λs:any_status HC08 t.λval.
662 set_alu … s (set_i_flag_HC08 (alu … s) val).
664 ndefinition set_i_flag_sHCS08 ≝
665 λt:memory_impl.λs:any_status HCS08 t.λval.
666 set_alu … s (set_i_flag_HC08 (alu … s) val).
668 (* setter forte di I *)
669 ndefinition set_i_flag ≝
672 return λm.any_status m t → bool → option (any_status m t)
674 [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHC05 t s val)
675 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHC08 t s val)
676 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHCS08 t s val)
677 | RS08 ⇒ λs:any_status ? t.λval.None ?
678 | IP2022 ⇒ λs:any_status ? t.λval.None ?
681 (* setter debole di I *)
682 ndefinition setweak_i_flag ≝
683 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
684 match set_i_flag m t s val with
685 [ None ⇒ s | Some s' ⇒ s' ].
689 ndefinition set_n_flag_sHC05 ≝
690 λt:memory_impl.λs:any_status HC05 t.λval.
691 set_alu … s (set_n_flag_HC05 (alu … s) val).
693 ndefinition set_n_flag_sHC08 ≝
694 λt:memory_impl.λs:any_status HC08 t.λval.
695 set_alu … s (set_n_flag_HC08 (alu … s) val).
697 ndefinition set_n_flag_sHCS08 ≝
698 λt:memory_impl.λs:any_status HCS08 t.λval.
699 set_alu … s (set_n_flag_HC08 (alu … s) val).
701 (* setter forte di N *)
702 ndefinition set_n_flag ≝
705 return λm.any_status m t → bool → option (any_status m t)
707 [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHC05 t s val)
708 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHC08 t s val)
709 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHCS08 t s val)
710 | RS08 ⇒ λs:any_status ? t.λval.None ?
711 | IP2022 ⇒ λs:any_status ? t.λval.None ?
714 (* setter debole di N *)
715 ndefinition setweak_n_flag ≝
716 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
717 match set_n_flag m t s val with
718 [ None ⇒ s | Some s' ⇒ s' ].
722 (* setter forte di Z *)
723 ndefinition set_z_flag ≝
724 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
726 (match m return aux_set_type bool with
727 [ HC05 ⇒ set_z_flag_HC05
728 | HC08 ⇒ set_z_flag_HC08
729 | HCS08 ⇒ set_z_flag_HC08
730 | RS08 ⇒ set_z_flag_RS08
731 | IP2022 ⇒ set_z_flag_IP2022
736 (* setter forte di C *)
737 ndefinition set_c_flag ≝
738 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
740 (match m return aux_set_type bool with
741 [ HC05 ⇒ set_c_flag_HC05
742 | HC08 ⇒ set_c_flag_HC08
743 | HCS08 ⇒ set_c_flag_HC08
744 | RS08 ⇒ set_c_flag_RS08
745 | IP2022 ⇒ set_c_flag_IP2022
750 ndefinition set_irq_flag_sHC05 ≝
751 λt:memory_impl.λs:any_status HC05 t.λval.
752 set_alu … s (set_irq_flag_HC05 (alu … s) val).
754 ndefinition set_irq_flag_sHC08 ≝
755 λt:memory_impl.λs:any_status HC08 t.λval.
756 set_alu … s (set_irq_flag_HC08 (alu … s) val).
758 ndefinition set_irq_flag_sHCS08 ≝
759 λt:memory_impl.λs:any_status HCS08 t.λval.
760 set_alu … s (set_irq_flag_HC08 (alu … s) val).
762 (* setter forte di IRQ *)
763 ndefinition set_irq_flag ≝
766 return λm.any_status m t → bool → option (any_status m t)
768 [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHC05 t s val)
769 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHC08 t s val)
770 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHCS08 t s val)
771 | RS08 ⇒ λs:any_status ? t.λval.None ?
772 | IP2022 ⇒ λs:any_status ? t.λval.None ?
775 (* setter debole di IRQ *)
776 ndefinition setweak_irq_flag ≝
777 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
778 match set_irq_flag m t s val with
779 [ None ⇒ s | Some s' ⇒ s' ].