Ignore:
Timestamp:
Mar 10, 2011, 11:48:33 AM (9 years ago)
Author:
mulligan
Message:

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

File:
1 edited

Legend:

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

    r465 r664  
     1include "List.ma".
    12include "ASM.ma".
    23
    3 ndefinition test: list instruction ≝
     4ndefinition test: List instruction ≝
    45 [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]);
    5   LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;false;true;false;false]]);
     6  LCALL … (ADDR16 [[false;false;false;false;false;false;false;true;false;false;false;false;true;false;false;false]]);
    67  SJMP … (RELATIVE [[true;true;true;true;true;true;true;false]]);
    7   MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉))));
    8   LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;true;true;true;false]]);
    9   MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;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]])〉)))));
    1011  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]]));
    1112  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
    12   MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    13   MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
    14   ORL … (inl … (inl … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
     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]])〉));
    1516  Jump … (JZ … (RELATIVE [[false;false;false;true;true;false;true;true]]));
    16   MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    17   MOV … (inl … (inl … (inr … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉)));
    18   MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    19   MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     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]])〉))));
    2021  CLR … (ACC_A);
    2122  MOVC … (ACC_A) (ACC_DPTR);
    22   MOVX … (inr … 〈(EXT_INDIRECT false),(ACC_A)〉);
     23  MOVX … (Right … 〈(EXT_INDIRECT false),(ACC_A)〉);
    2324  INC … (DPTR);
    2425  INC … (REGISTER [[false;false;false]]);
    25   Jump … (CJNE … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;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]]));
    2627  INC … (DIRECT [[true;false;true;false;false;false;false;false]]);
    2728  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]]));
    2829  Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;true;true;false;false;true;false]]));
    29   MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
     30  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
    3031  CLR … (ACC_A);
    31   MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
    32   MOV … (inl … (inl … (inl … (inl … (inr … 〈(INDIRECT false),(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)〉)))));
    3334  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;true]]));
    34   MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    35   MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
    36   ORL … (inl … (inl … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
     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]])〉));
    3738  Jump … (JZ … (RELATIVE [[false;false;false;false;true;false;true;false]]));
    38   MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    39   MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;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]])〉))));
    4041  CLR … (ACC_A);
    41   MOVX … (inr … 〈(EXT_INDIRECT true),(ACC_A)〉);
     42  MOVX … (Right … 〈(EXT_INDIRECT true),(ACC_A)〉);
    4243  INC … (REGISTER [[false;false;true]]);
    4344  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
    44   MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    45   MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
    46   ORL … (inl … (inl … 〈(ACC_A),(DATA [[false;false;false;false;false;false;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]])〉));
    4748  Jump … (JZ … (RELATIVE [[false;false;false;false;true;true;false;false]]));
    48   MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    49   MOV … (inl … (inl … (inr … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;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]])〉)));
    5051  CLR … (ACC_A);
    51   MOVX … (inr … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
     52  MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
    5253  INC … (DPTR);
    5354  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
    5455  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]]));
    5556  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
    56   MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉)))));
    57   MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉))));
    58   XCHD … (ACC_A) (INDIRECT false);
    59   MOV … (inl … (inl … (inr … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
    60   RET … ;
    61   MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
    62   RET … ;
    63   NOP … ;
    64   NOP … ;
    65   NOP … ;
    66   NOP … ;
    67   NOP … ;
    68   NOP … ;
    69   NOP … ;
    70   NOP … ;
    71   NOP … ;
    72   NOP … ;
    73   NOP … ;
    74   NOP … ;
    75   NOP … ;
    76   NOP … ;
    77   NOP … ;
    78   NOP … ;
    79   NOP … ;
    80   NOP … ;
    81   NOP … ;
    82   NOP … ;
    83   NOP … ;
    84   NOP … ;
    85   NOP … ;
    86   NOP … ;
    87   NOP … ;
    88   NOP … ;
    89   NOP … ;
    90   NOP … ;
    91   NOP … ;
    92   NOP … ;
    93   NOP … ;
    94   NOP … ;
    95   NOP … ;
    96   NOP … ;
    97   NOP … ;
    98   NOP … ;
    99   NOP … ;
    100   NOP … ;
    101   NOP … ;
    102   NOP … ;
    103   NOP … ;
    104   NOP … ;
    105   NOP … ;
    106   NOP … ;
    107   NOP … ;
    108   NOP … ;
    109   NOP … ;
    110   NOP … ;
    111   NOP … ;
    112   NOP … ;
    113   NOP … ;
    114   NOP … ;
    115   NOP … ;
    116   NOP … ;
    117   NOP … ;
    118   NOP … ;
    119   NOP … ;
    120   NOP … ;
    121   NOP … ;
    122   NOP … ;
    123   NOP … ;
    124   NOP … ;
    125   NOP … ;
    126   NOP … ;
    127   NOP … ;
    128   NOP … ;
    129   NOP … ;
    130   NOP … ;
    131   NOP … ;
    132   NOP … ;
    133   NOP … ;
    134   NOP … ;
    135   NOP … ;
    136   NOP … ;
    137   NOP … ;
    138   NOP … ;
    139   NOP … ;
    140   NOP … ;
    141   NOP … ;
    142   NOP … ;
    143   NOP … ;
    144   NOP … ;
    145   NOP … ;
    146   NOP … ;
    147   NOP … ;
    148   NOP … ;
    149   NOP … ].
     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]])〉))))].
    150115 @.
    151116nqed.
Note: See TracChangeset for help on using the changeset viewer.