(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
-set "baseuri" "cic:/matita/freescale/load_write/".
-
-(*include "/media/VIRTUOSO/freescale/model.ma".*)
include "freescale/model.ma".
(* errori possibili nel fetch *)
accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
*)
match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
- [ true ⇒ fMEM mem chk (or_w16 (fstT ?? (shr_w16 (fstT ?? (shr_w16 〈psm:〈x0,x0〉〉))))
+ [ true ⇒ fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
(and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉))
(*
accesso normale
accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
*)
match in_range addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
- [ true ⇒ opt_map ?? (fMEM mem chk (or_w16 (fstT ?? (shr_w16 (fstT ?? (shr_w16 〈psm:〈x0,x0〉〉))))
+ [ true ⇒ opt_map ?? (fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
(and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉)))
(λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
(*
definition writeb_to ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwriteb:byte8.
opt_map ?? (memory_filter_write m t s addr writeb)
- (λtmps.Some ? (pairT ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
+ (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
(* scrittura bit su addr *)
definition writebit_to ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.λwriteb:bool.
opt_map ?? (memory_filter_write_bit m t s addr sub writeb)
- (λtmps.Some ? (pairT ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
+ (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
(* scrittura word su addr *)
definition writew_to ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
opt_map ?? (memory_filter_write m t s addr (w16h writew))
- (λtmps.opt_map ?? (memory_filter_write m t s (succ_w16 addr) (w16l writew))
- (λtmps'.Some ? (pairT ?? tmps' (filtered_plus_w16 m t s cur_pc fetched)))).
+ (λtmps1.opt_map ?? (memory_filter_write m t tmps1 (succ_w16 addr) (w16l writew))
+ (λtmps2.Some ? (pair ?? tmps2 (filtered_plus_w16 m t tmps2 cur_pc fetched)))).
(* ausiliari per definire i tipi e la lettura/scrittura *)
λm:mcu_type.λt:memory_impl.λbyteflag:bool.
any_status m t → word16 → word16 → nat →
match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
- option (ProdT (any_status m t) word16).
+ option (Prod (any_status m t) word16).
(* per non dover ramificare i vari load in byte/word *)
definition aux_write ≝
opt_map ?? (memory_filter_read m t s cur_pc)
(λb.Some ? (tripleT ??? s b (filtered_inc_w16 m t s cur_pc))).
+(* lettura da [curpc]: IMM1 + estensione a word *)
+definition mode_IMM1EXT_load ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map ?? (memory_filter_read m t s cur_pc)
+ (λb.Some ? (tripleT ??? s 〈〈x0,x0〉:b〉 (filtered_inc_w16 m t s cur_pc))).
+
(* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
definition mode_IMM2_load ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
(λaddr.opt_map ?? (memory_filter_read m t s cur_pc)
(λoffs.(aux_load m t byteflag) s (plus_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
+(* lettura da X+[byte curpc] *)
+definition mode_IX1ADD_load ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map ?? (memory_filter_read m t s cur_pc)
+ (λb.opt_map ?? (get_IX m t s)
+ (λaddr.Some ? (tripleT ??? s (plus_w16nc addr 〈〈x0,x0〉:b〉) (filtered_inc_w16 m t s cur_pc)))).
+
(* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
definition mode_IX1_write ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
(λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
(λoffsl.(aux_load m t byteflag) s (plus_w16nc addr 〈offsh:offsl〉) cur_pc 2))).
+(* lettura da X+[word curpc] *)
+definition mode_IX2ADD_load ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
+ opt_map ?? (memory_filter_read m t s cur_pc)
+ (λbh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
+ (λbl.opt_map ?? (get_IX m t s)
+ (λaddr.Some ? (tripleT ??? s (plus_w16nc addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc 2))))).
+
(* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
definition mode_IX2_write ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
| MODE_INHH ⇒ opt_map ?? (get_indX_8_high_reg m t s)
(λindx.Some ? (tripleT ??? s indx cur_pc))
+(* NO: solo lettura word *)
+ | MODE_INHX0ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX1ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX2ADD ⇒ None ?
+
(* preleva 1 byte immediato *)
| MODE_IMM1 ⇒ mode_IMM1_load m t s cur_pc
+(* NO: solo lettura word *)
+ | MODE_IMM1EXT ⇒ None ?
(* NO: solo lettura word *)
| MODE_IMM2 ⇒ None ?
(* preleva 1 byte da indirizzo diretto 1 byte *)
(* NO: solo lettura/scrittura byte *)
| MODE_INHH ⇒ None ?
+(* preleva 1 word immediato *)
+ | MODE_INHX0ADD ⇒ opt_map ?? (get_IX m t s)
+ (λw.Some ? (tripleT ??? s w cur_pc))
+(* preleva 1 word immediato *)
+ | MODE_INHX1ADD ⇒ mode_IX1ADD_load m t s cur_pc
+(* preleva 1 word immediato *)
+ | MODE_INHX2ADD ⇒ mode_IX2ADD_load m t s cur_pc
+
(* NO: solo lettura byte *)
| MODE_IMM1 ⇒ None ?
+(* preleva 1 word immediato *)
+ | MODE_IMM1EXT ⇒ mode_IMM1EXT_load m t s cur_pc
(* preleva 1 word immediato *)
| MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
(* preleva 1 word da indirizzo diretto 1 byte *)
λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
return λbyteflag:bool.any_status m t → word16 → instr_mode →
match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
- option (ProdT (any_status m t) word16) with
+ option (Prod (any_status m t) word16) with
(* scrittura di un byte *)
[ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwriteb:byte8.match i with
(* NO: non ci sono indicazioni *)
[ MODE_INH ⇒ None ?
(* scrive A *)
- | MODE_INHA ⇒ Some ? (pairT ?? (set_acc_8_low_reg m t s writeb) cur_pc)
+ | MODE_INHA ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
(* scrive X *)
| MODE_INHX ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
- (λtmps.Some ? (pairT ?? tmps cur_pc))
+ (λtmps.Some ? (pair ?? tmps cur_pc))
(* scrive H *)
| MODE_INHH ⇒ opt_map ?? (set_indX_8_high_reg m t s writeb)
- (λtmps.Some ? (pairT ?? tmps cur_pc))
+ (λtmps.Some ? (pair ?? tmps cur_pc))
+
+(* NO: solo lettura word *)
+ | MODE_INHX0ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX1ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX2ADD ⇒ None ?
(* NO: solo lettura byte *)
| MODE_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM1EXT ⇒ None ?
(* NO: solo lettura word *)
| MODE_IMM2 ⇒ None ?
(* scrive 1 byte su indirizzo diretto 1 byte *)
| MODE_IMM1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
(* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
| MODE_IX0p_to_DIR1 ⇒ opt_map ?? (mode_DIR1_write true m t s cur_pc writeb)
- (λS_and_PC.match S_and_PC with [ pairT S_op PC_op ⇒
+ (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
(* H:X++ *)
opt_map ?? (aux_inc_indX_16 m t S_op)
- (λS_op'.Some ? (pairT ?? S_op' PC_op))])
+ (λS_op'.Some ? (pair ?? S_op' PC_op))])
(* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
| MODE_DIR1_to_IX0p ⇒ opt_map ?? (mode_IX0_write true m t s cur_pc writeb)
- (λS_and_PC.match S_and_PC with [ pairT S_op PC_op ⇒
+ (λS_and_PC.match S_and_PC with [ pair S_op PC_op ⇒
(* H:X++ *)
opt_map ?? (aux_inc_indX_16 m t S_op)
- (λS_op'.Some ? (pairT ?? S_op' PC_op))])
+ (λS_op'.Some ? (pair ?? S_op' PC_op))])
(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
- | MODE_INHA_and_IMM1 ⇒ Some ? (pairT ?? (set_acc_8_low_reg m t s writeb) cur_pc)
+ | MODE_INHA_and_IMM1 ⇒ Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)
| MODE_INHX_and_IMM1 ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
- (λtmps.Some ? (pairT ?? tmps cur_pc))
+ (λtmps.Some ? (pair ?? tmps cur_pc))
(* NO: solo lettura word *)
| MODE_IMM1_and_IMM1 ⇒ None ?
(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *)
| MODE_DIRn_and_IMM1 _ ⇒ None ?
(* scrive 1 byte su 0000 0000 0000 xxxxb *)
| MODE_TNY e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:〈x0,e〉〉 writeb)
- (λtmps.Some ? (pairT ?? tmps cur_pc))
+ (λtmps.Some ? (pair ?? tmps cur_pc))
(* scrive 1 byte su 0000 0000 000x xxxxb *)
| MODE_SRT e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉 writeb)
- (λtmps.Some ? (pairT ?? tmps cur_pc)) ]
+ (λtmps.Some ? (pair ?? tmps cur_pc)) ]
(* scrittura di una word *)
| false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwritew:word16.match i with
(* NO: non ci sono indicazioni *)
(* NO: solo lettura/scrittura byte *)
| MODE_INHH ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX0ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX1ADD ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_INHX2ADD ⇒ None ?
+
(* NO: solo lettura byte *)
| MODE_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM1EXT ⇒ None ?
(* NO: solo lettura word *)
| MODE_IMM2 ⇒ None ?
(* scrive 1 word su indirizzo diretto 1 byte *)