Formal Verification of SystemVerilog in Memora8

AI Summary: Memora8 is developing a dedicated formal verification path for SystemVerilog RTL. Machine-checkable contracts describe the properties hardware must satisfy, and a formal model searches for valid states or transitions that violate them. Current work includes real modules such as a memory page, pipeline registers, the System Bus command dispatcher, and the snapshot endpoint. Results are reported per property as VERIFIED, FAILED with a counterexample, or UNSUPPORTED when required RTL semantics are not modeled. SJP artifacts bind results to the specific RTL, contract, and verification configuration. The complete CPU is not yet formally proven; expanding the supported SystemVerilog semantics and hierarchical modeling remains necessary.

Memora8 is being developed as a processor architecture in which hardware correctness should be checked not only through simulation, but also through formal verification. For that purpose, we are building a dedicated verification path for SystemVerilog RTL and gradually converting critical processor properties into machine-checkable contracts.

The basic idea is straightforward: RTL describes how a hardware block behaves, while a formal contract defines what that block must guarantee. The verification system builds a mathematical model of the RTL and searches for any valid state in which the contract can be violated. If such a state exists, the result is a counterexample. If no violation can be found within the supported model, the property is marked VERIFIED.

Why Simulation Alone Is Not Enough

Simulation remains an essential part of processor development. It is useful for running instruction sequences, checking data transfers between blocks, observing pipeline behavior, and validating complete execution scenarios.

Its limitation is equally clear: simulation only checks the scenarios that were explicitly created. If a rare combination of signals or an unusual sequence of internal states was never included, simulation will not discover it on its own.

Formal verification asks a different question. Instead of checking one selected example, it defines a rule and asks whether any valid state exists in which that rule stops being true.

For example, simulation may check that a particular value is written to a particular memory address. A formal contract can express a broader requirement: whenever a write is enabled, the selected memory location must receive the supplied value, regardless of the specific address or data.

The two approaches therefore answer different questions. Simulation asks, “Did this scenario behave correctly?” Formal verification asks, “Is there any valid scenario that can violate this rule?”

Why This Matters Especially for a Processor

A processor contains many stateful elements: registers, queues, memories, control machines, buses, and pipeline stages. The behavior of one block often depends not only on current inputs, but also on what happened several clock cycles earlier.

A failure may appear only after a specific sequence of events: one command is delayed, another block changes state, a bus transaction arrives at the same time, and a later transition exposes the problem. Writing every such sequence manually is not realistic.

A formal contract makes the requirement explicit. For example, if a pipeline register is not enabled, its value must remain unchanged on the next cycle. The verification system then searches for any valid history that could violate that property.

This makes formal verification particularly useful for pipelines, arbitration logic, FIFOs, memory behavior, and communication protocols between processor blocks.

Verifying Real Memora8 Memory RTL

Formal verification in Memora8 is already being applied to real RTL modules. One example is the mr8_mem_067_page memory block:

logic [31:0] mem [0:2047];

This represents 2048 words of 32 bits each. In the formal model, the memory is represented as a single SMT array. Reading selects a value by address, while writing produces a new memory state with the selected location updated.

This representation allows addresses and data to remain symbolic instead of being fixed to predefined test values.

On the real MR8 RTL, we already verify write behavior and synchronous reading of the final word at address 2047. Additional checks cover read latency, matching and different read/write addresses, and an intentionally incorrect assumption about same-address read/write behavior.

The last case is especially important. If the assumption is wrong, the system must produce a concrete counterexample. Formal verification is valuable not only when it confirms correct behavior, but also when it exposes an incorrect understanding of the hardware.

Formal Verification Also Clarifies the Architecture

Formal verification is not only a way to find bugs in SystemVerilog. It also forces architectural assumptions to become precise.

A statement such as “memory returns the written value” is incomplete. When does that value become visible? In the same cycle or the next one? What happens if the same address is read and written at the same time? What happens during reset?

As long as such assumptions exist only in documentation or in a developer’s head, different blocks may interpret them differently. A formal contract turns them into explicit statements that can be checked.

For Memora8, this is especially important at the boundaries between the CPU, memory, and System Bus. Those blocks must agree on when state changes, when data becomes valid, and what behavior is guaranteed on the next clock cycle.

Why We Use a SystemVerilog Subset

SystemVerilog is a large language, and implementing its complete formal semantics before verifying any real Memora8 block would be impractical.

Instead, we support the subset that is actually required by Memora8 RTL.

The current formal model covers combinational logic, always_ff, register transitions, static procedural for loops, case, enum constants, $clog2, bit selection, part selection, and fixed one-dimensional memories.

When a new processor block depends on a SystemVerilog construct that is not yet modeled, the semantics of that construct are added first. Only then can the block become part of the verified area.

This keeps the verification system directly tied to the development of the processor itself.

Why UNSUPPORTED Matters

In formal verification, knowing the boundary of the proof is as important as the proof itself.

Successfully parsing a SystemVerilog module does not mean its behavior has been verified. A construct may be syntactically understood while still lacking a formal semantic model.

For that reason, verification results are explicitly separated into three states:

• VERIFIED: the property has been proven within the supported model;
• FAILED: a counterexample has been found;
• UNSUPPORTED: the required RTL semantics are not yet implemented.

This is preferable to silently treating partially understood hardware as verified. For Memora8, we want to know exactly which properties are proven and which parts remain outside the current formal model.

One Module Can Have Several Independent Proofs

A hardware module should not receive a single generic label such as “verified” or “not verified.” Different properties of the same module may have different results.

For a memory block, write correctness, read latency, boundary-address behavior, and same-address read/write semantics can all be checked independently. For a register, update and hold behavior may be separate contracts. For System Bus logic, different command transitions may have their own properties.

A single .sv module can therefore be checked against multiple .sjv contracts, each producing its own result.

This gives a much more precise statement than “the memory module was verified.” Instead, we can say that a specific write property is proven, a synchronous-read property is proven, while another behavior is still outside the supported model.

SJP Binds the Proof to a Specific Implementation

Each formal verification result is stored in a separate SJP artifact. It is tied to a specific RTL version, a specific contract, and the corresponding verification configuration.

This matters during long-term processor development. If the RTL changes, an old proof should not automatically remain valid for the new implementation.

The contract can be checked again against the updated RTL, producing a new result. In this way, formal verification becomes a continuous mechanism for preserving architectural guarantees rather than a one-time validation step.

Simulation and Formal Verification Serve Different Purposes

The goal in Memora8 is not to replace simulation with formal verification. They complement each other.

Simulation is useful when we want to observe real execution scenarios: running programs, moving data between blocks, processing command sequences, and checking integration behavior.

Formal verification is useful when we need to establish an architectural rule: a register must not change without enable, an invalid state must never occur, a boundary memory address must behave correctly, or an interface must preserve a required protocol.

In practice, simulation helps us observe system behavior, while formal verification helps us prove selected invariants and search for rare violations.

From Individual Properties to the Processor Core

Formal verification is already being applied to selected Memora8 blocks, including pipeline registers, a memory page, the System Bus command dispatcher, and the snapshot endpoint.

The complete CPU is not yet considered formally proven. Additional SystemVerilog semantics and hierarchical modeling are still required before larger portions of the processor can enter the verified area.

That gradual approach is intentional. The goal is not to claim that the entire processor is “formally verified” as early as possible. Each property should have a clearly defined scope and a real proof.

The long-term objective is to extend this approach from individual registers and memory pages to larger subsystems and, eventually, to the Memora8 processor core itself. Architectural guarantees should exist not only in documentation, but also as machine-checkable contracts bound to the actual RTL implementation.