The core · cores/rv64im

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.

What 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.)

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.

Step an instruction Play Back Step

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:

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.

No number in the table depends on an operand's value, which is what the scalar cryptography extension's Zkt asks of every RV64IM instruction, so that constant-time code stays constant-time on this core. The divider is the one unit where it could differ, since a divider may stop early on small operands. It promises (determined busy (start)), proven: how long it stays busy depends on when it started and on nothing else (Two runs: determined). An early-out divider fails that proof (V008). For the whole core, rv64im promises (determined zkt act (issued take waiting)), proven (sysr 022, 027): which cycles execute an instruction is decided by the instruction words executed, by which of them trap and by when a fence.t's deadline is reached, and by nothing else: not an operand, an address, a loaded value or the I/O bus. So the core implements Zkt. What the property leaves open is interrupt latency: an interrupt is taken in a cycle where an instruction would execute, so one that arrives during a division waits for it, up to 65 cycles that depend on what ran before.

Entropy: seed (Zkr)

The seed CSR (0x015) is Zkr's entropy source (sysr 028), and only machine mode reads it: a user-mode access, and a read-only access in any mode, is an illegal instruction, as the scalar cryptography manual (1.0.1, chapter 4) says. Behind it, the zkr unit takes one raw noise bit a cycle and runs SP 800-90B's two health tests on the raw bits: the repetition count test (a run of 21 equal bits fails) and the adaptive proportion test (589 bits equal to a window's first, in a window of 1024, fails), the cutoffs for one bit of min-entropy per raw bit at alpha 2^-20. It answers BIST until a whole window has passed, then WAIT until 16 bits are gathered, ES16 with them, and DEAD for good once a test fails; the poll that returns ES16 wipes the pool. Proven: entropy is 0 unless ES16, the reserved bits are 0, DEAD stays DEAD, and a returned sample is not returned again.

The noise is an input of the SoC. The testbench drives it with bit 31 of the cycle number times 0x9E3779B1, a sequence the ISS computes too, which passes the health tests and is no entropy at all: the simulated core's seed is for testing software, never for keys. The ULX3S has no measured source yet: its input is 0, the repetition count test fails within 21 cycles, and seed answers DEAD, which software must treat as fatal. A ring-oscillator source in the ECP5 fabric is the next step, and it needs measurements on the board itself (followups, item 4).

The temporal fence

fence.t rs1 (custom-1, every other field 0; machine mode only, illegal in user mode) closes that gap at a domain switch. Architecturally it does nothing; the next instruction executes in the first cycle in which mtime has reached rs1, and no interrupt is taken while it waits. A kernel that ends each switch with it, its deadline the end of the slice, switches at the same cycle whatever the previous domain did: the instruction pads the switch to a fixed latency. It follows Wistoff, Heiser et al.'s fence.t (IEEE Transactions on Computers, 2022), with an absolute deadline where theirs pads to cspad cycles after the timer interrupt, since sysk switches on the timer, on a wait and on a yield (sysk's choice). Their fence also clears the caches, TLBs and predictors; this core has none, and the property above shows that nothing left behind changes later timing, so the padding is the whole of it here. A cache added later is cleared by the same instruction.

One hazard comes with it. Nothing ends the wait but the deadline: no interrupt, no device. A deadline far ahead, from a bug or a garbage register, stops the core until reset. Machine-mode code with interrupts off could always hang the core with a loop that never ends; fence.t makes it one wrong value away. The hardware does not cap the wait, because a wait cut short by a cap or an interrupt would end at a time that depends on history, which is the timing channel the instruction exists to close. The kernel checks instead, before the instruction: the deadline must lie no more than one slice past mtime.

Machine mode behind PMP: Smepmp

Without it, a PMP entry binds machine mode only when it is locked, so a kernel in machine mode may execute any memory, a task's included, and a kernel bug that jumps there runs the task's bytes with every privilege. Smepmp (sysr 045; the privileged specification's Smepmp chapter) is the answer for machines with only machine and user mode, as SMEP and SMAP are on x86. It adds mseccfg (0x747, machine mode only) with three bits. MML (bit 0) changes what L means: set, the entry is machine mode's rule; clear, it is user mode's; and RW = 01, reserved without MML, becomes a region both share. MMWP (bit 1) denies machine mode wherever no entry matches. Both stay set until reset once set. RLB (bit 2) lets locked entries be changed, for boot; it cannot be set once an entry is locked while it is clear.

With MML, a matching entry grants this, by its L, R, W and X. Where no entry matches, machine mode may read and write (unless MMWP) but never execute, so a kernel must give its own text a locked R X rule before it sets MML. While MML is set and RLB clear, a pmpcfg write that would add a rule machine mode executes from (1001, 1101, 1010, 1011) is ignored.

isa.sysr writes the table as the specification prints it, row by row (pmp-mml-machine, pmp-mml-user); the hardware's pmp-perm computes it as four cases, and the two are proven equal. programs/smepmp.s walks the rows, the sticky bits, RLB's rule and the ignored writes on core and ISS. What sysk does with it is sysk's: with MML the current task's regions are user mode's alone, so the kernel's copies to and from that task need the shared encodings or a change of rules; other tasks' memory, which has no entry at the time, stays machine mode's to read and write unless MMWP is set.

The attention button and the light

A person at the console needs a way to reach the kernel that no program can fake or block, and a sign that no program can imitate while the kernel answers (the root's docs/research/users.md: the trusted path). sysr 046 gives the core both, as the CSR mattn (0x7E0) rather than as a device on the bus, so that no PMP entry can ever hand them to a task: like every machine CSR, user mode cannot reach it. Bit 0 is the light, which only a write to it changes. Bit 1 is the press: the button's rising edge sets it, a write of 0 clears it (a write of 1 leaves it as it is, and a press in the cycle of the clearing write wins). Bit 2 is the button as it is now. The press is also mip's bit 16, enabled by mie's bit 16: a machine interrupt with mcause 16, below the external and the timer interrupt (the AIA's default order), and, as every machine interrupt, always enabled in user mode, so a task cannot mask it.

The core takes the button as one input, attn, already clean; the board makes it so. On the ULX3S it is FIRE2, through two flip-flops and then sampled once every 16,384 cycles (about 1.1 ms at 15 MHz, longer than a switch bounces), and the light is LED 7 (The board). In simulation the testbench presses it for 16 cycles from +attn=N, the ISS from #:attn-at, and programs/attention.s (# attention: 150) checks the interrupt in user mode, the bits, the clearing write and the release on core and ISS. A press that a hung kernel should still answer is for Smrnmi, next in the order.

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: soc and virt

soc.sysr is the whole system: the core with the devices QEMU's virt gives sysk, and the board's SD card host, 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, the SiFive test device, which ends a simulation, and the SD card's SPI host (sysr 042); and the SDRAM controller on the core's external data port, the chip's pins its ports (sysr 034, 035). soc is all of it; virt is soc with models of the SDRAM chip and an SD card on those pins, the system the simulations run, and the board puts soc on its real pins. soc 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 soc: 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.

Both take the same 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), and the external RAM's: load-cycles, store-cycles, xram-words, boot-cycles and sdram-power (sysr 033 to 035). 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 soc 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).