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
- Odbranjene laboratorijske vežbe - 10%
- Odbrana projekta ili dva veća zadatka - 60%
- Završni ispit (teorija) - 30%
1. Motivacija za FV
2. Uvod u SVA
Formalna metodologija
Algoritmi
Literatura:
- Formal Verification - An Essential Toolkit for Modern VLSI Design - Erik Seligman, Tom Schubert, M V Achutha Kiran Kumar
- SVA: The Power of Assertions in SystemVerilog (2nd) - Eduard Cerny, Surrendra Dudani, John Havlicek, Dmitry Korchemny
- Introduction to Formal Hardware Verification - Thomas Kropf