Memora8: One Week of Simulator Alignment and Formal CPU Verification

AI Summary: From October 19 to 25, 2026, we aligned important parts of the independent mr8sim C++ emulator with the current Memora8 RTL and expanded formal checks against the real SystemVerilog implementation. The simulator now models eight separate pipeline slots, per-page SRAM ports, MMU waiting conditions, word-level PageMover streaming, PM2 buffers, and persistent 8 GiB virtual SD storage. Three Sekura JS module configurations produced LANGUAGE TESTS OK. Separate RTL/C++ programs matched 22/22 and 16/16 architectural COMMIT events. The public Assurance Memora8 repository records 859 proved SJV obligations, 51 expected counterexamples, and 51 SJP packages for selected properties across the 32 CPU opcodes. Neither the complete processor nor cycle-exact simulator equivalence is claimed to be proven.

During the past week, we made progress in two related areas of Memora8 development: checking the software emulator against the hardware architecture, and verifying mathematical properties of the actual processor RTL.

Memora8 is our custom 32-bit processor. Its development began with a software model that let us explore the instruction set and execute programs before the FPGA implementation existed. That model developed into mr8sim, an independent C++ emulator used for work on the Sekura JS language, the Reganta operating system, and system software.

The subsequent SystemVerilog implementation added hardware constraints that a simple instruction interpreter does not capture: registered memory responses, pipeline dependencies, physical port conflicts, asynchronous page transfers, and device protocols. This week’s simulator changes address those differences.

We also continued the formal verification work described in our earlier SystemVerilog verification report. The new result is a published, inspectable set of proof obligations covering selected computation and local-control properties for every CPU opcode.

Eight Pipeline Stages in the C++ Emulator

The most substantial CPU change was replacing the simplified pipeline representation with eight independently occupied instruction slots:

IFD-MMU → IFD-BRAM → IFD-RECV → LR
        → EX → MEM-MMU → MEM-BRAM → COMMIT

Each slot retains the instruction’s PC, decoded data, intermediate values, and control state. The text interface shows the contents of those slots, rather than projecting a smaller internal pipeline onto eight display rows.

The first three stages separate address translation, SRAM instruction access, and the registered fetch response. Until the instruction word has arrived, the interface displays FETCH... instead of a guessed mnemonic.

The execution model also handles arithmetic forwarding, RAW dependencies, resource stalls, branch cancellation, and exceptions carried with their instruction packets.

A useful example is a load followed by an instruction that consumes the loaded register. A sequential interpreter can return the load value immediately. A pipeline must preserve the dependency while the memory response is pending. In the updated model, LW captures its read result in MEM-BRAM; the architectural register change occurs at COMMIT.

The same distinction matters for exceptions. A fault detected before COMMIT must not let younger instructions leave architectural side effects, while older instructions are still allowed to retire in order.

These are real C++ state transitions, not a Verilator-controlled single-step interface. Some timing remains approximate, including selected hardware handshakes and the way long arithmetic operations stall the pipeline. We use the model to investigate functional behavior and instruction ordering; we do not call it cycle-accurate RTL.

SRAM Access Is Per Page, Not Per Bank

The current Memora8 067 cluster has eight CPUs and 1 MiB of shared SRAM, organized as 16 physical banks with eight 8 KiB pages per bank. In total there are 128 architectural physical pages.

During RTL comparison, we corrected a significant memory-model assumption.

In mr8_memory.sv, each physical page has two distinct access ports. Port A serves CPU data accesses; port B serves instruction fetches and PageMover. They are not two generic ports shared by an entire bank.

The revised C++ SharedSram model tracks access on that basis. Two operations on different pages of the same bank need not block each other, but competing requests for the same port of the same page cannot both succeed in one model cycle.

Multi-page operations check every required page before reserving any port. A rejected request must not leave the first page partially acquired.

We also tightened MMU context replacement and physical page ownership:

• A replacement context is validated before the old mappings are changed.
• Invalid or inaccessible pages, duplicate virtual mappings, and ownership conflicts cause rejection without partial updates.
• A mapped page in CLAIM, FLUSH, or LOADING causes an appropriate wait instead of a false unmapped-page exception.
• PageMover cannot silently acquire pages owned by another CPU.

