Inlämning av Examensarbete / Submission of Thesis

Andreas Karlsson; Fredrik Thelandersson , pp. 71. Inst för telekommunikation och signalbehandling/Dept. of Telecommunications and Signal Processing, 1999.

The work

Författare / Author: Andreas Karlsson, Fredrik Thelandersson
ets99akr@student.hk-r.se, ets99fth@student.hk-r.se
Titel / Title: Application of Formal Verification Techniques
Översatt titel / Translated title: Applikation för formell verifikation
Abstrakt Abstract:

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.

Populärvetenskaplig beskrivning / Popular science summary: Det finns elektronik överallt i vår vardag, i allt ifrån telefoner och tv-apparater till bilar och datorer. Problemet med dessa allt mer avancerade elektroniska maskiner är emellertid att de är så komplexa att det är omöjligt att testa alla funktioner fullständigt innan produkten måste sändas ut på marknaden.

Otillräcklig testning kan leda till defekta produkter. Två kända exempel är Intels Pentium processor som inte kunde räkna rätt när den blev utsatt för komplexa problem och det Europeiska rymdprogrammets Ariane-raket som exploderade strax efter start på grund av ett fel i en elektrisk krets.

Under många år har simulering varit det enda sättet att verifiera en krets gentemot dess specifikation. Eftersom simulering är tidskrävande kan man omöjligt testa alla fall för större kretsar. Detta är anledningen till att mjukvara har utvecklats som utför ekvivalenskontroll mellan två kretsar eller mellan en krets och dess specifikation. Denna mjukvara använder oftast någon form av trädstruktur t ex. binära beslutsträd, men eftersom det är en ny marknad och ett område med mycket forskning så är den bästa lösningen inte funnen än.

Detta examensarbete har två mål. Hitta en ny trädstruktur som kräver mindre tid än binära beslutsträd och som dessutom kan verifiera multiplikator-kretsar, vilket är omöjligt med binära beslutsträd. Det andra målet är att visa resultatet för användaren på ett överskådligt sätt utan några onödiga uttryck, och göra det möjligt för användaren att påverka resultatet genom att sätta variabler till ett eller noll.
Ämnesord / Subject: Telekommunikation - Telecommunications

Nyckelord / Keywords: Formal verification, BED, BDD, BMD, *BMD, Binary Trees, France, Frankrike, Telecom Valley, Andreas, Fredrik, Boolean, C, C++, Verilog, VHDL

Publication info

Dokument id / Document id:
Program:/ Programme Telekommunikation
Registreringsdatum / Date of registration: 09/16/2004
Uppsatstyp / Type of thesis: C-Uppsats

Context

Handledare / Supervisor: Frederic Rocheteau, Jerome Rampon
veriphia@cica.fr
Examinator / Examiner: Jörgen Andersson
Organisation / Organisation: Blekinge Institute of Technology
Institution / School: Inst för telekommunikation och signalbehandling/Dept. of Telecommunications and Signal Processing
Inst för telekommunikation och signalbehandling S-372 25 Ronneby
+46 455 780 00
http://www.bth.se/its
I samarbete med / In co-operation with: Veriphia (http://www.veriphia.com/)

Files & Access

Bifogad uppsats fil(er) / Files attached: attuuanm (1123 kB, öppnas i nytt fönster)