The post has been translated automatically. Original language: Russian
Formal verification does not begin with the launch of a verification tool. First, you need to determine exactly what is considered the correct behavior of the program.
A program can have thousands of possible states and a huge number of execution paths. The phrase "check the program" is too vague. It is necessary to formulate specific properties: what states are allowed, under what conditions the operation is allowed, and what should be the state after it is performed.
For this purpose, Sekura uses SJV, a language for describing the formal properties of the module being tested.
His task is simple in meaning: to separate the question "how does the program do this?" from the question "what is the program supposed to provide?"
The program and its contract are two different things
Suppose there is a function that changes the state of some device. There may be several checks, transitions, calculations, and memory accesses in the source code.
However, only a few rules may be important to the customer or developer during formal verification. For example:
- The condition must always be within the acceptable range.;
- the operation is allowed only from a certain state;
- after a successful operation, a specific feature should change.;
- some data should not be changed;
- the forbidden state should never occur.
All these requirements can be considered separately from the algorithm by which they are provided.
Simplified:
The implementation
answers the question
"HOW?"
↕
SJV
answers the question
"WHAT SHOULD BE TRUE?"This separation is especially important for formal verification. The verifying system must compare the actual behavior of the implementation with the explicitly specified requirements.
If the requirements are not strictly written down anywhere, it is not clear what exactly needs to be proved.
SJV specifies the module to be tested
The SJV description is related to a specific program module or hardware logic.
SJV uses a module that specifies the source file to be checked. For example, it can be a Sekura JS module or a SystemVerilog file from a supported subset.
Conditional:
module motor.sjsor:
module controller.svBy using the file extension, the checking tool determines which type of implementation it works with.
This is important because the same general approach to contracts can be applied to different types of implementation, but the rules for parsing them and the execution model vary.
SJV remains a separate description of the requirements for the module being tested.
First you need to describe the acceptable states.
One of the main tasks of a formal contract is to determine which system states are considered acceptable.
Suppose a device has a state variable that can take values from 0 to 3. Then one of the requirements may be the condition:
state >= 0
state <= 3The purpose of this condition is not to check several selected program launches. The verification tool must establish that the implementation does not lead to a condition violating this rule within the considered model.
In SJV, the general condition conditions are set by top-level blocks.
The conditions are considered together within one block: all specified expressions must be fulfilled. If there are several such blocks, they can describe several acceptable state options.
In terms of meaning, it can be represented as follows:
Acceptable:
state A
And
condition B
And
condition C
or
state D
And
condition EThis way, you can describe not one specific value of all variables, but a set of allowed states of the system.
Why do I need to set acceptable states explicitly?
Without the state constraint, the verifier would have to consider values that should not occur in the real system at all.
For example, let's say the controller has three operating states:
0 — stopped
1 — it is being launched
2 — it worksThe value 255 should not physically exist as a valid controller state. If this rule is part of the device, it is useful to fix it in the contract.
Then the verification gets a formal basis to consider:
state = 0
OR
state = 1
OR
state = 2acceptable states, and the remaining values are a violation of the specified model.
This is no longer a comment in the source code or a description in the documentation. The condition becomes part of what is being checked directly.
A function is a transition from one state to another
For checking functions, it is especially important to distinguish between the state before execution and the state after execution.
Let's imagine a simple function:
start()The device must be stopped before calling it.:
state = 0After execution, it should switch to the startup state.:
state = 1It turns out the relation:
BEFORE AFTER
state = 0 ───► state = 1It is convenient to describe such transitions formally.
SJV uses function blocks for this purpose. The expressions describe the conditions of the initial and new state.
How does SJV distinguish between the state before and after
In the SJV model, the status after execution is indicated by a stroke.
Conditional:
statemeans the value before the transition, and:
state'— the value after it.
Therefore, the contract can be read something like this:
state = 0
state' = 1That is:
if the state is 0 before execution, it should be 1 after execution.
This allows you to record transitions very compactly, without introducing separate constructions like before, after, requires and ensures for each expression.
The meaning remains the same: the contract binds the initial state to the resulting one.
The contract of a function does not describe its algorithm
Suppose there is a function to bring the controller to a working state.
One implementation can use multiple intermediate checks.:
check the power supply
check the memory readiness
check the sensor
set the internal flag
change the statusAnother version of the program may do things differently.
SJV is not required to reproduce this sequence. A contract can only fix what is important from the outside:
Before:
state = READY
After:
state = RUNNING
error' = 0If the developer completely rewrites the internal algorithm later, the contract may remain the same.
Then the formal verification answers a specific question.: has the new implementation retained the required properties?
This is one of the strengths of separating specification from implementation.
The precondition limits the allowed call
The function is not required to work correctly from any possible state.
For example, the stop() command it may make sense to call only when the device is actually working. The requirement can be represented as:
state = RUNNINGThis condition refers to the condition before execution.
Next, the contract sets the result:
state' = STOPPEDIt turns out together:
state = RUNNING
│
│ stop()
▼
state' = STOPPEDThis entry shows the boundary of the function promise. We assert the required behavior in a certain initial state, not in all conceivable circumstances.
The formal specification becomes more precise precisely because it clearly shows such boundaries.
You can also describe things that shouldn't change.
A contract can specify more than just mutable values.
Suppose the function changes the state of the device, but should not change its identifier. Then this is also a property of the behavior.:
device_id' = device_idMeaning:
the value after execution must match the value before execution.
class="paragraph"> Such properties are especially useful in low-level code, where an error may accidentally affect neighboring data or a state that the function should not change at all.
If immutability is important, it's better to make it part of the contract rather than leave it as an implicit expectation of the developer.
One function can have several valid results.
Real behavior does not always have a single result.
For example, a read operation may complete successfully or return an error condition. Both outcomes can be correct if there are precise conditions for each.
Then the contract should not describe the "ideal path", but the entire set of behavior that is considered acceptable.
This is an important difference between a formal specification and a usage example. The example shows one scenario, and the contract defines the boundaries of the set of allowed scenarios.
The more precise these boundaries are, the more meaningful the verification result.
What happens if you forgot to record the property?
This is one of the most important points in formal verification.
Suppose the function must simultaneously:
- switch to the RUNNING state;
- leave the device ID unchanged;
- do not increase the error counter;
- save a protected memory area.
But only the first condition was written in SJV.
The verifier can successfully prove:
state' = RUNNINGand at the same time, do not assert anything about the other three properties.
A successful check does not mean that the program is automatically correct in all other respects.
Therefore, the quality of the formal proof directly depends on the quality of the contract.
What is written in SJV
│
▼
That becomes
the subject of proof.This seems obvious, but it is here that the words "formally verified" are often interpreted too broadly.
A good contract should be verifiable.
Phrase:
the function should work correctly.
it is not a formal property.
Statement:
after calling start(), the state should be equal to RUNNING
it is already much closer to the verifiable requirement.
Even more precisely:
if state = READY,
then after start()
state' = RUNNINGThe formal specification forces us to translate natural requirements into precise relationships between values and states.
This is useful even before running the verifier. When trying to write down a contract, it often turns out that the requirement was ambiguous or that different project participants understood it differently.
SJV may be clearer than the source code
A large function can take hundreds of lines and contain many technical details. But her essential contract is sometimes expressed in several terms.
For example, instead of examining the entire implementation, it may be enough for an external participant to see the meaning.:
Before:
mode = standby
error = 0
After:
mode = operation
error' = 0
counter'>= counterIt does not replace the source code. But such a specification answers the question much more precisely, which behavior the developer promises to check.
That is why SJV can be used not only as an input for a tool, but also as a form of technical agreement between the parties.
One contract can be applied to a new implementation.
Separating SJV from the source code provides another useful feature.
Let's say the first version of the function is written in one way:
v1 implementation
│
▼
SJVLater, a completely rewritten version appears.:
v2 implementation
The same SJVIf the external contract of the system has not changed, the new implementation must meet the same requirements.
This allows you to use the formal specification as a stable point of verification when reworking the code.
The developer is free to change the internal structure of the program as long as the new solution continues to satisfy the stated contract.
SJV is not only suitable for Sekura JS
SJV is separate from the specific implementation language.
The module can specify, for example, a Sekura JS file or a supported SystemVerilog file. Then the appropriate implementation analysis is used, but the very idea of the contract remains.
This is especially noticeable when working with hardware logic.
For the RTL module, there are also:
- acceptable states;
- input conditions;
- transitions between states;
- values before and after the clock cycle;
- properties that must always be fulfilled.
Therefore, one approach to the specification can be applied to both the software module and the supported description of digital logic, although the internal models of their verification differ.
Dependencies should be based on proven contracts.
A module rarely exists alone. It can import other components.
In compositional verification, it is important not just to assume that the dependency is working correctly. The verification should be based on a specific proven contract of this dependency.
In Sekura, such a connection can be built through SJP dependent modules.
Simplified:
Module B
SJV
│
▼
SJP-B
│
The contract is used
when verifying module AAs a result, a large project can be built from smaller, proven parts without rediscovering the entire internal implementation of each component at each level.
SJV is not a test
The test usually sets specific input values:
state = 0
command = 1after that, the program is started and compared with the expected result.
SJV describes properties of a more general nature. Its task is to set the relationships and constraints that the testing tool should set for the model in question.
For example, a test might show:
with state = 0
, we got state = 1And the formal property raises a broader question.:
for all considered cases
satisfying a given precondition,
a given
relation must be fulfilled after the transition.Testing and SJV do not compete. They test the system from different angles and can be used together.
SJV is not documentation in the usual sense.
The documentation is written primarily for humans. Explanations, examples, and a certain amount of natural ambiguity are acceptable in it.
The formal contract must be unambiguous for the verification tool.
Therefore, a good system can have both levels.:
The documentation
explains the meaning of the requirement
│
SJV
sets it formallyThe person understands why the rule exists, and the verifier gets an exact expression that can be included in the mathematical verification.
The SJV public documentation is needed precisely so that a third party can understand the meaning of these expressions and the rules for their interpretation.
Where does the proof end
SJV simultaneously defines the strength of the proof and its limits.
If the contract describes five properties, successful verification refers to these five properties. If it describes only the behavior of one function, you cannot automatically extend the result to the entire product.
Therefore, when reading the result of formal verification, it is useful not to start with a question.:
Was the check successful?
And from the question:
What was recorded in SJV?
After that, it makes sense to look at the implementation, the verification result, and the resulting SJP.
This sequence does not allow you to turn a limited formal statement into an overly broad promise.
First to negotiate, then to prove
The most important role of SJV appears even before mathematical verification.
The developer, the customer, or the auditor must first determine which behavior really matters. This behavior is translated into the exact states and relationships between them, after which it becomes the subject of verification.
It turns out to be a simple process:
The requirement is in the usual language
│
▼
The exact formal property
│
▼
SJV
│
▼
Checking the implementation
│
An evidence-based resultIf the first transition is poorly executed, a strong solver will not fix the situation. It will very accurately check the wrong property.
Therefore, SJV is not an auxiliary file next to the verifier. This is the place where the meaning of the proof itself is determined.
The implementation shows how the system works. SJV records what we require of it and what exactly we are going to prove.
Documentation
The verification language is SJV.
A supported subset of SystemVerilog.
A description of the SJP format and other formal verification materials are available in the Sekura JS documentation section.
Формальная верификация начинается не с запуска проверяющего инструмента. Сначала нужно точно определить, что именно считается правильным поведением программы.
У программы могут быть тысячи возможных состояний и огромное количество путей выполнения. Фраза «проверить программу» слишком неопределённа. Нужно сформулировать конкретные свойства: какие состояния допустимы, при каких условиях разрешена операция и каким должно быть состояние после её выполнения.
В Sekura для этого используется SJV — язык описания формальных свойств проверяемого модуля.
Его задача проста по смыслу: отделить вопрос «как программа это делает?» от вопроса «что программа обязана обеспечить?».
Программа и её контракт — разные вещи
Предположим, есть функция, которая изменяет состояние некоторого устройства. В исходном коде может быть несколько проверок, переходов, вычислений и обращений к памяти.
Но заказчику или разработчику при формальной проверке могут быть важны только несколько правил. Например:
- состояние всегда должно находиться в допустимом диапазоне;
- операция разрешена только из определённого состояния;
- после успешной операции должен измениться конкретный признак;
- некоторые данные не должны изменяться;
- запрещённое состояние никогда не должно возникнуть.
Все эти требования можно рассматривать отдельно от алгоритма, которым они обеспечиваются.
Упрощённо:
Реализация
отвечает на вопрос
«КАК?»
↕
SJV
отвечает на вопрос
«ЧТО ДОЛЖНО БЫТЬ ИСТИННО?»Это разделение особенно важно для формальной верификации. Проверяющая система должна сравнить фактическое поведение реализации с явно заданными требованиями.
Если требования нигде строго не записаны, непонятно и то, что именно должно быть доказано.
SJV указывает проверяемый модуль
Описание SJV связано с конкретным модулем программы или аппаратной логики.
В SJV используется module, который указывает проверяемый исходный файл. Например, это может быть модуль Sekura JS или файл SystemVerilog из поддерживаемого подмножества.
Условно:
module motor.sjsили:
module controller.svПо расширению файла проверяющий инструмент определяет, с каким видом реализации он работает.
Это важно, потому что один и тот же общий подход к контрактам может применяться к разным видам реализации, но правила их разбора и модель исполнения различаются.
SJV при этом остаётся отдельным описанием требований к проверяемому модулю.
Сначала нужно описать допустимые состояния
Одна из главных задач формального контракта — определить, какие состояния системы считаются допустимыми.
Предположим, у устройства есть переменная state, которая может принимать значения от 0 до 3. Тогда одним из требований может быть условие:
state >= 0
state <= 3Смысл такого условия не в том, чтобы проверить несколько выбранных запусков программы. Проверяющий инструмент должен установить, что реализация не приводит к состоянию, нарушающему это правило, в пределах рассматриваемой модели.
В SJV общие условия состояния задаются блоками верхнего уровня.
Внутри одного блока условия рассматриваются совместно: должны выполняться все указанные выражения. Если таких блоков несколько, они могут описывать несколько допустимых вариантов состояния.
По смыслу это можно представить так:
Допустимо:
состояние A
И
условие B
И
условие C
ИЛИ
состояние D
И
условие EТак можно описывать не одно конкретное значение всех переменных, а множество разрешённых состояний системы.
Почему допустимые состояния нужно задавать явно
Без ограничения состояния верификатору пришлось бы рассматривать значения, которые в реальной системе вообще не должны возникать.
Например, пусть контроллер имеет три рабочих состояния:
0 — остановлен
1 — запускается
2 — работаетЗначение 255 физически не должно существовать как допустимое состояние контроллера. Если это правило является частью устройства, его полезно зафиксировать в контракте.
Тогда проверка получает формальное основание считать:
state = 0
ИЛИ
state = 1
ИЛИ
state = 2допустимыми состояниями, а остальные значения — нарушением заданной модели.
Это уже не комментарий в исходном коде и не описание в документации. Условие становится частью того, что непосредственно проверяется.
Функция — это переход из одного состояния в другое
Для проверки функций особенно важно различать состояние до выполнения и состояние после выполнения.
Представим простую функцию:
start()Перед её вызовом устройство должно быть остановлено:
state = 0После выполнения оно должно перейти в состояние запуска:
state = 1Получается отношение:
ДО ПОСЛЕ
state = 0 ───► state = 1Именно такие переходы удобно описывать формально.
В SJV для этого используются блоки function. Выражения описывают условия исходного и нового состояния.
Как SJV различает состояние до и после
В модели SJV состояние после выполнения обозначается штрихом.
Условно:
stateозначает значение до перехода, а:
state'— значение после него.
Поэтому контракт можно читать примерно так:
state = 0
state' = 1То есть:
если до выполнения состояние равно 0, после выполнения оно должно быть равно 1.
Это позволяет записывать переходы очень компактно, не вводя отдельные конструкции вроде before, after, requires и ensures для каждого выражения.
Смысл при этом остаётся тем же: контракт связывает исходное состояние с результирующим.
Контракт функции описывает не её алгоритм
Предположим, есть функция перевода контроллера в рабочее состояние.
Одна реализация может использовать несколько промежуточных проверок:
проверить питание
проверить готовность памяти
проверить датчик
установить внутренний флаг
изменить состояниеДругая версия программы может выполнять всё иначе.
SJV не обязан воспроизводить эту последовательность. Контракт может фиксировать только то, что важно снаружи:
До:
state = READY
После:
state = RUNNING
error' = 0Если позже разработчик полностью перепишет внутренний алгоритм, контракт может остаться прежним.
Тогда формальная проверка отвечает на конкретный вопрос: сохранила ли новая реализация требуемые свойства?
В этом и состоит одна из сильных сторон отделения спецификации от реализации.
Предусловие ограничивает допустимый вызов
Функция не обязана корректно работать из любого возможного состояния.
Например, команду stop() может иметь смысл вызывать только тогда, когда устройство действительно работает. Требование можно представить как:
state = RUNNINGЭто условие относится к состоянию до выполнения.
Дальше контракт задаёт результат:
state' = STOPPEDВместе получается:
state = RUNNING
│
│ stop()
▼
state' = STOPPEDТакая запись показывает границу обещания функции. Мы утверждаем требуемое поведение при определённом исходном состоянии, а не во всех мыслимых обстоятельствах.
Формальная спецификация становится точнее именно потому, что явно показывает такие границы.
Можно описывать и то, что не должно меняться
Контракт может задавать не только изменяемые значения.
Предположим, функция меняет состояние устройства, но не должна изменять его идентификатор. Тогда это тоже является свойством поведения:
device_id' = device_idСмысл:
значение после выполнения должно совпадать со значением до выполнения.
Такие свойства особенно полезны в низкоуровневом коде, где ошибка может случайно затронуть соседние данные или состояние, которое функция вообще не должна изменять.
Если неизменность важна, её лучше сделать частью контракта, а не оставлять неявным ожиданием разработчика.
Одной функции может соответствовать несколько допустимых результатов
Реальное поведение не всегда имеет один единственный результат.
Например, операция чтения может завершиться успешно или вернуть состояние ошибки. Оба исхода могут быть корректными, если для каждого существуют точные условия.
Тогда контракт должен описывать не «идеальный путь», а весь набор поведения, которое считается допустимым.
Это важное отличие формальной спецификации от примера использования. Пример показывает один сценарий, а контракт определяет границы множества разрешённых сценариев.
Чем точнее эти границы, тем содержательнее результат проверки.
Что произойдёт, если свойство забыли записать
Это один из самых важных моментов в формальной верификации.
Предположим, функция должна одновременно:
- перейти в состояние RUNNING;
- оставить идентификатор устройства неизменным;
- не увеличивать счётчик ошибок;
- сохранить защищённую область памяти.
Но в SJV было записано только первое условие.
Верификатор может успешно доказать:
state' = RUNNINGи при этом ничего не утверждать об остальных трёх свойствах.
Успешная проверка не означает, что программа автоматически правильна во всех остальных отношениях.
Поэтому качество формального доказательства напрямую зависит от качества контракта.
Что записано в SJV
│
▼
То и становится
предметом доказательстваЭто кажется очевидным, но именно здесь часто возникает слишком широкая интерпретация слов «формально проверено».
Хороший контракт должен быть проверяемым
Фраза:
функция должна работать правильно
не является формальным свойством.
Утверждение:
после вызова start() состояние должно быть равно RUNNING
уже значительно ближе к проверяемому требованию.
Ещё точнее:
если state = READY,
то после start()
state' = RUNNINGФормальная спецификация заставляет переводить естественные требования в точные отношения между значениями и состояниями.
Это полезно даже до запуска верификатора. При попытке записать контракт часто обнаруживается, что требование было двусмысленным или что разные участники проекта понимали его по-разному.
SJV может быть понятнее исходного кода
Большая функция может занимать сотни строк и содержать множество технических деталей. Но её существенный контракт иногда помещается в несколько выражений.
Например, вместо изучения всей реализации внешнему участнику может быть достаточно увидеть смысл:
До:
режим = ожидание
ошибка = 0
После:
режим = работа
ошибка' = 0
счётчик' >= счётчикЭто не заменяет исходный код. Но такая спецификация гораздо точнее отвечает на вопрос, какое поведение разработчик обещает проверить.
Именно поэтому SJV может использоваться не только как вход для инструмента, но и как форма технического договора между сторонами.
Один контракт можно применять к новой реализации
Отделение SJV от исходного кода даёт ещё одно полезное свойство.
Допустим, первая версия функции написана одним способом:
реализация v1
│
▼
SJVПозже появляется полностью переписанная версия:
реализация v2
│
▼
тот же SJVЕсли внешний контракт системы не изменился, новая реализация должна пройти те же требования.
Это позволяет использовать формальную спецификацию как устойчивую точку проверки при переработке кода.
Разработчик свободен менять внутреннюю структуру программы, пока новое решение продолжает удовлетворять заявленному контракту.
SJV подходит не только для Sekura JS
SJV отделён от конкретного языка реализации.
module может указывать, например, файл Sekura JS или файл поддерживаемого SystemVerilog. Дальше используется соответствующий разбор реализации, но сама идея контракта сохраняется.
Это особенно заметно при работе с аппаратной логикой.
Для RTL-модуля также существуют:
- допустимые состояния;
- входные условия;
- переходы между состояниями;
- значения до такта и после него;
- свойства, которые должны выполняться всегда.
Поэтому один подход к спецификации можно применять как к программному модулю, так и к поддерживаемому описанию цифровой логики, хотя внутренние модели их проверки различаются.
Зависимости должны опираться на доказанные контракты
Модуль редко существует один. Он может импортировать другие компоненты.
При композиционной проверке важно не просто предположить, что зависимость работает правильно. Проверка должна опираться на конкретный доказанный контракт этой зависимости.
В Sekura такая связь может строиться через SJP зависимых модулей.
Упрощённо:
Модуль B
│
SJV
│
▼
SJP-B
│
▼
контракт используется
при проверке модуля AВ результате большой проект можно строить из меньших проверенных частей, не раскрывая заново всю внутреннюю реализацию каждого компонента на каждом уровне.
SJV — не тест
Тест обычно задаёт конкретные входные значения:
state = 0
command = 1после чего программа запускается и сравнивается с ожидаемым результатом.
SJV описывает свойства более общего характера. Его задача — задать отношения и ограничения, которые проверяющий инструмент должен установить для рассматриваемой модели.
Например, тест может показать:
при state = 0
получили state = 1А формальное свойство ставит вопрос шире:
для всех рассматриваемых случаев,
удовлетворяющих заданному предусловию,
должно выполняться заданное
отношение после переходаТестирование и SJV не конкурируют. Они проверяют систему с разных сторон и могут использоваться вместе.
SJV — не документация в обычном смысле
Документация написана прежде всего для человека. В ней допустимы объяснения, примеры и некоторое количество естественной неоднозначности.
Формальный контракт должен быть однозначным для проверяющего инструмента.
Поэтому хорошая система может иметь оба уровня:
Документация
объясняет смысл требования
│
SJV
задаёт его формальноЧеловек понимает, зачем существует правило, а верификатор получает точное выражение, которое можно включить в математическую проверку.
Публичная документация SJV нужна как раз для того, чтобы третья сторона могла понимать значение этих выражений и правила их интерпретации.
Где заканчивается доказательство
SJV одновременно задаёт силу доказательства и его границы.
Если контракт описывает пять свойств, успешная проверка относится к этим пяти свойствам. Если он описывает только поведение одной функции, нельзя автоматически распространить результат на весь продукт.
Поэтому при чтении результата формальной верификации полезно начинать не с вопроса:
Проверка прошла?
а с вопроса:
Что было записано в SJV?
После этого уже имеет смысл смотреть на реализацию, результат проверки и полученный SJP.
Такая последовательность не позволяет превратить ограниченное формальное утверждение в слишком широкое обещание.
Сначала договориться, потом доказывать
Самая важная роль SJV проявляется ещё до математической проверки.
Разработчик, заказчик или аудитор сначала должны определить, какое поведение действительно имеет значение. Это поведение переводится в точные состояния и отношения между ними, после чего становится предметом проверки.
Получается простой процесс:
Требование на обычном языке
│
▼
Точное формальное свойство
│
▼
SJV
│
▼
Проверка реализации
│
▼
Доказательный результатЕсли первый переход выполнен плохо, сильный решатель ситуацию не исправит. Он очень точно проверит не то свойство.
Поэтому SJV — это не вспомогательный файл рядом с верификатором. Это место, где определяется смысл самого доказательства.
Реализация показывает, как работает система. SJV фиксирует, что мы от неё требуем и что именно собираемся доказать.
Документация
Поддерживаемое подмножество SystemVerilog.
Описание формата SJP и остальные материалы по формальной верификации доступны в разделе документации Sekura JS.
Share
