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 - 10%

  • Odbrana projekta ili dva veća zadatka - 60%

  • Završni ispit (teorija) - 30%


Materijal za predavanja:
Predavanja:

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

Materijal za laboratorijske/računarske vežbe: