During October 19–25, Memora8 advanced its independent C++ emulator and the formal verification of its SystemVerilog RTL. mr8sim gained a more faithful eight-stage pipeline, per-page SRAM port arbitration, word-streamed PageMover and a persistent sparse 8 GiB SD image. Static and dynamic Sekura JS programs passed language tests; selected RTL/C++ traces matched 22/22 and 16/16 COMMIT events. The open Assurance Memora8 repository records 859 proved obligations, 51 expected counterexamples and 51 SJP packages for scoped properties across all 32 opcodes.
qNac: High-Precision Mathematics Without an FPU for Memora8
qNac is a Sekura JS mathematical library for Memora8 that implements qNac64 and qNac32f using integer instructions, multiword arithmetic, and CORDIC algorithms. Simulator benchmarks report qNac32f at 11.83× the speed of qNac64 for one 1,300-check workload; the result is specific to that test and is not a hardware FPU comparison.
Memora8: Eight-Core FPGA System Fits Artix-7 200T
On October 17, 2026, the complete Memora8 digital architecture passed synthesis, placement, routing, and timing analysis on an Artix-7 XC7A200T. This report covers the eight-core processor cluster, 1 MiB SRAM, System Bus, planned peripheral logic, the LOAD/STORE pipeline redesign, and implementation results: 90.2% LUT use, 84.5% Block RAM use, and +0.030 ns WNS. The bitstream was generated, while validation of external devices on the physical BX72 board remains future work.
Memora8: One Week of Building an Eight-Core FPGA Computer
From October 3 to 10, 2026, Memora8 added physical microSD, UART, and GPIO tests, integrated BLAKE3 and Ed25519 VERIFY, and optimized PageMover while retaining a routed 125 MHz eight-core Artix-7 build. This report summarizes the measured results and the next steps: a custom Ethernet controller and incremental formal verification.
Memora8 FPGA Implementation: 8-Core Artix-7 Status
As of October 4, 2026, the Memora8 FPGA implementation combines eight 32-bit CPU cores, 1 MiB of banked SRAM, MMU page windows, SYSTEM BUS devices, PageMover, DDR3/MIG connectivity, and UDP debug for the BX72 Artix-7 XC7A200T. The completed routed build meets 125 MHz timing, but the reported integration tests use a simulated DDR3/MIG and bypass physical Ethernet MAC/RGMII; board-level operation and the planned cryptographic accelerators remain future work.
Sekura JS Formal Verification: A First Step Toward Evidence for the Language
Assurance Sekura JS establishes an initial, inspectable evidence base for selected properties of compiled programs. This article explains the source-to-object-to-contract chain, the current evidence across five language areas, optimization profiles O0–O4, restricted preconditions, and why test results, formal proofs, signatures, and SMT replay must not be conflated.
Proof Without Disclosing Source Code: How SJV Contracts and SJP Packages Support Independent Verification
Source code may need to remain private, but verification evidence can still be shared. This article explains how SJV defines the properties under review and how an SJP package carries verification results and replayable SMT obligations. It distinguishes contract scope, package integrity, Ed25519 signatures, and proof provenance, and makes clear that replaying stored obligations alone does not prove they were generated from the claimed private source revision.
Sekura Noda Assurance: Requirements, Verification, and Engineering Evidence
Sekura Noda Assurance helps engineering teams preserve why a claim is supported for a specific system version. It links requirements, specifications, implementations, verification runs, and evidence; tracks coverage and freshness; and records immutable baselines. Noda organizes evidence but does not run verification tools or certify compliance with industry standards.
Formal Verification of SystemVerilog in Memora8: RTL Contracts and Proof Scope
Memora8 is developing a formal verification path for real SystemVerilog modules. This article explains why simulation and formal methods complement each other, how RTL properties are checked, what the current SystemVerilog subset supports, how SJP binds results to RTL and contracts, and why verification claims are made property by property.
Memora8 Memory Architecture: K4,4 Topology Closes 125 MHz Timing on Artix-7
A report on finalizing the baseline Memora8 cluster memory geometry: 8 CPUs, 16 physical shared banks, 32 logical banks, 128 pages of 8 KiB, and 1 MiB SRAM. The K4,4 topology routed on an Artix-7 XC7A200T at 125 MHz with positive timing slack and one-cycle CPU reads; full integration with the MMU and other processor blocks remains to be verified.