X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Femulator%2Fstatus%2Fstatus_base.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Femulator%2Fstatus%2Fstatus_base.ma;h=b6d394c919f5c928b4074006fe8e7e142ea3fdfd;hb=cacd19eb7ce2395301b31ed3932b4cd7c23ca90e;hp=0000000000000000000000000000000000000000;hpb=3e758134d629980e9bf018a913404b98eccc514c;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly2/emulator/status/status_base.ma b/helm/software/matita/contribs/ng_assembly2/emulator/status/status_base.ma new file mode 100755 index 000000000..b6d394c91 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly2/emulator/status/status_base.ma @@ -0,0 +1,171 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "emulator/memory/memory_abs.ma". +include "emulator/status/HC05_status.ma". +include "emulator/status/HC08_status.ma". +include "emulator/status/RS08_status.ma". +include "emulator/status/IP2022_status.ma". +include "emulator/opcodes/pseudo.ma". + +(* *********************************** *) +(* STATUS INTERNO DEL PROCESSORE (ALU) *) +(* *********************************** *) + +(* descrittore del click = stato di avanzamento dell'esecuzione *) +(* 1) None = istruzione eseguita, attesa del fetch *) +(* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito *) +ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_pseudo_type m) (aux_im_type m) byte8 word16. + +nlemma clk_is_comparable : mcu_type → comparable. + #m; @ (aux_clk_type m) + ##[ napply (zeroc (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable)) + ##| napply (forallc (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable)) + ##| napply (eqc (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable)) + ##| napply (eqc_to_eq (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable)) + ##| napply (eq_to_eqc (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable)) + ##| napply (neqc_to_neq (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable)) + ##| napply (neq_to_neqc (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable)) + ##| napply (decidable_c (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable)) + ##| napply (symmetric_eqc (quintuple_is_comparable byte8_is_comparable (pseudo_is_comparable m) (im_is_comparable m) byte8_is_comparable word16_is_comparable)) + ##] +nqed. + +unification hint 0 ≔ M:mcu_type ⊢ carr (clk_is_comparable M) ≡ aux_clk_type M. + +(* descritture della alu *) +ndefinition aux_alu_type ≝ +λm.match m with + [ HC05 ⇒ alu_HC05 + | HC08 ⇒ alu_HC08 + | HCS08 ⇒ alu_HC08 + | RS08 ⇒ alu_RS08 + | IP2022 ⇒ alu_IP2022 + ]. + +nlemma alu_is_comparable : mcu_type → comparable. + #m; @ (aux_alu_type m) + ##[ nelim m; + ##[ napply (zeroc aluHC05_is_comparable) + ##| napply (zeroc aluHC08_is_comparable) + ##| napply (zeroc aluHC08_is_comparable) + ##| napply (zeroc aluRS08_is_comparable) + ##| napply (zeroc aluIP2022_is_comparable) ##] + ##| nelim m; + ##[ napply (forallc aluHC05_is_comparable) + ##| napply (forallc aluHC08_is_comparable) + ##| napply (forallc aluHC08_is_comparable) + ##| napply (forallc aluRS08_is_comparable) + ##| napply (forallc aluIP2022_is_comparable) ##] + ##| nelim m; + ##[ napply (eqc aluHC05_is_comparable) + ##| napply (eqc aluHC08_is_comparable) + ##| napply (eqc aluHC08_is_comparable) + ##| napply (eqc aluRS08_is_comparable) + ##| napply (eqc aluIP2022_is_comparable) ##] + ##| nelim m; + ##[ napply (eqc_to_eq aluHC05_is_comparable) + ##| napply (eqc_to_eq aluHC08_is_comparable) + ##| napply (eqc_to_eq aluHC08_is_comparable) + ##| napply (eqc_to_eq aluRS08_is_comparable) + ##| napply (eqc_to_eq aluIP2022_is_comparable) ##] + ##| nelim m; + ##[ napply (eq_to_eqc aluHC05_is_comparable) + ##| napply (eq_to_eqc aluHC08_is_comparable) + ##| napply (eq_to_eqc aluHC08_is_comparable) + ##| napply (eq_to_eqc aluRS08_is_comparable) + ##| napply (eq_to_eqc aluIP2022_is_comparable) ##] + ##| nelim m; + ##[ napply (neqc_to_neq aluHC05_is_comparable) + ##| napply (neqc_to_neq aluHC08_is_comparable) + ##| napply (neqc_to_neq aluHC08_is_comparable) + ##| napply (neqc_to_neq aluRS08_is_comparable) + ##| napply (neqc_to_neq aluIP2022_is_comparable) ##] + ##| nelim m; + ##[ napply (neq_to_neqc aluHC05_is_comparable) + ##| napply (neq_to_neqc aluHC08_is_comparable) + ##| napply (neq_to_neqc aluHC08_is_comparable) + ##| napply (neq_to_neqc aluRS08_is_comparable) + ##| napply (neq_to_neqc aluIP2022_is_comparable) ##] + ##| nelim m; + ##[ napply (decidable_c aluHC05_is_comparable) + ##| napply (decidable_c aluHC08_is_comparable) + ##| napply (decidable_c aluHC08_is_comparable) + ##| napply (decidable_c aluRS08_is_comparable) + ##| napply (decidable_c aluIP2022_is_comparable) ##] + ##| nelim m; + ##[ napply (symmetric_eqc aluHC05_is_comparable) + ##| napply (symmetric_eqc aluHC08_is_comparable) + ##| napply (symmetric_eqc aluHC08_is_comparable) + ##| napply (symmetric_eqc aluRS08_is_comparable) + ##| napply (symmetric_eqc aluIP2022_is_comparable) ##] + ##] +nqed. + +unification hint 0 ≔ M:mcu_type ⊢ carr (alu_is_comparable M) ≡ aux_alu_type M. + +(* tipo processore dipendente dalla mcu, varia solo la ALU *) +nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝ + { + (* descrittore della alu *) + alu : aux_alu_type mcu; + (* descritore della memoria *) + mem_desc : aux_mem_type t; + (* descrittore del tipo di memoria installata *) + chk_desc : aux_chk_type t; + (* descrittore del clik *) + clk_desc : option (aux_clk_type mcu) + }. + +(* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *) +notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80 + for @{ 'mk_any_status $alu $mem $chk $clk }. +interpretation "mk_any_status" 'mk_any_status alu mem chk clk = + (mk_any_status alu mem chk clk). + +(* ******************** *) +(* CONFRONTO FRA STATUS *) +(* ******************** *) + +ndefinition eq_anystatus ≝ +λm,t.λs1,s2:any_status m t. + (eqc ? (alu … s1) (alu … s2)) ⊗ + (eqc ? (mem_desc … s1) (mem_desc … s2)) ⊗ + (eqc ? (chk_desc … s1) (chk_desc … s2)) ⊗ + (eqc ? (clk_desc … s1) (clk_desc … s2)). + +ndefinition forall_anystatus ≝ λm,t.λP:any_status m t → bool. + forallc ? (λr1.forallc ? (λr2. + forallc ? (λr3.forallc ? (λr4. + P (mk_any_status m t r1 r2 r3 r4))))). + +(* confronto di una regione di memoria [addr1 ; ... ; addrn] *) +nlet rec forall_memory_ranged + (t:memory_impl) + (chk1:aux_chk_type t) (chk2:aux_chk_type t) + (mem1:aux_mem_type t) (mem2:aux_mem_type t) + (sel:oct) (addrl:list word16) on addrl ≝ + match addrl return λ_.bool with + [ nil ⇒ true + | cons hd tl ⇒ (eqc ? (mem_read t mem1 chk1 sel hd) (mem_read t mem2 chk2 sel hd)) ⊗ + (forall_memory_ranged t chk1 chk2 mem1 mem2 sel tl) + ].