freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / model.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/model.ma b/helm/software/matita/contribs/ng_assembly/freescale/model.ma
index 95c26f5e070658570a1b252de15f043152f6e1f7..fe01726c7cfbf1bf9d34cdcfe4519cc690542ab5 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/model.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/model.ma
@@ -13,15 +13,11 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 include "freescale/status.ma".
@@ -35,69 +31,22 @@ ninductive HC05_mcu_model : Type ≝
   MC68HC05J5A: HC05_mcu_model
   (*..*).
 
-ndefinition HC05_mcu_model_ind : ΠP:HC05_mcu_model → Prop.P MC68HC05J5A → Πh:HC05_mcu_model.P h ≝
-λP:HC05_mcu_model → Prop.λp:P MC68HC05J5A.λh:HC05_mcu_model.
- match h with [ MC68HC05J5A ⇒ p ].
-
-ndefinition HC05_mcu_model_rec : ΠP:HC05_mcu_model → Set.P MC68HC05J5A → Πh:HC05_mcu_model.P h ≝
-λP:HC05_mcu_model → Set.λp:P MC68HC05J5A.λh:HC05_mcu_model.
- match h with [ MC68HC05J5A ⇒ p ].
-
-ndefinition HC05_mcu_model_rect : ΠP:HC05_mcu_model → Type.P MC68HC05J5A → Πh:HC05_mcu_model.P h ≝
-λP:HC05_mcu_model → Type.λp:P MC68HC05J5A.λh:HC05_mcu_model.
- match h with [ MC68HC05J5A ⇒ p ].
-
 (* modelli di HC08 *)
 ninductive HC08_mcu_model : Type ≝
   MC68HC08AB16A: HC08_mcu_model
   (*..*). 
 
-ndefinition HC08_mcu_model_ind : ΠP:HC08_mcu_model → Prop.P MC68HC08AB16A → Πh:HC08_mcu_model.P h ≝
-λP:HC08_mcu_model → Prop.λp:P MC68HC08AB16A.λh:HC08_mcu_model.
- match h with [ MC68HC08AB16A ⇒ p ].
-
-ndefinition HC08_mcu_model_rec : ΠP:HC08_mcu_model → Set.P MC68HC08AB16A → Πh:HC08_mcu_model.P h ≝
-λP:HC08_mcu_model → Set.λp:P MC68HC08AB16A.λh:HC08_mcu_model.
- match h with [ MC68HC08AB16A ⇒ p ].
-
-ndefinition HC08_mcu_model_rect : ΠP:HC08_mcu_model → Type.P MC68HC08AB16A → Πh:HC08_mcu_model.P h ≝
-λP:HC08_mcu_model → Type.λp:P MC68HC08AB16A.λh:HC08_mcu_model.
- match h with [ MC68HC08AB16A ⇒ p ].
-
 (* modelli di HCS08 *)
 ninductive HCS08_mcu_model : Type ≝
-  MC9S08AW60  : HCS08_mcu_model
+  MC9S08AW60 : HCS08_mcu_model
+| MC9S08GB60 : HCS08_mcu_model
   (*..*).
 
-ndefinition HCS08_mcu_model_ind : ΠP:HCS08_mcu_model → Prop.P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝
-λP:HCS08_mcu_model → Prop.λp:P MC9S08AW60.λh:HCS08_mcu_model.
- match h with [ MC9S08AW60 ⇒ p ].
-
-ndefinition HCS08_mcu_model_rec : ΠP:HCS08_mcu_model → Set.P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝
-λP:HCS08_mcu_model → Set.λp:P MC9S08AW60.λh:HCS08_mcu_model.
- match h with [ MC9S08AW60 ⇒ p ].
-
-ndefinition HCS08_mcu_model_rect : ΠP:HCS08_mcu_model → Type.P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝
-λP:HCS08_mcu_model → Type.λp:P MC9S08AW60.λh:HCS08_mcu_model.
- match h with [ MC9S08AW60 ⇒ p ].
-
 (* modelli di RS08 *)
 ninductive RS08_mcu_model : Type ≝
   MC9RS08KA1 : RS08_mcu_model
 | MC9RS08KA2 : RS08_mcu_model.
 
-ndefinition RS08_mcu_model_ind : ΠP:RS08_mcu_model → Prop.P MC9RS08KA1 → P MC9RS08KA2 → Πr:RS08_mcu_model.P r ≝
-λP:RS08_mcu_model → Prop.λp:P MC9RS08KA1.λp1:P MC9RS08KA2.λr:RS08_mcu_model.
-  match r with [ MC9RS08KA1 ⇒ p | MC9RS08KA2 ⇒ p1 ].
-
-ndefinition RS08_mcu_model_rec : ΠP:RS08_mcu_model → Set.P MC9RS08KA1 → P MC9RS08KA2 → Πr:RS08_mcu_model.P r ≝
-λP:RS08_mcu_model → Set.λp:P MC9RS08KA1.λp1:P MC9RS08KA2.λr:RS08_mcu_model.
-  match r with [ MC9RS08KA1 ⇒ p | MC9RS08KA2 ⇒ p1 ].
-
-ndefinition RS08_mcu_model_rect : ΠP:RS08_mcu_model → Type.P MC9RS08KA1 → P MC9RS08KA2 → Πr:RS08_mcu_model.P r ≝
-λP:RS08_mcu_model → Type.λp:P MC9RS08KA1.λp1:P MC9RS08KA2.λr:RS08_mcu_model.
-  match r with [ MC9RS08KA1 ⇒ p | MC9RS08KA2 ⇒ p1 ].
-
 (* raggruppamento dei modelli *)
 ninductive any_mcu_model : Type ≝
   FamilyHC05  : HC05_mcu_model → any_mcu_model
