Особенности формальной верификации

Особенности формальной верификации [c.263]

И в завершении этих рассуждений уточню под формальной верификацией мы будем понимать именно верификацию модели. Также замечу, что существует и другая категория формальной верификации, известная как автоматизированные рассуждения, которые для тестирования устройств используют логику, больше напоминающую формальное математическое доказательство, и применение этого вида тестирования имеет свои характерные особенности. [c.263]

Разумеется, утверждения и свойства могут быть связаны с устройством на любом уровне, т. е. могут относиться к отдельным блокам, к нескольким соединённым по какому-либо интерфейсу блокам или ко всей системе. Эта особенность предусматривает важную процедуру, которая называется повторная верификация. До появления формальной верификации повторная верификация использовалась довольно редко. Например, при продаже ядро 1Р обычно снабжается соответствующими средствами тестирования, которые анализируют сигналы ввода/вывода непосредственно на его входах и выходах. Эти средства позволяют проверять отдельное ядро, но как только ядро будет интегрировано в устройство, поставляемые с ним средства тестирования становятся бесполезными. [c.264]

Несмотря на то что большие компьютерные компании и производители микросхем, такие как IBM, Intel и Motorola, десятилетиями разрабатывают и используют свои средства формальной верификации (примерно с середины 80-х), для большинства людей эта область тестирования всё же является новой. Особенно это касается ПЛИС, где применение формальной верификации отстаёт от заказных микросхем. Следует заметить, что формальная верификация может быть настолько мощным средством, что всё больше и больше людей начинают воспринимать её всерьез. [c.262]

Энциклопедия по машиностроению XXL

Оборудование, материаловедение, механика и ...