The MTR exception path was brought closer to the RTL as well. A fault must preserve the PC of the offending instruction, its address, and the cause; installed handler and no-handler paths have different outcomes.

These details are relevant to Reganta because module loading and memory management depend on exactly these architectural rules.

System Bus and Asynchronous Page Transfers

Memora8 system devices are accessed through the SB and SBI instructions, using a 32-word System Bus window. Words 0–30 hold data and arguments; writing word 31 launches the operation:

DATA[0..30] = arguments / results
DATA[31]    = (CMD << 10) | DEVICE

The write to word 31 is the ordering point: device selection comes from that control word, not from DATA0. We aligned the emulator’s command decoding and lifecycle behavior with this contract.

For example, waking a sleeping CPU must preserve its saved PC and execution state. CPU_RESTART is a different command, requiring its own context checks.

PageMover was another major source of simplified behavior. An immediate page copy can produce the correct final bytes, but it cannot represent FIFO occupancy, a blocked destination, or a conflict over a physical SRAM port.

The optional word-streaming profile now transfers an 8 KiB page as 2,048 32-bit words. It models registered request/response stages and an eight-word FIFO. Source and destination readiness are independent, and backpressure retains data until it can be accepted.

For DDR and RAW backing stores, accepted words are written as the transfer progresses instead of always appearing only when the entire page is complete. Independent transfers can progress concurrently where their page and device resources permit it; overlapping resources are rejected.

This is a model of the relevant transfer contracts, not a complete simulation of the physical DDR3 MIG implementation or every FPGA timing path.

A Persistent 8 GiB Virtual SD Card

Reganta needs persistent storage, but a local mr8sim execution should not require an SD card connected to an FPGA.

We implemented a file-backed virtual SD image, created by default at .mr8sim/sdcard.img when running in simulator mode.

The image has a logical capacity of 8 GiB:

It is a sparse file, so a new empty image does not require 8 GiB of allocated disk blocks. The existing image is preserved between runs.

The data path follows the hardware-oriented PM2 buffer design. There are four external buffer pages, 0x400–0x403, separate from the CPU’s 128-page SRAM space. Each has a registered Bus port for PM0/PM1 and a Card port for PM2.

A page transfer proceeds through 16 sectors. Each sector contains 128 words. The model advances through initialization, sector-command and data phases, and completion on simulator ticks, rather than on wall-clock timers.

The regression test writes to the last page of a temporary 8 GiB image, inspects an intermediate sector, reopens the image, verifies that the full page survived the restart, and rejects an out-of-range request.

This does not reproduce the SD/SPI wire protocol bit for bit. The virtual device does not claim real MOSI/MISO, CRC, card initialization timing, or physical transfer-rate equivalence.

Running Static and Dynamic Sekura JS Modules

An independent simulator is most useful when it runs code generated by the real compiler.

This week we corrected how mr8sim loads SOBJ modules, including the entry_point field and the placement of TEXT and DATA sections into MMU windows.

A dynamically linked module starts through its entry stub at the relocated text base. A statically linked monolithic SOBJ can identify an entry point inside TEXT. Treating the start of TEXT as the entry for both forms was incorrect.

The loader now validates the original entry and preserves its offset after placement. Static DATA can also occupy a separate virtual region requiring its own MMU mapping.

We used the same Sekura JS source suite to check three build configurations:

The integration script requires the exact success message, rejects language-test errors, and checks that each execution retires at least 500 instructions. It compiles into a temporary directory rather than modifying the checked-in program images.

This tests more than individual opcodes. It exercises compiler output, module loading, entry selection, MMU placement, and actual instruction execution together.

Differential Checks Against the Real RTL

We use Verilator for separate RTL tests, not as mr8sim’s execution engine.

Selected machine-code programs are run independently against the SystemVerilog processor and the C++ emulator. We compare ordered architectural COMMIT events: PC, instruction word, destination register, and result.

The recorded comparisons include:

An additional C++ regression runs a branch program with and without systematic instruction-fetch backpressure. All 16 COMMIT events and the final general-purpose registers match between those simulator executions, despite different cycle counts.

