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

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

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

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

Коммерческие инструменты для формальной верификации дизайна аппаратуры существуют уже несколько десятилетий, но простой в использовании альтернативы с открытым исходным кодом, которая могла бы загружать проект на языке Verilog с заданными формальными ограничениями, не было до выхода SymbiYosys^[1].

Инструменты и определения

SymbiYosys (SBY) — фронтенд автоматизации верификации. Читает конфигурационные файлы (.sby), управляет запуском Yosys и передает сформированные уравнения вычислительным движкам (SMT/SAT-солверам). Yosys в свою очередь транслирует код Verilog/SystemVerilog во внутреннее представление, преобразуя логику в математические форматы.

В основе анализа лежит задача выполняемости булевых формул (SAT, Satisfiability). Это математическая задача определения того, существует ли такой набор значений для логических переменных, при котором вся заданная булева формула принимает значение «истина».

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

SMT (Satisfiability Modulo Theories) — расширение SAT, которое позволяет решать уравнения не только на уровне отдельных бит, но и с использованием более сложных конструкций, таких как битовые векторы или массивы. Именно формат SMT2 является стандартным входным языком для большинства современных солверов.

Инструмент верификации может использовать различные внешние программы-решатели. В нашем случае применяется встроенный движок-транслятор smtbmc, вызывающий внешний решатель z3. Подробнее про другие возможные движки и солверы можно прочитать в документации SymbiYosys.

Все инструменты должны быть доступны после установки OSS CAD Suite.

Операторы верификации

Для описания ограничений и проверок используются три оператора:

assume(выражение); задает ограничения на входные сигналы. Солвер рассматривает только те сценарии, в которых данное выражение истинно. Без явных ограничений инструмент может подать на входы недопустимые спецификацией значения.
assert(выражение); определяет целевое правило для проверки. Солвер ищет условия, нарушающие данное утверждение.
cover(выражение); проверяет достижимость определенного состояния логики. Инструмент ищет хотя бы один набор значений сигналов, делающий выражение истинным.

Операторы верификации являются процедурными. Они должны находиться внутри процедурного контекста, например always или initial.

Для интеграции верификации в комбинационный модуль логика проверок изолируется макросом `ifdef FORMAL.

Разберём пример с уже известным нам сумматором:

src/02-combination-logic/formal-verification/adder_1_bit_fv.sv

module adder_1_bit_fv (
    input  logic a,
    input  logic b,
    input  logic c_in,
    output logic c_out,
    output logic sum
);

  assign sum   = a ^ b ^ c_in;
  assign c_out = (a & b) | (c_in & (a ^ b));  (1)

`ifdef FORMAL
  always @* begin
    assert ({c_out, sum} == (a + b + c_in));  (2)
    cover (c_in == 1'b1 && sum == 1'b0);  (3)
  end
