freescale porting, work in progress

[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..4f6d713d1e1d9e0e7b497d6128e3c448b4f29f8b 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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 include "freescale/status.ma".
@@ -66,20 +62,20 @@ ndefinition HC08_mcu_model_rect : ΠP:HC08_mcu_model → Type.P MC68HC08AB16A 
 
 (* modelli di HCS08 *)
 ninductive HCS08_mcu_model : Type ≝
-  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_ind : ΠP:HCS08_mcu_model → Prop.P MC9S08GB60 → Πh:HCS08_mcu_model.P h ≝
+λP:HCS08_mcu_model → Prop.λp:P MC9S08GB60.λh:HCS08_mcu_model.
+ match h with [ MC9S08GB60 ⇒ 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_rec : ΠP:HCS08_mcu_model → Set.P MC9S08GB60 → Πh:HCS08_mcu_model.P h ≝
+λP:HCS08_mcu_model → Set.λp:P MC9S08GB60.λh:HCS08_mcu_model.
+ match h with [ MC9S08GB60 ⇒ 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 ].
+ndefinition HCS08_mcu_model_rect : ΠP:HCS08_mcu_model → Type.P MC9S08GB60 → Πh:HCS08_mcu_model.P h ≝
+λP:HCS08_mcu_model → Type.λp:P MC9S08GB60.λh:HCS08_mcu_model.
+ match h with [ MC9S08GB60 ⇒ p ].
 
 (* modelli di RS08 *)
 ninductive RS08_mcu_model : Type ≝
@@ -191,14 +187,14 @@ ndefinition memory_type_of_FamilyHC08 ≝
 (* memoria degli HCS08 *)
 ndefinition memory_type_of_FamilyHCS08 ≝
 λm:HCS08_mcu_model.match m with
-  [ MC9S08AW60 ⇒
+  [ MC9S08GB60 ⇒
    [ 
   (* 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〉:〈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 *)