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