X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmodel.ma;h=5dad70809d036fb226473c97bbfbd39093b9d8fe;hb=633b66b935bbc2c38a5abc2be958359335123258;hp=95c26f5e070658570a1b252de15f043152f6e1f7;hpb=9f580d9bf8f6ba6950b252f587166e95bc8fb1a8;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
index 95c26f5e0..5dad70809 100755
--- 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,21 @@ ndefinition HC08_mcu_model_rect : ΠP:HC08_mcu_model → Type.P MC68HC08AB16A 
 
 (* 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_ind : ΠP:HCS08_mcu_model → Prop.P MC9S08GB60 → P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝
+λP:HCS08_mcu_model → Prop.λp:P MC9S08GB60.λp1:P MC9S08AW60.λh:HCS08_mcu_model.
+ match h with [ MC9S08GB60 ⇒ p | MC9S08AW60 ⇒ p1 ].
 
-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 → P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝
+λP:HCS08_mcu_model → Set.λp:P MC9S08GB60.λp1:P MC9S08AW60.λh:HCS08_mcu_model.
+ match h with [ MC9S08GB60 ⇒ p | MC9S08AW60 ⇒ p1 ].
 
-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 → P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝
+λP:HCS08_mcu_model → Type.λp:P MC9S08GB60.λp1:P MC9S08AW60.λh:HCS08_mcu_model.
+ match h with [ MC9S08GB60 ⇒ p | MC9S08AW60 ⇒ p1 ].
 
 (* modelli di RS08 *)
 ninductive RS08_mcu_model : Type ≝
@@ -199,6 +196,14 @@ ndefinition memory_type_of_FamilyHCS08 ≝
      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 *)