Fakulta informačních technologií VUT v Brně

Detail práce

Automated Verification in HW/SW Co-design

Disertační práce Student: Charvát Lukáš Ak.rok: 2019/2020 Vedoucí: Vojnar Tomáš, prof. Ing., Ph.D.
Název česky
Automatická verifikace v procesu soubežného návrhu hardware a software
Jazyk
anglický
Stav
odevzdáno
Obhajoba
1. října 2019
Ústav
Studijní program
Obor studia
Soubory
Klíčová slova
Formální verifikace, mikroprocesor, souběžný návrh hardware a software, jazyk pro popis architektury, formální ověřování ekvivalence, hazardy v lince zřetězení, parametrické systémy
Abstrakt
Předmětem dizertační práce je návrh nových technik pro verifikaci hardwaru, které jsou optimalizovány pro použití v procesu souběžného vývoje hardwaru a softwaru. V rámci tohoto typu vývoje je hardware spolu se software vyvíjen paralelně s cílem urychlit vývoj nových systémů. Současné nástroje pro tvorbu mikroprocesorů stavějící na tomto stylu vývoje obvykle umožňují vývojářům ověřit jejich návrh využitím různých simulačních technik a/nebo za pomoci tzv. funkční verifikace. Společnou nevýhodou těchto přístupů je, že se zaměřují pouze na hledání chyb. Výsledný produkt tedy může stále obsahovat nenalezené netriviální defekty. Z tohoto důvodu se v posledních letech stává stále více žádané nasazení formálních metod. Na rozdíl od výše uvedených přístupů založených na hledání chyb, se formální verifikace zaměřuje na dodání rigorózního důkazu, že daný systém skutečně splňuje požadované vlastnosti. I když bylo v uplynulých letech v této oblasti dosaženo značného pokroku, tak aktuální formální přístupy nemají zdaleka schopnost plně automaticky prověřit všechny relevantní vlastnosti verifikovaného návrhu bez výrazného a často nákladného zapojení lidí v rámci verifikačního procesu. Tato práce se snaží řešit problém s automatizací verifikačního procesu jejím zaměřením na verifikační techniky, ve kterých je ale záměrně kladen menší důraz na jejich přesnost a obecnost za cenu dosažení plné automatizace (např. vyloučením potřeby ručně vytvářet modely prostředí). Dále se práce také zaměřuje na efektivitu navrhovaných technik a jejich schopnost poskytovat nepřetržitou zpětnou vazbu o verifikačním procesu (např. v podobě podaní informace o aktuálních stavu pokrytí). Zvláštní pozornost je pak věnována vývoji formálních metod ověřujících ekvivalenci návrhů mikroprocesorů na různých úrovních abstrakce. Tyto návrhy se mohou lišit ve způsobu, jakým jsou vnitřně zpracovány programové instrukce, nicméně z vnějšího pohledu (daného např. obsahem registrů viditelných z pozice programátora) musí být jejich chování při provádění stejného vstupního programu shodné. Jako další téma se práce dále věnuje návrhu metod pro verifikaci správnosti mechanismů zabraňujících výskytu datových a řídících hazardů v rámci linky zřetězeného zpracování instrukcí. Veškeré metody popsané v této práci byly implementovány ve formě několika nástrojů. Aplikací těchto nástrojů pro verifikaci návrhů netriviálních procesorů bylo dosaženo slibných experimentálních výsledků.
Citace
CHARVÁT, Lukáš. Automated Verification in HW/SW Co-design. Brno, 2019. Disertační práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2019-10-01. Vedoucí práce Vojnar Tomáš. Dostupné z: https://www.fit.vut.cz/study/phd-thesis/625/
BibTeX
@PHDTHESIS{FITPT625,
    author = "Luk\'{a}\v{s} Charv\'{a}t",
    type = "Diserta\v{c}n\'{i} pr\'{a}ce",
    title = "Automated Verification in HW/SW Co-design",
    school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
    year = 2019,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/phd-thesis/625/"
}
Nahoru