Статическая и динамическая формальная верификация

Давайте вернемся к рассмотрению очень простого утверждения/свойства вида Сигналы А и Б никогда не будут активными одновременно . Здесь должен прозвучать термин верификация на основе утверждений, который постоянно присутствует в разговорах о моделировании, статической формальной верификации и динамической формальной верификации. При статической формальной верификации соответствующее средство считывает функциональное описание устройства, обычно на уровне абстракции регистровых передач (КТЬ), и затем полностью анализирует его логику, чтобы гарантировать, что именно это частное условие никогда не наступит. При динамической формальной верификации соответствующим образом расширенная система логического моделирования будет работать до определенного момента, затем прервется и автоматически запустит соответствующее средство формальной верификации. [c.264]

Статическая и динамическая формальная верификация [c.268]

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

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

Статическая формальная верификация — формальная проверка, в ходе которой проверяется всё пространство состояний устройства без использования каких-либо средств моделирования. Недостатком такого метода является то, что он может использоваться только для небольших частей устройства, так как с ростом сложности конструкции объем пространства состояний увеличивается по экспоненциальному закону и очень быстро можно достичь точки его разрыва . См. также Формальная верификация VI Динамическая формальная верификация. [c.393]

В качестве простого примера применения динамической формальной верификации рассмотрим память типа FIFO (очередь вида первым пришёл, первым вышел ), в которой состояния заполнена и пустая могут считаться тупиковыми ситуациями. Для заполнения такой очереди потребуется много тактов, поэтому состояния заполнена можно достичь с помощью системы моделирования. Но точная оценка утверждений/свойств, связанных с этими тупиковыми ситуациями, например факт того, что в память FIFO невозможно записать какие-либо данные, пока не освободится место, лучше всего достигается с помощью статических методов. [c.268]

Формальная верификация — в недалёком прошлом термин формальная верификация (проверка) для большинства инженеров являлся синонимом проверки на эквивалентность. В контексте рассматриваемого материала проверка на эквивалентность подразумевает под собой средства, которые используют формальные (строго математические) методы сравнения двух различных представлений одного устройства — скажем RTL-описания и таблицы соединений вентилей — для определения идентичности их функциональности от входов до выходов. На практике проверка на эквивалентность может рассматриваться как подкласс формальной верификации и называться верификацией модели (model he king), которая используется при анализе конечных автоматов системы для тестирования некоторых свойств устройства, которые обычно нгзывгютутверждениями. См. также Статическая формальная верификация и Динамическая формальная верификация. [c.395]

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

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