{"id":14,"date":"2018-03-07T08:37:11","date_gmt":"2018-03-07T08:37:11","guid":{"rendered":"http:\/\/www.elektronika.ftn.uns.ac.rs\/formalne-metode-projektovanja-i-verifikacije-hardvera\/?post_type=specifikacija&#038;p=14"},"modified":"2023-10-06T07:39:26","modified_gmt":"2023-10-06T07:39:26","slug":"specifikacija-predmeta","status":"publish","type":"specifikacija","link":"https:\/\/www.elektronika.ftn.uns.ac.rs\/formalne-metode-projektovanja-i-verifikacije-hardvera\/specifikacija\/specifikacija-predmeta\/","title":{"rendered":"Formalne metode projektovanja i verifikacije hardvera"},"content":{"rendered":"<h1>Cilj predmeta<\/h1>\n<p>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\u017eenjera.<\/p>\n<h1>Ishodi predmeta<\/h1>\n<p>Nakon uspe\u0161nog zavr\u0161etka predmeta studenti \u0107e znati teorijske osnove za formalnu specifikaciju i verifikaciju hardvera. Studenti \u0107e mo\u0107i prevesti neformalni opis hardvera na formalne specifikacije osobina i zna\u0107e da koriste EDA alate potrebne za formalnu verifikaciju hardvera.<\/p>\n<h1>Sadr\u017eaj predmeta<\/h1>\n<p>Uvod u formalnu specifikaciju i verifikaciju hardvera: kontekst, dizajn kola, gre\u0161ke i ciklus dizajniranja, formalna verifikacija naspram simulacije, test-vektora, design-for-verification stilova pisanja koda i verifikacije bazirane na trvr\u0111enjima (assertion-based verification, ABV), formalni (stati\u010dki), semi-formalni i neformalni (dinami\u010dki, funkcionalni) pristup verifikaciji, jezici za specifikaciju osobina (PSL, SVA), simboli\u010dka provera modela (model checking), zlatni dizajn, logi\u010dka ekvivalentnost, pristupi verifikaciji bazirani na Bulovim funkcijama, reprezentacije Bulovih funkcija preko binarnih dijagrama odlu\u010divanja (BDD), pristupi verifikaciji bazirani na problemu zadovoljivosti (SAT), ograni\u010dena provera modela (BMC), re\u0161ava\u010di SAT problema, kombinovani SAT-BDD proveriva\u010di, pristupi verifikaciji bazirani na kona\u010dnim automatima (FSM), formalna verifikacija hardvera u logikama vi\u0161eg reda (CTL, LTL), opisi hardvera kori\u0161\u0107enjem temporalnih struktura, logi\u010dkih formula i specifikacija, kori\u0161\u0107enje formalnih EDA alata za verifikaciju hardvera.<\/p>\n","protected":false},"featured_media":0,"template":"","acf":[],"_links":{"self":[{"href":"https:\/\/www.elektronika.ftn.uns.ac.rs\/formalne-metode-projektovanja-i-verifikacije-hardvera\/wp-json\/wp\/v2\/specifikacija\/14"}],"collection":[{"href":"https:\/\/www.elektronika.ftn.uns.ac.rs\/formalne-metode-projektovanja-i-verifikacije-hardvera\/wp-json\/wp\/v2\/specifikacija"}],"about":[{"href":"https:\/\/www.elektronika.ftn.uns.ac.rs\/formalne-metode-projektovanja-i-verifikacije-hardvera\/wp-json\/wp\/v2\/types\/specifikacija"}],"version-history":[{"count":23,"href":"https:\/\/www.elektronika.ftn.uns.ac.rs\/formalne-metode-projektovanja-i-verifikacije-hardvera\/wp-json\/wp\/v2\/specifikacija\/14\/revisions"}],"predecessor-version":[{"id":84,"href":"https:\/\/www.elektronika.ftn.uns.ac.rs\/formalne-metode-projektovanja-i-verifikacije-hardvera\/wp-json\/wp\/v2\/specifikacija\/14\/revisions\/84"}],"wp:attachment":[{"href":"https:\/\/www.elektronika.ftn.uns.ac.rs\/formalne-metode-projektovanja-i-verifikacije-hardvera\/wp-json\/wp\/v2\/media?parent=14"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}