Obrazovni cilj ovog kursa je sticanje znanja iz oblasti formalne specifikacije i verifikacije digitalnog hardvera. To su napredna znanja potrebna u radu jednog verifikacionog inženjera.

Nakon uspešnog završetka predmeta studenti će znati teorijske osnove za specifikaciju i verifikaciju hardvera. Studenti će moći prevesti neformalni opis hardvera na formalne specifikacije osobina i znaće da koriste EDA alate potrebne za formalnu verifikaciju hardvera.

Uvod u formalnu specifikaciju i verifikaciju hardvera: kontekst, dizajn kola, greške i ciklus dizajniranja, formalna verifikacija naspram simulacije, test-vektora, design-for-verification stilova pisanja koda i verifikacije bazirane na trvrđenjima (assertion-based verification, ABV), formalni (statički), semi-formalni i neformalni (dinamički, funkcionalni) pristup verifikaciji, jezici za specifikaciju osobina (PSL, SVA), simbolička provera modela (model checking), zlatni dizajn, logička ekvivalentnost, pristupi verifikaciji bazirani na Bulovim funkcijama, reprezentacije Bulovih funkcija preko binarnih dijagrama odlučivanja (BDD), pristupi verifikaciji bazirani na problemu zadovoljivosti (SAT), ograničena provera modela (BMC), rešavači SAT problema, kombinovani SAT-BDD proverivači, pristupi verifikaciji bazirani na konačnim automatima (FSM), formalna verifikacija hardvera u logikama višeg reda (CTL, LTL), opisi hardvera korišćenjem temporalnih struktura, logičkih formula i specifikacija, korišćenje formalnih EDA alata za verifikaciju hardvera.

Predavanja. Računarske vežbe. Konsultacije.