]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma
projects / helm.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
freescale porting, work in progress
[helm.git] / helm / software / matita / contribs / ng_assembly / freescale_tests / micro_tests.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Ultima modifica: 05/08/2009                                          *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "freescale/multivm.ma".
24 include "freescale/status_lemmas.ma".
25
26 (* ****************************************** *)
27 (* MICRO TEST DI CORRETTEZZA DELLE ISTRUZIONI *)
28 (* ****************************************** *)
29
30 (* tabella 0x00 - 0xFF utile da caricare in RAM/ROM *)
31 ndefinition mTest_bytes : list byte8 ≝
32  [   〈x0,x0〉 ; 〈x0,x1〉 ; 〈x0,x2〉 ; 〈x0,x3〉 ; 〈x0,x4〉 ; 〈x0,x5〉 ; 〈x0,x6〉 ; 〈x0,x7〉
33  ; 〈x0,x8〉 ; 〈x0,x9〉 ; 〈x0,xA〉 ; 〈x0,xB〉 ; 〈x0,xC〉 ; 〈x0,xD〉 ; 〈x0,xE〉 ; 〈x0,xF〉 ]
34 @[   〈x1,x0〉 ; 〈x1,x1〉 ; 〈x1,x2〉 ; 〈x1,x3〉 ; 〈x1,x4〉 ; 〈x1,x5〉 ; 〈x1,x6〉 ; 〈x1,x7〉
35  ; 〈x1,x8〉 ; 〈x1,x9〉 ; 〈x1,xA〉 ; 〈x1,xB〉 ; 〈x1,xC〉 ; 〈x1,xD〉 ; 〈x1,xE〉 ; 〈x1,xF〉 ]
36 @[   〈x2,x0〉 ; 〈x2,x1〉 ; 〈x2,x2〉 ; 〈x2,x3〉 ; 〈x2,x4〉 ; 〈x2,x5〉 ; 〈x2,x6〉 ; 〈x2,x7〉
37  ; 〈x2,x8〉 ; 〈x2,x9〉 ; 〈x2,xA〉 ; 〈x2,xB〉 ; 〈x2,xC〉 ; 〈x2,xD〉 ; 〈x2,xE〉 ; 〈x2,xF〉 ]
38 @[   〈x3,x0〉 ; 〈x3,x1〉 ; 〈x3,x2〉 ; 〈x3,x3〉 ; 〈x3,x4〉 ; 〈x3,x5〉 ; 〈x3,x6〉 ; 〈x3,x7〉
39  ; 〈x3,x8〉 ; 〈x3,x9〉 ; 〈x3,xA〉 ; 〈x3,xB〉 ; 〈x3,xC〉 ; 〈x3,xD〉 ; 〈x3,xE〉 ; 〈x3,xF〉 ]
40 @[   〈x4,x0〉 ; 〈x4,x1〉 ; 〈x4,x2〉 ; 〈x4,x3〉 ; 〈x4,x4〉 ; 〈x4,x5〉 ; 〈x4,x6〉 ; 〈x4,x7〉
41  ; 〈x4,x8〉 ; 〈x4,x9〉 ; 〈x4,xA〉 ; 〈x4,xB〉 ; 〈x4,xC〉 ; 〈x4,xD〉 ; 〈x4,xE〉 ; 〈x4,xF〉 ]
42 @[   〈x5,x0〉 ; 〈x5,x1〉 ; 〈x5,x2〉 ; 〈x5,x3〉 ; 〈x5,x4〉 ; 〈x5,x5〉 ; 〈x5,x6〉 ; 〈x5,x7〉
43  ; 〈x5,x8〉 ; 〈x5,x9〉 ; 〈x5,xA〉 ; 〈x5,xB〉 ; 〈x5,xC〉 ; 〈x5,xD〉 ; 〈x5,xE〉 ; 〈x5,xF〉 ]
44 @[   〈x6,x0〉 ; 〈x6,x1〉 ; 〈x6,x2〉 ; 〈x6,x3〉 ; 〈x6,x4〉 ; 〈x6,x5〉 ; 〈x6,x6〉 ; 〈x6,x7〉
45  ; 〈x6,x8〉 ; 〈x6,x9〉 ; 〈x6,xA〉 ; 〈x6,xB〉 ; 〈x6,xC〉 ; 〈x6,xD〉 ; 〈x6,xE〉 ; 〈x6,xF〉 ]
46 @[   〈x7,x0〉 ; 〈x7,x1〉 ; 〈x7,x2〉 ; 〈x7,x3〉 ; 〈x7,x4〉 ; 〈x7,x5〉 ; 〈x7,x6〉 ; 〈x7,x7〉
47  ; 〈x7,x8〉 ; 〈x7,x9〉 ; 〈x7,xA〉 ; 〈x7,xB〉 ; 〈x7,xC〉 ; 〈x7,xD〉 ; 〈x7,xE〉 ; 〈x7,xF〉 ]
48 @[  〈x8,x0〉 ; 〈x8,x1〉 ; 〈x8,x2〉 ; 〈x8,x3〉 ; 〈x8,x4〉 ; 〈x8,x5〉 ; 〈x8,x6〉 ; 〈x8,x7〉
49  ; 〈x8,x8〉 ; 〈x8,x9〉 ; 〈x8,xA〉 ; 〈x8,xB〉 ; 〈x8,xC〉 ; 〈x8,xD〉 ; 〈x8,xE〉 ; 〈x8,xF〉 ]
50 @[   〈x9,x0〉 ; 〈x9,x1〉 ; 〈x9,x2〉 ; 〈x9,x3〉 ; 〈x9,x4〉 ; 〈x9,x5〉 ; 〈x9,x6〉 ; 〈x9,x7〉
51  ; 〈x9,x8〉 ; 〈x9,x9〉 ; 〈x9,xA〉 ; 〈x9,xB〉 ; 〈x9,xC〉 ; 〈x9,xD〉 ; 〈x9,xE〉 ; 〈x9,xF〉 ]
52 @[   〈xA,x0〉 ; 〈xA,x1〉 ; 〈xA,x2〉 ; 〈xA,x3〉 ; 〈xA,x4〉 ; 〈xA,x5〉 ; 〈xA,x6〉 ; 〈xA,x7〉
53  ; 〈xA,x8〉 ; 〈xA,x9〉 ; 〈xA,xA〉 ; 〈xA,xB〉 ; 〈xA,xC〉 ; 〈xA,xD〉 ; 〈xA,xE〉 ; 〈xA,xF〉 ]
54 @[   〈xB,x0〉 ; 〈xB,x1〉 ; 〈xB,x2〉 ; 〈xB,x3〉 ; 〈xB,x4〉 ; 〈xB,x5〉 ; 〈xB,x6〉 ; 〈xB,x7〉
55  ; 〈xB,x8〉 ; 〈xB,x9〉 ; 〈xB,xA〉 ; 〈xB,xB〉 ; 〈xB,xC〉 ; 〈xB,xD〉 ; 〈xB,xE〉 ; 〈xB,xF〉 ]
56 @[   〈xC,x0〉 ; 〈xC,x1〉 ; 〈xC,x2〉 ; 〈xC,x3〉 ; 〈xC,x4〉 ; 〈xC,x5〉 ; 〈xC,x6〉 ; 〈xC,x7〉
57  ; 〈xC,x8〉 ; 〈xC,x9〉 ; 〈xC,xA〉 ; 〈xC,xB〉 ; 〈xC,xC〉 ; 〈xC,xD〉 ; 〈xC,xE〉 ; 〈xC,xF〉 ]
58 @[   〈xD,x0〉 ; 〈xD,x1〉 ; 〈xD,x2〉 ; 〈xD,x3〉 ; 〈xD,x4〉 ; 〈xD,x5〉 ; 〈xD,x6〉 ; 〈xD,x7〉
59  ; 〈xD,x8〉 ; 〈xD,x9〉 ; 〈xD,xA〉 ; 〈xD,xB〉 ; 〈xD,xC〉 ; 〈xD,xD〉 ; 〈xD,xE〉 ; 〈xD,xF〉 ]
60 @[   〈xE,x0〉 ; 〈xE,x1〉 ; 〈xE,x2〉 ; 〈xE,x3〉 ; 〈xE,x4〉 ; 〈xE,x5〉 ; 〈xE,x6〉 ; 〈xE,x7〉
61  ; 〈xE,x8〉 ; 〈xE,x9〉 ; 〈xE,xA〉 ; 〈xE,xB〉 ; 〈xE,xC〉 ; 〈xE,xD〉 ; 〈xE,xE〉 ; 〈xE,xF〉 ]
62 @[   〈xF,x0〉 ; 〈xF,x1〉 ; 〈xF,x2〉 ; 〈xF,x3〉 ; 〈xF,x4〉 ; 〈xF,x5〉 ; 〈xF,x6〉 ; 〈xF,x7〉
63  ; 〈xF,x8〉 ; 〈xF,x9〉 ; 〈xF,xA〉 ; 〈xF,xB〉 ; 〈xF,xC〉 ; 〈xF,xD〉 ; 〈xF,xE〉 ; 〈xF,xF〉
64  ].
65
66 (*
67    1) mTest_x_RAM : inizio della RAM
68        (start point per caricamento mTest_bytes in RAM) 
69    2) mTest_x_prog: inizio della ROM
70        (start point per caricamento programma in ROM)
71    3) mTest_x_data: ultimi 256b della ROM
72        (start point per caricamento mTest_bytes in ROM)
73 *)
74 ndefinition mTest_HCS08_RAM ≝ 〈〈x0,x0〉:〈x7,x0〉〉.
75 ndefinition mTest_HCS08_prog ≝ 〈〈x1,x8〉:〈x6,x0〉〉.
76 ndefinition mTest_HCS08_data ≝ 〈〈xF,xF〉:〈x0,x0〉〉.
77
78 ndefinition mTest_RS08_RAM ≝ 〈〈x0,x0〉:〈x2,x0〉〉.
79 ndefinition mTest_RS08_prog ≝ 〈〈x3,x8〉:〈x0,x0〉〉.
80 ndefinition mTest_RS08_data ≝ 〈〈x3,xF〉:〈x0,x0〉〉.
81
82 ndefinition mTest_HCS08_ADC_source ≝ let m ≝ HCS08 in source_to_byte8 m (
83 (* testa la logica di ADC e le modalita' IMM1,DIR1/2,IX0/1/2,SP1/2 *)
84 (* BEFORE: A=0x00 H:X=0xFF50 PC=0x1860 SP=0x0110 C=true *)
85 (* [0x1860] 2clk *) (compile m ? ADC (maIMM1 〈xA,xA〉) I) @           (* AFTER1: imm1=0xAA quindi 0x00+imm1+true=A:0xAB C:false *)
86 (* [0x1862] 3clk *) (compile m ? ADC (maDIR1 〈xF,xF〉) I) @           (* AFTER2: dir1=[0x00FF]=0x8F quindi 0xAB+dir1+false=A:0x3A C:true *)
87 (* [0x1864] 4clk *) (compile m ? ADC (maDIR2 〈〈xF,xF〉:〈x1,x1〉〉) I) @ (* AFTER3: dir2=[0xFF11]=0x11 quindi 0x3A+dir2+true=A:0x4C C:false *)
88 (* [0x1867] 4clk *) (compile m ? ADC (maIX2 〈〈xF,xF〉:〈xF,x0〉〉) I) @  (* AFTER4: ix2=[X+0xFFF0]=[0xFF40]=0x40 quindi 0x4C+ix2+false=A:0x8C C:false *)
89 (* [0x186A] 3clk *) (compile m ? ADC (maIX1 〈x2,x4〉) I) @            (* AFTER5: ix1=[X+0x0024]=[0xFF74]=0x74 quindi 0x8C+ix1+false=A:0x00 C:true *)
90 (* [0x186C] 3clk *) (compile m ? ADC maIX0 I) @                      (* AFTER6: ix0=[X]=[0xFF50]=0x50 quindi 0x00+ix0+true=A:0x51 C:false *)
91 (* [0x186D] 5clk *) (compile m ? ADC (maSP2 〈〈xF,xF〉:〈x6,x1〉〉) I) @  (* AFTER7: sp2=[SP+0xFF61]=[0x0071]=0x01 quindi 0x51+sp2+false=A:0x52 C:false *)
92 (* [0x1871] 4clk *) (compile m ? ADC (maSP1 〈x2,x4〉) I)              (* AFTER8: sp1=[SP+0x0024]=[0x0134]=0xC4 quindi 0x52+sp1+false=A:0x16 C:true *)
93 (* [0x1874] si puo' quindi enunciare che dopo 2+3+4+4+3+3+5+4=28 clk *)
94 (*          A<-0x16 PC<-0x1874 *)
95 ).
96
97 (* creazione del processore+caricamento+impostazione registri *)
98 ndefinition mTest_HCS08_ADC_status ≝
99 λt:memory_impl.
100  set_c_flag HCS08 t (* C<-true *)
101   (setweak_sp_reg HCS08 t (* SP<-0x0110 *)
102    (setweak_indX_16_reg HCS08 t (* H:X<-0xFF50 *)
103     (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *)
104      (start_of_mcu_version_HCS08
105       MC9S08AW60 t
106       (load_from_source_at t (* carica mTest_bytes in ROM:mTest_HCS08_data *)
107        (load_from_source_at t (* carica mTest_bytes in RAM:mTest_HCS08_RAM *)
108         (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_HCS08_prog *)
109           mTest_HCS08_ADC_source mTest_HCS08_prog)
110          mTest_bytes mTest_HCS08_RAM)
111         mTest_bytes mTest_HCS08_data)
112       (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08AW60) t)
113       (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
114       false false false false false false) (* non deterministici tutti a 0 *)
115      mTest_HCS08_prog)
116     (mk_word16 〈xF,xF〉 〈x5,x0〉))
117    (mk_word16 〈x0,x1〉 〈x1,x0〉))
118   true.
119
120 (* dimostrazione senza svolgimento degli stati, immediata *)
121 nlemma ok_mTest_HCS08_ADC_full :
122  ∀t:memory_impl.
123  execute HCS08 t (TickOK ? (mTest_HCS08_ADC_status t)) nat28 =
124  (* NB: V,N,Z sono tornati false C e' tornato true *)
125  TickOK ? (set_pc_reg HCS08 t (* nuovo PC *)
126            (set_acc_8_low_reg HCS08 t (mTest_HCS08_ADC_status t) 〈x1,x6〉) (* nuovo A *)
127             (mk_word16 〈x1,x8〉 〈x7,x4〉)).
128  #t; nelim t;
129  (* esempio per svoglimento degli stati manualmente
130  [ 1:
131   letin BEFORE ≝ (get_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC));
132   normalize in BEFORE:(%);
133
134  letin AFTER_ALU1 ≝ (match execute HCS08 MEM_FUNC (TickOK ? (mTest_HCS08_ADC_status MEM_FUNC)) 2 with
135   [ TickERR _ _ ⇒ BEFORE 
136   | TickSUSP _ _ ⇒ BEFORE 
137   | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]);
138  normalize in AFTER_ALU1:(%);
139
140  letin AFTER_ALU2 ≝ (match execute HCS08 MEM_FUNC (TickOK ? 
141                      (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU1)) 3 with
142   [ TickERR _ _ ⇒ BEFORE 
143   | TickSUSP _ _ ⇒ BEFORE 
144   | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]);
145  normalize in AFTER_ALU2:(%);
146
147   letin AFTER_ALU3 ≝ (match execute HCS08 MEM_FUNC (TickOK ? 
148                      (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU2)) 4 with
149   [ TickERR _ _ ⇒ BEFORE 
150   | TickSUSP _ _ ⇒ BEFORE 
151   | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]);
152  normalize in AFTER_ALU3:(%);  
153
154  letin AFTER_ALU4 ≝ (match execute HCS08 MEM_FUNC (TickOK ? 
155                      (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU3)) 4 with
156   [ TickERR _ _ ⇒ BEFORE 
157   | TickSUSP _ _ ⇒ BEFORE 
158   | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]);
159  normalize in AFTER_ALU4:(%); 
160
161  letin AFTER_ALU5 ≝ (match execute HCS08 MEM_FUNC (TickOK ? 
162                      (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU4)) 3 with
163   [ TickERR _ _ ⇒ BEFORE 
164   | TickSUSP _ _ ⇒ BEFORE 
165   | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]);
166  normalize in AFTER_ALU5:(%); 
167
168  letin AFTER_ALU6 ≝ (match execute HCS08 MEM_FUNC (TickOK ? 
169                      (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU5)) 3 with
170   [ TickERR _ _ ⇒ BEFORE 
171   | TickSUSP _ _ ⇒ BEFORE 
172   | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]);
173  normalize in AFTER_ALU6:(%); 
174
175  letin AFTER_ALU7 ≝ (match execute HCS08 MEM_FUNC (TickOK ? 
176                      (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU6)) 5 with
177   [ TickERR _ _ ⇒ BEFORE 
178   | TickSUSP _ _ ⇒ BEFORE 
179   | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]);
180  normalize in AFTER_ALU7:(%); 
181
182  letin AFTER_ALU8 ≝ (match execute HCS08 MEM_FUNC (TickOK ? 
183                      (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU7)) 4 with
184   [ TickERR _ _ ⇒ BEFORE
185   | TickSUSP _ _ ⇒ BEFORE
186   | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]);
187  normalize in AFTER_ALU8:(%); *) 
188
189  napply refl_eq.
190 nqed.
191
192 (* -------------------------------------
193
194 (* ********* *)
195 (* HCS08 MOV *)
196 (* ********* *)
197
198 (*
199 definition mTest_HCS08_MOV_source ≝ let m ≝ HCS08 in source_to_byte8 m (
200 (* testa la logica di MOV e le modalita' xxx_to_xxx *)
201 (* BEFORE: H:X=0x0071 PC=0x1860 *)
202 (* [0x1860] 4clk *) (compile m ? MOV (maIMM1_to_DIR1 〈x3,xA〉 〈x7,x0〉) I) @ (* 0x3A in [0x0070] *)
203 (* [0x1863] 5clk *) (compile m ? MOV (maDIR1_to_DIR1 〈x7,x0〉 〈x7,x1〉) I) @ (* [0x0070] in [0x0071] *)
204 (* [0x1866] 5clk *) (compile m ? MOV (maIX0p_to_DIR1 〈x7,x2〉) I) @         (* [X++=0x0071] in [0x0072] *)
205 (* [0x1868] 5clk *) (compile m ? MOV (maDIR1_to_IX0p 〈x7,x2〉) I)           (* [0x0072] in [X++=0x0072] *)
206 (* [0x186A] si puo' quindi enunciare che dopo 4+5+5+5=19 clk *)
207 (*          PC<-0x186A X<-0x0073 *)
208 ).
209
210 (* creazione del processore+caricamento+impostazione registri *)
211 definition mTest_HCS08_MOV_status ≝
212 λt:memory_impl.
213 λb1,b2,b3:byte8.
214  setweak_indX_16_reg HCS08 t (* H:X<-0x0071 *)
215   (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *)
216    (start_of_mcu_version_HCS08
217     MC9S08AW60 t
218     (load_from_source_at t (* carica b1-3 in RAM:mTest_HCS08_RAM *)
219      (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_HCS08_prog *)
220        mTest_HCS08_MOV_source mTest_HCS08_prog)
221      [ b1 ; b2 ; b3 ] mTest_HCS08_RAM)
222     (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08AW60) t)
223     (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
224     false false false false false false) (* non deterministici tutti a 0 *)
225    mTest_HCS08_prog)
226   (mk_word16 〈x0,x0〉 〈x7,x1〉).
227
228 (* dimostrazione senza svolgimento degli stati, immediata *)
229 (* NB: la memoria e' cambiata e bisogna applicare eq_status *)
230 lemma ok_mTest_HCS08_MOV_full :
231 ∀t:memory_impl.
232  eq_status HCS08 t
233   (match execute HCS08 t (TickOK ? (mTest_HCS08_MOV_status t 〈x0,x0〉 〈x0,x0〉 〈x0,x0〉)) 19
234    with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
235   (setweak_indX_16_reg HCS08 t (* H:X *) 
236    (set_pc_reg HCS08 t (mTest_HCS08_MOV_status t 〈x3,xA〉 〈x3,xA〉 〈x3,xA〉) (* PC *)
237     (mk_word16 〈x1,x8〉 〈x6,xA〉))
238      (mk_word16 〈x0,x0〉 〈x7,x3〉))
239   [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] = true.
240  intro; 
241  apply (eq_to_eqstatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] HCS08 t
242         (match execute HCS08 t (TickOK ? (mTest_HCS08_MOV_status t 〈x0,x0〉 〈x0,x0〉 〈x0,x0〉)) 19
243          with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
244         (setweak_indX_16_reg HCS08 t (* H:X *) 
245          (set_pc_reg HCS08 t (mTest_HCS08_MOV_status t 〈x3,xA〉 〈x3,xA〉 〈x3,xA〉) (* PC *)
246           (mk_word16 〈x1,x8〉 〈x6,xA〉))
247            (mk_word16 〈x0,x0〉 〈x7,x3〉)));
248  elim t;
249  [ 1,2,3: normalize in ⊢ (? ? ? %); reflexivity
250  | 4,5,6: normalize in ⊢ (? ? ? %); reflexivity
251  | 7,8,9: normalize; reflexivity
252  ].
253 qed.
254
255 (* ************* *)
256 (* HCS08 ROL/ROR *)
257 (* ************* *)
258
259 definition mTest_HCS08_ROL_ROR_source ≝ let m ≝ HCS08 in source_to_byte8 m (
260 (* testa la logica di ROL/ROR e le modalita' IMM2,INHx *)
261 (* BEFORE: A=0x00 H:X=0x0000 PC=0x1860 Z=true *)
262 (* [0x1860] 3clk *) (compile m ? LDHX (maIMM2 〈〈x1,x2〉:〈x3,x4〉〉) I) @
263 (* [0x1863] 2clk *) (compile m ? LDA (maIMM1 〈x5,x6〉) I) @
264 (* [0x1865] 1clk *) (compile m ? ROL maINHA I) @
265 (* [0x1866] 1clk *) (compile m ? ROL maINHX I) @
266 (* [0x1867] 1clk *) (compile m ? ROR maINHA I) @
267 (* [0x1868] 1clk *) (compile m ? ROR maINHX I) @
268 (* [0x1869] 1clk *) (compile m ? CLR maINHA I) @
269 (* [0x186A] 1clk *) (compile m ? CLR maINHX I) @
270 (* [0x186B] 1clk *) (compile m ? CLR maINHH I)
271 (* [0x186C] si puo' quindi enunciare che dopo 3+2+1+1+1+1+1+1+1=12 clk *)
272 (*          PC<-0x186C *)
273 ).
274
275 (* creazione del processore+caricamento+impostazione registri *)
276 definition mTest_HCS08_ROL_ROR_status ≝
277 λt:memory_impl.
278  set_z_flag HCS08 t (* Z<-true *)
279   (setweak_indX_16_reg HCS08 t (* H:X<-0x0000 *)
280    (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *)
281     (start_of_mcu_version_HCS08
282      MC9S08AW60 t
283      (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_HCS08_prog *)
284       mTest_HCS08_ROL_ROR_source mTest_HCS08_prog)
285      (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08AW60) t)
286      (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
287      false false false false false false) (* non deterministici tutti a 0 *)
288     mTest_HCS08_prog)
289    (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)))
290   true.
291
292 (* dimostrazione senza svolgimento degli stati, immediata *)
293 lemma ok_mTest_HCS08_ROL_ROR_full :
294  ∀t:memory_impl.
295  execute HCS08 t (TickOK ? (mTest_HCS08_ROL_ROR_status t)) 12 =
296  TickOK ? (set_pc_reg HCS08 t (* nuovo PC *)
297            (mTest_HCS08_ROL_ROR_status t) (mk_word16 〈x1,x8〉 〈x6,xC〉)).
298  intro;
299  elim t;
300  reflexivity.
301 qed.
302
303 (* **************** *)
304 (* HCS08 CBEQx/DBNZ *)
305 (* **************** *)
306
307 definition mTest_HCS08_CBEQ_DBNZ_source ≝ let m ≝ HCS08 in source_to_byte8 m (
308 (* testa la logica di CBEQx/DBNZ e le modalita' xxx_and_IMM1 *)
309 (* BEFORE: H:X=0x006F SP=0x006F PC=0x1860 *)
310 (* [0x1860] 5clk *) (compile m ? CBEQA (maDIR1_and_IMM1 〈x7,x1〉 〈x0,x1〉) I) @
311 (* [0x1863] 1clk *) (compile m ? NOP maINH I) @                               (* eseguito: A≠[0x0071]=0x01 *)
312 (* [0x1864] 4clk *) (compile m ? CBEQA (maIMM1_and_IMM1 〈x0,x0〉 〈x0,x1〉) I) @
313 (* [0x1867] 1clk *) (compile m ? NOP maINH I) @                               (* non eseguito: A=0x00 *)
314 (* [0x1868] 4clk *) (compile m ? CBEQX (maIMM1_and_IMM1 〈x6,xF〉 〈x0,x1〉) I) @
315 (* [0x186B] 1clk *) (compile m ? NOP maINH I) @                               (* non eseguito: X=0x6F *)
316 (* [0x186C] 5clk *) (compile m ? CBEQA (maIX1p_and_IMM1 〈x0,x1〉 〈x0,x1〉) I) @ (* H:X++ *)
317 (* [0x186F] 1clk *) (compile m ? NOP maINH I) @                               (* non eseguito: A=[X+0x01]=[0x0070]=0x00 *)
318 (* [0x1870] 5clk *) (compile m ? CBEQA (maIX0p_and_IMM1 〈x0,x1〉) I) @         (* H:X++ *)
319 (* [0x1872] 1clk *) (compile m ? NOP maINH I) @                               (* non eseguito: A=[X]=[0x0070]=0x00 *)
320 (* [0x1873] 6clk *) (compile m ? CBEQA (maSP1_and_IMM1 〈x0,x2〉 〈x0,x1〉) I) @
321 (* [0x1877] 1clk *) (compile m ? NOP maINH I) @                               (* eseguito: A≠[SP+0x02]=[0x0071]=0x01 *)
322
323 (* [0x1878] 7clk *) (compile m ? DBNZ (maDIR1_and_IMM1 〈x7,x2〉 〈x0,x1〉) I) @
324 (* [0x187B] 1clk *) (compile m ? NOP maINH I) @                               (* non eseguito: --[0x0072]=0x01≠0 *)
325 (* [0x187C] 4clk *) (compile m ? DBNZ (maINHA_and_IMM1 〈x0,x1〉) I) @
326 (* [0x187E] 1clk *) (compile m ? NOP maINH I) @                               (* non eseguito: --A=0xFF≠0 *)
327 (* [0x187F] 4clk *) (compile m ? DBNZ (maINHX_and_IMM1 〈x0,x1〉) I) @
328 (* [0x1881] 1clk *) (compile m ? NOP maINH I) @                               (* non eseguito: --X=0x70≠0 *)
329 (* [0x1882] 7clk *) (compile m ? DBNZ (maIX1_and_IMM1 〈x0,x2〉 〈x0,x1〉) I) @
330 (* [0x1885] 1clk *) (compile m ? NOP maINH I) @                               (* eseguito: --[X+0x02]=[0x0072]=0x00=0 *)
331 (* [0x1886] 6clk *) (compile m ? DBNZ (maIX0_and_IMM1 〈x0,x1〉) I) @
332 (* [0x1888] 1clk *) (compile m ? NOP maINH I) @                               (* non eseguito: --[X]=[0x0070]=0xFF≠0 *)
333 (* [0x1889] 8clk *) (compile m ? DBNZ (maSP1_and_IMM1 〈x0,x1〉 〈x0,x1〉) I) @ 
334 (* [0x188D] 1clk *) (compile m ? NOP maINH I)                                 (* non eseguito: --[SP+0x01]=[0x0070]=0xFE≠0 *)
335 (* [0x188E] si puo' quindi enunciare che dopo 5+1+4+4+5+5+6+1 (31)
336                                               7+4+4+7+1+6+8   (37) =68 clk *)
337 (*          A<-0xFF PC<-0x188E H:X<-0070 *)
338 ).
339
340 (* creazione del processore+caricamento+impostazione registri *)
341 definition mTest_HCS08_CBEQ_DBNZ_status ≝
342 λt:memory_impl.
343 λb1,b2,b3:byte8.
344  setweak_sp_reg HCS08 t (* SP<-0x006F *)
345   (setweak_indX_16_reg HCS08 t (* H:X<-0x006F *)
346    (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *)
347     (start_of_mcu_version_HCS08
348      MC9S08AW60 t
349      (load_from_source_at t (* carica b1-3 in RAM:mTest_HCS08_RAM *)
350       (load_from_source_at t (* carica mTest_bytes in RAM:mTest_HCS08_RAM *)
351        (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_HCS08_prog *)
352          mTest_HCS08_CBEQ_DBNZ_source mTest_HCS08_prog)
353         mTest_bytes mTest_HCS08_RAM)
354        [ b1 ; b2 ; b3 ] mTest_HCS08_RAM)
355      (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08AW60) t)
356      (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
357      false false false false false false) (* non deterministici tutti a 0 *)
358     mTest_HCS08_prog)
359    (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x6 xF)))
360   (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x6 xF)).
361
362 (* dimostrazione senza svolgimento degli stati, immediata *)
363 (* NB: la memoria e' cambiata e bisogna applicare eq_status *)
364 lemma ok_mTest_HCS08_CBEQ_DBNZ_full :
365 ∀t:memory_impl.
366  eq_status HCS08 t
367   (match execute HCS08 t (TickOK ? (mTest_HCS08_CBEQ_DBNZ_status t 〈x0,x0〉 〈x0,x1〉 〈x0,x2〉)) 68
368    with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
369   (set_acc_8_low_reg HCS08 t (* nuovo A *)
370    (set_pc_reg HCS08 t (* nuovo PC *)
371     (setweak_indX_16_reg HCS08 t (mTest_HCS08_CBEQ_DBNZ_status t 〈xF,xE〉 〈x0,x1〉 〈x0,x0〉) (* nuovo H:X *)
372      (mk_word16 〈x0,x0〉 〈x7,x0〉))
373     (mk_word16 〈x1,x8〉 〈x8,xE〉))
374    (mk_byte8 xF xF))
375   [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] = true.
376  intro; 
377  apply (eq_to_eqstatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] HCS08 t
378         (match execute HCS08 t (TickOK ? (mTest_HCS08_CBEQ_DBNZ_status t 〈x0,x0〉 〈x0,x1〉 〈x0,x2〉)) 68
379          with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
380         (set_acc_8_low_reg HCS08 t (* nuovo A *)
381          (set_pc_reg HCS08 t (* nuovo PC *)
382           (setweak_indX_16_reg HCS08 t (mTest_HCS08_CBEQ_DBNZ_status t 〈xF,xE〉 〈x0,x1〉 〈x0,x0〉) (* nuovo H:X *)
383            (mk_word16 〈x0,x0〉 〈x7,x0〉))
384           (mk_word16 〈x1,x8〉 〈x8,xE〉))
385          (mk_byte8 xF xF)));
386  elim t;
387  [ 1,2,3: normalize in ⊢ (? ? ? %); reflexivity
388  | 4,5,6: normalize in ⊢ (? ? ? %); reflexivity
389  | 7,8,9: normalize; reflexivity
390  ].
391 qed.
392
393 (* ***************** *)
394 (* HCS08 BSETn/BCLRn *)
395 (* ***************** *)
396
397 definition mTest_HCS08_BSETn_BCLRn_source ≝ let m ≝ HCS08 in source_to_byte8 m (
398 (* testa la logica di BSETn/BCLRn e le modalita' DIRn *)
399 (* BEFORE: PC=0x1860 *)
400 (* [0x1860] 5clk *) (compile m ? BSETn (maDIRn o0 〈x7,x0〉) I) @ (* [0x0070]=0x01 *)
401 (* [0x1862] 5clk *) (compile m ? BSETn (maDIRn o1 〈x7,x0〉) I) @ (* [0x0070]=0x03 *)
402 (* [0x1864] 5clk *) (compile m ? BSETn (maDIRn o2 〈x7,x0〉) I) @ (* [0x0070]=0x07 *)
403 (* [0x1866] 5clk *) (compile m ? BSETn (maDIRn o3 〈x7,x0〉) I) @ (* [0x0070]=0x0F *)
404 (* [0x1868] 5clk *) (compile m ? BSETn (maDIRn o4 〈x7,x0〉) I) @ (* [0x0070]=0x1F *)
405 (* [0x186A] 5clk *) (compile m ? BSETn (maDIRn o5 〈x7,x0〉) I) @ (* [0x0070]=0x3F *)
406 (* [0x186C] 5clk *) (compile m ? BSETn (maDIRn o6 〈x7,x0〉) I) @ (* [0x0070]=0x7F *)
407 (* [0x186E] 5clk *) (compile m ? BSETn (maDIRn o7 〈x7,x0〉) I) @ (* [0x0070]=0xFF *)
408
409 (* [0x1870] 5clk *) (compile m ? BCLRn (maDIRn o0 〈x7,x0〉) I) @ (* [0x0070]=0xFE *)
410 (* [0x1872] 5clk *) (compile m ? BCLRn (maDIRn o1 〈x7,x0〉) I) @ (* [0x0070]=0xFC *)
411 (* [0x1874] 5clk *) (compile m ? BCLRn (maDIRn o2 〈x7,x0〉) I) @ (* [0x0070]=0xF8 *)
412 (* [0x1876] 5clk *) (compile m ? BCLRn (maDIRn o3 〈x7,x0〉) I) @ (* [0x0070]=0xF0 *)
413 (* [0x1878] 5clk *) (compile m ? BCLRn (maDIRn o4 〈x7,x0〉) I) @ (* [0x0070]=0xE0 *)
414 (* [0x187A] 5clk *) (compile m ? BCLRn (maDIRn o5 〈x7,x0〉) I) @ (* [0x0070]=0xC0 *)
415 (* [0x187C] 5clk *) (compile m ? BCLRn (maDIRn o6 〈x7,x0〉) I) @ (* [0x0070]=0x80 *)
416 (* [0x187E] 5clk *) (compile m ? BCLRn (maDIRn o7 〈x7,x0〉) I)   (* [0x0070]=0x00 *)
417 (* [0x1880] si puo' quindi enunciare che dopo 5+5+5+5+5+5+5+5
418                                               5+5+5+5+5+5+5+5 =80 clk *)
419 (*          PC<-0x1880 *)
420 ).
421
422 (* creazione del processore+caricamento+impostazione registri *)
423 definition mTest_HCS08_BSETn_BCLRn_status ≝
424 λt:memory_impl.
425 λb1:byte8.
426  set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *)
427   (start_of_mcu_version_HCS08
428    MC9S08AW60 t
429    (load_from_source_at t (* carica b1 in RAM:mTest_HCS08_RAM *)
430     (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_HCS08_prog *)
431       mTest_HCS08_BSETn_BCLRn_source mTest_HCS08_prog)
432      [ b1 ] mTest_HCS08_RAM)
433    (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08AW60) t)
434    (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
435    false false false false false false) (* non deterministici tutti a 0 *)
436   mTest_HCS08_prog.
437
438 (* dimostrazione senza svolgimento degli stati, immediata *)
439 (* NB: la memoria e' cambiata e bisogna applicare eq_status *)
440 lemma ok_mTest_HCS08_BSETn_BCLRn_full :
441 ∀t:memory_impl.
442  eq_status HCS08 t
443   (match execute HCS08 t (TickOK ? (mTest_HCS08_BSETn_BCLRn_status t 〈x0,x0〉)) 80
444    with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
445   (set_pc_reg HCS08 t (mTest_HCS08_BSETn_BCLRn_status t 〈x0,x0〉) 〈〈x1,x8〉:〈x8,x0〉〉 (* nuovo PC *))
446   [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] = true.
447  intro; 
448  apply (eq_to_eqstatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] HCS08 t
449         (match execute HCS08 t (TickOK ? (mTest_HCS08_BSETn_BCLRn_status t 〈x0,x0〉)) 80
450          with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
451         (set_pc_reg HCS08 t (mTest_HCS08_BSETn_BCLRn_status t 〈x0,x0〉) 〈〈x1,x8〉:〈x8,x0〉〉 (* nuovo PC *)));
452  elim t;
453  [ 1,2,3: normalize in ⊢ (? ? ? %); reflexivity
454  | 4,5,6: normalize in ⊢ (? ? ? %); reflexivity
455  | 7,8,9: normalize; reflexivity
456  ].
457 qed.
458
459 (* ******************* *)
460 (* HCS08 BRSETn/BRCLRn *)
461 (* ******************* *)
462
463 definition mTest_HCS08_BRSETn_BRCLRn_source ≝ let m ≝ HCS08 in source_to_byte8 m (
464 (* testa la logica di BRSETn/BRCLRn e le modalita' DIRn_and_IMM1 *)
465 (* BEFORE: va a testare [0x00C5]=0x55 PC=0x1860 *)
466 (* [0x1860] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o0 〈xC,x5〉 〈x0,x1〉) I) @
467 (* [0x1863] 1clk *) (compile m ? NOP maINH I) @
468 (* [0x1864] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o1 〈xC,x5〉 〈x0,x1〉) I) @
469 (* [0x1867] 1clk *) (compile m ? NOP maINH I) @
470 (* [0x1868] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o2 〈xC,x5〉 〈x0,x1〉) I) @
471 (* [0x186B] 1clk *) (compile m ? NOP maINH I) @
472 (* [0x186C] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o3 〈xC,x5〉 〈x0,x1〉) I) @
473 (* [0x186F] 1clk *) (compile m ? NOP maINH I) @
474 (* [0x1870] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o4 〈xC,x5〉 〈x0,x1〉) I) @
475 (* [0x1873] 1clk *) (compile m ? NOP maINH I) @
476 (* [0x1874] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o5 〈xC,x5〉 〈x0,x1〉) I) @
477 (* [0x1877] 1clk *) (compile m ? NOP maINH I) @
478 (* [0x1878] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o6 〈xC,x5〉 〈x0,x1〉) I) @
479 (* [0x187B] 1clk *) (compile m ? NOP maINH I) @
480 (* [0x187C] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o7 〈xC,x5〉 〈x0,x1〉) I) @
481 (* [0x187F] 1clk *) (compile m ? NOP maINH I) @
482
483 (* [0x1880] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o0 〈xC,x5〉 〈x0,x1〉) I) @
484 (* [0x1883] 1clk *) (compile m ? NOP maINH I) @
485 (* [0x1884] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o1 〈xC,x5〉 〈x0,x1〉) I) @
486 (* [0x1887] 1clk *) (compile m ? NOP maINH I) @
487 (* [0x1888] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o2 〈xC,x5〉 〈x0,x1〉) I) @
488 (* [0x188B] 1clk *) (compile m ? NOP maINH I) @
489 (* [0x188C] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o3 〈xC,x5〉 〈x0,x1〉) I) @
490 (* [0x188F] 1clk *) (compile m ? NOP maINH I) @
491 (* [0x1890] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o4 〈xC,x5〉 〈x0,x1〉) I) @
492 (* [0x1893] 1clk *) (compile m ? NOP maINH I) @
493 (* [0x1894] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o5 〈xC,x5〉 〈x0,x1〉) I) @
494 (* [0x1897] 1clk *) (compile m ? NOP maINH I) @
495 (* [0x1898] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o6 〈xC,x5〉 〈x0,x1〉) I) @
496 (* [0x189B] 1clk *) (compile m ? NOP maINH I) @
497 (* [0x189C] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o7 〈xC,x5〉 〈x0,x1〉) I) @
498 (* [0x189F] 1clk *) (compile m ? NOP maINH I)
499
500 (* [0x18A0] si puo' quindi enunciare che dopo 80+8=88 clk
501             (vengono eseguiti 16*5 test, meta' BRSETn/BRCLRn saltano *) 
502 (*          PC<-0x18A0 *)
503 ).
504
505 (* creazione del processore+caricamento+impostazione registri *)
506 definition mTest_HCS08_BRSETn_BRCLRn_status ≝
507 λt:memory_impl.
508  set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *)
509   (start_of_mcu_version_HCS08
510    MC9S08AW60 t
511    (load_from_source_at t
512     (load_from_source_at t (zero_memory t) (* carica mTest_bytes in RAM:mTest_HCS08_RAM *)
513       mTest_HCS08_BRSETn_BRCLRn_source mTest_HCS08_prog) (* carica source in ROM:mTest_HCS08_prog *)
514      mTest_bytes mTest_HCS08_RAM)
515    (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08AW60) t)
516    (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
517    false false false false false false) (* non deterministici tutti a 0 *)
518   mTest_HCS08_prog.
519
520 (* dimostrazione senza svolgimento degli stati, immediata *)
521 lemma ok_mTest_HCS08_BRSETn_BRCLRn_full :
522  ∀t:memory_impl.
523  execute HCS08 t (TickOK ? (mTest_HCS08_BRSETn_BRCLRn_status t)) 88 =
524  TickOK ? (set_pc_reg HCS08 t (mTest_HCS08_BRSETn_BRCLRn_status t) (* nuovo PC *)
525            (mk_word16 〈x1,x8〉 〈xA,x0〉)).
526  intro;
527  elim t;
528  reflexivity.
529 qed.
530
531 (* *************** *)
532 (* RS08 X,D[X],TNY *)
533 (* *************** *)
534
535 definition mTest_RS08_TNY_source ≝ let m ≝ RS08 in source_to_byte8 m (
536 (* testa la logica RS08 X,D[X] le modalita' TNY *)
537 (* NB: il meccanismo utilizzato e' quello complesso dell'RS08
538        fare riferimento alle spiegazioni in STATUS/LOAD_WRITE *)
539 (* X=20 PS=0 *)
540 (* [0x3800] 3clk *) (compile m ? ADD (maTNY xD) I) @       (* ... +[0x000D]=0x0C *)
541 (* [0x3801] 3clk *) (compile m ? ADD (maTNY xE) I) @       (* ... +D[X]=[0x0020]=0x1F *)
542 (* [0x3802] 3clk *) (compile m ? ADD (maTNY xF) I) @       (* ... +X=0x20 *)
543 (* [0x3803] 3clk *) (compile m ? ADD (maDIR1 〈xC,xF〉) I) @ (* ... +X=0x20 *)
544 (* [0x3805] 3clk *) (compile m ? ADD (maDIR1 〈xC,xE〉) I)   (* ... +[0x000E]=0x0D *)
545 (* [0x3807] si puo' quindi enunciare che dopo 15 clk
546             A<-0x78 PC<-0x3807 *)
547 ).
548
549 (* creazione del processore+caricamento+impostazione registri *)
550 definition mTest_RS08_TNY_status ≝
551 λt:memory_impl.
552  setweak_x_map RS08 t (* X<-0x20 *)
553  (setweak_ps_map RS08 t (* PS<-0x00 *)
554  (set_pc_reg RS08 t (* PC<-mTest_RS08_prog *)
555   (start_of_mcu_version_RS08 
556    MC9RS08KA2 t
557    (load_from_source_at t (* carica mTest_bytes in RAM:mTest_RS08_RAM *)
558     (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_RS08_prog *)
559      mTest_RS08_TNY_source mTest_RS08_prog)
560     mTest_bytes 〈〈x0,x0〉:〈x0,x1〉〉)
561    (build_memory_type_of_mcu_version (FamilyRS08 MC9RS08KA2) t)
562    (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
563    false false false false false false (* non deterministici tutti a 0 *)
564    ) mTest_RS08_prog)
565   (mk_byte8 x0 x0))
566   (mk_byte8 x2 x0).
567
568 (* dimostrazione senza svolgimento degli stati, immediata *)
569 lemma ok_mTest_RS08_TNY_full :
570  ∀t:memory_impl.
571  execute RS08 t (TickOK ? (mTest_RS08_TNY_status t)) 15 =
572  TickOK ? (set_acc_8_low_reg RS08 t (* nuovo A *)
573            (set_pc_reg RS08 t (mTest_RS08_TNY_status t) (* nuovo PC *)
574             (mk_word16 〈x3,x8〉 〈x0,x7〉))
575              (mk_byte8 x7 x8)).
576  intro;
577  elim t;
578  reflexivity.
579 qed.
580
581 (* *********** *)
582 (* RS08 PS,SRT *)
583 (* *********** *)
584
585 definition mTest_RS08_SRT_source ≝ let m ≝ RS08 in source_to_byte8 m (
586 (* testa la logica RS08 PS le modalita' SRT *)
587 (* NB: il meccanismo utilizzato e' quello complesso dell'RS08
588        fare riferimento alle spiegazioni in STATUS/LOAD_WRITE *)
589 (* X=0x1F PS=0xFE Z=1 *)
590 (* [0x3800] 3clk *) (compile m ? LDA (maSRT t1F) I) @      (* A<-PS *)
591 (* [0x3801] 2clk *) (compile m ? SUB (maIMM1 〈xF,xE〉) I) @ (* risulta 0 *)
592 (* [0x3803] 3clk *) (compile m ? BEQ (maIMM1 〈x0,x1〉) I) @ (* salta *)
593 (* [0x3805] 1clk *) (compile m ? NOP maINH I) @ 
594
595 (* [0x3806] 3clk *) (compile m ? LDA (maSRT t0E) I) @      (* A<-PS *)
596 (* [0x3807] 2clk *) (compile m ? SUB (maIMM1 〈xF,xE〉) I) @ (* risulta 0 *)
597 (* [0x3809] 3clk *) (compile m ? BEQ (maIMM1 〈x0,x1〉) I) @ (* salta *)
598 (* [0x380B] 1clk *) (compile m ? NOP maINH I) @
599
600 (* [0x380C] 3clk *) (compile m ? LDA (maDIR1 〈xC,x3〉) I) @ (* A<-[0x00C3]=[0x3F83]=0x83 *)
601 (* [0x380E] 2clk *) (compile m ? SUB (maIMM1 〈x8,x3〉) I) @ (* risulta 0 *)
602 (* [0x3810] 3clk *) (compile m ? BEQ (maIMM1 〈x0,x1〉) I) @ (* salta *)
603 (* [0x3812] 1clk *) (compile m ? NOP maINH I)
604 (* [0x3813] si puo' quindi enunciare che dopo 24 clk
605             PC<-0x3813 *)
606 ).
607
608 (* creazione del processore+caricamento+impostazione registri *)
609 definition mTest_RS08_SRT_status ≝
610 λt:memory_impl.
611  setweak_x_map RS08 t (* X<-0x1F *)
612   (setweak_ps_map RS08 t (* PS<-0xFE *)
613    (set_z_flag RS08 t (* Z<-true *)
614     (set_pc_reg RS08 t (* PC<-mTest_RS08_prog *)
615      (start_of_mcu_version_RS08
616       MC9RS08KA2 t
617        (load_from_source_at t (* carica mTest_bytes in ROM:mTest_RS08_data *)
618         (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_RS08_prog *)
619          mTest_RS08_SRT_source mTest_RS08_prog)
620         mTest_bytes mTest_RS08_data)
621        (build_memory_type_of_mcu_version (FamilyRS08 MC9RS08KA2) t)
622       (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
623       false false false false false false (* non deterministici tutti a 0 *)
624       ) mTest_RS08_prog)
625      true)
626     (mk_byte8 xF xE))
627    (mk_byte8 x1 xF).
628
629 (* dimostrazione senza svolgimento degli stati, immediata *)
630 lemma ok_mTest_RS08_SRT_full :
631  ∀t:memory_impl.
632  execute RS08 t (TickOK ? (mTest_RS08_SRT_status t)) 24 =
633  TickOK ? (set_pc_reg RS08 t (mTest_RS08_SRT_status t) (* nuovo PC *)
634            (mk_word16 〈x3,x8〉 〈x1,x3〉)).
635  intro;
636  elim t;
637  reflexivity.
638 qed.
639
640 (* ********************* *)
641 (* TEOREMA MULT PER RS08 *)
642 (* ********************* *)
643
644 definition mTest_RS08_mult_source ≝ let m ≝ RS08 in source_to_byte8 m (
645 (* 
646    ZH:ZL=X*Y con [0x0020-0x004F] X ≝ [0x0020] Y ≝ [0x0021] ZH ≝ [0x0022] ZL ≝ [0x0023]
647 *)
648 (* [0x3800] ZH <- 0      3clk *) (compile m ? CLR (maDIR1 〈x2,x2〉) I) @
649 (* [0x3802] ZL <- 0      3clk *) (compile m ? CLR (maDIR1 〈x2,x3〉) I) @
650 (* [0x3804] (l1) A <- Y  3clk *) (compile m ? LDA (maDIR1 〈x2,x1〉) I) @
651 (* [0x3806] A=0 goto l2  3clk *) (compile m ? BEQ (maIMM1 〈x0,xE〉) I) @
652 (* [0x3808] A <- ZL      3clk *) (compile m ? LDA (maDIR1 〈x2,x3〉) I) @
653 (* [0x380A] Y --         5clk *) (compile m ? DEC (maDIR1 〈x2,x1〉) I) @
654 (* [0x380C] A += X       3clk *) (compile m ? ADD (maDIR1 〈x2,x0〉) I) @
655 (* [0x380E] C=0 goto l3  3clk *) (compile m ? BCC (maIMM1 〈x0,x2〉) I) @
656 (* [0x3810] ZH ++        5clk *) (compile m ? INC (maDIR1 〈x2,x2〉) I) @
657 (* [0x3812] (l3) ZL <- A 3clk *) (compile m ? STA (maDIR1 〈x2,x3〉) I) @
658 (* [0x3814] goto l1      3clk *) (compile m ? BRA (maIMM1 〈xE,xE〉) I)
659 (* [0x3816] (l2) si puo' quindi enunciare che
660                  - il caso base X * 0 richiede 12 cicli
661                  - bisogna aggiungere Y * 26 cicli, Y>0
662                  - bisogna aggiungere ZH * 5 cicli, X * Y > 0xFF *)
663 ).
664
665 (* creazione del processore+caricamento+impostazione registri *)
666 definition mTest_RS08_mult_status ≝
667 λt:memory_impl.
668 λb1,b2,b3,b4:byte8.
669  set_z_flag RS08 t (* Z<-true *)
670  (set_pc_reg RS08 t (* PC<-mTest_RS08_prog *)
671   (start_of_mcu_version_RS08 
672    MC9RS08KA2 t
673    (load_from_source_at t (* carica X,Y,ZH,ZL:mTest_RS08_RAM *)
674     (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_RS08_prog *)
675      mTest_RS08_mult_source mTest_RS08_prog)
676     [ b1 ; b2 ; b3 ; b4 ] mTest_RS08_RAM)
677    (build_memory_type_of_mcu_version (FamilyRS08 MC9RS08KA2) t)
678    (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
679    false false false false false false (* non deterministici tutti a 0 *)
680    ) mTest_RS08_prog)
681   true.
682
683 (* parametrizzazione dell'enunciato del teorema mult *)
684 (* NB: la memoria e' cambiata e bisogna applicare eq_status *)
685 definition ok_mTest_RS08_mult_full_aux ≝
686 λt:memory_impl.λX,Y:byte8.
687  eq_status RS08 t
688   (match execute RS08 t (TickOK ? (mTest_RS08_mult_status t X Y 〈x0,x0〉 〈x0,x0〉))
689                                   (12 + (26 * (nat_of_byte8 Y)) + (5 * (nat_of_byte8 (w16h (mul_b8 X Y)))))
690    (* FIXME: alla ALU azzero C perche' la funzione che ne descrive il valore finale e' MOLTO complessa *)
691    with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ set_c_flag RS08 t s false ])
692   (set_pc_reg RS08 t (mTest_RS08_mult_status t X 〈x0,x0〉 (w16h (mul_b8 X Y)) (w16l (mul_b8 X Y))) 〈〈x3,x8〉:〈x1,x6〉〉)
693   (* controllo che coincidano X,Y,ZH,ZL *)
694   [ 〈〈x0,x0〉:〈x2,x0〉〉 ; 〈〈x0,x0〉:〈x2,x1〉〉 ; 〈〈x0,x0〉:〈x2,x2〉〉 ; 〈〈x0,x0〉:〈x2,x3〉〉 ] = true.
695
696 lemma ok_mTest_RS08_mult_full : 
697 let X ≝ 〈xF,xF〉 in
698 let Y ≝ 〈x1,xE〉 in
699  ∀t:memory_impl.
700   ok_mTest_RS08_mult_full_aux t X Y.
701  unfold ok_mTest_RS08_mult_full_aux;
702  intros 3; 
703  apply (eq_to_eqstatus_weak [ 〈〈x0,x0〉:〈x2,x0〉〉 ; 〈〈x0,x0〉:〈x2,x1〉〉 ; 〈〈x0,x0〉:〈x2,x2〉〉 ; 〈〈x0,x0〉:〈x2,x3〉〉 ] RS08 t
704         (match execute RS08 t (TickOK ? (mTest_RS08_mult_status t X Y 〈x0,x0〉 〈x0,x0〉))
705                                         (12 + (26 * (nat_of_byte8 Y)) + (5 * (nat_of_byte8 (w16h (mul_b8 X Y)))))
706          with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ set_c_flag RS08 t s false ])
707         (set_pc_reg RS08 t (mTest_RS08_mult_status t X 〈x0,x0〉 (w16h (mul_b8 X Y)) (w16l (mul_b8 X Y))) 〈〈x3,x8〉:〈x1,x6〉〉));
708  elim t;
709  [ 1,2,3: normalize in ⊢ (? ? ? %); reflexivity
710  | 4,5,6: normalize in ⊢ (? ? ? %); reflexivity
711  | 7,8,9: normalize; reflexivity
712  ].
713 qed.
714
715 (* ************************ *)
716 (* TEST SU GRANULARITA' BIT *)
717 (* ************************ *)
718
719 definition mTest_bits_source ≝ let m ≝ HCS08 in source_to_byte8 m (
720 (* BEFORE: va a testare [0x0070]=0x00 *)
721 (* [0x1860] 4clk *) (compile m ? MOV (maIMM1_to_DIR1 〈xF,xF〉 〈x7,x0〉) I)
722 (* [0x1863] *)
723 ).
724
725 (* creazione del processore+caricamento+impostazione registri *)
726 definition mTest_bits_status ≝
727 λt:memory_impl.
728 λsub:oct.
729 λb:byte8.
730  setweak_n_flag HCS08 t (* N<-1 *)
731   (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *)
732    (start_of_mcu_version_HCS08
733     MC9S08AW60 t
734     (load_from_source_at t
735      (load_from_source_at t (zero_memory t) (* carica b in RAM:mTest_HCS08_RAM *)
736        mTest_bits_source mTest_HCS08_prog) (* carica source in ROM:mTest_HCS08_prog *)
737       [ b ] mTest_HCS08_RAM)
738     (check_update_bit t (* setta mTest_HCS08_RAM,o come ROM *)
739      (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08AW60) t)
740      mTest_HCS08_RAM sub MEM_READ_ONLY)
741     (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
742     false false false false false false) (* non deterministici tutti a 0 *)
743    mTest_HCS08_prog)
744   true.
745
746 (* dimostrazione senza svolgimento degli stati, immediata *)
747 lemma ok_mTest_bits_MEM_BITS_full :
748  ∀sub:oct.
749  execute HCS08 MEM_BITS (TickOK ? (mTest_bits_status MEM_BITS sub 〈x0,x0〉)) 4 =
750  TickOK ? (set_pc_reg HCS08 MEM_BITS (mTest_bits_status MEM_BITS sub (byte8_of_bits (setn_array8T sub ? (bits_of_byte8 〈xF,xF〉) false))) (* nuovo PC *)
751            (mk_word16 〈x1,x8〉 〈x6,x3〉)).
752  intro;
753  elim sub;
754  reflexivity.
755 qed.
756
757 (* NB: la memoria e' cambiata e bisogna applicare eq_status *)
758 lemma ok_mTest_bits_MEM_FUNC_full :
759 ∀sub:oct.
760  eq_status HCS08 MEM_FUNC
761   (match execute HCS08 MEM_FUNC (TickOK ? (mTest_bits_status MEM_FUNC sub 〈x0,x0〉)) 4
762    with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
763   (set_pc_reg HCS08 MEM_FUNC (mTest_bits_status MEM_FUNC sub 〈xF,xF〉) (* nuovo PC *) 〈〈x1,x8〉:〈x6,x3〉〉)
764   [ 〈〈x0,x0〉:〈x7,x0〉〉 ] = true.
765  intro; 
766  apply (eq_to_eqstatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ] HCS08 MEM_FUNC
767         (match execute HCS08 MEM_FUNC (TickOK ? (mTest_bits_status MEM_FUNC sub 〈x0,x0〉)) 4
768          with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
769         (set_pc_reg HCS08 MEM_FUNC (mTest_bits_status MEM_FUNC sub 〈xF,xF〉) (* nuovo PC *) 〈〈x1,x8〉:〈x6,x3〉〉));
770  normalize in ⊢ (? ? ? %);
771  reflexivity.
772 qed.
773
774 lemma ok_mTest_bits_MEM_TREE_full :
775 ∀sub:oct.
776  eq_status HCS08 MEM_TREE
777   (match execute HCS08 MEM_TREE (TickOK ? (mTest_bits_status MEM_TREE sub 〈x0,x0〉)) 4
778    with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
779   (set_pc_reg HCS08 MEM_TREE (mTest_bits_status MEM_TREE sub 〈xF,xF〉) (* nuovo PC *) 〈〈x1,x8〉:〈x6,x3〉〉)
780   [ 〈〈x0,x0〉:〈x7,x0〉〉 ] = true.
781  intro; 
782  apply (eq_to_eqstatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ] HCS08 MEM_TREE
783         (match execute HCS08 MEM_TREE (TickOK ? (mTest_bits_status MEM_TREE sub 〈x0,x0〉)) 4
784          with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
785         (set_pc_reg HCS08 MEM_TREE (mTest_bits_status MEM_TREE sub 〈xF,xF〉) (* nuovo PC *) 〈〈x1,x8〉:〈x6,x3〉〉));
786  normalize in ⊢ (? ? ? %);
787  reflexivity.
788 qed.
789 *)
790 *)
Unnamed repository; edit this file 'description' to name the repository.