The post has been translated automatically. Original language: Russian
A routine check of a digital module most often begins with a simulation. The developer inputs pre-selected values, switches the clock signal, and looks to see if the behavior matches the expected one.
This approach is necessary, but it has an obvious limitation: only those scripts that have been run are checked. If a combination of inputs or states is not included in the tests, the error may go unnoticed.
Formal verification sets the task differently. Instead of a set of specific tests, we describe the properties that must be performed for all the system states under consideration, and then mathematically check the RTL module for compliance with these properties.
Sekura uses a bundle of the original RTL, the formal SJV description, and the SJP evidence package for SystemVerilog.
We start with the usual RTL
Let's take a simple counter:
module counter (
input logic clk,
input logic reset,
input logic enable,
output logic [7:0] value
);
always_ff @(posedge clk) begin
if (reset)
value <= 8'd0;
else if (enable)
value <= value + 8'd1;
end
endmoduleThis is a regular synthesized SystemVerilog. Such a file can be used by a standard FPGA synthesis tool.
Formal verification does not require creating a separate copy of the schema in another language. The same source RTL is checked.
The general scheme looks like this:
counter.sv
│
───► FPGA synthesis
│
└──► Formal verification
The mathematical modelThis is important: the proof must relate to the same implementation that is then used in the device.
First, we define what we want to prove
The SystemVerilog file itself does not tell us which properties we are interested in.
Different requirements can be formulated for the counter:
- after the reset, the value is zero;
- if enable = 0, the value does not change.;
- if enable = 1, the value increases by one.;
- no other signal should change state unexpectedly.;
- after an overflow, the 8-bit counter returns to zero.
These are different properties. You can prove one of them, several of them, or all of them at once.
Therefore, the formal verification does not begin with the launch command, but with a question.:
What exactly should this scheme guarantee?
In Sekura, such requirements are set via SJV.
Linking SJV with RTL module
SJV indicates which source module is being checked.
Simplified:
module counter.svThe following describes the acceptable states and transitions.
For example, if enable = 0, the counter should keep the value:
enable = 0
value' = valueThe stroke indicates the value after the transition. Therefore, the expression:
value' = valueit can be read as:
the value after the next step must match the current one.
For the case of enable = 1, the property is already different.:
enable = 1
value' = value + 1This is how SJV describes not the internal RTL algorithm, but the expected relationship between states.
The state before and the state after
A serial digital circuit is naturally represented as a transition between states.
For the counter:
value(t)
│
│ posedge clk
▼
value(t+1)If enable = 1, it is expected:
value(t+1) = value(t) + 1If enable = 0:
value(t+1) = value(t)If reset is active:
value(t+1) = 0Instead of running three separate tests, we formulate three relationships that must be performed for all valid values of the current state.
This is where formal verification begins to differ markedly from modeling.
The inputs do not have to be specified in specific numbers.
The test usually says something like:
enable = 1
value = 37and they check that the next result is 38.
The formal model can treat value as an arbitrary 8-bit value.:
value ∈ 0..255Then the property:
enable = 1
value' = value + 1It is checked for all 256 possible values at once.
This means that it is not necessary to write separate tests for 0, 1, 17, 128 and 255 to prove exactly this property.
However, formal verification does not cancel testing. She answers another question.
Overflow is also included in the model
In SystemVerilog, the width of the signal matters.
Our counter has eight bits:
logic [7:0] value;Therefore, after:
255 + 1the result does not become 256.
For an 8-bit value, it returns to zero.:
11111111
+1
─────────
00000000A formal analyzer should take into account exactly this bit semantics of SystemVerilog.
If, when constructing a mathematical model, we consider value to be an ordinary unlimited integer, we will get a different system.
Therefore, the exact width of the signals is part of the proof.
The next step is to build a transition model.
After reading the SystemVerilog, the verifier should turn the RTL into a mathematical model.
Conditional:
SystemVerilog
The structure of the modules
│
─
Registers and signals
, The rules of transitions
The mathematical modelFor our example, the state is practically reduced to a single register.:
S(t) = value(t)Entrances:
I(t) = reset(t), enable(t)And the transition ratio describes what the value will be equal to after the next clock edge.
Simplified:
if reset:
value' = 0
otherwise, if enable:
value' = value + 1
otherwise:
value' = valueThis model is then mapped to properties from SJV.
The property turns into a mathematical problem.
Suppose we want to prove:
When enable = 0, the counter value does not change.
The verifier already knows the RTL transitions. He also knows the requirement:
enable = 0
→
value' = valueFor verification, you can ask the opposite question.:
Can there be a state in which enable = 0, but the value has changed after the clock cycle?
Conventionally, the mathematical problem looks like this:
RTL behavior
And
enable = 0
And
value' != valueIf such a combination is not possible, the solver returns a result indicating that there is no counterexample.
Thus, a formal proof often actually boils down to an attempt to mathematically find a violation of a property.
What does the SMT solver do?
After converting RTL and SJV into mathematical expressions, the problem is passed to an SMT solver, such as Z3.
The common chain:
counter.sv
+
counter.sjv
│
The transition model
│
- Mathematical obligations
│
▼
Z3If the solver does not find a condition violating the property, the commitment can be confirmed.
If a violation exists, a counterexample can be obtained.
This is one of the key advantages of the approach: the result is not necessarily just "error found". You can see a specific condition that breaks the declared property.
A counterexample is more useful than a general error message
Let's imagine that we made a mistake.:
else if (enable)
value <= value + 8'd2;And the contract still requires:
enable = 1
value' = value + 1A formal check will reveal a contradiction.
Instead of having to manually come up with a suitable test, you can get a specific example.:
value = 37
enable = 1
expected:
value' = 38
really:
value' = 39For more complex circuits, a counterexample may contain a sequence of clock cycles, input values, and internal states.
This turns formal verification not only into a proof mechanism, but also into a means of finding difficult-to-reproduce errors.
The reset needs to be described accurately
Resetting often seems like an obvious part of RTL, but to prove it, its semantics must be unambiguous.
For example:
always_ff @(posedge clk) begin
if (reset)
value <= 0;
...
endmeans a synchronous reset.
And the construction:
always_ff @(posedge clk or negedge reset_n)it already describes an asynchronous reset event.
For the formal model, these are different transitions.
You can't just assume that any reset works the same way. If the reset model does not match the real RTL, you can prove the properties of another scheme.
The same applies to memory
Consider memory:
logic [31:0] mem [0:2047];If the module writes and reads it, the mathematical model must maintain the relationship between the address and the contents.
For example:
entry:
mem[address] = datait should affect exactly the element that is then read at the same address.
The details are important.:
- synchronous or asynchronous reading;
- what happens when reading and writing the same address?;
- is there a partial record;
- who owns the memory;
- how many processes can write.
SJV-SV already has a formal model for some types of synchronous RAM. More complex cases may end up as unsupported.
And this is the correct behavior: unsupported memory is better to explicitly reject than to silently prove a simplified model.
We only check the supported SystemVerilog
Before formal verification, RTL must be part of a supported subset of SJV-SV.
This means that it is not enough to successfully read the syntax of the file. All constructions affecting the proof must have certain mathematical semantics.
For example, the usual:
module
always_comb
always_ff
assign
if / case
fixed arrays
enum
packed structthey can be part of a supported profile.
And designs for which there is no model should lead to a clear failure.
Result:
UNSUPPORTEDmuch more honest than the result:
VERIFIEDif part of the scheme was actually ignored.
The whole hierarchy must be taken into account
A real module rarely consists of a single file.
For example:
top.sv
├─ control.sv
├─ fifo.sv
└─ memory.svIn addition, the result may be influenced by:
package
include
define
parameter
selected top moduleTherefore, a formal check should capture the entire set of source data that affects the final scheme.
You can't prove it top.sv , and then imperceptibly replace fifo.sv and continue to consider the old proof valid.
The proof refers to the specific configuration of the entire test area.
One RTL can have multiple formal contracts.
It is not necessary to try to describe all the properties of a module in one huge SJV.
A single SystemVerilog file can be verified by several independent specifications.
For example:
controller.sv
controller.safety.sjv
controller.protocol.sjv
controller.memory.sjvThe first can check the security of states, the second — the correctness of the exchange, the third — the rules of access to memory.
Each check has its own scope and its own result.
This is convenient because the statement:
the module has been formally verified
getting more specific:
Certain security properties and protocol properties have been proven for this module.
What does the practical process look like?
For a small RTL module, the sequence of operation can be represented as follows:
1. Write SystemVerilog RTL
│
▼
2. Make sure that it is being used
supported subset
3. Define properties
│
▼
4. Write them in SJV
│
▼
5. Perform a formal verification
│
▼
6. Explore a counterexample
or confirmed properties
7
. Form SJPIf the check reveals an error, the RTL is corrected or, if the problem was in the statement of the requirement, the SJV.
After that, the check is performed again.
Example: the forbidden state of the machine
Let's consider a simple automaton with states:
IDLE
RUN
ERRORLet the register have two bits, so technically four values are possible.:
00
01
10
11But the value 11 should never occur.
With regular tests, you can run through a lot of transitions and never see it.
The formal property can be formulated directly:
state != 3Now the task is not to iterate through several test sequences, but to try to find any valid sequence of inputs that will lead to state = 3.
If it exists, the formal verification should show the appropriate path.
If an invariant is proven, the property applies to all states within the accepted model, not just to a pre-selected test length.
Limited verification and proof are not the same thing.
Sometimes the instrument examines the system only for a certain number of clock cycles.
For example:
0 → 1 → 2 → ... → 20 clock cyclesIf no violation is found in 20 steps, this is a useful result. But it does not necessarily mean that a violation is impossible on the 21st or 1000th clock cycle.
Therefore, it is necessary to distinguish:
limited verificationand:
unlimited inductive proofThese results should not be mixed in the report.
That is why a good formal process captures not only the word "successful", but also the way in which the property was confirmed.
What happens after successful verification
It is advisable not to leave a successful proof only in the console log.
In Sekura, the result can be formatted as a SJP, a separate evidence package.
The chain becomes like this:
controller.sv
+
controller.sjv
│
─
formal verification
│
▼
controller.sjpSJP captures the relationship of a result to a specific implementation, formal contract, validation parameters, and dependencies.
This allows you to save the proof along with the project or transfer it to another party.
Why is SJP important for RTL?
Hardware projects are particularly version-sensitive.
The same module can be assembled:
- with different parameters;
- with different define;
- with different packages;
- in different hierarchy configurations.
Therefore, it is not enough to say:
controller.sv it was checked.
You need to know the exact configuration for which the proof is constructed.
SJP allows you to associate the result with this particular set of inputs.
If one of them has changed, a new check is required.
Formal verification is not a substitute for synthesis
Even a perfectly proven RTL still needs to be synthesized and implemented for the target FPGA or ASIC.
The formal verifier verifies the logical properties of the RTL model. He doesn't automatically answer questions.:
- does the project pass the time limits;
- does it fit into the selected FPGA;
- are the physical signals separated correctly?;
- does the memory latency match the actual device?;
- whether there are power problems or analog effects.
Therefore, a normal process contains several independent steps.:
RTL
│
├──► Formal verification
│
├──► Modeling
│
├──► synthesis
│
└──► implementation on the deviceThey complement each other.
Formal verification is not a substitute for tests
The same applies to modeling and testing.
Formal methods are especially strong where the property can be precisely formulated mathematically: states, transitions, access restrictions, protocols, counters, queues, arbitration.
Tests are more convenient for other tasks: integration with the environment, performance, temporary behavior of real devices, complex external protocols and verification of the whole system.
The best result is usually a combination of both approaches.
For example:
tests:
they show practical scenarios
formal verification:
explores the entire space
specified by the modelOne method closes the weaknesses of the other.
Where to start on a real module
For the first practical experience, it is better not to take the entire processor or a large system unit at once.
A suitable candidate is a small module with an understandable state.:
- counter;
- finite state machine;
- FIFO;
- the arbitrator;
- status register;
- A simple controller;
- a small memory block.
For such a component, it is easier to formulate several precise properties and check whether the implementation corresponds to them.
For example, for FIFO, you can start with three requirements:
count never exceeds DEPTH
reading an empty queue is prohibited
after successful recording
, the count increases by oneAfter that, you can move on to more complex dependencies and compositional verification.
The basic principle
The practical meaning of formal RTL verification can be reduced to a single chain:
SystemVerilog
The exact model of behavior
│
+
formal properties of SJV
Math
commitments
, The solver
The proof
│
▼
SJPThe main thing here is not the presence of the solver itself. The main work happens earlier: you need to accurately determine the RTL configuration to be tested, build a valid model, and formulate properties that really make engineering sense.
Only then does the VERIFIED result become a meaningful statement.
It doesn't mean "the SystemVerilog module is generally correct", but a much more precise thing.:
For a specific RTL version and configuration, the specifically listed properties are checked within a given model.
It is precisely this precision that makes formal verification a useful engineering practice.
Documentation
A supported subset of SystemVerilog.
Обычная проверка цифрового модуля чаще всего начинается с моделирования. Разработчик подаёт на вход заранее выбранные значения, переключает тактовый сигнал и смотрит, соответствует ли поведение ожидаемому.
Такой подход необходим, но у него есть очевидное ограничение: проверяются только те сценарии, которые были запущены. Если комбинация входов или состояний не попала в тесты, ошибка может остаться незамеченной.
Формальная проверка ставит задачу иначе. Вместо набора конкретных тестов мы описываем свойства, которые должны выполняться для всех рассматриваемых состояний системы, а затем математически проверяем RTL-модуль на соответствие этим свойствам.
В Sekura для SystemVerilog используется связка из исходного RTL, формального описания SJV и доказательного пакета SJP.
Начинаем с обычного RTL
Возьмём простой счётчик:
module counter (
input logic clk,
input logic reset,
input logic enable,
output logic [7:0] value
);
always_ff @(posedge clk) begin
if (reset)
value <= 8'd0;
else if (enable)
value <= value + 8'd1;
end
endmoduleЭто обычный синтезируемый SystemVerilog. Такой файл может использоваться стандартным средством синтеза FPGA.
Для формальной проверки не требуется создавать отдельную копию схемы на другом языке. Проверяется тот же исходный RTL.
Общая схема выглядит так:
counter.sv
│
├──► синтез FPGA
│
└──► формальная проверка
│
▼
математическая модельЭто важно: доказательство должно относиться к той же реализации, которая затем используется в устройстве.
Сначала определяем, что хотим доказать
Файл SystemVerilog сам по себе ещё не говорит, какие свойства нас интересуют.
Для счётчика можно сформулировать разные требования:
- после сброса значение равно нулю;
- если enable = 0, значение не меняется;
- если enable = 1, значение увеличивается на единицу;
- никакой другой сигнал не должен неожиданно менять состояние;
- после переполнения 8-битный счётчик возвращается к нулю.
Это разные свойства. Можно доказать одно из них, несколько или все сразу.
Поэтому формальная проверка начинается не с команды запуска, а с вопроса:
Что именно должна гарантировать эта схема?
В Sekura такие требования задаются через SJV.
Связываем SJV с RTL-модулем
SJV указывает, какой исходный модуль проверяется.
Упрощённо:
module counter.svДальше описываются допустимые состояния и переходы.
Например, если enable = 0, счётчик должен сохранить значение:
enable = 0
value' = valueШтрих означает значение после перехода. Поэтому выражение:
value' = valueможно читать как:
значение после следующего шага должно совпадать с текущим.
Для случая enable = 1 свойство уже другое:
enable = 1
value' = value + 1Так SJV описывает не внутренний алгоритм RTL, а ожидаемое отношение между состояниями.
Состояние до и состояние после
Последовательная цифровая схема естественным образом представляется как переход между состояниями.
Для счётчика:
value(t)
│
│ posedge clk
▼
value(t+1)Если enable = 1, ожидается:
value(t+1) = value(t) + 1Если enable = 0:
value(t+1) = value(t)Если активен сброс:
value(t+1) = 0Вместо запуска трёх отдельных тестов мы формулируем три отношения, которые должны выполняться для всех допустимых значений текущего состояния.
Именно здесь формальная проверка начинает заметно отличаться от моделирования.
Входы не обязательно задавать конкретными числами
В тесте обычно пишут что-то вроде:
enable = 1
value = 37и проверяют, что следующий результат равен 38.
Формальная модель может рассматривать value как произвольное 8-битное значение:
value ∈ 0..255Тогда свойство:
enable = 1
value' = value + 1проверяется сразу для всех 256 возможных значений.
Это означает, что отдельно писать тесты для 0, 1, 17, 128 и 255 не требуется для доказательства именно этого свойства.
При этом формальная проверка не отменяет тестирование. Она отвечает на другой вопрос.
Переполнение тоже входит в модель
В SystemVerilog ширина сигнала имеет значение.
Наш счётчик имеет восемь бит:
logic [7:0] value;Поэтому после:
255 + 1результат не становится 256.
Для 8-битного значения он возвращается к нулю:
11111111
+1
─────────
00000000Формальный анализатор должен учитывать именно эту битовую семантику SystemVerilog.
Если при построении математической модели считать value обычным неограниченным целым числом, получится уже другая система.
Поэтому точная ширина сигналов — часть доказательства.
Следующий шаг — построение модели переходов
После чтения SystemVerilog верификатор должен превратить RTL в математическую модель.
Условно:
SystemVerilog
│
▼
структура модулей
│
▼
регистры и сигналы
│
▼
правила переходов
│
▼
математическая модельДля нашего примера состояние практически сводится к одному регистру:
S(t) = value(t)Входы:
I(t) = reset(t), enable(t)А отношение перехода описывает, чему будет равен value после следующего фронта такта.
Упрощённо:
если reset:
value' = 0
иначе если enable:
value' = value + 1
иначе:
value' = valueЭта модель затем сопоставляется со свойствами из SJV.
Свойство превращается в математическую задачу
Предположим, мы хотим доказать:
При enable = 0 значение счётчика не меняется.
Верификатор уже знает переходы RTL. Он также знает требование:
enable = 0
→
value' = valueДля проверки можно поставить противоположный вопрос:
Может ли существовать состояние, в котором enable = 0, но после такта значение изменилось?
Условно математическая задача выглядит так:
поведение RTL
И
enable = 0
И
value' != valueЕсли такая комбинация невозможна, решатель возвращает результат, означающий отсутствие контрпримера.
Таким образом, формальное доказательство часто фактически сводится к попытке математически найти нарушение свойства.
Что делает SMT-решатель
После преобразования RTL и SJV в математические выражения задача передаётся SMT-решателю, например Z3.
Общая цепочка:
counter.sv
+
counter.sjv
│
▼
модель переходов
│
▼
математические обязательства
│
▼
Z3Если решатель не находит состояния, нарушающего свойство, обязательство может быть подтверждено.
Если нарушение существует, можно получить контрпример.
Это одно из ключевых преимуществ подхода: результатом не обязательно будет только «ошибка найдена». Можно увидеть конкретное состояние, которое ломает заявленное свойство.
Контрпример полезнее общего сообщения об ошибке
Представим, что мы допустили ошибку:
else if (enable)
value <= value + 8'd2;А контракт по-прежнему требует:
enable = 1
value' = value + 1Формальная проверка обнаружит противоречие.
Вместо необходимости вручную придумывать подходящий тест можно получить конкретный пример:
value = 37
enable = 1
ожидалось:
value' = 38
реально:
value' = 39Для более сложных схем контрпример может содержать последовательность тактов, значения входов и внутренние состояния.
Это превращает формальную проверку не только в механизм доказательства, но и в средство поиска трудно воспроизводимых ошибок.
Сброс нужно описывать точно
Сброс часто кажется очевидной частью RTL, но для доказательства его семантика должна быть однозначной.
Например:
always_ff @(posedge clk) begin
if (reset)
value <= 0;
...
endозначает синхронный сброс.
А конструкция:
always_ff @(posedge clk or negedge reset_n)уже описывает асинхронное событие сброса.
Для формальной модели это разные переходы.
Нельзя просто предположить, что любой reset работает одинаково. Если модель сброса не соответствует реальному RTL, можно доказать свойства другой схемы.
То же относится к памяти
Рассмотрим память:
logic [31:0] mem [0:2047];Если модуль пишет и читает её, математическая модель должна сохранять связь между адресом и содержимым.
Например:
запись:
mem[address] = dataдолжна влиять именно на тот элемент, который затем читается по тому же адресу.
При этом важны детали:
- синхронное или асинхронное чтение;
- что происходит при чтении и записи одного адреса;
- есть ли частичная запись;
- кто владеет памятью;
- сколько процессов могут выполнять запись.
Для некоторых видов синхронной RAM SJV-SV уже имеет формальную модель. Более сложные случаи могут завершаться как неподдерживаемые.
И это правильное поведение: неподдерживаемую память лучше явно отклонить, чем молча доказать упрощённую модель.
Проверяем только поддерживаемый SystemVerilog
Перед формальной проверкой RTL должен входить в поддерживаемое подмножество SJV-SV.
Это означает, что недостаточно успешно прочитать синтаксис файла. Все конструкции, влияющие на доказательство, должны иметь определённую математическую семантику.
Например, обычные:
module
always_comb
always_ff
assign
if / case
фиксированные массивы
enum
packed structмогут входить в поддерживаемый профиль.
А конструкции, для которых модель отсутствует, должны приводить к явному отказу.
Результат:
UNSUPPORTEDнамного честнее результата:
VERIFIEDесли часть схемы фактически была проигнорирована.
Нужно учитывать всю иерархию
Реальный модуль редко состоит из одного файла.
Например:
top.sv
├─ control.sv
├─ fifo.sv
└─ memory.svКроме того, на результат могут влиять:
package
include
define
parameter
выбранный top moduleПоэтому формальная проверка должна фиксировать весь набор исходных данных, влияющий на итоговую схему.
Нельзя доказать top.sv, а затем незаметно заменить fifo.sv и продолжать считать старое доказательство действительным.
Доказательство относится к конкретной конфигурации всей проверяемой области.
Один RTL может иметь несколько формальных контрактов
Не обязательно пытаться описать все свойства модуля в одном огромном SJV.
Один SystemVerilog-файл может проверяться несколькими независимыми спецификациями.
Например:
controller.sv
controller.safety.sjv
controller.protocol.sjv
controller.memory.sjvПервая может проверять безопасность состояний, вторая — правильность обмена, третья — правила доступа к памяти.
Каждая проверка имеет собственную область и собственный результат.
Это удобно, потому что утверждение:
модуль формально проверен
становится более конкретным:
для этого модуля доказаны такие-то свойства безопасности и такие-то свойства протокола.
Как выглядит практический процесс
Для небольшого RTL-модуля последовательность работы можно представить так:
1. Написать SystemVerilog RTL
│
▼
2. Убедиться, что используется
поддерживаемое подмножество
│
▼
3. Определить свойства
│
▼
4. Записать их в SJV
│
▼
5. Выполнить формальную проверку
│
▼
6. Исследовать контрпример
или подтверждённые свойства
│
▼
7. Сформировать SJPЕсли проверка выявила ошибку, исправляется RTL или, если проблема была в постановке требования, SJV.
После этого проверка выполняется снова.
Пример: запрещённое состояние автомата
Рассмотрим простой автомат с состояниями:
IDLE
RUN
ERRORПусть регистр имеет два бита, поэтому технически возможны четыре значения:
00
01
10
11Но значение 11 не должно возникать никогда.
Обычными тестами можно прогнать множество переходов и ни разу его не увидеть.
Формальное свойство можно сформулировать непосредственно:
state != 3Теперь задача состоит не в переборе нескольких тестовых последовательностей, а в попытке найти любую допустимую последовательность входов, которая приведёт к state = 3.
Если она существует, формальная проверка должна показать соответствующий путь.
Если доказан инвариант, свойство относится ко всем состояниям в пределах принятой модели, а не только к заранее выбранной длине теста.
Ограниченная проверка и доказательство — не одно и то же
Иногда инструмент исследует систему только на определённое число тактов.
Например:
0 → 1 → 2 → ... → 20 тактовЕсли нарушение не найдено за 20 шагов, это полезный результат. Но он ещё не обязательно означает, что нарушение невозможно на 21-м или 1000-м такте.
Поэтому нужно различать:
ограниченная проверкаи:
неограниченное индуктивное доказательствоВ отчёте эти результаты не должны смешиваться.
Именно поэтому хороший формальный процесс фиксирует не только слово «успешно», но и способ, которым свойство было подтверждено.
Что происходит после успешной проверки
Успешное доказательство желательно не оставлять только в журнале консоли.
В Sekura результат может оформляться как SJP — отдельный доказательный пакет.
Цепочка становится такой:
controller.sv
+
controller.sjv
│
▼
формальная проверка
│
▼
controller.sjpSJP фиксирует связь результата с конкретной реализацией, формальным контрактом, параметрами проверки и зависимостями.
Это позволяет сохранить доказательство вместе с проектом или передать его другой стороне.
Почему SJP важен именно для RTL
Аппаратные проекты особенно чувствительны к версиям.
Один и тот же модуль может собираться:
- с разными параметрами;
- с разными define;
- с разными пакетами;
- в разных конфигурациях иерархии.
Поэтому недостаточно сказать:
controller.sv был проверен.
Нужно знать точную конфигурацию, для которой построено доказательство.
SJP позволяет связать результат именно с этим набором входов.
Если один из них изменился, требуется новая проверка.
Формальная проверка не заменяет синтез
Даже идеально доказанный RTL всё равно нужно синтезировать и реализовать для целевой FPGA или ASIC.
Формальный верификатор проверяет логические свойства модели RTL. Он не отвечает автоматически на вопросы:
- проходит ли проект временные ограничения;
- помещается ли он в выбранную FPGA;
- корректно ли разведены физические сигналы;
- соответствует ли задержка памяти реальному устройству;
- нет ли проблем питания или аналоговых эффектов.
Поэтому нормальный процесс содержит несколько независимых этапов:
RTL
│
├──► формальная проверка
│
├──► моделирование
│
├──► синтез
│
└──► реализация на устройствеОни дополняют друг друга.
Формальная проверка не заменяет тесты
То же относится к моделированию и тестированию.
Формальные методы особенно сильны там, где свойство можно точно сформулировать математически: состояния, переходы, ограничения доступа, протоколы, счётчики, очереди, арбитраж.
Тесты удобнее для других задач: интеграции с окружением, производительности, временного поведения реальных устройств, сложных внешних протоколов и проверки целой системы.
Лучший результат обычно даёт сочетание обоих подходов.
Например:
тесты:
показывают практические сценарии
формальная проверка:
исследует всё пространство,
заданное модельюОдин метод закрывает слабые места другого.
С чего начать на реальном модуле
Для первого практического опыта лучше не брать сразу весь процессор или крупный системный блок.
Подходящий кандидат — небольшой модуль с понятным состоянием:
- счётчик;
- конечный автомат;
- FIFO;
- арбитр;
- регистр состояния;
- простой контроллер;
- небольшой блок памяти.
У такого компонента легче сформулировать несколько точных свойств и проверить, соответствует ли им реализация.
Например, для FIFO можно начать с трёх требований:
count никогда не превышает DEPTH
чтение пустой очереди запрещено
после успешной записи
count увеличивается на одинПосле этого уже можно переходить к более сложным зависимостям и композиционной проверке.
Основной принцип
Практический смысл формальной проверки RTL можно свести к одной цепочке:
SystemVerilog
│
▼
точная модель поведения
│
+
формальные свойства SJV
│
▼
математические обязательства
│
▼
решатель
│
▼
доказательство
│
▼
SJPГлавное здесь не само наличие решателя. Главная работа происходит раньше: нужно точно определить проверяемую конфигурацию RTL, построить корректную модель и сформулировать свойства, которые действительно имеют инженерный смысл.
Только после этого результат VERIFIED становится содержательным утверждением.
Он означает не «SystemVerilog-модуль вообще правильный», а гораздо более точную вещь:
для конкретной версии и конфигурации RTL в рамках заданной модели проверены конкретно перечисленные свойства.
Именно такая точность и делает формальную верификацию полезной инженерной практикой.
Документация
Поддерживаемое подмножество SystemVerilog.
Share
