Fakultet tehničkih nauka

Predmet: Formalne metode projektovanja i verifikacije hardvera (17.EM405A)

Matične organizacione jedinice predmeta: Departman za energetiku, elektroniku i telekomunikacije
Osnovne informacije:
 
Kategorija Teorijsko-metodološki
Uža naučna oblast Elektronika
ESPB 5

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.

Autori Naziv Godina Izdavač Jezik
Pallab Dasgupta A Roadmap for Formal Property Verification 2006 Springer Engleski
Eisner Cindy, Fisman Dana A Practical Introduction to PSL 2006 Springer Engleski
Christoph Meinel, Thorsten Theobald Algorithms and Data Structures in VLSI Design 1998 Springer Engleski
Thomas Kropf Introduction to Formal Hardware Verification 1999 Springer Engleski
Predmetna aktivnost Predispitna Obavezna Broj poena
Predmetna aktivnost
Pismeni deo ispita - kombinovani zadaci i teorija
Predispitna
Ne
Obavezna
Da
Broj poena
30.00
Predmetna aktivnost
Odbrana projekta
Predispitna
Da
Obavezna
Da
Broj poena
50.00
Predmetna aktivnost
Složeni oblici vežbi
Predispitna
Da
Obavezna
Da
Broj poena
20.00
Predavanja
Predavanja
Laboratorijske vežbe