Образовни циљ овог курса је стицање знања из области формалне спецификације и верификације дигиталног хардвера. То су напредна знања потребна у раду једног верификационог инжењера.

Након успешног завршетка предмета студенти ће знати теоријске основе за спецификацију и верификацију хардвера. Студенти ће моћи превести неформални опис хардвера на формалне спецификације особина и знаће да користе EDA алате потребне за формалну верификацију хардвера.

Увод у формалну спецификацију и верификацију хардвера: контекст, дизајн кола, грешке и циклус дизајнирања, формална верификација наспрам симулације, тест-вектора, design-for-verification стилова писања кода и верификације базиране на трврђењима (assertion-based verification, ABV), формални (статички), семи-формални и неформални (динамички, функционални) приступ верификацији, језици за спецификацију особина (PSL, SVA), симболичка провера модела (model checking), златни дизајн, логичка еквивалентност, приступи верификацији базирани на Буловим функцијама, репрезентације Булових функција преко бинарних дијаграма одлучивања (BDD), приступи верификацији базирани на проблему задовољивости (SAT), ограничена провера модела (BMC), решавачи SAT проблема, комбиновани SAT-BDD проверивачи, приступи верификацији базирани на коначним аутоматима (FSM), формална верификација хардвера у логикама вишег реда (CTL, LTL), описи хардвера коришћењем темпоралних структура, логичких формула и спецификација, коришћење формалних EDA алата за верификацију хардвера.

Предавања. Рачунарске вежбе. Консултације.