`endif
endmodule

1	Логика исходного модуля-сумматора.
2	Команда солверу убедиться в том, что данное условие выполняется всегда.
3	Команда солверу вывести набор значений, когда выполняется данное условие.

Настройка конфигурации

Управление процессом SymbiYosys происходит через конфигурационный файл .sby. Файл разбит на секции:

[options]: режим работы и параметры анализа;
[engines]: используемые движки и солверы с опциями;
[script] : команды Yosys для чтения и подготовки топ-модуля;
[files] : исходные файлы модулей.

Секция [options] поддерживает три основных режима работы:

bmc (Bounded Model Checking) проверяет выполнение assert от начального состояния схемы на фиксированную глубину шагов. Для комбинационной логики устанавливается depth 1.
cover использует тот же алгоритм BMC, но переключает фокус солвера на поиск цепочки сигналов, удовлетворяющей условиям операторов cover. В данном режиме получить статус FAIL возможно в двух случаях: целевое состояние недостижимо, либо для его достижения солверу придется нарушить любой из заданных assert.
prove выполняет проверку BMC, а затем пытается построить неограниченное доказательство методом математической индукции (k-induction). Если режим завершается успешно, схема гарантированно работает корректно на любом временном интервале.

Так выглядит конфигурационный файл для нашего сумматора в режиме bmc:

src/02-combination-logic/formal-verification/adder_1_bit.sby

[options]
mode bmc
depth 1

[engines]
smtbmc z3

[script]
read -sv -formal adder_1_bit_fv.sv
prep -top adder_1_bit_fv

[files]
adder_1_bit_fv.sv

В процессе работы SymbiYosys создается папку (по умолчанию с именем файла конфигурации), организуя промежуточные файлы и результаты следующим образом:

src/: копии исходных файлов.
model/: результаты трансформации кода в математическую модель. Yosys вызывается неоднократно, сохраняя промежуточные представления. Последней командой SBY вызывает yosys-smtbmc, передавая ему тип солвера (z3) и код формата SMT2.
engine_N/: для каждого солвера, указанного в секции [engines], создается своя папка. В ней лежат результаты работы математического движка (если в режиме bmc/prove нет контрпримера, то создаются только файлы логов):
- trace.vcd: файл данных трассы. В режиме bmc/prove это контрпример, показывающий, как именно сломался assert. В режиме cover — пример трассы, достигающей нужного состояния.
- trace_induct.vcd (только для prove): трасса нарушения свойства на шаге индукции.
- trace_tb.v: Verilog-тестбенч, воспроизводящий трассу.
- trace.smtc: математическое описание трассы.
Остальные файлы содержат логи и исходную конфигурацию.

Сгенерированный файл design_smt2.smt2 содержит только определения функций, в нем отсутствуют обязательные команды инициализации set-logic и финальные директивы assert или check-sat^[2]. Эти конструкции дописываются динамически в процессе передачи уравнений на стандартный вход SMT-солвера.

Со стандартом формата SMT2 можно ознакомиться здесь. Коротко: формат представления функций — (define-fun |имя| (<аргументы>) <тип_возвращаемого_значения> <тело>).

Посмотрим на математическое представление некоторых строк нашего примера (для удобства отформатированные ручным способом).

(define-fun |adder_1_bit_fv#6|
  ((state |adder_1_bit_fv_s|)) (_ BitVec 1)
  (bvor
    (|adder_1_bit_fv#3| state)
    (|adder_1_bit_fv#5| state)
  )
) ; \c_out  (1)

(define-fun |adder_1_bit_fv#10|
  ((state |adder_1_bit_fv_s|)) Bool
  (=
    (concat
      (|adder_1_bit_fv#6| state)
      (|adder_1_bit_fv#7| state)
    )
    (|adder_1_bit_fv#9| state)
  )
) ; $eq$adder_1_bit_fv.sv:14$11_Y  (2)
; yosys-smt2-assert 0 _witness_.check_assert_adder_1_bit_fv_sv_14_8 adder_1_bit_fv.sv:14.5-14.44  (3)

(define-fun |adder_1_bit_fv_a 0|
  ((state |adder_1_bit_fv_s|)) Bool
  (or
    (|adder_1_bit_fv#10| state)
    (not true)
  )
) ; _witness_.check_assert_adder_1_bit_fv_sv_14_8  (4)

(define-fun |adder_1_bit_fv_a|
  ((state |adder_1_bit_fv_s|)) Bool
  (|adder_1_bit_fv_a 0| state)
) ;  (5)

(define-fun |adder_1_bit_fv_u|
  ((state |adder_1_bit_fv_s|)) Bool
  true
) ;  (6)

1	Провод `c_out` мапится на внутреннюю функцию `\|adder_1_bit_fv#6\|`. Логическое выражение преобразуется в префиксную операцию «побитового ИЛИ» (`bvor`) над результатами функций `#3` (`a & b`) и `#5` (`c_in & (a ^ b)`). Функция помечается соответствующим комментарием.
2	Оператор `concat` объединяет однобитные значения сигналов `c_out` (`#6`) и `sum` (`#7`) в двухбитный вектор для сравнения со значением функции `#9`, представляющей собой результат арифметического сложения `a + b + c_in`.
3	Служебный комментарий с точными координатами в SystemVerilog-файле (строка 14, символы с 5 по 44 — строка, содержащая `assert`).
4	Функция-обертка для `#10` с проверкой ограничений (в нашем случае `assume` нет).
5	Финальная функция собирает все ассерты модуля. Задача солвера — доказать, что не существует состояния `state`, при котором она вернет `false`.
6	Функция ограничений на входные данные (в нашем случае ограничений нет, поэтому всегда возвращает `true`).

Получение результата

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

sby adder_1_bit.sby

Инструмент выдаст статус PASS, подтвердив выполнение assert для всех 8 входных комбинаций. Чтобы увидеть результат оператора cover, требуется изменить режим bmc на cover.

Представим, что мы совершили ошибку при написании сумматора:

assign c_out = (a & b) | (c_in | (a ^ b));

При повторном запуске sby -f adder_1_bit.sby солвер Z3 найдет ситуацию, опровергающую assert условие. Процесс завершится со статусом FAIL и создадутся файлы с трассой. Так как для комбинационной логики используется depth 1, то для просмотра контрпримера достаточно файла trace.smtc:

initial  (1)

state 0  (2)
assume (= [a] false)  (3)
assume (= [b] true)  (3)
assume (= [c_in] false)  (3)

1	Метка начальной точки трассы.
2	Обозначение первого шага (такта) проверки.
3	Конкретные значения на входах схемы, при которых произошел сбой (контрпример).

Таким образом, солвер определил, что при входной комбинации (0,1,0) результаты выходов не совпадают с эталоном. Посмотрим на наш отредактированный c_out: (0 & 1) | (0 | (0 ^ 1)) = 1, а ожидалось 0.

Обязательно пройдите упражнения.

1. https://tomverbeure.github.io/rtl/2019/01/04/Under-the-Hood-of-Formal-Verification.html

2. https://yosyshq.readthedocs.io/projects/yosys/en/0.40/cmd/write_smt2.html