@@ -105,30 +54,6 @@ ninductive any_mcu_model : Type ≝
 | FamilyHCS08 : HCS08_mcu_model → any_mcu_model
 | FamilyRS08  : RS08_mcu_model → any_mcu_model.
 
-ndefinition any_mcu_model_ind
- : ΠP:any_mcu_model → Prop.(Πn:HC05_mcu_model.P (FamilyHC05 n)) → (Πn:HC08_mcu_model.P (FamilyHC08 n)) →
-   (Πn:HCS08_mcu_model.P (FamilyHCS08 n)) → (Πn:RS08_mcu_model.P (FamilyRS08 n))→Πa:any_mcu_model.P a ≝
-λP:any_mcu_model → Prop.λf:Πn:HC05_mcu_model.P (FamilyHC05 n).λf1:Πn:HC08_mcu_model.P (FamilyHC08 n).
-λf2:Πn:HCS08_mcu_model.P (FamilyHCS08 n).λf3:Πn:RS08_mcu_model.P (FamilyRS08 n).λa:any_mcu_model.
- match a with [ FamilyHC05 n ⇒ f n | FamilyHC08 n ⇒ f1 n
-              | FamilyHCS08 n ⇒ f2 n | FamilyRS08 n ⇒ f3 n ].
-
-ndefinition any_mcu_model_rec
- : ΠP:any_mcu_model → Set.(Πn:HC05_mcu_model.P (FamilyHC05 n)) → (Πn:HC08_mcu_model.P (FamilyHC08 n)) →
-   (Πn:HCS08_mcu_model.P (FamilyHCS08 n)) → (Πn:RS08_mcu_model.P (FamilyRS08 n))→Πa:any_mcu_model.P a ≝
-λP:any_mcu_model → Set.λf:Πn:HC05_mcu_model.P (FamilyHC05 n).λf1:Πn:HC08_mcu_model.P (FamilyHC08 n).
-λf2:Πn:HCS08_mcu_model.P (FamilyHCS08 n).λf3:Πn:RS08_mcu_model.P (FamilyRS08 n).λa:any_mcu_model.
- match a with [ FamilyHC05 n ⇒ f n | FamilyHC08 n ⇒ f1 n
-              | FamilyHCS08 n ⇒ f2 n | FamilyRS08 n ⇒ f3 n ].
-
-ndefinition any_mcu_model_rect
- : ΠP:any_mcu_model → Type.(Πn:HC05_mcu_model.P (FamilyHC05 n)) → (Πn:HC08_mcu_model.P (FamilyHC08 n)) →
-   (Πn:HCS08_mcu_model.P (FamilyHCS08 n)) → (Πn:RS08_mcu_model.P (FamilyRS08 n))→Πa:any_mcu_model.P a ≝
-λP:any_mcu_model → Type.λf:Πn:HC05_mcu_model.P (FamilyHC05 n).λf1:Πn:HC08_mcu_model.P (FamilyHC08 n).
-λf2:Πn:HCS08_mcu_model.P (FamilyHCS08 n).λf3:Πn:RS08_mcu_model.P (FamilyRS08 n).λa:any_mcu_model.
- match a with [ FamilyHC05 n ⇒ f n | FamilyHC08 n ⇒ f1 n
-              | FamilyHCS08 n ⇒ f2 n | FamilyRS08 n ⇒ f3 n ].
-
 (* 
 condizioni errore interne alla MCU
 (Il programma viene caricato dal produttore in ROM o impostato in EEPROM)
@@ -162,9 +87,9 @@ ndefinition memory_type_of_FamilyHC05 ≝
   (* 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 *)
+     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 *)
     ]
    (*..*)
   ].
@@ -180,11 +105,11 @@ ndefinition memory_type_of_FamilyHC08 ≝
   (* 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 *) ]
+     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 *) ]
    (*..*)
   ].
 
@@ -196,9 +121,17 @@ ndefinition memory_type_of_FamilyHCS08 ≝
   (* 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 *) ]
+     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 *)
@@ -206,30 +139,30 @@ 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 *)
+     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 *)
+   ; 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 *)
+   ; 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 *)
+   ; 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 *) ]
+   ; 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 *)
+     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 *)
+   ; 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 *)
+   ; 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 *)
+   ; 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 *) ]
+   ; 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 *)