source: Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml @ 622

Last change on this file since 622 was 622, checked in by mulligan, 10 years ago

Started fixing assert false problem.

File size: 78.0 KB
Line 
1open BitVectors;;
2open Physical;;
3open ASM;;
4open IntelHex;;
5open Util;;
6open Parser;;
7
8exception Fetch_exception of string;;
9exception CodeTooLarge;;
10exception Halt;;
11
12type time = int;;
13type line = [ `P1 of byte
14            | `P3 of byte
15            | `SerialBuff of [ `Eight of byte | `Nine of BitVectors.bit * byte ]];;
16
17let string_of_line =
18  function
19  `P1 b ->
20    "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
21      "P1 OUTPUT: " ^ hex_string_of_vect b ^ "\n" ^
22      "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n"
23    | `P3 b ->
24      "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
25        "P2 OUTPUT: " ^ hex_string_of_vect b ^ "\n" ^
26        "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n"
27    | `SerialBuff (`Eight b) ->
28      "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
29        "SERIAL 8b OUTPUT: " ^ string_of_vect b ^ "\n" ^
30        "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n"
31    | `SerialBuff (`Nine (b, b')) ->
32      "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
33        "SERIAL 9b OUTPUT: " ^
34        (let i = int_of_vect b' in
35         if b then
36           string_of_int (128 + i)
37         else
38           string_of_int i) ^
39        "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n"
40
41(* In:  reception time, line of input, new continuation,
42   Out: transmission time, output line, expected duration until reply,
43        new continuation.
44*)
45
46type epsilon = int
47
48type continuation =
49  [`In of time * line * epsilon * continuation] option *
50    [`Out of (time -> line -> time * continuation)]
51
52let rec debug_continuation =
53  (Some (`In (1, (`SerialBuff (`Eight (vect_of_int 5 `Eight))), 0, debug_continuation))), `Out (
54    fun time line ->
55      (* let _ = prerr_endline <*> string_of_line $ line in *)
56      (time + 1),debug_continuation)
57   
58(* no differentiation between internal and external code memory *)
59type status =
60{
61  (* Memory *)
62  code_memory: Physical.WordMap.map;        (* can be reduced *)
63  low_internal_ram: Byte7Map.map;
64  high_internal_ram: Byte7Map.map;
65  external_ram: Physical.WordMap.map;
66
67  (* Program counter *)
68  pc: word;
69
70  (* SFRs *)
71  sp: byte;
72  dpl: byte;
73  dph: byte;
74  pcon: byte;
75  tcon: byte;
76  tmod: byte;
77  tl0: byte;
78  tl1: byte;
79  th0: byte;
80  th1: byte;
81  p1: byte;
82  scon: byte;
83  sbuf: byte;
84  ie: byte;
85  p3: byte;
86  ip: byte;
87  psw: byte;
88  acc: byte;
89  b: byte;
90  t2con: byte;   (* 8052 only *)
91  rcap2l: byte;  (* 8052 only *)
92  rcap2h: byte;  (* 8052 only *)
93  tl2: byte;     (* 8052 only *)
94  th2: byte;     (* 8052 only *)
95
96  (* Latches for the output lines *)
97  p1_latch: byte;
98  p3_latch: byte;
99
100  (* Fields for tracking the state of the processor. *)
101 
102  (* IO specific *)
103  previous_p1_val: bool;
104  previous_p3_val: bool;
105
106  serial_epsilon_out: epsilon option;
107  serial_epsilon_in: epsilon option;
108
109  io_epsilon: epsilon;
110
111  serial_v_in: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option;
112  serial_v_out: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option;
113
114  serial_k_out: continuation option;
115
116  io: continuation;
117  expected_out_time: [ `None | `Now | `At of time ];
118
119  (* Timer and clock specific *)
120  clock: time;
121  timer0: word;
122  timer1: word;
123  timer2: word;  (* can be missing *)
124
125  esi_running: bool;
126  t0i_running: bool;
127  t1i_running: bool;
128  e0i_running: bool;
129  e1i_running: bool;
130  es_running: bool;
131
132  exit_addr   : BitVectors.word;
133  cost_labels : string BitVectors.WordMap.t
134}
135
136(* Try to understand what DEC really does!!! *)
137(* Try to understand I/O *)
138let get_sfr status addr from_latch =
139  match int_of_vect addr with
140    (* I/O and timer ports *)
141      0x80 -> assert false (* P0 not modeled *)
142    | 0x90 ->
143      if from_latch then
144        status.p1_latch
145      else status.p1
146    | 0xA0 -> assert false (* P2 not modeled *)
147    | 0xB0 ->
148      if from_latch then
149        status.p3_latch
150      else status.p3
151    | 0x99 -> status.sbuf
152    | 0x8A -> status.tl0
153    | 0x8B -> status.tl1
154    | 0x8C -> status.th0
155    | 0x8D -> status.th1
156    | 0xC8 -> status.t2con
157    | 0xCA -> status.rcap2l
158    | 0xCB -> status.rcap2h
159    | 0xCC -> status.tl2
160    | 0xCD -> status.th2
161
162  (* control ports *)
163    | 0x87 -> status.pcon
164    | 0x88 -> status.tcon
165    | 0x89 -> status.tmod
166    | 0x98 -> status.scon
167    | 0xA8 -> status.ie
168    | 0xB8 -> status.ip
169     
170  (* registers *)
171    | 0x81 -> status.sp
172    | 0x82 -> status.dpl
173    | 0x83 -> status.dph
174    | 0xD0 -> status.psw
175    | 0xE0 -> status.acc
176    | 0xF0 -> status.b
177    | _ -> assert false
178;;
179
180(* Try to understand I/O *)
181let set_sfr status addr v =
182  match int_of_vect addr with
183    (* I/O and timer ports *)
184      0x80 -> assert false (* P0 not modeled *)
185    | 0x90 -> { status with p1 = v; p1_latch = v }
186    | 0xA0 -> assert false (* P2 not modeled *)
187    | 0xB0 -> { status with p3 = v; p3_latch = v }
188    | 0x99 ->
189      if status.expected_out_time = `None then
190        { status with sbuf = v; expected_out_time = `Now }
191      else
192        (* a real assert false: trying to initiate a transmission whilst one is still active *)
193        assert false
194    | 0x8A -> { status with tl0 = v }
195    | 0x8B -> { status with tl1 = v }
196    | 0x8C -> { status with th0 = v }
197    | 0x8D -> { status with th1 = v }
198    | 0xC8 -> { status with t2con = v }
199    | 0xCA -> { status with rcap2l = v }
200    | 0xCB -> { status with rcap2h = v }
201    | 0xCD -> { status with tl2 = v }
202    | 0xCE -> { status with th2 = v }
203
204    (* control ports *)
205    | 0x87 -> { status with pcon = v }
206    | 0x88 -> { status with tcon = v }
207    | 0x89 -> { status with tmod = v }
208    | 0x98 -> { status with scon = v }
209    | 0xA8 -> { status with ie = v }
210    | 0xB8 -> { status with ip = v }
211     
212    (* registers *)
213    | 0x81 -> { status with sp = v }
214    | 0x82 -> { status with dpl = v }
215    | 0x83 -> { status with dph = v }
216    | 0xD0 -> { status with psw = v }
217    | 0xE0 -> { status with acc = v }
218    | 0xF0 -> { status with b = v }
219    | _ -> assert false
220;;
221
222let initialize = {
223  code_memory = Physical.WordMap.empty;
224  low_internal_ram = Byte7Map.empty;
225  high_internal_ram = Byte7Map.empty;
226  external_ram = Physical.WordMap.empty;
227 
228  pc = zero `Sixteen;
229 
230  sp = vect_of_int 7 `Eight;
231  dpl = zero `Eight;
232  dph = zero `Eight;
233  pcon = zero `Eight;
234  tcon = zero `Eight;
235  tmod = zero `Eight;
236  tl0 = zero `Eight;
237  tl1 = zero `Eight;
238  th0 = zero `Eight;
239  th1 = zero `Eight;
240  p1 = zero `Eight;
241  p1_latch = zero `Eight;
242  scon = zero `Eight;
243  sbuf = zero `Eight;
244  ie = zero `Eight;
245  p3 = zero `Eight;
246  p3_latch = zero `Eight;
247  ip = zero `Eight;
248  psw = zero `Eight;
249  acc = zero `Eight;
250  b = zero `Eight;
251  t2con = zero `Eight;
252  rcap2l = zero `Eight;
253  rcap2h = zero `Eight;
254  tl2 = zero `Eight;
255  th2 = zero `Eight;
256
257  previous_p1_val = false;
258  previous_p3_val = false;
259
260  serial_v_in = None;
261  serial_v_out = None;
262  serial_epsilon_in = None;
263  serial_epsilon_out = None;
264  serial_k_out = None;
265
266  io_epsilon = 5;
267
268  clock = 0;
269  timer0 = zero `Sixteen;
270  timer1 = zero `Sixteen;
271  timer2 = zero `Sixteen;
272
273  expected_out_time = `None;
274
275  io = debug_continuation; (* a real assert false: unprepared for i/o *)
276
277  (* Initially no interrupts are executing *)
278  esi_running = false;
279  t0i_running = false;
280  t1i_running = false;
281  e0i_running = false;
282  e1i_running = false;
283  es_running = false;
284
285  exit_addr = BitVectors.zero `Sixteen;
286  cost_labels = BitVectors.WordMap.empty
287}
288
289let get_cy_flag status =
290  let (cy,_,_,_),(_,_,_,_) = bits_of_byte status.psw in cy
291let get_ac_flag status =
292  let (_,ac,_,_),(_,_,_,_) = bits_of_byte status.psw in ac
293let get_fo_flag status =
294  let (_,_,fo,_),(_,_,_,_) = bits_of_byte status.psw in fo
295let get_rs1_flag status =
296  let (_,_,_,rs1),(_,_,_,_) = bits_of_byte status.psw in rs1
297let get_rs0_flag status =
298  let (_,_,_,_),(rs0,_,_,_) = bits_of_byte status.psw in rs0
299let get_ov_flag status =
300  let (_,_,_,_),(_,ov,_,_) = bits_of_byte status.psw in ov
301let get_ud_flag status =
302  let (_,_,_,_),(_,_,ud,_) = bits_of_byte status.psw in ud
303let get_p_flag status =
304  let (_,_,_,_),(_,_,_,p) = bits_of_byte status.psw in p
305
306let get_address_of_register status (b1,b2,b3) =
307  let bu,_bl = from_byte status.psw in
308  let (_,_,rs1,rs0) = from_nibble bu in
309  let base =
310    match rs1,rs0 with
311        false,false -> 0x00
312      | false,true  -> 0x08
313      | true,false  -> 0x10
314      | true,true   -> 0x18
315  in
316  vect_of_int (base + int_of_vect (mk_nibble false b1 b2 b3)) `Seven
317;;
318
319let get_register status reg =
320  let addr = get_address_of_register status reg in
321  Byte7Map.find addr status.low_internal_ram
322;;
323
324let string_of_status status =   
325  let acc_str = (string_of_int <*> int_of_vect $ status.acc) ^ " (" ^ string_of_vect status.acc ^ ")" in
326  let b_str   = (string_of_int <*> int_of_vect $ status.b) ^ " (" ^ string_of_vect status.b ^ ")" in
327  let psw_str = (string_of_int <*> int_of_vect $ status.psw) ^ " (" ^ string_of_vect status.psw ^ ")" in
328  let sp_str  = (string_of_int <*> int_of_vect $ status.sp) ^ " (" ^ string_of_vect status.sp ^ ")" in
329  let ip_str  = (string_of_int <*> int_of_vect $ status.ip) ^ " (" ^ string_of_vect status.ip ^ ")" in
330  let pc_str  = (string_of_int <*> int_of_vect $ status.pc) ^ " (" ^ string_of_vect status.pc ^ ")" in
331  let dpl_str = (string_of_int <*> int_of_vect $ status.dpl) ^ " (" ^ string_of_vect status.dpl ^ ")" in
332  let dph_str = (string_of_int <*> int_of_vect $ status.dph) ^ " (" ^ string_of_vect status.dph ^ ")" in
333  let scn_str = (string_of_int <*> int_of_vect $ status.scon) ^ " (" ^ string_of_vect status.scon ^ ")" in
334  let sbf_str = (string_of_int <*> int_of_vect $ status.sbuf) ^ " (" ^ string_of_vect status.sbuf ^ ")" in
335  let tcn_str = (string_of_int <*> int_of_vect $ status.tcon) ^ " (" ^ string_of_vect status.tcon ^ ")" in
336  let tmd_str = (string_of_int <*> int_of_vect $ status.tmod) ^ " (" ^ string_of_vect status.tmod ^ ")" in
337  let r0_str  = (string_of_int <*> int_of_vect $ get_register status (false, false, false)) ^ " (" ^ (string_of_vect $ get_register status (false, false, false)) ^ ")" in
338  let r1_str  = (string_of_int <*> int_of_vect $ get_register status (false, false, true)) ^ " (" ^ (string_of_vect $ get_register status (false, false, true)) ^ ")" in
339  let r2_str  = (string_of_int <*> int_of_vect $ get_register status (false, true, false)) ^ " (" ^ (string_of_vect $ get_register status (false, true, false)) ^ ")" in
340  let r3_str  = (string_of_int <*> int_of_vect $ get_register status (false, true, true)) ^ " (" ^ (string_of_vect $ get_register status (false, true, true)) ^ ")" in
341  let r4_str  = (string_of_int <*> int_of_vect $ get_register status (true, false, false)) ^ " (" ^ (string_of_vect $ get_register status (true, false, false)) ^ ")" in
342  let r5_str  = (string_of_int <*> int_of_vect $ get_register status (true, false, true)) ^ " (" ^ (string_of_vect $ get_register status (true, false, true)) ^ ")" in
343  let r6_str  = (string_of_int <*> int_of_vect $ get_register status (true, true, false)) ^ " (" ^ (string_of_vect $ get_register status (true, true, false)) ^ ")" in
344  let r7_str  = (string_of_int <*> int_of_vect $ get_register status (true, true, true)) ^ " (" ^ (string_of_vect $ get_register status (true, true, true)) ^ ")" in
345    "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
346    " Processor status:                               \n" ^
347    "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n" ^
348    "   ACC : " ^ acc_str ^ "\n"                          ^
349    "   B   : " ^ b_str   ^ "\n"                          ^
350    "   PSW : " ^ psw_str ^ "\n"                          ^
351    "    with flags set as                            \n" ^
352    "     CY  : " ^ (string_of_bool <*> get_cy_flag $ status) ^ "\n" ^
353    "     AC  : " ^ (string_of_bool <*> get_ac_flag $ status) ^ "\n" ^
354    "     FO  : " ^ (string_of_bool <*> get_fo_flag $ status) ^ "\n" ^
355    "     RS1 : " ^ (string_of_bool <*> get_rs1_flag $ status) ^ "\n" ^
356    "     RS0 : " ^ (string_of_bool <*> get_rs0_flag $ status) ^ "\n" ^
357    "     OV  : " ^ (string_of_bool <*> get_ov_flag $ status) ^ "\n" ^
358    "     UD  : " ^ (string_of_bool <*> get_ud_flag $ status) ^ "\n" ^
359    "     P   : " ^ (string_of_bool <*> get_p_flag $ status) ^ "\n" ^
360    "   SP  : " ^ sp_str  ^ "\n"                          ^
361    "   IP  : " ^ ip_str  ^ "\n"                          ^
362    "   PC  : " ^ pc_str  ^ "\n"                          ^
363    "   DPL : " ^ dpl_str ^ "\n"                          ^
364    "   DPH : " ^ dph_str ^ "\n"                          ^
365    "   SCON: " ^ scn_str ^ "\n"                          ^
366    "   SBUF: " ^ sbf_str ^ "\n"                          ^
367    "   TMOD: " ^ tmd_str ^ "\n"                          ^
368    "   TCON: " ^ tcn_str ^ "\n"                          ^
369    "   Registers:                                    \n" ^
370    "    R0 : " ^ r0_str  ^ "\n"                          ^
371    "    R1 : " ^ r1_str  ^ "\n"                          ^
372    "    R2 : " ^ r2_str  ^ "\n"                          ^
373    "    R3 : " ^ r3_str  ^ "\n"                          ^
374    "    R4 : " ^ r4_str  ^ "\n"                          ^
375    "    R5 : " ^ r5_str  ^ "\n"                          ^
376    "    R6 : " ^ r6_str  ^ "\n"                          ^
377    "    R7 : " ^ r7_str  ^ "\n"                          ^
378    "-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-\n"
379
380(* timings taken from SIEMENS *)
381
382let fetch pmem pc =
383  let next pc =
384    let _carry, res = half_add pc (vect_of_int 1 `Sixteen) in
385    res, Physical.WordMap.find pc pmem
386  in
387  let pc,instr = next pc in
388  let un, ln = from_byte instr in
389  let bits = (from_nibble un, from_nibble ln) in
390  match bits with
391      (a10,a9,a8,true),(false,false,false,true) ->
392        let pc,b1 = next pc in
393        `ACALL (`ADDR11 (mk_word11 a10 a9 a8 b1)), pc, 2
394    | (false,false,true,false),(true,r1,r2,r3) ->
395      `ADD (`A,`REG (r1,r2,r3)), pc, 1
396    | (false,false,true,false),(false,true,false,true) ->
397      let pc,b1 = next pc in
398      `ADD (`A,`DIRECT b1), pc, 1
399    | (false,false,true,false),(false,true,true,i1) ->
400      `ADD (`A,`INDIRECT i1), pc, 1
401    | (false,false,true,false),(false,true,false,false) ->
402      let pc,b1 = next pc in
403      `ADD (`A,`DATA b1), pc, 1
404    | (false,false,true,true),(true,r1,r2,r3) ->
405      `ADDC (`A,`REG (r1,r2,r3)), pc, 1
406    | (false,false,true,true),(false,true,false,true) ->
407      let pc,b1 = next pc in
408      `ADDC (`A,`DIRECT b1), pc, 1
409    | (false,false,true,true),(false,true,true,i1) ->
410      `ADDC (`A,`INDIRECT i1), pc, 1
411    | (false,false,true,true),(false,true,false,false) ->
412      let pc,b1 = next pc in
413      `ADDC (`A,`DATA b1), pc, 1
414    | (a10,a9,a8,false),(false,false,false,true) ->
415      let pc,b1 = next pc in
416      `AJMP (`ADDR11 (mk_word11 a10 a9 a8 b1)), pc, 2
417    | (false,true,false,true),(true,r1,r2,r3) ->
418      `ANL (`U1 (`A, `REG (r1,r2,r3))), pc, 1
419    | (false,true,false,true),(false,true,false,true) ->
420      let pc,b1 = next pc in
421      `ANL (`U1 (`A, `DIRECT b1)), pc, 1
422    | (false,true,false,true),(false,true,true,i1) ->
423      `ANL (`U1 (`A, `INDIRECT i1)), pc, 1
424    | (false,true,false,true),(false,true,false,false) ->
425      let pc,b1 = next pc in
426      `ANL (`U1 (`A, `DATA b1)), pc, 1
427    | (false,true,false,true),(false,false,true,false) ->
428      let pc,b1 = next pc in
429      `ANL (`U2 (`DIRECT b1,`A)), pc, 1
430    | (false,true,false,true),(false,false,true,true) ->
431      let pc,b1 = next pc in
432      let pc,b2 = next pc in
433      `ANL (`U2 (`DIRECT b1,`DATA b2)), pc, 2
434    | (true,false,false,false),(false,false,true,false) ->
435      let pc,b1 = next pc in
436      `ANL (`U3 (`C,`BIT b1)), pc, 2
437    | (true,false,true,true),(false,false,false,false) ->
438      let pc,b1 = next pc in
439      `ANL (`U3 (`C,`NBIT b1)), pc, 2
440    | (true,false,true,true),(false,true,false,true) ->
441      let pc,b1 = next pc in
442      let pc,b2 = next pc in
443      `CJNE (`U1 (`A, `DIRECT b1), `REL b2), pc, 2
444    | (true,false,true,true),(false,true,false,false) ->
445      let pc,b1 = next pc in
446      let pc,b2 = next pc in
447      `CJNE (`U1 (`A, `DATA b1), `REL b2), pc, 2
448    | (true,false,true,true),(true,r1,r2,r3) ->
449      let pc,b1 = next pc in
450      let pc,b2 = next pc in
451      `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2), pc, 2
452    | (true,false,true,true),(false,true,true,i1) ->
453      let pc,b1 = next pc in
454      let pc,b2 = next pc in
455      `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2), pc, 2
456    | (true,true,true,false),(false,true,false,false) ->
457      `CLR `A, pc, 1
458    | (true,true,false,false),(false,false,true,true) ->
459      `CLR `C, pc, 1
460    | (true,true,false,false),(false,false,true,false) ->
461      let pc,b1 = next pc in
462      `CLR (`BIT b1), pc, 1
463    | (true,true,true,true),(false,true,false,false) ->
464      `CPL `A, pc, 1
465    | (true,false,true,true),(false,false,true,true) ->
466      `CPL `C, pc, 1
467    | (true,false,true,true),(false,false,true,false) ->
468      let pc,b1 = next pc in
469      `CPL (`BIT b1), pc, 1
470    | (true,true,false,true),(false,true,false,false) ->
471      `DA `A, pc, 1
472    | (false,false,false,true),(false,true,false,false) ->
473      `DEC `A, pc, 1
474    | (false,false,false,true),(true,r1,r2,r3) ->
475      `DEC (`REG(r1,r2,r3)), pc, 1
476    | (false,false,false,true),(false,true,false,true) ->
477      let pc,b1 = next pc in
478      `DEC (`DIRECT b1), pc, 1
479    | (false,false,false,true),(false,true,true,i1) ->
480      `DEC (`INDIRECT i1), pc, 1
481    | (true,false,false,false),(false,true,false,false) ->
482      `DIV (`A, `B), pc, 4
483    | (true,true,false,true),(true,r1,r2,r3) ->
484      let pc,b1 = next pc in
485      `DJNZ (`REG(r1,r2,r3), `REL b1), pc, 2
486    | (true,true,false,true),(false,true,false,true) ->
487      let pc,b1 = next pc in
488      let pc,b2 = next pc in
489      `DJNZ (`DIRECT b1, `REL b2), pc, 2
490    | (false,false,false,false),(false,true,false,false) ->
491      `INC `A, pc, 1
492    | (false,false,false,false),(true,r1,r2,r3) ->
493      `INC (`REG(r1,r2,r3)), pc, 1
494    | (false,false,false,false),(false,true,false,true) ->
495      let pc,b1 = next pc in
496      `INC (`DIRECT b1), pc, 1
497    | (false,false,false,false),(false,true,true,i1) ->
498      `INC (`INDIRECT i1), pc, 1
499    | (true,false,true,false),(false,false,true,true) ->
500      `INC `DPTR, pc, 2
501    | (false,false,true,false),(false,false,false,false) ->
502      let pc,b1 = next pc in
503      let pc,b2 = next pc in
504      `JB (`BIT b1, `REL b2), pc, 2
505    | (false,false,false,true),(false,false,false,false) ->
506      let pc,b1 = next pc in
507      let pc,b2 = next pc in
508      `JBC (`BIT b1, `REL b2), pc, 2
509    | (false,true,false,false),(false,false,false,false) ->
510      let pc,b1 = next pc in
511      `JC (`REL b1), pc, 2
512    | (false,true,true,true),(false,false,true,true) ->
513      `JMP `IND_DPTR, pc, 2
514    | (false,false,true,true),(false,false,false,false) ->
515      let pc,b1 = next pc in
516      let pc,b2 = next pc in
517      `JNB (`BIT b1, `REL b2), pc, 2
518    | (false,true,false,true),(false,false,false,false) ->
519      let pc,b1 = next pc in
520      `JNC (`REL b1), pc, 2
521    | (false,true,true,true),(false,false,false,false) ->
522      let pc,b1 = next pc in
523      `JNZ (`REL b1), pc, 2
524    | (false,true,true,false),(false,false,false,false) ->
525      let pc,b1 = next pc in
526      `JZ (`REL b1), pc, 2
527    | (false,false,false,true),(false,false,true,false) ->
528      let pc,b1 = next pc in
529      let pc,b2 = next pc in
530      `LCALL (`ADDR16 (mk_word b1 b2)), pc, 2
531    | (false,false,false,false),(false,false,true,false) ->
532      let pc,b1 = next pc in
533      let pc,b2 = next pc in
534      `LJMP (`ADDR16 (mk_word b1 b2)), pc, 2
535   | (true,true,true,false),(true,r1,r2,r3) ->
536         `MOV (`U1 (`A, `REG(r1,r2,r3))), pc, 1
537   | (true,true,true,false),(false,true,false,true) ->
538       let pc,b1 = next pc in
539         `MOV (`U1 (`A, `DIRECT b1)), pc, 1
540   | (true,true,true,false),(false,true,true,i1) ->
541         `MOV (`U1 (`A, `INDIRECT i1)), pc, 1
542   | (false,true,true,true),(false,true,false,false) ->
543       let pc,b1 = next pc in
544         `MOV (`U1 (`A, `DATA b1)), pc, 1
545   | (true,true,true,true),(true,r1,r2,r3) ->
546         `MOV (`U2 (`REG(r1,r2,r3), `A)), pc, 1
547   | (true,false,true,false),(true,r1,r2,r3) ->
548       let pc,b1 = next pc in
549         `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))), pc, 2
550   | (false,true,true,true),(true,r1,r2,r3) ->
551       let pc,b1 = next pc in
552         `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))), pc, 1
553   | (true,true,true,true),(false,true,false,true) ->
554       let pc,b1 = next pc in
555         `MOV (`U3 (`DIRECT b1, `A)), pc, 1
556   | (true,false,false,false),(true,r1,r2,r3) ->
557       let pc,b1 = next pc in
558         `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))), pc, 2
559   | (true,false,false,false),(false,true,false,true) ->
560       let pc,b1 = next pc in
561       let pc,b2 = next pc in
562         `MOV (`U3 (`DIRECT b1, `DIRECT b2)), pc, 2
563   | (true,false,false,false),(false,true,true,i1) ->
564       let pc,b1 = next pc in
565         `MOV (`U3 (`DIRECT b1, `INDIRECT i1)), pc, 2
566   | (false,true,true,true),(false,true,false,true) ->
567       let pc,b1 = next pc in
568       let pc,b2 = next pc in
569         `MOV (`U3 (`DIRECT b1, `DATA b2)), pc, 3
570   | (true,true,true,true),(false,true,true,i1) ->
571         `MOV (`U2 (`INDIRECT i1, `A)), pc, 1
572   | (true,false,true,false),(false,true,true,i1) ->
573       let pc,b1 = next pc in
574         `MOV (`U2 (`INDIRECT i1, `DIRECT b1)), pc, 2
575   | (false,true,true,true),(false,true,true,i1) ->
576       let pc,b1 = next pc in
577         `MOV (`U2 (`INDIRECT i1, `DATA b1)), pc, 1
578   | (true,false,true,false),(false,false,true,false) ->
579       let pc,b1 = next pc in
580         `MOV (`U5 (`C, `BIT b1)), pc, 1
581   | (true,false,false,true),(false,false,true,false) ->
582       let pc,b1 = next pc in
583         `MOV (`U6 (`BIT b1, `C)), pc, 2
584   | (true,false,false,true),(false,false,false,false) ->
585       let pc,b1 = next pc in
586       let pc,b2 = next pc in
587         `MOV (`U4 (`DPTR, `DATA16(mk_word b1 b2))), pc, 2
588   | (true,false,false,true),(false,false,true,true) ->
589         `MOVC (`A, `A_DPTR), pc, 2
590   | (true,false,false,false),(false,false,true,true) ->
591         `MOVC (`A, `A_PC), pc, 2
592   | (true,true,true,false),(false,false,true,i1) ->
593         `MOVX (`U1 (`A, `EXT_INDIRECT i1)), pc, 2
594   | (true,true,true,false),(false,false,false,false) ->
595         `MOVX (`U1 (`A, `EXT_IND_DPTR)), pc, 2
596   | (true,true,true,true),(false,false,true,i1) ->
597         `MOVX (`U2 (`EXT_INDIRECT i1, `A)), pc, 2
598   | (true,true,true,true),(false,false,false,false) ->
599         `MOVX (`U2 (`EXT_IND_DPTR, `A)), pc, 2
600   | (true,false,true,false),(false,true,false,false) ->
601         `MUL(`A, `B), pc, 4
602   | (false,false,false,false),(false,false,false,false) ->
603         `NOP, pc, 1
604   | (false,true,false,false),(true,r1,r2,r3) ->
605         `ORL (`U1(`A, `REG(r1,r2,r3))), pc, 1
606   | (false,true,false,false),(false,true,false,true) ->
607       let pc,b1 = next pc in
608         `ORL (`U1(`A, `DIRECT b1)), pc, 1
609   | (false,true,false,false),(false,true,true,i1) ->
610         `ORL (`U1(`A, `INDIRECT i1)), pc, 1
611   | (false,true,false,false),(false,true,false,false) ->
612       let pc,b1 = next pc in
613         `ORL (`U1(`A, `DATA b1)), pc, 1
614   | (false,true,false,false),(false,false,true,false) ->
615       let pc,b1 = next pc in
616         `ORL (`U2(`DIRECT b1, `A)), pc, 1
617   | (false,true,false,false),(false,false,true,true) ->
618       let pc,b1 = next pc in
619       let pc,b2 = next pc in
620         `ORL (`U2 (`DIRECT b1, `DATA b2)), pc, 2
621   | (false,true,true,true),(false,false,true,false) ->
622       let pc,b1 = next pc in
623         `ORL (`U3 (`C, `BIT b1)), pc, 2
624   | (true,false,true,false),(false,false,false,false) ->
625       let pc,b1 = next pc in
626         `ORL (`U3 (`C, `NBIT b1)), pc, 2
627   | (true,true,false,true),(false,false,false,false) ->
628       let pc,b1 = next pc in
629         `POP (`DIRECT b1), pc, 2
630   | (true,true,false,false),(false,false,false,false) ->
631       let pc,b1 = next pc in
632         `PUSH (`DIRECT b1), pc, 2
633   | (false,false,true,false),(false,false,true,false) ->
634         `RET, pc, 2
635   | (false,false,true,true),(false,false,true,false) ->
636         `RETI, pc, 2
637   | (false,false,true,false),(false,false,true,true) ->
638         `RL `A, pc, 1
639   | (false,false,true,true),(false,false,true,true) ->
640         `RLC `A, pc, 1
641   | (false,false,false,false),(false,false,true,true) ->
642         `RR `A, pc, 1
643   | (false,false,false,true),(false,false,true,true) ->
644         `RRC `A, pc, 1
645   | (true,true,false,true),(false,false,true,true) ->
646         `SETB `C, pc, 1
647   | (true,true,false,true),(false,false,true,false) ->
648       let pc,b1 = next pc in
649         `SETB (`BIT b1), pc, 1
650   | (true,false,false,false),(false,false,false,false) ->
651       let pc,b1 = next pc in
652         `SJMP (`REL b1), pc, 2
653   | (true,false,false,true),(true,r1,r2,r3) ->
654       `SUBB (`A, `REG(r1,r2,r3)), pc, 1
655   | (true,false,false,true),(false,true,false,true) ->
656       let pc,b1 = next pc in
657         `SUBB (`A, `DIRECT b1), pc, 1
658   | (true,false,false,true),(false,true,true,i1) ->
659         `SUBB (`A, `INDIRECT i1), pc, 1
660   | (true,false,false,true),(false,true,false,false) ->
661       let pc,b1 = next pc in
662         `SUBB (`A, `DATA b1), pc, 1
663   | (true,true,false,false),(false,true,false,false) ->
664         `SWAP `A, pc, 1
665   | (true,true,false,false),(true,r1,r2,r3) ->
666         `XCH (`A, `REG(r1,r2,r3)), pc, 1
667   | (true,true,false,false),(false,true,false,true) ->
668       let pc,b1 = next pc in
669         `XCH (`A, `DIRECT b1), pc, 1
670   | (true,true,false,false),(false,true,true,i1) ->
671         `XCH (`A, `INDIRECT i1), pc, 1
672   | (true,true,false,true),(false,true,true,i1) ->
673         `XCHD(`A, `INDIRECT i1), pc, 1
674   | (false,true,true,false),(true,r1,r2,r3) ->
675         `XRL(`U1(`A, `REG(r1,r2,r3))), pc, 1
676   | (false,true,true,false),(false,true,false,true) ->
677       let pc,b1 = next pc in
678         `XRL(`U1(`A, `DIRECT b1)), pc, 1
679   | (false,true,true,false),(false,true,true,i1) ->
680         `XRL(`U1(`A, `INDIRECT i1)), pc, 1
681   | (false,true,true,false),(false,true,false,false) ->
682       let pc,b1 = next pc in
683         `XRL(`U1(`A, `DATA b1)), pc, 1
684   | (false,true,true,false),(false,false,true,false) ->
685       let pc,b1 = next pc in
686         `XRL(`U2(`DIRECT b1, `A)), pc, 1
687   | (false,true,true,false),(false,false,true,true) ->
688       let pc,b1 = next pc in
689       let pc,b2 = next pc in
690         `XRL(`U2(`DIRECT b1, `DATA b2)), pc, 2
691   | (true,false,true,false),(false,true,false,true) ->
692       (* undefined opcode *) assert false
693;;
694
695let assembly1 =
696 function
697    `ACALL (`ADDR11 w) ->
698      let (a10,a9,a8,b1) = from_word11 w in
699        [mk_byte_from_bits ((a10,a9,a8,true),(false,false,false,true)); b1]
700  | `ADD (`A,`REG (r1,r2,r3)) ->
701     [mk_byte_from_bits ((false,false,true,false),(true,r1,r2,r3))]
702  | `ADD (`A, `DIRECT b1) ->
703     [mk_byte_from_bits ((false,false,true,false),(false,true,false,true)); b1]
704  | `ADD (`A, `INDIRECT i1) ->
705     [mk_byte_from_bits ((false,false,true,false),(false,true,true,i1))]
706  | `ADD (`A, `DATA b1) ->
707     [mk_byte_from_bits ((false,false,true,false),(false,true,false,false)); b1]
708  | `ADDC (`A, `REG(r1,r2,r3)) ->
709     [mk_byte_from_bits ((false,false,true,true),(true,r1,r2,r3))]
710  | `ADDC (`A, `DIRECT b1) ->
711     [mk_byte_from_bits ((false,false,true,true),(false,true,false,true)); b1]
712  | `ADDC (`A,`INDIRECT i1) ->
713     [mk_byte_from_bits ((false,false,true,true),(false,true,true,i1))]
714  | `ADDC (`A,`DATA b1) ->
715     [mk_byte_from_bits ((false,false,true,true),(false,true,false,false)); b1]
716  | `AJMP (`ADDR11 w) ->
717     let (a10,a9,a8,b1) = from_word11 w in
718       [mk_byte_from_bits ((a10,a9,a8,false),(false,false,false,true)); b1]
719  | `ANL (`U1 (`A, `REG (r1,r2,r3))) ->
720     [mk_byte_from_bits ((false,true,false,true),(true,r1,r2,r3))]
721  | `ANL (`U1 (`A, `DIRECT b1)) ->
722     [mk_byte_from_bits ((false,true,false,true),(false,true,false,true)); b1]
723  | `ANL (`U1 (`A, `INDIRECT i1)) ->
724     [mk_byte_from_bits ((false,true,false,true),(false,true,true,i1))]
725  | `ANL (`U1 (`A, `DATA b1)) ->
726     [mk_byte_from_bits ((false,true,false,true),(false,true,false,false)); b1]
727  | `ANL (`U2 (`DIRECT b1,`A)) ->
728     [mk_byte_from_bits ((false,true,false,true),(false,false,true,false)); b1]
729  | `ANL (`U2 (`DIRECT b1,`DATA b2)) ->
730     [mk_byte_from_bits ((false,true,false,true),(false,false,true,true)); b1; b2]
731  | `ANL (`U3 (`C,`BIT b1)) ->
732     [mk_byte_from_bits ((true,false,false,false),(false,false,true,false)); b1]
733  | `ANL (`U3 (`C,`NBIT b1)) ->
734    [mk_byte_from_bits ((true,false,true,true),(false,false,false,false)); b1]
735  | `CJNE (`U1 (`A, `DIRECT b1), `REL b2) ->
736    [mk_byte_from_bits ((true,false,true,true),(false,true,false,true)); b1; b2]
737  | `CJNE (`U1 (`A, `DATA b1), `REL b2) ->
738    [mk_byte_from_bits ((true,false,true,true),(false,true,false,false)); b1; b2]
739  | `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) ->
740    [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2]
741  | `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) ->
742    [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2]
743  | `CLR `A ->
744    [mk_byte_from_bits ((true,true,true,false),(false,true,false,false))]
745  | `CLR `C ->
746    [mk_byte_from_bits ((true,true,false,false),(false,false,true,true))]
747  | `CLR (`BIT b1) ->
748    [mk_byte_from_bits ((true,true,false,false),(false,false,true,false)); b1]
749  | `CPL `A ->
750    [mk_byte_from_bits ((true,true,true,true),(false,true,false,false))]
751  | `CPL `C ->
752    [mk_byte_from_bits ((true,false,true,true),(false,false,true,true))]
753  | `CPL (`BIT b1) ->
754    [mk_byte_from_bits ((true,false,true,true),(false,false,true,false)); b1]
755  | `DA `A ->
756    [mk_byte_from_bits ((true,true,false,true),(false,true,false,false))]
757  | `DEC `A ->
758    [mk_byte_from_bits ((false,false,false,true),(false,true,false,false))]
759  | `DEC (`REG(r1,r2,r3)) ->
760    [mk_byte_from_bits ((false,false,false,true),(true,r1,r2,r3))]
761  | `DEC (`DIRECT b1) ->
762    [mk_byte_from_bits ((false,false,false,true),(false,true,false,true)); b1]
763  | `DEC (`INDIRECT i1) ->
764    [mk_byte_from_bits ((false,false,false,true),(false,true,true,i1))]
765  | `DIV (`A, `B) ->
766    [mk_byte_from_bits ((true,false,false,false),(false,true,false,false))]
767  | `DJNZ (`REG(r1,r2,r3), `REL b1) ->
768    [mk_byte_from_bits ((true,true,false,true),(true,r1,r2,r3)); b1]
769  | `DJNZ (`DIRECT b1, `REL b2) ->
770    [mk_byte_from_bits ((true,true,false,true),(false,true,false,true)); b1; b2]
771  | `INC `A ->
772    [mk_byte_from_bits ((false,false,false,false),(false,true,false,false))]
773  | `INC (`REG(r1,r2,r3)) ->
774    [mk_byte_from_bits ((false,false,false,false),(true,r1,r2,r3))]
775  | `INC (`DIRECT b1) ->
776    [mk_byte_from_bits ((false,false,false,false),(false,true,false,true)); b1]
777  | `INC (`INDIRECT i1) ->
778    [mk_byte_from_bits ((false,false,false,false),(false,true,true,i1))]
779  | `INC `DPTR ->
780    [mk_byte_from_bits ((true,false,true,false),(false,false,true,true))]
781  | `JB (`BIT b1, `REL b2) ->
782    [mk_byte_from_bits ((false,false,true,false),(false,false,false,false)); b1; b2]
783  | `JBC (`BIT b1, `REL b2) ->
784    [mk_byte_from_bits ((false,false,false,true),(false,false,false,false)); b1; b2]
785  | `JC (`REL b1) ->
786    [mk_byte_from_bits ((false,true,false,false),(false,false,false,false)); b1]
787  | `JMP `IND_DPTR ->
788    [mk_byte_from_bits ((false,true,true,true),(false,false,true,true))]
789  | `JNB (`BIT b1, `REL b2) ->
790    [mk_byte_from_bits ((false,false,true,true),(false,false,false,false)); b1; b2]
791  | `JNC (`REL b1) ->
792    [mk_byte_from_bits ((false,true,false,true),(false,false,false,false)); b1]
793  | `JNZ (`REL b1) ->
794    [mk_byte_from_bits ((false,true,true,true),(false,false,false,false)); b1]
795  | `JZ (`REL b1) ->
796    [mk_byte_from_bits ((false,true,true,false),(false,false,false,false)); b1]
797  | `LCALL (`ADDR16 w) ->
798      let (b1,b2) = from_word w in
799        [mk_byte_from_bits ((false,false,false,true),(false,false,true,false)); b1; b2]
800  | `LJMP (`ADDR16 w) ->
801      let (b1,b2) = from_word w in
802        [mk_byte_from_bits ((false,false,false,false),(false,false,true,false)); b1; b2]
803  | `MOV (`U1 (`A, `REG(r1,r2,r3))) ->
804    [mk_byte_from_bits ((true,true,true,false),(true,r1,r2,r3))]
805  | `MOV (`U1 (`A, `DIRECT b1)) ->
806    [mk_byte_from_bits ((true,true,true,false),(false,true,false,true)); b1]
807  | `MOV (`U1 (`A, `INDIRECT i1)) ->
808    [mk_byte_from_bits ((true,true,true,false),(false,true,true,i1))]
809  | `MOV (`U1 (`A, `DATA b1)) ->
810    [mk_byte_from_bits ((false,true,true,true),(false,true,false,false)); b1]
811  | `MOV (`U2 (`REG(r1,r2,r3), `A)) ->
812    [mk_byte_from_bits ((true,true,true,true),(true,r1,r2,r3))]
813  | `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))) ->
814    [mk_byte_from_bits ((true,false,true,false),(true,r1,r2,r3)); b1]
815  | `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))) ->
816    [mk_byte_from_bits ((false,true,true,true),(true,r1,r2,r3)); b1]
817  | `MOV (`U3 (`DIRECT b1, `A)) ->
818    [mk_byte_from_bits ((true,true,true,true),(false,true,false,true)); b1]
819  | `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))) ->
820    [mk_byte_from_bits ((true,false,false,false),(true,r1,r2,r3)); b1]
821  | `MOV (`U3 (`DIRECT b1, `DIRECT b2)) ->
822    [mk_byte_from_bits ((true,false,false,false),(false,true,false,true)); b1; b2]
823  | `MOV (`U3 (`DIRECT b1, `INDIRECT i1)) ->
824    [mk_byte_from_bits ((true,false,false,false),(false,true,true,i1)); b1]
825  | `MOV (`U3 (`DIRECT b1, `DATA b2)) ->
826    [mk_byte_from_bits ((false,true,true,true),(false,true,false,true)); b1; b2]
827  | `MOV (`U2 (`INDIRECT i1, `A)) ->
828    [mk_byte_from_bits ((true,true,true,true),(false,true,true,i1))]
829  | `MOV (`U2 (`INDIRECT i1, `DIRECT b1)) ->
830    [mk_byte_from_bits ((true,false,true,false),(false,true,true,i1)); b1]
831  | `MOV (`U2 (`INDIRECT i1, `DATA b1)) ->
832    [mk_byte_from_bits ((false,true,true,true),(false,true,true,i1)); b1]
833  | `MOV (`U5 (`C, `BIT b1)) ->
834    [mk_byte_from_bits ((true,false,true,false),(false,false,true,false)); b1]
835  | `MOV (`U6 (`BIT b1, `C)) ->
836    [mk_byte_from_bits ((true,false,false,true),(false,false,true,false)); b1]
837  | `MOV (`U4 (`DPTR, `DATA16 w)) ->
838    let (b1,b2) = from_word w in
839      [mk_byte_from_bits ((true,false,false,true),(false,false,false,false)); b1; b2]
840  | `MOVC (`A, `A_DPTR) ->
841    [mk_byte_from_bits ((true,false,false,true),(false,false,true,true))]
842  | `MOVC (`A, `A_PC) ->
843    [mk_byte_from_bits ((true,false,false,false),(false,false,true,true))]
844  | `MOVX (`U1 (`A, `EXT_INDIRECT i1)) ->
845    [mk_byte_from_bits ((true,true,true,false),(false,false,true,i1))]
846  | `MOVX (`U1 (`A, `EXT_IND_DPTR)) ->
847    [mk_byte_from_bits ((true,true,true,false),(false,false,false,false))]
848  | `MOVX (`U2 (`EXT_INDIRECT i1, `A)) ->
849    [mk_byte_from_bits ((true,true,true,true),(false,false,true,i1))]
850  | `MOVX (`U2 (`EXT_IND_DPTR, `A)) ->
851    [mk_byte_from_bits ((true,true,true,true),(false,false,false,false))]
852  | `MUL(`A, `B) ->
853    [mk_byte_from_bits ((true,false,true,false),(false,true,false,false))]
854  | `NOP ->
855    [mk_byte_from_bits ((false,false,false,false),(false,false,false,false))]
856  | `ORL (`U1(`A, `REG(r1,r2,r3))) ->
857    [mk_byte_from_bits ((false,true,false,false),(true,r1,r2,r3))]
858  | `ORL (`U1(`A, `DIRECT b1)) ->
859    [mk_byte_from_bits ((false,true,false,false),(false,true,false,true)); b1]
860  | `ORL (`U1(`A, `INDIRECT i1)) ->
861    [mk_byte_from_bits ((false,true,false,false),(false,true,true,i1))]
862  | `ORL (`U1(`A, `DATA b1)) ->
863    [mk_byte_from_bits ((false,true,false,false),(false,true,false,false)); b1]
864  | `ORL (`U2(`DIRECT b1, `A)) ->
865    [mk_byte_from_bits ((false,true,false,false),(false,false,true,false)); b1]
866  | `ORL (`U2 (`DIRECT b1, `DATA b2)) ->
867    [mk_byte_from_bits ((false,true,false,false),(false,false,true,true)); b1; b2]
868  | `ORL (`U3 (`C, `BIT b1)) ->
869    [mk_byte_from_bits ((false,true,true,true),(false,false,true,false)); b1]
870  | `ORL (`U3 (`C, `NBIT b1)) ->
871    [mk_byte_from_bits ((true,false,true,false),(false,false,false,false)); b1]
872  | `POP (`DIRECT b1) ->
873    [mk_byte_from_bits ((true,true,false,true),(false,false,false,false)); b1]
874  | `PUSH (`DIRECT b1) ->
875    [mk_byte_from_bits ((true,true,false,false),(false,false,false,false)); b1]
876  | `RET ->
877    [mk_byte_from_bits ((false,false,true,false),(false,false,true,false))]
878  | `RETI ->
879    [mk_byte_from_bits ((false,false,true,true),(false,false,true,false))]
880  | `RL `A ->
881    [mk_byte_from_bits ((false,false,true,false),(false,false,true,true))]
882  | `RLC `A ->
883    [mk_byte_from_bits ((false,false,true,true),(false,false,true,true))]
884  | `RR `A ->
885    [mk_byte_from_bits ((false,false,false,false),(false,false,true,true))]
886  | `RRC `A ->
887    [mk_byte_from_bits ((false,false,false,true),(false,false,true,true))]
888  | `SETB `C ->
889    [mk_byte_from_bits ((true,true,false,true),(false,false,true,true))]
890  | `SETB (`BIT b1) ->
891    [mk_byte_from_bits ((true,true,false,true),(false,false,true,false)); b1]
892  | `SJMP (`REL b1) ->
893    [mk_byte_from_bits ((true,false,false,false),(false,false,false,false)); b1]
894  | `SUBB (`A, `REG(r1,r2,r3)) ->
895    [mk_byte_from_bits ((true,false,false,true),(true,r1,r2,r3))]
896  | `SUBB (`A, `DIRECT b1) ->
897    [mk_byte_from_bits ((true,false,false,true),(false,true,false,true)); b1]
898  | `SUBB (`A, `INDIRECT i1) ->
899    [mk_byte_from_bits ((true,false,false,true),(false,true,true,i1))]
900  | `SUBB (`A, `DATA b1) ->
901    [mk_byte_from_bits ((true,false,false,true),(false,true,false,false)); b1]
902  | `SWAP `A ->
903    [mk_byte_from_bits ((true,true,false,false),(false,true,false,false))]
904  | `XCH (`A, `REG(r1,r2,r3)) ->
905    [mk_byte_from_bits ((true,true,false,false),(true,r1,r2,r3))]
906  | `XCH (`A, `DIRECT b1) ->
907    [mk_byte_from_bits ((true,true,false,false),(false,true,false,true)); b1]
908  | `XCH (`A, `INDIRECT i1) ->
909    [mk_byte_from_bits ((true,true,false,false),(false,true,true,i1))]
910  | `XCHD(`A, `INDIRECT i1) ->
911    [mk_byte_from_bits ((true,true,false,true),(false,true,true,i1))]
912  | `XRL(`U1(`A, `REG(r1,r2,r3))) ->
913    [mk_byte_from_bits ((false,true,true,false),(true,r1,r2,r3))]
914  | `XRL(`U1(`A, `DIRECT b1)) ->
915    [mk_byte_from_bits ((false,true,true,false),(false,true,false,true)); b1]
916  | `XRL(`U1(`A, `INDIRECT i1)) ->
917    [mk_byte_from_bits ((false,true,true,false),(false,true,true,i1))]
918  | `XRL(`U1(`A, `DATA b1)) ->
919    [mk_byte_from_bits ((false,true,true,false),(false,true,false,false)); b1]
920  | `XRL(`U2(`DIRECT b1, `A)) ->
921    [mk_byte_from_bits ((false,true,true,false),(false,false,true,false)); b1]
922  | `XRL(`U2(`DIRECT b1, `DATA b2)) ->
923    [mk_byte_from_bits ((false,true,true,false),(false,false,true,true)); b1; b2]
924;;
925
926let load_code_memory = MiscPottier.foldi (fun i mem v -> Physical.WordMap.add (vect_of_int i `Sixteen) v mem) Physical.WordMap.empty
927
928let load_mem mem status = { status with code_memory = mem }
929let load l = load_mem (load_code_memory l)
930
931let assembly_jump addr_of =
932 function
933    `JC a1 -> `JC (addr_of a1)
934  | `JNC a1 -> `JNC (addr_of a1)
935  | `JB (a1,a2) -> `JB (a1,addr_of a2)
936  | `JNB (a1,a2) -> `JNB (a1,addr_of a2)
937  | `JBC (a1,a2) -> `JBC (a1,addr_of a2)
938  | `JZ a1 -> `JZ (addr_of a1)
939  | `JNZ a1 -> `JNZ (addr_of a1)
940  | `CJNE (a1,a2) -> `CJNE (a1,addr_of a2)
941  | `DJNZ (a1,a2) -> `DJNZ (a1,addr_of a2)
942;;
943
944let assembly p =
945 let datalabels,_ =
946  List.fold_left
947   (fun (datalabels,addr) (name,size) ->
948     let addr16 = vect_of_int addr `Sixteen in
949      StringTools.Map.add name addr16 datalabels, addr+size
950   ) (StringTools.Map.empty,0) p.ASM.ppreamble
951 in
952 let pc,exit_addr,labels,costs =
953  List.fold_left
954   (fun (pc,exit_addr,labels,costs) i ->
955     match i with
956        `Label s when s = p.ASM.pexit_label ->
957          pc, pc, StringTools.Map.add s pc labels, costs
958      | `Label s ->
959          pc, exit_addr, StringTools.Map.add s pc labels, costs
960      | `Cost s -> pc, exit_addr, labels, BitVectors.WordMap.add pc s costs
961      | `Mov (_,_) -> pc, exit_addr, labels, costs
962      | `Jmp _ 
963      | `Call _ ->
964        (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))),
965        exit_addr, labels, costs
966      (*CSC: very stupid: always expand to worst opcode *)
967      | `WithLabel i ->
968        let fake_addr _ = `REL (zero `Eight) in
969        let fake_jump = assembly_jump fake_addr i in
970        let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in
971        assert (fake_jump = i');
972        (snd (half_add pc pc'), exit_addr, labels, costs)
973      | #instruction as i ->
974        let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
975         assert (i = i');
976         (snd (half_add pc pc'),exit_addr,labels, costs)
977   )
978    (BitVectors.zero `Sixteen,BitVectors.zero `Sixteen,
979     StringTools.Map.empty, BitVectors.WordMap.empty) p.ASM.pcode
980 in
981 let code =
982  List.flatten (List.map
983     (function
984        `Label _
985      | `Cost _ -> []
986      | `WithLabel i ->
987         let translation = assert false (*
988           match i with
989             `JC (`Label a) -> (*
990               let offset = vect_of_int 2 `Eight in
991               let address = StringTools.Map.find a labels in *)
992                 assert false
993           | `JNC a ->
994               (* let offset = vect_of_int 2 `Eight in *)
995                 assert false
996           | `JB (b, a) ->
997               (* let offset = vect_of_int 3 `Eight in *)
998                 assert false
999           | `JNB (b, a) ->
1000               (* let offset = vect_of_int 3 `Eight in *)
1001                 assert false
1002           | `JBC (b, a) ->
1003               (* let offset = vect_of_int 2 `Eight in *)
1004                 assert false
1005           | `JZ a ->
1006               (* let offset = vect_of_int 2 `Eight in *)
1007                 assert false
1008           | `JNZ a ->
1009               (* let offset = vect_of_int 2 `Eight in *)
1010                 assert false
1011           | `CJNE (args, a) ->
1012               (* let offset = vect_of_int 3 `Eight in *)
1013                 assert false
1014           | `DJNZ ((`DIRECT, `REL _), a) ->
1015               (* let offset = vect_of_int 3 `Eight in *)
1016                 assert false
1017           | `DJNZ ((`REG _, `REL _), a) ->
1018               (* let offset = vect_of_int 2 `Eight in *)
1019                 assert false *)
1020         in
1021           List.flatten (List.map assembly1 translation)
1022      | `Mov (`DPTR,s) ->
1023          let addrr16 = StringTools.Map.find s datalabels in
1024           assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
1025      | `Jmp s ->
1026          let pc_offset = StringTools.Map.find s labels in
1027            assembly1 (`LJMP (`ADDR16 pc_offset))
1028      | `Call s ->
1029          let pc_offset = StringTools.Map.find s labels in
1030            assembly1 (`LCALL (`ADDR16 pc_offset ))
1031      | #instruction as i -> assembly1 i) p.ASM.pcode) in
1032 { ASM.code = code ; ASM.cost_labels = costs ;
1033   ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main }
1034;;
1035
1036let set_register status v reg =
1037  let addr = get_address_of_register status reg in
1038    { status with low_internal_ram =
1039        Byte7Map.add addr v status.low_internal_ram }
1040;;
1041
1042let get_arg_8 status from_latch = 
1043 function
1044    `DIRECT addr ->
1045       let n0, n1 = from_byte addr in
1046       (match from_nibble n0 with
1047          (false,r1,r2,r3) ->
1048            Byte7Map.find (mk_byte7 r1 r2 r3 n1) status.low_internal_ram
1049        | _ -> get_sfr status addr from_latch)
1050  | `INDIRECT b ->
1051       let (b1, b2) = from_byte (get_register status (false,false,b)) in
1052         (match (from_nibble b1, b2) with 
1053           (false,r1,r2,r3),b2 ->
1054             Byte7Map.find (mk_byte7 r1 r2 r3 b2) status.low_internal_ram
1055         | (true,r1,r2,r3),b2 ->
1056             Byte7Map.find (mk_byte7 r1 r2 r3 b2) status.high_internal_ram)
1057  | `REG (b1,b2,b3) -> get_register status (b1,b2,b3)
1058  | `A -> status.acc
1059  | `B -> status.b
1060  | `DATA b -> b
1061  | `A_DPTR ->
1062       let dpr = mk_word status.dph status.dpl in
1063       (* CSC: what is the right behaviour in case of overflow?
1064          assert false for now. Try to understand what DEC really does *)
1065       let cry,addr = half_add dpr (mk_word (vect_of_int 0 `Eight) status.acc) in
1066         Physical.WordMap.find addr status.external_ram
1067  | `A_PC ->
1068       (* CSC: what is the right behaviour in case of overflow?
1069          assert false for now *)
1070       let cry,addr = half_add status.pc (mk_word (vect_of_int 0 `Eight) status.acc) in
1071         Physical.WordMap.find addr status.external_ram
1072  | `EXT_INDIRECT b ->
1073         let addr = get_register status (false,false,b) in
1074           Physical.WordMap.find (mk_word (zero `Eight) addr) status.external_ram
1075  | `EXT_IND_DPTR ->
1076       let dpr = mk_word status.dph status.dpl in
1077         Physical.WordMap.find dpr status.external_ram
1078;;
1079
1080let get_arg_16 _status = function `DATA16 w -> w
1081
1082let get_arg_1 status from_latch =
1083  function
1084    `BIT addr
1085  | `NBIT addr as x ->
1086     let n1, n2 = from_byte addr in
1087     let res =
1088      (match from_nibble n1 with
1089         (false,r1,r2,r3) ->
1090           let addr = (int_of_vect (mk_byte7 r1 r2 r3 n2)) in
1091           let addr' = vect_of_int ((addr / 8) + 32) `Seven in
1092             get_bit (Byte7Map.find addr' status.low_internal_ram) (addr mod 8)
1093        | (true,r1,r2,r3) ->
1094            let addr = int_of_vect $ mk_byte7 r1 r2 r3 n2 in
1095            let div = addr / 8 in
1096            let rem = addr mod 8 in
1097              get_bit (get_sfr status (vect_of_int ((div * 8) + 128) `Eight) from_latch) rem)
1098    in (match x with `NBIT _ -> not res | _ -> res)
1099  | `C -> get_cy_flag status
1100
1101let set_arg_1 status v =
1102  function
1103    `BIT addr ->
1104      let n1, n2 = from_byte addr in
1105      (match from_nibble n1 with
1106         (false,r1,r2,r3) ->
1107           let addr = (int_of_vect (mk_byte7 r1 r2 r3 n2)) in
1108           let addr' = vect_of_int ((addr / 8) + 32) `Seven in
1109           let n_bit = set_bit (Byte7Map.find addr' status.low_internal_ram) (addr mod 8) v in
1110             { status with low_internal_ram = Byte7Map.add addr' n_bit status.low_internal_ram }
1111      | (true,r1,r2,r3) ->
1112            let addr = int_of_vect $ mk_byte7 r1 r2 r3 n2 in
1113            let div = addr / 8 in
1114            let rem = addr mod 8 in
1115            let addr' = vect_of_int ((div * 8) + 128) `Eight in
1116            let sfr = get_sfr status addr' true in (* are we reading from the latch here? *)
1117            let sfr' = set_bit sfr rem v in
1118              set_sfr status addr' sfr')
1119    | `C ->
1120       let (n1,n2) = from_byte status.psw in
1121       let (_,b2,b3,b4) = from_nibble n1 in
1122         { status with psw = (mk_byte (mk_nibble v b2 b3 b4) n2) }
1123
1124let set_arg_8 status v =
1125  function
1126  `DIRECT addr ->
1127    let (b1, b2) = from_byte addr in
1128    (match from_nibble b1 with
1129        (false,r1,r2,r3) ->
1130          { status with low_internal_ram =
1131              Byte7Map.add (mk_byte7 r1 r2 r3 b2) v status.low_internal_ram }
1132      | _ -> set_sfr status addr v)
1133    | `INDIRECT b ->
1134      let (b1, b2) = from_byte (get_register status (false,false,b)) in
1135      (match (from_nibble b1, b2) with 
1136          (false,r1,r2,r3),n1 ->
1137            { status with low_internal_ram =
1138                Byte7Map.add (mk_byte7 r1 r2 r3 n1) v status.low_internal_ram }
1139        | (true,r1,r2,r3),n1 ->
1140          { status with high_internal_ram =
1141              Byte7Map.add (mk_byte7 r1 r2 r3 n1) v status.high_internal_ram })
1142    | `REG (b1,b2,b3) ->
1143      set_register status v (b1,b2,b3)
1144    | `A -> { status with acc = v }
1145    | `B -> { status with b = v }
1146    | `EXT_IND_DPTR ->
1147      let dpr = mk_word status.dph status.dpl in
1148      { status with external_ram =
1149          Physical.WordMap.add dpr v status.external_ram }
1150    | `EXT_INDIRECT b ->
1151      let addr = get_register status (false,false,b) in
1152      { status with external_ram =
1153          Physical.WordMap.add (mk_word (zero `Eight) addr) v status.external_ram }
1154;;
1155
1156let set_arg_16 status wrd =
1157  function
1158  `DPTR ->
1159    let (dh, dl) = from_word wrd in
1160    { status with dph = dh; dpl = dl }
1161     
1162let set_flags status c ac ov =
1163  { status with psw =
1164      let bu,bl = from_byte status.psw in
1165      let (_c,oac,fo,rs1),(rs0,_ov,ud,p) = from_nibble bu, from_nibble bl in
1166      let ac = match ac with None -> oac | Some v -> v in
1167      mk_byte (mk_nibble c ac fo rs1) (mk_nibble rs0 ov ud p)
1168  }
1169;;
1170
1171let xor b1 b2 =
1172  if b1 = true && b2 = true then
1173    false
1174  else if b1 = false && b2 = false then
1175    false
1176  else true
1177;;
1178
1179let read_at_sp status =
1180  let n1,n2 = from_byte status.sp in
1181  let m,r1,r2,r3 = from_nibble n1 in
1182  Byte7Map.find (mk_byte7 r1 r2 r3 n2)
1183    (if m then status.low_internal_ram else status.high_internal_ram)
1184;;
1185
1186let write_at_sp status v =
1187  let n1,n2 = from_byte status.sp in
1188  match from_nibble n1 with
1189      true,r1,r2,r3 ->
1190        let memory =
1191          Byte7Map.add (mk_byte7 r1 r2 r3 n2) v status.low_internal_ram
1192        in
1193        { status with low_internal_ram = memory }
1194    | false,r1,r2,r3 ->
1195      let memory =
1196        Byte7Map.add (mk_byte7 r1 r2 r3 n2) v status.high_internal_ram
1197      in
1198      { status with high_internal_ram = memory }
1199;;
1200
1201let timer0 status b1 b2 ticks =
1202  let b = get_bit status.tcon 4 in
1203          (* Timer0 first *)
1204  (match b1,b2 with
1205      true,true ->
1206              (* Archaic 13 bit mode. *)
1207        if b then
1208          let res,_,_,_ = add8_with_c status.tl0 (vect_of_int ticks `Eight) false in
1209          let res = int_of_vect res in
1210          if res > 31 then
1211            let res = res mod 32 in
1212            let res',cy',ov',ac' = add8_with_c status.th0 (vect_of_int 1 `Eight) false in
1213            if ov' then
1214              let b = set_bit status.tcon 7 true in
1215              { status with tcon = b; th0 = res'; tl0 = vect_of_int res `Eight }
1216            else
1217              { status with th0 = res'; tl0 = vect_of_int res `Eight }
1218          else
1219            { status with tl0 = vect_of_int res `Eight }
1220        else
1221          status
1222    | false,false ->
1223              (* 8 bit split timer mode. *)
1224      let status = 
1225        (if b then
1226            let res,cy,ov,ac = add8_with_c status.tl0 (vect_of_int ticks `Eight) false in
1227            if ov then
1228              let b = set_bit status.tcon 5 true in
1229              { status with tcon = b; tl0 = res }
1230            else
1231              { status with tl0 = res }
1232         else
1233            status)
1234      in
1235      if get_bit status.tcon 6 then
1236        let res,cy,ov,ac = add8_with_c status.th0 (vect_of_int ticks `Eight) false in
1237        if ov then
1238          let b = set_bit status.tcon 7 true in
1239          { status with tcon = b; th0 = res }
1240        else
1241          { status with th0 = res }
1242      else
1243        status
1244    | false,true ->
1245             (* 16 bit timer mode. *)
1246      if b then
1247        let res,_,ov,_ = add16_with_c (mk_word status.th0 status.tl0) (vect_of_int ticks `Sixteen) false in
1248                if ov then
1249                  let b = set_bit status.tcon 5 true in
1250                  let new_th0,new_tl0 = from_word res in
1251                  { status with tcon = b; th0 = new_th0; tl0 = new_tl0 }
1252                else
1253                  let new_th0,new_tl0 = from_word res in
1254                  { status with th0 = new_th0; tl0 = new_tl0 }
1255      else
1256        status
1257    | true,false ->
1258              (* 8 bit single timer mode. *)
1259      if b then
1260        let res,_,ov,_ = add8_with_c status.tl0 (vect_of_int ticks `Eight) false in
1261        if ov then
1262          let b = set_bit status.tcon 5 true in
1263          { status with tcon = b; tl0 = status.th0; }
1264        else
1265          { status with tl0 = res }
1266      else
1267        status)
1268   
1269let timer1 status b3 b4 ticks =
1270  let b = get_bit status.tcon 4 in
1271  (match b3,b4 with
1272      true,true ->
1273        (* Archaic 13 bit mode. *)
1274        if b then
1275          let res,_,_,_ = add8_with_c status.tl1 (vect_of_int ticks `Eight) false in
1276          let res = int_of_vect res in
1277          if res > 31 then
1278            let res = res mod 32 in
1279            let res',cy',ov',ac' = add8_with_c status.th1 (vect_of_int 1 `Eight) false in
1280            if ov' then
1281              let b = set_bit status.tcon 7 true in
1282              { status with tcon = b; th1 = res'; tl1 = vect_of_int res `Eight }
1283            else
1284              { status with th1 = res'; tl0 = vect_of_int res `Eight }
1285          else
1286            { status with tl1 = vect_of_int res `Eight }
1287        else
1288          status
1289    | false,false ->
1290              (* 8 bit split timer mode. *)
1291      let status = 
1292        (if b then
1293            let res,cy,ov,ac = add8_with_c status.tl1 (vect_of_int ticks `Eight) false in
1294            if ov then
1295              let b = set_bit status.tcon 5 true in
1296                        { status with tcon = b; tl1 = res }
1297            else
1298              { status with tl1 = res }
1299         else
1300            status)
1301      in
1302      if get_bit status.tcon 6 then
1303        let res,cy,ov,ac = add8_with_c status.th1 (vect_of_int ticks `Eight) false in
1304        if ov then
1305          let b = set_bit status.tcon 7 true in
1306          { status with tcon = b; th1 = res }
1307        else
1308          { status with th1 = res }
1309      else
1310        status
1311    | false,true ->
1312             (* 16 bit timer mode. *)
1313      if b then
1314        let res,_,ov,_ = add16_with_c (mk_word status.th0 status.tl1) (vect_of_int ticks `Sixteen) false in
1315        if ov then
1316          let b = set_bit status.tcon 5 true in
1317          let new_th1,new_tl1 = from_word res in
1318          { status with tcon = b; th1 = new_th1; tl1 = new_tl1 }
1319        else
1320          let new_th1,new_tl1 = from_word res in
1321          { status with th1 = new_th1; tl1 = new_tl1 }
1322      else
1323        status
1324    | true,false ->
1325              (* 8 bit single timer mode. *)
1326      if b then
1327        let res,_,ov,_ = add8_with_c status.tl1 (vect_of_int ticks `Eight) false in
1328        if ov then
1329          let b = set_bit status.tcon 5 true in
1330          { status with tcon = b; tl1 = status.th1; }
1331        else
1332          { status with tl1 = res }
1333      else
1334        status)
1335;;
1336
1337let timers status ticks =
1338  (* DPM: Clock/Timer code follows. *)
1339  match bits_of_byte status.tmod with
1340    | (g1,c1,b1,b2),(g0,c0,b3,b4) ->
1341      let status =
1342        (if g0 then
1343            if get_bit status.p3 2 then
1344              if c0 then
1345                if status.previous_p1_val && not $ get_bit status.p3 4 then
1346                  timer0 status b1 b2 ticks
1347                else
1348                  status
1349              else
1350                timer0 status b1 b2 ticks
1351            else
1352              status
1353         else
1354            timer0 status b1 b2 ticks) in
1355      (* Timer 1 follows. *)
1356      let status =
1357        (if g1 then
1358            if get_bit status.p1 3 then
1359              if c1 then
1360                if status.previous_p3_val && not $ get_bit status.p3 5 then
1361                  timer1 status b3 b4 ticks
1362                else
1363                  status
1364              else
1365                timer1 status b3 b4 ticks
1366            else
1367              status
1368         else
1369            timer1 status b3 b4 ticks) in
1370      (* Timer 2 follows *)
1371      let status =
1372        (let (tf2,exf2,rclk,tclk),(exen2,tr2,ct2,cp2) = bits_of_byte status.t2con in
1373          (* Timer2 is enabled *)
1374         if tr2 then
1375            (* Counter/interval mode *)
1376           if ct2 && not cp2 then
1377             let word = mk_word status.th2 status.tl2 in
1378             let res,_,ov,_ = add16_with_c word (vect_of_int ticks `Sixteen) false in
1379             if ov then
1380               let new_th2 = status.rcap2h in
1381               let new_tl2 = status.rcap2l in
1382                  (* Overflow flag not set if either of the following flags are set *)
1383               if not rclk && not tclk then
1384                 let b = set_bit status.t2con 7 true in
1385                 { status with t2con = b;
1386                   th2 = new_th2;
1387                   tl2 = new_tl2 }
1388               else
1389                 { status with th2 = new_th2;
1390                   tl2 = new_tl2 }
1391             else
1392                (* Reload also signalled when a 1-0 transition is detected *)
1393               if status.previous_p1_val && not $ get_bit status.p1 1 then
1394                  (* In which case signal reload by setting T2CON.6 *)
1395                 let b = set_bit status.t2con 6 true in
1396                 { status with th2 = status.rcap2h;
1397                   tl2 = status.rcap2l;
1398                   t2con = b }
1399               else
1400                 let new_th2, new_tl2 = from_word res in
1401                 { status with th2 = new_th2;
1402                   tl2 = new_tl2 }
1403            (* Capture mode *)
1404           else if cp2 && exen2 then
1405              (* 1-0 transition detected *)
1406              (* DPM: look at this: is the timer still running throughout? *)
1407             if status.previous_p1_val && not $ get_bit status.p1 1 then
1408               status (* Implement clock here *)
1409             else
1410               status (* Implement clock here *)
1411           else
1412             status
1413           else
1414             status) in status
1415                     
1416;;
1417
1418let serial_port_input status in_cont =
1419      (* Serial port input *)
1420  match in_cont with
1421      Some (`In(time, line, epsilon, cont)) when get_bit status.scon 4 ->
1422        (let status =
1423           (match line with
1424               `P1 b ->
1425                 if status.clock >= time then
1426                   { status with p1 = b; p1_latch = b; }
1427                 else
1428                   status
1429             | `P3 b ->
1430               if status.clock >= time then
1431                 { status with p3 = b; p3_latch = b; }
1432               else
1433                 status
1434             | `SerialBuff (`Eight b) ->
1435               let sm0 = get_bit status.scon 7 in
1436               let sm1 = get_bit status.scon 6 in
1437               (match (sm0, sm1) with
1438                   (false, false) ->
1439                       (* Mode 0: shift register.  No delay. *)
1440                     if status.clock >= time then
1441                       { status with scon = set_bit status.scon 0 true;
1442                         io   = cont;
1443                         sbuf = b }
1444                     else
1445                       status
1446                 | (false, true) ->
1447                       (* Mode 1: 8-bit UART *)
1448                       (* Explanation: 8 bit asynchronous communication.  There's a delay (epsilon)
1449                          which needs taking care of.  If we're trying to communicate at the same time
1450                          an existing communication is occurring, we assert false (else clause of first
1451                          if). *)
1452                   if status.serial_epsilon_in = None && status.serial_v_in = None then
1453                     if status.clock >= time then
1454                           (* Waiting for nine bits, multiprocessor communication mode requires nine bits *)
1455                       if get_bit status.scon 5 then
1456                         assert false (* really: crash! *)
1457                       else
1458                         { status with serial_epsilon_in = Some (epsilon + time);
1459                           serial_v_in       = Some (`Eight b) }
1460                     else
1461                           (* Warning about incomplete case analysis here, but safe as we've already tested for
1462                              None. *)
1463                       let Some e = status.serial_epsilon_in in
1464                       let Some v = status.serial_v_in in
1465                       if status.clock >= e then
1466                         match v with
1467                             `Eight v' ->
1468                               { status with sbuf = v';
1469                                 serial_v_in = None;
1470                                 serial_epsilon_in = None;
1471                                 scon = set_bit status.scon 0 true;
1472                                 io = cont }
1473                           | _ -> assert false (* trying to read in 9 bits instead of 8 *)
1474                       else
1475                         status
1476                   else
1477                     assert false
1478                 | (true, false) | (true, true) ->
1479                   assert false (* only got eight bits on the line when in 9 bit mode *))
1480             | `SerialBuff (`Nine (b,b')) ->
1481               let sm0 = get_bit status.scon 7 in
1482               let sm1 = get_bit status.scon 6 in
1483               match(sm0, sm1) with
1484                   (false, false) | (false, true) -> assert false
1485                 | (true, false)  | (true, true) ->
1486                       (* Modes 2 and 3: 9-bit UART *)
1487                       (* Explanation: 9 bit asynchronous communication.  There's a delay (epsilon)
1488                          which needs taking care of.  If we're trying to communicate at the same time
1489                          an existing communication is occurring, we assert false (else claus of first
1490                          if). *)
1491                   if status.serial_epsilon_in = None && status.serial_v_in = None then
1492                     if status.clock >= time then
1493                           (* waiting for nine bits, multiprocessor communication mode requires nine bits *)
1494                       if get_bit status.scon 5 then
1495                         assert false (* really: crash! *)
1496                       else
1497                         { status with serial_epsilon_in = Some (epsilon + time);
1498                           serial_v_in       = Some (`Nine (b, b')) }
1499                     else
1500                           (* Warning about incomplete case analysis here, but safe as we've already tested for
1501                              None. *)
1502                       let Some e = status.serial_epsilon_in in
1503                       let Some v = status.serial_v_in in
1504                       if status.clock >= e then
1505                         match v with
1506                             `Nine (v, v') ->
1507                               let scon' = set_bit status.scon 0 true in
1508                               { status with sbuf = v';
1509                                 serial_v_in = None;
1510                                 serial_epsilon_in = None;
1511                                 scon = set_bit scon' 2 b;
1512                                 io = cont }
1513                           | _ -> assert false (* trying to read in 8 bits instead of 9 *)
1514                       else
1515                         status
1516                   else
1517                     assert false)
1518         in
1519         { status with io = cont })
1520    | _ -> status
1521;;
1522
1523let serial_port_output status out_cont =
1524  (* Serial port output *)
1525  (let status = { status with serial_epsilon_out = Some (status.clock + status.io_epsilon);
1526    serial_v_out = Some (`Eight status.sbuf);
1527    serial_k_out = Some (snd (out_cont (status.clock + status.io_epsilon) (`SerialBuff (`Eight status.sbuf)))) } in
1528   match status.serial_epsilon_out with
1529       Some s ->
1530         if status.clock >= s then
1531           match status.serial_k_out with
1532               None -> assert false (* correct? *)
1533             | Some k' -> { status with io   = k';
1534               scon = set_bit status.scon 1 true; }
1535         else
1536           status
1537     | _ -> assert false)
1538;;
1539
1540let external_serial_interrupt status esi =
1541  (* Interrupt enabled *)
1542  if esi then
1543    (* If we're already running, then fine (todo: check for *another* interrupt
1544       and add to a queue, or something? *)
1545    if status.t1i_running then
1546      status
1547    else
1548      (* If we should be running, but aren't... *)
1549      if false then
1550        assert false
1551      else
1552        status
1553  else
1554    status
1555;;
1556
1557let external0_interrupt status e0i =
1558  (* Interrupt enabled *)
1559  if e0i then
1560    (* If we're already running, then fine (todo: check for *another* interrupt
1561       and add to a queue, or something? *)
1562    if status.t1i_running then
1563      status
1564    else
1565      (* If we should be running, but aren't... *)
1566      if false then
1567        assert false
1568      else
1569        status
1570  else
1571    status
1572;;
1573
1574let external1_interrupt status e1i =
1575  (* Interrupt enabled *)
1576  if e1i then
1577    (* If we're already running, then fine (todo: check for *another* interrupt
1578       and add to a queue, or something? *)
1579    if status.t1i_running then
1580      status
1581    else
1582      (* If we should be running, but aren't... *)
1583      if false then
1584        assert false
1585      else
1586        status
1587  else
1588    status
1589;;
1590
1591let timer0_interrupt status t0i =
1592  (* Interrupt enabled *)
1593  if t0i then
1594    (* If we're already running, then fine (todo: check for *another* interrupt
1595       and add to a queue, or something? *)
1596    if status.t1i_running then
1597      status
1598    else
1599      (* If we should be running, but aren't... *)
1600      if false then
1601        assert false
1602      else
1603        status
1604  else
1605    status
1606;;
1607
1608let timer1_interrupt status t1i =
1609  (* Interrupt enabled *)
1610  if t1i then
1611    (* If we're already running, then fine (todo: check for *another* interrupt
1612       and add to a queue, or something? *)
1613    if status.t1i_running then
1614      status
1615    else
1616      (* If we should be running, but aren't... *)
1617      if false then
1618        assert false
1619      else
1620        status
1621  else
1622    status
1623;;
1624
1625let interrupts status =
1626  let (ea,_,_,es), (et1,ex1,et0,ex0) = bits_of_byte status.ie in
1627  let (_,_,_,ps), (pt1,px1,pt0,px0) = bits_of_byte status.ip in
1628    (* DPM: are interrupts enabled? *)
1629  if ea then
1630    match (ps,pt1,px1,pt0,px0) with
1631        _ -> assert false
1632  else
1633    status
1634;;
1635
1636let execute1 status =
1637  let instr,pc,ticks = fetch status.code_memory status.pc in
1638  let status = { status with clock = status.clock + ticks; pc = pc } in
1639  let status =
1640    (match instr with
1641        `ADD (`A,d1) ->
1642          let v,c,ac,ov =
1643            add8_with_c (get_arg_8 status false `A) (get_arg_8 status false d1) false
1644          in
1645          set_flags (set_arg_8 status v `A) c (Some ac) ov
1646      | `ADDC (`A,d1) ->
1647        let v,c,ac,ov =
1648          add8_with_c (get_arg_8 status false `A) (get_arg_8 status false d1) (get_cy_flag status)
1649        in
1650        set_flags (set_arg_8 status v `A) c (Some ac) ov
1651      | `SUBB (`A,d1) ->
1652        let v,c,ac,ov =
1653          subb8_with_c (get_arg_8 status false `A) (get_arg_8 status false d1) (get_cy_flag status)
1654        in
1655        set_flags (set_arg_8 status v `A) c (Some ac) ov
1656      | `INC `DPTR ->
1657        let cry, low_order_byte = half_add status.dpl (vect_of_int 1 `Eight) in
1658        let cry, high_order_byte = full_add status.dph (vect_of_int 0 `Eight) cry in
1659        { status with dpl = low_order_byte; dph = high_order_byte }
1660      | `INC ((`A | `REG _ | `DIRECT _ | `INDIRECT _) as d) ->
1661        let b = get_arg_8 status true d in
1662        let cry, res = half_add b (vect_of_int 1 `Eight) in
1663        set_arg_8 status res d
1664      | `DEC d ->
1665        let b = get_arg_8 status true d in
1666        let res,c,ac,ov = subb8_with_c b (vect_of_int 1 `Eight) false in
1667        set_arg_8 status res d
1668      | `MUL (`A,`B) ->
1669        let acc = int_of_vect status.acc in
1670        let b = int_of_vect status.b in
1671        let prod = acc * b in
1672        let ov = prod > 255 in
1673        let l = vect_of_int (prod  mod 256) `Eight in
1674        let h = vect_of_int (prod / 256) `Eight in
1675        let status = { status with acc = l ; b = h } in
1676         (* DPM: Carry flag is always cleared. *)
1677        set_flags status false None ov
1678      | `DIV (`A,`B) ->
1679        let acc = int_of_vect status.acc in
1680        let b = int_of_vect status.b in
1681        if b = 0 then
1682        (* CSC: ACC and B undefined! We leave them as they are. *)
1683          set_flags status false None true
1684        else
1685          let q = vect_of_int (acc / b) `Eight in
1686          let r = vect_of_int (acc mod b) `Eight in
1687          let status = { status with acc = q ; b = r } in
1688          set_flags status false None false
1689      | `DA `A ->
1690        let acc_upper_nibble, acc_lower_nibble = from_byte status.acc in
1691        if int_of_vect acc_lower_nibble > 9 or get_ac_flag status = true then
1692          let acc,cy,_,_ = add8_with_c status.acc (vect_of_int 6 `Eight) false in
1693          let acc_upper_nibble, acc_lower_nibble = from_byte acc in
1694          if int_of_vect acc_upper_nibble > 9 or cy = true then
1695            let cry,acc_upper_nibble = half_add acc_upper_nibble (vect_of_int 6 `Four) in
1696            let status = { status with acc = mk_byte acc_upper_nibble acc_lower_nibble } in
1697            set_flags status cry (Some (get_ac_flag status)) (get_ov_flag status)
1698          else
1699            status
1700        else
1701          status
1702      | `ANL (`U1(`A, ag)) ->
1703        let and_val = get_arg_8 status true `A -&- get_arg_8 status true ag in
1704        set_arg_8 status and_val `A
1705      | `ANL (`U2((`DIRECT d), ag)) ->
1706        let and_val = get_arg_8 status true (`DIRECT d) -&- get_arg_8 status true ag in
1707        set_arg_8 status and_val (`DIRECT d)
1708      | `ANL (`U3 (`C, b)) ->
1709        let and_val = get_cy_flag status && get_arg_1 status true b in
1710        set_flags status and_val None (get_ov_flag status)
1711      | `ORL (`U1(`A, ag)) ->
1712        let or_val = get_arg_8 status true `A -|- get_arg_8 status true ag in
1713        set_arg_8 status or_val `A
1714      | `ORL (`U2((`DIRECT d), ag)) ->
1715        let or_val = get_arg_8 status true (`DIRECT d) -|- get_arg_8 status true ag in
1716        set_arg_8 status or_val (`DIRECT d)
1717      | `ORL (`U3 (`C, b)) ->
1718        let or_val = get_cy_flag status || get_arg_1 status true b in
1719        set_flags status or_val None (get_ov_flag status)
1720      | `XRL (`U1(`A, ag)) ->
1721        let xor_val = get_arg_8 status true `A -^- get_arg_8 status true ag in
1722        set_arg_8 status xor_val `A
1723      | `XRL (`U2((`DIRECT d), ag)) ->
1724        let xor_val = get_arg_8 status true (`DIRECT d) -^- get_arg_8 status true ag in
1725        set_arg_8 status xor_val (`DIRECT d)
1726      | `CLR `A -> set_arg_8 status (zero `Eight) `A
1727      | `CLR `C -> set_arg_1 status false `C
1728      | `CLR ((`BIT _) as a) -> set_arg_1 status false a
1729      | `CPL `A -> { status with acc = complement status.acc }
1730      | `CPL `C -> set_arg_1 status (not $ get_arg_1 status true `C) `C
1731      | `CPL ((`BIT _) as b) -> set_arg_1 status (not $ get_arg_1 status true b) b
1732      | `RL `A -> { status with acc = rotate_left status.acc }
1733      | `RLC `A ->
1734        let old_cy = get_cy_flag status in
1735        let n1, n2 = from_byte status.acc in
1736        let (b1,b2,b3,b4),(b5,b6,b7,b8) = from_nibble n1, from_nibble n2 in
1737        let status = set_arg_1 status b1 `C in
1738        { status with acc = mk_byte (mk_nibble b2 b3 b4 b5) (mk_nibble b6 b7 b8 old_cy) }
1739      | `RR `A -> { status with acc = rotate_right status.acc }
1740      | `RRC `A ->
1741        let old_cy = get_cy_flag status in
1742        let n1, n2 = from_byte status.acc in
1743        let (b1,b2,b3,b4),(b5,b6,b7,b8) = from_nibble n1, from_nibble n2 in
1744        let status = set_arg_1 status b8 `C in
1745        { status with acc = mk_byte (mk_nibble old_cy b1 b2 b3) (mk_nibble b4 b5 b6 b7) }
1746      | `SWAP `A ->
1747        let (acc_nibble_upper, acc_nibble_lower) = from_byte status.acc in
1748        { status with acc = mk_byte acc_nibble_lower acc_nibble_upper }
1749      | `MOV(`U1(b1, b2)) -> set_arg_8 status (get_arg_8 status false b2) b1
1750      | `MOV(`U2(b1, b2)) -> set_arg_8 status (get_arg_8 status false b2) b1
1751      | `MOV(`U3(b1, b2)) -> set_arg_8 status (get_arg_8 status false b2) b1
1752      | `MOV(`U4(b1,b2)) -> set_arg_16 status (get_arg_16 status b2) b1
1753      | `MOV(`U5(b1,b2)) -> set_arg_1 status (get_arg_1 status false b2) b1
1754      | `MOV(`U6(b1,b2)) -> set_arg_1 status (get_arg_1 status false b2) b1
1755      | `MOVC (`A, `A_DPTR) ->
1756        let big_acc = mk_word (zero `Eight) status.acc in
1757        let dptr = mk_word status.dph status.dpl in
1758        let cry, addr = half_add dptr big_acc in
1759        let lookup = Physical.WordMap.find addr status.code_memory in
1760        { status with acc = lookup }
1761      | `MOVC (`A, `A_PC) ->
1762        let big_acc = mk_word (zero `Eight) status.acc in
1763        (* DPM: Under specified: does the carry from PC incrementation affect the *)
1764        (*      addition of the PC with the DPTR? At the moment, no.              *)
1765        let cry,inc_pc = half_add status.pc (vect_of_int 1 `Sixteen) in
1766        let status = { status with pc = inc_pc } in
1767        let cry,addr = half_add inc_pc big_acc in
1768        let lookup = Physical.WordMap.find addr status.code_memory in
1769        { status with acc = lookup }
1770      (* data transfer *)
1771      (* DPM: MOVX currently only implements the *copying* of data! *)
1772      | `MOVX (`U1 (a1, a2)) -> set_arg_8 status (get_arg_8 status false a2) a1
1773      | `MOVX (`U2 (a1, a2)) -> set_arg_8 status (get_arg_8 status false a2) a1
1774      | `SETB b -> set_arg_1 status true b
1775      | `PUSH a ->
1776       (* DPM: What happens if we overflow? *)
1777        let cry,new_sp = half_add status.sp (vect_of_int 1 `Eight) in
1778        let status = { status with sp = new_sp } in
1779        write_at_sp status (get_arg_8 status false a)
1780      | `POP (`DIRECT b) ->
1781        let contents = read_at_sp status in
1782        let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in
1783        let status = { status with sp = new_sp } in
1784        let status = set_arg_8 status contents (`DIRECT b) in
1785        status
1786      | `XCH(`A, arg) ->
1787        let old_arg = get_arg_8 status false arg in
1788        let old_acc = status.acc in
1789        let status = set_arg_8 status old_acc arg in
1790        { status with acc = old_arg }
1791      | `XCHD(`A, i) ->
1792        let acc_upper_nibble, acc_lower_nibble = from_byte $ get_arg_8 status false `A in
1793        let ind_upper_nibble, ind_lower_nibble = from_byte $ get_arg_8 status false i in
1794        let new_acc = mk_byte acc_upper_nibble ind_lower_nibble in
1795        let new_reg = mk_byte ind_upper_nibble acc_lower_nibble in
1796        let status = { status with acc = new_acc } in
1797        set_arg_8 status new_reg i
1798      (* program branching *)
1799      | `JC (`REL rel) ->
1800        if get_cy_flag status then
1801          let cry, new_pc = half_add status.pc (sign_extension rel) in
1802          { status with pc = new_pc }
1803        else
1804          status
1805      | `JNC (`REL rel) ->
1806        if not $ get_cy_flag status then
1807          let cry, new_pc = half_add status.pc (sign_extension rel) in
1808          { status with pc = new_pc }
1809        else
1810          status
1811      | `JB (b, (`REL rel)) ->
1812        if get_arg_1 status false b then
1813          let cry, new_pc = half_add status.pc (sign_extension rel) in
1814          { status with pc = new_pc }
1815        else
1816          status
1817      | `JNB (b, (`REL rel)) ->
1818        if not $ get_arg_1 status false b then
1819          let cry, new_pc = half_add status.pc (sign_extension rel) in
1820          { status with pc = new_pc }
1821        else
1822          status
1823      | `JBC (b, (`REL rel)) ->
1824        let status = set_arg_1 status false b in
1825        if get_arg_1 status false b then
1826          let cry, new_pc = half_add status.pc (sign_extension rel) in
1827          { status with pc = new_pc }
1828        else
1829          status
1830      | `RET ->
1831        (* DPM: What happens when we underflow? *)
1832        let high_bits = read_at_sp status in
1833        let new_sp,cy,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in
1834        let status = { status with sp = new_sp } in
1835        let low_bits = read_at_sp status in
1836        let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) cy in
1837        let status = { status with sp = new_sp } in
1838        { status with pc = mk_word high_bits low_bits }
1839      | `RETI ->
1840        let high_bits = read_at_sp status in
1841        let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in
1842        let status = { status with sp = new_sp } in
1843        let low_bits = read_at_sp status in
1844        let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in
1845        let status = { status with sp = new_sp } in
1846        { status with pc = mk_word high_bits low_bits }
1847      | `ACALL (`ADDR11 a) ->
1848        let cry, new_sp = half_add status.sp (vect_of_int 1 `Eight) in
1849        let status = { status with sp = new_sp } in
1850        let pc_upper_byte, pc_lower_byte = from_word status.pc in
1851        let status = write_at_sp status pc_lower_byte in
1852        let cry, new_sp = half_add status.sp (vect_of_int 1 `Eight) in
1853        let status = { status with sp = new_sp } in
1854        let status = write_at_sp status pc_upper_byte in
1855        let addr = addr16_of_addr11 status.pc a in
1856        { status with pc = addr }
1857      | `LCALL (`ADDR16 addr) ->
1858        let cry, new_sp = half_add status.sp (vect_of_int 1 `Eight) in
1859        let status = { status with sp = new_sp } in
1860        let pc_upper_byte, pc_lower_byte = from_word status.pc in
1861        let status = write_at_sp status pc_lower_byte in
1862        let cry, new_sp = half_add status.sp (vect_of_int 1 `Eight) in
1863        let status = { status with sp = new_sp } in
1864        let status = write_at_sp status pc_upper_byte in
1865        { status with pc = addr }
1866      | `AJMP (`ADDR11 a) ->
1867        let addr = addr16_of_addr11 status.pc a in
1868        { status with pc = addr }
1869      | `LJMP (`ADDR16 a) ->
1870        { status with pc = a }
1871      | `SJMP (`REL rel) ->
1872        let cry, new_pc = half_add status.pc (sign_extension rel) in
1873        { status with pc = new_pc }
1874      | `JMP `IND_DPTR ->
1875        let dptr = mk_word status.dph status.dpl in
1876        let big_acc = mk_word (zero `Eight) status.acc in
1877        let cry, jmp_addr = half_add big_acc dptr in
1878        let cry, new_pc = half_add status.pc jmp_addr in
1879        { status with pc = new_pc }
1880      | `JZ (`REL rel) ->
1881        if status.acc = zero `Eight then
1882          let cry, new_pc = half_add status.pc (sign_extension rel) in
1883          { status with pc = new_pc }
1884        else
1885          status
1886      | `JNZ (`REL rel) ->
1887        if status.acc <> zero `Eight then
1888          let cry, new_pc = half_add status.pc (sign_extension rel) in
1889          { status with pc = new_pc }
1890        else
1891          status
1892      | `CJNE ((`U1 (`A, ag)), `REL rel) ->
1893        let new_carry = status.acc < get_arg_8 status false ag in
1894        if get_arg_8 status false ag <> status.acc then
1895          let cry, new_pc = half_add status.pc (sign_extension rel) in
1896          let status = set_flags status new_carry None (get_ov_flag status) in
1897          { status with pc = new_pc;  }
1898        else
1899          set_flags status new_carry None (get_ov_flag status)
1900      | `CJNE ((`U2 (ag, `DATA d)), `REL rel) ->
1901        let new_carry = get_arg_8 status false ag < d in
1902        if get_arg_8 status false ag <> d then
1903          let cry, new_pc = half_add status.pc (sign_extension rel) in
1904          let status = { status with pc = new_pc } in
1905          set_flags status new_carry None (get_ov_flag status)
1906        else
1907          set_flags status new_carry None (get_ov_flag status)
1908      | `DJNZ (ag, (`REL rel)) ->
1909        let new_ag,_,_,_ = subb8_with_c (get_arg_8 status true ag) (vect_of_int 1 `Eight) false in
1910        let status = set_arg_8 status new_ag ag in
1911        if new_ag <> zero `Eight then
1912          let cry, new_pc = half_add status.pc (sign_extension rel) in
1913          { status with pc = new_pc }
1914        else
1915          status
1916      | `NOP -> status) in
1917  let status = timers status ticks in
1918  let in_cont, `Out out_cont = status.io in
1919  let status = serial_port_input status in_cont in
1920  let status = serial_port_output status out_cont in
1921  let status = interrupts status in
1922  { status with previous_p1_val = get_bit status.p3 4;
1923    previous_p3_val = get_bit status.p3 5 }
1924;;
1925
1926(*
1927OLD output routine:
1928           (* Serial port output, part one *)
1929           let status =
1930             (match status.expected_out_time with
1931               `At t when status.clock >= t ->
1932                 { status with scon = set_bit status.scon 1 true; expected_out_time = `None }
1933              | _ -> status) in
1934
1935             (if status.expected_out_time = `Now then
1936               if get_bit status.scon 7 then
1937                 let exp_time, new_cont = out_cont status.clock (`SerialBuff (`Nine ((get_bit status.scon 3), status.sbuf))) in
1938                   { status with expected_out_time = `At exp_time; io = new_cont }
1939               else
1940                 let exp_time, new_cont = out_cont status.clock (`SerialBuff (`Eight status.sbuf)) in
1941                   { status with expected_out_time = `At exp_time; io = new_cont }               
1942             else
1943               status) in
1944*)
1945
1946let rec execute f s =
1947  let cont =
1948    try f s; true
1949    with Halt -> false
1950  in
1951  if cont then execute f (execute1 s)
1952  else s
1953;;
1954
1955
1956let load_program p =
1957  let st = load p.ASM.code initialize in
1958  { st with exit_addr = p.ASM.exit_addr ; cost_labels = p.ASM.cost_labels }
1959
1960let observe_trace trace_ref st =
1961  let cost_label =
1962    if BitVectors.WordMap.mem st.pc st.cost_labels then
1963      [BitVectors.WordMap.find st.pc st.cost_labels]
1964    else [] in
1965  trace_ref := cost_label @ !trace_ref ;
1966  if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st
1967
1968let result st =
1969  let i = BitVectors.int_of_vect st.dpl in
1970  IntValue.Int8.of_int i
1971
1972let interpret print_result p =
1973  if p.ASM.has_main then
1974    let st = load_program p in
1975    let trace = ref [] in
1976    let callback = observe_trace trace in
1977    let st = execute callback st in
1978    let res = result st in
1979    if print_result then
1980      Printf.printf "8051: %s\n%!" (IntValue.Int8.to_string res) ;
1981    (res, List.rev !trace)
1982  else (IntValue.Int8.zero, [])
Note: See TracBrowser for help on using the repository browser.