-(* 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 *)
- match in_range 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〉〉))))
+ 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〉〉))))
ndefinition memory_filter_read ≝
λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → option byte8 with
[ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.
ndefinition memory_filter_read ≝
λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → option byte8 with
[ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.
ndefinition memory_filter_read_bit ≝
λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → oct → option bool with
[ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.
ndefinition memory_filter_read_bit ≝
λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → oct → option bool with
[ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.
altrimenti sarebbero 2 indirezioni
*)
match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
altrimenti sarebbero 2 indirezioni
*)
match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
(λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
| false ⇒
(*
accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
*)
(λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
| false ⇒
(*
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 (fst ?? (shr_w16 (fst ?? (shr_w16 〈psm:〈x0,x0〉〉))))
+ 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))
(*
accesso normale
*)
(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))
(*
accesso normale
*)
(λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk)) ]]]]]].
(* scrittura RS08 di un byte *)
(λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk)) ]]]]]].
(* scrittura RS08 di un byte *)
λm:mcu_type.λt:memory_impl.match m
return λm:mcu_type.any_status m t → word16 → byte8 → option (any_status m t) with
[ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λval:byte8.
λm:mcu_type.λt:memory_impl.match m
return λm:mcu_type.any_status m t → word16 → byte8 → option (any_status m t) with
[ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λval:byte8.
(λmem.Some ? (set_mem_desc ? t s mem))
| RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λval:byte8.
RS08_memory_filter_write t s addr val
(λmem.Some ? (set_mem_desc ? t s mem))
| RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λval:byte8.
RS08_memory_filter_write t s addr val
λm:mcu_type.λt:memory_impl.match m
return λm:mcu_type.any_status m t → word16 → oct → bool → option (any_status m t) with
[ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.λval:bool.
λm:mcu_type.λt:memory_impl.match m
return λm:mcu_type.any_status m t → word16 → oct → bool → option (any_status m t) with
[ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.λval:bool.
(λmem.Some ? (set_mem_desc ? t s mem))
| HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.λval:bool.
(λmem.Some ? (set_mem_desc ? t s mem))
| HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.λval:bool.
(λmem.Some ? (set_mem_desc ? t s mem))
| HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.λval:bool.
(λmem.Some ? (set_mem_desc ? t s mem))
| HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.λval:bool.
(λmem.Some ? (set_mem_desc ? t s mem))
| RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
RS08_memory_filter_write_bit t s addr sub val
(λmem.Some ? (set_mem_desc ? t s mem))
| RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool.
RS08_memory_filter_write_bit t s addr sub val
(* lettura byte da addr *)
ndefinition loadb_from ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
(* lettura byte da addr *)
ndefinition loadb_from ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
- opt_map ?? (memory_filter_read m t s addr)
- (λb.Some ? (triple ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
+ opt_map … (memory_filter_read m t s addr)
+ (λb.Some ? (triple … s b (filtered_plus_w16 m t s cur_pc fetched))).
(* lettura bit da addr *)
ndefinition loadbit_from ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.
(* lettura bit da addr *)
ndefinition loadbit_from ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.
- opt_map ?? (memory_filter_read_bit m t s addr sub)
- (λb.Some ? (triple ??? s b (filtered_plus_w16 m t s cur_pc fetched))).
+ opt_map … (memory_filter_read_bit m t s addr sub)
+ (λb.Some ? (triple … s b (filtered_plus_w16 m t s cur_pc fetched))).
(* lettura word da addr *)
ndefinition loadw_from ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
(* lettura word da addr *)
ndefinition loadw_from ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.
- opt_map ?? (memory_filter_read m t s addr)
- (λbh.opt_map ?? (memory_filter_read m t s (succ_w16 addr))
- (λbl.Some ? (triple ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc fetched)))).
+ opt_map … (memory_filter_read m t s addr)
+ (λbh.opt_map … (memory_filter_read m t s (succ_w16 addr))
+ (λbl.Some ? (triple … s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc fetched)))).
(* scrittura byte su addr *)
ndefinition writeb_to ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwriteb:byte8.
(* scrittura byte su addr *)
ndefinition 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 ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
+ opt_map … (memory_filter_write m t s addr writeb)
+ (λtmps.Some ? (pair … tmps (filtered_plus_w16 m t s cur_pc fetched))).
(* scrittura bit su addr *)
ndefinition writebit_to ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.λwriteb:bool.
(* scrittura bit su addr *)
ndefinition 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 ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
+ opt_map … (memory_filter_write_bit m t s addr sub writeb)
+ (λtmps.Some ? (pair … tmps (filtered_plus_w16 m t s cur_pc fetched))).
(* scrittura word su addr *)
ndefinition writew_to ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
(* scrittura word su addr *)
ndefinition 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))
- (λ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)))).
+ opt_map … (memory_filter_write m t s addr (w16h writew))
+ (λ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)))).
(* lettura da [curpc]: IMM1 comportamento asimmetrico, quindi non si appoggia a loadb *)
ndefinition mode_IMM1_load ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
(* lettura da [curpc]: IMM1 comportamento asimmetrico, quindi non si appoggia a loadb *)
ndefinition mode_IMM1_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 ? (triple ??? s b (filtered_inc_w16 m t s cur_pc))).
+ opt_map … (memory_filter_read m t s cur_pc)
+ (λb.Some ? (triple … s b (filtered_inc_w16 m t s cur_pc))).
(* lettura da [curpc]: IMM1 + estensione a word *)
ndefinition mode_IMM1EXT_load ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
(* lettura da [curpc]: IMM1 + estensione a word *)
ndefinition 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 ? (triple ??? s 〈〈x0,x0〉:b〉 (filtered_inc_w16 m t s cur_pc))).
+ opt_map … (memory_filter_read m t s cur_pc)
+ (λb.Some ? (triple … s 〈〈x0,x0〉:b〉 (filtered_inc_w16 m t s cur_pc))).
(* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
ndefinition mode_IMM2_load ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
(* lettura da [curpc]: IMM2 comportamento asimmetrico, quindi non si appoggia a loadw *)
ndefinition mode_IMM2_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.Some ? (triple ??? s (mk_word16 bh bl) (filtered_plus_w16 m t s cur_pc 2)))).
+ 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)))).
(* 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.
(* 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.
(λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
(* 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.
(λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
(* 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.
(λaddr.loadbit_from m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1).
(* 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 ].
(λaddr.loadbit_from m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1).
(* 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 ].
(λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 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.
(λaddr.(aux_write m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1 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.
(λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1 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.
(λaddr.writebit_to m t s 〈〈x0,x0〉:addr〉 sub cur_pc 1 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))
+ 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)).
(* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
ndefinition mode_DIR2_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 ].
(λaddrl.(aux_load m t byteflag) s 〈addrh:addrl〉 cur_pc 2)).
(* scrittura su [word [curpc]]: true=DIR2 writeb, false=DIR2 writew *)
ndefinition mode_DIR2_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)
- (λaddrh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
+ 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)).
ndefinition get_IX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.
match m with
(λaddrl.(aux_write m t byteflag) s 〈addrh:addrl〉 cur_pc 2 writebw)).
ndefinition get_IX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.
match m with
- [ HC05 ⇒ opt_map ?? (get_indX_8_low_reg m t s) (λindx.Some ? 〈〈x0,x0〉:indx〉)
- | HC08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx)
- | HCS08 ⇒ opt_map ?? (get_indX_16_reg m t s) (λindx.Some ? indx)
+ [ HC05 ⇒ opt_map … (get_indX_8_low_reg m t s) (λindx.Some ? 〈〈x0,x0〉:indx〉)
+ | HC08 ⇒ opt_map … (get_indX_16_reg m t s) (λindx.Some ? indx)
+ | HCS08 ⇒ opt_map … (get_indX_16_reg m t s) (λindx.Some ? indx)
| RS08 ⇒ None ? ].
(* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
ndefinition mode_IX0_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
| RS08 ⇒ None ? ].
(* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
ndefinition mode_IX0_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
(λaddr.(aux_load m t byteflag) s addr cur_pc 0).
(* 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 ].
(λaddr.(aux_load m t byteflag) s addr cur_pc 0).
(* 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 ].
(λaddr.(aux_write m t byteflag) s addr cur_pc 0 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.
(λaddr.(aux_write m t byteflag) s addr cur_pc 0 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.
(λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
(* lettura da X+[byte curpc] *)
ndefinition mode_IX1ADD_load ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
(λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
(* lettura da X+[byte curpc] *)
ndefinition 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 ? (triple ??? s (plus_w16_d_d addr 〈〈x0,x0〉:b〉) (filtered_inc_w16 m t s cur_pc)))).
+ opt_map … (memory_filter_read m t s cur_pc)
+ (λb.opt_map … (get_IX m t s)
+ (λaddr.Some ? (triple … s (plus_w16_d_d addr 〈〈x0,x0〉:b〉) (filtered_inc_w16 m t s cur_pc)))).
(* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
ndefinition mode_IX1_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 ].
(* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
ndefinition mode_IX1_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 ].
(λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
(* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
ndefinition mode_IX2_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
(λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
(* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
ndefinition mode_IX2_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)
- (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
+ 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))).
(* lettura da X+[word curpc] *)
ndefinition mode_IX2ADD_load ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
(λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
(* lettura da X+[word curpc] *)
ndefinition 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 ? (triple ??? s (plus_w16_d_d addr 〈bh:bl〉) (filtered_plus_w16 m t s cur_pc 2))))).
+ 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))))).
(* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
ndefinition mode_IX2_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 ].
(* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
ndefinition mode_IX2_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.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))
+ 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))).
(* 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.
(λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 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.
(λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
(* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
ndefinition mode_SP1_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 ].
(λoffs.(aux_load m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
(* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
ndefinition mode_SP1_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 ].
(λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
(* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
ndefinition mode_SP2_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
(λoffs.(aux_write m t byteflag) s (plus_w16_d_d addr 〈〈x0,x0〉:offs〉) cur_pc 1 writebw)).
(* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
ndefinition mode_SP2_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)
- (λoffsh.opt_map ?? (memory_filter_read m t s (filtered_inc_w16 m t s cur_pc))
+ 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))).
(* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
ndefinition mode_SP2_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 ].
(λoffsl.(aux_load m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2))).
(* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
ndefinition mode_SP2_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_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))
+ 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 2 writebw))).
(* ************************************** *)
(λs_tmp.Some ? s_tmp)).
(* tutte le modalita' di lettura: false=loadb true=loadw *)
ndefinition multi_mode_load ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.
match byteflag
(λs_tmp.Some ? s_tmp)).
(* tutte le modalita' di lettura: false=loadb true=loadw *)
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
(* NO: non ci sono indicazioni *)
[ MODE_INH ⇒ None ?
(* restituisce A *)
with
(* lettura di un byte *)
[ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
(* NO: non ci sono indicazioni *)
[ MODE_INH ⇒ None ?
(* restituisce A *)
(* NO: solo lettura word *)
| MODE_DIRn_and_IMM1 _ ⇒ None ?
(* preleva 1 byte da 0000 0000 0000 xxxxb *)
(* NO: solo lettura word *)
| MODE_DIRn_and_IMM1 _ ⇒ None ?
(* preleva 1 byte da 0000 0000 0000 xxxxb *)
- | MODE_TNY e ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:〈x0,e〉〉)
- (λb.Some ? (triple ??? s b cur_pc))
+ | MODE_TNY e ⇒ opt_map … (memory_filter_read m t s 〈〈x0,x0〉:〈x0,e〉〉)
+ (λb.Some ? (triple … s b cur_pc))
- | MODE_SRT e ⇒ opt_map ?? (memory_filter_read m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉)
- (λb.Some ? (triple ??? s b cur_pc))
+ | MODE_SRT e ⇒ opt_map … (memory_filter_read m t s 〈〈x0,x0〉:(b8_of_bit e)〉)
+ (λb.Some ? (triple … s b cur_pc))
(* preleva 1 word immediato *)
| MODE_INHX1ADD ⇒ mode_IX1ADD_load m t s cur_pc
(* preleva 1 word immediato *)
(* preleva 1 word immediato *)
| MODE_INHX1ADD ⇒ mode_IX1ADD_load m t s cur_pc
(* preleva 1 word immediato *)
| MODE_DIR1_to_IX0p ⇒ None ?
(* preleva 2 byte, possibilita' modificare Io argomento *)
| MODE_DIR1_to_IX0p ⇒ None ?
(* preleva 2 byte, possibilita' modificare Io argomento *)
- | MODE_INHX_and_IMM1 ⇒ opt_map ?? (get_indX_8_low_reg m t s)
- (λX_op.opt_map ?? (mode_IMM1_load m t s cur_pc)
+ | MODE_INHX_and_IMM1 ⇒ opt_map … (get_indX_8_low_reg m t s)
+ (λX_op.opt_map … (mode_IMM1_load m t s cur_pc)
(* NO: solo scrittura byte *)
| MODE_DIRn _ ⇒ None ?
(* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
(* NO: solo scrittura byte *)
| MODE_DIRn _ ⇒ None ?
(* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
(* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
| MODE_IMM1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
(* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
(* passo2: scrittura su DIR1, passo1: lettura da IMM1 *)
| 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_INHX_and_IMM1 ⇒ opt_map ?? (set_indX_8_low_reg m t s writeb)
- (λtmps.Some ? (pair ?? tmps cur_pc))
+ | MODE_INHX_and_IMM1 ⇒ opt_map … (set_indX_8_low_reg m t s writeb)
+ (λ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 *)
(* NO: solo lettura word *)
| MODE_IMM1_and_IMM1 ⇒ None ?
(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *)
(* NO: solo lettura word *)
| MODE_DIRn_and_IMM1 _ ⇒ None ?
(* scrive 1 byte su 0000 0000 0000 xxxxb *)
(* NO: solo lettura word *)
| 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 ? (pair ?? tmps cur_pc))
+ | MODE_TNY e ⇒ opt_map … (memory_filter_write m t s 〈〈x0,x0〉:〈x0,e〉〉 writeb)
+ (λtmps.Some ? (pair … tmps cur_pc))
- | MODE_SRT e ⇒ opt_map ?? (memory_filter_write m t s 〈〈x0,x0〉:(byte8_of_bitrigesim e)〉 writeb)
- (λtmps.Some ? (pair ?? tmps cur_pc)) ]
+ | 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
(* NO: non ci sono indicazioni *)
(* 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 *)