The post has been translated automatically. Original language: Russian
After publishing the materials on formal verification, we were asked which tools we use: ready-made open solutions, commercial systems, or our own developments.
Our chain has its own tools and open-source funds. To prepare and test the model, we develop SJV, and directly solve the feasibility problems of Z3 and CVC5.
A limited subset of SystemVerilog
The Memora8 hardware is described on SystemVerilog, but we don't use the entire language for formal verification. A special subset of SystemVerilog, SJV—SV, is defined for SJV.
The limitation of the language is fundamental here. The verifying tool must accurately understand the constructions that are included in the proof, their bit depth, signedness, the rules of operation of arrays, sequential and combinational logic. If an unsupported design occurs in the part being tested, it should not be silently ignored or replaced by a simplified model.
The same .sv source file is used in two independent ways:
SystemVerilog → Vivado → FPGA implementation
SystemVerilog → SJV → formal model → SMT
Thus, SJV analyzes the same source RTL that is used to implement the processor on the FPGA. A separate simplified version of the processor is not created specifically for the proof.
Detailed rules and current limitations of SJV-SV are described separately in the document "SystemVerilog Subset for SJV" — here you will find a link to the published description.
What does SJV do?
SJV is our formal verification tool. For SystemVerilog, it analyzes the selected module and its static hierarchy, performs the necessary transformations, and builds a model of system transitions.
The conditions that need to be checked are set separately. At the same time, you can create different checks for the same module: for example, you can check different properties of a single hardware unit independently of each other.
In the next step, SJV transfers the task to SMT. This is already a mathematical representation of conditions, states, and a verifiable property that can be passed to a specialized solver.
Simplified, the path looks like this:
SystemVerilog → SJV → SMT → Solver
Z3 as the main solver
The main solver in the current chain is Z3. SJV generates an SMT problem and passes it to Z3, which checks whether there is a condition that violates the specified condition.
If such a condition is found, the result is a counterexample. If the corresponding problem has no solution, this is used as a basis for confirming the checked property within the specified model and its conditions.
Here it is important to distinguish between the actual proof model and the work of the solver. SJV is responsible for translating the source system and requirements into SMT, while Z3 solves the mathematical problem already obtained.
Why do I need CVC5?
We also added the ability to re-test the same SMT problem with another independent solver, CVC5.
SJP retains the exact SMT-LIB2 tasks generated during the check. If you check them again, you can transfer them to Z3 again, and if necessary, additionally to CVC5 and compare the results.
If both solvers independently give the same definite answer, this reduces the dependence of the result on the possible error of one particular solver.
At the same time, such a check has a clear boundary. The coincidence of the results of Z3 and CVC5 confirms that both solvers solved the generated SMT problem in the same way. This alone does not prove that SJV has correctly transformed the original SystemVerilog and the test condition into this task.
It is important for us to clearly maintain this boundary, and not to call proven what is actually still part of the trusted chain.
SJP as a stored verification result
The result of the formal verification is saved in the SJP — Sekura Justified Proof format.
The current version of SJP may contain accurate SMT-LIB2 tasks, information about the source data being checked, verification conditions, and dependencies. This allows you not to limit yourself to the message "the check was successfully completed", but to save the data necessary for its repeated execution.
SJP can then be checked again. With this startup, the hashes of the associated data are re-monitored and the saved SMT tasks are solved again. Additionally, they can be passed to CVC5 for independent comparison with the result of Z3.
Reproducibility is an important part of the whole scheme for us. The verification result must be related to a specific source code, specific conditions, and specific mathematical problems.
What is private in this chain, and what is open
We are not building our own SMT solver. The existing Z3 and CVC5 open source projects are used for this part.
Our development focuses on another part of the chain: how to move from the real source code of the system to a formal model, create verifiable conditions, get SMT tasks and save the result so that it can be reproduced.
Today, this hardware chain looks like this:
limited subset of SystemVerilog → SJV → SMT → Z3 → SJP → Z3/CVC5 retest
This does not mean that the correctness of the entire processor or the entire system is automatically proven. Each proof relates to a specific property, a specific area of the model, and explicitly specified conditions.
But it is precisely from such verifiable and reproducible results that we are gradually building the evidence base for Memora8 and the entire Sekura hardware and software stack.
После публикации материалов о формальной верификации нас спросили, какие инструменты мы используем: готовые открытые решения, коммерческие системы или собственные разработки.
В нашей цепочке есть и собственные инструменты, и открытые средства. Для подготовки и проверки модели мы развиваем SJV, а непосредственно задачи выполнимости решают Z3 и CVC5.
Ограниченное подмножество SystemVerilog
Аппаратная часть Memora8 описывается на SystemVerilog, но для формальной проверки мы используем не весь язык. Для SJV определено специальное подмножество SystemVerilog — SJV-SV.
Ограничение языка здесь принципиально. Проверяющий инструмент должен точно понимать конструкции, которые входят в доказательство, их разрядность, знаковость, правила работы массивов, последовательной и комбинационной логики. Если в проверяемой части встречается неподдерживаемая конструкция, она не должна молча игнорироваться или заменяться упрощённой моделью.
Один и тот же исходный файл .sv используется двумя независимыми путями:
SystemVerilog → Vivado → реализация на FPGA
SystemVerilog → SJV → формальная модель → SMT
Таким образом, SJV анализирует тот же исходный RTL, который используется для реализации процессора на FPGA. Отдельная упрощённая версия процессора специально для доказательства не создаётся.
Подробные правила и текущие ограничения SJV-SV описаны отдельно в документе «Подмножество SystemVerilog для SJV» — здесь будет ссылка на опубликованное описание.
Что делает SJV
SJV — наш инструмент формальной проверки. Для SystemVerilog он разбирает выбранный модуль и его статическую иерархию, выполняет необходимые преобразования и строит модель переходов системы.
Условия, которые требуется проверить, задаются отдельно. При этом для одного и того же модуля можно создавать разные проверки: например, проверять разные свойства одного аппаратного блока независимо друг от друга.
На следующем этапе SJV переводит задачу в SMT. Это уже математическое представление условий, состояний и проверяемого свойства, которое можно передать специализированному решателю.
Упрощённо путь выглядит так:
SystemVerilog → SJV → SMT → решатель
Z3 как основной решатель
Основным решателем в текущей цепочке является Z3. SJV формирует SMT-задачу и передаёт её Z3, который проверяет, существует ли состояние, нарушающее заданное условие.
Если такое состояние найдено, результатом становится контрпример. Если соответствующая задача не имеет решения, это используется как основание для подтверждения проверяемого свойства в пределах заданной модели и её условий.
Здесь важно различать собственно доказательную модель и работу решателя. SJV отвечает за перевод исходной системы и требований в SMT, а Z3 решает уже полученную математическую задачу.
Зачем нужен CVC5
Мы также добавили возможность повторно проверить ту же SMT-задачу другим независимым решателем — CVC5.
SJP сохраняет точные SMT-LIB2 задачи, сформированные во время проверки. При повторной проверке их можно снова передать Z3, а при необходимости — дополнительно CVC5 и сравнить результаты.
Если оба решателя независимо дают один и тот же определённый ответ, это уменьшает зависимость результата от возможной ошибки одного конкретного решателя.
При этом такая проверка имеет чёткую границу. Совпадение результатов Z3 и CVC5 подтверждает, что оба решателя одинаково решили сформированную SMT-задачу. Оно само по себе не доказывает, что SJV безошибочно преобразовал исходный SystemVerilog и проверяемое условие в эту задачу.
Для нас важно явно сохранять эту границу, а не называть доказанным то, что в действительности ещё остаётся частью доверенной цепочки.
SJP как сохраняемый результат проверки
Результат формальной проверки сохраняется в формате SJP — Sekura Justified Proof.
Текущая версия SJP может содержать точные SMT-LIB2 задачи, сведения о проверяемых исходных данных, условиях проверки и зависимостях. Это позволяет не ограничиваться сообщением «проверка когда-то успешно прошла», а сохранить данные, необходимые для её повторного выполнения.
SJP можно затем проверить повторно. При таком запуске заново контролируются хеши связанных данных и повторно решаются сохранённые SMT-задачи. Дополнительно их можно передать CVC5 для независимого сравнения с результатом Z3.
Именно воспроизводимость для нас является важной частью всей схемы. Результат проверки должен быть связан с конкретным исходным кодом, конкретными условиями и конкретными математическими задачами.
Что в этой цепочке собственное, а что открытое
Мы не создаём собственный SMT-решатель. Для этой части используются существующие открытые проекты Z3 и CVC5.
Наша разработка сосредоточена на другом участке цепочки: на том, как перейти от реального исходного кода системы к формальной модели, сформировать проверяемые условия, получить SMT-задачи и сохранить результат так, чтобы его можно было воспроизвести.
Сегодня эта цепочка для аппаратной части выглядит следующим образом:
ограниченное подмножество SystemVerilog → SJV → SMT → Z3 → SJP → повторная проверка Z3/CVC5
Это не означает, что автоматически доказана корректность всего процессора или всей системы. Каждое доказательство относится к конкретному свойству, конкретной области модели и явно заданным условиям.
Но именно из таких проверяемых и воспроизводимых результатов мы постепенно строим доказательную базу для Memora8 и всего программно-аппаратного стека Sekura.
Share
