_   _                    _____        _____
 | \ | |                  / ____|      / ____|
 |  \| |_   _  __ _ _ __ | (___   ___ | |
 | . ` | | | |/ _` | '_ \ \___ \ / _ \| |
 | |\  | |_| | (_| | | | |____) | (_) | |____
 |_| \_|\__, |\__,_|_| |_|_____/ \___/ \_____|
         __/ |
        |___/

A small, formally verified RISC-V SoC targeting the Tang Nano 20K FPGA. Goal: boot full MMU Linux (Sv32) on a $18 board.

Features

• nyanrv — RV32IMA + Zicsr soft CPU
  • M-mode and S-mode privilege levels, full trap delegation (medeleg/mideleg)
  • Sv32 two-level hardware page-table walker with 16-entry direct-mapped TLB
  • Timer (MTI/STI) and external (MEI/SEI) interrupts
• UART TX/RX — parameterised baud-rate, formally verified
• SDRAM controller — GW2AR-18 embedded SDRAM (32 MB), direct CPU address mapping at 0x8000_0000
• SPI SD card controller — SPI-mode SD card, full init + block read/write
• CLINT — mtime / mtimecmp at 0x0200_0000 (ACLINT-compatible)
• PLIC — 1 source (UART RX), 1 S-mode context at 0x0C00_0000 (SiFive-compatible)
• UART loader — upload and run programs over UART without reflashing the FPGA
• OpenSBI — ported to NyanSoC; fw_jump.bin (258 KB) builds cleanly
• Formally verified with riscv-formal and SymbiYosys

Status

Component	Status
nyanrv CPU (RV32IMA + Zicsr)	✅ Done, formally verified
UART TX/RX	✅ Done, formally verified
SPI SD card controller	✅ Done, tested
SDRAM controller + direct CPU mapping	✅ Done, hardware verified
CLINT (mtime / mtimecmp)	✅ Done, tested
S-mode CSRs + privilege tracking	✅ Done, sim-tested
Sv32 MMU (PTW + TLB)	✅ Done, sim-tested
PLIC	✅ Done, hardware verified
OpenSBI port	✅ Done, hardware verified
UART loader + SDRAM instruction fetch	✅ Done, hardware verified
Linux kernel build	🔄 WIP — configs ready, needs Linux build host
SD card boot	❌ Not started (bootloader firmware exists)

Directory structure

NyanSoC/
├── rtl/
│   ├── nyanrv.v              # RV32IMA + Zicsr CPU (M+S mode, Sv32 MMU)
│   ├── plic.v                # PLIC (1 source, 1 S-mode context)
│   ├── uart/
│   │   ├── uart_tx.v         # UART transmitter
│   │   └── uart_rx.v         # UART receiver
│   ├── sdspi/
│   │   └── sdspi.v           # SPI SD card controller
│   ├── gowin/
│   │   └── sdram_gw2ar.v     # SDRAM controller for GW2AR embedded SDRAM
│   └── sim/                  # Simulation testbenches + RV32 assembly test suite
├── boards/
│   └── tangnano20k/
│       ├── top.v             # SoC top-level (CPU + all peripherals)
│       ├── Makefile          # Synthesis, P&R, flash targets
│       ├── nyansoc.dts       # Device Tree Source for Linux
│       └── nyansoc.dtb       # Compiled DTB (generated by `dtc`)
├── firmware/
│   ├── start_ram.S           # Shared CRT0 for UART-loader-uploaded programs
│   ├── link_ram.ld           # Shared linker script for RAM-targeted binaries
│   ├── uart_loader/          # UART loader firmware (lives in IMEM LUT-ROM)
│   ├── bootloader/           # SD card bootloader (lives in IMEM LUT-ROM)
│   ├── hello_world/          # "Hello, World!" over UART
│   ├── echo/                 # UART echo
│   ├── blinky/               # LED blink
│   ├── sbi_stub/             # Minimal S-mode stub kernel for OpenSBI testing
│   ├── smode_test/           # S-mode CSR / privilege test
│   ├── plic_test/            # PLIC register + interrupt test
│   ├── clint_test/           # CLINT timer test
│   ├── sdram_test/           # SDRAM read/write test
│   └── mmu_test/             # Sv32 MMU test
├── sw/
│   ├── Makefile              # Build OpenSBI, sbi_stub, SD card image
│   ├── opensbi/              # OpenSBI git submodule (v1.8.1)
│   ├── opensbi-platform/     # NyanSoC platform port for OpenSBI
│   ├── opensbi-no-pie.patch  # Patch to build OpenSBI with bare-metal toolchain
│   ├── linux-nyansoc.config  # Linux 6.6 kernel config for NyanSoC (WIP)
│   └── buildroot-nyansoc.config  # Buildroot config (toolchain + BusyBox + kernel, WIP)
├── scripts/
│   ├── uart_load.py          # Host-side UART loader script
│   └── make_sd_image.sh      # Assemble raw SD card image
└── formal/
    ├── nyanrv/               # riscv-formal config and wrapper for nyanrv
    └── Makefile              # Formal verification flow

Memory map

Address range	Region
0x0000_0000–0x0000_0FFF	IMEM (4 KiB, combinatorial LUT-ROM)
0x0001_0000–0x0001_0FFF	DMEM (4 KiB, BRAM, R/W)
0x0002_0000	GPIO — bits [5:0] drive LED[5:0]
0x0003_0000	UART RX — read: {23'b0, valid, data[7:0]} (clears valid)
0x0003_0004	UART TX — write: send byte; read: {31'b0, busy}
0x0004_0000–0x0004_000C	SD card controller (status / cmd / addr / data)
0x0005_0000–0x0005_0008	SDRAM register-mapped (legacy diagnostic interface)
0x0200_0000–0x0200_000C	CLINT — mtime lo/hi, mtimecmp lo/hi
0x0C00_0004	PLIC source 1 priority (3-bit)
0x0C00_1000	PLIC pending word 0 (bit 1 = UART RX)
0x0C00_2000	PLIC enable context 0 word 0
0x0C20_0000	PLIC threshold context 0
0x0C20_0004	PLIC claim/complete context 0
0x8000_0000–0x81FF_FFFF	SDRAM direct mapping (32 MB) — Linux lives here

Instruction fetch from 0x8000_0000–0x81FF_FFFF is supported: the CPU can execute code loaded into SDRAM (used by the UART loader).

Prerequisites

Tool	Purpose
OSS CAD Suite	yosys, nextpnr, iverilog, sby
openFPGALoader	Flashing the FPGA
riscv-gnu-toolchain	Cross-compiler for firmware and sim tests
dtc	Device Tree Compiler (for nyansoc.dtb)
python3 + pyserial	UART loader host script

# Install pyserial
pip3 install pyserial

# Compile the Device Tree Blob
dtc -I dts -O dtb -o boards/tangnano20k/nyansoc.dtb boards/tangnano20k/nyansoc.dts

Quick start

# Run all CPU simulation tests
make sim

# Run formal proofs and cover checks
make prove
make cover

# Build and flash a firmware bitstream (default: bootloader)
make -C boards/tangnano20k FW=hello_world flash-sram   # volatile SRAM
make -C boards/tangnano20k FW=hello_world flash         # persistent SPI flash

UART loader (recommended development workflow)

Flash the UART loader once, then upload and run any firmware over UART without rebuilding the bitstream.

# Step 1 — flash the loader firmware (one time)
make -C boards/tangnano20k FW=uart_loader flash-sram

# Step 2 — build a RAM-targeted binary for any firmware
make -C firmware/hello_world bin BIN_ADDR=0x80000000

# Step 3 — upload and run (stays connected, Ctrl+C to exit)
python3 scripts/uart_load.py -p /dev/tty.usbserial-XXXX run \
    firmware/hello_world/hello_world.bin 0x80000000

Other loader commands:

# Ping the board
python3 scripts/uart_load.py -p PORT ping

# Upload without jumping
python3 scripts/uart_load.py -p PORT load firmware.bin 0x80000000

# Jump to a previously loaded address
python3 scripts/uart_load.py -p PORT go 0x80000000 --stay

# Dump memory as hex
python3 scripts/uart_load.py -p PORT dump 0x80000000 256

Protocol (all multi-byte values big-endian):

Cmd	Host sends	Board replies
P	P	O
L	L + addr(4) + len(4) + data + XOR checksum(1)	K or E
G	G + addr(4)	(jumps, no reply)
D	D + addr(4) + len(4)	raw bytes

Building OpenSBI

# Build fw_jump.bin (loads at 0x8000_0000, jumps to kernel at 0x8020_0000)
make -C sw opensbi

# Output: sw/opensbi/build/platform/nyansoc/firmware/fw_jump.bin (258 KB)

Booting Linux (WIP)

Linux kernel and rootfs configs are in sw/. Building requires a Linux host (macOS lacks elf.h and other Linux-specific host headers).

# On a Linux machine — full build with Buildroot (toolchain + BusyBox + kernel)
make -C buildroot BR2_DEFCONFIG=/path/to/NyanSoC/sw/buildroot-nyansoc.config defconfig
make -C buildroot -j$(nproc)
# Output: buildroot/output/images/Image

# Or build the kernel directly (requires riscv64-linux-gnu-gcc)
make -C linux ARCH=riscv CROSS_COMPILE=riscv64-linux-gnu- \
    KCONFIG_CONFIG=/path/to/NyanSoC/sw/linux-nyansoc.config \
    -j$(nproc) Image

Once built, load everything over UART (~4–10 min at 115200 baud):

PORT=/dev/tty.usbserial-XXXX
python3 scripts/uart_load.py -p $PORT load sw/opensbi/build/platform/nyansoc/firmware/fw_jump.bin 0x80000000
python3 scripts/uart_load.py -p $PORT load linux/arch/riscv/boot/Image                             0x80200000
python3 scripts/uart_load.py -p $PORT load boards/tangnano20k/nyansoc.dtb                          0x81000000
python3 scripts/uart_load.py -p $PORT go 0x80000000 --stay

Simulation tests

make sim          # run all CPU tests under iverilog
make sim-waves    # run first test and dump a VCD waveform

Tests: test_alu, test_branch, test_mem, test_jump, test_csr, test_irq, test_mext.

Formal verification

make prove    # BMC checks: nyanrv (riscv-formal) + UART TX/RX
make cover    # Cover checks: reachability for all modules

The riscv-formal core files live in formal/nyanrv/ and are synced into the riscv-formal submodule at build time via make -C formal setup.