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 4f6d713d1e1d9e0e7b497d6128e3c448b4f29f8b..5dad70809d036fb226473c97bbfbd39093b9d8fe 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/model.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/model.ma
@@ -62,20 +62,21 @@ ndefinition HC08_mcu_model_rect : ΠP:HC08_mcu_model → Type.P MC68HC08AB16A 
 
 (* modelli di HCS08 *)
 ninductive HCS08_mcu_model : Type ≝
-  MC9S08GB60  : HCS08_mcu_model
+  MC9S08AW60 : HCS08_mcu_model
+| MC9S08GB60 : HCS08_mcu_model
   (*..*).
 
-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_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 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_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 MC9S08GB60 → Πh:HCS08_mcu_model.P h ≝
-λP:HCS08_mcu_model → Type.λp:P MC9S08GB60.λh:HCS08_mcu_model.
- match h with [ MC9S08GB60 ⇒ 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 ≝
@@ -187,7 +188,15 @@ ndefinition memory_type_of_FamilyHC08 ≝
 (* memoria degli HCS08 *)
 ndefinition memory_type_of_FamilyHCS08 ≝
 λm:HCS08_mcu_model.match m with
-  [ MC9S08GB60 ⇒
+  [ 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 *)