X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fstatus.ma;h=1354861e2a9858f0ef90c99e85917b6b1b04117b;hb=ec07ff398325533d848da92e9dc69852d24b78a5;hp=6a0f81887ef4431385fb048784bf9beecdd1e4a2;hpb=842e243be954d67360788d08701289f3237c2699;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma index 6a0f81887..1354861e2 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/status.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/status.ma @@ -15,14 +15,13 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) include "freescale/memory_abs.ma". include "freescale/opcode_base.ma". -include "freescale/prod.ma". (* *********************************** *) (* STATUS INTERNO DEL PROCESSORE (ALU) *) @@ -501,7 +500,7 @@ ndefinition set_indX_8_low_reg_HC08 ≝ (* setter forte di X *) ndefinition set_indX_8_low_reg ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8. - opt_map ?? (match m return aux_set_typing_opt byte8 with + opt_map … (match m return aux_set_typing_opt byte8 with [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05 | HC08 ⇒ Some ? set_indX_8_low_reg_HC08 | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08 @@ -536,7 +535,7 @@ ndefinition set_indX_8_high_reg_HC08 ≝ (* setter forte di H *) ndefinition set_indX_8_high_reg ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8. - opt_map ?? (match m return aux_set_typing_opt byte8 with + opt_map … (match m return aux_set_typing_opt byte8 with [ HC05 ⇒ None ? | HC08 ⇒ Some ? set_indX_8_high_reg_HC08 | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08 @@ -571,7 +570,7 @@ ndefinition set_indX_16_reg_HC08 ≝ (* setter forte di H:X *) ndefinition set_indX_16_reg ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16. - opt_map ?? (match m return aux_set_typing_opt word16 with + opt_map … (match m return aux_set_typing_opt word16 with [ HC05 ⇒ None ? | HC08 ⇒ Some ? set_indX_16_reg_HC08 | HCS08 ⇒ Some ? set_indX_16_reg_HC08 @@ -624,7 +623,7 @@ ndefinition set_sp_reg_HC08 ≝ (* setter forte di SP *) ndefinition set_sp_reg ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16. - opt_map ?? (match m return aux_set_typing_opt word16 with + opt_map … (match m return aux_set_typing_opt word16 with [ HC05 ⇒ Some ? set_sp_reg_HC05 | HC08 ⇒ Some ? set_sp_reg_HC08 | HCS08 ⇒ Some ? set_sp_reg_HC08 @@ -716,7 +715,7 @@ ndefinition set_spc_reg_RS08 ≝ (* setter forte di SPC *) ndefinition set_spc_reg ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16. - opt_map ?? (match m return aux_set_typing_opt word16 with + opt_map … (match m return aux_set_typing_opt word16 with [ HC05 ⇒ None ? | HC08 ⇒ None ? | HCS08 ⇒ None ? @@ -747,7 +746,7 @@ ndefinition set_x_map_RS08 ≝ (* setter forte di memory mapped X *) ndefinition set_x_map ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8. - opt_map ?? (match m return aux_set_typing_opt byte8 with + opt_map … (match m return aux_set_typing_opt byte8 with [ HC05 ⇒ None ? | HC08 ⇒ None ? | HCS08 ⇒ None ? @@ -778,7 +777,7 @@ ndefinition set_ps_map_RS08 ≝ (* setter forte di memory mapped PS *) ndefinition set_ps_map ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8. - opt_map ?? (match m return aux_set_typing_opt byte8 with + opt_map … (match m return aux_set_typing_opt byte8 with [ HC05 ⇒ None ? | HC08 ⇒ None ? | HCS08 ⇒ None ? @@ -813,7 +812,7 @@ ndefinition set_v_flag_HC08 ≝ (* setter forte di V *) ndefinition set_v_flag ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool. - opt_map ?? (match m return aux_set_typing_opt bool with + opt_map … (match m return aux_set_typing_opt bool with [ HC05 ⇒ None ? | HC08 ⇒ Some ? set_v_flag_HC08 | HCS08 ⇒ Some ? set_v_flag_HC08 @@ -866,7 +865,7 @@ ndefinition set_h_flag_HC08 ≝ (* setter forte di H *) ndefinition set_h_flag ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool. - opt_map ?? (match m return aux_set_typing_opt bool with + opt_map … (match m return aux_set_typing_opt bool with [ HC05 ⇒ Some ? set_h_flag_HC05 | HC08 ⇒ Some ? set_h_flag_HC08 | HCS08 ⇒ Some ? set_h_flag_HC08 @@ -919,7 +918,7 @@ ndefinition set_i_flag_HC08 ≝ (* setter forte di I *) ndefinition set_i_flag ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool. - opt_map ?? (match m return aux_set_typing_opt bool with + opt_map … (match m return aux_set_typing_opt bool with [ HC05 ⇒ Some ? set_i_flag_HC05 | HC08 ⇒ Some ? set_i_flag_HC08 | HCS08 ⇒ Some ? set_i_flag_HC08 @@ -972,7 +971,7 @@ ndefinition set_n_flag_HC08 ≝ (* setter forte di N *) ndefinition set_n_flag ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool. - opt_map ?? (match m return aux_set_typing_opt bool with + opt_map … (match m return aux_set_typing_opt bool with [ HC05 ⇒ Some ? set_n_flag_HC05 | HC08 ⇒ Some ? set_n_flag_HC08 | HCS08 ⇒ Some ? set_n_flag_HC08 @@ -1147,7 +1146,7 @@ ndefinition set_irq_flag_HC08 ≝ (* setter forte di IRQ *) ndefinition set_irq_flag ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool. - opt_map ?? (match m return aux_set_typing_opt bool with + opt_map … (match m return aux_set_typing_opt bool with [ HC05 ⇒ Some ? set_irq_flag_HC05 | HC08 ⇒ Some ? set_irq_flag_HC08 | HCS08 ⇒ Some ? set_irq_flag_HC08 @@ -1165,7 +1164,7 @@ ndefinition setweak_irq_flag ≝ (* ***************** *) (* confronto registro per registro dell'HC05 *) -ndefinition eq_alu_HC05 ≝ +ndefinition eq_aluHC05 ≝ λalu1,alu2:alu_HC05. match alu1 with [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒ @@ -1186,7 +1185,7 @@ ndefinition eq_alu_HC05 ≝ (eq_bool irqfl1 irqfl2) ]]. (* confronto registro per registro dell'HC08 *) -ndefinition eq_alu_HC08 ≝ +ndefinition eq_aluHC08 ≝ λalu1,alu2:alu_HC08. match alu1 with [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒ @@ -1206,7 +1205,7 @@ ndefinition eq_alu_HC08 ≝ (eq_bool irqfl1 irqfl2) ]]. (* confronto registro per registro dell'RS08 *) -ndefinition eq_alu_RS08 ≝ +ndefinition eq_aluRS08 ≝ λalu1,alu2:alu_RS08. match alu1 with [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒ @@ -1245,15 +1244,15 @@ ndefinition eq_clk ≝ [ None ⇒ match c2 with [ None ⇒ true | Some _ ⇒ false ] | Some c1' ⇒ match c2 with - [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T ????? c1') (fst5T ????? c2')) ⊗ - (eq_anyop m (snd5T ????? c1') (snd5T ????? c2')) ⊗ - (eq_instrmode (thd5T ????? c1') (thd5T ????? c2')) ⊗ - (eq_b8 (frth5T ????? c1') (frth5T ????? c2')) ⊗ - (eq_w16 (ffth5T ????? c1') (ffth5T ????? c2')) ] + [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T … c1') (fst5T … c2')) ⊗ + (eq_anyop m (snd5T … c1') (snd5T … c2')) ⊗ + (eq_im (thd5T … c1') (thd5T … c2')) ⊗ + (eq_b8 (frth5T … c1') (frth5T … c2')) ⊗ + (eq_w16 (ffth5T … c1') (ffth5T … c2')) ] ]. (* generalizzazione del confronto fra stati *) -ndefinition eq_status ≝ +ndefinition eq_anystatus ≝ λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word16. match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒ match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒ @@ -1265,7 +1264,7 @@ ndefinition eq_status ≝ match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] → bool with - [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ] + [ HC05 ⇒ eq_aluHC05 | HC08 ⇒ eq_aluHC08 | HCS08 ⇒ eq_aluHC08 | RS08 ⇒ eq_aluRS08 ] alu1 alu2) ⊗ (* 2) confronto della memoria in [inf,inf+n] *)