Формальная верификация «для бедных»: выбираем open source-решение / Хабр

Как убедиться, что в аппаратном дизайне нет багов? Результаты обычных тестов иногда сигнализируют только о том, что ошибки не нашлись, а не о том, что их нет вовсе. На помощь приходит формальная верификация — метод, который проверяет все состояния системы в поисках ошибки. Для промышленной верификации есть три решения: VC Formal от Synopsys, JasperGold от Cadence и коммерческая часть Yosys. Проприетарные инструменты проверены «в бою», но доступны далеко не всем.

Меня зовут Борис Новосёлов, я младший инженер по верификации в YADRO, и я изучил альтернативы с открытым исходным кодом: CIRCT, Slang, Synlig и другие. Вы узнаете, как работают эти инструменты и на что обратить внимание при выборе решения для своего проекта.

Как работает верификация

Как правило, для верификации строится референсная модель. Модель может сделать заранее другой инженер — это сокращает сроки верификации. А сама процедура проверки будет максимально простой: один вход на RTL и модель, ожидаем одинаковый выход, если его нет, то произошла ошибка. Есть два базовых формальных подхода для доказательства эквивалентности двух дизайнов:

Equivalence Checking — полная проверка эквивалентности, сравнение выходных результатов на полном спектре возможных входных данных.
Ограниченная проверка с помощью assert и assume.

Оба подхода работают на одних и тех же принципах доказательств, главные из них — Bounded Model Checking и k-Induction. Рассмотрим их подробнее.

Bounded Model Checking (BMC)

Bounded Model Checking — самый простой способ найти баг. Идея в том, чтобы развернуть состояния дизайна на ограниченное число тактов. Конечно, это не даст прямого доказательства ошибки, но эффективно в их поиске.

BMC проверит все состояния на заданное число шагов

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

Тогда функция перехода — это .

BMC строит формулу такого вида:

$Init(s_0) \land T(s_0, i_0, s_1) \land T(s_1, i_1, s_2) \land \dots \land T(s_{k-1}, i_{k-1}, s_k)$

Это просто модель всех возможных трасс длины , но можно выразить лаконичнее:

$Init(s_0) \wedge \bigwedge_{t=0}^{k-1} T(s_t, i_t, s_{t+1})$

Теперь в дело вступает SAT-solver, он пытается отыскать состояние, при котором заданный предикат не выполняется:

$\Phi_{\text{BMC}} = Init(s_0) \wedge \bigwedge_{t=0}^{k-1} T(s_t, i_t, s_{t+1}) \wedge \bigvee_{t=0}^{k} \neg P(s_t)$

На этом все и заканчивается. Множество систем просто невозможно доказать формально автоматическими средствами из-за экспоненциального роста состояний, так что этот метод подойдет, если вы согласны на компромисс.

k-Induction

И все же мы стремимся к совершенству. Как вообще доказать эквивалентность на бесчисленном множестве тактов. Нельзя же раскладывать состояния бесконечное число раз?

Можно воспользоваться индукцией, однако обычная индукция не учитывает временной контекст, иначе говоря, считается одношаговой . Индукция ничего не знает про достижимость, так что вполне вероятна ситуация, при которой найдется $P(s) \land \neg P(T(s))$ для недостижимого состояния из заданного .

k-Induction ослабляет индуктивное предположение и пытается доказать корректность свойства, если оно удовлетворяет k-шагов подряд.

BMC может выступать в качестве базы для такой индукции:

$\Phi_{\text{Base}} = Init(s_0) \wedge \bigwedge_{t=0}^{k-1} T(s_t, i_t, s_{t+1}) \wedge \bigvee_{t=0}^{k-1} \neg P(s_t)$

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

$\Phi_{\text{Step}} = \left( \bigwedge_{t=0}^{k-1} P(s_t) \right) \wedge \left( \bigwedge_{t=0}^{k-1} T(s_t, i_t, s_{t+1}) \right) \wedge \neg P(s_k)$

