+++ /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 *)
-(* 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 ?) ]]
- ].
projects / helm.git / blobdiff