(* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
definition mode_DIR1_load ≝
(* lettura da [byte [curpc]]: true=DIR1 loadb, false=DIR1 loadw *)
definition mode_DIR1_load ≝
opt_map ?? (memory_filter_read m t s cur_pc)
(λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
opt_map ?? (memory_filter_read m t s cur_pc)
(λaddr.(aux_load m t byteflag) s 〈〈x0,x0〉:addr〉 cur_pc 1).
(* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
definition mode_DIR1_write ≝
(* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
definition mode_DIR1_write ≝
λ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).
λ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).
(* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
definition mode_DIR2_load ≝
(* lettura da [word [curpc]]: true=DIR2 loadb, false=DIR2 loadw *)
definition mode_DIR2_load ≝
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 *)
definition mode_DIR2_write ≝
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 *)
definition 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))
λ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))
(* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
definition mode_IX0_load ≝
(* lettura da [IX]: true=IX0 loadb, false=IX0 loadw *)
definition mode_IX0_load ≝
opt_map ?? (get_IX m t s)
(λaddr.(aux_load m t byteflag) s addr cur_pc 0).
(* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
definition mode_IX0_write ≝
opt_map ?? (get_IX m t s)
(λaddr.(aux_load m t byteflag) s addr cur_pc 0).
(* scrittura su [IX]: true=IX0 writeb, false=IX0 writew *)
definition mode_IX0_write ≝
λ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).
(* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
definition mode_IX1_load ≝
λ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).
(* lettura da [IX+byte [pc]]: true=IX1 loadb, false=IX1 loadw *)
definition mode_IX1_load ≝
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_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
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_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
(* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
definition mode_IX1_write ≝
(* scrittura su [IX+byte [pc]]: true=IX1 writeb, false=IX1 writew *)
definition mode_IX1_write ≝
λ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)
λ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)
(* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
definition mode_IX2_load ≝
(* lettura da [IX+word [pc]]: true=IX2 loadb, false=IX2 loadw *)
definition 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))
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))
(* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
definition mode_IX2_write ≝
(* scrittura su [IX+word [pc]]: true=IX2 writeb, false=IX2 writew *)
definition mode_IX2_write ≝
λ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)
λ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)
(* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
definition mode_SP1_load ≝
(* lettura da [SP+byte [pc]]: true=SP1 loadb, false=SP1 loadw *)
definition mode_SP1_load ≝
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_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
(* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
definition mode_SP1_write ≝
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_w16nc addr 〈〈x0,x0〉:offs〉) cur_pc 1)).
(* scrittura su [SP+byte [pc]]: true=SP1 writeb, false=SP1 writew *)
definition 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)
λ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)
(* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
definition mode_SP2_load ≝
(* lettura da [SP+word [pc]]: true=SP2 loadb, false=SP2 loadw *)
definition 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))
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))
(* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
definition mode_SP2_write ≝
(* scrittura su [SP+word [pc]]: true=SP2 writeb, false=SP2 writew *)
definition mode_SP2_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)
λ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)
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)
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)
(* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
| MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load m t s cur_pc
(* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
(* come IMM1, chiamare scrittura per passo2: scrittura su DIR1 *)
| MODE_IMM1_to_DIR1 ⇒ mode_IMM1_load m t s cur_pc
(* come IX0, chiamare scrittura per passo2: scrittura su DIR1 e X++ *)
(* preleva 1 word immediato *)
| MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
(* preleva 1 word da indirizzo diretto 1 byte *)
(* preleva 1 word immediato *)
| MODE_IMM2 ⇒ mode_IMM2_load m t s cur_pc
(* preleva 1 word da indirizzo diretto 1 byte *)
[ tripleT _ immb2 cur_pc'' ⇒
Some ? (tripleT ??? s 〈immb1:immb2〉 cur_pc'')])])
(* preleva 2 byte, possibilita' modificare Io argomento *)
[ tripleT _ immb2 cur_pc'' ⇒
Some ? (tripleT ??? s 〈immb1:immb2〉 cur_pc'')])])
(* preleva 2 byte, possibilita' modificare Io argomento *)
(λS_dirb_and_PC.match S_dirb_and_PC with
[ tripleT _ dirb cur_pc' ⇒
opt_map ?? (mode_IMM1_load m t s cur_pc')
(λS_dirb_and_PC.match S_dirb_and_PC with
[ tripleT _ dirb cur_pc' ⇒
opt_map ?? (mode_IMM1_load m t s cur_pc')
[ tripleT _ immb cur_pc'' ⇒
Some ? (tripleT ??? s 〈dirb:immb〉 cur_pc'')])])
(* preleva 2 byte, possibilita' modificare Io argomento *)
[ tripleT _ immb cur_pc'' ⇒
Some ? (tripleT ??? s 〈dirb:immb〉 cur_pc'')])])
(* preleva 2 byte, possibilita' modificare Io argomento *)
(λS_ixb_and_PC.match S_ixb_and_PC with
[ tripleT _ ixb cur_pc' ⇒
opt_map ?? (mode_IMM1_load m t s cur_pc')
(λS_ixb_and_PC.match S_ixb_and_PC with
[ tripleT _ ixb cur_pc' ⇒
opt_map ?? (mode_IMM1_load m t s cur_pc')
[ tripleT _ immb cur_pc'' ⇒
Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
(* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
[ tripleT _ immb cur_pc'' ⇒
Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
(* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
(λS_ixb_and_PC.match S_ixb_and_PC with
[ tripleT _ ixb cur_pc' ⇒
opt_map ?? (mode_IMM1_load m t s cur_pc')
(λS_ixb_and_PC.match S_ixb_and_PC with
[ tripleT _ ixb cur_pc' ⇒
opt_map ?? (mode_IMM1_load m t s cur_pc')
opt_map ?? (aux_inc_indX_16 m t s)
(λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
(* preleva 2 byte, possibilita' modificare Io argomento *)
opt_map ?? (aux_inc_indX_16 m t s)
(λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
(* preleva 2 byte, possibilita' modificare Io argomento *)
(λS_ixb_and_PC.match S_ixb_and_PC with
[ tripleT _ ixb cur_pc' ⇒
opt_map ?? (mode_IMM1_load m t s cur_pc')
(λS_ixb_and_PC.match S_ixb_and_PC with
[ tripleT _ ixb cur_pc' ⇒
opt_map ?? (mode_IMM1_load m t s cur_pc')
[ tripleT _ immb cur_pc'' ⇒
Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
(* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
[ tripleT _ immb cur_pc'' ⇒
Some ? (tripleT ??? s 〈ixb:immb〉 cur_pc'')])])
(* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
(λS_ixb_and_PC.match S_ixb_and_PC with
[ tripleT _ ixb cur_pc' ⇒
opt_map ?? (mode_IMM1_load m t s cur_pc')
(λS_ixb_and_PC.match S_ixb_and_PC with
[ tripleT _ ixb cur_pc' ⇒
opt_map ?? (mode_IMM1_load m t s cur_pc')
opt_map ?? (aux_inc_indX_16 m t s)
(λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
(* preleva 2 byte, possibilita' modificare Io argomento *)
opt_map ?? (aux_inc_indX_16 m t s)
(λs'.Some ? (tripleT ??? s' 〈ixb:immb〉 cur_pc''))])])
(* preleva 2 byte, possibilita' modificare Io argomento *)
(λS_spb_and_PC.match S_spb_and_PC with
[ tripleT _ spb cur_pc' ⇒
opt_map ?? (mode_IMM1_load m t s cur_pc')
(λS_spb_and_PC.match S_spb_and_PC with
[ tripleT _ spb cur_pc' ⇒
opt_map ?? (mode_IMM1_load m t s cur_pc')
(* tutte le modalita' di scrittura: true=writeb, false=writew *)
definition multi_mode_write ≝
(* tutte le modalita' di scrittura: true=writeb, false=writew *)
definition multi_mode_write ≝
return λbyteflag:bool.any_status m t → word16 → instr_mode →
match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
option (Prod (any_status m t) word16) with
return λbyteflag:bool.any_status m t → word16 → instr_mode →
match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
option (Prod (any_status m t) word16) with
(λ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 ? (pair ?? S_op' PC_op))])
(* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
(λ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 ? (pair ?? S_op' PC_op))])
(* passo2: scrittura su IX0 e X++, passo1: lettura da 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_IMM1_and_IMM1 ⇒ None ?
(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *)
(* NO: solo lettura word *)
| MODE_IX0p_and_IMM1 ⇒ None ?
(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
(* NO: solo lettura word *)
| MODE_IX0p_and_IMM1 ⇒ None ?
(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
(* NO: solo lettura word *)
| MODE_IX1p_and_IMM1 ⇒ None ?
(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
(* NO: solo lettura word *)
| MODE_IX1p_and_IMM1 ⇒ None ?
(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
(* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
| MODE_DIRn msk ⇒ mode_DIR1n_write m t s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))
(* scrive 1 byte, ma la scrittura avviene solo per n-simo bit = leggi/modifica bit/scrivi *)
| MODE_DIRn msk ⇒ mode_DIR1n_write m t s cur_pc msk (getn_array8T msk bool (bits_of_byte8 writeb))