freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale_tests / micro_tests4.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests4.ma b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests4.ma
index 7f182852bf5a85c5fd0f65a5796bcbfb228e345c..c2f055c701d606736dd6dc5cfee74daefd6c2bae 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests4.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests4.ma
@@ -101,17 +101,52 @@ nlemma ok_mTest_HCS08_CBEQ_DBNZ_full :
     (mk_word16 〈x1,x8〉 〈x8,xE〉))
    (mk_byte8 xF xF))
   [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] = true.
- #t; 
- napply (eq_to_eqanystatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] HCS08 t
-        (match execute HCS08 t (TickOK ? (mTest_HCS08_CBEQ_DBNZ_status t 〈x0,x0〉 〈x0,x1〉 〈x0,x2〉)) nat68
-         with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
-        (set_acc_8_low_reg HCS08 t (* nuovo A *)
-         (set_pc_reg HCS08 t (* nuovo PC *)
-          (setweak_indX_16_reg HCS08 t (mTest_HCS08_CBEQ_DBNZ_status t 〈xF,xE〉 〈x0,x1〉 〈x0,x0〉) (* nuovo H:X *)
-           (mk_word16 〈x0,x0〉 〈x7,x0〉))
-          (mk_word16 〈x1,x8〉 〈x8,xE〉))
-         (mk_byte8 xF xF)));
- nelim t;
- nnormalize in ⊢ (? ? ? %);
- napply refl_eq.
+ #t;
+
+ (* nelim t; napply refl_eq; *)
+ (* cosi' in 7sec fa tutto *)
+
+ napply (eq_to_eqanystatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] HCS08 t …);
+ ##[ ##3: (* ram *) 
+          nelim t;
+          nnormalize in ⊢ (? ? % ?);
+          napply refl_eq;
+          (* 10sec con normalize, leggermente di piu' senza *)
+ ##| ##2: (* descrittore *)
+          nelim t;
+          nnormalize in ⊢ (? ? ? %);
+          nnormalize in ⊢ (? ? % ?);
+          napply refl_eq;
+          (* 7sec con normalize, leggermente di piu' senza il secondo normalize,
+             non termina senza il primo *)
+ ##| ##1: (* alu *)
+          nelim t;
+          (* senza questo normalize non va nulla *)
+          ##[ ##2,3: nnormalize in ⊢ (? ? ? %);
+                     napply refl_eq;
+          ##| ##1: (* in questo punto si vede benissimo come stato1 = stato2 esplode
+                      mentre la trasformazione eq_stato s1 s2 = true computa benissimo *)
+                   (* un napply refl_eq diretto non ci riesce proprio... *)
+                   napply (eqaluHC08_to_eq
+                    (alu HCS08 MEM_FUNC (match execute HCS08 MEM_FUNC (TickOK ? (mTest_HCS08_CBEQ_DBNZ_status MEM_FUNC 〈x0,x0〉 〈x0,x1〉 〈x0,x2〉)) nat68 with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]))
+                    (alu HCS08 MEM_FUNC (set_acc_8_low_reg HCS08 MEM_FUNC (* nuovo A *)
+                     (set_pc_reg HCS08 MEM_FUNC (* nuovo PC *)
+                      (setweak_indX_16_reg HCS08 MEM_FUNC (mTest_HCS08_CBEQ_DBNZ_status MEM_FUNC 〈xF,xE〉 〈x0,x1〉 〈x0,x0〉) (* nuovo H:X *)
+                       (mk_word16 〈x0,x0〉 〈x7,x0〉)) (mk_word16 〈x1,x8〉 〈x8,xE〉)) (mk_byte8 xF xF)))
+                    ?);
+                   nnormalize in ⊢ (? ? % ?);
+                   napply refl_eq;
+          ##]
+ ##]
+(* pero' ora si e' inceppato nqed... *)
 nqed.
+
+(* IMPRESSIONI
+   sembra confermato ora che un confronto diretto "oggettoGrosso1 = oggettoGrosso2" fallisca
+   mentre "funzione_eq oggettoGrosso1 oggettoGrosso2 = const." riesce
+
+   lo si vede in "forall_memory_ranged mem1 mem2 [addr] = true"
+   lo si vede in "get_clk (...) = const." NB: senza il normalize dx. infatti fallisce...
+   lo si vede in "alu1 = alu2" che fallisce stranamente solo nel caso MEM_FUNC
+    riportare "alu1 = alu2" a "eq alu1 alu2 = true" col teorema lo aggira, ma non chiude nqed
+*)