emulator/opcodes/IP2022_pseudo.ma num/bool.ma
compiler/ast_type_lemmas.ma common/list_utility_lemmas.ma compiler/ast_type.ma
emulator/memory/memory_struct_lemmas.ma emulator/memory/memory_struct.ma num/bool_lemmas.ma
+emulator/read_write/load_write.ma emulator/read_write/Freescale_load_write.ma emulator/read_write/IP2022_load_write.ma
num/quatern.ma num/bool.ma
num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma
emulator/status/IP2022_status_lemmas.ma emulator/memory/memory_struct_lemmas.ma emulator/status/IP2022_status.ma num/oct_lemmas.ma num/word16_lemmas.ma num/word24_lemmas.ma
test_errori.ma
compiler/environment.ma common/string.ma compiler/ast_type.ma
common/ascii_lemmas.ma common/ascii.ma num/bool_lemmas.ma
-emulator/translation/translation_base.ma common/option.ma emulator/opcodes/HC05_table.ma emulator/opcodes/HC08_table.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/RS08_table.ma emulator/opcodes/pseudo.ma
emulator/read_write/IP2022_read_write.ma emulator/read_write/read_write_base.ma emulator/status/status_setter.ma
+emulator/translation/translation_base.ma common/option.ma emulator/opcodes/HC05_table.ma emulator/opcodes/HC08_table.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/RS08_table.ma emulator/opcodes/pseudo.ma
emulator/opcodes/IP2022_table.ma common/list.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_pseudo.ma emulator/opcodes/byte_or_word.ma
emulator/status/HC05_status.ma num/word16.ma
emulator/opcodes/Freescale_pseudo_lemmas.ma emulator/opcodes/Freescale_pseudo.ma num/bool_lemmas.ma
emulator/memory/memory_struct.ma num/byte8.ma num/oct.ma
emulator/model/HC05_model.ma emulator/status/status.ma
emulator/status/status_setter.ma emulator/status/status.ma
+emulator/read_write/Freescale_load_write.ma emulator/read_write/load_write_base.ma emulator/status/status_getter.ma
num/word32.ma num/word16.ma
common/ascii.ma num/bool.ma
+emulator/read_write/load_write_base.ma emulator/read_write/read_write.ma
emulator/model/IP2022_model.ma emulator/status/status.ma
emulator/opcodes/HCS08_table_tests.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/pseudo.ma
emulator/opcodes/IP2022_table_tests.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/pseudo.ma
common/list_lemmas.ma common/list.ma
emulator/status/HC08_status_lemmas.ma emulator/status/HC08_status.ma num/word16_lemmas.ma
emulator/opcodes/HCS08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma
+emulator/read_write/IP2022_load_write.ma emulator/read_write/load_write_base.ma emulator/status/status_getter.ma
emulator/translation/IP2022_translation.ma emulator/translation/translation_base.ma
universe/universe.ma common/list.ma common/nat_lemmas.ma common/prod.ma
num/bitrigesim.ma num/bool.ma
emulator/opcodes/pseudo.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_pseudo.ma emulator/opcodes/byte_or_word.ma
common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma
emulator/translation/translation.ma emulator/translation/Freescale_translation.ma emulator/translation/IP2022_translation.ma
+emulator/read_write/fetch.ma emulator/memory/memory_abs.ma emulator/status/status_getter.ma emulator/translation/translation.ma
emulator/opcodes/IP2022_instr_mode_lemmas.ma emulator/opcodes/IP2022_instr_mode.ma num/bitrigesim_lemmas.ma num/bool_lemmas.ma num/oct_lemmas.ma
num/oct.ma num/bool.ma
common/list.ma common/theory.ma
λm:IP2022_model.match m with
[ IP2K ⇒
[
-(* 0x00000008-0x00000008 *) triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x8〉〉〉 〈〈x0,x0〉:〈x0,x1〉〉 MEM_READ_ONLY (* PCH read only memory reg *)
-(* 0x0000000E-0x0000000E *) ; triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xE〉〉〉 〈〈x0,x0〉:〈x0,x1〉〉 MEM_READ_ONLY (* PCH read only memory reg *)
-(* 0x00000080-0x00000FFF *) ; triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x8,x0〉〉〉 〈〈x0,xF〉:〈x8,x0〉〉 MEM_READ_WRITE (* 3968 GPR+RAM+STACK *)
+(* 0x02-0x13, 0x7E-0x7F registri memory mapped *)
+(* 0x00000002-0x0000007F *) triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x2〉〉〉 〈〈x0,x0〉:〈x7,xE〉〉 MEM_READ_ONLY (* 126B SystemMemoryReg *)
+(* 0x00000080-0x00000FFF *) ; triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x8,x0〉〉〉 〈〈x0,xF〉:〈x8,x0〉〉 MEM_READ_WRITE (* 3968 UserMemoryReg+RAM+STACK *)
(* 0x02000000-0x02003FFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_WRITE (* 16384B PROGRAM RAM *)
(* 0x02010000-0x02013FFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x1〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *)
(* 0x02014000-0x02017FFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x1〉〉.〈〈x4,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *)
ninductive IP2022_instr_mode: Type ≝
(* nessun operando : formato xxxxxxxx xxxxxxxx *)
MODE_INH : IP2022_instr_mode
+ (* operando implicito [ADDR] : formato xxxxxxxx xxxxxxxx *)
+| MODE_INHADDR : IP2022_instr_mode
+ (* operando implicito [ADDR]/ADDR+=2 : formato xxxxxxxx xxxxxxxx *)
+| MODE_INHADDRpp : IP2022_instr_mode
(* #lit3 → / : formato xxxxxxxx xxxxxkkk *)
| MODE_IMM3 : oct → IP2022_instr_mode
λi1,i2:IP2022_instr_mode.
match i1 with
[ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
+ | MODE_INHADDR ⇒ match i2 with [ MODE_INHADDR ⇒ true | _ ⇒ false ]
+ | MODE_INHADDRpp ⇒ match i2 with [ MODE_INHADDRpp ⇒ true | _ ⇒ false ]
| MODE_IMM3 o1 ⇒ match i2 with [ MODE_IMM3 o2 ⇒ eq_oct o1 o2 | _ ⇒ false ]
| MODE_IMM8 ⇒ match i2 with [ MODE_IMM8 ⇒ true | _ ⇒ false ]
| MODE_IMM13 t1 ⇒ match i2 with [ MODE_IMM13 t2 ⇒ eq_bit t1 t2 | _ ⇒ false ]
ndefinition forall_IP2022_im ≝ λP:IP2022_instr_mode → bool.
P MODE_INH
+⊗ P MODE_INHADDR
+⊗ P MODE_INHADDRpp
⊗ forall_oct (λo.P (MODE_IMM3 o))
⊗ P MODE_IMM8
⊗ forall_bit (λt.P (MODE_IMM13 t))
#n1; #n2; #H;
nrewrite > H;
nelim n2;
- ##[ ##2,9,10: #o; nrewrite > (eq_to_eqoct … (refl_eq …))
- ##| ##4: #t; nrewrite > (eq_to_eqbit … (refl_eq …)) ##]
+ ##[ ##4,11,12: #o; nrewrite > (eq_to_eqoct … (refl_eq …))
+ ##| ##6: #t; nrewrite > (eq_to_eqbit … (refl_eq …)) ##]
nnormalize;
napply refl_eq.
nqed.
| INCSZ : IP2022_pseudo (* increment & skip if zero *)
| INT : IP2022_pseudo (* interrupt -- not impl. ERR *)
| IREAD : IP2022_pseudo (* memory read *)
-| IREADI : IP2022_pseudo (* memory read & inc *)
+(* NB: ignorata la differenza IREAD/IREADI perche' non e' implementata EXT_MEM
+ IREAD → ADDRX= 0x00 ram, 0x01 flash, 0x80 0x81 ext_mem
+ IREADI → ADDRX= 0x00 ram, 0x01 flash *)
| IWRITE : IP2022_pseudo (* memory write *)
-| IWRITEI : IP2022_pseudo (* memory write & inc *)
+(* NB: ignorata la differenza IWRITE/IWRITEI perche' non e' implementata EXT_MEM
+ IREAD → ADDRX= 0x00 ram, 0x80 0x81 ext_mem
+ IREADI → ADDRX= 0x00 ram *)
| JMP : IP2022_pseudo (* jump *)
| LOADH : IP2022_pseudo (* load Data Pointer High *)
| LOADL : IP2022_pseudo (* load Data Pointer Low *)
| FREAD ⇒ match ps2 with [ FREAD ⇒ true | _ ⇒ false ] | FWRITE ⇒ match ps2 with [ FWRITE ⇒ true | _ ⇒ false ]
| INC ⇒ match ps2 with [ INC ⇒ true | _ ⇒ false ] | INCSNZ ⇒ match ps2 with [ INCSNZ ⇒ true | _ ⇒ false ]
| INCSZ ⇒ match ps2 with [ INCSZ ⇒ true | _ ⇒ false ] | INT ⇒ match ps2 with [ INT ⇒ true | _ ⇒ false ]
- | IREAD ⇒ match ps2 with [ IREAD ⇒ true | _ ⇒ false ] | IREADI ⇒ match ps2 with [ IREADI ⇒ true | _ ⇒ false ]
- | IWRITE ⇒ match ps2 with [ IWRITE ⇒ true | _ ⇒ false ] | IWRITEI ⇒ match ps2 with [ IWRITEI ⇒ true | _ ⇒ false ]
+ | IREAD ⇒ match ps2 with [ IREAD ⇒ true | _ ⇒ false ] | IWRITE ⇒ match ps2 with [ IWRITE ⇒ true | _ ⇒ false ]
| JMP ⇒ match ps2 with [ JMP ⇒ true | _ ⇒ false ] | LOADH ⇒ match ps2 with [ LOADH ⇒ true | _ ⇒ false ]
| LOADL ⇒ match ps2 with [ LOADL ⇒ true | _ ⇒ false ] | MOV ⇒ match ps2 with [ MOV ⇒ true | _ ⇒ false ]
| MULS ⇒ match ps2 with [ MULS ⇒ true | _ ⇒ false ] | MULU ⇒ match ps2 with [ MULU ⇒ true | _ ⇒ false ]
ndefinition forall_IP2022_pseudo ≝ λP:IP2022_pseudo → bool.
P ADD ⊗ P ADDC ⊗ P AND ⊗ P BREAK ⊗ P BREAKX ⊗ P CALL ⊗ P CLR ⊗ P CLRB ⊗
P CMP ⊗ P CSE ⊗ P CSNE ⊗ P CWDT ⊗ P DEC ⊗ P DECSNZ ⊗ P DECSZ ⊗ P FERASE ⊗
- P FREAD ⊗ P FWRITE ⊗ P INC ⊗ P INCSNZ ⊗ P INCSZ ⊗ P INT ⊗ P IREAD ⊗ P IREADI ⊗
- P IWRITE ⊗ P IWRITEI ⊗ P JMP ⊗ P LOADH ⊗ P LOADL ⊗ P MOV ⊗ P MULS ⊗ P MULU ⊗
- P NOP ⊗ P NOT ⊗ P OR ⊗ P PAGE ⊗ P POP ⊗ P PUSH ⊗ P RET ⊗ P RETI ⊗
- P RETNP ⊗ P RETW ⊗ P RL ⊗ P RR ⊗ P SB ⊗ P SETB ⊗ P SNB ⊗ P SPEED ⊗
- P SUB ⊗ P SUBC ⊗ P SWAP ⊗ P TEST ⊗ P XOR.
+ P FREAD ⊗ P FWRITE ⊗ P INC ⊗ P INCSNZ ⊗ P INCSZ ⊗ P INT ⊗ P IREAD ⊗ P IWRITE ⊗
+ P JMP ⊗ P LOADH ⊗ P LOADL ⊗ P MOV ⊗ P MULS ⊗ P MULU ⊗ P NOP ⊗ P NOT ⊗
+ P OR ⊗ P PAGE ⊗ P POP ⊗ P PUSH ⊗ P RET ⊗ P RETI ⊗ P RETNP ⊗ P RETW ⊗
+ P RL ⊗ P RR ⊗ P SB ⊗ P SETB ⊗ P SNB ⊗ P SPEED ⊗ P SUB ⊗ P SUBC ⊗
+ P SWAP ⊗ P TEST ⊗ P XOR.
ndefinition opcode_table_IP2022_4 ≝
[
- quadruple … BREAK MODE_INH (Word 〈〈x0,x0〉:〈x0,x1〉〉) 〈x0,x1〉
-; quadruple … BREAKX MODE_INH (Word 〈〈x0,x0〉:〈x0,x5〉〉) 〈x0,x1〉
-; quadruple … CWDT MODE_INH (Word 〈〈x0,x0〉:〈x0,x4〉〉) 〈x0,x1〉
-; quadruple … FERASE MODE_INH (Word 〈〈x0,x0〉:〈x0,x3〉〉) 〈x0,x1〉
-; quadruple … FREAD MODE_INH (Word 〈〈x0,x0〉:〈x1,xB〉〉) 〈x0,x1〉
-; quadruple … FWRITE MODE_INH (Word 〈〈x0,x0〉:〈x1,xA〉〉) 〈x0,x1〉
-; quadruple … INT MODE_INH (Word 〈〈x0,x0〉:〈x0,x6〉〉) 〈x0,x3〉
-; quadruple … IREAD MODE_INH (Word 〈〈x0,x0〉:〈x1,x9〉〉) 〈x0,x4〉 (* blocking *)
-; quadruple … IREADI MODE_INH (Word 〈〈x0,x0〉:〈x1,xD〉〉) 〈x0,x4〉 (* blocking *)
-; quadruple … IWRITE MODE_INH (Word 〈〈x0,x0〉:〈x1,x8〉〉) 〈x0,x4〉 (* blocking *)
-; quadruple … IWRITEI MODE_INH (Word 〈〈x0,x0〉:〈x1,xC〉〉) 〈x0,x4〉 (* blocking *)
-; quadruple … NOP MODE_INH (Word 〈〈x0,x0〉:〈x0,x0〉〉) 〈x0,x1〉
-; quadruple … RET MODE_INH (Word 〈〈x0,x0〉:〈x0,x7〉〉) 〈x0,x3〉
-; quadruple … RETNP MODE_INH (Word 〈〈x0,x0〉:〈x0,x2〉〉) 〈x0,x3〉
+ quadruple … BREAK MODE_INH (Word 〈〈x0,x0〉:〈x0,x1〉〉) 〈x0,x1〉
+; quadruple … BREAKX MODE_INH (Word 〈〈x0,x0〉:〈x0,x5〉〉) 〈x0,x1〉
+; quadruple … CWDT MODE_INH (Word 〈〈x0,x0〉:〈x0,x4〉〉) 〈x0,x1〉
+; quadruple … FERASE MODE_INH (Word 〈〈x0,x0〉:〈x0,x3〉〉) 〈x0,x1〉
+; quadruple … FREAD MODE_INH (Word 〈〈x0,x0〉:〈x1,xB〉〉) 〈x0,x1〉
+; quadruple … FWRITE MODE_INH (Word 〈〈x0,x0〉:〈x1,xA〉〉) 〈x0,x1〉
+; quadruple … INT MODE_INH (Word 〈〈x0,x0〉:〈x0,x6〉〉) 〈x0,x3〉
+; quadruple … IREAD MODE_INHADDR (Word 〈〈x0,x0〉:〈x1,x9〉〉) 〈x0,x4〉 (* only blocking implemented *)
+; quadruple … IREAD MODE_INHADDRpp (Word 〈〈x0,x0〉:〈x1,xD〉〉) 〈x0,x4〉 (* only blocking implemented *)
+; quadruple … IWRITE MODE_INHADDR (Word 〈〈x0,x0〉:〈x1,x8〉〉) 〈x0,x4〉 (* only blocking implemented *)
+; quadruple … IWRITE MODE_INHADDRpp (Word 〈〈x0,x0〉:〈x1,xC〉〉) 〈x0,x4〉 (* only blocking implemented *)
+; quadruple … NOP MODE_INH (Word 〈〈x0,x0〉:〈x0,x0〉〉) 〈x0,x1〉
+; quadruple … RET MODE_INH (Word 〈〈x0,x0〉:〈x0,x7〉〉) 〈x0,x3〉
+; quadruple … RETNP MODE_INH (Word 〈〈x0,x0〉:〈x0,x2〉〉) 〈x0,x3〉
].
ndefinition opcode_table_IP2022_5 ≝
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/read_write/load_write_base.ma".
+include "emulator/status/status_getter.ma".
+
+(* lettura da [curpc]: IMM1 *)
+ndefinition mode_IMM1_load ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λb.Some ? (triple … s b (succ_w16 cur_pc))).
+
+(* lettura da [curpc]: IMM1 + estensione a word *)
+ndefinition mode_IMM1EXT_load ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λb.Some ? (triple … s (extu_w16 b) (succ_w16 cur_pc))).
+
+(* lettura da [curpc]: IMM2 *)
+ndefinition mode_IMM2_load ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λbh.opt_map … (mem_read_s … s (extu_w32 (succ_w16 cur_pc)))
+ (λbl.Some ? (triple … s 〈bh:bl〉 (succ_w16 (succ_w16 cur_pc))))).
+
+(* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
+ndefinition mode_DIR1_load ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λaddr.(aux_load m t byteflag) s (extu2_w32 addr) cur_pc x1).
+
+(* lettura da [byte [curpc]]: loadbit *)
+ndefinition mode_DIR1n_load ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.
+ opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λaddr.loadbit_from … s (extu2_w32 addr) sub cur_pc x1).
+
+(* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
+ndefinition mode_DIR1_write ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
+ opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λaddr.(aux_write m t byteflag) s (extu2_w32 addr) auxMode_ok cur_pc x1 writebw).
+
+(* scrittura su [byte [curpc]]: writebit *)
+ndefinition mode_DIR1n_write ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.λwriteb:bool.
+ opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λaddr.writebit_to … s (extu2_w32 addr) sub cur_pc x1 writeb).
+
+(* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
+ndefinition mode_DIR2_load ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λaddrh.opt_map … (mem_read_s … s (extu_w32 (succ_w16 cur_pc)))
+ (λaddrl.(aux_load m t byteflag) s (extu_w32 〈addrh:addrl〉) cur_pc x2)).
+
+(* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
+ndefinition mode_DIR2_write ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
+ opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λaddrh.opt_map … (mem_read_s … s (extu_w32 (succ_w16 cur_pc)))
+ (λaddrl.(aux_write m t byteflag) s (extu_w32 〈addrh:addrl〉) auxMode_ok cur_pc x2 writebw)).
+
+ndefinition get_IX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ match m with
+ [ HC05 ⇒ opt_map … (get_indX_8_low_reg … s) (λindx.Some ? (extu_w16 indx))
+ | HC08 ⇒ opt_map … (get_indX_16_reg … s) (λindx.Some ? indx)
+ | HCS08 ⇒ opt_map … (get_indX_16_reg … s) (λindx.Some ? indx)
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ None ? ].
+
+(* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
+ndefinition mode_IX0_load ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map … (get_IX … s)
+ (λaddr.(aux_load m t byteflag) s (extu_w32 addr) cur_pc x0).
+
+(* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
+ndefinition mode_IX0_write ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
+ opt_map … (get_IX … s)
+ (λaddr.(aux_write m t byteflag) s (extu_w32 addr) auxMode_ok cur_pc x0 writebw).
+
+(* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
+ndefinition mode_IX1_load ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map … (get_IX … s)
+ (λaddr.opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λoffs.(aux_load m t byteflag) s (extu_w32 (plus_w16_d_d addr (extu_w16 offs))) cur_pc x1)).
+
+(* lettura da X+[byte curpc] *)
+ndefinition mode_IX1ADD_load ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map … (get_IX … s)
+ (λaddr.opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λb.Some ? (triple … s (plus_w16_d_d addr (extu_w16 b)) (succ_w16 cur_pc)))).
+
+(* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
+ndefinition mode_IX1_write ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
+ opt_map … (get_IX … s)
+ (λaddr.opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λoffs.(aux_write m t byteflag) s (extu_w32 (plus_w16_d_d addr (extu_w16 offs))) auxMode_ok cur_pc x1 writebw)).
+
+(* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
+ndefinition mode_IX2_load ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map … (get_IX … s)
+ (λaddr.opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λoffsh.opt_map … (mem_read_s … s (extu_w32 (succ_w16 cur_pc)))
+ (λoffsl.(aux_load m t byteflag) s (extu_w32 (plus_w16_d_d addr 〈offsh:offsl〉)) cur_pc x2))).
+
+(* lettura da X+[word curpc] *)
+ndefinition mode_IX2ADD_load ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map … (get_IX … s)
+ (λaddr.opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λbh.opt_map … (mem_read_s … s (extu_w32 (succ_w16 cur_pc)))
+ (λbl.Some ? (triple … s (plus_w16_d_d addr 〈bh:bl〉) (succ_w16 (succ_w16 cur_pc)))))).
+
+(* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
+ndefinition mode_IX2_write ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
+ opt_map … (get_IX … s)
+ (λaddr.opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λoffsh.opt_map … (mem_read_s … s (extu_w32 (succ_w16 cur_pc)))
+ (λoffsl.(aux_write m t byteflag) s (extu_w32 (plus_w16_d_d addr 〈offsh:offsl〉)) auxMode_ok cur_pc x2 writebw))).
+
+(* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
+ndefinition mode_SP1_load ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map … (get_sp_reg … s)
+ (λaddr.opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λoffs.(aux_load m t byteflag) s (extu_w32 (plus_w16_d_d addr (extu_w16 offs))) cur_pc x1)).
+
+(* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
+ndefinition mode_SP1_write ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
+ opt_map … (get_sp_reg … s)
+ (λaddr.opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λoffs.(aux_write m t byteflag) s (extu_w32 (plus_w16_d_d addr (extu_w16 offs))) auxMode_ok cur_pc x1 writebw)).
+
+(* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
+ndefinition mode_SP2_load ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map … (get_sp_reg … s)
+ (λaddr.opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λoffsh.opt_map … (mem_read_s … s (extu_w32 (succ_w16 cur_pc)))
+ (λoffsl.(aux_load m t byteflag) s (extu_w32 (plus_w16_d_d addr 〈offsh:offsl〉)) cur_pc x2))).
+
+(* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
+ndefinition mode_SP2_write ≝
+λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
+ opt_map … (get_sp_reg … s)
+ (λaddr.opt_map … (mem_read_s … s (extu_w32 cur_pc))
+ (λoffsh.opt_map … (mem_read_s … s (extu_w32 (succ_w16 cur_pc)))
+ (λoffsl.(aux_write m t byteflag) s (extu_w32 (plus_w16_d_d addr 〈offsh:offsl〉)) auxMode_ok cur_pc x2 writebw))).
+
+(* ************************************** *)
+(* raccordo di tutte le possibili letture *)
+(* ************************************** *)
+
+(* H:X++ *)
+ndefinition aux_inc_indX_16 ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ opt_map … (get_indX_16_reg m t s)
+ (λX_op.opt_map … (set_indX_16_reg m t s (succ_w16 X_op))
+ (λs_tmp.Some ? s_tmp)).
+
+ndefinition Freescale_multi_mode_load_auxb ≝
+λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with
+(* NO: non ci sono indicazioni *)
+ [ MODE_INH ⇒ None ?
+(* restituisce A *)
+ | MODE_INHA ⇒ Some ? (triple … s (get_acc_8_low_reg … s) cur_pc)
+(* restituisce X *)
+ | MODE_INHX ⇒ opt_map … (get_indX_8_low_reg … s)
+ (λindx.Some ? (triple … s indx cur_pc))
+(* restituisce H *)
+ | MODE_INHH ⇒ opt_map … (get_indX_8_high_reg … s)
+ (λindx.Some ? (triple … s indx cur_pc))
+
+(* NO: solo lettura word *)
+ | MODE_INHX0ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX1ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX2ADD ⇒ None ?
+
+(* preleva 1 byte immediato *)
+ | MODE_IMM1 ⇒ mode_IMM1_load … s cur_pc
+(* NO: solo lettura word *)
+ | MODE_IMM1EXT ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM2 ⇒ None ?
+(* preleva 1 byte da indirizzo diretto 1 byte *)
+ | MODE_DIR1 ⇒ mode_DIR1_load true … s cur_pc
+(* preleva 1 byte da indirizzo diretto 1 word *)
+ | MODE_DIR2 ⇒ mode_DIR2_load true … s cur_pc
+(* preleva 1 byte da H:X *)
+ | MODE_IX0 ⇒ mode_IX0_load true … s cur_pc
+(* preleva 1 byte da H:X+1 byte offset *)
+ | MODE_IX1 ⇒ mode_IX1_load true … s cur_pc
+(* preleva 1 byte da H:X+1 word offset *)
+ | MODE_IX2 ⇒ mode_IX2_load true … s cur_pc
+(* preleva 1 byte da SP+1 byte offset *)
+ | MODE_SP1 ⇒ mode_SP1_load true … s cur_pc
+(* preleva 1 byte da SP+1 word offset *)
+ | MODE_SP2 ⇒ mode_SP2_load true … s cur_pc
+
+(* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
+ | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true … s cur_pc
+(* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
+ | MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load … s cur_pc
+(* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
+ | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load true … s cur_pc
+(* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
+ | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true … s cur_pc
+
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_INHA_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_INHX_and_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM1_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_DIR1_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_IX0_and_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IX0p_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_IX1_and_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IX1p_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_SP1_and_IMM1 ⇒ None ?
+
+(* NO: solo scrittura byte *)
+ | MODE_DIRn _ ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_DIRn_and_IMM1 _ ⇒ None ?
+(* preleva 1 byte da 0000 0000 0000 xxxxb *)
+ | MODE_TNY e ⇒ opt_map … (memory_filter_read … s (extu3_w32 e))
+ (λb.Some ? (triple … s b cur_pc))
+(* preleva 1 byte da 0000 0000 000x xxxxb *)
+ | MODE_SRT e ⇒ opt_map … (memory_filter_read … s (extu2_w32 (b8_of_bit e)))
+ (λb.Some ? (triple … s b cur_pc))
+ ].
+
+ndefinition Freescale_multi_mode_load_auxw ≝
+λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with
+(* NO: non ci sono indicazioni *)
+ [ MODE_INH ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_INHA ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_INHX ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_INHH ⇒ None ?
+
+(* preleva 1 word immediato *)
+ | MODE_INHX0ADD ⇒ opt_map … (get_IX … s)
+ (λw.Some ? (triple … s w cur_pc))
+(* preleva 1 word immediato *)
+ | MODE_INHX1ADD ⇒ mode_IX1ADD_load … s cur_pc
+(* preleva 1 word immediato *)
+ | MODE_INHX2ADD ⇒ mode_IX2ADD_load … s cur_pc
+
+(* NO: solo lettura byte *)
+ | MODE_IMM1 ⇒ None ?
+(* preleva 1 word immediato *)
+ | MODE_IMM1EXT ⇒ mode_IMM1EXT_load … s cur_pc
+(* preleva 1 word immediato *)
+ | MODE_IMM2 ⇒ mode_IMM2_load … s cur_pc
+(* preleva 1 word da indirizzo diretto 1 byte *)
+ | MODE_DIR1 ⇒ mode_DIR1_load false … s cur_pc
+(* preleva 1 word da indirizzo diretto 1 word *)
+ | MODE_DIR2 ⇒ mode_DIR2_load false … s cur_pc
+(* preleva 1 word da H:X *)
+ | MODE_IX0 ⇒ mode_IX0_load false … s cur_pc
+(* preleva 1 word da H:X+1 byte offset *)
+ | MODE_IX1 ⇒ mode_IX1_load false … s cur_pc
+(* preleva 1 word da H:X+1 word offset *)
+ | MODE_IX2 ⇒ mode_IX2_load false … s cur_pc
+(* preleva 1 word da SP+1 byte offset *)
+ | MODE_SP1 ⇒ mode_SP1_load false … s cur_pc
+(* preleva 1 word da SP+1 word offset *)
+ | MODE_SP2 ⇒ mode_SP2_load false … s cur_pc
+
+(* NO: solo lettura/scrittura byte *)
+ | MODE_DIR1_to_DIR1 ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_IMM1_to_DIR1 ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_IX0p_to_DIR1 ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_DIR1_to_IX0p ⇒ None ?
+
+(* preleva 2 byte, possibilita' modificare Io argomento *)
+ | MODE_INHA_and_IMM1 ⇒ opt_map … (mode_IMM1_load … s cur_pc)
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc' ⇒
+ Some ? (triple … s 〈(get_acc_8_low_reg … s):immb〉 cur_pc')])
+(* preleva 2 byte, possibilita' modificare Io argomento *)
+ | MODE_INHX_and_IMM1 ⇒ opt_map … (get_indX_8_low_reg … s)
+ (λX_op.opt_map … (mode_IMM1_load … s cur_pc)
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc' ⇒
+ Some ? (triple … s 〈X_op:immb〉 cur_pc')]))
+(* preleva 2 byte, NO possibilita' modificare Io argomento *)
+ | MODE_IMM1_and_IMM1 ⇒ opt_map … (mode_IMM1_load … s cur_pc)
+ (λS_immb1_and_PC.match S_immb1_and_PC with
+ [ triple _ immb1 cur_pc' ⇒
+ opt_map … (mode_IMM1_load … s cur_pc')
+ (λS_immb2_and_PC.match S_immb2_and_PC with
+ [ triple _ immb2 cur_pc'' ⇒
+ Some ? (triple … s 〈immb1:immb2〉 cur_pc'')])])
+(* preleva 2 byte, possibilita' modificare Io argomento *)
+ | MODE_DIR1_and_IMM1 ⇒ opt_map … (mode_DIR1_load true … s cur_pc)
+ (λS_dirb_and_PC.match S_dirb_and_PC with
+ [ triple _ dirb cur_pc' ⇒
+ opt_map … (mode_IMM1_load … s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ Some ? (triple … s 〈dirb:immb〉 cur_pc'')])])
+(* preleva 2 byte, possibilita' modificare Io argomento *)
+ | MODE_IX0_and_IMM1 ⇒ opt_map … (mode_IX0_load true … s cur_pc)
+ (λS_ixb_and_PC.match S_ixb_and_PC with
+ [ triple _ ixb cur_pc' ⇒
+ opt_map … (mode_IMM1_load … s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ Some ? (triple … s 〈ixb:immb〉 cur_pc'')])])
+(* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
+ | MODE_IX0p_and_IMM1 ⇒ opt_map … (mode_IX0_load true … s cur_pc)
+ (λS_ixb_and_PC.match S_ixb_and_PC with
+ [ triple _ ixb cur_pc' ⇒
+ opt_map … (mode_IMM1_load … s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ (* H:X++ *)
+ opt_map … (aux_inc_indX_16 … s)
+ (λs'.Some ? (triple … s' 〈ixb:immb〉 cur_pc''))])])
+(* preleva 2 byte, possibilita' modificare Io argomento *)
+ | MODE_IX1_and_IMM1 ⇒ opt_map … (mode_IX1_load true … s cur_pc)
+ (λS_ixb_and_PC.match S_ixb_and_PC with
+ [ triple _ ixb cur_pc' ⇒
+ opt_map … (mode_IMM1_load … s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ Some ? (triple … s 〈ixb:immb〉 cur_pc'')])])
+(* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
+ | MODE_IX1p_and_IMM1 ⇒ opt_map … (mode_IX1_load true … s cur_pc)
+ (λS_ixb_and_PC.match S_ixb_and_PC with
+ [ triple _ ixb cur_pc' ⇒
+ opt_map … (mode_IMM1_load … s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ (* H:X++ *)
+ opt_map … (aux_inc_indX_16 … s)
+ (λs'.Some ? (triple … s' 〈ixb:immb〉 cur_pc''))])])
+(* preleva 2 byte, possibilita' modificare Io argomento *)
+ | MODE_SP1_and_IMM1 ⇒ opt_map … (mode_SP1_load true … s cur_pc)
+ (λS_spb_and_PC.match S_spb_and_PC with
+ [ triple _ spb cur_pc' ⇒
+ opt_map … (mode_IMM1_load … s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ Some ? (triple … s 〈spb:immb〉 cur_pc'')])])
+
+(* NO: solo scrittura byte *)
+ | MODE_DIRn _ ⇒ None ?
+(* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
+ | MODE_DIRn_and_IMM1 msk ⇒ opt_map … (mode_DIR1n_load … s cur_pc msk)
+ (λS_dirbn_and_PC.match S_dirbn_and_PC with
+ [ triple _ dirbn cur_pc' ⇒
+ opt_map … (mode_IMM1_load … s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ Some ? (triple … s 〈〈x0,match dirbn with [ true ⇒ x1 | false ⇒ x0 ]〉:immb〉 cur_pc'') ])])
+(* NO: solo lettura/scrittura byte *)
+ | MODE_TNY _ ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_SRT _ ⇒ None ?
+ ].
+
+(* **************************************** *)
+(* raccordo di tutte le possibili scritture *)
+(* **************************************** *)
+
+ndefinition Freescale_multi_mode_write_auxb ≝
+λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.λwriteb:byte8.match i with
+(* NO: non ci sono indicazioni *)
+ [ MODE_INH ⇒ None ?
+(* scrive A *)
+ | MODE_INHA ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
+(* scrive X *)
+ | MODE_INHX ⇒ opt_map … (set_indX_8_low_reg … s writeb)
+ (λtmps.Some ? (pair … tmps cur_pc))
+(* scrive H *)
+ | MODE_INHH ⇒ opt_map … (set_indX_8_high_reg … s writeb)
+ (λtmps.Some ? (pair … tmps cur_pc))
+
+(* NO: solo lettura word *)
+ | MODE_INHX0ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX1ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX2ADD ⇒ None ?
+
+(* NO: solo lettura byte *)
+ | MODE_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM1EXT ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM2 ⇒ None ?
+(* scrive 1 byte su indirizzo diretto 1 byte *)
+ | MODE_DIR1 ⇒ mode_DIR1_write true … s cur_pc writeb
+(* scrive 1 byte su indirizzo diretto 1 word *)
+ | MODE_DIR2 ⇒ mode_DIR2_write true … s cur_pc writeb
+(* scrive 1 byte su H:X *)
+ | MODE_IX0 ⇒ mode_IX0_write true … s cur_pc writeb
+(* scrive 1 byte su H:X+1 byte offset *)
+ | MODE_IX1 ⇒ mode_IX1_write true … s cur_pc writeb
+(* scrive 1 byte su H:X+1 word offset *)
+ | MODE_IX2 ⇒ mode_IX2_write true … s cur_pc writeb
+(* scrive 1 byte su SP+1 byte offset *)
+ | MODE_SP1 ⇒ mode_SP1_write true … s cur_pc writeb
+(* scrive 1 byte su SP+1 word offset *)
+ | MODE_SP2 ⇒ mode_SP2_write true … s cur_pc writeb
+
+(* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
+ | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_write true … s cur_pc writeb
+(* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
+ | MODE_IMM1_to_DIR1 ⇒ mode_DIR1_write true … s cur_pc writeb
+(* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
+ | MODE_IX0p_to_DIR1 ⇒ opt_map … (mode_DIR1_write true … s cur_pc writeb)
+ (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
+ (* H:X++ *)
+ opt_map … (aux_inc_indX_16 … S_op)
+ (λS_op'.Some ? (pair … S_op' PC_op))])
+(* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
+ | MODE_DIR1_to_IX0p ⇒ opt_map … (mode_IX0_write true … s cur_pc writeb)
+ (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
+ (* H:X++ *)
+ opt_map … (aux_inc_indX_16 … S_op)
+ (λS_op'.Some ? (pair … S_op' PC_op))])
+
+(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
+ | MODE_INHA_and_IMM1 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
+(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)
+ | MODE_INHX_and_IMM1 ⇒ opt_map … (set_indX_8_low_reg … s writeb)
+ (λtmps.Some ? (pair … tmps cur_pc))
+(* NO: solo lettura word *)
+ | MODE_IMM1_and_IMM1 ⇒ None ?
+(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *)
+ | MODE_DIR1_and_IMM1 ⇒ mode_DIR1_write true … s cur_pc writeb
+(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
+ | MODE_IX0_and_IMM1 ⇒ mode_IX0_write true … s cur_pc writeb
+(* NO: solo lettura word *)
+ | MODE_IX0p_and_IMM1 ⇒ None ?
+(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
+ | MODE_IX1_and_IMM1 ⇒ mode_IX1_write true … s cur_pc writeb
+(* NO: solo lettura word *)
+ | MODE_IX1p_and_IMM1 ⇒ None ?
+(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
+ | MODE_SP1_and_IMM1 ⇒ mode_SP1_write true … s cur_pc writeb
+
+(* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
+ | MODE_DIRn msk ⇒ mode_DIR1n_write … s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))
+(* NO: solo lettura word *)
+ | MODE_DIRn_and_IMM1 _ ⇒ None ?
+(* scrive 1 byte su 0000 0000 0000 xxxxb *)
+ | MODE_TNY e ⇒ opt_map … (memory_filter_write … s (extu3_w32 e) auxMode_ok writeb)
+ (λtmps.Some ? (pair … tmps cur_pc))
+(* scrive 1 byte su 0000 0000 000x xxxxb *)
+ | MODE_SRT e ⇒ opt_map … (memory_filter_write … s (extu2_w32 (b8_of_bit e)) auxMode_ok writeb)
+ (λtmps.Some ? (pair … tmps cur_pc))
+ ].
+
+ndefinition Freescale_multi_mode_write_auxw ≝
+λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.λwritew:word16.match i with
+(* NO: non ci sono indicazioni *)
+ [ MODE_INH ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_INHA ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_INHX ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_INHH ⇒ None ?
+
+(* NO: solo lettura word *)
+ | MODE_INHX0ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX1ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX2ADD ⇒ None ?
+
+(* NO: solo lettura byte *)
+ | MODE_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM1EXT ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM2 ⇒ None ?
+(* scrive 1 word su indirizzo diretto 1 byte *)
+ | MODE_DIR1 ⇒ mode_DIR1_write false … s cur_pc writew
+(* scrive 1 word su indirizzo diretto 1 word *)
+ | MODE_DIR2 ⇒ mode_DIR2_write false … s cur_pc writew
+(* scrive 1 word su H:X *)
+ | MODE_IX0 ⇒ mode_IX0_write false … s cur_pc writew
+(* scrive 1 word su H:X+1 byte offset *)
+ | MODE_IX1 ⇒ mode_IX1_write false … s cur_pc writew
+(* scrive 1 word su H:X+1 word offset *)
+ | MODE_IX2 ⇒ mode_IX2_write false … s cur_pc writew
+(* scrive 1 word su SP+1 byte offset *)
+ | MODE_SP1 ⇒ mode_SP1_write false … s cur_pc writew
+(* scrive 1 word su SP+1 word offset *)
+ | MODE_SP2 ⇒ mode_SP2_write false … s cur_pc writew
+
+(* NO: solo lettura/scrittura byte *)
+ | MODE_DIR1_to_DIR1 ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_IMM1_to_DIR1 ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_IX0p_to_DIR1 ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_DIR1_to_IX0p ⇒ None ?
+
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_INHA_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_INHX_and_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM1_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_DIR1_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_IX0_and_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IX0p_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_IX1_and_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IX1p_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_SP1_and_IMM1 ⇒ None ?
+
+(* NO: solo scrittura byte *)
+ | MODE_DIRn _ ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_DIRn_and_IMM1 _ ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_TNY _ ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_SRT _ ⇒ None ?
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/read_write/load_write_base.ma".
+include "emulator/status/status_getter.ma".
+
+(* lettura da [PC<<1 - 1] : argomento non caricato dal fetch word-aligned *)
+ndefinition mode_IMM1_load ≝
+λt:memory_impl.λs:any_status IP2022 t.
+ mem_read_s … s (rol_w32 〈〈〈x8,x1〉:〈x0,x0〉〉.(pred_w16 (get_pc_reg … s))〉).
+
+(* lettura da [ADDR] *)
+ndefinition mode_ADDR_load ≝
+λt:memory_impl.λs:any_status IP2022 t.
+ opt_map … (get_addr_reg … s)
+ (λaddr.match (eq_b8 (w24x addr) 〈x0,x1〉) ⊗ (le_w16 (pred_w16 (get_pc_reg … s)) 〈〈x1,xF〉:〈xF,xF〉〉) with
+ (* lettura della FLASH da codice in RAM : operazione non bloccante non implementata! *)
+ [ true ⇒ None ?
+ | false ⇒ opt_map … (memory_filter_read … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(w24l addr)〉〉)
+ (λbh.opt_map … (memory_filter_read … s 〈〈〈x0,x2〉:(w24x (succ_w24 addr))〉.〈(w24h (succ_w24 addr)):(w24l (succ_w24 addr))〉〉)
+ (λbl.Some ? 〈bh:bl〉))]).
+
+(* scrittura su [ADDR] *)
+ndefinition mode_ADDR_write ≝
+λt:memory_impl.λs:any_status IP2022 t.λval:word16.
+ opt_map … (get_addr_reg … s)
+ (λaddr.opt_map … (memory_filter_write … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(w24l addr)〉〉 auxMode_ok (cnH ? val))
+ (λs'.memory_filter_write … s' 〈〈〈x0,x2〉:(w24x (succ_w24 addr))〉.〈(w24h (succ_w24 addr)):(w24l (succ_w24 addr))〉〉 auxMode_ok (cnL ? val))).
+
+(* IMM1 > 0 : lettura/scrittura da [IMM1] *)
+(* else : lettura/scrittura da [IP] : IP ≥ 0x20 *)
+ndefinition mode_DIR1IP_aux ≝
+λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T.
+ opt_map … (mode_IMM1_load t s)
+ (λaddr.match eq_b8 addr 〈x0,x0〉 with
+ (* xxxxxxx0 00000000 → [IP] *)
+ [ true ⇒ opt_map … (get_ip_reg … s)
+ (λip.match ge_w16 ip 〈〈x0,x0〉:〈x2,x0〉〉 with
+ (* IP ≥ 0x20 *)
+ [ true ⇒ f (extu_w32 ip)
+ | false ⇒ None ? ])
+ (* xxxxxxx0 nnnnnnnn → [IMM1] *)
+ | false ⇒ f (extu2_w32 addr)
+ ]).
+
+(* IMM1 < 0x80 : lettura/scrittura da [DP+IMM1] : DP+IMM1 ≥ 0x20 *)
+(* else : lettura/scrittura da [SP+IMM1] : SP+IMM1 ≥ 0x20 *)
+ndefinition mode_DPSP_aux ≝
+λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T.
+ opt_map … (mode_IMM1_load t s)
+ (λaddr.opt_map … (match getMSB_b8 addr with
+ (* xxxxxxx1 1nnnnnnn → [SP+IMM1] *)
+ [ true ⇒ get_sp_reg … s
+ (* xxxxxxx1 0nnnnnnn → [DP+IMM1] *)
+ | false ⇒ get_dp_reg … s ])
+ (λreg.match ge_w16 (plus_w16_d_d reg (extu_w16 (clrMSB_b8 addr))) 〈〈x0,x0〉:〈x2,x0〉〉 with
+ (* reg+IMM1 ≥ 0x20 *)
+ [ true ⇒ f (extu_w32 (plus_w16_d_d reg (extu_w16 (clrMSB_b8 addr))))
+ | false ⇒ None ? ])).
+
+(* FR0 *)
+ndefinition mode_FR0_load ≝
+λt:memory_impl.λs:any_status IP2022 t.
+ mode_DIR1IP_aux t s byte8 (memory_filter_read … s).
+
+ndefinition mode_FR0n_load ≝
+λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
+ mode_DIR1IP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
+
+ndefinition mode_FR0_write ≝
+λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
+ mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
+
+ndefinition mode_FR0n_write ≝
+λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
+ mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
+
+(* FR1 *)
+ndefinition mode_FR1_load ≝
+λt:memory_impl.λs:any_status IP2022 t.
+ mode_DPSP_aux t s byte8 (memory_filter_read … s).
+
+ndefinition mode_FR1n_load ≝
+λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
+ mode_DPSP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
+
+ndefinition mode_FR1_write ≝
+λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
+ mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
+
+ndefinition mode_FR1n_write ≝
+λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
+ mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/memory/memory_abs.ma".
+include "emulator/translation/translation.ma".
+include "emulator/status/status_getter.ma".
+
+(* errori possibili nel fetch OPCODE / ILLEGAL ADDRESS *)
+ninductive error_type : Type ≝
+ ILL_OP: error_type
+| ILL_FETCH_AD: error_type
+.
+
+(* - errore: interessa solo l'errore
+ - ok: interessa info e il nuovo pc *)
+ninductive fetch_result (A:Type) : Type ≝
+ FetchERR : error_type → fetch_result A
+| FetchOK : A → word16 → fetch_result A.
+
+ndefinition fetch_byte_aux ≝
+λm:mcu_type.λpc:word16.λbh:byte8.
+ match full_info_of_word16 m (Byte bh) with
+ [ None ⇒ FetchERR ? ILL_FETCH_AD
+ | Some info ⇒ FetchOK ? info pc
+ ].
+
+ndefinition fetch_word_aux ≝
+λm:mcu_type.λpc:word16.λw:word16.
+ match full_info_of_word16 m (Word w) with
+ [ None ⇒ FetchERR ? ILL_FETCH_AD
+ | Some info ⇒ FetchOK ? info pc
+ ].
+
+(* opcode a byte : HC05 / RS08 *)
+ndefinition fetch_byte ≝
+λm:mcu_type.λfR:word32 → option byte8.λpc:word16.
+ match fR (extu_w32 pc) with
+ [ None ⇒ FetchERR ? ILL_FETCH_AD
+ | Some bh ⇒ fetch_byte_aux m (succ_w16 pc) bh ].
+
+(* opcode a byte o 0x9E + byte : HC08 / HCS08 *)
+ndefinition Freescale_fetch_byte_or_word ≝
+λm:mcu_type.λfR:word32 → option byte8.λpc:word16.
+ match fR (extu_w32 pc) with
+ [ None ⇒ FetchERR ? ILL_FETCH_AD
+ | Some bh ⇒ match eq_b8 bh 〈x9,xE〉 with
+ [ true ⇒ match fR (extu_w32 (succ_w16 pc)) with
+ [ None ⇒ FetchERR ? ILL_FETCH_AD
+ | Some bl ⇒ fetch_word_aux m (succ_w16 (succ_w16 pc)) 〈bh:bl〉
+ ]
+ | false ⇒ fetch_byte_aux m (succ_w16 pc) bh
+ ]
+ ].
+
+(* opcode a byte o 0x00 + byte : IP2022 *)
+(* opcode + operando a dimensione fissa 16bit *)
+(* pc word aligned, mappato in 0x02000000-0x0201FFFF *)
+ndefinition IP2022_fetch_byte_or_word ≝
+λm:mcu_type.λfR:word32 → option byte8.λpc:word16.
+ let map_pc ≝ rol_w32 〈〈〈x0,x1〉:〈x0,x0〉〉.pc〉 in
+ match fR map_pc with
+ [ None ⇒ FetchERR ? ILL_FETCH_AD
+ | Some bh ⇒ match eq_b8 bh 〈x0,x0〉 with
+ [ true ⇒ match fR (succ_w32 map_pc) with
+ [ None ⇒ FetchERR ? ILL_FETCH_AD
+ | Some bl ⇒ fetch_word_aux m (succ_w16 pc) 〈bh:bl〉
+ ]
+ | false ⇒ fetch_byte_aux m (succ_w16 pc) bh
+ ]
+ ].
+
+ndefinition fetch ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ match m with
+ [ HC05 ⇒ fetch_byte
+ | HC08 ⇒ Freescale_fetch_byte_or_word
+ | HCS08 ⇒ Freescale_fetch_byte_or_word
+ | RS08 ⇒ fetch_byte
+ | IP2022 ⇒ IP2022_fetch_byte_or_word
+ ] m (mem_read t (mem_desc … s) (chk_desc … s)) (get_pc_reg … s).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/read_write/Freescale_load_write.ma".
+include "emulator/read_write/IP2022_load_write.ma".
+
+(* ************************************** *)
+(* raccordo di tutte le possibili letture *)
+(* ************************************** *)
+
+ndefinition multi_mode_loadb ≝
+λm.match m
+ return λm.Πt.any_status m t → word16 → aux_im_type m →
+ option (Prod3T (any_status m t) byte8 word16)
+ with
+ [ HC05 ⇒ Freescale_multi_mode_load_auxb HC05
+ | HC08 ⇒ Freescale_multi_mode_load_auxb HC08
+ | HCS08 ⇒ Freescale_multi_mode_load_auxb HCS08
+ | RS08 ⇒ Freescale_multi_mode_load_auxb RS08
+ | IP2022 ⇒ IP2022_multi_mode_load_auxb
+ ].
+
+ndefinition multi_mode_loadw ≝
+λm.match m
+ return λm.Πt.any_status m t → word16 → aux_im_type m →
+ option (Prod3T (any_status m t) word16 word16)
+ with
+ [ HC05 ⇒ Freescale_multi_mode_load_auxw HC05
+ | HC08 ⇒ Freescale_multi_mode_load_auxw HC08
+ | HCS08 ⇒ Freescale_multi_mode_load_auxw HCS08
+ | RS08 ⇒ Freescale_multi_mode_load_auxw RS08
+ | IP2022 ⇒ IP2022_multi_mode_load_auxw
+ ].
+
+(* tutte le modalita' di lettura: false=loadb true=loadw *)
+
+(* **************************************** *)
+(* raccordo di tutte le possibili scritture *)
+(* **************************************** *)
+
+ndefinition multi_mode_writeb ≝
+λm.match m
+ return λm.Πt.any_status m t → word16 → aux_im_type m → byte8 →
+ option (ProdT (any_status m t) word16)
+ with
+ [ HC05 ⇒ Freescale_multi_mode_write_auxb HC05
+ | HC08 ⇒ Freescale_multi_mode_write_auxb HC08
+ | HCS08 ⇒ Freescale_multi_mode_write_auxb HCS08
+ | RS08 ⇒ Freescale_multi_mode_write_auxb RS08
+ | IP2022 ⇒ IP2022_multi_mode_write_auxb
+ ].
+
+ndefinition multi_mode_writew ≝
+λm.match m
+ return λm.Πt.any_status m t → word16 → aux_im_type m → word16 →
+ option (ProdT (any_status m t) word16)
+ with
+ [ HC05 ⇒ Freescale_multi_mode_write_auxw HC05
+ | HC08 ⇒ Freescale_multi_mode_write_auxw HC08
+ | HCS08 ⇒ Freescale_multi_mode_write_auxw HCS08
+ | RS08 ⇒ Freescale_multi_mode_write_auxw RS08
+ | IP2022 ⇒ IP2022_multi_mode_write_auxw
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/read_write/read_write.ma".
+
+(* ************************ *)
+(* MODALITA' INDIRIZZAMENTO *)
+(* ************************ *)
+
+(* mattoni base *)
+(* - incrementano l'indirizzo normalmente *)
+(* - incrementano PC attraverso il filtro *)
+
+(* lettura byte da addr *)
+ndefinition loadb_from ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+λaddr:word32.λcur_pc:word16.λfetched:exadecim.
+ opt_map … (memory_filter_read … s addr)
+ (λb.Some ? (triple … s b (plus_w16_d_d cur_pc (extu2_w16 fetched)))).
+
+(* lettura bit da addr *)
+ndefinition loadbit_from ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+λaddr:word32.λsub:oct.λcur_pc:word16.λfetched:exadecim.
+ opt_map … (memory_filter_read_bit … s addr sub)
+ (λb.Some ? (triple … s b (plus_w16_d_d cur_pc (extu2_w16 fetched)))).
+
+(* lettura word da addr *)
+ndefinition loadw_from ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+λaddr:word32.λcur_pc:word16.λfetched:exadecim.
+ opt_map … (memory_filter_read … s addr)
+ (λbh.opt_map … (memory_filter_read … s (succ_w32 addr))
+ (λbl.Some ? (triple … s 〈bh:bl〉 (plus_w16_d_d cur_pc (extu2_w16 fetched))))).
+
+(* scrittura byte su addr *)
+ndefinition writeb_to ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+λaddr:word32.λflag:aux_mod_type.λcur_pc:word16.λfetched:exadecim.λwriteb:byte8.
+ opt_map … (memory_filter_write … s addr flag writeb)
+ (λtmps.Some ? (pair … tmps (plus_w16_d_d cur_pc (extu2_w16 fetched)))).
+
+(* scrittura bit su addr *)
+ndefinition writebit_to ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+λaddr:word32.λsub:oct.λcur_pc:word16.λfetched:exadecim.λwriteb:bool.
+ opt_map … (memory_filter_write_bit … s addr sub writeb)
+ (λtmps.Some ? (pair … tmps (plus_w16_d_d cur_pc (extu2_w16 fetched)))).
+
+(* scrittura word su addr *)
+ndefinition writew_to ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+λaddr:word32.λflag:aux_mod_type.λcur_pc:word16.λfetched:exadecim.λwritew:word16.
+ opt_map … (memory_filter_write … s addr auxMode_ok (cnH ? writew))
+ (λtmps1.opt_map … (memory_filter_write … tmps1 (succ_w32 addr) auxMode_ok (cnL ? writew))
+ (λtmps2.Some ? (pair … tmps2 (plus_w16_d_d cur_pc (extu2_w16 fetched))))).
+
+(* ausiliari per definire i tipi e la lettura/scrittura *)
+
+(* ausiliaria per definire il tipo di aux_load *)
+ndefinition aux_load_typing ≝
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.
+ any_status m t → word32 → word16 → exadecim →
+ option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
+
+(* per non dover ramificare i vari load in byte/word *)
+ndefinition aux_load ≝
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
+ [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
+
+(* ausiliaria per definire il tipo di aux_write *)
+ndefinition aux_write_typing ≝
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.
+ any_status m t → word32 → aux_mod_type → word16 → exadecim →
+ match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
+ option (ProdT (any_status m t) word16).
+
+(* per non dover ramificare i vari load in byte/word *)
+ndefinition aux_write ≝
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
+ [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
+
+ndefinition mem_read_s ≝
+λm,t.λs:any_status m t.mem_read t (mem_desc … s) (chk_desc … s).
+
+ndefinition mem_read_bit_s ≝
+λm,t.λs:any_status m t.mem_read_bit t (mem_desc … s) (chk_desc … s).
(* operatore Most Significant Bit *)
ndefinition getMSB_b8 ≝ getOPH_cn ? getMSB_ex.
ndefinition setMSB_b8 ≝ setOPH_cn ? setMSB_ex.
+ndefinition clrMSB_b8 ≝ setOPH_cn ? clrMSB_ex.
(* operatore Least Significant Bit *)
ndefinition getLSB_b8 ≝ getOPL_cn ? getLSB_ex.
ndefinition setLSB_b8 ≝ setOPL_cn ? setLSB_ex.
+ndefinition clrLSB_b8 ≝ setOPL_cn ? clrLSB_ex.
(* operatore estensione unsigned *)
ndefinition extu_b8 ≝ λe2.〈x0,e2〉.
| x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
| xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ].
+ndefinition clrMSB_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
+ | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ].
+
(* operatore Least Significant Bit *)
ndefinition getLSB_ex ≝
λe:exadecim.match e with
| x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
| xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ].
+ndefinition clrLSB_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
+ | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
+ | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
+ | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ].
+
(* operatore rotazione destra con carry *)
ndefinition rcr_ex ≝
λc:bool.λe:exadecim.match c with
(* operatore Most Significant Bit *)
ndefinition getMSB_w16 ≝ getOPH_cn ? getMSB_b8.
ndefinition setMSB_w16 ≝ setOPH_cn ? setMSB_b8.
+ndefinition clrMSB_w16 ≝ setOPH_cn ? clrMSB_b8.
(* operatore Least Significant Bit *)
ndefinition getLSB_w16 ≝ getOPL_cn ? getLSB_b8.
ndefinition setLSB_w16 ≝ setOPL_cn ? setLSB_b8.
+ndefinition clrLSB_w16 ≝ setOPL_cn ? clrLSB_b8.
(* operatore estensione unsigned *)
ndefinition extu_w16 ≝ λb2.〈〈x0,x0〉:b2〉.
(* operatore Most Significant Bit *)
ndefinition getMSB_w32 ≝ getOPH_cn ? getMSB_w16.
ndefinition setMSB_w32 ≝ setOPH_cn ? setMSB_w16.
+ndefinition clrMSB_w32 ≝ setOPH_cn ? clrMSB_w16.
(* operatore Least Significant Bit *)
ndefinition getLSB_w32 ≝ getOPL_cn ? getLSB_w16.
ndefinition setLSB_w32 ≝ setOPL_cn ? setLSB_w16.
+ndefinition clrLSB_w32 ≝ setOPL_cn ? clrLSB_w16.
(* operatore estensione unsigned *)
ndefinition extu_w32 ≝ λw2.〈〈〈x0,x0〉:〈x0,x0〉〉.w2〉.
projects / helm.git / commitdiff