include "emulator/status/HC05_status.ma".
include "emulator/status/HC08_status.ma".
include "emulator/status/RS08_status.ma".
+include "emulator/status/IP2022_status.ma".
include "emulator/opcodes/opcode.ma".
(* *********************************** *)
nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
{
alu : match mcu with
- [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ];
+ [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ];
(* descritore della memoria *)
mem_desc : aux_mem_type t;
match m
return λm.
match m with
- [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
+ [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ] →
match m with
- [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
+ [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ] →
bool
with
[ HC05 ⇒ eq_HC05_alu
| HC08 ⇒ eq_HC08_alu
| HCS08 ⇒ eq_HC08_alu
| RS08 ⇒ eq_RS08_alu
+ | IP2022 ⇒ eq_IP2022_alu
].
(* confronto di una regione di memoria [addr1 ; ... ; addrn] *)
(addrl:list word32) on addrl ≝
match addrl return λ_.bool with
[ nil ⇒ true
- | cons hd tl ⇒ (eq_option byte8 (mem_read t mem1 chk1 hd)
- (mem_read t mem2 chk2 hd) eq_b8) ⊗
+ | cons hd tl ⇒ (eq_option byte8 eq_b8 (mem_read t mem1 chk1 hd)
+ (mem_read t mem2 chk2 hd)) ⊗
(forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
].