Changeset 318


Ignore:
Timestamp:
Nov 26, 2010, 5:54:01 PM (9 years ago)
Author:
sacerdot
Message:

First version: to be debugged.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Fetch.ma

    r316 r318  
    88   〈res, lookup … pc pmem (zero eight)〉.
    99
     10(* timings taken from SIEMENS *)
     11
    1012ndefinition fetch: BitVectorTrie Byte sixteen → Word → instruction × Word × Nat ≝
    1113 λpmem,pc.
    12   let 〈pc,instr〉 ≝ next pmem pc in
    13   let 〈instr1,instr2〉 ≝ split … three five instr in
    14    if eqv … instr2 [[true;false;false;false;true]] then
     14  let 〈pc,v〉 ≝ next pmem pc in
     15  let 〈v1,v2〉 ≝ split … three five v in
     16   if eqv … v2 [[true;false;false;false;true]] then
    1517    let 〈pc,b1〉 ≝ next pmem pc in
    16      〈〈ACALL … (ADDR11 (instr1 @@ b1)), pc〉, two〉
     18     〈〈ACALL … (ADDR11 (v1 @@ b1)), pc〉, two〉
     19   else if eqv … v2 [[false;false;false;false;true]] then
     20    let 〈pc,b1〉 ≝ next pmem pc in
     21     〈〈AJMP … (ADDR11 (v1 @@ b1)), pc〉, two〉
    1722   else
    18     〈〈NOP …, pc〉, two〉.
     23   let 〈b,v〉≝ head8 v in if b then
     24    let 〈b,v〉≝ head8 v in if b then
     25     let 〈b,v〉≝ head8 v in if b then
     26      let 〈b,v〉≝ head8 v in if b then
     27       let 〈b,v〉≝ head8 v in if b then
     28        〈〈MOV (U2 (REGISTER v, ACC_A)), pc〉, one〉
     29       else
     30        let 〈b,v〉≝ head8 v in if b then
     31         let 〈b,v〉≝ head8 v in if b then
     32          〈〈MOV (U2 (INDIRECT v, ACC_A)), pc〉, one〉
     33         else
     34          let 〈b,v〉≝ head8 v in if b then
     35           let pc,b1 = next pc in 〈〈MOV (U3 (DIRECT b1, ACC_A)), pc〉, one〉
     36          else
     37           〈〈CPL ACC_A, pc〉, one〉
     38        else
     39         let 〈b,v〉≝ head8 v in if b then
     40          〈〈MOVX (U2 (EXT_INDIRECT v, ACC_A)), pc〉, two〉
     41         else
     42          let 〈b,v〉≝ head8 v in if b then
     43           assert false
     44          else
     45           〈〈MOVX (U2 (EXT_IND_DPTR, ACC_A)), pc〉, two〉
     46      else
     47       let 〈b,v〉≝ head8 v in if b then
     48        〈〈MOV (U1 (A, REGISTER v)), pc〉, one〉
     49       else
     50        let 〈b,v〉≝ head8 v in if b then
     51         let 〈b,v〉≝ head8 v in if b then
     52          〈〈MOV (U1 (A, INDIRECT v)), pc〉, one〉
     53         else
     54          let 〈b,v〉≝ head8 v in if b then
     55           let pc,b1 = next pc in 〈〈MOV (U1 (A, DIRECT b1)), pc〉, one〉
     56          else
     57           〈〈CLR ACC_A, pc〉, one〉
     58        else
     59         let 〈b,v〉≝ head8 v in if b then
     60          〈〈MOVX (U1 (A, EXT_INDIRECT v)), pc〉, two〉
     61         else
     62          let 〈b,v〉≝ head8 v in if b then
     63           assert false
     64          else
     65           〈〈MOVX (U1 (A, EXT_IND_DPTR)), pc〉, two〉
     66     else
     67      let 〈b,v〉≝ head8 v in if b then
     68       let 〈b,v〉≝ head8 v in if b then
     69        let pc,b1 = next pc in 〈〈DJNZ (REGISTER v, REL b1), pc〉, two〉
     70       else
     71        let 〈b,v〉≝ head8 v in if b then
     72         let 〈b,v〉≝ head8 v in if b then
     73          〈〈XCHD(A, INDIRECT v), pc〉, one〉
     74         else
     75          let 〈b,v〉≝ head8 v in if b then
     76           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈DJNZ (DIRECT b1, REL b2), pc〉, two〉
     77          else
     78           〈〈DA ACC_A, pc〉, one〉
     79        else
     80         let 〈b,v〉≝ head8 v in if b then
     81          let 〈b,v〉≝ head8 v in if b then
     82           〈〈SETB C, pc〉, one〉
     83          else
     84           let pc,b1 = next pc in 〈〈SETB (BIT b1), pc〉, one〉
     85         else
     86          let 〈b,v〉≝ head8 v in if b then
     87           assert false
     88          else
     89           let pc,b1 = next pc in 〈〈POP (DIRECT b1), pc〉, two〉
     90      else
     91       let 〈b,v〉≝ head8 v in if b then
     92        〈〈XCH (A, REGISTER v), pc〉, one〉
     93       else
     94        let 〈b,v〉≝ head8 v in if b then
     95         let 〈b,v〉≝ head8 v in if b then
     96          〈〈XCH (A, INDIRECT v), pc〉, one〉
     97         else
     98          let 〈b,v〉≝ head8 v in if b then
     99           let pc,b1 = next pc in 〈〈XCH (A, DIRECT b1), pc〉, one〉
     100          else
     101           〈〈SWAP ACC_A, pc〉, one〉
     102        else
     103         let 〈b,v〉≝ head8 v in if b then
     104          let 〈b,v〉≝ head8 v in if b then
     105           〈〈CLR C, pc〉, one〉
     106          else
     107           let pc,b1 = next pc in 〈〈CLR (BIT b1), pc〉, one〉
     108         else
     109          let 〈b,v〉≝ head8 v in if b then
     110           assert false
     111          else
     112           let pc,b1 = next pc in 〈〈PUSH (DIRECT b1), pc〉, two〉
     113    else
     114     let 〈b,v〉≝ head8 v in if b then
     115      let 〈b,v〉≝ head8 v in if b then
     116       let 〈b,v〉≝ head8 v in if b then
     117        let pc,b1 = next pc in let pc,b2 = next pc in 〈〈CJNE (U2 (REGISTER v, DATA b1), REL b2), pc〉, two〉
     118       else
     119        let 〈b,v〉≝ head8 v in if b then
     120         let 〈b,v〉≝ head8 v in if b then
     121          let pc,b1 = next pc in let pc,b2 = next pc in 〈〈CJNE (U2 (INDIRECT v, DATA b1), REL b2), pc〉, two〉
     122         else
     123          let 〈b,v〉≝ head8 v in if b then
     124           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈CJNE (U1 (A, DIRECT b1), REL b2), pc〉, two〉
     125          else
     126           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈CJNE (U1 (A, DATA b1), REL b2), pc〉, two〉
     127        else
     128         let 〈b,v〉≝ head8 v in if b then
     129          let 〈b,v〉≝ head8 v in if b then
     130           〈〈CPL C, pc〉, one〉
     131          else
     132           let pc,b1 = next pc in 〈〈CPL (BIT b1), pc〉, one〉
     133         else
     134          let 〈b,v〉≝ head8 v in if b then
     135           assert false
     136          else
     137           let pc,b1 = next pc in 〈〈ANL (U3 (C,NBIT b1)), pc〉, two〉
     138      else
     139       let 〈b,v〉≝ head8 v in if b then
     140        let pc,b1 = next pc in 〈〈MOV (U2 (REGISTER v, (DIRECT b1))), pc〉, two〉
     141       else
     142        let 〈b,v〉≝ head8 v in if b then
     143         let 〈b,v〉≝ head8 v in if b then
     144          let pc,b1 = next pc in 〈〈MOV (U2 (INDIRECT v, DIRECT b1)), pc〉, two〉
     145         else
     146          〈〈MUL(A, B), pc〉, four〉
     147        else
     148         let 〈b,v〉≝ head8 v in if b then
     149          let 〈b,v〉≝ head8 v in if b then
     150           〈〈INC DPTR, pc〉, two〉
     151          else
     152           let pc,b1 = next pc in 〈〈MOV (U5 (C, BIT b1)), pc〉, one〉
     153         else
     154          let 〈b,v〉≝ head8 v in if b then
     155           assert false
     156          else
     157           let pc,b1 = next pc in 〈〈ORL (U3 (C, NBIT b1)), pc〉, two〉
     158     else
     159      let 〈b,v〉≝ head8 v in if b then
     160       let 〈b,v〉≝ head8 v in if b then
     161        〈〈SUBB (A, REGISTER v), pc〉, one〉
     162       else
     163        let 〈b,v〉≝ head8 v in if b then
     164         let 〈b,v〉≝ head8 v in if b then
     165          〈〈SUBB (A, INDIRECT v), pc〉, one〉
     166         else
     167          let 〈b,v〉≝ head8 v in if b then
     168           let pc,b1 = next pc in 〈〈SUBB (A, DIRECT b1), pc〉, one〉
     169          else
     170           let pc,b1 = next pc in 〈〈SUBB (A, DATA b1), pc〉, one〉
     171        else
     172         let 〈b,v〉≝ head8 v in if b then
     173          let 〈b,v〉≝ head8 v in if b then
     174           〈〈MOVC (A, ACC_A_DPTR), pc〉, two〉
     175          else
     176           let pc,b1 = next pc in 〈〈MOV (U6 (BIT b1, C)), pc〉, two〉
     177         else
     178          let 〈b,v〉≝ head8 v in if b then
     179           assert false
     180          else
     181           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈MOV (U4 (DPTR, DATA16(mk_word b1 b2))), pc〉, two〉
     182      else
     183       let 〈b,v〉≝ head8 v in if b then
     184        let pc,b1 = next pc in 〈〈MOV (U3 (DIRECT b1, REGISTER v)), pc〉, two〉
     185       else
     186        let 〈b,v〉≝ head8 v in if b then
     187         let 〈b,v〉≝ head8 v in if b then
     188          let pc,b1 = next pc in 〈〈MOV (U3 (DIRECT b1, INDIRECT v)), pc〉, two〉
     189         else
     190          let 〈b,v〉≝ head8 v in if b then
     191           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈MOV (U3 (DIRECT b1, DIRECT b2)), pc〉, two〉
     192          else
     193           〈〈DIV (A, B), pc〉, four〉
     194        else
     195         let 〈b,v〉≝ head8 v in if b then
     196          let 〈b,v〉≝ head8 v in if b then
     197           〈〈MOVC (A, ACC_A_PC), pc〉, two〉
     198          else
     199           let pc,b1 = next pc in 〈〈ANL (U3 (C,BIT b1)), pc〉, two〉
     200         else
     201          let 〈b,v〉≝ head8 v in if b then
     202           assert false
     203          else
     204           let pc,b1 = next pc in 〈〈SJMP (REL b1), pc〉, two〉
     205   else
     206    let 〈b,v〉≝ head8 v in if b then
     207     let 〈b,v〉≝ head8 v in if b then
     208      let 〈b,v〉≝ head8 v in if b then
     209       let 〈b,v〉≝ head8 v in if b then
     210        let pc,b1 = next pc in 〈〈MOV (U2 (REGISTER v, (DATA b1))), pc〉, one〉
     211       else
     212        let 〈b,v〉≝ head8 v in if b then
     213         let 〈b,v〉≝ head8 v in if b then
     214          let pc,b1 = next pc in 〈〈MOV (U2 (INDIRECT v, DATA b1)), pc〉, one〉
     215         else
     216          let 〈b,v〉≝ head8 v in if b then
     217           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈MOV (U3 (DIRECT b1, DATA b2)), pc〉, three〉
     218          else
     219           let pc,b1 = next pc in 〈〈MOV (U1 (A, DATA b1)), pc〉, one〉
     220        else
     221         let 〈b,v〉≝ head8 v in if b then
     222          let 〈b,v〉≝ head8 v in if b then
     223           〈〈JMP IND_DPTR, pc〉, two〉
     224          else
     225           let pc,b1 = next pc in 〈〈ORL (U3 (C, BIT b1)), pc〉, two〉
     226         else
     227          let 〈b,v〉≝ head8 v in if b then
     228           assert false
     229          else
     230           let pc,b1 = next pc in 〈〈JNZ (REL b1), pc〉, two〉
     231      else
     232       let 〈b,v〉≝ head8 v in if b then
     233        〈〈XRL(U1(A, REGISTER v)), pc〉, one〉
     234       else
     235        let 〈b,v〉≝ head8 v in if b then
     236         let 〈b,v〉≝ head8 v in if b then
     237          〈〈XRL(U1(A, INDIRECT v)), pc〉, one〉
     238         else
     239          let 〈b,v〉≝ head8 v in if b then
     240           let pc,b1 = next pc in 〈〈XRL(U1(A, DIRECT b1)), pc〉, one〉
     241          else
     242           let pc,b1 = next pc in 〈〈XRL(U1(A, DATA b1)), pc〉, one〉
     243        else
     244         let 〈b,v〉≝ head8 v in if b then
     245          let 〈b,v〉≝ head8 v in if b then
     246           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈XRL(U2(DIRECT b1, DATA b2)), pc〉, two〉
     247          else
     248           let pc,b1 = next pc in 〈〈XRL(U2(DIRECT b1, ACC_A)), pc〉, one〉
     249         else
     250          let 〈b,v〉≝ head8 v in if b then
     251           assert false
     252          else
     253           let pc,b1 = next pc in 〈〈JZ (REL b1), pc〉, two〉
     254     else
     255      let 〈b,v〉≝ head8 v in if b then
     256       let 〈b,v〉≝ head8 v in if b then
     257        〈〈ANL (U1 (A, REGISTER v)), pc〉, one〉
     258       else
     259        let 〈b,v〉≝ head8 v in if b then
     260         let 〈b,v〉≝ head8 v in if b then
     261          〈〈ANL (U1 (A, INDIRECT v)), pc〉, one〉
     262         else
     263          let 〈b,v〉≝ head8 v in if b then
     264           let pc,b1 = next pc in 〈〈ANL (U1 (A, DIRECT b1)), pc〉, one〉
     265          else
     266           let pc,b1 = next pc in 〈〈ANL (U1 (A, DATA b1)), pc〉, one〉
     267        else
     268         let 〈b,v〉≝ head8 v in if b then
     269          let 〈b,v〉≝ head8 v in if b then
     270           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈ANL (U2 (DIRECT b1,DATA b2)), pc〉, two〉
     271          else
     272           let pc,b1 = next pc in 〈〈ANL (U2 (DIRECT b1,A)), pc〉, one〉
     273         else
     274          let 〈b,v〉≝ head8 v in if b then
     275           assert false
     276          else
     277           let pc,b1 = next pc in 〈〈JNC (REL b1), pc〉, two〉
     278      else
     279       let 〈b,v〉≝ head8 v in if b then
     280        〈〈ORL (U1(A, REGISTER v)), pc〉, one〉
     281       else
     282        let 〈b,v〉≝ head8 v in if b then
     283         let 〈b,v〉≝ head8 v in if b then
     284          〈〈ORL (U1(A, INDIRECT v)), pc〉, one〉
     285         else
     286          let 〈b,v〉≝ head8 v in if b then
     287           let pc,b1 = next pc in 〈〈ORL (U1(A, DIRECT b1)), pc〉, one〉
     288          else
     289           let pc,b1 = next pc in 〈〈ORL (U1(A, DATA b1)), pc〉, one〉
     290        else
     291         let 〈b,v〉≝ head8 v in if b then
     292          let 〈b,v〉≝ head8 v in if b then
     293           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈ORL (U2 (DIRECT b1, DATA b2)), pc〉, two〉
     294          else
     295           let pc,b1 = next pc in 〈〈ORL (U2(DIRECT b1, ACC_A)), pc〉, one〉
     296         else
     297          let 〈b,v〉≝ head8 v in if b then
     298           assert false
     299          else
     300           let pc,b1 = next pc in 〈〈JC (REL b1), pc〉, two〉
     301    else
     302     let 〈b,v〉≝ head8 v in if b then
     303      let 〈b,v〉≝ head8 v in if b then
     304       let 〈b,v〉≝ head8 v in if b then
     305        〈〈ADDC (A,REGISTER v), pc〉, one〉
     306       else
     307        let 〈b,v〉≝ head8 v in if b then
     308         let 〈b,v〉≝ head8 v in if b then
     309          〈〈ADDC (A,INDIRECT v), pc〉, one〉
     310         else
     311          let 〈b,v〉≝ head8 v in if b then
     312           let pc,b1 = next pc in 〈〈ADDC (A,DIRECT b1), pc〉, one〉
     313          else
     314           let pc,b1 = next pc in 〈〈ADDC (A,DATA b1), pc〉, one〉
     315        else
     316         let 〈b,v〉≝ head8 v in if b then
     317          let 〈b,v〉≝ head8 v in if b then
     318           〈〈RLC ACC_A, pc〉, one〉
     319          else
     320           〈〈RETI, pc〉, two〉
     321         else
     322          let 〈b,v〉≝ head8 v in if b then
     323           assert false
     324          else
     325           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈JNB (BIT b1, REL b2), pc〉, two〉
     326      else
     327       let 〈b,v〉≝ head8 v in if b then
     328        〈〈ADD (A,REGISTER v), pc〉, one〉
     329       else
     330        let 〈b,v〉≝ head8 v in if b then
     331         let 〈b,v〉≝ head8 v in if b then
     332          〈〈ADD (A,INDIRECT v), pc〉, one〉
     333         else
     334          let 〈b,v〉≝ head8 v in if b then
     335           let pc,b1 = next pc in 〈〈ADD (A,DIRECT b1), pc〉, one〉
     336          else
     337           let pc,b1 = next pc in 〈〈ADD (A,DATA b1), pc〉, one〉
     338        else
     339         let 〈b,v〉≝ head8 v in if b then
     340          let 〈b,v〉≝ head8 v in if b then
     341           〈〈RL ACC_A, pc〉, one〉
     342          let 〈b,v〉≝ head8 v in if b then
     343          else
     344           〈〈RET, pc〉, two〉
     345         else
     346          let 〈b,v〉≝ head8 v in if b then
     347           assert false
     348          else
     349           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈JB (BIT b1, REL b2), pc〉, two〉
     350     else
     351      let 〈b,v〉≝ head8 v in if b then
     352       let 〈b,v〉≝ head8 v in if b then
     353        〈〈DEC (REGISTER v), pc〉, one〉
     354       else
     355        let 〈b,v〉≝ head8 v in if b then
     356         let 〈b,v〉≝ head8 v in if b then
     357          〈〈DEC (INDIRECT v), pc〉, one〉
     358         else
     359          let 〈b,v〉≝ head8 v in if b then
     360           let pc,b1 = next pc in 〈〈DEC (DIRECT b1), pc〉, one〉
     361          else
     362           〈〈DEC ACC_A, pc〉, one〉
     363        else
     364         let 〈b,v〉≝ head8 v in if b then
     365          let 〈b,v〉≝ head8 v in if b then
     366           〈〈RRC ACC_A, pc〉, one〉
     367          else
     368           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈LCALL (ADDR16 (mk_word b1 b2)), pc〉, two〉
     369         else
     370          let 〈b,v〉≝ head8 v in if b then
     371           assert false
     372          else
     373           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈JBC (BIT b1, REL b2), pc〉, two〉
     374      else
     375       let 〈b,v〉≝ head8 v in if b then
     376        〈〈INC (REGISTER v), pc〉, one〉
     377       else
     378        let 〈b,v〉≝ head8 v in if b then
     379         let 〈b,v〉≝ head8 v in if b then
     380          〈〈INC (INDIRECT v), pc〉, one〉
     381         else
     382          let 〈b,v〉≝ head8 v in if b then
     383           let pc,b1 = next pc in 〈〈INC (DIRECT b1), pc〉, one〉
     384          else
     385           〈〈INC ACC_A, pc〉, one〉
     386        else
     387         let 〈b,v〉≝ head8 v in if b then
     388          let 〈b,v〉≝ head8 v in if b then
     389           〈〈RR ACC_A, pc〉, one〉
     390          else
     391           let pc,b1 = next pc in let pc,b2 = next pc in 〈〈LJMP (ADDR16 (mk_word b1 b2)), pc〉, two〉
     392         else
     393          let 〈b,v〉≝ head8 v in if b then
     394           assert false
     395          else
     396           〈〈NOP, pc〉, one〉.
    19397 @.
    20398nqed.
    21    
    22 
    23 (*
    24 (* timings taken from SIEMENS *)
    25 
    26 let fetch pmem pc =
    27  let next pc =
    28    let _carry, res = half_add pc (vect_of_int 1 `Sixteen) in
    29      res, WordMap.find pc pmem
    30  in
    31  let pc,instr = next pc in
    32  let un, ln = from_byte instr in
    33  let bits = (from_nibble un, from_nibble ln) in
    34   match bits with
    35      (a10,a9,a8,true),(false,false,false,true) ->
    36       let pc,b1 = next pc in
    37        `ACALL (`ADDR11 (mk_word11 a10 a9 a8 b1)), pc, 2
    38    | (false,false,true,false),(true,r1,r2,r3) ->
    39        `ADD (`A,`REG (r1,r2,r3)), pc, 1
    40    | (false,false,true,false),(false,true,false,true) ->
    41       let pc,b1 = next pc in
    42        `ADD (`A,`DIRECT b1), pc, 1
    43    | (false,false,true,false),(false,true,true,i1) ->
    44        `ADD (`A,`INDIRECT i1), pc, 1
    45    | (false,false,true,false),(false,true,false,false) ->
    46       let pc,b1 = next pc in
    47        `ADD (`A,`DATA b1), pc, 1
    48    | (false,false,true,true),(true,r1,r2,r3) ->
    49        `ADDC (`A,`REG (r1,r2,r3)), pc, 1
    50    | (false,false,true,true),(false,true,false,true) ->
    51       let pc,b1 = next pc in
    52        `ADDC (`A,`DIRECT b1), pc, 1
    53    | (false,false,true,true),(false,true,true,i1) ->
    54        `ADDC (`A,`INDIRECT i1), pc, 1
    55    | (false,false,true,true),(false,true,false,false) ->
    56       let pc,b1 = next pc in
    57        `ADDC (`A,`DATA b1), pc, 1
    58    | (a10,a9,a8,false),(false,false,false,true) ->
    59       let pc,b1 = next pc in
    60        `AJMP (`ADDR11 (mk_word11 a10 a9 a8 b1)), pc, 2
    61    | (false,true,false,true),(true,r1,r2,r3) ->
    62        `ANL (`U1 (`A, `REG (r1,r2,r3))), pc, 1
    63    | (false,true,false,true),(false,true,false,true) ->
    64       let pc,b1 = next pc in
    65        `ANL (`U1 (`A, `DIRECT b1)), pc, 1
    66    | (false,true,false,true),(false,true,true,i1) ->
    67        `ANL (`U1 (`A, `INDIRECT i1)), pc, 1
    68    | (false,true,false,true),(false,true,false,false) ->
    69       let pc,b1 = next pc in
    70        `ANL (`U1 (`A, `DATA b1)), pc, 1
    71    | (false,true,false,true),(false,false,true,false) ->
    72       let pc,b1 = next pc in
    73        `ANL (`U2 (`DIRECT b1,`A)), pc, 1
    74    | (false,true,false,true),(false,false,true,true) ->
    75       let pc,b1 = next pc in
    76       let pc,b2 = next pc in
    77        `ANL (`U2 (`DIRECT b1,`DATA b2)), pc, 2
    78    | (true,false,false,false),(false,false,true,false) ->
    79       let pc,b1 = next pc in
    80        `ANL (`U3 (`C,`BIT b1)), pc, 2
    81    | (true,false,true,true),(false,false,false,false) ->
    82       let pc,b1 = next pc in
    83        `ANL (`U3 (`C,`NBIT b1)), pc, 2
    84    | (true,false,true,true),(false,true,false,true) ->
    85       let       pc,b1 = next pc in
    86       let pc,b2 = next pc in
    87         `CJNE (`U1 (`A, `DIRECT b1), `REL b2), pc, 2
    88    | (true,false,true,true),(false,true,false,false) ->
    89        let pc,b1 = next pc in
    90        let pc,b2 = next pc in
    91          `CJNE (`U1 (`A, `DATA b1), `REL b2), pc, 2
    92    | (true,false,true,true),(true,r1,r2,r3) ->
    93        let pc,b1 = next pc in
    94        let pc,b2 = next pc in
    95          `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2), pc, 2
    96    | (true,false,true,true),(false,true,true,i1) ->
    97        let pc,b1 = next pc in
    98        let pc,b2 = next pc in
    99          `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2), pc, 2
    100    | (true,true,true,false),(false,true,false,false) ->
    101          `CLR `A, pc, 1
    102    | (true,true,false,false),(false,false,true,true) ->
    103          `CLR `C, pc, 1
    104    | (true,true,false,false),(false,false,true,false) ->
    105        let pc,b1 = next pc in
    106          `CLR (`BIT b1), pc, 1
    107    | (true,true,true,true),(false,true,false,false) ->
    108          `CPL `A, pc, 1
    109    | (true,false,true,true),(false,false,true,true) ->
    110          `CPL `C, pc, 1
    111    | (true,false,true,true),(false,false,true,false) ->
    112        let pc,b1 = next pc in
    113          `CPL (`BIT b1), pc, 1
    114    | (true,true,false,true),(false,true,false,false) ->
    115          `DA `A, pc, 1
    116    | (false,false,false,true),(false,true,false,false) ->
    117          `DEC `A, pc, 1
    118    | (false,false,false,true),(true,r1,r2,r3) ->
    119          `DEC (`REG(r1,r2,r3)), pc, 1
    120    | (false,false,false,true),(false,true,false,true) ->
    121        let pc,b1 = next pc in
    122          `DEC (`DIRECT b1), pc, 1
    123    | (false,false,false,true),(false,true,true,i1) ->
    124          `DEC (`INDIRECT i1), pc, 1
    125    | (true,false,false,false),(false,true,false,false) ->
    126          `DIV (`A, `B), pc, 4
    127    | (true,true,false,true),(true,r1,r2,r3) ->
    128        let pc,b1 = next pc in
    129          `DJNZ (`REG(r1,r2,r3), `REL b1), pc, 2
    130    | (true,true,false,true),(false,true,false,true) ->
    131        let pc,b1 = next pc in
    132        let pc,b2 = next pc in
    133          `DJNZ (`DIRECT b1, `REL b2), pc, 2
    134    | (false,false,false,false),(false,true,false,false) ->
    135          `INC `A, pc, 1
    136    | (false,false,false,false),(true,r1,r2,r3) ->
    137          `INC (`REG(r1,r2,r3)), pc, 1
    138    | (false,false,false,false),(false,true,false,true) ->
    139        let pc,b1 = next pc in
    140          `INC (`DIRECT b1), pc, 1
    141    | (false,false,false,false),(false,true,true,i1) ->
    142          `INC (`INDIRECT i1), pc, 1
    143    | (true,false,true,false),(false,false,true,true) ->
    144          `INC `DPTR, pc, 2
    145    | (false,false,true,false),(false,false,false,false) ->
    146        let pc,b1 = next pc in
    147        let pc,b2 = next pc in
    148          `JB (`BIT b1, `REL b2), pc, 2
    149    | (false,false,false,true),(false,false,false,false) ->
    150        let pc,b1 = next pc in
    151        let pc,b2 = next pc in
    152          `JBC (`BIT b1, `REL b2), pc, 2
    153    | (false,true,false,false),(false,false,false,false) ->
    154        let pc,b1 = next pc in
    155          `JC (`REL b1), pc, 2
    156    | (false,true,true,true),(false,false,true,true) ->
    157          `JMP `IND_DPTR, pc, 2
    158    | (false,false,true,true),(false,false,false,false) ->
    159        let pc,b1 = next pc in
    160        let pc,b2 = next pc in
    161          `JNB (`BIT b1, `REL b2), pc, 2
    162    | (false,true,false,true),(false,false,false,false) ->
    163        let pc,b1 = next pc in
    164          `JNC (`REL b1), pc, 2
    165    | (false,true,true,true),(false,false,false,false) ->
    166        let pc,b1 = next pc in
    167          `JNZ (`REL b1), pc, 2
    168    | (false,true,true,false),(false,false,false,false) ->
    169        let pc,b1 = next pc in
    170          `JZ (`REL b1), pc, 2
    171    | (false,false,false,true),(false,false,true,false) ->
    172        let pc,b1 = next pc in
    173        let pc,b2 = next pc in
    174          `LCALL (`ADDR16 (mk_word b1 b2)), pc, 2
    175    | (false,false,false,false),(false,false,true,false) ->
    176        let pc,b1 = next pc in
    177        let pc,b2 = next pc in
    178          `LJMP (`ADDR16 (mk_word b1 b2)), pc, 2
    179    | (true,true,true,false),(true,r1,r2,r3) ->
    180          `MOV (`U1 (`A, `REG(r1,r2,r3))), pc, 1
    181    | (true,true,true,false),(false,true,false,true) ->
    182        let pc,b1 = next pc in
    183          `MOV (`U1 (`A, `DIRECT b1)), pc, 1
    184    | (true,true,true,false),(false,true,true,i1) ->
    185          `MOV (`U1 (`A, `INDIRECT i1)), pc, 1
    186    | (false,true,true,true),(false,true,false,false) ->
    187        let pc,b1 = next pc in
    188          `MOV (`U1 (`A, `DATA b1)), pc, 1
    189    | (true,true,true,true),(true,r1,r2,r3) ->
    190          `MOV (`U2 (`REG(r1,r2,r3), `A)), pc, 1
    191    | (true,false,true,false),(true,r1,r2,r3) ->
    192        let pc,b1 = next pc in
    193          `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))), pc, 2
    194    | (false,true,true,true),(true,r1,r2,r3) ->
    195        let pc,b1 = next pc in
    196          `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))), pc, 1
    197    | (true,true,true,true),(false,true,false,true) ->
    198        let pc,b1 = next pc in
    199          `MOV (`U3 (`DIRECT b1, `A)), pc, 1
    200    | (true,false,false,false),(true,r1,r2,r3) ->
    201        let pc,b1 = next pc in
    202          `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))), pc, 2
    203    | (true,false,false,false),(false,true,false,true) ->
    204        let pc,b1 = next pc in
    205        let pc,b2 = next pc in
    206          `MOV (`U3 (`DIRECT b1, `DIRECT b2)), pc, 2
    207    | (true,false,false,false),(false,true,true,i1) ->
    208        let pc,b1 = next pc in
    209          `MOV (`U3 (`DIRECT b1, `INDIRECT i1)), pc, 2
    210    | (false,true,true,true),(false,true,false,true) ->
    211        let pc,b1 = next pc in
    212        let pc,b2 = next pc in
    213          `MOV (`U3 (`DIRECT b1, `DATA b2)), pc, 3
    214    | (true,true,true,true),(false,true,true,i1) ->
    215          `MOV (`U2 (`INDIRECT i1, `A)), pc, 1
    216    | (true,false,true,false),(false,true,true,i1) ->
    217        let pc,b1 = next pc in
    218          `MOV (`U2 (`INDIRECT i1, `DIRECT b1)), pc, 2
    219    | (false,true,true,true),(false,true,true,i1) ->
    220        let pc,b1 = next pc in
    221          `MOV (`U2 (`INDIRECT i1, `DATA b1)), pc, 1
    222    | (true,false,true,false),(false,false,true,false) ->
    223        let pc,b1 = next pc in
    224          `MOV (`U5 (`C, `BIT b1)), pc, 1
    225    | (true,false,false,true),(false,false,true,false) ->
    226        let pc,b1 = next pc in
    227          `MOV (`U6 (`BIT b1, `C)), pc, 2
    228    | (true,false,false,true),(false,false,false,false) ->
    229        let pc,b1 = next pc in
    230        let pc,b2 = next pc in
    231          `MOV (`U4 (`DPTR, `DATA16(mk_word b1 b2))), pc, 2
    232    | (true,false,false,true),(false,false,true,true) ->
    233          `MOVC (`A, `A_DPTR), pc, 2
    234    | (true,false,false,false),(false,false,true,true) ->
    235          `MOVC (`A, `A_PC), pc, 2
    236    | (true,true,true,false),(false,false,true,i1) ->
    237          `MOVX (`U1 (`A, `EXT_INDIRECT i1)), pc, 2
    238    | (true,true,true,false),(false,false,false,false) ->
    239          `MOVX (`U1 (`A, `EXT_IND_DPTR)), pc, 2
    240    | (true,true,true,true),(false,false,true,i1) ->
    241          `MOVX (`U2 (`EXT_INDIRECT i1, `A)), pc, 2
    242    | (true,true,true,true),(false,false,false,false) ->
    243          `MOVX (`U2 (`EXT_IND_DPTR, `A)), pc, 2
    244    | (true,false,true,false),(false,true,false,false) ->
    245          `MUL(`A, `B), pc, 4
    246    | (false,false,false,false),(false,false,false,false) ->
    247          `NOP, pc, 1
    248    | (false,true,false,false),(true,r1,r2,r3) ->
    249          `ORL (`U1(`A, `REG(r1,r2,r3))), pc, 1
    250    | (false,true,false,false),(false,true,false,true) ->
    251        let pc,b1 = next pc in
    252          `ORL (`U1(`A, `DIRECT b1)), pc, 1
    253    | (false,true,false,false),(false,true,true,i1) ->
    254          `ORL (`U1(`A, `INDIRECT i1)), pc, 1
    255    | (false,true,false,false),(false,true,false,false) ->
    256        let pc,b1 = next pc in
    257          `ORL (`U1(`A, `DATA b1)), pc, 1
    258    | (false,true,false,false),(false,false,true,false) ->
    259        let pc,b1 = next pc in
    260          `ORL (`U2(`DIRECT b1, `A)), pc, 1
    261    | (false,true,false,false),(false,false,true,true) ->
    262        let pc,b1 = next pc in
    263        let pc,b2 = next pc in
    264          `ORL (`U2 (`DIRECT b1, `DATA b2)), pc, 2
    265    | (false,true,true,true),(false,false,true,false) ->
    266        let pc,b1 = next pc in
    267          `ORL (`U3 (`C, `BIT b1)), pc, 2
    268    | (true,false,true,false),(false,false,false,false) ->
    269        let pc,b1 = next pc in
    270          `ORL (`U3 (`C, `NBIT b1)), pc, 2
    271    | (true,true,false,true),(false,false,false,false) ->
    272        let pc,b1 = next pc in
    273          `POP (`DIRECT b1), pc, 2
    274    | (true,true,false,false),(false,false,false,false) ->
    275        let pc,b1 = next pc in
    276          `PUSH (`DIRECT b1), pc, 2
    277    | (false,false,true,false),(false,false,true,false) ->
    278          `RET, pc, 2
    279    | (false,false,true,true),(false,false,true,false) ->
    280          `RETI, pc, 2
    281    | (false,false,true,false),(false,false,true,true) ->
    282          `RL `A, pc, 1
    283    | (false,false,true,true),(false,false,true,true) ->
    284          `RLC `A, pc, 1
    285    | (false,false,false,false),(false,false,true,true) ->
    286          `RR `A, pc, 1
    287    | (false,false,false,true),(false,false,true,true) ->
    288          `RRC `A, pc, 1
    289    | (true,true,false,true),(false,false,true,true) ->
    290          `SETB `C, pc, 1
    291    | (true,true,false,true),(false,false,true,false) ->
    292        let pc,b1 = next pc in
    293          `SETB (`BIT b1), pc, 1
    294    | (true,false,false,false),(false,false,false,false) ->
    295        let pc,b1 = next pc in
    296          `SJMP (`REL b1), pc, 2
    297    | (true,false,false,true),(true,r1,r2,r3) ->
    298        `SUBB (`A, `REG(r1,r2,r3)), pc, 1
    299    | (true,false,false,true),(false,true,false,true) ->
    300        let pc,b1 = next pc in
    301          `SUBB (`A, `DIRECT b1), pc, 1
    302    | (true,false,false,true),(false,true,true,i1) ->
    303          `SUBB (`A, `INDIRECT i1), pc, 1
    304    | (true,false,false,true),(false,true,false,false) ->
    305        let pc,b1 = next pc in
    306          `SUBB (`A, `DATA b1), pc, 1
    307    | (true,true,false,false),(false,true,false,false) ->
    308          `SWAP `A, pc, 1
    309    | (true,true,false,false),(true,r1,r2,r3) ->
    310          `XCH (`A, `REG(r1,r2,r3)), pc, 1
    311    | (true,true,false,false),(false,true,false,true) ->
    312        let pc,b1 = next pc in
    313          `XCH (`A, `DIRECT b1), pc, 1
    314    | (true,true,false,false),(false,true,true,i1) ->
    315          `XCH (`A, `INDIRECT i1), pc, 1
    316    | (true,true,false,true),(false,true,true,i1) ->
    317          `XCHD(`A, `INDIRECT i1), pc, 1
    318    | (false,true,true,false),(true,r1,r2,r3) ->
    319          `XRL(`U1(`A, `REG(r1,r2,r3))), pc, 1
    320    | (false,true,true,false),(false,true,false,true) ->
    321        let pc,b1 = next pc in
    322          `XRL(`U1(`A, `DIRECT b1)), pc, 1
    323    | (false,true,true,false),(false,true,true,i1) ->
    324          `XRL(`U1(`A, `INDIRECT i1)), pc, 1
    325    | (false,true,true,false),(false,true,false,false) ->
    326        let pc,b1 = next pc in
    327          `XRL(`U1(`A, `DATA b1)), pc, 1
    328    | (false,true,true,false),(false,false,true,false) ->
    329        let pc,b1 = next pc in
    330          `XRL(`U2(`DIRECT b1, `A)), pc, 1
    331    | (false,true,true,false),(false,false,true,true) ->
    332        let pc,b1 = next pc in
    333        let pc,b2 = next pc in
    334          `XRL(`U2(`DIRECT b1, `DATA b2)), pc, 2
    335    | _,_ -> assert false
    336 ;;
    337 
    338 
    339 *)
    340 
    341 
    342 
    343 (*
    344 nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
    345    elem:> A;
    346    witness: T elem
    347 }.
    348 
    349 interpretation "Sigma" 'sigma T = (Sigma ? T).
    350 
    351 naxiom daemon: False.
    352 
    353 naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
    354 naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].
    355 
    356 ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
    357  ≝
    358  [mk_Cartesian ??
    359    (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
    360      (λl.
    361        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    362              (mk_subaddressing_mode ? ?    (decode_register l) ?));
    363   mk_Cartesian ??
    364    (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
    365      (λl.
    366        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    367              (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
    368 ncases daemon.
    369 nqed.
    370 
    371 
    372 naxiom decode_register: List Bool → [reg].
    373 naxiom decode_direct: List Bool → [direct].
    374 
    375 ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
    376  ≝
    377  [mk_Cartesian ??
    378    [ false; false; true; false; true]
    379      (λl.
    380        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    381              (mk_subaddressing_mode ? ?    (decode_register l) ?));
    382   mk_Cartesian ??
    383    [ false; false; true; false; true]
    384      (λl.
    385        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    386              (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
    387 ncases daemon.
    388 nqed.
    389 
    390 
    391 ndefinition decode_tbl1:
    392  List (List Bool × Σaddr:all_types. [addr] → Instruction)
    393  ≝
    394  [mk_Cartesian ??
    395    [ false; false; true; false; true]
    396    (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
    397      reg
    398      (λa.
    399        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    400              (mk_subaddressing_mode ? ? a ?))) ].
    401 ncases daemon.
    402 nqed.
    403              
    404 ndefinition decode_tbl2:
    405  List (List Bool × Σaddr:all_types. [addr] → Instruction)
    406  ≝
    407  [mk_Cartesian ??
    408    [ false; false; true; false; false; true; false; true]
    409    (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
    410      direct
    411      (λa.
    412        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    413              (mk_subaddressing_mode ? ?     a ?))) ].
    414 ncases daemon.
    415 nqed.
    416 
    417 ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
    418 
    419 decode_addr_mode; ∀addr:all_types. List Bool → [addr].
    420 
    421 decode ≝
    422  λl:List Bit.
    423   List.iter
    424    (fun l0 addr mk_f →
    425      match split_prefix l l0 with
    426       [ None ⇒ ...
    427       | Some r ⇒ mk_f (decode_addr_mode r) ]
    428      
    429    ) decode_tbl
    430 
    431 encode ≝
    432 
    433 ndefinition decode_tbl:
    434  List (List Bool × Σaddr:all_types. [addr] → Instruction)
    435  ≝
    436  [mk_Cartesian ??
    437    [ False; False; True; False; True]
    438    (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
    439      reg
    440      (λa:subaddressing_mode ? [reg].
    441        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    442              (mk_subaddressing_mode ? ?     a ?)));
    443   mk_Cartesian ??
    444    [ False; False; True; False; False; True; False; True]
    445    (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
    446      direct
    447      (λa:subaddressing_mode ? [direct].
    448        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    449              (mk_subaddressing_mode ? ?     a ?)))
    450  ].
    451 nnormalize;
    452  
    453  ].
    454 *)
    455 
Note: See TracChangeset for help on using the changeset viewer.