Освоение формальной верификации модулей VHDL с помощью PSL

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

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

Формальная верификация устраняет разрыв между требованиями и реализацией, доказывая, что каждая возможная последовательность входных сигналов удовлетворяет свойствам дизайна. Она незаменима для сертификации медицинских устройств, авионических систем или любой области, где требуется сертификация по стандарту DO‑254.

В этой гостевой статье Майкл Финн Йёргенсен — опытный практик формальной верификации — делится практическими инсайтами и готовыми к применению советами. Пример ниже основан на известном руководстве по AXI FIFO How to make an AXI FIFO in block RAM using the ready/valid handshake и демонстрирует, как применить PSL к реальному VHDL-дизайну.

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

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

Две основные техники ФВ:

Bounded Model Checking (BMC) — проверяет конечное число циклов, начиная с сброса.
Induction Proof (Доказательство индукцией) — верифицирует, что если состояние валидно, все последующие состояния остаются валидными. Требует полного набора свойств, но дает гарантии для бесконечного числа циклов.

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

Написание свойств на PSL

PSL (Property Specification Language) — лингва франка формальной верификации в VHDL. Свойства обычно хранятся в отдельном файле .psl, который решатель считывает на этапе верификации.

Три ключевых слова PSL описывают свойства:

assert — гарантирует, что условие всегда выполняется.
assume — задает предположения о входных сигналах.
cover — проверяет, может ли определенный сценарий когда-либо произойти.

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

Каждый PSL-файл начинается с блока vunit, связывающего файл с конкретной сущностью:

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) { }

Затем следует декларация тактового сигнала по умолчанию:

default clock is rising_edge(clk);

Синтаксис свойства выглядит так:

LABEL : assert always {PRECONDITION} |-> {POSTCONDITION}
LABEL : assume always {PRECONDITION} |-> {POSTCONDITION}

Используйте |=> для утверждений на следующем цикле:

LABEL : assert always {PRECONDITION} |=> {POSTCONDITION}

Внутри условий можно использовать stable для требования неизменности сигнала между циклами, а также цепочки условий с помощью {C1; C2} для выражения последовательных ограничений.

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

Коммерческие инструменты (например, ModelSim) поддерживают формальную верификацию, но бесплатная Student Edition не включает эту функцию. К счастью, существует надежный стек с открытым исходным кодом для Linux (и через WSL в Windows). Ниже приведена инструкция для Ubuntu 20.04 LTS, но она работает на любом современном Debian-based дистрибутиве.

Предварительные требования

sudo apt update && sudo apt upgrade

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

sudo apt install build-essential clang bison flex libreadline-dev \
gawk tcl-dev libffi-dev git mercurial graphviz \
xdot pkg-config python python3 libftdi-dev gperf \
libboost-program-options-dev autoconf libgmp-dev \
cmake gnat gtkwave

Yosys и SymbiYosys

git clone https://github.com/YosysHQ/yosys
cd yosys
make
sudo make install
cd ..
git clone https://github.com/YosysHQ/SymbiYosys
cd SymbiYosys
sudo make install
cd ..
git clone https://github.com/SRI-CSL/yices2
cd yices2
autoconf
./configure
make
sudo make install
cd ..

GHDL и плагин Yosys

git clone https://github.com/ghdl/ghdl
cd ghdl
./configure --prefix=/usr/local
make
sudo make install
cd ..
git clone https://github.com/ghdl/ghdl-yosys-plugin
cd ghdl-yosys-plugin
make
sudo make install
cd ..

Загрузка примера проекта

Заполните форму ниже, чтобы получить ZIP-архив с полным исходным кодом AXI FIFO, PSL-файлом и скриптами верификации.

Разбор примера: формальная верификация AXI FIFO

Ниже приведены ключевые категории свойств для FIFO и иллюстрация их кодирования на PSL.

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

f_reset : assume {rst};

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

f_after_reset_valid : assert always {rst} |=> {not out_valid};
f_after_reset_ready : assert always {rst} |=> {in_ready};
f_after_reset_head : assert always {rst} |=> {count = 0};

Обратите внимание: внутренние сигналы, такие как count, могут использоваться, так как декларация vunit включает имя архитектуры.

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

f_empty : assert always {count = 0} |-> {not out_valid};
f_full : assert always {count = ram_depth-1} |-> {not in_ready};

Соответствие протоколу AXI

f_in_data_stable : assume always {in_valid and not in_ready and not rst} |=> {stable(in_valid) and stable(in_data)};
f_out_data_stable : assert always {out_valid and not out_ready and not rst} |=> {stable(out_valid) and stable(out_data)};

Для стабильности сигнала ready:

f_out_ready_stable : assume always {out_ready and not out_valid and not rst} |=> {stable(out_ready)};
f_in_ready_stable : assert always {in_ready and not in_valid and not rst} |=> {stable(in_ready)};

Порядок FIFO

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

signal f_sampled_in_d1 : std_logic := '0';
signal f_sampled_in_d2 : std_logic := '0';
p_sampled : process (clk)
begin
  if rising_edge(clk) then
    if in_valid then
      if in_data = f_value_d1 then f_sampled_in_d1 <= '1'; end if;
      if in_data = f_value_d2 then f_sampled_in_d2 <= '1'; end if;
    end if;
    if out_valid then
      if out_data = f_value_d1 then f_sampled_out_d1 <= '1'; end if;
      if out_data = f_value_d2 then f_sampled_out_d2 <= '1'; end if;
    end if;
    if rst = '1' then
      f_sampled_in_d1 <= '0'; f_sampled_in_d2 <= '0';
      f_sampled_out_d1 <= '0'; f_sampled_out_d2 <= '0';
    end if;
  end if;
end process p_sampled;

Объявите значения данных как неограниченные константы, чтобы решатель мог выбрать любой битовый паттерн:

signal f_value_d1 : std_logic_vector(ram_width - 1 downto 0);
signal f_value_d2 : std_logic_vector(ram_width - 1 downto 0);
attribute anyconst : boolean;
attribute anyconst of f_value_d1 : signal is true;
attribute anyconst of f_value_d2 : signal is true;

Наконец, закодируйте ограничения порядка:

f_fifo_ordering_in : assume always {f_sampled_in_d2} |-> {f_sampled_in_d1};
f_fifo_ordering_out : assert always {f_sampled_out_d2} |-> {f_sampled_out_d1};

Запуск формальной верификации

Создайте скрипт axi_fifo.sby для инструмента sby:

[tasks]
bmc
[options]
bmc: mode bmc
bmc: depth 10
[engines]
smtbmc
[script]
ghdl --std=08 -gram_width=4 -gram_depth=8 axi_fifo.vhd axi_fifo.psl -e axi_fifo
prep -top axi_fifo
[files]
axi_fifo.psl
axi_fifo.vhd

Запустите верификацию:

sby --yosys ";yosys -m ghdl" -f axi_fifo.sby

Успешный запуск выводит:

[axi_fifo_bmc] DONE (PASS, rc=0)

Увеличение параметра depth сверх глубины FIFO обеспечивает исследование сценариев полной загрузки.

Мутационное тестирование

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

Пример сообщения об ошибке:

Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable

Откройте сгенерированный trace.vcd в GTKWave, чтобы точно определить цикл нарушения свойства.

Операторы cover

Операторы cover полезны для проверки достижимости сценария. Например, чтобы убедиться, что FIFO может быть заполнен и затем опустошен:

f_full_to_empty : cover { rst = '1'; rst = '0'[*]; rst = '0' and count = ram_depth-1; rst = '0'[*]; rst = '0' and count = 0};

Добавьте задачу cover в скрипт sby:

[tasks]
bmc cover
[options]
bmc: mode bmc
bmc: depth 10
cover: mode cover

Успешное покрытие дает:

Reached cover statement at i_axi_fifo.f_full_to_empty in step 15.

Замена count = ram_depth-1 на count = ram_depth сделает cover недостижимым, демонстрируя чувствительность инструмента к точности свойств.

Дальнейшие шаги

VUnit 101: Практическое руководство по автоматизированной VHDL-верификации Освоение Xilinx Vivado: Integrated Logic Analyzer (ILA) и Virtual Input/Output (VIO) для отладки

VHDL