The RV64IM core
An RV64IM processor written in sysr: 64-bit registers, the M extension, machine and user mode, PMP, traps, CSRs and interrupts. It executes one instruction per cycle, from one memory in block RAM, and it is the machine sysk boots on. Its parts are modules with contracts, and the ones that compute what an instruction does are proven equal to the ISA written as spec functions.
rv64im.sysr, each with its contractisa.sysr it is proven againstWhat it implements
sysk is compiled for rv64im/lp64, runs its tasks in user mode behind PMP, and uses neither supervisor mode nor virtual memory. The core implements exactly that much of RISC-V, on the memory map of QEMU's virt machine, so the kernel runs on it unchanged. (Features 004 to 006 built it as an RV32I core; 007 made it RV64IM.)
| Area | What the core does |
|---|---|
| ISA | RV64I and M, Zicsr, mret, wfi (does nothing); fence and fence.i do nothing; the custom instructions of custom.sysr (bsum, bfind) on the custom-0 opcode, in one cycle (Custom instructions). |
| Privilege | Machine and user mode. A trap enters machine mode; mret enters the level in mstatus.MPP (3 or 0). mstatus.MPRV makes machine-mode loads and stores use MPP's level. |
| PMP | 8 entries (pmpcfg0, pmpaddr0–7; pmpcfg2 and entries 8–15 read 0); OFF, TOR and NAPOT; R, W, X and the lock bit. Granularity 8 bytes, so NA4 cannot be selected (a write of it is stored as OFF) and an aligned access never straddles two granules. |
| Exceptions | Misaligned target (0), instruction access fault (1), illegal instruction (2), ebreak (3), misaligned load (4), load access fault (5), misaligned store (6), store access fault (7), ecall from user (8) or machine mode (11), with mtval as the privileged spec says. No misaligned access is performed: each traps. |
| Interrupts | The machine timer (mtime ≥ mtimecmp, both in the core) and one external line, irq-ext, which the SoC connects to the PLIC. External wins over timer. Taken between instructions; always enabled in user mode; mcause bit 63 set. |
| CSRs | mstatus (MIE, MPIE, MPP, MPRV; UXL reads 2), misa (RV64 I M U), mie, mip, mtvec (direct mode only), mscratch, mepc, mcause, mtval, mcounteren, mcycle, minstret, cycle, time, instret, the PMP registers, and mvendorid, marchid, mimpid, mhartid (read 0). Any other CSR, a write to a read-only one, or a machine CSR from user mode is an illegal instruction; user mode reads the counters only where mcounteren allows. |
| Memory | One unified RAM at 0x80000000 of ram-words doublewords (2048, 16 KB, unless --param says otherwise), as eight byte-wide block RAMs. A load or store past its end is an access fault, and so is a fetch from anywhere else. |
| I/O | Every address that is neither RAM nor the timer goes to a 64-bit I/O bus (io_valid, io_we, io_addr, io_wdata, io_size); a load takes io_rdata, the doubleword holding its address, in the cycle it is made. |
The core, unit by unit
The top module, rv64im, connects the units below and holds the pc, the timer registers and the few registers that remember a load or an M instruction in flight. The columns are the stages an instruction passes through, but the core is not pipelined: an instruction does all of them in its one cycle, except the write-back of a load, a multiply or a divide, which takes the cycles after it. Select a unit to see its contract and what it is proven against, or pick an instruction and step through its cycles.
rv64im (ex, rf, mu, dv, cs, ls, mem) and inside them (x, xw, cu in exec; px, pd in csrs); the devices are soc.sysr's. Contracts are read from the source as it is now.Timing
The instruction register is the RAM's fetch port. In the cycle an instruction executes, the fetch port reads the doubleword holding the next pc's instruction (the branch target, the trap vector or pc + 4, already computed combinationally), so it is there one cycle later and a taken branch costs nothing extra. Bit 2 of the pc picks which half of the doubleword is the instruction. Whatever must wait for a result holds the next instruction in the register meanwhile:
| What | Cycles | Why, in rv64im |
|---|
The ISS (The ISS and the comparisons) models these numbers to the cycle; its constants are MUL-CYCLES = 2 and DIV-CYCLES = 66 in tools/rviss.rkt. Interrupts are checked in a cycle where an instruction would execute and are taken instead of it.
The modules
Each module of rv64im.sysr, in file order, with the comment above it and every property it states. A requires is proven wherever the module is used; an ensures or invariant is proven inside it, for every reachable state. Spec functions named in a property are marked; they live in isa.sysr or custom.sysr (isa.sysr: what is proven).
The SoC: virt
soc.sysr is the whole system: the core with the devices QEMU's virt gives sysk, on the core's I/O bus. The devices are sysr modules too (Devices and the platform): a 16550 UART subset with a real serial line, a PLIC with 32 level-triggered sources, and the SiFive test device, which ends a simulation. virt decodes address bits 31:0 of each bus access with the platform's functions, routes reads back as the doubleword holding the address, and connects the UART's interrupt to PLIC source 10 and the PLIC's meip to the core's irq-ext:
A device acts on an access at the end of its cycle; its interrupt line changes from the next. The test device is two registers in virt: a word or doubleword store of 0x5555 to it sets halt with code 0, of 0x3333 + code << 16 sets halt and code. The testbench (tb.v) stops there. Its one proven property, uart-source, says the PLIC's source 10 is the UART's interrupt; the SoC's other obligations are the instances' requirements where they are used (the PLIC's, that an access is not a read and a write at once) and everything inside the instances.
virt takes five parameters: ram-words (passed to the core), uart-div and uart-half (the UART's cycles per bit and half of them) and tick-num/tick-den (mtime counts tick-num of every tick-den cycles: 1 of 1 by default, 2 of 3 on the ULX3S for 10 MHz from a 15 MHz clock). sysr build … --param ram-words=65536 gives sysk its 512 KB from the same source.
The platform map
platform.sysr is the one place the addresses are written: constant functions that rv64im and virt decode with, and that tools/platform.rkt reads to generate what sysk compiles against, so the kernel's idea of the hardware is the hardware's. Pick a region, or type an address, and see which unit answers it and why.
What it does not have
- No supervisor mode, virtual memory, vectored
mtvec, or A or C extension: sysk uses none of them. - No memory interface with wait states: the RAM is block RAM and answers in one cycle. External memory (SDRAM), which a kernel larger than a board's block RAM would need, waits for that interface.
- The divider is not proven, and neither is the claim that the core as a whole implements the ISA over many cycles (that would need specification state, which sysr does not have). Both are covered by comparison with the ISS (The ISS and the comparisons).