Странице предмета

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