Formalne metode projektovanja i verifikacije hardvera

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: EM405A
Broj 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

Način formiranja ocene:

  • Odbranjene laboratorijske vežbe - 20%

  • Odbrana projekta - 50%

  • Završni ispit (teorija) - 30%


Materijal za predavanja:
Predavanje: PSL
Algoritmi

Materijal za laboratorijske/računarske vežbe: