Формальная проверка в VHDL с использованием PSL

При разработке VHDL для критически важных с точки зрения безопасности приложений FPGA недостаточно написать испытательные стенды с максимальной отдачей. Вы должны предоставить доказательства того, что модуль работает должным образом и не имеет нежелательных побочных эффектов.

Методы формальной проверки могут помочь вам сопоставить требование с тестом, доказав, что ваш модуль VHDL соответствует спецификации. Это полезный инструмент для проверки медицинских приложений или получения сертификата DO-254 для бортовых решений FPGA.

Чтобы демистифицировать формальную проверку, VHDLwhiz заручается поддержкой Майкла Финна Йоргенсена для написания этого гостевого поста. У Майкла есть значительный опыт в этой теме, и он делится множеством советов на своей странице GitHub.

Тестируемое устройство в загружаемом примере этой статьи взято из существующего руководства:
Как создать AXI FIFO в блочной ОЗУ с помощью готового/действительного рукопожатия

Теперь я позволю Майклу взять на себя ответственность и объяснить вам формальную проверку в оставшейся части этого сообщения в блоге.

Что такое формальная проверка?

Цель формальной верификации (FV) — убедиться, что ваш модуль работает должным образом!

FV — это то, что вы делаете как часть процесса разработки, прежде чем синтезировать свой модуль. Иногда это называют «проверкой свойств», что, на мой взгляд, является более подходящим описанием.

В FV вы указываете свойства ваш модуль должен иметь, и тогда инструмент (называемый «Решатель удовлетворительности») докажет что ваш модуль удовлетворяет свойствам для всех возможных последовательностей входных данных .

Другими словами, инструмент будет искать любой переход от действительного состояние (где все свойства удовлетворены) на недействительное состояние (где одно или несколько свойств нарушены). Если такого перехода нет, т. е. нет способа перейти в недопустимое состояние, то доказано, что свойства всегда выполняются.

Задача FV состоит в том, чтобы выразить свойства вашего модуля на языке, понятном инструменту.

Формальная верификация — это альтернатива написанным вручную тестовым стендам. Цель как формальной проверки, так и ручных тестовых стендов состоит в том, чтобы устранить ошибки в проекте, но формальная проверка делает это путем изучения свойств и автоматического создания множества различных тестовых стендов.

Инструменты используют два разных метода:

Ограниченная проверка модели (BMC) . Начинается со сброса и проверяет фиксированное количество тактов.
Доказательство индукции . Начинает с произвольного допустимого состояния и проверяет, являются ли все последующие состояния также допустимыми.

Доказательство по индукции выполнить труднее, потому что оно требует всех свойства должны быть указаны, в то время как BMC можно запускать с несколькими свойствами и при этом давать полезные результаты.

Зачем использовать формальную проверку?

Формальная верификация очень хороша для обнаружения труднодоступных ошибок! Это связано с тем, что формальная проверка автоматически ищет все возможные входные данные.

Это отличается от традиционного письма на тестовом стенде, которое требует ручного создания стимулов. Практически невозможно исследовать все пространство состояний с помощью написанных вручную тестовых стендов.

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

Однако формальная верификация не заменяет написания тестового стенда. По моему опыту, формальная верификация хорошо подходит для модульного тестирования, тогда как интеграционное тестирование лучше проводить с помощью созданных вручную тестовых стендов. Это связано с тем, что время выполнения формальной проверки экспоненциально увеличивается с размером модуля.

Формальная верификация действительно требует некоторого обучения, но оно того стоит, и я надеюсь, что эта запись в блоге поможет вам справиться с этим процессом обучения. Вы завершите свой дизайн быстрее, и в нем будет меньше ошибок!

Как написать свойства в PSL

Выполняя формальную проверку, вы должны выразить свойства вашего модуля, используя язык спецификации свойств (PSL). Свойства обычно находятся в отдельном файле с окончанием .psl. , и этот файл используется только во время формальной проверки.

В этом разделе я в общих чертах опишу основные возможности языка PSL, а в следующем разделе я покажу вам конкретный пример.

В PSL есть три утверждения:

assert
assume
cover

Возможно, вам уже знакомо ключевое слово assert. при написании тестбенчей. Это же ключевое слово используется и в PSL, но с немного другим синтаксисом. assert ключевое слово используется для описания свойств, которые этот модуль обещает всегда выполнять. В частности, assert ключевое слово применяется к выходным данным модуля или, возможно, также к внутреннему состоянию.

assume ключевое слово используется для описания любых требований, которые этот модуль предъявляет к входным данным. Другими словами, assume ключевое слово применяется к входным данным модуля.

cover ключевое слово используется для описания свойств, которые должны быть доступны каким-то образом.

Вы также можете написать обычный код VHDL в файле PSL, включая объявления сигналов и процессы (как синхронные, так и комбинаторные).

Первая строка файла PSL должна быть

Здесь ENTITY_NAME и ARCHITECTURE_NAME обратитесь к модулю, который вы проверяете. INSTANCE_NAME может быть что угодно. Файл должен заканчиваться закрывающей фигурной скобкой:} .

Следующая строка в .psl файл должен быть:

Это позволяет избежать утомительного обращения к тактовому сигналу в каждом из операторов свойств.

Синтаксис для assert и assume утверждения:

Это утверждение выглядит следующим образом:Если PRECONDITION удерживается (в любом такте), то POSTCONDITION должно быть выполнено в одном тактовый цикл.

Существует еще одна часто используемая форма:

Это утверждение выглядит следующим образом:Если PRECONDITION сохраняется (в любом такте), то POSTCONDITION должно быть выполнено в следующем тактовый цикл.

Обе формы широко используются.

Внутри PRE- и POST-CONDITIONS , вы можете использовать ключевое слово stable . Это ключевое слово означает:значение в this тактовый цикл совпадает со значением в предыдущем тактовый цикл.

Внутри PRE- и POST-CONDITIONS , вы также можете использовать последовательности, написав следующее:

Это означает, что CONDITION_1 должен быть удовлетворен в этом такт и этот CONDITION_2 должно быть выполнено на следующем тактовый цикл.

Оператор покрытия имеет следующий синтаксис:

Мы увидим множество примеров всех этих утверждений в рабочем примере позже в этом блоге.

Установка необходимых инструментов

Формальная верификация поддерживается ведущими поставщиками инструментов, включая ModelSim. К сожалению, студенческая версия ModelSim НЕ поддерживает формальную проверку. Действительно, вы получаете следующую ошибку:

Таким образом, для использования ModelSim для формальной проверки требуется платная лицензия.

Вместо этого есть инструменты с открытым исходным кодом (бесплатные), которые позволяют проводить формальную проверку. В этом разделе я проведу вас через процесс установки этих инструментов.

В этом руководстве предполагается, что вы работаете на платформе Linux. Если вы работаете на платформе Windows, я рекомендую использовать подсистему Windows для Linux (WSL). Следующее руководство проверено с использованием Ubuntu 20.04 LTS.

Предпосылки

Во-первых, мы должны обновить систему, чтобы получить последние исправления:

Затем мы должны установить дополнительные пакеты разработки:

Йосис и др.

GHDL и др.

Для GHDL существуют предварительно упакованные бинарные файлы, но я рекомендую загрузить последние исходные файлы и скомпилировать их следующим образом:

Скачать пример проекта

Следующий раздел этой статьи поможет вам реализовать формальную проверку для существующего проекта VHDL. Вы можете загрузить полный код, указав свой адрес электронной почты в форме ниже.

Рабочий пример с формальной проверкой

В следующем разделе описывается, как официально проверить модуль axi_fifo, о котором мы писали ранее в этом блоге.

Чтобы начать формальную проверку, нам нужно спросить себя, какими свойствами обладает FIFO? Я выделил четыре категории свойств:

Обработка сброса:модуль просыпается в четко определенном состоянии после сброса.
Сигнализация заполнения и опустошения FIFO:проверяет, правильно ли FIFO указывает условия заполнения и опустошения.
Протокол AXI:модуль удовлетворяет требованиям действительного/готового квитирования AXI.
Упорядочивание FIFO:FIFO не отбрасывает/дублирует/переупорядочивает элементы, которые проходят через него.

Далее я рассмотрю каждое из этих свойств.

Обработка сброса

Во-первых, мы объявляем, что модуль ожидает подтверждения сброса в течение одного такта:

100

Обратите внимание на отсутствие ключевого слова always. . Без always ключевое слово, утверждение верно только для самого первого такта.

Принято (и очень полезно) давать каждому формальному утверждению ярлык. При выполнении формальной проверки инструмент будет ссылаться на эти метки при сообщении о любых сбоях. Я использую соглашение о том, что всем таким меткам предшествует f_. .

Затем мы указываем, что FIFO должен быть пустым после сброса:

Обратите внимание, что можно ссылаться на внутренний сигналы в модуле, а не только порты. Здесь мы ссылаемся на count , который является текущим уровнем заполнения, т. е. количеством элементов, находящихся в настоящее время в FIFO. Это возможно, потому что мы ссылаемся на название архитектуры в первой строке файла PSL.

В качестве альтернативы мы могли бы иметь отдельный процесс в файле PSL, подсчитывающий количество элементов, входящих и исходящих из FIFO. Хотя это предпочтительнее, я собираюсь использовать сигнал внутреннего подсчета, чтобы этот пост был кратким и по существу.

Сигнализация полного и пустого FIFO

То, как AXI FIFO сигнализирует о заполнении и опустошении, с out_valid и in_ready сигналы. out_valid сигнал утверждается всякий раз, когда FIFO не пуст, а in_ready сигнал утверждается всякий раз, когда FIFO не заполнен. Давайте проверим эти свойства:

Протокол AXI

Квитирование действительного/готового AXI указывает, что передача данных происходит только тогда, когда оба valid и ready утверждаются одновременно. Одной из типичных ошибок при работе с этим протоколом является подтверждение достоверности (и сопутствующих данных) и отсутствие проверки готовности. Другими словами, если valid утверждается и ready нет, то valid должен оставаться активным в следующем такте, а данные должны оставаться неизменными. Это относится как к данным, поступающим в FIFO, так и к данным, поступающим из FIFO. Для ввода данных в FIFO мы используем код assume ключевое слово, а для данных, поступающих из FIFO, мы используем assert ключевое слово.

Обратите внимание на использование stable ключевое слово в сочетании с |=> оператор. Эти операторы ссылаются на два последовательных такта. В первом такте он проверяет, соответствует ли valid утверждается и ready не утверждается. Затем на следующем (втором) тактовом цикле (обозначенном как |=> оператор), значения valid и data должен быть таким же, как предыдущий (то есть первый) тактовый цикл.

Во-вторых, для протокола AXI требуется, чтобы ready сигнал стабильный. Это означает, что если FIFO может принимать данные (ready утверждается), но данные не вводятся (valid не утверждается), то на следующем такте ready должен оставаться подтвержденным.

Порядок FIFO

Еще одним важным свойством FIFO является то, что данные не дублируются/удаляются/заменяются местами. Выразить это свойство в PSL довольно сложно, и это самая трудная часть этой формальной проверки. Давайте внимательно рассмотрим это свойство шаг за шагом.

В целом можно сказать, что если какие-либо данные D1 поступают в FIFO раньше некоторых других данных D2, то на стороне выхода те же данные D1 должны покинуть FIFO раньше, чем D2.

Чтобы выразить это в PSL, нам нужны вспомогательные сигналы:f_sampled_in_d1 , f_sampled_in_d2 , f_sampled_out_d1 и f_sampled_out_d2 . Эти сигналы очищаются при сбросе и устанавливаются всякий раз, когда D1 или D2 входят или выходят из FIFO. После утверждения эти сигналы остаются подтвержденными.

Итак, мы выражаем свойство FIFO-упорядочения в двух частях:во-первых, предположение что как только D2 входит в FIFO, то D1 уже вошел ранее:

И, во-вторых, утверждение что после того, как D2 покинет FIFO, D1 уже ушел ранее:

Нам все еще нужно объявить и заполнить сигналы дискретизации, упомянутые выше. Мы делаем это следующим образом для входных сигналов дискретизации:

Здесь мы ссылаемся на два других сигнала, f_value_d1. и f_value_d2 . Они содержат значения данных D1 и D2. Эти сигналы могут содержать любые произвольные значений, и есть специальный способ сообщить об этом инструменту формальной проверки:

anyconst атрибут распознается формальным инструментом проверки. Это указывает на то, что инструмент может вставить вместо него любое постоянное значение.

Выше мы указали свойства FIFO.

Выполнение формальной проверки

Прежде чем мы сможем запустить инструмент формальной проверки, нам нужно написать небольшой скрипт axi_fifo.sby. :

Раздел [tasks] заявляет, что мы хотим использовать ограниченную проверку модели. Раздел [options] указывает, что BMC должен работать в течение 10 тактов. По умолчанию 20. Раздел [engines] выбирает, какой из нескольких различных решателей использовать. Могут быть различия в скорости выполнения различных возможных двигателей, в зависимости от вашего конкретного проекта. Пока просто оставьте это значение без изменений.

[script] раздел представляет собой интересную часть. Здесь мы указываем стандарт VHDL (2008 г.), значения дженериков, файлы для обработки и имя сущности верхнего уровня. Наконец, [files] раздел снова содержит имена файлов.

Когда этот скрипт готов, мы можем запустить фактическую формальную проверку с помощью этой команды:

Запуск инструмента формальной проверки заканчивается бесцеремонным заявлением:

И это просто означает, что все указанные нами свойства удовлетворяются для всех произвольных входных данных до 10 тактов. Увеличение глубины приводит к увеличению времени выполнения решателя. Однако обратите внимание, что глубина больше, чем глубина FIFO, а это означает, что BMC столкнется с ситуацией заполнения FIFO для некоторых входных последовательностей. Если бы мы выбрали, скажем, только 5 тактов, формальная проверка никогда не наткнулась бы на переполнение FIFO и не обнаружила бы никаких ошибок, связанных с этим.

Можно доказать, что свойства выполняются для всех тактовых циклов с использованием индукционного доказательства. Однако это требует дополнительной работы по написанию свойств. Проблема в том, что пока мы только что написали несколько характеристики. Но для индукции нам нужно указать все свойств (или, по крайней мере, достаточно много). Это займет довольно много времени, поэтому вместо этого я расскажу об альтернативной стратегии повышения нашей уверенности.

Мутация

Итак, теперь мы описали некоторые свойства, которые axi_fifo модуль должен удовлетворять, и наш инструмент быстро подтверждает эти свойства, т. е. доказывает, что они удовлетворяются. Но у нас все еще может быть это тревожное чувство:уверены ли мы, что ошибок нет? Действительно ли мы выразили все свойства axi_fifo модуль?

Чтобы помочь ответить на эти вопросы и получить больше уверенности в полноте указанных свойств, мы можем применить технику, называемую мутацией. :Мы целенаправленно вносим небольшое изменение в реализацию, т.е. намеренно вносим баг, а потом смотрим, поймает ли формальная проверка баг!

Одним из таких изменений может быть удаление части логики, управляющей out_valid. сигнал. Например, мы могли бы закомментировать эти три строки:

Теперь, когда мы запускаем формальную проверку, мы получаем сообщение об ошибке

С помощью инструмента GTKwave мы можем просмотреть сопутствующую форму волны, и она выглядит следующим образом:

Здесь мы видим, что при 40 нс out_valid сигнал должен стать равным нулю, но это не так. Утверждение, которое не выполняется, находится на 50 нс, где out_valid остается высоким, но out_data изменения сигнала, указывающие на дублирование данных. Дублированные данные фактически не передавались в этой конкретной трассе, потому что out_ready составляет 40 нс, но формальная проверка тем не менее обнаруживает ошибку.

Сопроводительное заявление

Давайте, наконец, обратимся к другому применению формального инструмента проверки:заявлению об обложке. Цель оператора покрытия — проверить, существует ли последовательность входных данных, удовлетворяющая определенному свойству. Поскольку мы имеем дело с FIFO, давайте посмотрим, сможем ли мы заполнить его полностью, а затем снова опустошить. Это может быть выражено в одном операторе покрытия:

Это довольно много! Обратите внимание на точки с запятой внутри {}. . Для удобства чтения я разместил каждый раздел на отдельной строке. Это защитное заявление звучит следующим образом:Найдите последовательность входных данных, которая удовлетворяет:

Сброс выполняется в течение одного тактового цикла.
Затем может пройти любое количество тактовых циклов (когда сброс не установлен).
Один тактовый цикл, когда сброс не выполняется, а FIFO заполнен.
Затем может пройти любое количество тактовых циклов (когда сброс не установлен).
Один тактовый цикл, когда сброс не установлен, а буфер FIFO пуст.

Таким образом, синтаксис [*] означает повторение (ноль или более раз) предыдущего условия. В строке 3 мы могли бы удалить условие rst = '0' перед [*] . Результаты будут такими же. Причина в том, что формальный верификатор попытается найти самый короткий последовательность, которая удовлетворяет оператору покрытия, и подтверждение сброса при заполнении FIFO просто задержит это. Однако при очистке FIFO в строке 5 важно, чтобы сброс не выполнялся.

Чтобы запустить формальный верификатор сейчас, нам нужно внести небольшую модификацию в скрипт axi_fifo.sby. . Замените верхние разделы следующим:

Теперь решатель запустит BMC, а затем запустит анализ покрытия. В выводе вы увидите эти две строки:

Это означает, что оператор покрытия действительно может быть удовлетворен последовательностью из 15 тактовых циклов, и решатель сгенерировал форму сигнала специально для этого оператора покрытия:

Здесь мы видим, что на 80 нс FIFO заполнен и in_ready де-утвержден. А на 150 нс FIFO пуст и out_valid де-утвержден. Обратите внимание, как в течение периода от 30 нс до 80 нс out_ready держится низко. Это необходимо для обеспечения заполнения FIFO.

Если заменить условие count = ram_depth-1 с count = ram_depth , заявление покрытия не может быть выполнено. Затем инструмент сообщает об ошибке.

Таким образом, сообщение об ошибке содержит метку неудавшегося оператора покрытия. Это одна из причин, почему ярлыки так полезны! Мы интерпретируем приведенную выше ошибку как указание на то, что FIFO никогда не может содержать ram_depth. количество элементов. Это точно так, как указано в оригинальном сообщении в блоге AXI FIFO.

Что делать дальше

Учебник по языку PSL
Введение в формальную проверку
Серия небольших видеороликов, посвященных началу формальной проверки.
Блог, посвященный формальной проверке
Серия статей с более сложными темами формальной проверки.
Набор небольших примеров использования формальной проверки

Начало работы с VUnit Использование встроенного логического анализатора (ILA) и виртуального ввода/вывода (VIO)

VHDL