num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma
emulator/status/IP2022_status_lemmas.ma emulator/memory/memory_struct_lemmas.ma emulator/status/IP2022_status.ma num/oct_lemmas.ma num/word16_lemmas.ma num/word24_lemmas.ma
num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma
-emulator/status/status_lemmas.ma emulator/status/HC05_status_lemmas.ma emulator/status/HC08_status_lemmas.ma emulator/status/IP2022_status_lemmas.ma emulator/status/RS08_status_lemmas.ma
+emulator/status/status_lemmas.ma common/option_lemmas.ma common/prod_lemmas.ma emulator/opcodes/opcode_lemmas.ma emulator/status/HC05_status_lemmas.ma emulator/status/HC08_status_lemmas.ma emulator/status/IP2022_status_lemmas.ma emulator/status/RS08_status_lemmas.ma emulator/status/status.ma
emulator/status/status.ma emulator/memory/memory_abs.ma emulator/opcodes/opcode.ma emulator/status/HC05_status.ma emulator/status/HC08_status.ma emulator/status/IP2022_status.ma emulator/status/RS08_status.ma
num/byte8.ma common/nat.ma num/bitrigesim.ma num/comp_num.ma num/exadecim.ma
emulator/model/model.ma emulator/model/HC05_model.ma emulator/model/HC08_model.ma emulator/model/HCS08_model.ma emulator/model/IP2022_model.ma emulator/model/RS08_model.ma
test_errori.ma
compiler/environment.ma common/string.ma compiler/ast_type.ma
common/ascii_lemmas.ma common/ascii.ma num/bool_lemmas.ma
+emulator/read_write/IP2022_read_write.ma emulator/read_write/read_write_base.ma emulator/status/status_setter.ma
emulator/translation/translation_base.ma common/option.ma emulator/opcodes/HC05_table.ma emulator/opcodes/HC08_table.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/RS08_table.ma emulator/opcodes/opcode.ma
emulator/opcodes/IP2022_table.ma common/list.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_opcode.ma emulator/opcodes/byte_or_word.ma
emulator/status/HC05_status.ma num/word16.ma
emulator/memory/memory_bits.ma emulator/memory/memory_trees.ma
common/theory.ma
common/string.ma common/ascii.ma common/list_utility.ma
+emulator/read_write/RS08_read_write.ma emulator/status/status_setter.ma
emulator/opcodes/byte_or_word.ma num/word16.ma
compiler/ast_type.ma common/list_utility.ma
num/word16.ma num/byte8.ma
emulator/opcodes/IP2022_table_tests.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/opcode.ma
emulator/status/IP2022_status.ma emulator/memory/memory_struct.ma num/word16.ma num/word24.ma
num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma
+emulator/read_write/read_write.ma emulator/read_write/IP2022_read_write.ma emulator/read_write/RS08_read_write.ma
emulator/memory/memory_func.ma common/list.ma common/option.ma emulator/memory/memory_struct.ma num/word32.ma
emulator/opcodes/RS08_instr_mode.ma num/word16.ma
num/comp_num_lemmas.ma num/bool_lemmas.ma num/comp_num.ma
+emulator/read_write/read_write_base.ma common/theory.ma
emulator/status/RS08_status.ma num/word16.ma
emulator/opcodes/HC05_opcode_lemmas.ma emulator/opcodes/HC05_opcode.ma num/bool_lemmas.ma
emulator/opcodes/HC08_instr_mode.ma num/word16.ma
(* etc.. *)
].
-(*
- parametrizzati i non deterministici rispetto a tutti i valori casuali
+(* parametrizzati i non deterministici rispetto a tutti i valori casuali
che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
- (reset V-low), la memoria ed il check possono essere passati
-*)
+ (reset V-low), la memoria ed il check possono essere passati *)
ndefinition start_of_model_HC05 ≝
λmcu:HC05_model.λt:memory_impl.
λmem:aux_mem_type t.λchk:aux_chk_type t.
(*..*)
].
-(*
- cio' che non viene resettato mantiene il valore precedente: nella documentazione
+(* cio' che non viene resettato mantiene il valore precedente: nella documentazione
viene riportato come "unaffected"/"indeterminate"/"unpredictable"
- il soft RESET e' diverso da un calo di tensione e la ram non variera'
-*)
+ il soft RESET e' diverso da un calo di tensione e la ram non variera' *)
ndefinition reset_of_model_HC05 ≝
λt:memory_impl.λs:any_status HC05 t.
(mk_any_status HC05 t
(* etc... *)
].
-(*
- parametrizzati i non deterministici rispetto a tutti i valori casuali
+(* parametrizzati i non deterministici rispetto a tutti i valori casuali
che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
- (reset V-low), la memoria ed il check possono essere passati
-*)
+ (reset V-low), la memoria ed il check possono essere passati *)
ndefinition start_of_model_HC08 ≝
λmcu:HC08_model.λt:memory_impl.
λmem:aux_mem_type t.λchk:aux_chk_type t.
(* chk *) chk
(* clk: reset *) (None ?).
-(*
- cio' che non viene resettato mantiene il valore precedente: nella documentazione
+(* cio' che non viene resettato mantiene il valore precedente: nella documentazione
viene riportato come "unaffected"/"indeterminate"/"unpredictable"
- il soft RESET e' diverso da un calo di tensione e la ram non variera'
-*)
+ il soft RESET e' diverso da un calo di tensione e la ram non variera' *)
ndefinition reset_of_model_HC08 ≝
λt:memory_impl.λs:any_status HC08 t.
(mk_any_status HC08 t
(* etc... *)
].
-(*
- parametrizzati i non deterministici rispetto a tutti i valori casuali
+(* parametrizzati i non deterministici rispetto a tutti i valori casuali
che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
- (reset V-low), la memoria ed il check possono essere passati
-*)
+ (reset V-low), la memoria ed il check possono essere passati *)
ndefinition start_of_model_HCS08 ≝
λmcu:HCS08_model.λt:memory_impl.
λmem:aux_mem_type t.λchk:aux_chk_type t.
(* chk *) chk
(* clk: reset *) (None ?).
-(*
- cio' che non viene resettato mantiene il valore precedente: nella documentazione
+(* cio' che non viene resettato mantiene il valore precedente: nella documentazione
viene riportato come "unaffected"/"indeterminate"/"unpredictable"
- il soft RESET e' diverso da un calo di tensione e la ram non variera'
-*)
+ il soft RESET e' diverso da un calo di tensione e la ram non variera' *)
ndefinition reset_of_model_HCS08 ≝
λt:memory_impl.λs:any_status HCS08 t.
(mk_any_status HCS08 t
λm:IP2022_model.match m with
[ IP2K ⇒
[
-(* 0x00000080-0x00000FFF *) triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x8,x0〉〉〉 〈〈x0,xF〉:〈x8,x0〉〉 MEM_READ_WRITE (* 3968 GPR+RAM+STACK *)
+(* 0x00000008-0x00000008 *) triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x8〉〉〉 〈〈x0,x0〉:〈x0,x1〉〉 MEM_READ_ONLY (* PCH read only memory reg *)
+(* 0x0000000E-0x0000000E *) ; triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xE〉〉〉 〈〈x0,x0〉:〈x0,x1〉〉 MEM_READ_ONLY (* PCH read only memory reg *)
+(* 0x00000080-0x00000FFF *) ; triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x8,x0〉〉〉 〈〈x0,xF〉:〈x8,x0〉〉 MEM_READ_WRITE (* 3968 GPR+RAM+STACK *)
(* 0x02000000-0x02003FFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_WRITE (* 16384B PROGRAM RAM *)
(* 0x02010000-0x02013FFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x1〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *)
(* 0x02014000-0x02017FFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x1〉〉.〈〈x4,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *)
(* punto di riferimento per accessi ($PC) ($ADDR) *)
ndefinition IP2022_ram_base ≝ 〈〈〈x0,x2〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉.
-(*
- parametrizzati i non deterministici rispetto a tutti i valori casuali
+(* parametrizzati i non deterministici rispetto a tutti i valori casuali
che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
- (reset V-low), la memoria ed il check possono essere passati
-*)
+ (reset V-low), la memoria ed il check possono essere passati *)
ndefinition start_of_model_IP2022 ≝
λmcu:IP2022_model.λt:memory_impl.
λmem:aux_mem_type t.λchk:aux_chk_type t.
(* chk *) chk
(* clk: reset *) (None ?)).
-(*
- cio' che non viene resettato mantiene il valore precedente: nella documentazione
+(* cio' che non viene resettato mantiene il valore precedente: nella documentazione
viene riportato come "unaffected"/"indeterminate"/"unpredictable"
- il soft RESET e' diverso da un calo di tensione e la ram non variera'
-*)
+ il soft RESET e' diverso da un calo di tensione e la ram non variera' *)
ndefinition reset_of_model_IP2022 ≝
λt:memory_impl.λs:any_status IP2022 t.
(mk_any_status IP2022 t
(* 0x3800-0x3FFF *) ; triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x3,x8〉:〈x0,x0〉〉〉 〈〈x0,x8〉:〈x0,x0〉〉 MEM_READ_ONLY (* 2048B FLASH *) ]
].
-(*
- parametrizzati i non deterministici rispetto a tutti i valori casuali
+(* parametrizzati i non deterministici rispetto a tutti i valori casuali
che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
- (reset V-low), la memoria ed il check possono essere passati
-*)
+ (reset V-low), la memoria ed il check possono essere passati *)
ndefinition start_of_model_RS08 ≝
λmcu:RS08_model.λt:memory_impl.
λmem:aux_mem_type t.λchk:aux_chk_type t.
(* chk *) chk
(* clk: reset *) (None ?)).
-(*
- cio' che non viene resettato mantiene il valore precedente: nella documentazione
+(* cio' che non viene resettato mantiene il valore precedente: nella documentazione
viene riportato come "unaffected"/"indeterminate"/"unpredictable"
- il soft RESET e' diverso da un calo di tensione e la ram non variera'
-*)
+ il soft RESET e' diverso da un calo di tensione e la ram non variera' *)
ndefinition reset_of_model_RS08 ≝
λt:memory_impl.λs:any_status RS08 t.
(mk_any_status RS08 t
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/status/status_setter.ma".
+include "emulator/read_write/read_write_base.ma".
+
+ndefinition IP2022_ADDRSEL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x2〉〉〉.
+ndefinition IP2022_ADDRX_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x3〉〉〉.
+ndefinition IP2022_IPH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x4〉〉〉.
+ndefinition IP2022_IPL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x5〉〉〉.
+ndefinition IP2022_SPH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x6〉〉〉.
+ndefinition IP2022_SPL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x7〉〉〉.
+ndefinition IP2022_PCH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x8〉〉〉.
+ndefinition IP2022_PCL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x9〉〉〉.
+ndefinition IP2022_W_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xA〉〉〉.
+ndefinition IP2022_STATUS_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xB〉〉〉.
+ndefinition IP2022_DPH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xC〉〉〉.
+ndefinition IP2022_DPL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xD〉〉〉.
+ndefinition IP2022_SPEED_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xE〉〉〉.
+ndefinition IP2022_MULH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xF〉〉〉.
+ndefinition IP2022_ADDRH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x0〉〉〉.
+ndefinition IP2022_ADDRL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x1〉〉〉.
+ndefinition IP2022_DATAH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x2〉〉〉.
+ndefinition IP2022_DATAL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x3〉〉〉.
+ndefinition IP2022_CALLH_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x4〉〉〉.
+ndefinition IP2022_CALLL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x5〉〉〉.
+
+(* **** *)
+(* READ *)
+(* **** *)
+
+(* NB: non ci sono strane indirezioni,
+ solo registri memory mapped da intercettare *)
+ndefinition IP2022_memory_filter_read_aux ≝
+λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.
+λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option T.
+(* intercettare le locazioni memory mapped *)
+ match eq_w32 addr IP2022_ADDRSEL_loc with
+ [ true ⇒ fREG (addrsel_reg_IP2022 (alu … s))
+ | false ⇒
+ match eq_w32 addr IP2022_ADDRX_loc with
+ [ true ⇒ fREG (w24x (get_addrarray (addrsel_reg_IP2022 (alu … s))
+ (addr_array_IP2022 (alu … s))))
+ | false ⇒
+ match eq_w32 addr IP2022_IPH_loc with
+ [ true ⇒ fREG (cnH ? (ip_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_IPL_loc with
+ [ true ⇒ fREG (cnL ? (ip_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_SPH_loc with
+ [ true ⇒ fREG (cnH ? (sp_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_SPL_loc with
+ [ true ⇒ fREG (cnL ? (sp_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_PCH_loc with
+ [ true ⇒ fREG (cnH ? (pc_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_PCL_loc with
+ [ true ⇒ fREG (cnL ? (pc_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_W_loc with
+ [ true ⇒ fREG (acc_low_reg_IP2022 (alu … s))
+ | false ⇒
+ (* PAGE[7:5] Z[2] H[1] C [0] *)
+ match eq_w32 addr IP2022_STATUS_loc with
+ [ true ⇒ fREG 〈(rol_ex (ex_of_oct (page_reg_IP2022 (alu … s)))),
+ (or_ex (or_ex (match z_flag_IP2022 (alu … s) with
+ [ true ⇒ x4 | false ⇒ x0 ])
+ (match h_flag_IP2022 (alu … s) with
+ [ true ⇒ x2 | false ⇒ x0 ]))
+ (match c_flag_IP2022 (alu … s) with
+ [ true ⇒ x1 | false ⇒ x0 ]))〉
+ | false ⇒
+ match eq_w32 addr IP2022_DPH_loc with
+ [ true ⇒ fREG (cnH ? (dp_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_DPL_loc with
+ [ true ⇒ fREG (cnL ? (dp_reg_IP2022 (alu … s)))
+ | false ⇒
+ (* SPEED[3:0] *)
+ match eq_w32 addr IP2022_SPEED_loc with
+ [ true ⇒ fREG 〈x0,(speed_reg_IP2022 (alu … s))〉
+ | false ⇒
+ match eq_w32 addr IP2022_MULH_loc with
+ [ true ⇒ fREG (mulh_reg_IP2022 (alu … s))
+ | false ⇒
+ match eq_w32 addr IP2022_ADDRH_loc with
+ [ true ⇒ fREG (w24h (get_addrarray (addrsel_reg_IP2022 (alu … s))
+ (addr_array_IP2022 (alu … s))))
+ | false ⇒
+ match eq_w32 addr IP2022_ADDRL_loc with
+ [ true ⇒ fREG (w24l (get_addrarray (addrsel_reg_IP2022 (alu … s))
+ (addr_array_IP2022 (alu … s))))
+ | false ⇒
+ match eq_w32 addr IP2022_DATAH_loc with
+ [ true ⇒ fREG (cnH ? (data_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_DATAL_loc with
+ [ true ⇒ fREG (cnL ? (data_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_CALLH_loc with
+ [ true ⇒ fREG (cnH ? (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
+ | false ⇒
+ match eq_w32 addr IP2022_CALLL_loc with
+ [ true ⇒ fREG (cnL ? (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
+(* accesso normale *)
+ | false ⇒ fMEM (mem_desc … s) (chk_desc … s) addr
+ ]]]]]]]]]]]]]]]]]]]].
+
+(* lettura IP2022 di un byte *)
+ndefinition IP2022_memory_filter_read ≝
+λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.
+ IP2022_memory_filter_read_aux t s addr byte8
+ (λb.Some byte8 b)
+ (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read t m c a).
+
+(* lettura IP2022 di un bit *)
+ndefinition IP2022_memory_filter_read_bit ≝
+λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.λsub:oct.
+ IP2022_memory_filter_read_aux t s addr bool
+ (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
+ (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read_bit t m c a sub).
+
+(* ***** *)
+(* WRITE *)
+(* ***** *)
+
+ndefinition high_write_aux_w16 ≝
+λf:byte8 → byte8.λw:word16.〈(f (cnH ? w)):(cnL ? w)〉.
+
+ndefinition low_write_aux_w16 ≝
+λf:byte8 → byte8.λw:word16.λflag:aux_mod_type.
+ 〈((match flag with
+ [ auxMode_ok ⇒ λx.x
+ | auxMode_inc ⇒ succ_b8
+ | auxMode_dec ⇒ pred_b8 ]) (cnH ? w)):
+ (f (cnL ? w))〉.
+
+ndefinition ext_write_aux_w24 ≝
+λf:byte8 → byte8.λw:word24.〈(f (w24x w));(w24h w);(w24l w)〉.
+
+ndefinition high_write_aux_w24 ≝
+λf:byte8 → byte8.λw:word24.〈(w24x w);(f (w24h w));(w24l w)〉.
+
+ndefinition low_write_aux_w24 ≝
+λf:byte8 → byte8.λw:word24.λflag:aux_mod_type.
+ match (match flag with
+ [ auxMode_ok ⇒ λx.x
+ | auxMode_inc ⇒ succ_w16
+ | auxMode_dec ⇒ pred_w16 ]) 〈(w24x w):(w24h w)〉 with
+ [ mk_comp_num wx' wh' ⇒ 〈wx';wh';(w24l w)〉 ].
+
+(* flag di carry: riportare il carry al byte logicamente superiore *)
+ndefinition IP2022_memory_filter_write_aux ≝
+λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.λflag:aux_mod_type.
+λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option (aux_mem_type t).
+(* intercettare le locazioni memory mapped *)
+ match eq_w32 addr IP2022_ADDRSEL_loc with
+ [ true ⇒ set_addrsel_reg … s (fREG (addrsel_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_ADDRX_loc with
+ [ true ⇒ set_addr_reg … s (ext_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
+ (addr_array_IP2022 (alu … s))))
+ | false ⇒
+ match eq_w32 addr IP2022_IPH_loc with
+ [ true ⇒ set_ip_reg … s (high_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_IPL_loc with
+ [ true ⇒ set_ip_reg … s (low_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)) flag)
+ | false ⇒
+ match eq_w32 addr IP2022_SPH_loc with
+ [ true ⇒ set_sp_reg … s (high_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_SPL_loc with
+ [ true ⇒ set_sp_reg … s (low_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)) flag)
+ | false ⇒
+ match eq_w32 addr IP2022_PCL_loc with
+ [ true ⇒ Some ? (set_pc_reg … s (low_write_aux_w16 fREG (pc_reg_IP2022 (alu … s)) flag))
+ | false ⇒
+ match eq_w32 addr IP2022_W_loc with
+ [ true ⇒ Some ? (set_acc_8_low_reg … s (fREG (acc_low_reg_IP2022 (alu … s))))
+ | false ⇒
+ match eq_w32 addr IP2022_DPH_loc with
+ [ true ⇒ set_dp_reg … s (high_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_DPL_loc with
+ [ true ⇒ set_dp_reg … s (low_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)) flag)
+ | false ⇒
+ match eq_w32 addr IP2022_MULH_loc with
+ [ true ⇒ set_mulh_reg … s (fREG (mulh_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_ADDRH_loc with
+ [ true ⇒ set_addr_reg … s (high_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
+ (addr_array_IP2022 (alu … s))))
+ | false ⇒
+ match eq_w32 addr IP2022_ADDRL_loc with
+ [ true ⇒ set_addr_reg … s (low_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
+ (addr_array_IP2022 (alu … s))) flag)
+ | false ⇒
+ match eq_w32 addr IP2022_DATAH_loc with
+ [ true ⇒ set_data_reg … s (high_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
+ | false ⇒
+ match eq_w32 addr IP2022_DATAL_loc with
+ [ true ⇒ set_data_reg … s (low_write_aux_w16 fREG (data_reg_IP2022 (alu … s)) flag)
+ | false ⇒
+ match eq_w32 addr IP2022_CALLH_loc with
+ [ true ⇒ set_call_reg … s (high_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
+ | false ⇒
+ match eq_w32 addr IP2022_CALLL_loc with
+ [ true ⇒ set_call_reg … s (low_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))) flag)
+(* accesso normale *)
+ | false ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr)
+ (λmem'.Some ? (set_mem_desc … s mem')) ]]]]]]]]]]]]]]]]].
+
+(* scrittura IP2022 di un byte *)
+ndefinition IP2022_memory_filter_write ≝
+λt:memory_impl.λs:any_status IP2022 t.
+λaddr:word32.λflag:aux_mod_type.λval:byte8.
+ (* PAGE[7:5] Z[2] H[1] C [0] *)
+ match eq_w32 addr IP2022_STATUS_loc with
+ [ true ⇒ Some ? (set_alu … s
+ (set_page_reg_IP2022
+ (set_z_flag_IP2022
+ (set_h_flag_IP2022
+ (set_c_flag_IP2022 (alu … s)
+ (getn_array8T o7 ? (bits_of_byte8 val)))
+ (getn_array8T o6 ? (bits_of_byte8 val)))
+ (getn_array8T o5 ? (bits_of_byte8 val)))
+ (oct_of_exH (cnH ? val))))
+ (* accesso a registro_non_spezzato/normale *)
+ | false ⇒ IP2022_memory_filter_write_aux t s addr flag
+ (λb.val)
+ (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update t m c a val) ].
+
+(* scrittura IP2022 di un bit *)
+ndefinition IP2022_memory_filter_write_bit ≝
+λt:memory_impl.λs:any_status IP2022 t.
+λaddr:word32.λsub:oct.λval:bool.
+ (* PAGE[7:5] Z[2] H[1] C [0] *)
+ match eq_w32 addr IP2022_STATUS_loc with
+ [ true ⇒ Some ? (set_alu … s
+ (match sub with
+ [ o0 ⇒ set_page_reg_IP2022 (alu … s)
+ ((match val with [ true ⇒ or_oct o4 | false ⇒ and_oct o3 ])
+ (page_reg_IP2022 (alu … s)))
+ | o1 ⇒ set_page_reg_IP2022 (alu … s)
+ ((match val with [ true ⇒ or_oct o2 | false ⇒ and_oct o5 ])
+ (page_reg_IP2022 (alu … s)))
+ | o2 ⇒ set_page_reg_IP2022 (alu … s)
+ ((match val with [ true ⇒ or_oct o1 | false ⇒ and_oct o6 ])
+ (page_reg_IP2022 (alu … s)))
+ | o5 ⇒ set_z_flag_IP2022 (alu … s) val
+ | o6 ⇒ set_h_flag_IP2022 (alu … s) val
+ | o7 ⇒ set_c_flag_IP2022 (alu … s) val
+ | _ ⇒ alu … s ]))
+ (* accesso a registro_non_spezzato/normale *)
+ | false ⇒ IP2022_memory_filter_write_aux t s addr auxMode_ok
+ (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
+ (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update_bit t m c a sub val) ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/status/status_setter.ma".
+
+(* **** *)
+(* READ *)
+(* **** *)
+
+(* NB: fare molta attenzione alle note sulle combinazioni possibili perche'
+ il comportamento della memoria nell'RS08 e' strano e ci sono
+ precise condizioni che impediscono una semantica circolare dell'accesso
+ (divergenza=assenza di definizione) *)
+ndefinition RS08_memory_filter_read_aux ≝
+λt:memory_impl.λs:any_status RS08 t.λaddr:word32.
+λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option T.
+(* solo indirizzi nei 64Kb *)
+ match gt_w16 (cnH ? addr) 〈〈x0,x0〉:〈x0,x0〉〉 with
+ [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) addr
+ | false ⇒
+(* possibili accessi al registro X
+ 1) addr=000F: diretto
+ 2) addr=000E (X =0F): indiretto
+ 3) addr=00CF (PS=00): paging
+ [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
+ non si possono combinare due effetti contemporaneamente!
+ per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni *)
+ match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
+ (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 (x_map_RS08 (alu … s)) 〈x0,xF〉) ⊕
+ (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 (ps_map_RS08 (alu … s)) 〈x0,x0〉) with
+ [ true ⇒ fREG (x_map_RS08 (alu … s))
+ | false ⇒
+(* possibili accessi al registro PS
+ 1) addr=001F: diretto
+ 2) addr=000E (X =1F): indiretto
+ 3) addr=00DF (PS=00): paging *)
+ match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
+ (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 (x_map_RS08 (alu … s)) 〈x1,xF〉) ⊕
+ (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 (ps_map_RS08 (alu … s)) 〈x0,x0〉) with
+ [ true ⇒ fREG (ps_map_RS08 (alu … s))
+ | false ⇒
+(* accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
+ altrimenti sarebbero 2 indirezioni *)
+ match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 with
+ [ true ⇒ fMEM (mem_desc … s) (chk_desc … s) 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:(x_map_RS08 (alu … s))〉〉
+ | false ⇒
+(* accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr *)
+ match inrange_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
+ [ true ⇒ fMEM (mem_desc … s) (chk_desc … s)
+ (〈〈〈x0,x0〉:〈x0,x0〉〉.(or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
+ (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉))〉)
+(* accesso normale *)
+ | false ⇒ fMEM (mem_desc … s) (chk_desc … s) addr ]]]]].
+
+(* lettura RS08 di un byte *)
+ndefinition RS08_memory_filter_read ≝
+λt:memory_impl.λs:any_status RS08 t.λaddr:word32.
+ RS08_memory_filter_read_aux t s addr byte8
+ (λb.Some byte8 b)
+ (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read t m c a).
+
+(* lettura RS08 di un bit *)
+ndefinition RS08_memory_filter_read_bit ≝
+λt:memory_impl.λs:any_status RS08 t.λaddr:word32.λsub:oct.
+ RS08_memory_filter_read_aux t s addr bool
+ (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
+ (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read_bit t m c a sub).
+
+(* ***** *)
+(* WRITE *)
+(* ***** *)
+
+ndefinition RS08_memory_filter_write_aux ≝
+λt:memory_impl.λs:any_status RS08 t.λaddr:word32.
+λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option (aux_mem_type t).
+(* solo indirizzi nei 64Kb *)
+ match gt_w16 (cnH ? addr) 〈〈x0,x0〉:〈x0,x0〉〉 with
+ [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr)
+ (λmem'.Some ? (set_mem_desc … s mem'))
+ | false ⇒
+(* possibili accessi al registro X
+ 1) addr=000F: diretto
+ 2) addr=000E (X =0F): indiretto
+ 3) addr=00CF (PS=00): paging
+ [NB] altre combinazioni non funzionano perche' la MCU non e' un oggetto reattivo:
+ non si possono combinare due effetti contemporaneamente!
+ per esempio accesso addr=00CE (PS=00,X=0F) non puo' produrre 2 indirezioni *)
+ match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
+ (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 (x_map_RS08 (alu … s)) 〈x0,xF〉) ⊕
+ (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 (ps_map_RS08 (alu … s)) 〈x0,x0〉) with
+ [ true ⇒ set_x_map … s (fREG (x_map_RS08 (alu … s)))
+ | false ⇒
+(* possibili accessi al registro PS
+ 1) addr=001F: diretto
+ 2) addr=000E (X =1F): indiretto
+ 3) addr=00DF (PS=00): paging *)
+ match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
+ (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 (x_map_RS08 (alu … s)) 〈x1,xF〉) ⊕
+ (eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 (ps_map_RS08 (alu … s)) 〈x0,x0〉) with
+ [ true ⇒ set_ps_map … s (fREG (x_map_RS08 (alu … s)))
+ | false ⇒
+(* accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
+ altrimenti sarebbero 2 indirezioni *)
+ match eq_w16 (cnL ? addr) 〈〈x0,x0〉:〈x0,xE〉〉 with
+ [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:(x_map_RS08 (alu … s))〉〉)
+ (λmem'.Some ? (set_mem_desc … s mem'))
+ | false ⇒
+(* accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr *)
+ match inrange_w16 (cnL ? addr) 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 with
+ [ true ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s)
+ (〈〈〈x0,x0〉:〈x0,x0〉〉.(or_w16 (ror_w16 (ror_w16 〈(ps_map_RS08 (alu … s)):〈x0,x0〉〉))
+ (and_w16 (cnL ? addr) 〈〈x0,x0〉:〈x3,xF〉〉))〉))
+ (λmem'.Some ? (set_mem_desc … s mem'))
+(* accesso normale *)
+ | false ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr)
+ (λmem'.Some ? (set_mem_desc … s mem')) ]]]]].
+
+(* scrittura RS08 di un byte *)
+ndefinition RS08_memory_filter_write ≝
+λt:memory_impl.λs:any_status RS08 t.λaddr:word32.λval:byte8.
+ RS08_memory_filter_write_aux t s addr
+ (λb.val)
+ (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update t m c a val).
+
+(* scrittura RS08 di un bit *)
+ndefinition RS08_memory_filter_write_bit ≝
+λt:memory_impl.λs:any_status RS08 t.λaddr:word32.λsub:oct.λval:bool.
+ RS08_memory_filter_write_aux t s addr
+ (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
+ (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update_bit t m c a sub val).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/read_write/RS08_read_write.ma".
+include "emulator/read_write/IP2022_read_write.ma".
+
+(* in caso di RS08/IP2022 si dirotta sul filtro, altrimenti si legge direttamente *)
+ndefinition memory_filter_read ≝
+λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word32 → option byte8 with
+ [ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.
+ mem_read t (mem_desc ? t s) (chk_desc ? t s) addr
+ | HC08 ⇒ λs:any_status HC08 t.λaddr:word32.
+ mem_read t (mem_desc ? t s) (chk_desc ? t s) addr
+ | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.
+ mem_read t (mem_desc ? t s) (chk_desc ? t s) addr
+ | RS08 ⇒ λs:any_status RS08 t.λaddr:word32.
+ RS08_memory_filter_read t s addr
+ | IP2022 ⇒ λs:any_status IP2022 t.λaddr:word32.
+ IP2022_memory_filter_read t s addr
+ ].
+
+ndefinition memory_filter_read_bit ≝
+λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word32 → oct → option bool with
+ [ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.λsub:oct.
+ mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub
+ | HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λsub:oct.
+ mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub
+ | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λsub:oct.
+ mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub
+ | RS08 ⇒ λs:any_status RS08 t.λaddr:word32.λsub:oct.
+ RS08_memory_filter_read_bit t s addr sub
+ | IP2022 ⇒ λs:any_status IP2022 t.λaddr:word32.λsub:oct.
+ IP2022_memory_filter_read_bit t s addr sub
+ ].
+
+ndefinition memory_filter_write ≝
+λm:mcu_type.λt:memory_impl.match m
+ return λm:mcu_type.any_status m t → word32 → aux_mod_type → byte8 → option (any_status m t) with
+ [ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
+ opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
+ (λmem.Some ? (set_mem_desc ? t s mem))
+ | HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
+ opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
+ (λmem.Some ? (set_mem_desc ? t s mem))
+ | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
+ opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
+ (λmem.Some ? (set_mem_desc ? t s mem))
+ | RS08 ⇒ λs:any_status RS08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
+ RS08_memory_filter_write t s addr val
+ | IP2022 ⇒ λs:any_status IP2022 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
+ IP2022_memory_filter_write t s addr flag val
+ ].
+
+ndefinition memory_filter_write_bit ≝
+λm:mcu_type.λt:memory_impl.match m
+ return λm:mcu_type.any_status m t → word32 → oct → bool → option (any_status m t) with
+ [ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.λsub:oct.λval:bool.
+ opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
+ (λmem.Some ? (set_mem_desc ? t s mem))
+ | HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λsub:oct.λval:bool.
+ opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
+ (λmem.Some ? (set_mem_desc ? t s mem))
+ | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λsub:oct.λval:bool.
+ opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
+ (λmem.Some ? (set_mem_desc ? t s mem))
+ | RS08 ⇒ λs:any_status RS08 t.λaddr:word32.λsub:oct.λval:bool.
+ RS08_memory_filter_write_bit t s addr sub val
+ | IP2022 ⇒ λs:any_status IP2022 t.λaddr:word32.λsub:oct.λval:bool.
+ IP2022_memory_filter_write_bit t s addr sub val
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "common/theory.ma".
+
+(* flag ausiliario per la scrittura
+ normale / con riporto(+) / con riporto(-) *)
+ninductive aux_mod_type : Type ≝
+ auxMode_ok : aux_mod_type
+| auxMode_inc : aux_mod_type
+| auxMode_dec : aux_mod_type
+.
+
ndefinition pop_callstack ≝
λcs:aux_callstack_type.
- pair ?? (a16_1 ? cs)
- (mk_Array16T ? (a16_2 ? cs) (a16_3 ? cs) (a16_4 ? cs) (a16_5 ? cs)
- (a16_6 ? cs) (a16_7 ? cs) (a16_8 ? cs) (a16_9 ? cs)
- (a16_10 ? cs) (a16_11 ? cs) (a16_12 ? cs) (a16_13 ? cs)
- (a16_14 ? cs) (a16_15 ? cs) (a16_16 ? cs) 〈〈xF,xF〉:〈xF,xF〉〉).
+ pair … (a16_1 ? cs)
+ (mk_Array16T ? (a16_2 ? cs) (a16_3 ? cs) (a16_4 ? cs) (a16_5 ? cs)
+ (a16_6 ? cs) (a16_7 ? cs) (a16_8 ? cs) (a16_9 ? cs)
+ (a16_10 ? cs) (a16_11 ? cs) (a16_12 ? cs) (a16_13 ? cs)
+ (a16_14 ? cs) (a16_15 ? cs) (a16_16 ? cs) 〈〈xF,xF〉:〈xF,xF〉〉).
ndefinition push_callstack ≝
λcs:aux_callstack_type.λtop.
(〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
(〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉).
-ndefinition get_low3bits ≝
-λaddrsel:byte8.
- match cnL ? addrsel with
- [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7
- | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ].
-
ndefinition get_addrarray ≝
λaddrsel:byte8.λaa:aux_addrarray_type.
- getn_array8T (get_low3bits addrsel) ? aa.
+ getn_array8T (oct_of_exL (cnL ? addrsel)) ? aa.
ndefinition set_addrarray ≝
λaddrsel:byte8.λaa:aux_addrarray_type.λv.
- setn_array8T (get_low3bits addrsel) ? aa v.
+ setn_array8T (oct_of_exL (cnL ? addrsel)) ? aa v.
(* *********************************** *)
(* STATUS INTERNO DEL PROCESSORE (ALU) *)
(c_flag_IP2022 alu)
(skip_mode_IP2022 alu).
+ndefinition pop_call_reg_IP2022 ≝
+λalu.
+ match pop_callstack (call_stack_IP2022 alu) with
+ [ pair val call' ⇒
+ pair … val
+ (mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ call'
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu)) ].
+
(* setter specifico IP2022 di IP *)
ndefinition set_ip_reg_IP2022 ≝
λalu.λip':word16.
(* X: registro indice parte bassa *)
(* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
(* la lettura/scrittura avviene tramite la locazione [0x000F] *)
- (* la funzione memory_filter_read/write si occupera' di intercettare *)
- (* e deviare sul registro le letture/scritture (modulo load_write) *)
x_map_RS08 : byte8;
(* PS: registro selezione di pagina *)
(* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *)
(* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *)
(* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
(* la lettura/scrittura avviene tramite la locazione [0x001F] *)
- (* la funzione memory_filter_read/write si occupera' di intercettare *)
- (* e deviare sul registro le letture/scritture (modulo load_write) *)
ps_map_RS08 : byte8;
(* Z: flag zero *)
| IP2022 ⇒ Some ? push_call_reg_IP2022 ])
(λf.Some ? (set_alu m t s (f (alu m t s) call'))).
-(* push debole di CALL *)
-ndefinition pushweak_call_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
- match push_call_reg m t s call' with
- [ None ⇒ s | Some s' ⇒ s' ].
+(* pop forte di CALL *)
+ndefinition pop_call_reg ≝
+λm:mcu_type.
+ match m
+ return λm.Πt.any_status m t → option (ProdT word16 (any_status m t))
+ with
+ [ HC05 ⇒ λt:memory_impl.λs:any_status HC05 t.None ?
+ | HC08 ⇒ λt:memory_impl.λs:any_status HC08 t.None ?
+ | HCS08 ⇒ λt:memory_impl.λs:any_status HCS08 t.None ?
+ | RS08 ⇒ λt:memory_impl.λs:any_status RS08 t.None ?
+ | IP2022 ⇒ λt:memory_impl.λs:any_status IP2022 t.
+ match pop_call_reg_IP2022 (alu … s) with
+ [ pair val alu' ⇒ Some ? (pair … val (set_alu … s alu')) ]
+ ].
(* REGISTRO IP *)
ndefinition ex_of_oct ≝
λn.match n with
[ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].
+
+(* esadecimali xNNNN → ottali *)
+ndefinition oct_of_exL ≝
+λn.match n with
+ [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7
+ | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ].
+
+(* esadecimali NNNNx → ottali *)
+ndefinition oct_of_exH ≝
+λn.match n with
+ [ x0 ⇒ o0 | x1 ⇒ o0 | x2 ⇒ o1 | x3 ⇒ o1 | x4 ⇒ o2 | x5 ⇒ o2 | x6 ⇒ o3 | x7 ⇒ o3
+ | x8 ⇒ o4 | x9 ⇒ o4 | xA ⇒ o5 | xB ⇒ o5 | xC ⇒ o6 | xD ⇒ o6 | xE ⇒ o7 | xF ⇒ o7 ].
| o6: oct
| o7: oct.
+(* iteratore sugli ottali *)
+ndefinition forall_oct ≝ λP.
+ P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
+
(* operatore = *)
ndefinition eq_oct ≝
λn1,n2:oct.
| o7 ⇒ match n2 with [ o7 ⇒ true | _ ⇒ false ]
].
-(* iteratore sugli ottali *)
-ndefinition forall_oct ≝ λP.
- P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
+(* operatore and *)
+ndefinition and_oct ≝
+λe1,e2:oct.match e1 with
+ [ o0 ⇒ match e2 with
+ [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0
+ | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o0 | o7 ⇒ o0 ]
+ | o1 ⇒ match e2 with
+ [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1
+ | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o0 | o7 ⇒ o1 ]
+ | o2 ⇒ match e2 with
+ [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2
+ | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o2 | o7 ⇒ o2 ]
+ | o3 ⇒ match e2 with
+ [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
+ | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ]
+ | o4 ⇒ match e2 with
+ [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0
+ | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o4 | o7 ⇒ o4 ]
+ | o5 ⇒ match e2 with
+ [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1
+ | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o4 | o7 ⇒ o5 ]
+ | o6 ⇒ match e2 with
+ [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2
+ | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o6 | o7 ⇒ o6 ]
+ | o7 ⇒ match e2 with
+ [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
+ | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
+ ].
+
+(* operatore or *)
+ndefinition or_oct ≝
+λe1,e2:oct.match e1 with
+ [ o0 ⇒ match e2 with
+ [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
+ | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
+ | o1 ⇒ match e2 with
+ [ o0 ⇒ o1 | o1 ⇒ o1 | o2 ⇒ o3 | o3 ⇒ o3
+ | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ]
+ | o2 ⇒ match e2 with
+ [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o2 | o3 ⇒ o3
+ | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ]
+ | o3 ⇒ match e2 with
+ [ o0 ⇒ o3 | o1 ⇒ o3 | o2 ⇒ o3 | o3 ⇒ o3
+ | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ]
+ | o4 ⇒ match e2 with
+ [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7
+ | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
+ | o5 ⇒ match e2 with
+ [ o0 ⇒ o5 | o1 ⇒ o5 | o2 ⇒ o7 | o3 ⇒ o7
+ | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ]
+ | o6 ⇒ match e2 with
+ [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o6 | o3 ⇒ o7
+ | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ]
+ | o7 ⇒ match e2 with
+ [ o0 ⇒ o7 | o1 ⇒ o7 | o2 ⇒ o7 | o3 ⇒ o7
+ | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ]
+ ].
+
+(* operatore xor *)
+ndefinition xor_oct ≝
+λe1,e2:oct.match e1 with
+ [ o0 ⇒ match e2 with
+ [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
+ | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
+ | o1 ⇒ match e2 with
+ [ o0 ⇒ o1 | o1 ⇒ o0 | o2 ⇒ o3 | o3 ⇒ o2
+ | o4 ⇒ o5 | o5 ⇒ o4 | o6 ⇒ o7 | o7 ⇒ o6 ]
+ | o2 ⇒ match e2 with
+ [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o0 | o3 ⇒ o1
+ | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o4 | o7 ⇒ o5 ]
+ | o3 ⇒ match e2 with
+ [ o0 ⇒ o3 | o1 ⇒ o2 | o2 ⇒ o1 | o3 ⇒ o0
+ | o4 ⇒ o7 | o5 ⇒ o6 | o6 ⇒ o5 | o7 ⇒ o4 ]
+ | o4 ⇒ match e2 with
+ [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7
+ | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ]
+ | o5 ⇒ match e2 with
+ [ o0 ⇒ o5 | o1 ⇒ o4 | o2 ⇒ o7 | o3 ⇒ o6
+ | o4 ⇒ o1 | o5 ⇒ o0 | o6 ⇒ o3 | o7 ⇒ o2 ]
+ | o6 ⇒ match e2 with
+ [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o4 | o3 ⇒ o5
+ | o4 ⇒ o2 | o5 ⇒ o3 | o6 ⇒ o0 | o7 ⇒ o1 ]
+ | o7 ⇒ match e2 with
+ [ o0 ⇒ o7 | o1 ⇒ o6 | o2 ⇒ o5 | o3 ⇒ o4
+ | o4 ⇒ o3 | o5 ⇒ o2 | o6 ⇒ o1 | o7 ⇒ o0 ]
+ ].
(* operatore successore *)
ndefinition succ_oct ≝
projects / helm.git / commitdiff