From ced2abc1e3fe84d5bbfa9ccb2ebf46f253279ebe Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Sun, 31 Jan 2010 06:38:45 +0000 Subject: [PATCH] freescale porting --- .../matita/contribs/ng_assembly/depends | 7 +- .../emulator/model/IP2022_model.ma | 6 +- .../emulator/opcodes/IP2022_instr_mode.ma | 8 + .../opcodes/IP2022_instr_mode_lemmas.ma | 4 +- .../emulator/opcodes/IP2022_pseudo.ma | 21 +- .../emulator/opcodes/IP2022_table.ma | 28 +- .../read_write/Freescale_load_write.ma | 584 ++++++++++++++++++ .../emulator/read_write/IP2022_load_write.ma | 112 ++++ .../ng_assembly/emulator/read_write/fetch.ma | 99 +++ .../emulator/read_write/load_write.ma | 82 +++ .../emulator/read_write/load_write_base.ma | 106 ++++ .../matita/contribs/ng_assembly/num/byte8.ma | 2 + .../contribs/ng_assembly/num/exadecim.ma | 14 + .../matita/contribs/ng_assembly/num/word16.ma | 2 + .../matita/contribs/ng_assembly/num/word32.ma | 2 + 15 files changed, 1048 insertions(+), 29 deletions(-) create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/read_write/fetch.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write_base.ma diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index dfbc41974..ee5ea13b4 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -12,6 +12,7 @@ common/string_lemmas.ma common/ascii_lemmas.ma common/list_utility_lemmas.ma com 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 @@ -32,8 +33,8 @@ emulator/opcodes/Freescale_instr_mode_lemmas.ma emulator/opcodes/Freescale_instr 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 @@ -58,8 +59,10 @@ num/oct_lemmas.ma num/bool_lemmas.ma num/oct.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 @@ -83,12 +86,14 @@ common/sigma.ma common/theory.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 diff --git a/helm/software/matita/contribs/ng_assembly/emulator/model/IP2022_model.ma b/helm/software/matita/contribs/ng_assembly/emulator/model/IP2022_model.ma index 03b3745b9..a83028e2a 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/model/IP2022_model.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/model/IP2022_model.ma @@ -35,9 +35,9 @@ ndefinition memory_type_of_FamilyIP2022 ≝ λ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 *) diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma index a12114d80..1998586e9 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma @@ -30,6 +30,10 @@ include "num/word16.ma". 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 @@ -57,6 +61,8 @@ ndefinition eq_IP2022_im ≝ λ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 ] @@ -70,6 +76,8 @@ ndefinition eq_IP2022_im ≝ 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)) diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode_lemmas.ma index eb7f9b820..7538086c1 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode_lemmas.ma @@ -29,8 +29,8 @@ nlemma eq_to_eqIP2022im : ∀n1,n2.n1 = n2 → eq_IP2022_im n1 n2 = true. #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. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo.ma index 9aa26cfdb..9a2950683 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_pseudo.ma @@ -51,9 +51,13 @@ ninductive IP2022_pseudo: Type ≝ | 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 *) @@ -97,8 +101,7 @@ ndefinition eq_IP2022_pseudo ≝ | 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 ] @@ -118,8 +121,8 @@ ndefinition eq_IP2022_pseudo ≝ 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. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table.ma index 0125d0506..287644c8d 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_table.ma @@ -60,20 +60,20 @@ ndefinition opcode_table_IP2022_3 ≝ 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 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma new file mode 100755 index 000000000..be04ff2f1 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma @@ -0,0 +1,584 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ? + ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma new file mode 100755 index 000000000..5e9a7d231 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma @@ -0,0 +1,112 @@ +(**************************************************************************) +(* ___ *) +(* ||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). diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/fetch.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/fetch.ma new file mode 100755 index 000000000..37d095106 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/fetch.ma @@ -0,0 +1,99 @@ +(**************************************************************************) +(* ___ *) +(* ||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). diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma new file mode 100755 index 000000000..683a0f7af --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma @@ -0,0 +1,82 @@ +(**************************************************************************) +(* ___ *) +(* ||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 + ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write_base.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write_base.ma new file mode 100755 index 000000000..d3bd4f96d --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write_base.ma @@ -0,0 +1,106 @@ +(**************************************************************************) +(* ___ *) +(* ||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). diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma index 9cf490eab..f625e71db 100755 --- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma +++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma @@ -66,10 +66,12 @@ ndefinition xor_b8 ≝ fop2_cn ? xor_ex. (* 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〉. diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma index 07c19464a..9400d9074 100755 --- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma +++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma @@ -688,6 +688,13 @@ ndefinition setMSB_ex ≝ | 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 @@ -703,6 +710,13 @@ ndefinition setLSB_ex ≝ | 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 diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma index a6c12ec9e..80281eeea 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word16.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma @@ -65,10 +65,12 @@ ndefinition xor_w16 ≝ fop2_cn ? xor_b8. (* 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〉. diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma index 7be3a53c5..09cd0ada2 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word32.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma @@ -64,10 +64,12 @@ ndefinition xor_w32 ≝ fop2_cn ? xor_w16. (* 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〉. -- 2.39.2