From: Cosimo Oliboni Date: Wed, 5 Aug 2009 11:03:09 +0000 (+0000) Subject: freescale porting, work in progress X-Git-Tag: make_still_working~3568 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=be0ca791abbf1084b7218f2d17ab48462fbb3049;p=helm.git freescale porting, work in progress --- diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index 41b4315f8..ef011e972 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -1,50 +1,60 @@ -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 diff --git a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma new file mode 100755 index 000000000..0c14beae6 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma @@ -0,0 +1,946 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ? + ] + ]. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/model.ma b/helm/software/matita/contribs/ng_assembly/freescale/model.ma new file mode 100755 index 000000000..f1e5b9488 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/freescale/model.ma @@ -0,0 +1,357 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ?) ]] + ]. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma new file mode 100755 index 000000000..37ef8d9c6 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma @@ -0,0 +1,1307 @@ +(**************************************************************************) +(* ___ *) +(* ||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' ] + ]. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/multivm_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/multivm_lemmas.ma new file mode 100755 index 000000000..c1a6e2737 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/freescale/multivm_lemmas.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma index f2cbdb758..260e49ad0 100755 --- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma +++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma @@ -91,10 +91,10 @@ ndefinition ror_b8 ≝ | 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 ≝ @@ -117,10 +117,10 @@ ndefinition rol_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 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma index 10019b379..b0c0faf19 100755 --- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma +++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma @@ -24,6 +24,7 @@ include "num/bool.ma". include "num/quatern.ma". include "num/oct.ma". include "common/prod.ma". +include "common/nat.ma". (* *********** *) (* ESADECIMALI *) @@ -712,10 +713,10 @@ ndefinition ror_ex ≝ | 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 ≝ @@ -761,10 +762,10 @@ ndefinition rol_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 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma index b078169d7..965fb4b38 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word16.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma @@ -90,10 +90,10 @@ ndefinition ror_w16 ≝ | 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 ≝ @@ -116,10 +116,10 @@ ndefinition rol_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 ≝ @@ -200,15 +200,15 @@ ndefinition mul_b8 ≝ ]]]]]]. (* 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 @@ -224,7 +224,7 @@ ndefinition div_b8 ≝ (* 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 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma index 091d0f73c..4fd80d63b 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word32.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma @@ -90,10 +90,10 @@ ndefinition ror_w32 ≝ | 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 ≝ @@ -116,10 +116,10 @@ ndefinition rol_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 ≝ @@ -200,15 +200,15 @@ ndefinition mul_w16 ≝ ]]]]]]. (* 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 @@ -224,7 +224,7 @@ ndefinition div_w16 ≝ (* 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 ≝