(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
(*
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
+ match inrange_w16 addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
[ true ⇒ fMEM mem chk (or_w16 (fst … (shr_w16 (fst … (shr_w16 〈psm:〈x0,x0〉〉))))
(and_w16 addr 〈〈x0,x0〉:〈x3,xF〉〉))
(*
(*
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
+ match inrange_w16 addr 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
[ 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))
λ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.Some ? (triple … s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc 2)))).
+ (λbl.Some ? (triple … s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc nat2)))).
(* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
ndefinition mode_DIR1_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
opt_map … (memory_filter_read m t s cur_pc)
- (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
+ (λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc nat1).
(* lettura da [byte [curpc]]: loadbit *)
ndefinition mode_DIR1n_load ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.
opt_map … (memory_filter_read m t s cur_pc)
- (λaddr.loadbit_from m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1).
+ (λaddr.loadbit_from m t s 〈〈x0,x0〉:addr〉 sub cur_pc nat1).
(* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
ndefinition mode_DIR1_write ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
opt_map … (memory_filter_read m t s cur_pc)
- (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 writebw).
+ (λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc nat1 writebw).
(* scrittura su [byte [curpc]]: writebit *)
ndefinition mode_DIR1n_write ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λsub:oct.λwriteb:bool.
opt_map … (memory_filter_read m t s cur_pc)
- (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1 writeb).
+ (λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc nat1 writeb).
(* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
ndefinition mode_DIR2_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
opt_map … (memory_filter_read m t s cur_pc)
(λaddrh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
- (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc 2)).
+ (λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc nat2)).
(* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
ndefinition mode_DIR2_write ≝
λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
opt_map … (memory_filter_read m t s cur_pc)
(λaddrh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
- (λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc 2 writebw)).
+ (λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc nat2 writebw)).
ndefinition get_IX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.
ndefinition mode_IX0_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
opt_map … (get_IX m t s)
- (λaddr.(aux_load m t byteflag) s addr cur_pc 0).
+ (λaddr.(aux_load m t byteflag) s addr cur_pc O).
(* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
ndefinition mode_IX0_write ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
opt_map … (get_IX m t s)
- (λaddr.(aux_write m t byteflag) s addr cur_pc 0 writebw).
+ (λaddr.(aux_write m t byteflag) s addr cur_pc O writebw).
(* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
ndefinition mode_IX1_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
opt_map … (get_IX m t s)
(λaddr.opt_map … (memory_filter_read m t s cur_pc)
- (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
+ (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc nat1)).
(* lettura da X+[byte curpc] *)
ndefinition mode_IX1ADD_load ≝
λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
opt_map … (get_IX m t s)
(λaddr.opt_map … (memory_filter_read m t s cur_pc)
- (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
+ (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc nat1 writebw)).
(* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
ndefinition mode_IX2_load ≝
opt_map … (get_IX m t s)
(λaddr.opt_map … (memory_filter_read m t s cur_pc)
(λ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_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
+ (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc nat2))).
(* lettura da X+[word curpc] *)
ndefinition mode_IX2ADD_load ≝
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 ? (triple … s (plus_w16_d_d addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc 2))))).
+ (λaddr.Some ? (triple … s (plus_w16_d_d addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc nat2))))).
(* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
ndefinition mode_IX2_write ≝
opt_map … (get_IX m t s)
(λaddr.opt_map … (memory_filter_read m t s cur_pc)
(λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
- (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
+ (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc nat2 writebw))).
(* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
ndefinition mode_SP1_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
opt_map … (get_sp_reg m t s)
(λaddr.opt_map … (memory_filter_read m t s cur_pc)
- (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
+ (λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc nat1)).
(* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
ndefinition mode_SP1_write ≝
λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
opt_map … (get_sp_reg m t s)
(λaddr.opt_map … (memory_filter_read m t s cur_pc)
- (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
+ (λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc nat1 writebw)).
(* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
ndefinition mode_SP2_load ≝
opt_map … (get_sp_reg m t s)
(λaddr.opt_map … (memory_filter_read m t s cur_pc)
(λ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_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
+ (λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc nat2))).
(* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
ndefinition mode_SP2_write ≝
opt_map … (get_sp_reg m t s)
(λaddr.opt_map … (memory_filter_read m t s cur_pc)
(λoffsh.opt_map … (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
- (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
+ (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc nat2 writebw))).
(* ************************************** *)
(* raccordo di tutte le possibili letture *)
ndefinition multi_mode_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.
match byteflag
- return λbyteflag:bool.any_status m t → word16 → instr_mode →
- option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16)
+ return λbyteflag:bool.any_status m t → word16 → instr_mode →
+ option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16)
with
(* lettura di un byte *)
[ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
| MODE_TNY e ⇒ opt_map … (memory_filter_read m t s 〈〈x0,x0〉:〈x0,e〉〉)
(λb.Some ? (triple … s b cur_pc))
(* preleva 1 byte da 0000 0000 000x xxxxb *)
- | MODE_SRT e ⇒ opt_map … (memory_filter_read m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉)
+ | MODE_SRT e ⇒ opt_map … (memory_filter_read m t s 〈〈x0,x0〉:(b8_of_bit e)〉)
(λb.Some ? (triple … s b cur_pc))
]
(* lettura di una word *)
| MODE_TNY e ⇒ opt_map … (memory_filter_write m t s 〈〈x0,x0〉:〈x0,e〉〉 writeb)
(λ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)
+ | MODE_SRT e ⇒ opt_map … (memory_filter_write m t s 〈〈x0,x0〉:(b8_of_bit e)〉 writeb)
(λ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