Original title: Integrace formálních technik do procesu verifikace procesoru RISC-V
Translated title: Enriching the Process of Verification of RISC-V Processor with Formal Techniques
Authors: Horký, Jakub ; Šnobl, Pavel (referee) ; Hruška, Tomáš (advisor)
Document type: Bachelor's theses
Year: 2020
Language: cze
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [cze] [eng]
Tato práce krátce rozebírá architekturu RISC-V a návrh procesorů a jak jednoduše může vzniknout chyba při jejich vytváření. Dále popisuji, jakým způsobem se snaží funkční verifikace tyto chyby odhalit a jaké jsou její výhody a nedostatky. Konkrétněji se zaměřím, jak vypadá verifikační prostředí podle UVM.  Popisuji, jakým způsobem do funkční verifikace zapadá formální verifikace a jaké jsou dostupné nástroje pro formální verifikaci.   Ke konci této práce popisuji konkrétně způsob mého postupu při psaní tvrzení (psaných v SVA jazyce) pro RISC-V procesor za použití nástroje pro formální verifikaci tvrzení. Při využití těchto tvrzení pro ověření procesoru v pozdější fázi vývoje, kdy funkční verifikace již měla možnost většinu chyb odhalit, se mi přesto podařilo několik chyb najít. This thesis provides a brief overview of the RISC-V architecture, design of processors, and how easily a bug can arise during the development. Then this thesis describes the way functional verification tries to discover those bugs and what are its pros and cons. More specifically, the thesis focuses on what the verification environment in UVM look like. Then the thesis describes, how formal verification fits in to the functional verification and shows the tools that are available for formal verification.   The final part of this thesis, describes the process of how I wrote the assertions (written in SVA) for a RISC-V processor, using a property checking tool. Using these assertions for verifying a processor in the late stage of development, when functional verification already had the possibility to discover most of the bugs, I still was able to discover few of those bugs.
Keywords: assertions; formal verification; functional verification; RISC-V; SVA; UVM; formální verifikace; funkční verifikace; RISC-V.; SVA; tvrzení; UVM

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/212673

Permalink: http://www.nusl.cz/ntk/nusl-530902


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Bachelor's theses