-common/nat.ma num/bool.ma
-num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma
-num/word32.ma num/word16.ma
-test_errori.ma
-common/list_lemmas.ma common/list.ma
-num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma
-num/bitrigesim.ma num/bool.ma
+freescale/multivm_lemmas.ma common/nat_lemmas.ma freescale/multivm.ma
+freescale/status.ma freescale/memory_abs.ma freescale/opcode_base.ma
+freescale/memory_bits.ma freescale/memory_trees.ma
+common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma
+num/bool.ma common/theory.ma
+freescale/table_HCS08_tests.ma freescale/opcode.ma freescale/table_HCS08.ma
+freescale/multivm.ma freescale/load_write.ma
common/ascii_lemmas1.ma common/ascii.ma
-num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma
-common/prod.ma num/bool.ma
-common/ascii_lemmas2.ma common/ascii_lemmas1.ma num/bool_lemmas.ma
-freescale/opcode.ma common/list.ma freescale/opcode_base.ma
-common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma
+freescale/opcode_base_lemmas.ma freescale/opcode_base.ma num/bool_lemmas.ma
common/string_lemmas.ma common/ascii_lemmas2.ma common/list_utility_lemmas.ma common/string.ma
-common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma
-num/bool_lemmas.ma num/bool.ma
-freescale/table_RS08.ma common/list.ma freescale/opcode_base.ma
-common/option_lemmas.ma common/option.ma num/bool_lemmas.ma
-num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma
-freescale/opcode_base.ma num/word16.ma
-num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma
+common/nat.ma num/bool.ma
+num/quatern.ma num/bool.ma
freescale/table_HC05_tests.ma freescale/opcode.ma freescale/table_HC05.ma
+num/exadecim.ma common/nat.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma
+num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma
+num/byte8.ma num/bitrigesim.ma num/exadecim.ma
+freescale/opcode_base_lemmas_opcode1.ma freescale/opcode_base.ma num/bool_lemmas.ma
+freescale/memory_func.ma common/list.ma common/option.ma freescale/memory_struct.ma num/word16.ma
+freescale/load_write.ma freescale/model.ma freescale/translation.ma
+freescale/table_RS08.ma common/list.ma freescale/opcode_base.ma
+common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma
+common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma
+freescale/table_RS08_tests.ma freescale/opcode.ma freescale/table_RS08.ma
+freescale/translation.ma common/option.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma
+freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma
+num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma
+test_errori.ma
+freescale/memory_struct.ma num/byte8.ma num/oct.ma
+freescale/model.ma freescale/status.ma
+freescale/table_HC05.ma common/list.ma freescale/opcode_base.ma
+common/string.ma common/ascii.ma common/list_utility.ma
common/theory.ma
+num/word16.ma num/byte8.ma
+freescale/memory_trees.ma common/list.ma common/option.ma freescale/memory_struct.ma num/word16.ma
+common/prod.ma num/bool.ma
+freescale/opcode_base_lemmas_instrmode2.ma freescale/opcode_base_lemmas_instrmode1.ma
+num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma
+num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma
+freescale/opcode_base_lemmas1.ma freescale/opcode_base_lemmas_instrmode2.ma freescale/opcode_base_lemmas_opcode2.ma num/word16_lemmas.ma
+freescale/table_HC08.ma common/list.ma freescale/opcode_base.ma
+num/bool_lemmas.ma num/bool.ma
freescale/table_HCS08.ma common/list.ma freescale/opcode_base.ma
+num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma
+common/ascii.ma num/bool.ma
+num/word32.ma num/word16.ma
+freescale/opcode_base.ma num/word16.ma
+num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma
freescale/table_HC08_tests.ma freescale/opcode.ma freescale/table_HC08.ma
-num/quatern.ma num/bool.ma
-freescale/table_RS08_tests.ma freescale/opcode.ma freescale/table_RS08.ma
+common/option.ma num/bool.ma
+common/option_lemmas.ma common/option.ma num/bool_lemmas.ma
+num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma
+common/ascii_lemmas2.ma common/ascii_lemmas1.ma num/bool_lemmas.ma
+common/list_lemmas.ma common/list.ma
freescale/opcode_base_lemmas_instrmode1.ma freescale/opcode_base.ma num/bitrigesim_lemmas.ma num/exadecim_lemmas.ma num/oct_lemmas.ma
-freescale/opcode_base_lemmas_instrmode2.ma freescale/opcode_base_lemmas_instrmode1.ma
-freescale/opcode_base_lemmas_opcode1.ma freescale/opcode_base.ma num/bool_lemmas.ma
-num/oct.ma num/bool.ma
+num/bitrigesim.ma num/bool.ma
+common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma
freescale/opcode_base_lemmas_opcode2.ma freescale/opcode_base_lemmas_opcode1.ma
-num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma
-freescale/table_HCS08_tests.ma freescale/opcode.ma freescale/table_HCS08.ma
-freescale/table_HC05.ma common/list.ma freescale/opcode_base.ma
-freescale/opcode_base_lemmas.ma freescale/opcode_base.ma num/bool_lemmas.ma
-common/option.ma num/bool.ma
-num/byte8.ma num/bitrigesim.ma num/exadecim.ma
-num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma
-common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma
-num/bool.ma common/theory.ma
-freescale/table_HC08.ma common/list.ma freescale/opcode_base.ma
-num/word16.ma num/byte8.ma
-common/string.ma common/ascii.ma common/list_utility.ma
-common/ascii.ma num/bool.ma
common/list.ma common/theory.ma
-freescale/opcode_base_lemmas1.ma freescale/opcode_base_lemmas_instrmode2.ma freescale/opcode_base_lemmas_opcode2.ma num/word16_lemmas.ma
-common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma
-freescale/translation.ma common/option.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma
-num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma
+num/oct.ma num/bool.ma
+freescale/opcode.ma common/list.ma freescale/opcode_base.ma
--- /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: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "freescale/model.ma".
+include "freescale/translation.ma".
+
+(* errori possibili nel fetch *)
+ninductive error_type : Type ≝
+ ILL_OP: error_type
+| ILL_FETCH_AD: error_type
+| ILL_EX_AD: error_type.
+
+(* un tipo opzione ad hoc
+ - errore: interessa solo l'errore
+ - ok: interessa info e il nuovo pc
+*)
+ninductive fetch_result (A:Type) : Type ≝
+ FetchERR : error_type → fetch_result A
+| FetchOK : A → word16 → fetch_result A.
+
+(* **************************** *)
+(* FETCH E ACCESSO ALLA MEMORIA *)
+(* **************************** *)
+
+(* ausialiaria per RS08 read *)
+(* come anticipato in status, nell'RS08 ci sono 2 registri importanti
+ memory mapped, quindi bisona intercettare la lettura.
+ 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:word16.
+λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option T.
+match s with
+ [ mk_any_status alu mem chk _ ⇒ match alu with
+ [ mk_alu_RS08 _ _ _ _ xm psm _ _ ⇒
+(*
+ 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 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
+ (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
+ (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
+ [ true ⇒ fREG xm
+ | 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 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
+ (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
+ (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
+ [ true ⇒ fREG psm
+ | false ⇒
+(*
+ accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
+ altrimenti sarebbero 2 indirezioni
+*)
+ match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
+ [ true ⇒ fMEM mem chk 〈〈x0,x0〉:xm〉
+ | false ⇒
+(*
+ accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
+*)
+ 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 normale
+*)
+ | false ⇒ fMEM mem chk addr ]]]]]].
+
+(* lettura RS08 di un byte *)
+ndefinition RS08_memory_filter_read ≝
+λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
+ RS08_memory_filter_read_aux t s addr byte8
+ (λb.Some byte8 b)
+ (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.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:word16.λ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:word16.mem_read_bit t m c a sub).
+
+(* in caso di RS08 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 → word16 → option byte8 with
+ [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.
+ mem_read t (mem_desc ? t s) (chk_desc ? t s) addr
+ | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.
+ mem_read t (mem_desc ? t s) (chk_desc ? t s) addr
+ | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.
+ mem_read t (mem_desc ? t s) (chk_desc ? t s) addr
+ | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.
+ RS08_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 → word16 → oct → option bool with
+ [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.
+ mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub
+ | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.
+ mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub
+ | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.
+ mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub
+ | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.
+ RS08_memory_filter_read_bit t s addr sub
+ ].
+
+(* ausialiaria per RS08 write *)
+(* come anticipato in status, nell'RS08 ci sono 2 registri importanti
+ memory mapped, quindi bisona intercettare la scrittura.
+ 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_write_aux ≝
+λt:memory_impl.λs:any_status RS08 t.λaddr:word16.
+λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word16 → option (aux_mem_type t).
+match s with
+ [ mk_any_status alu mem chk clk ⇒ match alu with
+ [ mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl ⇒
+(*
+ 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 addr 〈〈x0,x0〉:〈x0,xF〉〉 ⊕
+ (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x0,xF〉) ⊕
+ (eq_w16 addr 〈〈x0,x0〉:〈xC,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
+ [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc (fREG xm) psm zfl cfl) mem chk clk)
+ | 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 addr 〈〈x0,x0〉:〈x1,xF〉〉 ⊕
+ (eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 ⊗ eq_b8 xm 〈x1,xF〉) ⊕
+ (eq_w16 addr 〈〈x0,x0〉:〈xD,xF〉〉 ⊗ eq_b8 psm 〈x0,x0〉) with
+ [ true ⇒ Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm (fREG psm) zfl cfl) mem chk clk)
+ | false ⇒
+(*
+ accesso a D[X]: se accede a [00C0-00FF] e' la RAM fisica, non il paging
+ altrimenti sarebbero 2 indirezioni
+*)
+ match eq_w16 addr 〈〈x0,x0〉:〈x0,xE〉〉 with
+ [ true ⇒ opt_map … (fMEM mem chk 〈〈x0,x0〉:xm〉)
+ (λ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 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
+*)
+ | false ⇒ opt_map … (fMEM mem chk addr)
+ (λ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 *)
+ndefinition RS08_memory_filter_write ≝
+λt:memory_impl.λs:any_status RS08 t.λaddr:word16.λval:byte8.
+ RS08_memory_filter_write_aux t s addr
+ (λb.val)
+ (λm:aux_mem_type t.λc:aux_chk_type t.λa:word16.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:word16.λ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:word16.mem_update_bit t m c a sub val).
+
+(* in caso di RS08 si dirotta sul filtro, altrimenti si scrive direttamente *)
+ndefinition memory_filter_write ≝
+λ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.
+ 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:word16.λ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:word16.λ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:word16.λval:byte8.
+ RS08_memory_filter_write t s addr val
+ ].
+
+ndefinition memory_filter_write_bit ≝
+λ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.
+ 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:word16.λ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:word16.λ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:word16.λsub:oct.λval:bool.
+ RS08_memory_filter_write_bit t s addr sub val
+ ].
+
+(*
+ Da utilizzarsi solo per gli aggiornamenti di PC (per il fetch),
+ NON per il caricamento degli indiretti.
+ - il caricamento degli immediati spetta al fetcher
+ (incremento progressivo di PC ciclo per ciclo, e riempimento del prefetch
+ che a questo punto DEVE poter indirizzare qualsiasi locazione puntata da PC)
+ - il caricamento degli indiretti non spetta al fetcher
+*)
+ndefinition filtered_inc_w16 ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
+ get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
+
+nlet rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
+ match n with
+ [ O ⇒ w
+ | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
+
+(*
+ errore1: non esiste traduzione ILL_OP
+ errore2: non e' riuscito a leggere ILL_FETCH_AD
+ altrimenti OK=info+new_pc
+*)
+ndefinition fetch ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ let pc ≝ get_pc_reg m t s in
+ let pc_next1 ≝ filtered_inc_w16 m t s pc in
+ let pc_next2 ≝ filtered_inc_w16 m t s pc_next1 in
+ match memory_filter_read m t s pc with
+ [ None ⇒ FetchERR ? ILL_FETCH_AD
+ | Some bh ⇒ match full_info_of_word16 m (Byte bh) with
+ (* non ha trovato una traduzione con 1 byte *)
+ [ None ⇒ match m with
+ (* HC05 non esistono op a 2 byte *)
+ [ HC05 ⇒ FetchERR ? ILL_OP
+ | HC08 ⇒ match eq_b8 bh 〈x9,xE〉 with
+ (* HC08 se il primo byte e' 0x9E il secondo puo' avere senso *)
+ [ true ⇒ match memory_filter_read m t s pc_next1 with
+ [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
+ [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
+ (* HC08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
+ | false ⇒ FetchERR ? ILL_OP
+ ]
+ | HCS08 ⇒ match eq_b8 bh 〈x9,xE〉 with
+ (* HCS08 se il primo byte e' 0x9E il secondo puo' avere senso *)
+ [ true ⇒ match memory_filter_read m t s pc_next1 with
+ [ None ⇒ FetchERR ? ILL_FETCH_AD | Some bl ⇒ match full_info_of_word16 m (Word (mk_word16 bh bl)) with
+ [ None ⇒ FetchERR ? ILL_OP | Some info ⇒ FetchOK ? info pc_next2 ]]
+ (* HCS08 se il primo byte non e' 0x9E il secondo non puo' avere senso *)
+ | false ⇒ FetchERR ? ILL_OP
+ ]
+ (* RS08 non esistono op a 2 byte *)
+ | RS08 ⇒ FetchERR ? ILL_OP
+ ]
+ (* ha trovato una traduzione con 1 byte *)
+ | Some info ⇒ FetchOK ? info pc_next1 ]].
+
+(* ************************ *)
+(* MODALITA' INDIRIZZAMENTO *)
+(* ************************ *)
+
+(* mattoni base *)
+(* - incrementano l'indirizzo normalmente *)
+(* - incrementano PC attraverso il filtro *)
+
+(* 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))).
+
+(* 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))).
+
+(* 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)))).
+
+(* 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))).
+
+(* 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))).
+
+(* 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)))).
+
+(* ausiliari per definire i tipi e la lettura/scrittura *)
+
+(* ausiliaria per definire il tipo di aux_load *)
+ndefinition aux_load_typing ≝
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.
+ any_status m t → word16 → word16 → nat →
+ option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
+
+(* per non dover ramificare i vari load in byte/word *)
+ndefinition aux_load ≝
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
+ [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
+
+(* ausiliaria per definire il tipo di aux_write *)
+ndefinition aux_write_typing ≝
+λ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).
+
+(* per non dover ramificare i vari load in byte/word *)
+ndefinition aux_write ≝
+λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
+ [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
+
+(* modalita' vere e proprie *)
+
+(* 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))).
+
+(* 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))).
+
+(* 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)))).
+
+(* 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).
+
+(* 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).
+
+(* 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).
+
+(* 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).
+
+(* 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)).
+
+(* 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))
+ (λ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)
+ | 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.
+ 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 *)
+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).
+
+(* 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)).
+
+(* 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)))).
+
+(* 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 ].
+ 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)).
+
+(* 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))
+ (λ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))))).
+
+(* 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))
+ (λ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.
+ 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)).
+
+(* 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 ].
+ 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)).
+
+(* 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))
+ (λ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))
+ (λoffsl.(aux_write m t byteflag) s (plus_w16_d_d addr 〈offsh:offsl〉) cur_pc 2 writebw))).
+
+(* ************************************** *)
+(* raccordo di tutte le possibili letture *)
+(* ************************************** *)
+
+(* H:X++ *)
+ndefinition aux_inc_indX_16 ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ opt_map … (get_indX_16_reg m t s)
+ (λX_op.opt_map … (set_indX_16_reg m t s (succ_w16 X_op))
+ (λ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)
+ 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 *)
+ | MODE_INHA ⇒ Some ? (triple … s (get_acc_8_low_reg m t s) cur_pc)
+(* restituisce X *)
+ | MODE_INHX ⇒ opt_map … (get_indX_8_low_reg m t s)
+ (λindx.Some ? (triple … s indx cur_pc))
+(* restituisce H *)
+ | MODE_INHH ⇒ opt_map … (get_indX_8_high_reg m t s)
+ (λindx.Some ? (triple … 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 *)
+ | MODE_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
+(* preleva 1 byte da indirizzo diretto 1 word *)
+ | MODE_DIR2 ⇒ mode_DIR2_load true m t s cur_pc
+(* preleva 1 byte da H:X *)
+ | MODE_IX0 ⇒ mode_IX0_load true m t s cur_pc
+(* preleva 1 byte da H:X+1 byte offset *)
+ | MODE_IX1 ⇒ mode_IX1_load true m t s cur_pc
+(* preleva 1 byte da H:X+1 word offset *)
+ | MODE_IX2 ⇒ mode_IX2_load true m t s cur_pc
+(* preleva 1 byte da SP+1 byte offset *)
+ | MODE_SP1 ⇒ mode_SP1_load true m t s cur_pc
+(* preleva 1 byte da SP+1 word offset *)
+ | MODE_SP2 ⇒ mode_SP2_load true m t s cur_pc
+
+(* come DIR1, chiamare scrittura per passo2: scrittura su DIR1 *)
+ | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_load true m t s cur_pc
+(* 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++ *)
+ | MODE_IX0p_to_DIR1 ⇒ mode_IX0_load true m t s cur_pc
+(* come DIR1, chiamare scrittura per passo2: scrittura su IX0 e X++ *)
+ | MODE_DIR1_to_IX0p ⇒ mode_DIR1_load true m t s cur_pc
+
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_INHA_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_INHX_and_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM1_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_DIR1_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_IX0_and_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IX0p_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_IX1_and_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IX1p_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_SP1_and_IMM1 ⇒ None ?
+
+(* NO: solo scrittura byte *)
+ | MODE_DIRn _ ⇒ None ?
+(* 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))
+(* preleva 1 byte da 0000 0000 000x xxxxb *)
+ | 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 *)
+ | false ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.match i with
+(* NO: non ci sono indicazioni *)
+ [ MODE_INH ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_INHA ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_INHX ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_INHH ⇒ None ?
+
+(* preleva 1 word immediato *)
+ | MODE_INHX0ADD ⇒ opt_map … (get_IX m t s)
+ (λw.Some ? (triple … 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 *)
+ | MODE_DIR1 ⇒ mode_DIR1_load false m t s cur_pc
+(* preleva 1 word da indirizzo diretto 1 word *)
+ | MODE_DIR2 ⇒ mode_DIR2_load false m t s cur_pc
+(* preleva 1 word da H:X *)
+ | MODE_IX0 ⇒ mode_IX0_load false m t s cur_pc
+(* preleva 1 word da H:X+1 byte offset *)
+ | MODE_IX1 ⇒ mode_IX1_load false m t s cur_pc
+(* preleva 1 word da H:X+1 word offset *)
+ | MODE_IX2 ⇒ mode_IX2_load false m t s cur_pc
+(* preleva 1 word da SP+1 byte offset *)
+ | MODE_SP1 ⇒ mode_SP1_load false m t s cur_pc
+(* preleva 1 word da SP+1 word offset *)
+ | MODE_SP2 ⇒ mode_SP2_load false m t s cur_pc
+
+(* NO: solo lettura/scrittura byte *)
+ | MODE_DIR1_to_DIR1 ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_IMM1_to_DIR1 ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_IX0p_to_DIR1 ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_DIR1_to_IX0p ⇒ None ?
+
+(* preleva 2 byte, possibilita' modificare Io argomento *)
+ | MODE_INHA_and_IMM1 ⇒ opt_map … (mode_IMM1_load m t s cur_pc)
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc' ⇒
+ Some ? (triple … s 〈(get_acc_8_low_reg m t s):immb〉 cur_pc')])
+(* 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)
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc' ⇒
+ Some ? (triple … s 〈X_op:immb〉 cur_pc')]))
+(* preleva 2 byte, NO possibilita' modificare Io argomento *)
+ | MODE_IMM1_and_IMM1 ⇒ opt_map … (mode_IMM1_load m t s cur_pc)
+ (λS_immb1_and_PC.match S_immb1_and_PC with
+ [ triple _ immb1 cur_pc' ⇒
+ opt_map … (mode_IMM1_load m t s cur_pc')
+ (λS_immb2_and_PC.match S_immb2_and_PC with
+ [ triple _ immb2 cur_pc'' ⇒
+ Some ? (triple … s 〈immb1:immb2〉 cur_pc'')])])
+(* preleva 2 byte, possibilita' modificare Io argomento *)
+ | MODE_DIR1_and_IMM1 ⇒ opt_map … (mode_DIR1_load true m t s cur_pc)
+ (λS_dirb_and_PC.match S_dirb_and_PC with
+ [ triple _ dirb cur_pc' ⇒
+ opt_map … (mode_IMM1_load m t s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ Some ? (triple … s 〈dirb:immb〉 cur_pc'')])])
+(* preleva 2 byte, possibilita' modificare Io argomento *)
+ | MODE_IX0_and_IMM1 ⇒ opt_map … (mode_IX0_load true m t s cur_pc)
+ (λS_ixb_and_PC.match S_ixb_and_PC with
+ [ triple _ ixb cur_pc' ⇒
+ opt_map … (mode_IMM1_load m t s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ Some ? (triple … s 〈ixb:immb〉 cur_pc'')])])
+(* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
+ | MODE_IX0p_and_IMM1 ⇒ opt_map … (mode_IX0_load true m t s cur_pc)
+ (λS_ixb_and_PC.match S_ixb_and_PC with
+ [ triple _ ixb cur_pc' ⇒
+ opt_map … (mode_IMM1_load m t s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ (* H:X++ *)
+ opt_map … (aux_inc_indX_16 m t s)
+ (λs'.Some ? (triple … s' 〈ixb:immb〉 cur_pc''))])])
+(* preleva 2 byte, possibilita' modificare Io argomento *)
+ | MODE_IX1_and_IMM1 ⇒ opt_map … (mode_IX1_load true m t s cur_pc)
+ (λS_ixb_and_PC.match S_ixb_and_PC with
+ [ triple _ ixb cur_pc' ⇒
+ opt_map … (mode_IMM1_load m t s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ Some ? (triple … s 〈ixb:immb〉 cur_pc'')])])
+(* preleva 2 byte, H:X++, NO possibilita' modificare Io argomento *)
+ | MODE_IX1p_and_IMM1 ⇒ opt_map … (mode_IX1_load true m t s cur_pc)
+ (λS_ixb_and_PC.match S_ixb_and_PC with
+ [ triple _ ixb cur_pc' ⇒
+ opt_map … (mode_IMM1_load m t s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ (* H:X++ *)
+ opt_map … (aux_inc_indX_16 m t s)
+ (λs'.Some ? (triple … s' 〈ixb:immb〉 cur_pc''))])])
+(* preleva 2 byte, possibilita' modificare Io argomento *)
+ | MODE_SP1_and_IMM1 ⇒ opt_map … (mode_SP1_load true m t s cur_pc)
+ (λS_spb_and_PC.match S_spb_and_PC with
+ [ triple _ spb cur_pc' ⇒
+ opt_map … (mode_IMM1_load m t s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ Some ? (triple … s 〈spb:immb〉 cur_pc'')])])
+
+(* NO: solo scrittura byte *)
+ | MODE_DIRn _ ⇒ None ?
+(* preleva 2 byte, il primo e' filtrato per azzerare tutti i bit tranne n-simo *)
+ | MODE_DIRn_and_IMM1 msk ⇒ opt_map … (mode_DIR1n_load m t s cur_pc msk)
+ (λS_dirbn_and_PC.match S_dirbn_and_PC with
+ [ triple _ dirbn cur_pc' ⇒
+ opt_map … (mode_IMM1_load m t s cur_pc')
+ (λS_immb_and_PC.match S_immb_and_PC with
+ [ triple _ immb cur_pc'' ⇒
+ Some ? (triple … s 〈〈x0,match dirbn with [ true ⇒ x1 | false ⇒ x0 ]〉:immb〉 cur_pc'') ])])
+(* NO: solo lettura/scrittura byte *)
+ | MODE_TNY _ ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_SRT _ ⇒ None ?
+ ]
+ ].
+
+(* **************************************** *)
+(* raccordo di tutte le possibili scritture *)
+(* **************************************** *)
+
+(* tutte le modalita' di scrittura: true=writeb, false=writew *)
+ndefinition multi_mode_write ≝
+λ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
+ (* 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 ? (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 ? (pair … tmps cur_pc))
+(* scrive H *)
+ | MODE_INHH ⇒ opt_map … (set_indX_8_high_reg m t s writeb)
+ (λ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_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
+(* scrive 1 byte su indirizzo diretto 1 word *)
+ | MODE_DIR2 ⇒ mode_DIR2_write true m t s cur_pc writeb
+(* scrive 1 byte su H:X *)
+ | MODE_IX0 ⇒ mode_IX0_write true m t s cur_pc writeb
+(* scrive 1 byte su H:X+1 byte offset *)
+ | MODE_IX1 ⇒ mode_IX1_write true m t s cur_pc writeb
+(* scrive 1 byte su H:X+1 word offset *)
+ | MODE_IX2 ⇒ mode_IX2_write true m t s cur_pc writeb
+(* scrive 1 byte su SP+1 byte offset *)
+ | MODE_SP1 ⇒ mode_SP1_write true m t s cur_pc writeb
+(* scrive 1 byte su SP+1 word offset *)
+ | MODE_SP2 ⇒ mode_SP2_write true m t s cur_pc writeb
+
+(* passo2: scrittura su DIR1, passo1: lettura da DIR1 *)
+ | MODE_DIR1_to_DIR1 ⇒ mode_DIR1_write true m t s cur_pc writeb
+(* 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_IX0p_to_DIR1 ⇒ opt_map … (mode_DIR1_write true m t s cur_pc writeb)
+ (λ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 *)
+ | MODE_DIR1_to_IX0p ⇒ opt_map … (mode_IX0_write true m t s cur_pc writeb)
+ (λ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))])
+
+(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
+ | 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 ? (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_DIR1_and_IMM1 ⇒ mode_DIR1_write true m t s cur_pc writeb
+(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX0 *)
+ | MODE_IX0_and_IMM1 ⇒ mode_IX0_write true m t s cur_pc writeb
+(* NO: solo lettura word *)
+ | MODE_IX0p_and_IMM1 ⇒ None ?
+(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = IX1 *)
+ | MODE_IX1_and_IMM1 ⇒ mode_IX1_write true m t s cur_pc writeb
+(* NO: solo lettura word *)
+ | MODE_IX1p_and_IMM1 ⇒ None ?
+(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = SP1 *)
+ | MODE_SP1_and_IMM1 ⇒ mode_SP1_write true m t s cur_pc 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))
+(* 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))
+(* scrive 1 byte su 0000 0000 000x xxxxb *)
+ | 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 *)
+ [ MODE_INH ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_INHA ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_INHX ⇒ None ?
+(* 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 *)
+ | MODE_DIR1 ⇒ mode_DIR1_write false m t s cur_pc writew
+(* scrive 1 word su indirizzo diretto 1 word *)
+ | MODE_DIR2 ⇒ mode_DIR2_write false m t s cur_pc writew
+(* scrive 1 word su H:X *)
+ | MODE_IX0 ⇒ mode_IX0_write false m t s cur_pc writew
+(* scrive 1 word su H:X+1 byte offset *)
+ | MODE_IX1 ⇒ mode_IX1_write false m t s cur_pc writew
+(* scrive 1 word su H:X+1 word offset *)
+ | MODE_IX2 ⇒ mode_IX2_write false m t s cur_pc writew
+(* scrive 1 word su SP+1 byte offset *)
+ | MODE_SP1 ⇒ mode_SP1_write false m t s cur_pc writew
+(* scrive 1 word su SP+1 word offset *)
+ | MODE_SP2 ⇒ mode_SP2_write false m t s cur_pc writew
+
+(* NO: solo lettura/scrittura byte *)
+ | MODE_DIR1_to_DIR1 ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_IMM1_to_DIR1 ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_IX0p_to_DIR1 ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_DIR1_to_IX0p ⇒ None ?
+
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_INHA_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_INHX_and_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IMM1_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_DIR1_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_IX0_and_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IX0p_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_IX1_and_IMM1 ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_IX1p_and_IMM1 ⇒ None ?
+(* NO: solo lettura word/scrittura byte *)
+ | MODE_SP1_and_IMM1 ⇒ None ?
+
+(* NO: solo scrittura byte *)
+ | MODE_DIRn _ ⇒ None ?
+(* NO: solo lettura word *)
+ | MODE_DIRn_and_IMM1 _ ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_TNY _ ⇒ None ?
+(* NO: solo lettura/scrittura byte *)
+ | MODE_SRT _ ⇒ None ?
+ ]
+ ].
--- /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: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "freescale/status.ma".
+
+(* *********************************** *)
+(* IMPOSTAZIONI SPECIFICHE DEI MODELLI *)
+(* *********************************** *)
+
+(* modelli di HC05 *)
+ninductive HC05_mcu_model : Type ≝
+ MC68HC05J5A: HC05_mcu_model
+ (*..*).
+
+(* modelli di HC08 *)
+ninductive HC08_mcu_model : Type ≝
+ MC68HC08AB16A: HC08_mcu_model
+ (*..*).
+
+(* modelli di HCS08 *)
+ninductive HCS08_mcu_model : Type ≝
+ MC9S08AW60 : HCS08_mcu_model
+| MC9S08GB60 : HCS08_mcu_model
+ (*..*).
+
+(* modelli di RS08 *)
+ninductive RS08_mcu_model : Type ≝
+ MC9RS08KA1 : RS08_mcu_model
+| MC9RS08KA2 : RS08_mcu_model.
+
+(* raggruppamento dei modelli *)
+ninductive any_mcu_model : Type ≝
+ FamilyHC05 : HC05_mcu_model → any_mcu_model
+| FamilyHC08 : HC08_mcu_model → any_mcu_model
+| FamilyHCS08 : HCS08_mcu_model → any_mcu_model
+| FamilyRS08 : RS08_mcu_model → any_mcu_model.
+
+(*
+condizioni errore interne alla MCU
+(Il programma viene caricato dal produttore in ROM o impostato in EEPROM)
+HC05: +illegal address during opcode fetch
+HC08: +illegal address duting opcode fetch (ILAD mascherabile)
+ +illegal opcode (ILOP mascherabile)
+
+(Il programma viene programmato nella FLASH)
+HCS08: +illegal address during opcode fetch (ILAD mascherabile)
+ +illegal opcode (ILOP mascherabile)
+ +security = accesso a RAM e zone FLASH dichiarate sicure da zone sicure
+ da' 0 in lettura e ignore in scrittura, [FLASH]SEC00:SEC01 (1,0)
+ corrisponde a OFF, altre ON, disattivabile solo da modalita' sicura se
+ opzione [FLASH]KEYEN e' 1 passando chiave a 8byte da modalita' sicura.
+ Altrimenti disattivabile solo con FLASH mass erase. Obbiettivo
+ e' impedire duplicazione di software di controllo, dato che esiste
+ modalita' debugging. A restart viene ricaricata da FLASH impostazione
+ sicurezza!
+RS08: +illegal address durting opcode fetch (ILAD) mascherabile
+ +illegal opcode (ILOP mascherabile)
+ +security = solo la FLASH e' considerata sicura. Stesso meccanismo di HCS08
+ ma governato solo da [FLASH]SECD (0) OFF.Una volta attivato l'unica
+ disattivazione e' la cancellazione della FLASH.
+*)
+
+(* memoria degli HC05 *)
+ndefinition memory_type_of_FamilyHC05 ≝
+λm:HC05_mcu_model.match m with
+ [ MC68HC05J5A ⇒
+ [
+ (* astraggo molto *)
+ (* 0x0000-0x001F,0x0FF0: sarebbe memory mapped IO *)
+
+ triple … 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 128B RAM+STACK *)
+ ; triple … 〈〈x0,x3〉:〈x0,x0〉〉 〈〈x0,xC〉:〈xF,xF〉〉 MEM_READ_ONLY (* 2560B USER ROM *)
+ ; triple … 〈〈x0,xE〉:〈x0,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 512B INTERNAL ROM *)
+ ]
+ (*..*)
+ ].
+
+(* memoria degli HC08 *)
+ndefinition memory_type_of_FamilyHC08 ≝
+λm:HC08_mcu_model.match m with
+ [ MC68HC08AB16A ⇒
+ [
+ (* astraggo molto *)
+ (* 0x0000-0x004F,0xFE00-0xFE01,0xFE03,
+ 0xFE0C-0xFE11,0xFE1A-0xFE1D,0xFE1F: sarebbe memory mapped IO *)
+ (* 0x0500-0x057F,0xFE02,0xFE04-0xFE07,
+ 0xFE09-0xFE0B,0xFE12-0xFE19,0xFE1E,0xFFC0-0xFFCF : sarebbe reserved *)
+
+ triple … 〈〈x0,x0〉:〈x5,x0〉〉 〈〈x0,x2〉:〈x4,xF〉〉 MEM_READ_WRITE (* 512B RAM *)
+ ; triple … 〈〈x0,x8〉:〈x0,x0〉〉 〈〈x0,x9〉:〈xF,xF〉〉 MEM_READ_ONLY (* 512B EEPROM *)
+ ; triple … 〈〈xB,xE〉:〈x0,x0〉〉 〈〈xF,xD〉:〈xF,xF〉〉 MEM_READ_ONLY (* 16384B ROM *)
+ ; triple … 〈〈xF,xE〉:〈x2,x0〉〉 〈〈xF,xF〉:〈x5,x2〉〉 MEM_READ_ONLY (* 307B ROM *)
+ ; triple … 〈〈xF,xF〉:〈xD,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 48B ROM *) ]
+ (*..*)
+ ].
+
+(* memoria degli HCS08 *)
+ndefinition memory_type_of_FamilyHCS08 ≝
+λm:HCS08_mcu_model.match m with
+ [ MC9S08AW60 ⇒
+ [
+ (* astraggo molto *)
+ (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *)
+
+ triple … 〈〈x0,x0〉:〈x7,x0〉〉 〈〈x0,x8〉:〈x6,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
+ ; triple … 〈〈x0,x8〉:〈x7,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 3984B FLASH *)
+ ; triple … 〈〈x1,x8〉:〈x6,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59296B FLASH *) ]
+ | MC9S08GB60 ⇒
+ [
+ (* astraggo molto *)
+ (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *)
+
+ triple … 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x1,x0〉:〈x7,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
+ ; triple … 〈〈x1,x0〉:〈x8,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 1920B FLASH *)
+ ; triple … 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59348B FLASH *) ]
+ ].
+
+(* memoria dei RS08 *)
+ndefinition memory_type_of_FamilyRS08 ≝
+λm:RS08_mcu_model.match m with
+ [ MC9RS08KA1 ⇒
+ [
+ triple … 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,xE〉〉 MEM_READ_WRITE (* 15B RAM *)
+ (* [000F] e' il registro X *)
+ (* 0x0010-0x001E sarebbe memory mapped IO, proviamo per completezza con RAM *)
+ ; triple … 〈〈x0,x0〉:〈x1,x0〉〉 〈〈x0,x0〉:〈x1,xE〉〉 MEM_READ_WRITE (* 15B MEMORY MAPPED IO *)
+ (* [001F] e' il registro PAGESEL *)
+ ; triple … 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x4,xF〉〉 MEM_READ_WRITE (* 48B RAM *)
+ (* [00C0-00FF] mappato da PAGESEL su [00pp pppp ppxx xxxx] *)
+ ; triple … 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 64B RAM PAGING *)
+ (* 0x0200-0x023F sarebbe memory mapped IO, proviamo per completezza con RAM *)
+ ; triple … 〈〈x0,x2〉:〈x0,x0〉〉 〈〈x0,x2〉:〈x3,xF〉〉 MEM_READ_WRITE (* 64B MEMORY MAPPED IO *)
+ ; triple … 〈〈x3,xC〉:〈x0,x0〉〉 〈〈x3,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 1024B FLASH *) ]
+ | MC9RS08KA2 ⇒
+ [
+ triple … 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,xE〉〉 MEM_READ_WRITE (* 15B RAM *)
+ (* [000F] e' il registro X *)
+ (* 0x0010-0x001E sarebbe memory mapped IO, proviamo per completezza con RAM *)
+ ; triple … 〈〈x0,x0〉:〈x1,x0〉〉 〈〈x0,x0〉:〈x1,xE〉〉 MEM_READ_WRITE (* 15B MEMORY MAPPED IO *)
+ (* [001F] e' il registro PAGESEL *)
+ ; triple … 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x4,xF〉〉 MEM_READ_WRITE (* 48B RAM *)
+ (* [00C0-00FF] mappato da PAGESEL su [00pp pppp ppxx xxxx] *)
+ ; triple … 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 64B RAM PAGING *)
+ (* 0x0200-0x023F sarebbe memory mapped IO, proviamo per completezza con RAM *)
+ ; triple … 〈〈x0,x2〉:〈x0,x0〉〉 〈〈x0,x2〉:〈x3,xF〉〉 MEM_READ_WRITE (* 64B MEMORY MAPPED IO *)
+ ; triple … 〈〈x3,x8〉:〈x0,x0〉〉 〈〈x3,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 2048B FLASH *) ]
+ ].
+
+(* ∀modello.descrizione della memoria installata *)
+ndefinition memory_type_of_mcu_version ≝
+λmcu:any_mcu_model.match mcu with
+ [ FamilyHC05 m ⇒ memory_type_of_FamilyHC05 m
+ | FamilyHC08 m ⇒ memory_type_of_FamilyHC08 m
+ | FamilyHCS08 m ⇒ memory_type_of_FamilyHCS08 m
+ | FamilyRS08 m ⇒ memory_type_of_FamilyRS08 m
+ ].
+
+(* dato un modello costruisce un descrittore a partire dalla lista precedente *)
+nlet rec build_memory_type_of_mcu_version_aux t param (result:aux_chk_type t) on param ≝
+ match param with
+ [ nil ⇒ result
+ | cons hd tl ⇒
+ build_memory_type_of_mcu_version_aux t tl
+ (check_update_ranged t result (fst3T ??? hd) (snd3T ??? hd) (thd3T ??? hd)) ].
+
+ndefinition build_memory_type_of_mcu_version ≝
+λmcu:any_mcu_model.λt:memory_impl.
+ build_memory_type_of_mcu_version_aux t (memory_type_of_mcu_version mcu) (out_of_bound_memory t).
+
+(* sarebbe programma da caricare/zero_memory, ora test *)
+ndefinition memory_of_mcu_version ≝
+λmcu:any_mcu_model.λt:memory_impl.match mcu with
+ [ FamilyHC05 m ⇒ match m with
+ [ MC68HC05J5A ⇒ zero_memory t
+ (*..*)
+ ]
+ | FamilyHC08 m ⇒ match m with
+ [ MC68HC08AB16A ⇒ zero_memory t
+ (*..*)
+ ]
+ (* tralascio l'enumerazione dei casi, per ora e' tutto 0 *)
+ | FamilyHCS08 _ ⇒ zero_memory t
+ | FamilyRS08 _ ⇒ zero_memory t
+ ].
+
+(*
+ 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 puo' essere passata, per esempio da
+ - (memory_of_mcu_version MC68HC05J5A)
+ - (build_memory_type_of_mcu_version MC68HC05J5A)
+*)
+ndefinition start_of_mcu_version_HC05 ≝
+λmcu:HC05_mcu_model.λt:memory_impl.
+λmem:aux_mem_type t.λchk:aux_chk_type t.
+λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
+ let build ≝ λspm,spf,pcm:word16.
+ let fetched_pc ≝ mk_word16 (mem_read_abs t mem (and_w16 〈〈xF,xF〉:〈xF,xE〉〉 pcm))
+ (mem_read_abs t mem (and_w16 〈〈xF,xF〉:〈xF,xF〉〉 pcm)) in
+ mk_any_status HC05 t
+ (mk_alu_HC05
+ (* acc_low: ? *) ndby1 (* indx_low: ? *) ndby2
+ (* sp: reset *) (or_w16 (and_w16 〈〈x0,x0〉:〈xF,xF〉〉 spm) spf) spm spf
+ (* pc: reset+fetch *) (and_w16 fetched_pc pcm) pcm
+ (* H: ? *) ndbo1 (* I: reset *) true (* N: ? *) ndbo2
+ (* Z: ? *) ndbo3 (* C: ? *) ndbo4 (* IRQ: ? *) irqfl)
+ (* mem *) mem
+ (* chk *) chk
+ (* clk: reset *) (None ?) in
+ match mcu with
+ [ MC68HC05J5A ⇒ build 〈〈x0,x0〉:〈x3,xF〉〉 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉
+ (*..*)
+ ].
+
+ndefinition start_of_mcu_version_HC08 ≝
+λmcu:HC08_mcu_model.λt:memory_impl.
+λmem:aux_mem_type t.λchk:aux_chk_type t.
+λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
+ let fetched_pc ≝ mk_word16 (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xE〉〉)
+ (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xF〉〉) in
+ mk_any_status HC08 t
+ (mk_alu_HC08
+ (* acc_low: ? *) ndby1 (* indw_low: ? *) ndby2 (* indx_high: reset *) 〈x0,x0〉
+ (* sp: reset *) 〈〈x0,x0〉:〈xF,xF〉〉 (* pc: reset+fetch *) fetched_pc
+ (* V: ? *) ndbo1 (* H: ? *) ndbo2 (* I: reset *) true
+ (* N: ? *) ndbo3 (* Z: ? *) ndbo4 (* C: ? *) ndbo5 (* IRQ: ? *) irqfl)
+ (* mem *) mem
+ (* chk *) chk
+ (* clk: reset *) (None ?).
+
+ndefinition start_of_mcu_version_HCS08 ≝
+λmcu:HCS08_mcu_model.λt:memory_impl.
+λmem:aux_mem_type t.λchk:aux_chk_type t.
+λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
+ let fetched_pc ≝ mk_word16 (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xE〉〉)
+ (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xF〉〉) in
+ mk_any_status HCS08 t
+ (mk_alu_HC08
+ (* acc_low: ? *) ndby1 (* indw_low: ? *) ndby2 (* indx_high: reset *) 〈x0,x0〉
+ (* sp: reset *) 〈〈x0,x0〉:〈xF,xF〉〉 (* pc: reset+fetch *) fetched_pc
+ (* V: ? *) ndbo1 (* H: ? *) ndbo2 (* I: reset *) true
+ (* N: ? *) ndbo3 (* Z: ? *) ndbo4 (* C: ? *) ndbo5 (* IRQ: ? *) irqfl)
+ (* mem *) mem
+ (* chk *) chk
+ (* clk: reset *) (None ?).
+
+ndefinition start_of_mcu_version_RS08 ≝
+λmcu:RS08_mcu_model.λt:memory_impl.
+λmem:aux_mem_type t.λchk:aux_chk_type t.
+λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
+ let build ≝ λpcm.
+ mk_any_status RS08 t
+ (mk_alu_RS08
+ (* acc_low: reset *) 〈x0,x0〉
+ (* pc: reset *) (and_w16 〈〈xF,xF〉:〈xF,xD〉〉 pcm) pcm
+ (* spc: reset *) (and_w16 〈〈xF,xF〉:〈xF,xD〉〉 pcm)
+ (* xm: reset *) 〈x0,x0〉 (* psm: *) 〈x8,x0〉
+ (* Z: reset *) false (* C: reset *) false)
+ (* mem *) mem
+ (* chk *) chk
+ (* clk: reset *) (None ?) in
+ (* tralascio l'enumerazione dei casi, tanto i valori sono uguali *)
+ build 〈〈x3,xF〉:〈xF,xF〉〉.
+
+(*
+ 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'
+*)
+ndefinition reset_of_mcu ≝
+λm:mcu_type.λt:memory_impl.
+let pc_reset_h ≝ 〈〈xF,xF〉:〈xF,xE〉〉 in
+let pc_reset_l ≝ 〈〈xF,xF〉:〈xF,xF〉〉 in
+let pc_RS08_reset ≝ 〈〈xF,xF〉:〈xF,xD〉〉 in
+let sp_reset ≝ 〈〈x0,x0〉:〈xF,xF〉〉 in
+ match m return λm:mcu_type.(any_status m t) → (any_status m t) with
+(* HC05: parzialmente non deterministico *)
+ [ HC05 ⇒ λs:any_status HC05 t.match s with
+ [ mk_any_status alu mem chk clk ⇒ match alu with
+ [ mk_alu_HC05 acclow indxlow _ spm spf _ pcm hfl _ nfl zfl cfl irqfl ⇒
+ let fetched_pc ≝ mk_word16 (mem_read_abs t mem (and_w16 pc_reset_h pcm))
+ (mem_read_abs t mem (and_w16 pc_reset_l pcm)) in
+ mk_any_status HC05 t
+ (mk_alu_HC05
+ (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow
+ (* sp: reset *) (or_w16 (and_w16 sp_reset spm) spf) spm spf
+ (* pc: reset+fetch *) (and_w16 fetched_pc pcm) pcm
+ (* H: inv. *) hfl (* I: reset *) true (* N: inv. *) nfl
+ (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
+ (* mem: inv. *) mem
+ (* chk: inv. *) chk
+ (* clk: reset *) (None ?) ]]
+(* HC08: parzialmente non deterministico *)
+ | HC08 ⇒ λs:any_status HC08 t.match s with
+ [ mk_any_status alu mem chk clk ⇒ match alu with
+ [ mk_alu_HC08 acclow indxlow _ _ _ vfl hfl _ nfl zfl cfl irqfl ⇒
+ let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
+ (mem_read_abs t mem pc_reset_l) in
+ mk_any_status HC08 t
+ (mk_alu_HC08
+ (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow (* indx_high: reset *) 〈x0,x0〉
+ (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
+ (* V: inv. *) vfl (* H: inv. *) hfl (* I: reset *) true
+ (* N: inv. *) nfl (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
+ (* mem: inv. *) mem
+ (* chk: inv. *) chk
+ (* clk: reset *) (None ?) ]]
+(* HCS08: parzialmente non deterministico *)
+ | HCS08 ⇒ λs:any_status HCS08 t.match s with
+ [ mk_any_status alu mem chk clk ⇒ match alu with
+ [ mk_alu_HC08 acclow indxlow _ _ _ vfl hfl _ nfl zfl cfl irqfl ⇒
+ let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
+ (mem_read_abs t mem pc_reset_l) in
+ mk_any_status HCS08 t
+ (mk_alu_HC08
+ (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow (* indx_high: reset *) 〈x0,x0〉
+ (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
+ (* V: inv. *) vfl (* H: inv. *) hfl (* I: reset *) true
+ (* N: inv. *) nfl (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
+ (* mem: inv. *) mem
+ (* chk: inv. *) chk
+ (* clk: reset *) (None ?) ]]
+(* RS08: deterministico *)
+ | RS08 ⇒ λs:any_status RS08 t.match s with
+ [ mk_any_status alu mem chk clk ⇒ match alu with
+ [ mk_alu_RS08 _ _ pcm _ _ _ _ _ ⇒
+ mk_any_status RS08 t
+ (mk_alu_RS08
+ (* acc_low: reset *) 〈x0,x0〉
+ (* pc: reset *) (and_w16 pc_RS08_reset pcm) pcm
+ (* spc: reset *) (and_w16 pc_RS08_reset pcm)
+ (* xm: reset *) 〈x0,x0〉 (* psm: reset *) 〈x8,x0〉
+ (* Z: reset *) false (* C: reset *) false)
+ (* mem: inv. *) mem
+ (* chk: inv. *) chk
+ (* clk: reset *) (None ?) ]]
+ ].
--- /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: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "freescale/load_write.ma".
+
+(* ************************************************ *)
+(* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *)
+(* ************************************************ *)
+
+(* NB: dentro il codice i commenti cercano di spiegare la logica
+ secondo quanto riportato dalle specifiche delle mcu *)
+
+(* NB: notare che tranne nei casi in cui PC viene modificato esplicitamente
+ il suo avanzamento viene delegato totalmente agli strati inferiori
+ I) avanzamento dovuto al decode degli op (fetch)
+ II) avanzamento dovuto al caricamento degli argomenti (multi_mode_load/write)
+ la modifica effettiva avviene poi centralizzata in tick *)
+
+(* A = [true] fAMC(A,M,C), [false] A *)
+(* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
+(* fAMC e' la logica da applicare: somma con/senza carry *)
+ndefinition execute_ADC_ADD_aux ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
+λfAMC:byte8 → byte8 → bool → ProdT byte8 bool.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
+ match fAMC A_op M_op (get_c_flag m t s_tmp1) with
+ [ pair R_op carry ⇒
+ let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
+ let A3 ≝ MSB_ex (b8l A_op) in let M3 ≝ MSB_ex (b8l M_op) in let R3 ≝ MSB_ex (b8l R_op) in
+ (* A = [true] fAMC(A,M,C), [false] A *)
+ let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
+ (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
+ (* C = A7&M7 | M7&nR7 | nR7&A7 *)
+ let s_tmp4 ≝ set_c_flag m t s_tmp3 ((A7⊗M7) ⊕ (M7⊗(⊖R7)) ⊕ ((⊖R7)⊗A7)) in
+ (* N = R7 *)
+ let s_tmp5 ≝ setweak_n_flag m t s_tmp4 R7 in
+ (* H = A3&M3 | M3&nR3 | nR3&A3 *)
+ let s_tmp6 ≝ setweak_h_flag m t s_tmp5 ((A3⊗M3) ⊕ (M3⊗(⊖R3)) ⊕ ((⊖R3)⊗A3)) in
+ (* V = A7&M7&nR7 | nA7&nM7&R7 *)
+ let s_tmp7 ≝ setweak_v_flag m t s_tmp6 ((A7⊗M7⊗(⊖R7)) ⊕ ((⊖A7)⊗(⊖M7)⊗R7)) in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp7 new_pc) ]]).
+
+(* A = [true] fAM(A,M), [false] A *)
+(* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
+(* fAM e' la logica da applicare: and/xor/or *)
+ndefinition execute_AND_BIT_EOR_ORA_aux ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
+λfAM:byte8 → byte8 → byte8.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ let R_op ≝ fAM (get_acc_8_low_reg m t s_tmp1) M_op in
+ (* A = [true] fAM(A,M), [false] A *)
+ let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
+ (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
+ (* N = R7 *)
+ let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
+ (* V = 0 *)
+ let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp5 new_pc) ]).
+
+(* M = fMC(M,C) *)
+(* fMC e' la logica da applicare: rc_/ro_/sh_ *)
+ndefinition execute_ASL_ASR_LSR_ROL_ROR_aux ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+λfMC:byte8 → bool → ProdT byte8 bool.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op _ ⇒
+ match fMC M_op (get_c_flag m t s_tmp1) with [ pair R_op carry ⇒
+ (* M = fMC(M,C) *)
+ opt_map … (multi_mode_write true m t s_tmp1 cur_pc i R_op)
+ (λS_PC.match S_PC with
+ [ pair s_tmp2 new_pc ⇒
+ (* C = carry *)
+ let s_tmp3 ≝ set_c_flag m t s_tmp2 carry in
+ (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp4 ≝ set_z_flag m t s_tmp3 (eq_b8 R_op 〈x0,x0〉) in
+ (* N = R7 *)
+ let s_tmp5 ≝ setweak_n_flag m t s_tmp4 (MSB_b8 R_op) in
+ (* V = R7 ⊙ carry *)
+ let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((MSB_b8 R_op) ⊙ carry) in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp6 new_pc) ])]]).
+
+(* estensione del segno byte → word *)
+ndefinition byte_extension ≝
+λb:byte8.〈match MSB_b8 b with [ true ⇒ 〈xF,xF〉 | false ⇒ 〈x0,x0〉 ]:b〉.
+
+(* branch con byte+estensione segno *)
+ndefinition branched_pc ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λb:byte8.
+ get_pc_reg m t (set_pc_reg m t s (plus_w16_d_d cur_pc (byte_extension b))).
+
+(* if COND=1 branch *)
+(* tutti i branch calcoleranno la condizione e la passeranno qui *)
+ndefinition execute_any_BRANCH ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:bool.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ (* if true, branch *)
+ match fCOND with
+ (* newpc = nextpc + rel *)
+ [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc M_op))
+ (* newpc = nextpc *)
+ | false ⇒ Some ? (pair … s_tmp1 new_pc) ]]).
+
+(* Mn = filtered optval *)
+(* il chiamante passa 0x00 per azzerare, 0xFF per impostare il bit di M *)
+ndefinition execute_BCLRn_BSETn_aux ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λoptval:byte8.
+ (* Mn = filtered optval *)
+ opt_map … (multi_mode_write true m t s cur_pc i optval)
+ (λS_PC.match S_PC with
+ (* newpc = nextpc *)
+ [ pair s_tmp1 new_pc ⇒ Some ? (pair … s_tmp1 new_pc) ]).
+
+(* if COND(Mn) branch *)
+(* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
+ndefinition execute_BRCLRn_BRSETn_aux ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:byte8 → bool.
+ opt_map … (multi_mode_load false m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒ match M_op with
+ [ mk_word16 MH_op ML_op ⇒
+ (* if COND(Mn) branch *)
+ match fCOND MH_op with
+ (* newpc = nextpc + rel *)
+ [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
+ (* newpc = nextpc *)
+ | false ⇒ Some ? (pair … s_tmp1 new_pc) ]]]).
+
+(* M = fM(M) *)
+(* fM e' la logica da applicare: not/neg/++/-- *)
+ndefinition execute_COM_DEC_INC_NEG_aux ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+λfM:byte8 → byte8.λfV:bool → bool → bool.λfC:bool → byte8 → bool.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op _ ⇒
+ let R_op ≝ fM M_op in
+ (* M = fM(M) *)
+ opt_map … (multi_mode_write true m t s_tmp1 cur_pc i R_op)
+ (λS_PC.match S_PC with
+ [ pair s_tmp2 new_pc ⇒
+ (* C = fCR (C,R) *)
+ let s_tmp3 ≝ set_c_flag m t s_tmp2 (fC (get_c_flag m t s_tmp2) R_op) in
+ (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp4 ≝ set_z_flag m t s_tmp3 (eq_b8 R_op 〈x0,x0〉) in
+ (* N = R7 *)
+ let s_tmp5 ≝ setweak_n_flag m t s_tmp4 (MSB_b8 R_op) in
+ (* V = fV (M7,R7) *)
+ let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (fV (MSB_b8 M_op) (MSB_b8 R_op)) in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp6 new_pc) ])]).
+
+(* A = [true] fAMC(A,M,C), [false] A *)
+(* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
+(* fAMC e' la logica da applicare: sottrazione con/senza carry *)
+ndefinition execute_SBC_SUB_aux ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
+λfAMC:byte8 → byte8 → bool → ProdT byte8 bool.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
+ match fAMC A_op M_op (get_c_flag m t s_tmp1) with
+ [ pair R_op carry ⇒
+ let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
+ (* A = [true] fAMC(A,M,C), [false] A *)
+ let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
+ (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
+ (* C = nA7&M7 | M7&R7 | R7&nA7 *)
+ let s_tmp4 ≝ set_c_flag m t s_tmp3 (((⊖A7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖A7))) in
+ (* N = R7 *)
+ let s_tmp5 ≝ setweak_n_flag m t s_tmp4 R7 in
+ (* V = A7&nM7&nR7 | nA7&M7&R7 *)
+ let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((A7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖A7)⊗M7⊗R7)) in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp6 new_pc) ]]).
+
+(* il classico push *)
+ndefinition aux_push ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
+ opt_map … (get_sp_reg m t s)
+ (* [SP] = val *)
+ (λSP_op.opt_map … (memory_filter_write m t s SP_op val)
+ (* SP -- *)
+ (λs_tmp1.opt_map … (set_sp_reg m t s_tmp1 (pred_w16 SP_op))
+ (λs_tmp2.Some ? s_tmp2))).
+
+(* il classico pop *)
+(* NB: l'incremento di SP deve essere filtrato dalla ALU, quindi get(set(SP)) *)
+ndefinition aux_pop ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ opt_map … (get_sp_reg m t s)
+ (* SP ++ *)
+ (λSP_op.opt_map … (set_sp_reg m t s (succ_w16 SP_op))
+ (λs_tmp1.opt_map … (get_sp_reg m t s_tmp1)
+ (* val = [SP] *)
+ (λSP_op'.opt_map … (memory_filter_read m t s_tmp1 SP_op')
+ (λval.Some ? (pair … s_tmp1 val))))).
+
+(* CCR corrisponde a V11HINZC e cmq 1 se un flag non esiste *)
+(* i flag mantengono posizione costante nelle varie ALU, e se non sono
+ implementati corrispondono a 1 *)
+ndefinition aux_get_CCR ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+let V_comp ≝ match get_v_flag m t s with
+ [ None ⇒ 〈x8,x0〉 | Some V_val ⇒ match V_val with [ true ⇒ 〈x8,x0〉 | false ⇒ 〈x0,x0〉 ]] in
+let H_comp ≝ match get_h_flag m t s with
+ [ None ⇒ 〈x1,x0〉 | Some H_val ⇒ match H_val with [ true ⇒ 〈x1,x0〉 | false ⇒ 〈x0,x0〉 ]] in
+let I_comp ≝ match get_i_flag m t s with
+ [ None ⇒ 〈x0,x8〉 | Some I_val ⇒ match I_val with [ true ⇒ 〈x0,x8〉 | false ⇒ 〈x0,x0〉 ]] in
+let N_comp ≝ match get_n_flag m t s with
+ [ None ⇒ 〈x0,x4〉 | Some N_val ⇒ match N_val with [ true ⇒ 〈x0,x4〉 | false ⇒ 〈x0,x0〉 ]] in
+let Z_comp ≝ match get_z_flag m t s with
+ [ true ⇒ 〈x0,x2〉 | false ⇒ 〈x0,x0〉 ] in
+let C_comp ≝ match get_c_flag m t s with
+ [ true ⇒ 〈x0,x1〉 | false ⇒ 〈x0,x0〉 ] in
+or_b8 〈x6,x0〉 (or_b8 V_comp (or_b8 H_comp (or_b8 I_comp (or_b8 N_comp (or_b8 Z_comp C_comp))))).
+
+(* CCR corrisponde a V11HINZC *)
+(* i flag mantengono posizione costante nelle varie ALU, e se non sono
+ implementati si puo' usare tranquillamente setweak *)
+ndefinition aux_set_CCR ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λCCR:byte8.
+ let s_tmp1 ≝ set_c_flag m t s (eq_b8 〈x0,x1〉 (and_b8 〈x0,x1〉 CCR)) in
+ let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 〈x0,x2〉 (and_b8 〈x0,x2〉 CCR)) in
+ let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (eq_b8 〈x0,x4〉 (and_b8 〈x0,x4〉 CCR)) in
+ let s_tmp4 ≝ setweak_i_flag m t s_tmp3 (eq_b8 〈x0,x8〉 (and_b8 〈x0,x8〉 CCR)) in
+ let s_tmp5 ≝ setweak_h_flag m t s_tmp4 (eq_b8 〈x1,x0〉 (and_b8 〈x1,x0〉 CCR)) in
+ let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (eq_b8 〈x8,x0〉 (and_b8 〈x8,x0〉 CCR)) in
+ s_tmp6.
+
+(* **************** *)
+(* LOGICA DELLA ALU *)
+(* **************** *)
+
+(* A = A + M + C *)
+ndefinition execute_ADC ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_ADC_ADD_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8_dc_dc A_op M_op C_op).
+
+(* A = A + M *)
+ndefinition execute_ADD ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_ADC_ADD_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8_dc_dc A_op M_op false).
+
+(* SP += extended M *)
+ndefinition execute_AIS ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ opt_map … (get_sp_reg m t s_tmp1)
+ (* SP += extended M *)
+ (λSP_op.opt_map … (set_sp_reg m t s_tmp1 (plus_w16_d_d SP_op (byte_extension M_op)))
+ (λs_tmp2.Some ? (pair … s_tmp2 new_pc))) ]).
+
+(* H:X += extended M *)
+ndefinition execute_AIX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ opt_map … (get_indX_16_reg m t s_tmp1)
+ (* H:X += extended M *)
+ (λHX_op.opt_map … (set_indX_16_reg m t s_tmp1 (plus_w16_d_d HX_op (byte_extension M_op)))
+ (λs_tmp2.Some ? (pair … s_tmp2 new_pc))) ]).
+
+(* A = A & M *)
+ndefinition execute_AND ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true and_b8.
+
+(* M = C' <- rcl M <- 0 *)
+ndefinition execute_ASL ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcl_b8 M_op false).
+
+(* M = M7 -> rcr M -> C' *)
+ndefinition execute_ASR ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op (MSB_b8 M_op)).
+
+(* if C=0, branch *)
+ndefinition execute_BCC ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_any_BRANCH m t s i cur_pc (⊖(get_c_flag m t s)).
+
+(* Mn = 0 *)
+ndefinition execute_BCLRn ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_BCLRn_BSETn_aux m t s i cur_pc 〈x0,x0〉.
+
+(* if C=1, branch *)
+ndefinition execute_BCS ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_any_BRANCH m t s i cur_pc (get_c_flag m t s).
+
+(* if Z=1, branch *)
+ndefinition execute_BEQ ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_any_BRANCH m t s i cur_pc (get_z_flag m t s).
+
+(* if N⊙V=0, branch *)
+ndefinition execute_BGE ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_n_flag m t s)
+ (λN_op.opt_map … (get_v_flag m t s)
+ (λV_op.execute_any_BRANCH m t s i cur_pc (⊖(N_op ⊙ V_op)))).
+
+(* BGND mode *)
+ndefinition execute_BGND ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ Some ? (pair … s cur_pc).
+
+(* if Z|N⊙V=0, branch *)
+ndefinition execute_BGT ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_n_flag m t s)
+ (λN_op.opt_map … (get_v_flag m t s)
+ (λV_op.execute_any_BRANCH m t s i cur_pc (⊖((get_z_flag m t s) ⊕ (N_op ⊙ V_op))))).
+
+(* if H=0, branch *)
+ndefinition execute_BHCC ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_h_flag m t s)
+ (λH_op.execute_any_BRANCH m t s i cur_pc (⊖H_op)).
+
+(* if H=1, branch *)
+ndefinition execute_BHCS ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_h_flag m t s)
+ (λH_op.execute_any_BRANCH m t s i cur_pc H_op).
+
+(* if C|Z=0, branch *)
+ndefinition execute_BHI ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_any_BRANCH m t s i cur_pc (⊖((get_c_flag m t s) ⊕ (get_z_flag m t s))).
+
+(* if nIRQ=1, branch NB: irqflag e' un negato del pin *)
+ndefinition execute_BIH ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_irq_flag m t s)
+ (λIRQ_op.execute_any_BRANCH m t s i cur_pc (⊖IRQ_op)).
+
+(* if nIRQ=0, branch NB: irqflag e' un negato del pin *)
+ndefinition execute_BIL ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_irq_flag m t s)
+ (λIRQ_op.execute_any_BRANCH m t s i cur_pc IRQ_op).
+
+(* flags = A & M *)
+ndefinition execute_BIT ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_AND_BIT_EOR_ORA_aux m t s i cur_pc false and_b8.
+
+(* if Z|N⊙V=1, branch *)
+ndefinition execute_BLE ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_n_flag m t s)
+ (λN_op.opt_map … (get_v_flag m t s)
+ (λV_op.execute_any_BRANCH m t s i cur_pc ((get_z_flag m t s) ⊕ (N_op ⊙ V_op)))).
+
+(* if C|Z=1, branch *)
+ndefinition execute_BLS ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_any_BRANCH m t s i cur_pc ((get_c_flag m t s) ⊕ (get_z_flag m t s)).
+
+(* if N⊙V=1, branch *)
+ndefinition execute_BLT ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_n_flag m t s)
+ (λN_op.opt_map … (get_v_flag m t s)
+ (λV_op.execute_any_BRANCH m t s i cur_pc (N_op ⊙ V_op))).
+
+(* if I=0, branch *)
+ndefinition execute_BMC ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_i_flag m t s)
+ (λI_op.execute_any_BRANCH m t s i cur_pc (⊖I_op)).
+
+(* if N=1, branch *)
+ndefinition execute_BMI ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_n_flag m t s)
+ (λN_op.execute_any_BRANCH m t s i cur_pc N_op).
+
+(* if I=1, branch *)
+ndefinition execute_BMS ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_i_flag m t s)
+ (λI_op.execute_any_BRANCH m t s i cur_pc I_op).
+
+(* if Z=0, branch *)
+ndefinition execute_BNE ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_any_BRANCH m t s i cur_pc (⊖(get_z_flag m t s)).
+
+(* if N=0, branch *)
+ndefinition execute_BPL ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_n_flag m t s)
+ (λN_op.execute_any_BRANCH m t s i cur_pc (⊖N_op)).
+
+(* branch always *)
+ndefinition execute_BRA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_any_BRANCH m t s i cur_pc true.
+
+(* if Mn=0 branch *)
+ndefinition execute_BRCLRn ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_BRCLRn_BRSETn_aux m t s i cur_pc
+ (λMn_op.eq_b8 Mn_op 〈x0,x0〉).
+
+(* branch never... come se fosse un nop da 2 byte *)
+ndefinition execute_BRN ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_any_BRANCH m t s i cur_pc false.
+
+(* if Mn=1 branch *)
+ndefinition execute_BRSETn ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_BRCLRn_BRSETn_aux m t s i cur_pc
+ (λMn_op.⊖(eq_b8 Mn_op 〈x0,x0〉)).
+
+(* Mn = 1 *)
+ndefinition execute_BSETn ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_BCLRn_BSETn_aux m t s i cur_pc 〈xF,xF〉.
+
+(* branch to subroutine *)
+(* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
+ndefinition execute_BSR ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t .λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒ let aux ≝
+ (* push (new_pc low) *)
+ opt_map … (aux_push m t s_tmp1 (w16l new_pc))
+ (* push (new_pc high) *)
+ (λs_tmp2.opt_map … (aux_push m t s_tmp2 (w16h new_pc))
+ (* new_pc = new_pc + rel *)
+ (λs_tmp3.Some ? (pair … s_tmp3 (branched_pc m t s_tmp3 new_pc M_op))))
+ in match m with
+ [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
+ | RS08 ⇒
+ (* SPC = new_pc *)
+ opt_map … (set_spc_reg m t s_tmp1 new_pc)
+ (* new_pc = new_pc + rel *)
+ (λs_tmp2.Some ? (pair … s_tmp2 (branched_pc m t s_tmp2 new_pc M_op)))
+ ]]).
+
+(* if A=M, branch *)
+ndefinition execute_CBEQA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load false m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ match M_op with
+ [ mk_word16 MH_op ML_op ⇒
+ (* if A=M, branch *)
+ match eq_b8 (get_acc_8_low_reg m t s_tmp1) MH_op with
+ (* new_pc = new_pc + rel *)
+ [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
+ (* new_pc = new_pc *)
+ | false ⇒ Some ? (pair … s_tmp1 new_pc)
+ ]]]).
+
+(* if X=M, branch *)
+ndefinition execute_CBEQX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load false m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ match M_op with
+ [ mk_word16 MH_op ML_op ⇒
+ opt_map … (get_indX_8_low_reg m t s_tmp1)
+ (* if X=M, branch *)
+ (λX_op.match eq_b8 X_op MH_op with
+ (* new_pc = new_pc + rel *)
+ [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
+ (* new_pc = new_pc *)
+ | false ⇒ Some ? (pair … s_tmp1 new_pc)
+ ])]]).
+
+(* C = 0 *)
+ndefinition execute_CLC ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ Some ? (pair … (set_c_flag m t s false) cur_pc).
+
+(* I = 0 *)
+ndefinition execute_CLI ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (set_i_flag m t s false)
+ (λs_tmp.Some ? (pair … s_tmp cur_pc)).
+
+(* M = 0 *)
+ndefinition execute_CLR ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ (* M = 0 *)
+ opt_map … (multi_mode_write true m t s cur_pc i 〈x0,x0〉)
+ (λS_PC.match S_PC with
+ [ pair s_tmp1 new_pc ⇒
+ (* Z = 1 *)
+ let s_tmp2 ≝ set_z_flag m t s_tmp1 true in
+ (* N = 0 *)
+ let s_tmp3 ≝ setweak_n_flag m t s_tmp2 false in
+ (* V = 0 *)
+ let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp4 new_pc) ]).
+
+(* flags = A - M *)
+ndefinition execute_CMP ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_SBC_SUB_aux m t s i cur_pc false (λA_op.λM_op.λC_op.plus_b8_dc_dc A_op (compl_b8 M_op) false).
+
+(* M = not M *)
+ndefinition execute_COM ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_COM_DEC_INC_NEG_aux m t s i cur_pc not_b8
+ (* fV = 0 *)
+ (λM7.λR7.false)
+ (* fC = 1 *)
+ (λC_op.λR_op.true).
+
+(* flags = H:X - M *)
+ndefinition execute_CPHX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load false m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ opt_map … (get_indX_16_reg m t s_tmp1)
+ (λX_op.
+ match plus_w16_dc_dc X_op (compl_w16 M_op) false with
+ [ pair R_op carry ⇒
+ let X15 ≝ MSB_w16 X_op in let M15 ≝ MSB_w16 M_op in let R15 ≝ MSB_w16 R_op in
+ (* Z = nR15&nR14&nR13&nR12&nR11&nR10&nR9&nR8&nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 R_op 〈〈x0,x0〉:〈x0,x0〉〉) in
+ (* C = nX15&M15 | M15&R15 | R15&nX15 *)
+ let s_tmp3 ≝ set_c_flag m t s_tmp2 (((⊖X15)⊗M15) ⊕ (M15⊗R15) ⊕ (R15⊗(⊖X15))) in
+ (* N = R15 *)
+ let s_tmp4 ≝ setweak_n_flag m t s_tmp3 R15 in
+ (* V = X15&nM15&nR15 | nX15&M15&R15 *)
+ let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X15⊗(⊖M15)⊗(⊖R15)) ⊕ ((⊖X15)⊗M15⊗R15)) in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp5 new_pc) ] ) ]).
+
+(* flags = X - M *)
+ndefinition execute_CPX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ opt_map … (get_indX_8_low_reg m t s_tmp1)
+ (λX_op.
+ match plus_b8_dc_dc X_op (compl_b8 M_op) false with
+ [ pair R_op carry ⇒
+ let X7 ≝ MSB_b8 X_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
+ (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 R_op 〈x0,x0〉) in
+ (* C = nX7&M7 | M7&R7 | R7&nX7 *)
+ let s_tmp3 ≝ set_c_flag m t s_tmp2 (((⊖X7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖X7))) in
+ (* N = R7 *)
+ let s_tmp4 ≝ setweak_n_flag m t s_tmp3 R7 in
+ (* V = X7&nM7&nR7 | nX7&M7&R7 *)
+ let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖X7)⊗M7⊗R7)) in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp5 new_pc) ] ) ]).
+
+(* decimal adjiust A *)
+(* per i dettagli vedere daa_b8 (modulo byte8) *)
+ndefinition execute_DAA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_h_flag m t s)
+ (λH.
+ let M_op ≝ get_acc_8_low_reg m t s in
+ match daa_b8 H (get_c_flag m t s) M_op with
+ [ pair R_op carry ⇒
+ (* A = R *)
+ let s_tmp1 ≝ set_acc_8_low_reg m t s R_op in
+ (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 R_op 〈x0,x0〉) in
+ (* C = carry *)
+ let s_tmp3 ≝ set_c_flag m t s_tmp2 carry in
+ (* N = R7 *)
+ let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
+ (* V = M7 ⊙ R7 *)
+ let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((MSB_b8 M_op) ⊙ (MSB_b8 R_op)) in
+ (* newpc = curpc *)
+ Some ? (pair … s_tmp5 cur_pc) ]).
+
+(* if (--M)≠0, branch *)
+ndefinition execute_DBNZ ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load false m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ match M_op with
+ [ mk_word16 MH_op ML_op ⇒
+ (* --M *)
+ let MH_op' ≝ pred_b8 MH_op in
+ opt_map … (multi_mode_write true m t s_tmp1 cur_pc i MH_op')
+ (λS_PC.match S_PC with
+ [ pair s_tmp2 _ ⇒
+ (* if (--M)≠0, branch *)
+ match eq_b8 MH_op' 〈x0,x0〉 with
+ (* new_pc = new_pc *)
+ [ true ⇒ Some ? (pair … s_tmp2 new_pc)
+ (* new_pc = new_pc + rel *)
+ | false ⇒ Some ? (pair … s_tmp2 (branched_pc m t s_tmp2 new_pc ML_op)) ]])]]).
+
+(* M = M - 1 *)
+ndefinition execute_DEC ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_COM_DEC_INC_NEG_aux m t s i cur_pc pred_b8
+ (* fV = M7&nR7 *)
+ (λM7.λR7.M7⊗(⊖R7))
+ (* fC = C *)
+ (λC_op.λR_op.C_op).
+
+(* A = H:A/X, H = H:AmodX se non c'e' overflow, altrimenti invariati *)
+(* per i dettagli vedere div_b8 (modulo word16) *)
+ndefinition execute_DIV ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_indX_8_high_reg m t s)
+ (λH_op.opt_map … (get_indX_8_low_reg m t s)
+ (λX_op.match div_b8 〈H_op:(get_acc_8_low_reg m t s)〉 X_op with
+ [ triple quoz rest overflow ⇒
+ (* C = overflow *)
+ let s_tmp1 ≝ set_c_flag m t s overflow in
+ (* A = A o H:A/X *)
+ let s_tmp2 ≝ match overflow with
+ [ true ⇒ s_tmp1
+ | false ⇒ set_acc_8_low_reg m t s_tmp1 quoz ] in
+ (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
+ (* NB: che A sia cambiato o no, lo testa *)
+ let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 (get_acc_8_low_reg m t s_tmp2) 〈x0,x0〉) in
+ (* H = H o H:AmodX *)
+ opt_map … (match overflow with
+ [ true ⇒ Some ? s_tmp3
+ | false ⇒ set_indX_8_high_reg m t s_tmp3 rest])
+ (λs_tmp4.Some ? (pair … s_tmp4 cur_pc)) ])).
+
+(* A = A ⊙ M *)
+ndefinition execute_EOR ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true xor_b8.
+
+(* M = M + 1 *)
+ndefinition execute_INC ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_COM_DEC_INC_NEG_aux m t s i cur_pc succ_b8
+ (* fV = nM7&R7 *)
+ (λM7.λR7.(⊖M7)⊗R7)
+ (* fC = C *)
+ (λC_op.λR_op.C_op).
+
+(* jmp, il nuovo indirizzo e' una WORD *)
+ndefinition execute_JMP ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load false m t s cur_pc i)
+ (λS_M_PC.
+ (* newpc = M_op *)
+ Some ? (pair … (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
+
+(* jump to subroutine *)
+(* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
+ndefinition execute_JSR ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load false m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒ let aux ≝
+ (* push (new_pc low) *)
+ opt_map … (aux_push m t s_tmp1 (w16l new_pc))
+ (* push (new_pc high) *)
+ (λs_tmp2.opt_map … (aux_push m t s_tmp2 (w16h new_pc))
+ (* newpc = M_op *)
+ (λs_tmp3.Some ? (pair … s_tmp3 M_op)))
+ in match m with
+ [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
+ | RS08 ⇒
+ (* SPC = new_pc *)
+ opt_map … (set_spc_reg m t s_tmp1 new_pc)
+ (* newpc = M_op *)
+ (λs_tmp2.Some ? (pair … s_tmp2 M_op))
+ ]]).
+
+(* A = M *)
+ndefinition execute_LDA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ (* A = M *)
+ let s_tmp2 ≝ set_acc_8_low_reg m t s_tmp1 M_op in
+ (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 M_op 〈x0,x0〉) in
+ (* N = R7 *)
+ let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 M_op) in
+ (* V = 0 *)
+ let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp5 new_pc) ]).
+
+(* H:X = M *)
+ndefinition execute_LDHX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load false m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ opt_map … (set_indX_16_reg m t s_tmp1 M_op)
+ (λs_tmp2.
+ (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_w16 M_op 〈〈x0,x0〉:〈x0,x0〉〉) in
+ (* N = R15 *)
+ let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_w16 M_op) in
+ (* V = 0 *)
+ let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp5 new_pc)) ]).
+
+(* X = M *)
+ndefinition execute_LDX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ opt_map … (set_indX_8_low_reg m t s_tmp1 M_op)
+ (λs_tmp2.
+ (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 M_op 〈x0,x0〉) in
+ (* N = R7 *)
+ let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 M_op) in
+ (* V = 0 *)
+ let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp5 new_pc)) ]).
+
+(* M = 0 -> rcr M -> C' *)
+ndefinition execute_LSR ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op false).
+
+(* M2 = M1 *)
+ndefinition execute_MOV ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ (* R_op = M1 *)
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_R_PC.match S_R_PC with
+ [ triple s_tmp1 R_op tmp_pc ⇒
+ (* M2 = R_op *)
+ opt_map … (multi_mode_write true m t s_tmp1 tmp_pc i R_op)
+ (λS_PC.match S_PC with
+ [ pair s_tmp2 new_pc ⇒
+ (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
+ (* N = R7 *)
+ let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
+ (* V = 0 *)
+ let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp5 new_pc)])]).
+
+(* X:A = X * A *)
+ndefinition execute_MUL ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_indX_8_low_reg m t s)
+ (λX_op.let R_op ≝ mul_b8 X_op (get_acc_8_low_reg m t s) in
+ opt_map … (set_indX_8_low_reg m t s (w16h R_op))
+ (λs_tmp.Some ? (pair … (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
+
+(* M = compl M *)
+ndefinition execute_NEG ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_COM_DEC_INC_NEG_aux m t s i cur_pc compl_b8
+ (* fV = M7&R7 *)
+ (λM7.λR7.M7⊗R7)
+ (* fC = R7|R6|R5|R4|R3|R2|R1|R0 *)
+ (λC_op.λR_op.⊖(eq_b8 R_op 〈x0,x0〉)).
+
+(* nulla *)
+ndefinition execute_NOP ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ Some ? (pair … s cur_pc).
+
+(* A = (mk_byte8 (b8l A) (b8h A)) *)
+(* cioe' swap del nibble alto/nibble basso di A *)
+ndefinition execute_NSA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ match get_acc_8_low_reg m t s with [ mk_byte8 ah al ⇒
+ (* A = (mk_byte8 (b8l A) (b8h A)) *)
+ Some ? (pair … (set_acc_8_low_reg m t s 〈al,ah〉) cur_pc) ].
+
+(* A = A | M *)
+ndefinition execute_ORA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true or_b8.
+
+(* push A *)
+ndefinition execute_PSHA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (aux_push m t s (get_acc_8_low_reg m t s))
+ (λs_tmp1.Some ? (pair … s_tmp1 cur_pc)).
+
+(* push H *)
+ndefinition execute_PSHH ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_indX_8_high_reg m t s)
+ (λH_op.opt_map … (aux_push m t s H_op)
+ (λs_tmp1.Some ? (pair … s_tmp1 cur_pc))).
+
+(* push X *)
+ndefinition execute_PSHX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_indX_8_low_reg m t s)
+ (λH_op.opt_map … (aux_push m t s H_op)
+ (λs_tmp1.Some ? (pair … s_tmp1 cur_pc))).
+
+(* pop A *)
+ndefinition execute_PULA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (aux_pop m t s)
+ (λS_and_A.match S_and_A with [ pair s_tmp1 A_op ⇒
+ Some ? (pair … (set_acc_8_low_reg m t s_tmp1 A_op) cur_pc) ]).
+
+(* pop H *)
+ndefinition execute_PULH ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (aux_pop m t s)
+ (λS_and_H.match S_and_H with [ pair s_tmp1 H_op ⇒
+ opt_map … (set_indX_8_high_reg m t s_tmp1 H_op)
+ (λs_tmp2.Some ? (pair … s_tmp2 cur_pc))]).
+
+(* pop X *)
+ndefinition execute_PULX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (aux_pop m t s)
+ (λS_and_X.match S_and_X with [ pair s_tmp1 X_op ⇒
+ opt_map … (set_indX_8_low_reg m t s_tmp1 X_op)
+ (λs_tmp2.Some ? (pair … s_tmp2 cur_pc))]).
+
+(* M = C' <- rcl M <- C *)
+ndefinition execute_ROL ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcl_b8 M_op C_op).
+
+(* M = C -> rcr M -> C' *)
+ndefinition execute_ROR ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op C_op).
+
+(* SP = 0xuuFF *)
+(* lascia inalterato il byte superiore di SP *)
+ndefinition execute_RSP ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_sp_reg m t s)
+ (λSP_op.match SP_op with [ mk_word16 sph spl ⇒
+ opt_map … (set_sp_reg m t s 〈sph:〈xF,xF〉〉)
+ (λs_tmp.Some ? (pair … s_tmp cur_pc))]).
+
+(* return from interrupt *)
+ndefinition execute_RTI ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ (* pop (CCR) *)
+ opt_map … (aux_pop m t s)
+ (λS_and_CCR.match S_and_CCR with [ pair s_tmp1 CCR_op ⇒
+ let s_tmp2 ≝ aux_set_CCR m t s_tmp1 CCR_op in
+ (* pop (A) *)
+ opt_map … (aux_pop m t s_tmp2)
+ (λS_and_A.match S_and_A with [ pair s_tmp3 A_op ⇒
+ let s_tmp4 ≝ set_acc_8_low_reg m t s_tmp3 A_op in
+ (* pop (X) *)
+ opt_map … (aux_pop m t s_tmp4)
+ (λS_and_X.match S_and_X with [ pair s_tmp5 X_op ⇒
+ opt_map … (set_indX_8_low_reg m t s_tmp5 X_op)
+ (* pop (PC high) *)
+ (λs_tmp6.opt_map … (aux_pop m t s_tmp6)
+ (λS_and_PCH.match S_and_PCH with [ pair s_tmp7 PCH_op ⇒
+ (* pop (PC low) *)
+ opt_map … (aux_pop m t s_tmp7)
+ (λS_and_PCL.match S_and_PCL with [ pair s_tmp8 PCL_op ⇒
+ Some ? (pair … s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
+
+(* return from subroutine *)
+(* HC05/HC08/HCS08 si appoggia allo stack, RS08 si appoggia a SPC *)
+ndefinition execute_RTS ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ let aux ≝
+ (* pop (PC high) *)
+ opt_map … (aux_pop m t s)
+ (λS_and_PCH.match S_and_PCH with [ pair s_tmp1 PCH_op ⇒
+ (* pop (PC low) *)
+ opt_map … (aux_pop m t s_tmp1)
+ (λS_and_PCL.match S_and_PCL with [ pair s_tmp2 PCL_op ⇒
+ Some ? (pair … s_tmp2 〈PCH_op:PCL_op〉)])])
+ in match m with
+ [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
+ | RS08 ⇒
+ (* new_pc = SPC *)
+ opt_map … (get_spc_reg m t s)
+ (λSPC_op.Some ? (pair … s SPC_op))
+ ].
+
+(* A = A - M - C *)
+ndefinition execute_SBC ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_SBC_SUB_aux m t s i cur_pc true
+ (λA_op.λM_op.λC_op.match plus_b8_dc_dc A_op (compl_b8 M_op) false with
+ [ pair resb resc ⇒ match C_op with
+ [ true ⇒ plus_b8_dc_dc resb 〈xF,xF〉 false
+ | false ⇒ pair … resb resc ]]).
+
+(* C = 1 *)
+ndefinition execute_SEC ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ Some ? (pair … (set_c_flag m t s true) cur_pc).
+
+(* I = 1 *)
+ndefinition execute_SEI ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (set_i_flag m t s true)
+ (λs_tmp.Some ? (pair … s_tmp cur_pc)).
+
+(* swap SPCh,A *)
+(* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
+ fare subroutine annidate se RA (return address) e' salvato sempre in SPC?
+ occore accedere a SPC e salvarne il contenuto *)
+ndefinition execute_SHA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_spc_reg m t s)
+ (λSPC_op.opt_map … (set_spc_reg m t s 〈(get_acc_8_low_reg m t s):(w16l SPC_op)〉)
+ (λs_tmp1.Some ? (pair … (set_acc_8_low_reg m t s_tmp1 (w16h SPC_op)) cur_pc))).
+
+(* swap SPCl,A *)
+(* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
+ fare subroutine annidate se RA (return address) e' salvato sempre in SPC?
+ occore accedere a SPC e salvarne il contenuto *)
+ndefinition execute_SLA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_spc_reg m t s)
+ (λSPC_op.opt_map … (set_spc_reg m t s 〈(w16h SPC_op):(get_acc_8_low_reg m t s)〉)
+ (λs_tmp1.Some ? (pair … (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
+
+(* M = A *)
+ndefinition execute_STA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ (* M = A *)
+ let A_op ≝ (get_acc_8_low_reg m t s) in
+ opt_map … (multi_mode_write true m t s cur_pc i A_op)
+ (λS_op_and_PC.match S_op_and_PC with
+ [ pair s_tmp1 new_pc ⇒
+ (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
+ let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 A_op 〈x0,x0〉) in
+ (* N = A7 *)
+ let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 A_op) in
+ (* V = 0 *)
+ let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp4 new_pc) ]).
+
+(* M = H:X *)
+ndefinition execute_STHX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ (* M = H:X *)
+ opt_map … (get_indX_16_reg m t s)
+ (λX_op.opt_map … (multi_mode_write false m t s cur_pc i X_op)
+ (λS_op_and_PC.match S_op_and_PC with
+ [ pair s_tmp1 new_pc ⇒
+ (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 X_op 〈〈x0,x0〉:〈x0,x0〉〉) in
+ (* N = R15 *)
+ let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_w16 X_op) in
+ (* V = 0 *)
+ let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp4 new_pc) ])).
+
+(* I = 0 *)
+ndefinition execute_STOP ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ Some ? (pair … (setweak_i_flag m t s false) cur_pc).
+
+(* M = X *)
+ndefinition execute_STX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ (* M = X *)
+ opt_map … (get_indX_8_low_reg m t s)
+ (λX_op.opt_map … (multi_mode_write true m t s cur_pc i X_op)
+ (λS_op_and_PC.match S_op_and_PC with
+ [ pair s_tmp1 new_pc ⇒
+ (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 X_op 〈x0,x0〉) in
+ (* N = R7 *)
+ let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 X_op) in
+ (* V = 0 *)
+ let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp4 new_pc) ])).
+
+(* A = A - M *)
+ndefinition execute_SUB ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ execute_SBC_SUB_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8_dc_dc A_op (compl_b8 M_op) false).
+
+(* software interrupt *)
+ndefinition execute_SWI ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ (* indirizzo da cui caricare il nuovo pc *)
+ let vector ≝ get_pc_reg m t (set_pc_reg m t s 〈〈xF,xF〉:〈xF,xC〉〉) in
+ (* push (cur_pc low) *)
+ opt_map … (aux_push m t s (w16l cur_pc))
+ (* push (cur_pc high *)
+ (λs_tmp1.opt_map … (aux_push m t s_tmp1 (w16h cur_pc))
+ (λs_tmp2.opt_map … (get_indX_8_low_reg m t s_tmp2)
+ (* push (X) *)
+ (λX_op.opt_map … (aux_push m t s_tmp2 X_op)
+ (* push (A) *)
+ (λs_tmp3.opt_map … (aux_push m t s_tmp3 (get_acc_8_low_reg m t s_tmp3))
+ (* push (CCR) *)
+ (λs_tmp4.opt_map … (aux_push m t s_tmp4 (aux_get_CCR m t s_tmp4))
+ (* I = 1 *)
+ (λs_tmp5.opt_map … (set_i_flag m t s_tmp5 true)
+ (* load from vector high *)
+ (λs_tmp6.opt_map … (memory_filter_read m t s_tmp6 vector)
+ (* load from vector low *)
+ (λaddrh.opt_map … (memory_filter_read m t s_tmp6 (succ_w16 vector))
+ (* newpc = [vector] *)
+ (λaddrl.Some ? (pair … s_tmp6 〈addrh:addrl〉)))))))))).
+
+(* flags = A *)
+ndefinition execute_TAP ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ Some ? (pair … (aux_set_CCR m t s (get_acc_8_low_reg m t s)) cur_pc).
+
+(* X = A *)
+ndefinition execute_TAX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (set_indX_8_low_reg m t s (get_acc_8_low_reg m t s))
+ (λs_tmp.Some ? (pair … s_tmp cur_pc)).
+
+(* A = flags *)
+ndefinition execute_TPA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ Some ? (pair … (set_acc_8_low_reg m t s (aux_get_CCR m t s)) cur_pc).
+
+(* flags = M - 0 *)
+(* implementata senza richiamare la sottrazione, la modifica dei flag
+ e' immediata *)
+ndefinition execute_TST ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (multi_mode_load true m t s cur_pc i)
+ (λS_M_PC.match S_M_PC with
+ [ triple s_tmp1 M_op new_pc ⇒
+ (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
+ let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 M_op 〈x0,x0〉) in
+ (* N = R7 *)
+ let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 M_op) in
+ (* V = 0 *)
+ let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
+ (* newpc = nextpc *)
+ Some ? (pair … s_tmp4 new_pc) ]).
+
+(* H:X = SP + 1 *)
+ndefinition execute_TSX ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_sp_reg m t s )
+ (λSP_op.opt_map … (set_indX_16_reg m t s (succ_w16 SP_op))
+ (* H:X = SP + 1 *)
+ (λs_tmp.Some ? (pair … s_tmp cur_pc))).
+
+(* A = X *)
+ndefinition execute_TXA ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_indX_8_low_reg m t s)
+ (λX_op.Some ? (pair … (set_acc_8_low_reg m t s X_op) cur_pc)).
+
+(* SP = H:X - 1 *)
+ndefinition execute_TXS ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ opt_map … (get_indX_16_reg m t s )
+ (λX_op.opt_map … (set_sp_reg m t s (pred_w16 X_op))
+ (* SP = H:X - 1 *)
+ (λs_tmp.Some ? (pair … s_tmp cur_pc))).
+
+(* I = 0 *)
+ndefinition execute_WAIT ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
+ Some ? (pair … (setweak_i_flag m t s false) cur_pc).
+
+(* **** *)
+(* TICK *)
+(* **** *)
+
+(* enumerazione delle possibili modalita' di sospensione *)
+ninductive susp_type : Type ≝
+ BGND_MODE: susp_type
+| STOP_MODE: susp_type
+| WAIT_MODE: susp_type.
+
+(* un tipo opzione ad hoc
+ - errore: errore+stato (seguira' reset o …, cmq lo stato non va buttato)
+ - sospensione: sospensione+stato (seguira' resume o …)
+ - ok: stato
+*)
+ninductive tick_result (A:Type) : Type ≝
+ TickERR : A → error_type → tick_result A
+| TickSUSP : A → susp_type → tick_result A
+| TickOK : A → tick_result A.
+
+(* sostanazialmente simula
+ - fetch/decode/execute
+ - l'esecuzione e' considerata atomica quindi nel caso di un'instruzione
+ da 3 cicli la successione sara'
+ ([fetch/decode] s,clk:None) →
+ ( s,clk:Some 1,pseudo,mode,3,cur_pc) →
+ ( s,clk:Some 2,pseudo,mode,3,cur_pc) →
+ ([execute] s',clk:None) *)
+
+ndefinition tick_execute ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+λpseudo:any_opcode m.λmode:instr_mode.λcur_pc:word16.
+ let abs_pseudo ≝ match pseudo with [ anyOP pseudo' ⇒ pseudo' ] in
+ let a_status_and_fetch ≝ match abs_pseudo with
+ [ ADC ⇒ execute_ADC m t s mode cur_pc (* add with carry *)
+ | ADD ⇒ execute_ADD m t s mode cur_pc (* add *)
+ | AIS ⇒ execute_AIS m t s mode cur_pc (* add immediate to SP *)
+ | AIX ⇒ execute_AIX m t s mode cur_pc (* add immediate to X *)
+ | AND ⇒ execute_AND m t s mode cur_pc (* and *)
+ | ASL ⇒ execute_ASL m t s mode cur_pc (* aritmetic shift left *)
+ | ASR ⇒ execute_ASR m t s mode cur_pc (* aritmetic shift right *)
+ | BCC ⇒ execute_BCC m t s mode cur_pc (* branch if C=0 *)
+ | BCLRn ⇒ execute_BCLRn m t s mode cur_pc (* clear bit n *)
+ | BCS ⇒ execute_BCS m t s mode cur_pc (* branch if C=1 *)
+ | BEQ ⇒ execute_BEQ m t s mode cur_pc (* branch if Z=1 *)
+ | BGE ⇒ execute_BGE m t s mode cur_pc (* branch if N⊙V=0 (great or equal) *)
+ | BGND ⇒ execute_BGND m t s mode cur_pc (* !!background mode!!*)
+ | BGT ⇒ execute_BGT m t s mode cur_pc (* branch if Z|N⊙V=0 clear (great) *)
+ | BHCC ⇒ execute_BHCC m t s mode cur_pc (* branch if H=0 *)
+ | BHCS ⇒ execute_BHCS m t s mode cur_pc (* branch if H=1 *)
+ | BHI ⇒ execute_BHI m t s mode cur_pc (* branch if C|Z=0, (higher) *)
+ | BIH ⇒ execute_BIH m t s mode cur_pc (* branch if nIRQ=1 *)
+ | BIL ⇒ execute_BIL m t s mode cur_pc (* branch if nIRQ=0 *)
+ | BIT ⇒ execute_BIT m t s mode cur_pc (* flag = and (bit test) *)
+ | BLE ⇒ execute_BLE m t s mode cur_pc (* branch if Z|N⊙V=1 (less or equal) *)
+ | BLS ⇒ execute_BLS m t s mode cur_pc (* branch if C|Z=1 (lower or same) *)
+ | BLT ⇒ execute_BLT m t s mode cur_pc (* branch if N⊙1=1 (less) *)
+ | BMC ⇒ execute_BMC m t s mode cur_pc (* branch if I=0 (interrupt mask clear) *)
+ | BMI ⇒ execute_BMI m t s mode cur_pc (* branch if N=1 (minus) *)
+ | BMS ⇒ execute_BMS m t s mode cur_pc (* branch if I=1 (interrupt mask set) *)
+ | BNE ⇒ execute_BNE m t s mode cur_pc (* branch if Z=0 *)
+ | BPL ⇒ execute_BPL m t s mode cur_pc (* branch if N=0 (plus) *)
+ | BRA ⇒ execute_BRA m t s mode cur_pc (* branch always *)
+ | BRCLRn ⇒ execute_BRCLRn m t s mode cur_pc (* branch if bit n clear *)
+ | BRN ⇒ execute_BRN m t s mode cur_pc (* branch never (nop) *)
+ | BRSETn ⇒ execute_BRSETn m t s mode cur_pc (* branch if bit n set *)
+ | BSETn ⇒ execute_BSETn m t s mode cur_pc (* set bit n *)
+ | BSR ⇒ execute_BSR m t s mode cur_pc (* branch to subroutine *)
+ | CBEQA ⇒ execute_CBEQA m t s mode cur_pc (* compare (A) and BEQ *)
+ | CBEQX ⇒ execute_CBEQX m t s mode cur_pc (* compare (X) and BEQ *)
+ | CLC ⇒ execute_CLC m t s mode cur_pc (* C=0 *)
+ | CLI ⇒ execute_CLI m t s mode cur_pc (* I=0 *)
+ | CLR ⇒ execute_CLR m t s mode cur_pc (* operand=0 *)
+ | CMP ⇒ execute_CMP m t s mode cur_pc (* flag = sub (compare A) *)
+ | COM ⇒ execute_COM m t s mode cur_pc (* not (1 complement) *)
+ | CPHX ⇒ execute_CPHX m t s mode cur_pc (* flag = sub (compare H:X) *)
+ | CPX ⇒ execute_CPX m t s mode cur_pc (* flag = sub (compare X) *)
+ | DAA ⇒ execute_DAA m t s mode cur_pc (* decimal adjust A *)
+ | DBNZ ⇒ execute_DBNZ m t s mode cur_pc (* dec and BNE *)
+ | DEC ⇒ execute_DEC m t s mode cur_pc (* operand=operand-1 (decrement) *)
+ | DIV ⇒ execute_DIV m t s mode cur_pc (* div *)
+ | EOR ⇒ execute_EOR m t s mode cur_pc (* xor *)
+ | INC ⇒ execute_INC m t s mode cur_pc (* operand=operand+1 (increment) *)
+ | JMP ⇒ execute_JMP m t s mode cur_pc (* jmp word [operand] *)
+ | JSR ⇒ execute_JSR m t s mode cur_pc (* jmp to subroutine *)
+ | LDA ⇒ execute_LDA m t s mode cur_pc (* load in A *)
+ | LDHX ⇒ execute_LDHX m t s mode cur_pc (* load in H:X *)
+ | LDX ⇒ execute_LDX m t s mode cur_pc (* load in X *)
+ | LSR ⇒ execute_LSR m t s mode cur_pc (* logical shift right *)
+ | MOV ⇒ execute_MOV m t s mode cur_pc (* move *)
+ | MUL ⇒ execute_MUL m t s mode cur_pc (* mul *)
+ | NEG ⇒ execute_NEG m t s mode cur_pc (* neg (2 complement) *)
+ | NOP ⇒ execute_NOP m t s mode cur_pc (* nop *)
+ | NSA ⇒ execute_NSA m t s mode cur_pc (* nibble swap A (al:ah <- ah:al) *)
+ | ORA ⇒ execute_ORA m t s mode cur_pc (* or *)
+ | PSHA ⇒ execute_PSHA m t s mode cur_pc (* push A *)
+ | PSHH ⇒ execute_PSHH m t s mode cur_pc (* push H *)
+ | PSHX ⇒ execute_PSHX m t s mode cur_pc (* push X *)
+ | PULA ⇒ execute_PULA m t s mode cur_pc (* pop A *)
+ | PULH ⇒ execute_PULH m t s mode cur_pc (* pop H *)
+ | PULX ⇒ execute_PULX m t s mode cur_pc (* pop X *)
+ | ROL ⇒ execute_ROL m t s mode cur_pc (* rotate left *)
+ | ROR ⇒ execute_ROR m t s mode cur_pc (* rotate right *)
+ | RSP ⇒ execute_RSP m t s mode cur_pc (* reset SP (0x00FF) *)
+ | RTI ⇒ execute_RTI m t s mode cur_pc (* return from interrupt *)
+ | RTS ⇒ execute_RTS m t s mode cur_pc (* return from subroutine *)
+ | SBC ⇒ execute_SBC m t s mode cur_pc (* sub with carry*)
+ | SEC ⇒ execute_SEC m t s mode cur_pc (* C=1 *)
+ | SEI ⇒ execute_SEI m t s mode cur_pc (* I=1 *)
+ | SHA ⇒ execute_SHA m t s mode cur_pc (* swap spc_high,A *)
+ | SLA ⇒ execute_SLA m t s mode cur_pc (* swap spc_low,A *)
+ | STA ⇒ execute_STA m t s mode cur_pc (* store from A *)
+ | STHX ⇒ execute_STHX m t s mode cur_pc (* store from H:X *)
+ | STOP ⇒ execute_STOP m t s mode cur_pc (* !!stop mode!! *)
+ | STX ⇒ execute_STX m t s mode cur_pc (* store from X *)
+ | SUB ⇒ execute_SUB m t s mode cur_pc (* sub *)
+ | SWI ⇒ execute_SWI m t s mode cur_pc (* software interrupt *)
+ | TAP ⇒ execute_TAP m t s mode cur_pc (* flag=A (transfer A to process status byte *)
+ | TAX ⇒ execute_TAX m t s mode cur_pc (* X=A (transfer A to X) *)
+ | TPA ⇒ execute_TPA m t s mode cur_pc (* A=flag (transfer process status byte to A) *)
+ | TST ⇒ execute_TST m t s mode cur_pc (* flag = sub (test) *)
+ | TSX ⇒ execute_TSX m t s mode cur_pc (* X:H=SP (transfer SP to H:X) *)
+ | TXA ⇒ execute_TXA m t s mode cur_pc (* A=X (transfer X to A) *)
+ | TXS ⇒ execute_TXS m t s mode cur_pc (* SP=X:H (transfer H:X to SP) *)
+ | WAIT ⇒ execute_WAIT m t s mode cur_pc (* !!wait mode!!*)
+ ] in match a_status_and_fetch with
+(* errore nell'execute (=caricamento argomenti)? riportato in output *)
+(* nessun avanzamento e clk a None *)
+ [ None ⇒ TickERR ? (set_clk_desc m t s (None ?)) ILL_EX_AD
+ | Some status_and_newpc ⇒
+(* aggiornamento centralizzato di pc e clk *)
+ match status_and_newpc with
+ [ pair s_tmp1 new_pc ⇒
+ let s_tmp2 ≝ set_pc_reg m t s_tmp1 new_pc in
+ let s_tmp3 ≝ set_clk_desc m t s_tmp2 (None ?) in
+(* distinzione fra le 4 modalita' possibili, normale/BGND/STOP/WAIT *)
+ match eq_op abs_pseudo BGND with
+ [ true ⇒ TickSUSP ? s_tmp3 BGND_MODE
+ | false ⇒ match eq_op abs_pseudo STOP with
+ [ true ⇒ TickSUSP ? s_tmp3 STOP_MODE
+ | false ⇒ match eq_op abs_pseudo WAIT with
+ [ true ⇒ TickSUSP ? s_tmp3 WAIT_MODE
+ | false ⇒ TickOK ? s_tmp3
+ ]]]]].
+
+ndefinition tick ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ let opt_info ≝ clk_desc m t s in
+ match opt_info with
+ (* e' il momento del fetch *)
+ [ None ⇒ match fetch m t s with
+ (* errore nel fetch/decode? riportato in output, nessun avanzamento *)
+ [ FetchERR err ⇒ TickERR ? s err
+ (* nessun errore nel fetch *)
+ | FetchOK fetch_info cur_pc ⇒ match fetch_info with
+ [ quadruple pseudo mode _ tot_clk ⇒
+ match eq_b8 〈x0,x1〉 tot_clk with
+ (* un solo clk, execute subito *)
+ [ true ⇒ tick_execute m t s pseudo mode cur_pc
+ (* piu' clk, execute rimandata *)
+ | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple … 〈x0,x1〉 pseudo mode tot_clk cur_pc)))
+ ]
+ ]
+ ]
+ (* il fetch e' gia' stato eseguito, e' il turno di execute? *)
+ | Some info ⇒ match info with [ quintuple cur_clk pseudo mode tot_clk cur_pc ⇒
+ match eq_b8 (succ_b8 cur_clk) tot_clk with
+ (* si *)
+ [ true ⇒ tick_execute m t s pseudo mode cur_pc
+ (* no, avanzamento cur_clk *)
+ | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple … (succ_b8 cur_clk) pseudo mode tot_clk cur_pc)))
+ ]
+ ]
+ ].
+
+(* ********** *)
+(* ESECUZIONE *)
+(* ********** *)
+
+nlet rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
+ match s with
+ [ TickERR s' error ⇒ TickERR ? s' error
+ | TickSUSP s' susp ⇒ TickSUSP ? s' susp
+ | TickOK s' ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ]
+ ].
--- /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: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "freescale/multivm.ma".
+include "common/nat_lemmas.ma".
+
+nlemma breakpoint_err : ∀m,t,s,err,n.execute m t (TickERR ? s err) n = TickERR ? s err.
+ #m; #t; #s; #err; #n;
+ ncases n;
+ ##[ ##2: #n1; ##]
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma breakpoint_susp : ∀m,t,s,susp,n.execute m t (TickSUSP ? s susp) n = TickSUSP ? s susp.
+ #m; #t; #s; #susp; #n;
+ ncases n;
+ ##[ ##2: #n1; ##]
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma breakpoint :
+ ∀m,t,n1,n2,s. execute m t s (n1 + n2) = execute m t (execute m t s n1) n2.
+ #m; #t; #n1;
+ nelim n1;
+ ##[ ##1: nnormalize; #n2; #s; ncases s; nnormalize; ##[ ##1,2: #x ##] #y; napply refl_eq
+ ##| ##2: #n3; #H; #n2; #s; ncases s;
+ ##[ ##1: #x; #y; nnormalize; nrewrite > (breakpoint_err m t x y n2); napply refl_eq
+ ##| ##2: #x; #y; nnormalize; nrewrite > (breakpoint_susp m t x y n2); napply refl_eq
+ ##| ##3: #x; nrewrite > (Sn_p_n_to_S_npn n3 n2);
+ nchange with ((execute m t (tick m t x) (n3+n2)) =
+ (execute m t (execute m t (tick m t x) n3) n2));
+ nrewrite > (H n2 (tick m t x));
+ napply refl_eq
+ ##]
+ ##]
+nqed.
| false ⇒ mk_byte8 bh' bl' ]]].
(* operatore rotazione destra n-volte *)
-nlet rec ror_b8_n (b:byte8) (n:oct) (r:rec_oct n) on r ≝
- match r with
- [ oc_O ⇒ b
- | oc_S t n' ⇒ ror_b8_n (ror_b8 b) t n' ].
+nlet rec ror_b8_n (b:byte8) (n:nat) on n ≝
+ match n with
+ [ O ⇒ b
+ | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
(* operatore rotazione sinistra con carry *)
ndefinition rcl_b8 ≝
| false ⇒ mk_byte8 bh' bl' ]]].
(* operatore rotazione sinistra n-volte *)
-nlet rec rol_b8_n (b:byte8) (n:oct) (r:rec_oct n) on r ≝
- match r with
- [ oc_O ⇒ b
- | oc_S t n' ⇒ rol_b8_n (rol_b8 b) t n' ].
+nlet rec rol_b8_n (b:byte8) (n:nat) on n ≝
+ match n with
+ [ O ⇒ b
+ | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
(* operatore not/complemento a 1 *)
ndefinition not_b8 ≝
include "num/quatern.ma".
include "num/oct.ma".
include "common/prod.ma".
+include "common/nat.ma".
(* *********** *)
(* ESADECIMALI *)
| xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
(* operatore rotazione destra n-volte *)
-nlet rec ror_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝
- match r with
- [ qu_O ⇒ e
- | qu_S t n' ⇒ ror_ex_n (ror_ex e) t n' ].
+nlet rec ror_ex_n (e:exadecim) (n:nat) on n ≝
+ match n with
+ [ O ⇒ e
+ | S n' ⇒ ror_ex_n (ror_ex e) n' ].
(* operatore rotazione sinistra con carry *)
ndefinition rcl_ex ≝
| xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
(* operatore rotazione sinistra n-volte *)
-nlet rec rol_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝
- match r with
- [ qu_O ⇒ e
- | qu_S t n' ⇒ rol_ex_n (rol_ex e) t n' ].
+nlet rec rol_ex_n (e:exadecim) (n:nat) on n ≝
+ match n with
+ [ O ⇒ e
+ | S n' ⇒ rol_ex_n (rol_ex e) n' ].
(* operatore not/complemento a 1 *)
ndefinition not_ex ≝
| false ⇒ mk_word16 wh' wl' ]]].
(* operatore rotazione destra n-volte *)
-nlet rec ror_w16_n (w:word16) (n:exadecim) (r:rec_exadecim n) on r ≝
- match r with
- [ ex_O ⇒ w
- | ex_S t n' ⇒ ror_w16_n (ror_w16 w) t n' ].
+nlet rec ror_w16_n (w:word16) (n:nat) on n ≝
+ match n with
+ [ O ⇒ w
+ | S n' ⇒ ror_w16_n (ror_w16 w) n' ].
(* operatore rotazione sinistra con carry *)
ndefinition rcl_w16 ≝
| false ⇒ mk_word16 wh' wl' ]]].
(* operatore rotazione sinistra n-volte *)
-nlet rec rol_w16_n (w:word16) (n:exadecim) (r:rec_exadecim n) on r ≝
- match r with
- [ ex_O ⇒ w
- | ex_S t n' ⇒ rol_w16_n (rol_w16 w) t n' ].
+nlet rec rol_w16_n (w:word16) (n:nat) on n ≝
+ match n with
+ [ O ⇒ w
+ | S n' ⇒ rol_w16_n (rol_w16 w) n' ].
(* operatore not/complemento a 1 *)
ndefinition not_w16 ≝
]]]]]].
(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
-nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:oct) (rc:rec_oct c) on rc ≝
+nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:nat) on c ≝
let w' ≝ plus_w16_d_d divd (compl_w16 divs) in
- match rc with
- [ oc_O ⇒ match le_w16 divs divd with
+ match c with
+ [ O ⇒ match le_w16 divs divd with
[ true ⇒ triple … (or_b8 molt q) (w16l w') (⊖ (eq_b8 (w16h w') 〈x0,x0〉))
| false ⇒ triple … q (w16l divd) (⊖ (eq_b8 (w16h divd) 〈x0,x0〉)) ]
- | oc_S t c' ⇒ match le_w16 divs divd with
- [ true ⇒ div_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) t c'
- | false ⇒ div_b8_aux divd (ror_w16 divs) (ror_b8 molt) q t c' ]].
+ | S c' ⇒ match le_w16 divs divd with
+ [ true ⇒ div_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) c'
+ | false ⇒ div_b8_aux divd (ror_w16 divs) (ror_b8 molt) q c' ]].
ndefinition div_b8 ≝
λw:word16.λb:byte8.match eq_b8 b 〈x0,x0〉 with
(* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
(* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
(* puo' essere sottratto al dividendo *)
- | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 ? (ex_to_recex x7)) 〈x8,x0〉 〈x0,x0〉 ? (oct_to_recoct o7) ]].
+ | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 7) 〈x8,x0〉 〈x0,x0〉 7 ]].
(* operatore x in [inf,sup] *)
ndefinition inrange_w16 ≝
| false ⇒ mk_word32 wh' wl' ]]].
(* operatore rotazione destra n-volte *)
-nlet rec ror_w32_n (dw:word32) (n:bitrigesim) (r:rec_bitrigesim n) on r ≝
- match r with
- [ bi_O ⇒ dw
- | bi_S t n' ⇒ ror_w32_n (ror_w32 dw) t n' ].
+nlet rec ror_w32_n (dw:word32) (n:nat) on n ≝
+ match n with
+ [ O ⇒ dw
+ | S n' ⇒ ror_w32_n (ror_w32 dw) n' ].
(* operatore rotazione sinistra con carry *)
ndefinition rcl_w32 ≝
| false ⇒ mk_word32 wh' wl' ]]].
(* operatore rotazione sinistra n-volte *)
-nlet rec rol_w32_n (dw:word32) (n:bitrigesim) (r:rec_bitrigesim n) on r ≝
- match r with
- [ bi_O ⇒ dw
- | bi_S t n' ⇒ rol_w32_n (rol_w32 dw) t n' ].
+nlet rec rol_w32_n (dw:word32) (n:nat) on n ≝
+ match n with
+ [ O ⇒ dw
+ | S n' ⇒ rol_w32_n (rol_w32 dw) n' ].
(* operatore not/complemento a 1 *)
ndefinition not_w32 ≝
]]]]]].
(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
-nlet rec div_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (c:exadecim) (rc:rec_exadecim c) on rc ≝
+nlet rec div_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (c:nat) on c ≝
let w' ≝ plus_w32_d_d divd (compl_w32 divs) in
- match rc with
- [ ex_O ⇒ match le_w32 divs divd with
+ match c with
+ [ O ⇒ match le_w32 divs divd with
[ true ⇒ triple … (or_w16 molt q) (w32l w') (⊖ (eq_w16 (w32h w') 〈〈x0,x0〉:〈x0,x0〉〉))
| false ⇒ triple … q (w32l divd) (⊖ (eq_w16 (w32h divd) 〈〈x0,x0〉:〈x0,x0〉〉)) ]
- | ex_S t c' ⇒ match le_w32 divs divd with
- [ true ⇒ div_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) t c'
- | false ⇒ div_w16_aux divd (ror_w32 divs) (ror_w16 molt) q t c' ]].
+ | S c' ⇒ match le_w32 divs divd with
+ [ true ⇒ div_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) c'
+ | false ⇒ div_w16_aux divd (ror_w32 divs) (ror_w16 molt) q c' ]].
ndefinition div_w16 ≝
λw:word32.λb:word16.match eq_w16 b 〈〈x0,x0〉:〈x0,x0〉〉 with
(* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
(* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
(* puo' essere sottratto al dividendo *)
- | false ⇒ div_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 ? (bit_to_recbit t0F)) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 ? (ex_to_recex xF) ]].
+ | false ⇒ div_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 15) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 15 ]].
(* operatore x in [inf,sup] *)
ndefinition inrange_w32 ≝
projects / helm.git / commitdiff