source: src/ASM/Fetch.ma @ 2085

Last change on this file since 2085 was 1961, checked in by sacerdot, 8 years ago

No more interaction required.

File size: 23.6 KB
RevLine 
[698]1include "ASM/BitVectorTrie.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/ASM.ma".
[1600]4include "basics/russell.ma".
[475]5
[1591]6definition bitvector_max_nat ≝
7  λlength: nat.
8    2^length.
[475]9
[1591]10definition code_memory_size ≝ bitvector_max_nat 16.
11
[1941]12include alias "ASM/BitVectorTrie.ma".
[1961]13include alias "ASM/Arithmetic.ma".
[1941]14
[1604]15definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
[1591]16  λpmem: BitVectorTrie Byte 16.
17  λpc: Word.
[1941]18    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
[1591]19
[1598]20lemma Prod_inv_rect_Type0:
21 ∀A,B. ∀P: A × B → Type[0].∀ab.
22  (∀a,b. ab = 〈a,b〉 → P 〈a,b〉) → P ab.
23 #A #B #P * /2/
24qed.
25
26notation > "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
27 with precedence 10
28for @{ Prod_inv_rect_Type0 ??? $t (λ${ident x}.λ${ident y}.λ${ident H}.$s) }.
29
30notation < "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
31 with precedence 10
32for @{ Prod_inv_rect_Type0 $z $w $r $t (λ${ident x}:$X.λ${ident y}:$Y.λ${ident H}:$h.$s) }.
33
34lemma breakup_pair' : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:∀a:A.∀b:B. x=〈a,b〉 → C.
35  R (P (\fst x) (\snd x) ?) → R (let 〈a,b〉 {H} ≝ x in P a b H).
36[2: // ]
37#A #B #C *; normalize /2/
38qed.
39
[475]40(* timings taken from SIEMENS *)
41
[1604]42definition fetch0: ∀code_memory: BitVectorTrie Byte 16.
43    ∀program_counter: Word. Byte → instruction × Word × nat ≝
[1591]44  λpmem.
45  λpc.
46  λv.
[475]47   let 〈b,v〉 ≝ head … v in if b then
48    let 〈b,v〉 ≝ head … v in if b then
49     let 〈b,v〉 ≝ head … v in if b then
50      let 〈b,v〉 ≝ head … v in if b then
51       let 〈b,v〉 ≝ head … v in if b then
[820]52        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉
[475]53       else
54        let 〈b,v〉≝  head … v in if b then
55         let 〈b,v〉≝  head … v in if b then
[820]56          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉
[475]57         else
58          let 〈b,v〉≝  head … v in if b then
[1604]59           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
[475]60          else
[856]61           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
[475]62        else
63         let 〈b,v〉≝  head … v in if b then
[820]64          〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉
[475]65         else
66          let 〈b,v〉≝  head … v in if b then
[1604]67           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
[475]68          else
[820]69           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
[475]70      else
71       let 〈b,v〉≝  head … v in if b then
[820]72        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉
[475]73       else
74        let 〈b,v〉≝  head … v in if b then
75         let 〈b,v〉≝  head … v in if b then
[820]76          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉
[475]77         else
78          let 〈b,v〉≝  head … v in if b then
[1604]79           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
[475]80          else
[820]81           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
[475]82        else
83         let 〈b,v〉≝  head … v in if b then
[820]84          〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉
[475]85         else
86          let 〈b,v〉≝  head … v in if b then
[1604]87           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
[475]88          else
[820]89           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
[475]90     else
91      let 〈b,v〉≝  head … v in if b then
92       let 〈b,v〉≝  head … v in if b then
[1604]93        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
[475]94       else
95        let 〈b,v〉≝  head … v in if b then
96         let 〈b,v〉≝  head … v in if b then
[820]97          〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]98         else
99          let 〈b,v〉≝  head … v in if b then
[1604]100           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
[475]101          else
[820]102           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
[475]103        else
104         let 〈b,v〉≝  head … v in if b then
105          let 〈b,v〉≝  head … v in if b then
[820]106           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
[475]107          else
[1604]108           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
[475]109         else
110          let 〈b,v〉≝  head … v in if b then
[1604]111           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
[475]112          else
[1604]113           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
[475]114      else
115       let 〈b,v〉≝  head … v in if b then
[820]116        〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉
[475]117       else
118        let 〈b,v〉≝  head … v in if b then
119         let 〈b,v〉≝  head … v in if b then
[820]120          〈〈RealInstruction (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]121         else
122          let 〈b,v〉≝  head … v in if b then
[1604]123           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
[475]124          else
[820]125           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
[475]126        else
127         let 〈b,v〉≝  head … v in if b then
128          let 〈b,v〉≝  head … v in if b then
[820]129           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
[475]130          else
[1604]131           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
[475]132         else
133          let 〈b,v〉≝  head … v in if b then
[1604]134           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
[475]135          else
[1604]136           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
[475]137    else
138     let 〈b,v〉≝  head … v in if b then
139      let 〈b,v〉≝  head … v in if b then
140       let 〈b,v〉≝  head … v in if b then
[1604]141        let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
[475]142       else
143        let 〈b,v〉≝  head … v in if b then
144         let 〈b,v〉≝  head … v in if b then
[1604]145          let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
[475]146         else
147          let 〈b,v〉≝  head … v in if b then
[1604]148           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
[475]149          else
[1604]150           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
[475]151        else
152         let 〈b,v〉≝  head … v in if b then
153          let 〈b,v〉≝  head … v in if b then
[820]154           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
[475]155          else
[1604]156           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
[475]157         else
158          let 〈b,v〉≝  head … v in if b then
[1604]159           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
[475]160          else
[1604]161           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
[475]162      else
163       let 〈b,v〉≝  head … v in if b then
[1604]164        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
[475]165       else
166        let 〈b,v〉≝  head … v in if b then
167         let 〈b,v〉≝  head … v in if b then
[1604]168          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
[475]169         else
[820]170          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
[475]171        else
172         let 〈b,v〉≝  head … v in if b then
173          let 〈b,v〉≝  head … v in if b then
[820]174           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
[475]175          else
[1604]176           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
[475]177         else
178          let 〈b,v〉≝  head … v in if b then
[1604]179           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
[475]180          else
[1604]181           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
[475]182     else
183      let 〈b,v〉≝  head … v in if b then
184       let 〈b,v〉≝  head … v in if b then
[820]185        〈〈RealInstruction (SUBB … ACC_A (REGISTER v)), pc〉, 1〉
[475]186       else
187        let 〈b,v〉≝  head … v in if b then
188         let 〈b,v〉≝  head … v in if b then
[820]189          〈〈RealInstruction (SUBB … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]190         else
191          let 〈b,v〉≝  head … v in if b then
[1604]192           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
[475]193          else
[1604]194           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
[475]195        else
196         let 〈b,v〉≝  head … v in if b then
197          let 〈b,v〉≝  head … v in if b then
198           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
199          else
[1604]200           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
[475]201         else
202          let 〈b,v〉≝  head … v in if b then
[1604]203           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
[475]204          else
[1604]205           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
[475]206      else
207       let 〈b,v〉≝  head … v in if b then
[1604]208        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
[475]209       else
210        let 〈b,v〉≝  head … v in if b then
211         let 〈b,v〉≝  head … v in if b then
[1604]212          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
[475]213         else
214          let 〈b,v〉≝  head … v in if b then
[1604]215           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
[475]216          else
[820]217           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
[475]218        else
219         let 〈b,v〉≝  head … v in if b then
220          let 〈b,v〉≝  head … v in if b then
221           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
222          else
[1604]223           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
[475]224         else
225          let 〈b,v〉≝  head … v in if b then
[1604]226           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
[475]227          else
[1604]228           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
[475]229   else
230    let 〈b,v〉≝  head … v in if b then
231     let 〈b,v〉≝  head … v in if b then
232      let 〈b,v〉≝  head … v in if b then
233       let 〈b,v〉≝  head … v in if b then
[1604]234        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
[475]235       else
236        let 〈b,v〉≝  head … v in if b then
237         let 〈b,v〉≝  head … v in if b then
[1604]238          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
[475]239         else
240          let 〈b,v〉≝  head … v in if b then
[1604]241           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
[475]242          else
[1604]243           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
[475]244        else
245         let 〈b,v〉≝  head … v in if b then
246          let 〈b,v〉≝  head … v in if b then
247           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
248          else
[1604]249           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
[475]250         else
251          let 〈b,v〉≝  head … v in if b then
[1604]252           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
[475]253          else
[1604]254           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
[475]255      else
256       let 〈b,v〉≝  head … v in if b then
[820]257        〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
[475]258       else
259        let 〈b,v〉≝  head … v in if b then
260         let 〈b,v〉≝  head … v in if b then
[820]261          〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
[475]262         else
263          let 〈b,v〉≝  head … v in if b then
[1604]264           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
[475]265          else
[1604]266           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
[475]267        else
268         let 〈b,v〉≝  head … v in if b then
269          let 〈b,v〉≝  head … v in if b then
[1604]270           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
[475]271          else
[1604]272           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
[475]273         else
274          let 〈b,v〉≝  head … v in if b then
[1604]275           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
[475]276          else
[1604]277           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
[475]278     else
279      let 〈b,v〉≝  head … v in if b then
280       let 〈b,v〉≝  head … v in if b then
[820]281        〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
[475]282       else
283        let 〈b,v〉≝  head … v in if b then
284         let 〈b,v〉≝  head … v in if b then
[820]285          〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
[475]286         else
287          let 〈b,v〉≝  head … v in if b then
[1604]288           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
[475]289          else
[1604]290           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
[475]291        else
292         let 〈b,v〉≝  head … v in if b then
293          let 〈b,v〉≝  head … v in if b then
[1604]294           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
[475]295          else
[1604]296           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
[475]297         else
298          let 〈b,v〉≝  head … v in if b then
[1604]299           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
[475]300          else
[1604]301           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
[475]302      else
303       let 〈b,v〉≝  head … v in if b then
[820]304        〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
[475]305       else
306        let 〈b,v〉≝  head … v in if b then
307         let 〈b,v〉≝  head … v in if b then
[820]308          〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
[475]309         else
310          let 〈b,v〉≝  head … v in if b then
[1604]311           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
[475]312          else
[1604]313           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
[475]314        else
315         let 〈b,v〉≝  head … v in if b then
316          let 〈b,v〉≝  head … v in if b then
[1604]317           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
[475]318          else
[1604]319           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
[475]320         else
321          let 〈b,v〉≝  head … v in if b then
[1604]322           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
[475]323          else
[1604]324           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
[475]325    else
326     let 〈b,v〉≝  head … v in if b then
327      let 〈b,v〉≝  head … v in if b then
328       let 〈b,v〉≝  head … v in if b then
[820]329        〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉
[475]330       else
331        let 〈b,v〉≝  head … v in if b then
332         let 〈b,v〉≝  head … v in if b then
[820]333          〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]334         else
335          let 〈b,v〉≝  head … v in if b then
[1604]336           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
[475]337          else
[1604]338           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
[475]339        else
340         let 〈b,v〉≝  head … v in if b then
341          let 〈b,v〉≝  head … v in if b then
[820]342           〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉
[475]343          else
[820]344           〈〈RealInstruction (RETI …), pc〉, 2〉
[475]345         else
346          let 〈b,v〉≝  head … v in if b then
[1604]347           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
[475]348          else
[1604]349           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
[475]350      else
351       let 〈b,v〉≝  head … v in if b then
[820]352        〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉
[475]353       else
354        let 〈b,v〉≝  head … v in if b then
355         let 〈b,v〉≝  head … v in if b then
[820]356          〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]357         else
358          let 〈b,v〉≝  head … v in if b then
[1604]359           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
[475]360          else
[1604]361           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
[475]362        else
363         let 〈b,v〉≝  head … v in if b then
364          let 〈b,v〉≝  head … v in if b then
[820]365           〈〈RealInstruction (RL … ACC_A), pc〉, 1〉
[475]366          else
[820]367           〈〈RealInstruction (RET …), pc〉, 2〉
[475]368         else
369          let 〈b,v〉≝  head … v in if b then
[1604]370           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
[475]371          else
[1604]372           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
[475]373     else
374      let 〈b,v〉≝  head … v in if b then
375       let 〈b,v〉≝  head … v in if b then
[820]376        〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉
[475]377       else
378        let 〈b,v〉≝  head … v in if b then
379         let 〈b,v〉≝  head … v in if b then
[820]380          〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉
[475]381         else
382          let 〈b,v〉≝  head … v in if b then
[1604]383           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
[475]384          else
[820]385           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
[475]386        else
387         let 〈b,v〉≝  head … v in if b then
388          let 〈b,v〉≝  head … v in if b then
[820]389           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
[475]390          else
[1604]391           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
[475]392         else
393          let 〈b,v〉≝  head … v in if b then
[1604]394           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
[475]395          else
[1604]396           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
[475]397      else
398       let 〈b,v〉≝  head … v in if b then
[820]399        〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉
[475]400       else
401        let 〈b,v〉≝  head … v in if b then
402         let 〈b,v〉≝  head … v in if b then
[820]403          〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉
[475]404         else
405          let 〈b,v〉≝  head … v in if b then
[1604]406           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
[475]407          else
[820]408           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
[475]409        else
410         let 〈b,v〉≝  head … v in if b then
411          let 〈b,v〉≝  head … v in if b then
[820]412           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
[475]413          else
[1604]414           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
[475]415         else
416          let 〈b,v〉≝  head … v in if b then
[1604]417           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
[475]418          else
[820]419           〈〈RealInstruction (NOP …), pc〉, 1〉.
[1604]420  %
[475]421qed.
[876]422
[1604]423definition fetch: ∀code_memory: BitVectorTrie Byte 16.
424    ∀program_counter: Word. instruction × Word × nat ≝
[1591]425  λpmem: BitVectorTrie Byte 16.
426  λpc: Word.
[1604]427  let 〈word, byte〉 ≝ next pmem pc in
[1946]428    fetch0 pmem word byte.
Note: See TracBrowser for help on using the repository browser.