Detail práce

Verifikace ASIP založena na formálních tvrzeních

Diplomová práce Student: Šulek Jakub Akademický rok: 2014/2015 Vedoucí: Zachariášová Marcela, Ing., Ph.D.
Název anglicky
Assertion-Based Verification of ASIP
Jazyk práce
český
Abstrakt
Tato práce představuje koncept pro ověřování správnosti procesorů s aplikačně-specifickou instrukční sadou (ASIP) pomocí verifi kace založené na formálních tvrzeních. Koncept je implementován v jazyku SystemVerilog Assertions jako součást verifi kačního prostředí vytvořeného v nástroji Codasip Framework. Implementovaný koncept je simulován nástrojem QuestaSim na procesoru Codix RISC. Hlavním výsledkem práce je koncept ověřování, který může být součástí systému automatizujícího návrh procesorů, a který je použitelný pro různé typy procesorů.
Klíčová slova

SystemVerilog Assertions, verifi kace založena na formálních tvrzeních, procesor s aplikačně-specifi ckou instrukční sadou, veri fikační prostředí

Ústav
Studijní program
Informační technologie, obor Informační systémy
Stav
obhájeno, hodnocení B
Obhajoba
23. června 2015
Oponent
Průběh obhajoby

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.

Otázky u obhajoby

Jak pameťove náročná je verifikace založená na formálních tvrzení?

Komise
Kolář Dušan, doc. Dr. Ing. (UIFS FIT VUT), předseda
Brada Přemysl, doc. Ing., MSc. Ph.D. (ZČU v Plzni), člen
Janoušek Vladimír, doc. Ing., Ph.D. (UITS FIT VUT), člen
Květoňová Šárka, Ing., Ph.D. (UIFS FIT VUT), člen
Očenášek Pavel, Mgr. Ing., Ph.D. (UIFS FIT VUT), člen
Zendulka Jaroslav, doc. Ing., CSc. (UIFS FIT VUT), člen
Citace
ŠULEK, Jakub. Verifikace ASIP založena na formálních tvrzeních. Brno, 2015. Diplomová práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2015-06-23. Vedoucí práce Zachariášová Marcela. Dostupné z: https://www.fit.vut.cz/study/thesis/17782/
BibTeX
@mastersthesis{FITMT17782,
    author = "Jakub \v{S}ulek",
    type = "Diplomov\'{a} pr\'{a}ce",
    title = "Verifikace ASIP zalo\v{z}ena na form\'{a}ln\'{i}ch tvrzen\'{i}ch",
    school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
    year = 2015,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/17782/"
}
Nahoru