ПОИСК Статьи Чертежи Таблицы Статическая и динамическая формальная верификация из "Проектирование на ПЛИС архитектура, средства и методы " Данная тема может оказаться несколько трудной для восприятия, поэтому будем погружаться в нее постепенно. Во-первых, в среде моделирования можно использовать утверждения/свойства. В том случае, когда эти свойства и утверждения означают, что сигналы А и В никогда не будут активными одновременно , и когда такая недопустимая ситуация всё-таки имеет место во время моделирования, на экране появится соответствующее предупреждение и данное событие будет зарегистрировано в журнале. [c.268] Альтернативой системам моделирования может служить статическая формальная верификация. Эти средства отличаются высокой точностью и позволяют проверять всё пространство состояний устройства без применения систем моделирования. Их недостаток кроется в том, что обычно они могут использоваться только для небольших частей устройства, так как пространство состояний с увеличением сложности возрастает по экспоненте и можно очень быстро дойти до так называемого разрыва пространства состояний. В отличие от статической формальной верификации системы логического моделирования, которые также могут быть использованы для проверки утверждений, могут охватывать огромные устройства, но для их работы требуются задающие воздействия и применять их можно не в каждой ситуации. [c.268] Например, можно использовать моделирование до тех пор, пока не будет достигнуто определённое тупиковое состояние, затем сделать паузу и автоматически вызвать алгоритм статической формальной верификации для более тщательного обследования этого состояния. В контексте рассматриваемого материала понятия тупиковое состояние и тупиковая ситуация характеризуют трудновыполнимые и труднодоступные функциональные состояния устройства. После оценки тупикового состояния управление автоматически вернётся к системе моделирования для выполнения дальнейшей работы. Эта комбинация системы моделирования и традиционной статической формальной верификации называется динамической формальной верификацией. [c.268] В качестве простого примера применения динамической формальной верификации рассмотрим память типа FIFO (очередь вида первым пришёл, первым вышел ), в которой состояния заполнена и пустая могут считаться тупиковыми ситуациями. Для заполнения такой очереди потребуется много тактов, поэтому состояния заполнена можно достичь с помощью системы моделирования. Но точная оценка утверждений/свойств, связанных с этими тупиковыми ситуациями, например факт того, что в память FIFO невозможно записать какие-либо данные, пока не освободится место, лучше всего достигается с помощью статических методов. [c.268] И еще хороший пример такого средства динамического верификации предоставляет компания 0-1п. Библиотека моделей he kerWare содержит подробные описания тупиковых ситуаций. Если в процессе моделирования достигается положение тупикового состояния, система останавливается, и для детального анализа этого случая используется средство статической верификации. [c.268] Вернуться к основной статье