Узнать больше можно в статьях "Bounded Model Checking", "Checking safety properties using induction and a SAT-solver".

Чем заменить промышленное решение: выбираем open source-инструмент

Итак, мы разобрались, как устроена формальная верификация в теории, и знаем, что коммерческие инструменты справляются с задачей успешно. Теперь попробуем найти решение в мире open source, которое могло бы заменить проприетарные инструменты — на случай, если платные решения вам недоступны. Хороший open source-инструмент должен «прожевать» дизайн и исполнить хотя бы ограниченную проверку с помощью заданных assert и assume.

Yosys и SymbiYosys

Yosys — это, пожалуй, самый знаменитый open source-фреймворк. На самом деле это фронтенд над библиотекой Berkley ABC для синтеза RTL. Для него есть фронтенд формальной верификации SymbiYosys (sby), который использует SMT-solver Z3.

Структура SMT-LIB2 файлов

Yosys преобразует Verilog/SystemVerilog-код в SMT-LIB2-формат для формальной верификации. Рассмотрим процесс на примере D-триггера с assert:

module dff(input clk, input d, output reg q);
always @(posedge clk)
q <= d;

always @(posedge clk) begin
assert property (q == d);
end
endmodule

Тип состояния схемы

(declare-sort |dff_s| 0)
(declare-fun |dff_is| (|dff_s|) Bool)

dff_s — абстрактный тип состояния (моментальный снимок всех регистров);
dff_is — предикат инициализации (проверяет корректность начального состояния).

Регистры схемы

Yosys создает шесть внутренних регистров для моделирования последовательной логики:

; Основные регистры DFF
 (declare-fun |dff#0| (|dff_s|) (_ BitVec 1))  ; clk#sampled (основной)
 (declare-fun |dff#1| (|dff_s|) (_ BitVec 1))  ; d#sampled (данные)
 (declare-fun |dff#2| (|dff_s|) (_ BitVec 1))  ; q#sampled (выход)

; Регистры для assert 
 (declare-fun |dff#3| (|dff_s|) (_ BitVec 1))  ; assert#sampled (q==d)
 (declare-fun |dff#4| (|dff_s|) (_ BitVec 1))  ; 1'1#sampled (константа true)
 (declare-fun |dff#5| (|dff_s|) (_ BitVec 1))  ; clk#sampled (для assert)

; Вообще dff#0 и dff#5 можно было бы слить в один регистр, но Yosys такие оптимизации не делает похоже

Функции доступа (BitVec → Bool):

; Конвертация BitVec в Bool
 (define-fun |dff_n clk_sampled| ((state |dff_s|)) Bool
 (= ((_ extract 0 0) (|dff#0| state)) #b1))

; я опустил ряд подобных функций

Входы схемы

; Входы схемы (не сохраняются между тактами)
 (declare-fun |dff#6| (|dff_s|) Bool)  ; clk (текущий)
 (declare-fun |dff#7| (|dff_s|) Bool)  ; d (текущий)

; Функции доступа к входам
 (define-fun |dff_n clk| ((state |dff_s|)) Bool (|dff#6| state))
 (define-fun |dff_n d| ((state |dff_s|)) Bool (|dff#7| state))

Комбинаторная логика и выходы

Эта функция моделирует переход тактового сигнала из 0 в 1 и в обратную сторону:

(define-fun |dff#8| ((state |dff_s|)) Bool
 (= (concat (|dff#0| state) (ite (|dff#6| state) #b1 #b0)) #b01))

Логика выхода DFF, если фронт clk → q = d, иначе q = q:

(define-fun |dff#9| ((state |dff_s|)) (_ BitVec 1)
(ite (|dff#8| state) (|dff#1| state) (|dff#2| state)))
(define-fun |dff_n q| ((state |dff_s|)) Bool
(= ((_ extract 0 0) (|dff#9| state)) #b1))

Временная логика для assert:

; Детектор фронта для assert
(define-fun |dff#10| ((state |dff_s|)) Bool (= (concat (|dff#5| state) (ite (|dff#6| state) #b1 #b0)) #b01))
; Логика OR
(define-fun |dff#11| ((state |dff_s|)) Bool
(or (|dff#10| state) false))
; Генератор импульса для assert
; Создает импульс длительностью в один такт на фронте clk для assert (define-fun |dff#12| ((state |dff_s|)) (_ BitVec 1)
(bvand (|dff#4| state) (ite (|dff#11| state) #b1 #b0)))

Assert-функции

Проверка условия assert (q == d, основное условие):

(define-fun |dff#13| ((state |dff_s|)) Bool
 (= (|dff#9| state) (ite (|dff#7| state) #b1 #b0)))

Основная функция проверки:

(define-fun |dff_a 0| ((state |dff_s|)) Bool
 (or (= ((_ extract 0 0) (|dff#3| state)) #b1)
 (not (= ((_ extract 0 0) (|dff#12| state)) #b1))))

(define-fun |dff_a| ((state |dff_s|)) Bool
 (|dff_a 0| state))

FSM-функции

Инициализация состояния:

(define-fun |dff_i| ((state |dff_s|)) Bool (and
 (= (= ((_ extract 0 0) (|dff#0| state)) #b1) true)   ; clk#sampled = 1
 (= (= ((_ extract 0 0) (|dff#1| state)) #b1) false)  ; d#sampled = 0
 (= (= ((_ extract 0 0) (|dff#3| state)) #b1) true)   ; assert#sampled = 1
 (= (= ((_ extract 0 0) (|dff#4| state)) #b1) false)  ; 1'1#sampled = 0
 (= (= ((_ extract 0 0) (|dff#5| state)) #b1) true)   ; clk#sampled = 1
 ))

Переходная функция (state → next_state):

(define-fun |dff_t| ((state |dff_s|) (next_state |dff_s|)) Bool (and
 ; Обновление clk#sampled для assert
 (= (ite (|dff#6| state) #b1 #b0) (|dff#5| next_state))

; Константа 1'1
 (= #b1 (|dff#4| next_state))

; Обновление assert#sampled (q==d)
 (= (ite (|dff#13| state) #b1 #b0) (|dff#3| next_state))

; Обновление q#sampled (новое значение q)
 (= (|dff#9| state) (|dff#2| next_state))

; Обновление d#sampled (сохранение d)
 (= (ite (|dff#7| state) #b1 #b0) (|dff#1| next_state))

; Обновление clk#sampled (основной)
 (= (ite (|dff#6| state) #b1 #b0) (|dff#0| next_state))
 ))

Служебные функции:

(define-fun |dff_u| ((state |dff_s|)) Bool true)  ; assume условия
(define-fun |dff_h| ((state |dff_s|)) Bool true)  ; hold условия

В итоге работу FSM можно изобразить следующим образом:

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

Теперь можно запустить артефакт в Z3.

Запуск SMT-LIB2

user@station ~/v/s/build> z3 -smt2 dff.smt2 -st
 (:max-memory   17.08
 :memory   	17.08
 :num-allocs   10644
 :rlimit-count 503
 :total-time   0.00**)**

Хм, Z3 не видит assert, потому что Yosys оборачивает их в dff_a.

Можно запустить с оберткой от sby:

user@station ~/v/s/build [1]> yosys-smtbmc -s z3 dff.smt2
 ##   0:00:00  Solver: z3
 ##   0:00:00  Checking assertions in step 0..
 ##   0:00:00  Checking assertions in step 1..
 ##   0:00:00  BMC failed!
 ##   0:00:00  Assert failed in dff: designs/dff.sv:7.5-7.29 (designs/dff.sv:7$3)
 ##   0:00:00  Status: FAILED

Сработало! Конечно, проверка упала, однако нас интересует сама возможность такой проверки. Но что такого сделала обертка, чего не получилось сделать с чистым SMT-solver?

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

user@station ~/v/s/build [1]> yosys-smtbmc -s z3 -m dff -t 5 --dump-smt2 unrolled.smt2 dff.smt2
 ##   0:00:00  Solver: z3
 ##   0:00:00  Checking assertions in step 0..
 ##   0:00:00  Checking assertions in step 1..
 ##   0:00:00  BMC failed!
 ##   0:00:00  Assert failed in dff: designs/dff.sv:7.5-7.29 (designs/dff.sv:7$3)
 ##   0:00:00  Status: FAILED

user@station ~/v/s/build [1]> z3 -smt2 unrolled.smt2
 unsat
 sat
 (((|dff_a| s1) false**))**
 (((|dff_a 0| s1) false**))**

Несмотря на то что Yosys производит нужный результат, его фронтенд оставляет желать лучшего. Например, у меня не получилось собрать сколько-нибудь сложный проект в виде ядра scr1. Кроме этого, команда Yosys принципиально не добавляет обработку сложных SVA-конструкций в некоммерческую часть, так что ждать обновлений бессмысленно. Продолжим поиски.

CIRCT

CIRCT — это новинка, пока что, исключительно исследовательский проект, цель которого можно описать как LLVM для аппаратного описания. Можно написать свой HDL, подвязать его к диалекту MLIR, и это будет работать. Уже сейчас есть поддержка Chisel, Python, SV/VHDL.

Похоже, что CIRCT получит более широкую поддержку со стороны сообщества, чем Yosys, благодаря эгиде LLVM и всем преимуществам использования продуманного IR.

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

HW Dialect — конструкции этого диалекта описывают определение модулей, констант, входов и выходов, а также массивов.
Comb Dialect — содержит в себе операции для комбинационной логики без состояния. Такими операциями могут быть логические, арифметические, сравнения и мультиплексоры.
Moore Dialect — высокоуровневое представление SystemVerilog после парсинга, выступает базой для последующего деления на диалекты.
SV Dialect — представление для генерации SystemVerilog-кода, благодаря этому диалекту можно конвертировать новые HDL в то, что реально можно запустить.
LLHD Dialect — детальное представление аппаратуры для симуляции и синтеза, поддерживает временные характеристики, моделирует задержки.
SMT Dialect — представление для SMT-решателей и формальной верификации, то, что искали, выражает битовые векторы, условные выражения, проверки на равенство и массивы.

Тяжбы конвертаций

Это не совсем очевидно, однако по дефолту CIRCT не собирается со Slang (фронтендом для SV). А еще могут не подхватиться пути до Z3, так что я на всякий случай явно укажу команду сборки, поскольку потратил на это несколько часов:

cmake -G Ninja llvm/llvm -B build \
  	-DCMAKE_BUILD_TYPE=RelWithDebInfo \
  	-DLLVM_ENABLE_ASSERTIONS=ON \
  	-DLLVM_TARGETS_TO_BUILD=host \
  	-DLLVM_ENABLE_PROJECTS=mlir \
  	-DLLVM_EXTERNAL_PROJECTS=circt \
  	-DLLVM_EXTERNAL_CIRCT_SOURCE_DIR=$PWD \
  	-DCIRCT_SLANG_FRONTEND_ENABLED=ON \
  	-DZ3_DIR=/usr/lib/cmake/z3 \
  	-DLLVM_ENABLE_Z3_SOLVER=ON \
  	-DLLVM_ENABLE_LLD=ON \
  	-DLLVM_USE_SPLIT_DWARF=ON

Вообще, я был настроен оптимистично, так что решил загнать целый АЛУ для проверки:

module alu (
	input  logic [3:0]  a,
	input  logic [3:0]  b,
	input  logic [1:0]  op,
	output logic [3:0]  result,
	output logic    	zero
);

	// ALU operations
	typedef enum logic [1:0] {
    	ADD = 2'b00,
    	SUB = 2'b01,
    	AND = 2'b10,
    	OR  = 2'b11
	} op_t;
   
	logic [3:0] sum, diff, and_result, or_result;
   
	// Combinational logic
	assign sum = a + b;
	assign diff = a - b;
	assign and_result = a & b;
	assign or_result = a | b;
   
	// Result selection
	always_comb begin
    	case (op)
        	ADD: result = sum;
        	SUB: result = diff;
        	AND: result = and_result;
        	OR:  result = or_result;
        	default: result = 4'b0;
    	endcase
	end
   
	// Zero flag
	assign zero = (result == 4'b0);

	assert property (op == ADD && result == a + b);

endmodule

Такой вот можно получить hw после circt-verilog --ir-hw alu.sv:

module {
 hw.module (in %a : i4, in %b : i4, in %op : i2, out result : i4, out zero : i1) {
 %true = hw.constant true
 %c0_i4 = hw.constant 0 : i4
 %c-2_i2 = hw.constant -2 : i2
 %c1_i2 = hw.constant 1 : i2
 %c0_i2 = hw.constant 0 : i2
 %0 = comb.add %a, %b : i4
 %1 = comb.sub %a, %b : i4
 %2 = comb.and %a, %b : i4
 %3 = comb.or %a, %b : i4
 %4 = comb.icmp ceq %op, %c0_i2 : i2
 %5 = comb.icmp ceq %op, %c1_i2 : i2
 %6 = comb.icmp ceq %op, %c-2_i2 : i2
 %7 = comb.mux %6, %2, %3 : i4
 %8 = comb.xor %4, %true : i1
 %9 = comb.and %8, %5 : i1
 %10 = comb.mux %9, %1, %7 : i4
 %11 = comb.mux %4, %0, %10 : i4
 %12 = comb.icmp eq %11, %c0_i4 : i4
 llhd.process {
 cf.br ^bb1
 ^bb1:  // 2 preds: ^bb0, ^bb1
 %13 = comb.icmp eq %op, %c0_i2 : i2
 %14 = comb.icmp eq %11, %0 : i4
 %15 = comb.and %13, %14 : i1
 verif.assert %15 : i1
 cf.br ^bb1
 }
 hw.output %11, %12 : i4, i1
 }
 }

circt-verilog — это специальный бинарь, генерируемый при сборке. Документацию на него можно найти только в разделе help самой утилиты, так что я даже и не подразумевал, что придется оперировать инструментами, которые непонятно как друг с другом сочетать.

Все вроде отлично, даже диалект verif четко указывает на присутствие assert, однако при попытке конвертации файла происходит следующее:

user@station ~/s/test_designs (master) [1]> circt-opt --convert-hw-to-smt ./tmp/alu.hw.mlir
 ./tmp/alu.hw.mlir:21:5: error: 'llhd.process' op expects parent op 'hw.module'
 llhd.process {
 ^
 ./tmp/alu.hw.mlir:21:5: note: see current operation:
 "llhd.process"() ({
 "cf.br"()[^bb1] : () -> ()
 ^bb1:  // 2 preds: ^bb0, ^bb1
 %28 = "comb.icmp"(%0, %12**)** <{predicate = 0 : i64}> : (i2, i2) -> i1
 %29 = "comb.icmp"(%24, %13**)** <{predicate = 0 : i64}> : (i4, i4) -> i1
 %30 = "comb.and"(%28, %29**)** : (i1, i1) -> i1
 "verif.assert"(%30**)** : (i1) -> ()
 "cf.br"()[^bb1] : () -> ()
 }) : () -> ()

circt-opt не может прожевать диалект llhd, который идет исключительно в комплекте с assert, если удалить assert, то получим файл MLIR с SMT-диалектом, то есть не сам .smt2:

module {
 func.func (%arg0: !smt.bv<4>, %arg1: !smt.bv<4>, %arg2: !smt.bv<2>) -> (!smt.bv<4>, !smt.bv<1>) {
 %0 = builtin.unrealized_conversion_cast %arg2 : !smt.bv<2> to i2
 %1 = builtin.unrealized_conversion_cast %arg1 : !smt.bv<4> to i4
 %2 = builtin.unrealized_conversion_cast %arg0 : !smt.bv<4> to i4
 %c-1_bv1 = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
 %3 = builtin.unrealized_conversion_cast %c-1_bv1 : !smt.bv<1> to i1
 %c0_bv4 = smt.bv.constant #smt.bv<0> : !smt.bv<4>
 %4 = builtin.unrealized_conversion_cast %c0_bv4 : !smt.bv<4> to i4
 %c-2_bv2 = smt.bv.constant #smt.bv<-2> : !smt.bv<2>
 %5 = builtin.unrealized_conversion_cast %c-2_bv2 : !smt.bv<2> to i2
 %c1_bv2 = smt.bv.constant #smt.bv<1> : !smt.bv<2>
 %6 = builtin.unrealized_conversion_cast %c1_bv2 : !smt.bv<2> to i2
 %c0_bv2 = smt.bv.constant #smt.bv<0> : !smt.bv<2>
 %7 = builtin.unrealized_conversion_cast %c0_bv2 : !smt.bv<2> to i2
 %8 = comb.add %2, %1 : i4
 %9 = comb.sub %2, %1 : i4
 %10 = comb.and %2, %1 : i4
 %11 = comb.or %2, %1 : i4
 %12 = comb.icmp ceq %0, %7 : i2
 %13 = comb.icmp ceq %0, %6 : i2
 %14 = comb.icmp ceq %0, %5 : i2
 %15 = comb.mux %14, %10, %11 : i4
 %16 = comb.xor %12, %3 : i1
 %17 = comb.and %16, %13 : i1
 %18 = comb.mux %17, %9, %15 : i4
 %19 = comb.mux %12, %8, %18 : i4
 %20 = builtin.unrealized_conversion_cast %19 : i4 to !smt.bv<4>
 %21 = comb.icmp eq %19, %4 : i4
 %22 = builtin.unrealized_conversion_cast %21 : i1 to !smt.bv<1>
 return %20, %22 : !smt.bv<4>, !smt.bv<1>
 }
 }

Что делать дальше с smt.mlir-файлом, я так и не понял… Но у нас есть ведь еще бинарник circt-bmc, который должен принимать на вход hw-диалект!

user@station ~/s/test_designs (master) [1]> circt-bmc tmp/alu.hw.mlir -b 100 --module=alu
 tmp/alu.hw.mlir:21:5: error: Dialect `llhd' not found for custom op 'llhd.process'
 llhd.process {
 ^
 tmp/alu.hw.mlir:21:5: note: Available dialects: arith, builtin, comb, emit, func, hw, llvm, om, seq, smt, verif ; for more info on dialect registration see https://mlir.llvm.org/getting_started/Faq/#registered-loaded-dependent-whats-up-with-dialects-management

llhd все еще не воспринимает. Попробуем без assert:

user@station ~/s/test_designs (master) [1]> circt-bmc tmp/alu_simple.hw.mlir -b 100 --module=alu_simple
 tmp/alu_simple.hw.mlir:2:3: error: no property provided to check in module
 hw.module **(in** %a : i4, in %b : i4, in %op : i2, out result : i4, out zero : i1**)** {
 ^

Как бы я ни пытался обработать hw.mlir с помощью существующих бинарников, у меня это не получилось, зато если отредактировать его руками, удалив упоминание llhd:

module {
hw.module @alu_simple(in %a : i4, in %b : i4, in %op : i2, out result : i4, out zero : i1) {
%true = hw.constant true
%c0_i4 = hw.constant 0 :
%c-2_i2 = hw.constant -2
%c1_i2 = hw.constant 1 :
%c0_i2 = hw.constant 0 :
%0 = comb.add %a, %b : i4
%1 = comb.sub %a, %b : i4
%2 = comb.and %a, %b : i4
%3 = comb.or %a, %b : i4
%4 = comb.icmp eq %op, %c0_i2 : i2 %5 = comb.icmp eq %op, %c1_i2 : i2 %6 = comb.icmp eq %op, %c-2_i2 : i2 %7 = comb.mux %6, %2, %3 : i4
%8 = comb.xor %4, %true : i1
%9 = comb.and %8, %5 : i1
%10 = comb.mux %9, %1, %7 : i4
%11 = comb.mux %4, %0, %10 : i4
%12 = comb.icmp eq %11, %c0_i4 : i4
// Assert: op == ADD && result == a + b
%is_add = comb.icmp eq %op, %c0_i2 : i2
%expected_result = comb.add %a, %b : i4
%result_correct = comb.icmp eq %11, %expected_result : i4 %assert_condition = comb.and %is_add, %result_correct : i1 verif.assert %assert_condition : i1
hw.output %11, %12 : i4, i1 }
}

Получим заветный результат:

user@station ~/v/s/tmp [1]> circt-bmc alu_simple.hw.mlir -b 100 --module=alu_simple
Assertion can be violated!

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

Если коротко, решение сырое: нет поддержки формалки для последовательной логики, проблемы с парсингом результата из Slang, то есть единственного фронтенда для SV, из-за чего и появляются проблемы с llhd.

Мы разговорились с авторами треда про поддержку последовательной логики. На мое предложение реализовать представление как в Yosys, через функцию перехода, отозвались положительно, даже предоставили конкретные начальные шаги. Интересно, будут ли продолжать работу в этом направлении?

Slang

Slang можно приделать не только к CIRCT, но и к Yosys, для этого даже существует специальный плагин.

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

[script]
 # load slang plugin
 plugin -i /usr/share/yosys/plugins/slang.so

# ...

cmd = f"read_slang -Wno-invalid-source-encoding -DNO_FULL_SKIP=1 -DSCR1_RVM_EXT -DFORMAL"
 for inc_dir in include_dirs:
 cmd += f" -I{inc_dir}"
 cmd += f" {' '.join(files)}"

Получилось собрать ядро scr1, что по меркам открытого ПО настоящее достижение! Однако моя обертка, содержащая SVA, так и падала. Оказалось, что поддержка SVA в плагине — неприоритетная задача.

Судя по всему, Slang способен парсить сложные SVA, но ни у кого не доходят руки связать этот результат с Yosys IR.

Synlig

У меня оставалась надежда на репозиторий, в котором последний коммит был целых два года назад.

Synlig, как и Slang поставляется в двух видах: бинарник и плагин для Yosys. В репозитории указано, что плагин вторичен по отношению к бинарнику и поддерживается постольку-поскольку, поэтому я решил использовать центральный инструмент.

Synlig использует Slang как парсер, и у его бинарника есть много функций для обработки полученного (чувствуются отголоски работы с CIRCT). Бэкендом по-прежнему выступает Yosys.

Я написал примитивный счетчик и положил на него несколько SVA-конструкций. Затем запустил подобный скрипт, который подавался на вход бинарнику Synlig:

read_systemverilog   -defer simple_design/counter.sv
 read_systemverilog   -defer simple_design/wrapper.sv

read_systemverilog -link

proc

sim -clock clk -resetn rst_n -assert wrapper

prep -top counter
sat -prove-asserts counter

Он распарсил все и сказал, что мои SVA — это несинтезируемые конструкции. То есть не просто пропустил эту часть за ненадобностью, а выдал полезную информацию. С помощью команды sim я просимулировал свой дизайн, наконец дошел до команды sat и…

...
6.12. Printing statistics.
=== counter ===
Number Number Number Number Number Number Number Number Number Number
$add $adff
of wires:
of wire bits:
of public wires:
of public wire bits: of ports:
of port bits:
of memories:
of memory bits:
of processes:
of cells:
4 10 3 6 3 6 0 0 0 2 1 1
6.13. Executing CHECK pass (checking Checking module counter...
Found and reported 0 problems.
for obvious problems).
7. Executing SAT pass (solving SAT problems in the circuit).
Setting up SAT problem:
Final constraint equation: { } = { }
ERROR: Failed to import cell $procdff$8 (type $adff) to SAT database. make: *** [Makefile:2: run] Error 1

И ничего не понятно. Я догадывался, что дело в падении на стороне Yosys, но внятного объяснения нет.

И вновь я иду открывать issue. Оказалось, что Synlig оперирует уж слишком низкоуровневыми конструкциями Yosys, чтобы я сделал все правильно. В любом случае, ни о какой сборке ядра подобным образом речи идти не может, поскольку необходимо руками прописывать нужные операции над дизайном, чтобы он смог перевариться для формальной верификации. Мне посоветовали использовать команду sby от Yosys, так как она способна делать это все за человека, и я вспомнил про плагин от Synlig.

Логичное решение: собрать все, что собирается через плагин. Осталось собрать сам плагин.

Я перебрал еще ключи компиляции, потерпел неудачу и понял, что это конец — силы на эксперименты закончились. Open source для формальной верификации победил, но в ином смысле.

Выводы

Когда я был студентом бакалавриата, мне казалось, что все нужные вещи давно кем-то написаны и выложены в открытый доступ. Подумать только: у нас есть прекрасные компиляторы, операционные системы, дошли даже до того, что переписываем все на safety-языки. Тему диплома приходилось скорее выдумывать, нежели формулировать решение реальной проблемы.

Все изменилось, когда я попал в отдел верификации аппаратных блоков. Появилось ощущение, что мы застряли где-то в 90-х по уровню развития тулов. Нам пришлось отказаться от форматтеров, так как они ломают исходный код, ни один из симуляторов вендоров не поддерживает спецификацию языка в полном объеме, а open source-решения… Хорошо, если ломаются сразу.

Есть и позитивные моменты. Кажется, на карте еще есть незакрашенные места для энтузиастов, которые хотят себя проявить. CIRCT стал приятным открытием, хоть он и не способен сейчас конкурировать с Yosys. А еще впечатлил уровень вовлеченности людей, с которыми успел пообщаться в процессе исследования.

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

Решение	Какие задачи потянет сейчас	Что должно появиться, чтобы решение стало оптимальным
Yosys + SymbiYosys (sby)	BMC, k-induction и интеграция с различными SMT-решателями. Подходит для небольших дизайнов и простых assert/assume.	Поддержка сложных конструкций SystemVerilog Assertions (SVA) в некоммерческой части, развитие фронтенда.
CIRCT	Работу с различными HDL (Chisel, Python, SV) через MLIR-диалекты. Есть перспективная архитектура («LLVM для аппаратного описания») и специализированные диалектов для формальной верификации (SMT Dialect, verif).	Стабилизация бэкенда для формальной верификации (устранение конфликтов с `llhd`-диалектом), полноценная поддержка последовательной логики, автоматическая конвертация из Slang без ручного редактирования MLIR-файлов, готовая документация по связке утилит (`circt-opt`, `circt-bmc`).
Slang	Парсит почти все, хорош в связке, если есть поддержка со стороны бэкенда.	Интеграция результатов парсинга SVA с Yosys IR, расширение функциональности плагина для передачи SVA в формальные инструменты.
Synlig	Формальная верификация небольших дизайнов, если разбираетесь во внутреннем представлении Yosys.	Актуальная поддержка, стабильная работа плагина для Yosys, простая настройка для формальной верификации.

Над этим текстом мне помогал работать коллега — Алексей Ковалов, руководитель отдела модульной верификации в YADRO. Недавно в блоге вышла его статья о том, как расти верификаторам. Прочитайте, если хотите развиваться в этом направлении.

Формальная верификация «для бедных»: выбираем open source-решение