Abstracts Communications and the Arts

Application of Formal Verification Techniques

by Andreas Karlsson

Today there are electrical circuits everywhere, e.g. telephones, TVs, cars and computers. The big problem with the rapidly-growing complexity in today's machines is, however, that since they are so complex it is impossible to check all combinations of events before the products are sent to the market. This lack of testing can lead to defective products. There are two well-known examples: Intel’s Pentium-processor, which failed on complex mathematical problems, and the European spaceprogram’s Ariane-rocket that exploded after take-off due to an error in an electrical circuit. For a long time simulation was the only way to verify a design’s behaviour. But simulation cannot check all possible cases within reasonable time for larger circuits. Therefore, the existence of software that performs equivalence checking between two circuits or between a circuit and its specification is justified. This software typically uses some kind of tree structure, e.g. binary decision diagram. Since this market is still rather young the best solution has not yet been found. There are two goals of this diploma work. The first is to find a new structure that uses less time than binary decision diagrams and is able to verify multipliers, which is impossible with binary decision diagrams. The second goal is to provide the results for the user in a manageable way without any unnecessary expressions, and make it possible for the user to influence the expression by setting variables to zero or one.