Thesis Details
Integrace formálních technik do procesu verifikace procesoru RISC-V
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.
functional verification, formal verification, UVM, SVA, assertions, RISC-V
Bidlo Michal, doc. Ing., Ph.D. (DCSY FIT BUT), člen
Fučík Otto, doc. Dr. Ing. (DCSY FIT BUT), člen
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT), člen
Szőke Igor, Ing., Ph.D. (DCGM FIT BUT), člen
@bachelorsthesis{FITBT22489,
author = "Jakub Hork\'{y}",
type = "Bachelor's thesis",
title = "Integrace form\'{a}ln\'{i}ch technik do procesu verifikace procesoru RISC-V",
school = "Brno University of Technology, Faculty of Information Technology",
year = 2020,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/22489/"
}