Формальная верификация

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

Основная проблема формальной верификации состоит в том, что она ещё не вышла на уровень повсеместного использования, поэтому находится много желающих, которые с радостью бросаются в эту область и теряются в массе различных направлений. Кроме отсутствия стандартов, здесь существует множество предложений, от которых просто голова идёт кругом. При этом почти каждый пытается внести свою лепту в существующую неразбериху, тем самым ещё больше осложняя ситуацию. Например, если попросить 20 поставщиков САПР дать определение терминам утверждение и свойство и указать их отличия, вы сойдете с ума из-за диаметрально противоположных ответов [c.262]

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

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

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

Что такое формальная верификация, и чем она хороша [c.263]

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

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

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

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

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

Хотя аппаратное моделирование по-прежнему остаётся основным способом системной проверки, убедиться в правильности работы устройства вы можете только с помощью средств формальной верификации см. также гл. 19). В отличие от средств моделирования, формальная верификация математически доказывает, что реализация системы соответствует некоторой спецификации. [c.322]

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

Качества формальной верификации определяются тем, как инженеры её используют, что, впрочем, справедливо для всех средств. Фактически формальная верификация может ответить только на один вопрос — насколько моя реализация соответствует спецификации Но появляется другой вопрос — насколько корректно составлена сама спецификация [c.324]

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

Верификация модели — см. Формальная верификация, [c.382]

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

Описание — в контексте формальной верификации этот термин объединяет в себе утверждения, свойства, события и ограничения, которые существуют вместе с другими структурными элементами устройства. [c.389]

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

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

Ограничения — термин пришел из области верификации модели (Model he king). В процессе формальной верификации модели устройства рассматриваются все возможные допустимые входные комбинации. Следовательно, часто возникает необходимость ограничивать входные воздействия по каким-либо признакам, в противном случае средства проверки будут сигнализировать об ошибочных отказах и нарушениях свойств устройства, которые обычно не возникают в реальных устройствах. Как и свойства, ограничения также могут быть простыми и сложными. В некоторых случаях ограничения могут быть интерпретированы как свойства, которые подлежат доказательству Например, входное ограничение первого модуля может быть также свойством выходного сигнала второго модуля, при этом выход второго модуля подключен к входу первого. Поэтому свойства и ограничения могут иметь двойственную природу Термин ограничение также используется в системах ограниченного стохастического моделирования, и в этом случае ограничение обычно применяется для обозначения диапазона значений, которые могут быть использованы для управления шиной. [c.265]

Прагмы — сокращение словосочетания прагматическая информация , относится к специальным директивам в виде псевдокомментариев, которые могут интерпретироваться и использоваться различными анализаторами, компиляторами и другими средствами. (Это универсальный термин, и прагма-методы широко используются не только при формальной верификации.) [c.266]

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

Общий слой — токопроводящий слой, находящийся в или на подложке, обеспечивающий заземление или общий провод для компонентов микросхемы. В микросхеме может быть несколько таких слоёв, разделённых изоляционными слоями. Объединенный инженерный совет по электронным устройствам — см. JEDE . Ограничения — понятие относится к формальной верификации. В процессе верификации устройства (системы) рассматриваются все возможные комбинации входных воздействий, следовательно, часто возникает необходимость ограничить входные воздействия для корректного поведения устройства (системы). [c.388]

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

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