X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmodel.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmodel.ma;h=0000000000000000000000000000000000000000;hb=16d0ba4a14fd6bede3e8b3520af7deaefb4f8068;hp=fe01726c7cfbf1bf9d34cdcfe4519cc690542ab5;hpb=d97886196d2c730f72312b226bebc388be08f39e;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/freescale/model.ma b/helm/software/matita/contribs/ng_assembly/freescale/model.ma deleted file mode 100755 index fe01726c7..000000000 --- a/helm/software/matita/contribs/ng_assembly/freescale/model.ma +++ /dev/null @@ -1,357 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* Ultima modifica: 05/08/2009 *) -(* *) -(* ********************************************************************** *) - -include "freescale/status.ma". - -(* *********************************** *) -(* IMPOSTAZIONI SPECIFICHE DEI MODELLI *) -(* *********************************** *) - -(* modelli di HC05 *) -ninductive HC05_mcu_model : Type ≝ - MC68HC05J5A: HC05_mcu_model - (*..*). - -(* modelli di HC08 *) -ninductive HC08_mcu_model : Type ≝ - MC68HC08AB16A: HC08_mcu_model - (*..*). - -(* modelli di HCS08 *) -ninductive HCS08_mcu_model : Type ≝ - MC9S08AW60 : HCS08_mcu_model -| MC9S08GB60 : HCS08_mcu_model - (*..*). - -(* modelli di RS08 *) -ninductive RS08_mcu_model : Type ≝ - MC9RS08KA1 : RS08_mcu_model -| MC9RS08KA2 : RS08_mcu_model. - -(* raggruppamento dei modelli *) -ninductive any_mcu_model : Type ≝ - FamilyHC05 : HC05_mcu_model → any_mcu_model -| FamilyHC08 : HC08_mcu_model → any_mcu_model -| FamilyHCS08 : HCS08_mcu_model → any_mcu_model -| FamilyRS08 : RS08_mcu_model → any_mcu_model. - -(* -condizioni errore interne alla MCU -(Il programma viene caricato dal produttore in ROM o impostato in EEPROM) -HC05: +illegal address during opcode fetch -HC08: +illegal address duting opcode fetch (ILAD mascherabile) - +illegal opcode (ILOP mascherabile) - -(Il programma viene programmato nella FLASH) -HCS08: +illegal address during opcode fetch (ILAD mascherabile) - +illegal opcode (ILOP mascherabile) - +security = accesso a RAM e zone FLASH dichiarate sicure da zone sicure - da' 0 in lettura e ignore in scrittura, [FLASH]SEC00:SEC01 (1,0) - corrisponde a OFF, altre ON, disattivabile solo da modalita' sicura se - opzione [FLASH]KEYEN e' 1 passando chiave a 8byte da modalita' sicura. - Altrimenti disattivabile solo con FLASH mass erase. Obbiettivo - e' impedire duplicazione di software di controllo, dato che esiste - modalita' debugging. A restart viene ricaricata da FLASH impostazione - sicurezza! -RS08: +illegal address durting opcode fetch (ILAD) mascherabile - +illegal opcode (ILOP mascherabile) - +security = solo la FLASH e' considerata sicura. Stesso meccanismo di HCS08 - ma governato solo da [FLASH]SECD (0) OFF.Una volta attivato l'unica - disattivazione e' la cancellazione della FLASH. -*) - -(* memoria degli HC05 *) -ndefinition memory_type_of_FamilyHC05 ≝ -λm:HC05_mcu_model.match m with - [ MC68HC05J5A ⇒ - [ - (* astraggo molto *) - (* 0x0000-0x001F,0x0FF0: sarebbe memory mapped IO *) - - triple … 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 128B RAM+STACK *) - ; triple … 〈〈x0,x3〉:〈x0,x0〉〉 〈〈x0,xC〉:〈xF,xF〉〉 MEM_READ_ONLY (* 2560B USER ROM *) - ; triple … 〈〈x0,xE〉:〈x0,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 512B INTERNAL ROM *) - ] - (*..*) - ]. - -(* memoria degli HC08 *) -ndefinition memory_type_of_FamilyHC08 ≝ -λm:HC08_mcu_model.match m with - [ MC68HC08AB16A ⇒ - [ - (* astraggo molto *) - (* 0x0000-0x004F,0xFE00-0xFE01,0xFE03, - 0xFE0C-0xFE11,0xFE1A-0xFE1D,0xFE1F: sarebbe memory mapped IO *) - (* 0x0500-0x057F,0xFE02,0xFE04-0xFE07, - 0xFE09-0xFE0B,0xFE12-0xFE19,0xFE1E,0xFFC0-0xFFCF : sarebbe reserved *) - - triple … 〈〈x0,x0〉:〈x5,x0〉〉 〈〈x0,x2〉:〈x4,xF〉〉 MEM_READ_WRITE (* 512B RAM *) - ; triple … 〈〈x0,x8〉:〈x0,x0〉〉 〈〈x0,x9〉:〈xF,xF〉〉 MEM_READ_ONLY (* 512B EEPROM *) - ; triple … 〈〈xB,xE〉:〈x0,x0〉〉 〈〈xF,xD〉:〈xF,xF〉〉 MEM_READ_ONLY (* 16384B ROM *) - ; triple … 〈〈xF,xE〉:〈x2,x0〉〉 〈〈xF,xF〉:〈x5,x2〉〉 MEM_READ_ONLY (* 307B ROM *) - ; triple … 〈〈xF,xF〉:〈xD,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 48B ROM *) ] - (*..*) - ]. - -(* memoria degli HCS08 *) -ndefinition memory_type_of_FamilyHCS08 ≝ -λm:HCS08_mcu_model.match m with - [ MC9S08AW60 ⇒ - [ - (* astraggo molto *) - (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *) - - triple … 〈〈x0,x0〉:〈x7,x0〉〉 〈〈x0,x8〉:〈x6,xF〉〉 MEM_READ_WRITE (* 2048B RAM *) - ; triple … 〈〈x0,x8〉:〈x7,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 3984B FLASH *) - ; triple … 〈〈x1,x8〉:〈x6,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59296B FLASH *) ] - | MC9S08GB60 ⇒ - [ - (* astraggo molto *) - (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *) - - triple … 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x1,x0〉:〈x7,xF〉〉 MEM_READ_WRITE (* 4096B RAM *) - ; triple … 〈〈x1,x0〉:〈x8,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 1920B FLASH *) - ; triple … 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59348B FLASH *) ] - ]. - -(* memoria dei RS08 *) -ndefinition memory_type_of_FamilyRS08 ≝ -λm:RS08_mcu_model.match m with - [ MC9RS08KA1 ⇒ - [ - triple … 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,xE〉〉 MEM_READ_WRITE (* 15B RAM *) - (* [000F] e' il registro X *) - (* 0x0010-0x001E sarebbe memory mapped IO, proviamo per completezza con RAM *) - ; triple … 〈〈x0,x0〉:〈x1,x0〉〉 〈〈x0,x0〉:〈x1,xE〉〉 MEM_READ_WRITE (* 15B MEMORY MAPPED IO *) - (* [001F] e' il registro PAGESEL *) - ; triple … 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x4,xF〉〉 MEM_READ_WRITE (* 48B RAM *) - (* [00C0-00FF] mappato da PAGESEL su [00pp pppp ppxx xxxx] *) - ; triple … 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 64B RAM PAGING *) - (* 0x0200-0x023F sarebbe memory mapped IO, proviamo per completezza con RAM *) - ; triple … 〈〈x0,x2〉:〈x0,x0〉〉 〈〈x0,x2〉:〈x3,xF〉〉 MEM_READ_WRITE (* 64B MEMORY MAPPED IO *) - ; triple … 〈〈x3,xC〉:〈x0,x0〉〉 〈〈x3,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 1024B FLASH *) ] - | MC9RS08KA2 ⇒ - [ - triple … 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,xE〉〉 MEM_READ_WRITE (* 15B RAM *) - (* [000F] e' il registro X *) - (* 0x0010-0x001E sarebbe memory mapped IO, proviamo per completezza con RAM *) - ; triple … 〈〈x0,x0〉:〈x1,x0〉〉 〈〈x0,x0〉:〈x1,xE〉〉 MEM_READ_WRITE (* 15B MEMORY MAPPED IO *) - (* [001F] e' il registro PAGESEL *) - ; triple … 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x4,xF〉〉 MEM_READ_WRITE (* 48B RAM *) - (* [00C0-00FF] mappato da PAGESEL su [00pp pppp ppxx xxxx] *) - ; triple … 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 64B RAM PAGING *) - (* 0x0200-0x023F sarebbe memory mapped IO, proviamo per completezza con RAM *) - ; triple … 〈〈x0,x2〉:〈x0,x0〉〉 〈〈x0,x2〉:〈x3,xF〉〉 MEM_READ_WRITE (* 64B MEMORY MAPPED IO *) - ; triple … 〈〈x3,x8〉:〈x0,x0〉〉 〈〈x3,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 2048B FLASH *) ] - ]. - -(* ∀modello.descrizione della memoria installata *) -ndefinition memory_type_of_mcu_version ≝ -λmcu:any_mcu_model.match mcu with - [ FamilyHC05 m ⇒ memory_type_of_FamilyHC05 m - | FamilyHC08 m ⇒ memory_type_of_FamilyHC08 m - | FamilyHCS08 m ⇒ memory_type_of_FamilyHCS08 m - | FamilyRS08 m ⇒ memory_type_of_FamilyRS08 m - ]. - -(* dato un modello costruisce un descrittore a partire dalla lista precedente *) -nlet rec build_memory_type_of_mcu_version_aux t param (result:aux_chk_type t) on param ≝ - match param with - [ nil ⇒ result - | cons hd tl ⇒ - build_memory_type_of_mcu_version_aux t tl - (check_update_ranged t result (fst3T ??? hd) (snd3T ??? hd) (thd3T ??? hd)) ]. - -ndefinition build_memory_type_of_mcu_version ≝ -λmcu:any_mcu_model.λt:memory_impl. - build_memory_type_of_mcu_version_aux t (memory_type_of_mcu_version mcu) (out_of_bound_memory t). - -(* sarebbe programma da caricare/zero_memory, ora test *) -ndefinition memory_of_mcu_version ≝ -λmcu:any_mcu_model.λt:memory_impl.match mcu with - [ FamilyHC05 m ⇒ match m with - [ MC68HC05J5A ⇒ zero_memory t - (*..*) - ] - | FamilyHC08 m ⇒ match m with - [ MC68HC08AB16A ⇒ zero_memory t - (*..*) - ] - (* tralascio l'enumerazione dei casi, per ora e' tutto 0 *) - | FamilyHCS08 _ ⇒ zero_memory t - | FamilyRS08 _ ⇒ zero_memory t - ]. - -(* - parametrizzati i non deterministici rispetto a tutti i valori casuali - che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5). - l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione - (reset V-low), la memoria ed il check puo' essere passata, per esempio da - - (memory_of_mcu_version MC68HC05J5A) - - (build_memory_type_of_mcu_version MC68HC05J5A) -*) -ndefinition start_of_mcu_version_HC05 ≝ -λmcu:HC05_mcu_model.λt:memory_impl. -λmem:aux_mem_type t.λchk:aux_chk_type t. -λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool. - let build ≝ λspm,spf,pcm:word16. - let fetched_pc ≝ mk_word16 (mem_read_abs t mem (and_w16 〈〈xF,xF〉:〈xF,xE〉〉 pcm)) - (mem_read_abs t mem (and_w16 〈〈xF,xF〉:〈xF,xF〉〉 pcm)) in - mk_any_status HC05 t - (mk_alu_HC05 - (* acc_low: ? *) ndby1 (* indx_low: ? *) ndby2 - (* sp: reset *) (or_w16 (and_w16 〈〈x0,x0〉:〈xF,xF〉〉 spm) spf) spm spf - (* pc: reset+fetch *) (and_w16 fetched_pc pcm) pcm - (* H: ? *) ndbo1 (* I: reset *) true (* N: ? *) ndbo2 - (* Z: ? *) ndbo3 (* C: ? *) ndbo4 (* IRQ: ? *) irqfl) - (* mem *) mem - (* chk *) chk - (* clk: reset *) (None ?) in - match mcu with - [ MC68HC05J5A ⇒ build 〈〈x0,x0〉:〈x3,xF〉〉 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉 - (*..*) - ]. - -ndefinition start_of_mcu_version_HC08 ≝ -λmcu:HC08_mcu_model.λt:memory_impl. -λmem:aux_mem_type t.λchk:aux_chk_type t. -λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool. - let fetched_pc ≝ mk_word16 (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xE〉〉) - (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xF〉〉) in - mk_any_status HC08 t - (mk_alu_HC08 - (* acc_low: ? *) ndby1 (* indw_low: ? *) ndby2 (* indx_high: reset *) 〈x0,x0〉 - (* sp: reset *) 〈〈x0,x0〉:〈xF,xF〉〉 (* pc: reset+fetch *) fetched_pc - (* V: ? *) ndbo1 (* H: ? *) ndbo2 (* I: reset *) true - (* N: ? *) ndbo3 (* Z: ? *) ndbo4 (* C: ? *) ndbo5 (* IRQ: ? *) irqfl) - (* mem *) mem - (* chk *) chk - (* clk: reset *) (None ?). - -ndefinition start_of_mcu_version_HCS08 ≝ -λmcu:HCS08_mcu_model.λt:memory_impl. -λmem:aux_mem_type t.λchk:aux_chk_type t. -λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool. - let fetched_pc ≝ mk_word16 (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xE〉〉) - (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xF〉〉) in - mk_any_status HCS08 t - (mk_alu_HC08 - (* acc_low: ? *) ndby1 (* indw_low: ? *) ndby2 (* indx_high: reset *) 〈x0,x0〉 - (* sp: reset *) 〈〈x0,x0〉:〈xF,xF〉〉 (* pc: reset+fetch *) fetched_pc - (* V: ? *) ndbo1 (* H: ? *) ndbo2 (* I: reset *) true - (* N: ? *) ndbo3 (* Z: ? *) ndbo4 (* C: ? *) ndbo5 (* IRQ: ? *) irqfl) - (* mem *) mem - (* chk *) chk - (* clk: reset *) (None ?). - -ndefinition start_of_mcu_version_RS08 ≝ -λmcu:RS08_mcu_model.λt:memory_impl. -λmem:aux_mem_type t.λchk:aux_chk_type t. -λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool. - let build ≝ λpcm. - mk_any_status RS08 t - (mk_alu_RS08 - (* acc_low: reset *) 〈x0,x0〉 - (* pc: reset *) (and_w16 〈〈xF,xF〉:〈xF,xD〉〉 pcm) pcm - (* spc: reset *) (and_w16 〈〈xF,xF〉:〈xF,xD〉〉 pcm) - (* xm: reset *) 〈x0,x0〉 (* psm: *) 〈x8,x0〉 - (* Z: reset *) false (* C: reset *) false) - (* mem *) mem - (* chk *) chk - (* clk: reset *) (None ?) in - (* tralascio l'enumerazione dei casi, tanto i valori sono uguali *) - build 〈〈x3,xF〉:〈xF,xF〉〉. - -(* - cio' che non viene resettato mantiene il valore precedente: nella documentazione - viene riportato come "unaffected"/"indeterminate"/"unpredictable" - il soft RESET e' diverso da un calo di tensione e la ram non variera' -*) -ndefinition reset_of_mcu ≝ -λm:mcu_type.λt:memory_impl. -let pc_reset_h ≝ 〈〈xF,xF〉:〈xF,xE〉〉 in -let pc_reset_l ≝ 〈〈xF,xF〉:〈xF,xF〉〉 in -let pc_RS08_reset ≝ 〈〈xF,xF〉:〈xF,xD〉〉 in -let sp_reset ≝ 〈〈x0,x0〉:〈xF,xF〉〉 in - match m return λm:mcu_type.(any_status m t) → (any_status m t) with -(* HC05: parzialmente non deterministico *) - [ HC05 ⇒ λs:any_status HC05 t.match s with - [ mk_any_status alu mem chk clk ⇒ match alu with - [ mk_alu_HC05 acclow indxlow _ spm spf _ pcm hfl _ nfl zfl cfl irqfl ⇒ - let fetched_pc ≝ mk_word16 (mem_read_abs t mem (and_w16 pc_reset_h pcm)) - (mem_read_abs t mem (and_w16 pc_reset_l pcm)) in - mk_any_status HC05 t - (mk_alu_HC05 - (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow - (* sp: reset *) (or_w16 (and_w16 sp_reset spm) spf) spm spf - (* pc: reset+fetch *) (and_w16 fetched_pc pcm) pcm - (* H: inv. *) hfl (* I: reset *) true (* N: inv. *) nfl - (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl) - (* mem: inv. *) mem - (* chk: inv. *) chk - (* clk: reset *) (None ?) ]] -(* HC08: parzialmente non deterministico *) - | HC08 ⇒ λs:any_status HC08 t.match s with - [ mk_any_status alu mem chk clk ⇒ match alu with - [ mk_alu_HC08 acclow indxlow _ _ _ vfl hfl _ nfl zfl cfl irqfl ⇒ - let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h) - (mem_read_abs t mem pc_reset_l) in - mk_any_status HC08 t - (mk_alu_HC08 - (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow (* indx_high: reset *) 〈x0,x0〉 - (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc - (* V: inv. *) vfl (* H: inv. *) hfl (* I: reset *) true - (* N: inv. *) nfl (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl) - (* mem: inv. *) mem - (* chk: inv. *) chk - (* clk: reset *) (None ?) ]] -(* HCS08: parzialmente non deterministico *) - | HCS08 ⇒ λs:any_status HCS08 t.match s with - [ mk_any_status alu mem chk clk ⇒ match alu with - [ mk_alu_HC08 acclow indxlow _ _ _ vfl hfl _ nfl zfl cfl irqfl ⇒ - let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h) - (mem_read_abs t mem pc_reset_l) in - mk_any_status HCS08 t - (mk_alu_HC08 - (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow (* indx_high: reset *) 〈x0,x0〉 - (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc - (* V: inv. *) vfl (* H: inv. *) hfl (* I: reset *) true - (* N: inv. *) nfl (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl) - (* mem: inv. *) mem - (* chk: inv. *) chk - (* clk: reset *) (None ?) ]] -(* RS08: deterministico *) - | RS08 ⇒ λs:any_status RS08 t.match s with - [ mk_any_status alu mem chk clk ⇒ match alu with - [ mk_alu_RS08 _ _ pcm _ _ _ _ _ ⇒ - mk_any_status RS08 t - (mk_alu_RS08 - (* acc_low: reset *) 〈x0,x0〉 - (* pc: reset *) (and_w16 pc_RS08_reset pcm) pcm - (* spc: reset *) (and_w16 pc_RS08_reset pcm) - (* xm: reset *) 〈x0,x0〉 (* psm: reset *) 〈x8,x0〉 - (* Z: reset *) false (* C: reset *) false) - (* mem: inv. *) mem - (* chk: inv. *) chk - (* clk: reset *) (None ?) ]] - ].