Other CTest regressions cover SRAM port contracts, MMU waits, precise retirement, System Bus read hazards, PageMover FIFO backpressure, PM2 buffer ports and lifecycle, and virtual SD persistence.

These tests establish agreement for the scenarios actually exercised. They do not establish end-to-end ISA completeness, identical cycle counts, or full timing equivalence between mr8sim and the FPGA RTL.

Formal Verification Across All 32 Opcodes

In parallel with the simulator work, we extended SJV to check selected properties directly against the Memora8 SystemVerilog implementation.

The checker now supports additional RTL constructs required by the processor, including relevant always_ff and always_comb semantics, parameterized elaboration, hierarchical names, packed structures, arrays, and wide vectors.

A contract can refer to a named field in the actual RTL packet:

ex_packet.opcode == 0;
ex_result'.result ==
    (ex_packet.rs1_value + ex_packet.rs2_value)
    % 0x1_0000_0000;

The verifier derives field positions and widths from elaborated RTL. The operands remain symbolic rather than being restricted to a list of test values.

For multicycle computation, a bounded composition of clock transitions allows verification of selected arithmetic-unit results over several edges. The applicable input-hold and control assumptions are recorded for each proof profile.

The public coverage currently consists of:

• 23 local EX computation/control slices for arithmetic, shifts, comparisons, branches, local memory properties, and SB/SBI behavior.
• Nine isolated multicycle results for multiply, divide, remainder, and MSB/MSBI operations.

The corresponding coverage index records 859 proved SJV obligations and 51 expected counterexamples. The current evidence set includes 51 SJP packages.

An updated core recheck accounts for 585 of those proved obligations, 28 expected counterexamples, 28 SJP packages, and 1,161 matching replayed SAT/UNSAT queries. These counts are included in the overall evidence; they are not extra obligations to add to the totals.

For division, the proof basis includes arithmetic invariants and a composed numerical argument. That composition has its own explicitly trusted checker. Replaying an SJP’s stored SMT queries validates those queries’ reported results, but it does not independently validate every step by which the private RTL was translated into them.

The distinction between local computation and full processor behavior remains essential. An opcode having a proved computation slice does not mean its complete execution has been proved from fetch through retirement.

Open Assurance Evidence, Private Processor Source

We published the verification evidence in a separate GitLab project:

Assurance Memora8 — public repository

It provides the contracts, requirements, coverage index, selected proof reports, and reproducibility information.

Useful entry points are:

• CPU-ISA-COMPUTE requirement
• CPU opcode coverage index
• Current formal verification results
• ADD contract example

The Memora8 processor RTL and the SJV implementation are not included in this public repository. Publishing contracts and proof artifacts does not imply releasing the processor or checker source code.

The scoped CPU-ISA-COMPUTE requirement has recorded FORMAL evidence in Noda Assurance and a COVERED traceability result. Its parent CPU-ISA-32 remains GAP. Noda records evidence and its relationship to requirements; it does not execute the verification tools or independently certify the processor.

For background on the distinction between shareable evidence and source-code provenance, see Proof Without Disclosing Source Code.

What These Results Establish

This week’s work improved mr8sim as an independent environment for testing the behavior of Memora8 programs and devices. It also gave us a stronger way to compare selected architectural events with the processor’s SystemVerilog implementation.

Formal verification now provides published mathematical evidence for selected local computation and control properties of all 32 opcodes.

The next verification problem is larger: proving correct instruction movement, operand selection, forwarding, cancellation, memory ordering, exception behavior, and exactly-once architectural effects through COMMIT.

Those results cannot be inferred merely from local arithmetic proofs or successful simulator runs.

The value of an independent emulator is not only that it runs programs without the physical processor. Together with formal contracts and RTL comparisons, it helps expose disagreements between the intended architecture, its hardware implementation, and the software running on it.

Memora8 is developed by Jupiter Soft, Kazakhstan, as part of the Sekura technology initiative. This report covers changes and recorded verification results from October 19–25, 2026.

Technical basis: Memora8 RTL and mr8sim C++ revisions from October 24–25, 2026; mr8sim/RTL_ALIGNMENT.md; simulator regression and COMMIT comparison tests; and public Assurance Memora8 evidence at revision d8e94fe.