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