The post has been translated automatically. Original language: Russian
When developing Memora8, RTL simulation alone is not enough. The processor consists of registers, a pipeline, memory, System Bus, queues, and control machines, and an error can occur only with a rare combination of states and signals. For a software error, it is often enough to release an update. For an error in an already manufactured processor, the cost of correction is much higher, so some of the properties must be checked at the SystemVerilog level.
Formal verification solves exactly this problem. It does not replace the usual simulation checks, but complements them with another control method: the simulation shows the behavior of the circuit in selected scenarios, and the formal check looks for any acceptable scenario in which a given property may be violated.
Checking examples and verifying rules
Let's take an Mr8 memory page with 2048 words of 32 bits each. In a normal simulation, you can write several values at different addresses, check the read, check the first and last addresses separately, and then add simultaneous reads and writes.
Such verification is useful, but it only confirms pre-selected scenarios. If some option was not provided, the simulation itself will not find it.
Formal verification allows you to set the rule itself. For example: if recording is allowed, after a clock cycle, the selected memory location must contain the recorded value. The address and data can remain arbitrary within the specified limits. The system tries to find a combination that violates this rule.
The practical difference is simple. In the simulation, we ask: "is this value being written correctly at this address?". In formal verification, the question is different: "is there a valid address and value at which the write rule is violated?".
The sequence of states is more important than one clock cycle
It's not just the state of the inputs and outputs at a particular moment that matters to the processor. The result often depends on what happened a few bars before.
For example, the pipeline register can be updated only if there is a permissive signal. A typical simulation checks several prepared sequences: an update is allowed, it is forbidden, a reset has occurred, and the following command has arrived.
The formal contract sets a general rule: if there is no update condition, the register value should not change on the next clock cycle. After that, the system searches for any valid sequence of states capable of violating this requirement.
This approach is especially useful for pipeline, command dispatchers, FIFO, and arbitration, where the error often depends not on a single signal, but on a combination of several previous events.
Checking the real Memora8 memory
Formal verification in Memora8 is already applied to real RTL modules. One of them is mr8_mem_067_page:
logic [31:0] mem [0:2047]
This is a memory page of 2048 words in 32 bits. In the mathematical model, it is represented as a single array: a read operation selects a value at an address, and a write operation creates a new memory state with a modified cell.
The recording and synchronous reading of the last word at address 2047 are already being checked on real RTL. The read delay, matching and different read and write addresses, as well as intentionally incorrect assumptions about memory behavior when writing and reading the same address are checked separately.
The latter case is especially important. If the formulated property is incorrect, the system must show a specific counterexample. This allows you to detect not only an error in the RTL, but also a developer's misconception of how the scheme should work.
Where formal verification is particularly useful
A regular simulation is well suited for testing normal operating scenarios: command sequences, data exchange between blocks, program loading, and overall system operation. But it depends on which cases the developer decided to check in advance.
The formal approach is especially useful where it is important to ensure that there are no rare exceptions: at boundary memory addresses, during transitions between states, in states of an empty or full queue, during simultaneous requests, when holding a register, and in situations that, according to the architecture, should not occur at all.
For a processor, such cases are fundamental. The error may not manifest itself in thousands of common operations and may occur only with one specific sequence of signals.
Not only the implementation is checked, but also the architectural rule.
Sometimes the problem is not in the SystemVerilog code, but in the expectations of it. For example, a developer may assume that when writing and reading a single address, the memory should immediately return a new value. The actual scheme may have different synchronous semantics.
During a routine check, the expected result is set by the developer himself, so it is easy to transfer an erroneous assumption into a verification scenario. A formal contract makes an assumption a separate statement that needs to be proved. If it is incorrect, the system shows the state in which it is being violated.
For Memora8, this is important at the boundaries between CPU, memory, and System Bus. Different parts of the processor must equally understand when the state changes, when the data becomes valid, and what behavior is guaranteed on the next clock cycle.
Why is a subset of SystemVerilog used?
SystemVerilog is a big language, and there is no need to implement it completely right away to test Memora8. We chose a practical approach: to support those designs that are actually used in the RTL processor.
Combinational logic, always_ff, register transitions, and static loops are now supported. for, case, enum constants, $clog2, selection of individual bits and ranges, as well as fixed one-dimensional memory arrays.
Support is expanding along with the processor itself. If a new SystemVerilog construct is required for the next CPU block, its exact semantics are added first, after which this block can be included in the formal verification area.
Unsupported design is not considered proven
For formal verification, the exact boundary between what is actually verified and what the tool is not yet able to model is especially important.
If a SystemVerilog module has been successfully disassembled, this does not mean that its behavior has been proven. If there is a construction for which formal semantics has not yet been implemented, the result is UNSUPPORTED.
Three basic states are used:
VERIFIED — the specified property is proven.;
FAILED — a counterexample has been found.;
UNSUPPORTED — the proof cannot be performed in the current version of the formal model.
This approach is better than partially checking the module and implicitly considering the result to be complete. For Memora8, it is important to know exactly which properties already have proof, and which parts of the processor are still outside the supported area.
One module can have several independent proofs.
The formal verification does not apply to a module in general, but to a specific property of that module. For a single memory page, you can separately check the write, synchronous read, boundary address, and behavior when the read and write addresses match.
One property can get VERIFIED, another can get FAILED, and the third can get UNSUPPORTED. This is much more accurate than the general mark "module tested".
For each such contract, a separate SJP is generated, associated with a specific RTL version and a specific verifiable property.
A practical role for Memora8
The main task of formal verification in Memora8 is to preserve architectural guarantees during processor development. Today, you can prove the operation rule of a register or memory, then change the pipeline, rebuild the System Bus, or optimize the internal implementation and re-check the same properties.
As a result, the processor requirements gradually cease to exist only in the documentation and in the developer's memory. They turn into machine-readable contracts that can be automatically validated on each new RTL version.
For Memora8, simulation and formal verification perform different tasks. The simulation shows how the processor works in specific scenarios. Formal verification checks architectural rules and looks for rare combinations that can violate them. As the supported subset of SystemVerilog expands, the scope of such evidence can grow from individual registers and memory pages to large subsystems and, subsequently, the Memora8 processor core.
При разработке Memora8 одной симуляции RTL недостаточно. Процессор состоит из регистров, конвейера, памяти, System Bus, очередей и управляющих автоматов, а ошибка может проявиться только при редком сочетании состояний и сигналов. Для программной ошибки часто достаточно выпустить обновление. Для ошибки в уже изготовленном процессоре цена исправления значительно выше, поэтому часть свойств необходимо проверять ещё на уровне SystemVerilog.
Формальная верификация решает именно эту задачу. Она не заменяет обычные симуляционные проверки, а дополняет их другим способом контроля: симуляция показывает поведение схемы в выбранных сценариях, а формальная проверка ищет любой допустимый сценарий, в котором заданное свойство может нарушиться.
Проверка примеров и проверка правила
Возьмём страницу памяти Mr8 на 2048 слов по 32 бита. При обычной симуляции можно записать несколько значений по разным адресам, проверить чтение, отдельно проверить первый и последний адрес, затем добавить случаи одновременного чтения и записи.
Такая проверка полезна, но она подтверждает только заранее выбранные сценарии. Если какой-то вариант не был предусмотрен, симуляция сама его не найдёт.
Формальная проверка позволяет задать само правило. Например: если запись разрешена, после такта выбранная ячейка памяти должна содержать записанное значение. Адрес и данные при этом могут оставаться произвольными в пределах заданных ограничений. Система пытается найти комбинацию, которая нарушает это правило.
Практическая разница проста. При симуляции мы спрашиваем: «правильно ли записывается это значение по этому адресу?». При формальной проверке вопрос звучит иначе: «существует ли допустимый адрес и значение, при которых правило записи нарушится?».
Последовательность состояний важнее одного такта
Для процессора важно не только состояние входов и выходов в конкретный момент. Результат часто зависит от того, что происходило несколько тактов до этого.
Например, регистр конвейера может обновляться только при наличии разрешающего сигнала. Обычная симуляция проверяет несколько подготовленных последовательностей: обновление разрешено, запрещено, произошёл сброс, пришла следующая команда.
Формальный контракт задаёт общее правило: если условие обновления отсутствует, значение регистра на следующем такте не должно измениться. После этого система ищет любую допустимую последовательность состояний, способную нарушить это требование.
Такой подход особенно полезен для конвейера, диспетчеров команд, FIFO и арбитража, где ошибка нередко зависит не от одного сигнала, а от комбинации нескольких предыдущих событий.
Проверка реальной памяти Memora8
Формальная верификация в Memora8 уже применяется к реальным RTL-модулям. Один из них — mr8_mem_067_page:
logic [31:0] mem [0:2047]
Это страница памяти размером 2048 слов по 32 бита. В математической модели она представляется единым массивом: операция чтения выбирает значение по адресу, операция записи создаёт новое состояние памяти с изменённой ячейкой.
На реальном RTL уже проверяются запись и синхронное чтение последнего слова по адресу 2047. Отдельно проверяются задержка чтения, совпадающие и разные адреса чтения и записи, а также намеренно неверное предположение о поведении памяти при одновременной записи и чтении одного адреса.
Последний случай особенно важен. Если сформулированное свойство неверно, система должна показать конкретный контрпример. Это позволяет обнаруживать не только ошибку в RTL, но и неверное представление разработчика о том, как должна работать схема.
Где формальная верификация особенно полезна
Обычная симуляция хорошо подходит для проверки нормальных рабочих сценариев: последовательности команд, обмена данными между блоками, загрузки программы и общей работы системы. Но она зависит от того, какие случаи разработчик решил проверить заранее.
Формальный подход особенно полезен там, где важно гарантировать отсутствие редких исключений: на граничных адресах памяти, при переходах между состояниями, в состояниях пустой или полной очереди, при одновременных запросах, при удержании регистра и в ситуациях, которые по архитектуре вообще не должны возникать.
Для процессора такие случаи принципиальны. Ошибка может не проявляться в тысячах обычных операций и возникнуть только при одной специфической последовательности сигналов.
Проверяется не только реализация, но и архитектурное правило
Иногда проблема находится не в SystemVerilog-коде, а в ожиданиях от него. Например, разработчик может считать, что при записи и чтении одного адреса память должна сразу возвращать новое значение. Реальная схема может иметь другую синхронную семантику.
При обычной проверке ожидаемый результат задаётся самим разработчиком, поэтому ошибочное предположение легко перенести в проверочный сценарий. Формальный контракт делает предположение отдельным утверждением, которое необходимо доказать. Если оно неверно, система показывает состояние, в котором оно нарушается.
Для Memora8 это важно на границах между CPU, памятью и System Bus. Разные части процессора должны одинаково понимать, когда меняется состояние, когда данные становятся действительными и какое поведение гарантируется на следующем такте.
Почему используется подмножество SystemVerilog
SystemVerilog — большой язык, и для проверки Memora8 нет необходимости сразу реализовывать его полностью. Мы выбрали практический подход: поддерживать те конструкции, которые действительно используются в RTL процессора.
Сейчас поддерживаются комбинационная логика, always_ff, переходы регистров, статические циклы for, case, enum-константы, $clog2, выбор отдельных битов и диапазонов, а также фиксированные одномерные массивы памяти.
Поддержка расширяется вместе с самим процессором. Если для следующего блока CPU требуется новая конструкция SystemVerilog, сначала добавляется её точная семантика, после чего этот блок можно включать в область формальной проверки.
Неподдерживаемая конструкция не считается доказанной
Для формальной верификации особенно важна точная граница между тем, что действительно проверено, и тем, что инструмент пока не умеет моделировать.
Если SystemVerilog-модуль успешно разобран, это ещё не означает, что его поведение доказано. Если встречается конструкция, для которой формальная семантика ещё не реализована, результатом становится UNSUPPORTED.
Используются три основных состояния:
VERIFIED — заданное свойство доказано;
FAILED — найден контрпример;
UNSUPPORTED — доказательство невозможно выполнить в текущей версии формальной модели.
Такой подход лучше, чем частично проверить модуль и неявно считать результат полным. Для Memora8 важно точно знать, какие свойства уже имеют доказательство, а какие участки процессора ещё находятся за пределами поддерживаемой области.
Один модуль может иметь несколько независимых доказательств
Формальная проверка относится не к модулю вообще, а к конкретному свойству этого модуля. Для одной страницы памяти можно отдельно проверять запись, синхронное чтение, граничный адрес и поведение при совпадении адресов чтения и записи.
Одно свойство может получить VERIFIED, другое — FAILED, третье — UNSUPPORTED. Это значительно точнее общей отметки «модуль проверен».
Для каждого такого контракта формируется отдельный SJP, связанный с конкретной версией RTL и конкретным проверяемым свойством.
Практическая роль для Memora8
Главная задача формальной верификации в Memora8 — сохранить архитектурные гарантии при развитии процессора. Сегодня можно доказать правило работы регистра или памяти, затем изменить конвейер, перестроить System Bus или оптимизировать внутреннюю реализацию и повторно проверить те же свойства.
В результате требования к процессору постепенно перестают существовать только в документации и в памяти разработчика. Они превращаются в машиночитаемые контракты, которые можно автоматически проверять на каждой новой версии RTL.
Для Memora8 симуляция и формальная верификация выполняют разные задачи. Симуляция показывает работу процессора в конкретных сценариях. Формальная верификация проверяет архитектурные правила и ищет редкие комбинации, способные их нарушить. По мере расширения поддерживаемого подмножества SystemVerilog область таких доказательств может расти от отдельных регистров и страниц памяти до крупных подсистем и, в дальнейшем, процессорного ядра Memora8.
Share
