Application of Formal Verification Techniques
1999 (English)Independent thesis Basic level (degree of Bachelor)
Student thesisAlternative title
Applikation för formell verifikation (Swedish)
Abstract [en]
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.
Abstract [sv]
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.
Place, publisher, year, edition, pages
1999. , p. 71
Keywords [en]
Formal verification, BED, BDD, BMD, *BMD, Binary Trees, France, Frankrike, Telecom Valley, Andreas, Fredrik, Boolean, C, C++, Verilog, VHDL
National Category
Telecommunications
Identifiers
URN: urn:nbn:se:bth-2622Local ID: oai:bth.se:arkivexDF4DC39C6FB06366C125687D005B93DFOAI: oai:DiVA.org:bth-2622DiVA, id: diva2:829908
Uppsok
Technology
Supervisors
2015-04-222000-02-062015-06-30Bibliographically approved