(* 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 ≝
(* 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 *)