High-level Modeling, Analysis and Verification of Programmable Hardware Design

formální verifikace, vysokoúrovňová verifikace, analýza hardwarového návrhu, testování propustnosti, časovaná analýza

Tato práce se zabývá abstraktním modelováním návrhu a verifikací některých bezpečnostních vlastností. Hlavním cílem bylo zjistit, jestli se v systému vyskytuje přetečení bufferu a jak nastavit parametry délky front, aby k této chybě nedocházelo. Tato práce ukazuje, jak ručně modelovat složité systémy, a ukazuje dosažené výsledky touto metodou.