source: Deliverables/D4.1/Matita/Test.ma @ 664

Last change on this file since 664 was 664, checked in by mulligan, 9 years ago

Changed output of Intel HEX files so we no longer have those gargantuan blocks of zeroes at the end.

File size: 11.4 KB
Line 
1include "List.ma".
2include "ASM.ma".
3
4ndefinition test: List instruction ≝
5 [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]);
6  LCALL … (ADDR16 [[false;false;false;false;false;false;false;true;false;false;false;false;true;false;false;false]]);
7  SJMP … (RELATIVE [[true;true;true;true;true;true;true;false]]);
8  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;true;false;false;false;true]])〉))));
9  LCALL … (ADDR16 [[false;false;false;false;false;false;false;true;true;false;true;false;true;true;true;false]]);
10  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
11  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]]));
12  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
13  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
14  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
15  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
16  Jump … (JZ … (RELATIVE [[false;false;false;true;true;false;true;true]]));
17  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
18  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;true;true;false;true;true;false;false;true;false]])〉)));
19  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
20  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
21  CLR … (ACC_A);
22  MOVC … (ACC_A) (ACC_DPTR);
23  MOVX … (Right … 〈(EXT_INDIRECT false),(ACC_A)〉);
24  INC … (DPTR);
25  INC … (REGISTER [[false;false;false]]);
26  Jump … (CJNE … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;false]]));
27  INC … (DIRECT [[true;false;true;false;false;false;false;false]]);
28  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]]));
29  Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;true;true;false;false;true;false]]));
30  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
31  CLR … (ACC_A);
32  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
33  MOV … (Left … (Left … (Left … (Left … (Right … 〈(INDIRECT false),(ACC_A)〉)))));
34  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;true]]));
35  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
36  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
37  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
38  Jump … (JZ … (RELATIVE [[false;false;false;false;true;false;true;false]]));
39  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
40  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
41  CLR … (ACC_A);
42  MOVX … (Right … 〈(EXT_INDIRECT true),(ACC_A)〉);
43  INC … (REGISTER [[false;false;true]]);
44  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
45  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
46  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
47  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
48  Jump … (JZ … (RELATIVE [[false;false;false;false;true;true;false;false]]));
49  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
50  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
51  CLR … (ACC_A);
52  MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
53  INC … (DPTR);
54  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
55  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]]));
56  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
57  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
58  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;true]]),(DIRECT [[true;false;false;false;false;false;true;true]])〉)))));
59  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;false;false]]),(DIRECT [[true;true;true;true;false;false;false;false]])〉)))));
60  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
61  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;false]])〉)))));
62  DEC … (ACC_A);
63  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;true;false;true;false]]),(ACC_A)〉))));
64  CLR … (CARRY);
65  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;false]])〉)))));
66  XRL … (Left … 〈(ACC_A),(DATA [[true;false;false;false;false;false;false;false]])〉);
67  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(REGISTER [[true;false;true]])〉))));
68  XRL … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(DATA [[true;false;false;false;false;false;false;false]])〉);
69  SUBB … (ACC_A) (DIRECT [[true;true;true;true;false;false;false;false]]);
70  Jump … (JNC … (RELATIVE [[false;false;false;false;false;false;true;true]]));
71  LJMP … (ADDR16 [[false;false;false;false;false;false;false;true;false;false;false;false;false;true;false;false]]);
72  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;true;false]])〉)))));
73  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;true;true]]),(ACC_A)〉)))));
74  RLC … (ACC_A);
75  SUBB … (ACC_A) (DIRECT [[true;true;true;false;false;false;false;false]]);
76  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(ACC_A)〉)))));
77  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[true;false;true]])〉)))));
78  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(ACC_A)〉)))));
79  RLC … (ACC_A);
80  SUBB … (ACC_A) (DIRECT [[true;true;true;false;false;false;false;false]]);
81  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;true;false]]),(ACC_A)〉)))));
82  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
83  ADD … (ACC_A) (REGISTER [[true;true;true]]);
84  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(ACC_A)〉))));
85  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[true;true;false]])〉)))));
86  ADDC … (ACC_A) (REGISTER [[false;false;false]]);
87  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(ACC_A)〉))));
88  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;true;false;false;false;false]]),(DATA [[false;false;false;false;false;false;true;false]])〉))));
89  CLR … (ACC_A);
90  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;true;false;false;false;true]]),(ACC_A)〉))));
91  PUSH … (DIRECT [[false;false;false;false;false;false;true;false]]);
92  PUSH … (DIRECT [[false;false;false;false;false;false;true;true]]);
93  PUSH … (DIRECT [[false;false;false;false;false;true;false;false]]);
94  PUSH … (DIRECT [[false;false;false;false;false;true;false;true]]);
95  LCALL … (ADDR16 [[false;false;false;false;false;false;false;true;false;true;true;true;false;true;true;false]]);
96  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;true;false]]),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
97  POP … (DIRECT [[false;false;false;false;false;true;false;true]]);
98  POP … (DIRECT [[false;false;false;false;false;true;false;false]]);
99  POP … (DIRECT [[false;false;false;false;false;false;true;true]]);
100  POP … (DIRECT [[false;false;false;false;false;false;true;false]]);
101  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[true;true;false]])〉)))));
102  ADD … (ACC_A) (REGISTER [[false;true;false]]);
103  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;true;true]]),(ACC_A)〉)))));
104  CLR … (ACC_A);
105  ADDC … (ACC_A) (REGISTER [[false;true;true]]);
106  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(ACC_A)〉)))));
107  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;false;false;true]]),(REGISTER [[true;false;false]])〉))));
108  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(REGISTER [[true;true;true]])〉))));
109  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;true]]),(REGISTER [[false;false;false]])〉))));
110  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;true;true;true;false;false;false;false]]),(REGISTER [[false;false;true]])〉))));
111  LCALL … (ADDR16 [[false;false;false;false;false;false;false;true;false;true;false;true;true;false;true;false]]);
112  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[true;true;true]]),(ACC_A)〉)))));
113  Jump … (CJNE … (Left … 〈(ACC_A),(DIRECT [[false;false;false;false;true;false;false;true]])〉) (RELATIVE [[false;false;false;false;false;false;true;true]]));
114  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(REGISTER [[true;true;false]])〉))))].
115 @.
116nqed.
Note: See TracBrowser for help on using the repository browser.