Пројектовање и верификација хардвера

Увод у формалну спецификацију и верификацију хардвера: контекст, дизајн кола, грешке и циклус дизајнирања. Формална верификација, симулације, тест-вектори, тест-бенчеви, design-for-test и design-for-verification стилови писања кода и верификације базиране на тврђењима (assertion-based verification, ABV). Формални (статички), семи-формални и неформални (динамички, функционални) приступ верификацији. Језици за верификацију хардвера (HVLs). Језици за спецификацију особина (PSLs). Језици за опис формалних особина хардвера (FPLs). Симболичка провера модела (model checking), златни дизајн, логичка еквивалентност. Приступи верификацији базирани на Буловим функцијама. Репрезентације Булових функција преко бинарних дијаграма одлучивања (BDD). Проширења и варијанте BDD-ова. Приступи верификацији базирани на проблему задовољивости (SAT), ограничена провера модела (BMC), израчунавање симболичке трајекторије (STE), решавачи SAT проблема, комбиновани SAT-BDD проверивачи. Приступи верификацији базирани на коначним аутоматима (FSM). Формална верификација хардвера у логикама вишег реда (PTL, CTL, LTL). Описи хардвера коришћењем темпоралних структура, логичких формула и спецификација. Пробабилистичка провера модела.

Рачунарски факултет Рачунарски факултет 011-33-48-079