From d00e19c7000a00659ffd609ef79675eb0f010659 Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Thu, 15 Oct 2009 08:47:14 +0000 Subject: [PATCH] freescale porting, work in progress --- .../matita/contribs/ng_assembly/depends | 3 +- .../freescale_tests/micro_tests4bis.ma | 89 +++++++++++++++++++ 2 files changed, 91 insertions(+), 1 deletion(-) create mode 100755 helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests4bis.ma diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index da004c3fd..7690f37b4 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -21,6 +21,7 @@ num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma num/byte8.ma num/bitrigesim.ma num/exadecim.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_tests/micro_tests4bis.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma freescale/table_RS08.ma common/list.ma freescale/opcode_base.ma common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma @@ -51,8 +52,8 @@ freescale_tests/medium_tests.ma common/list_utility.ma common/nat_to_num.ma free freescale/opcode_base_lemmas1.ma freescale/opcode_base_lemmas_instrmode.ma freescale/opcode_base_lemmas_opcode.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 +freescale/table_HCS08.ma common/list.ma freescale/opcode_base.ma common/ascii.ma num/bool.ma num/word32.ma num/word16.ma freescale_tests/micro_tests8.ma freescale/multivm.ma freescale/status_lemmas.ma freescale_tests/micro_tests_tools.ma diff --git a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests4bis.ma b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests4bis.ma new file mode 100755 index 000000000..cb3844651 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests4bis.ma @@ -0,0 +1,89 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) +(* *) +(* ********************************************************************** *) + +include "freescale_tests/micro_tests_tools.ma". +include "freescale/multivm.ma". +include "freescale/status_lemmas.ma". + +(* ****************************************** *) +(* MICRO TEST DI CORRETTEZZA DELLE ISTRUZIONI *) +(* ****************************************** *) + +(* **************** *) +(* HCS08 CBEQx/DBNZ *) +(* **************** *) + +ndefinition mTest_HCS08_CBEQ_DBNZ_source ≝ let m ≝ HCS08 in source_to_byte8 m ( +(* testa la logica di CBEQx/DBNZ e le modalita' xxx_and_IMM1 *) +(* BEFORE: H:X=0x006F SP=0x006F PC=0x1860 *) +(* [0x1860] 5clk *) (compile m ? CBEQA (maDIR1_and_IMM1 〈x7,x1〉 〈x0,x1〉) I) @ +(* [0x1863] 1clk *) (compile m ? NOP maINH I) @ (* eseguito: A≠[0x0071]=0x01 *) +(* [0x1864] 4clk *) (compile m ? CBEQA (maIMM1_and_IMM1 〈x0,x0〉 〈x0,x1〉) I) @ +(* [0x1867] 1clk *) (compile m ? NOP maINH I) @ (* non eseguito: A=0x00 *) +(* [0x1868] 4clk *) (compile m ? CBEQX (maIMM1_and_IMM1 〈x6,xF〉 〈x0,x1〉) I) @ +(* [0x186B] 1clk *) (compile m ? NOP maINH I) (* non eseguito: X=0x6F *) +(* [0x186C] si puo' quindi enunciare che dopo 5+1+4+4 =14 *) +(* PC<-0x186C H:X<-006F *) +). + +(* creazione del processore+caricamento+impostazione registri *) +ndefinition mTest_HCS08_CBEQ_DBNZ_status ≝ +λt:memory_impl. +λb1,b2,b3:byte8. + setweak_sp_reg HCS08 t (* SP<-0x006F *) + (setweak_indX_16_reg HCS08 t (* H:X<-0x006F *) + (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *) + (start_of_mcu_version_HCS08 + MC9S08AW60 t + (load_from_source_at t (* carica b1-3 in RAM:mTest_HCS08_RAM *) + (load_from_source_at t (* carica mTest_bytes in RAM:mTest_HCS08_RAM *) + (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_HCS08_prog *) + mTest_HCS08_CBEQ_DBNZ_source mTest_HCS08_prog) + mTest_bytes mTest_HCS08_RAM) + [ b1 ; b2 ; b3 ] mTest_HCS08_RAM) + (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08AW60) t) + (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *) + false false false false false false) (* non deterministici tutti a 0 *) + mTest_HCS08_prog) + (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x6 xF))) + (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x6 xF)). + +(* dimostrazione senza svolgimento degli stati, immediata *) +(* NB: la memoria e' cambiata e bisogna applicare eq_status *) +nlemma ok_mTest_HCS08_CBEQ_DBNZ_full : +∀t:memory_impl. + eq_anystatus HCS08 t + (match execute HCS08 t (TickOK ? (mTest_HCS08_CBEQ_DBNZ_status t 〈x0,x0〉 〈x0,x1〉 〈x0,x2〉)) nat14 + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]) + (set_pc_reg HCS08 t (* nuovo PC *) + (mTest_HCS08_CBEQ_DBNZ_status t 〈x0,x0〉 〈x0,x1〉 〈x0,x2〉) (* nuovo H:X *) + (mk_word16 〈x1,x8〉 〈x6,xC〉)) + [] = true. + #t; + + (* nelim t; napply refl_eq; nqed. *) + (* cosi' in 3sec fa tutto *) + + napply (eq_to_eqanystatus_weak [] HCS08 t …); + nelim t; + napply refl_eq. +nqed. -- 2.39.2