Detail práce
Integrace formálních technik do procesu verifikace procesoru RISC-V
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.
funkční verifikace, formální verifikace, UVM, SVA, tvrzení, RISC-V.
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm B.
- Můžete uvést, do jaké míry jsou Vámi implementovaná tvrzení použitelná i na ostatních procesorech od firmy Codasip implementujících instrukční sadu RISC-V - konkrétně procesorech Bk5 a Bk7?
- Do jaké míry je nutné daná tvrzení změnit v případě verifikace procesoru založeného na 64-bitové verzi RISC-V specifikace?
Bidlo Michal, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Fučík Otto, doc. Dr. Ing. (UPSY FIT VUT), člen
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT), člen
Szőke Igor, Ing., Ph.D. (UPGM FIT VUT), člen
@bachelorsthesis{FITBT22489,
author = "Jakub Hork\'{y}",
type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
title = "Integrace form\'{a}ln\'{i}ch technik do procesu verifikace procesoru RISC-V",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2020,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/22489/"
}