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