Cilj predmeta
Obrazovni cilj ovog predmeta je sticanje znanja iz oblasti formalne specifikacije i verifikacije digitalnog hardvera. To su napredna znanja potrebna u radu jednog verifikacionog inženjera.
Ishodi predmeta
Nakon uspešnog završetka predmeta studenti će znati teorijske osnove za formalnu 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.
Sadržaj predmeta
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.
Specifikacija predmeta
Oznaka predmeta: EM405ABroj ESPB: 4
Broj časova aktivne nastave nedeljno: 2+2
Nastavni kadar
Nastavnik: dr Vuk VranjkovićKonsultacije: Po dogovoru
Asistenti: dr Vuk Vranjković
Konsultacije: Po dogovoru
Način polaganja ispita
- Laboratorijske vežbe - 10%
- Primenjeni deo - 60%
- Teorijski deo - 30%