Devices and the platform
The SoC's devices are written in sysr like the core: a 16550 UART subset with a real serial line, a PLIC whose claim is proven to pick the right source, an SDRAM controller whose timing is proven not to depend on an address, and the SD card's SPI host, whose timing is proven not to depend on the bytes it moves. Their register layouts are functions the SoC decodes addresses with, and their properties have names. From both, tools/platform.rkt generates what a kernel compiles against, and a contract that turns assumptions in sysk's trusted base into proven statements.
uart.sysr and plic.sysrcustom.S)The obligation counts are what sysr check devices/uart.sysr --top uart and --top plic printed when this page was written, sysr check devices/sdram.sysr --top sdram for the SDRAM, and --top spi and --top sd-card of devices/sd.sysr.
The UART: devices/uart.sysr
The UART is the subset of a 16550 that QEMU's virt machine has and sysk uses: 8 data bits, no parity, one stop bit, at a fixed rate of div clock cycles per bit (a module parameter; there is no divisor latch). Its registers, by address: 0 is RBR when read (the oldest received byte, popped by the read) and THR when written (send a byte, if the transmitter is idle; a write while it is busy is lost); 1 is IER, the two interrupt enables; 2 is IIR; 5 is LSR, with data ready in bit 0, overrun in bit 1 and transmitter idle in bits 5 and 6. Received bytes go into a 16-byte FIFO. Both interrupts are levels: received data while enabled and waiting, transmitter idle while enabled and idle.
The serial line is real, and its timing is exact so that the ISS can model it to the cycle. Type a byte to see its frame. A byte written to THR in cycle c is on tx from cycle c+1 for ten bit times, lowest data bit first. The receiver, seeing a start bit begin in cycle b, checks it half a bit in and samples each later bit in its middle.
tx; the dashed green marks are the cycles in which a receiver with the same div samples it, by the timing in uart.sysr's header. Enter one character or a hex byte such as 0x0a.What is proven about it
These are the UART's named properties, read from uart.sysr as it is. Each is an invariant over every reachable state, proven by k-induction; the unnamed ones beside them keep the counters in range. A driver relies on the last three: the receive interrupt is exactly "enabled and data waiting", and LSR tells the truth about data and the transmitter.
The programs that drive it poll exactly these bits. This is the core's hello.s, which waits on LSR bit 5 before each store to THR, and what the ISS printed when the docs were built:
cores/rv64im/programs/hello.s
racket tools/rviss.rkt hello.s
The PLIC: devices/plic.sysr
The PLIC collects interrupt lines and hands the core one at a time. It has 32 level-triggered sources (source 0 does not exist) and one context, hart 0 in machine mode. Each source has a priority from 0 to 7 (0 never interrupts) and an enable bit; the context has a threshold. A source whose line is high and that is not claimed is pending. Reading the claim register returns the highest-priority pending enabled source above the threshold, the lowest id among equals, or 0, and claims it: it is no longer pending until the driver completes it by writing its id back.
The hardware finds that source with a chain: b0 is 0, and each bi is i if source i is eligible and its priority is strictly greater than that of bi-1, else bi-1. Strictly greater is what sends ties to the lower id. Try it: raise lines, change priorities, enables and the threshold, then claim and complete. The UART is source 10.
b1 to b31: green where it changes.plic.sysr's registers in your browser: pending is the line and not claimed, the chain is the b0…b31 lets, a claim sets the claimed bit of best, and a completion clears the written id's bit only if that source is enabled. "level" is the source's input line, "en" its enable bit.What is proven about it
The first group says the claim is right: best-none, best-eligible and one best-max per source together say that the source returned is eligible and that no eligible source beats it. The second group is what sysk relies on: a claimed source forwards nothing more until it is completed, and a completion the PLIC did not issue changes nothing. The PLIC requires that an access is a read or a write, not both; a counterexample found that one: a claim and a completion in the same cycle lost the completion.
The properties were tested by planting bugs. The proofs caught ties going to the higher id, a claim that does not quiet its source, a completion of a disabled source, a FIFO that takes a byte when full, a line that is not high when idle, an overrun not always flagged, and bytes with bit 7 clear never sent. The disabled completion was missed at first, because the property was stated with the implementation's own complete signal; the properties are now stated from register accesses, which is why they mention wr, claim-at and wdata.
The SDRAM: devices/sdram.sysr
The board's 32 MB SDRAM sits behind the core's external data port (sysr 033), and its controller answers every load and store at one fixed latency, whatever the address and whenever a refresh falls (sysr 034). It is closed-page: each access activates its row, reads or writes four 16-bit beats (one doubleword; bursts of 4, a write's bytes masked by DQM) with auto-precharge, and leaves every bank idle, so every access takes the same cycles. A refresh is owed every refi cycles (7.8 µs), counted from the end of power-up, and goes before any request due at the same time. The worst case is therefore one refresh, the same for every address: a load's doubleword is on rdata by c + trfc + trcd + cl + 5, and the core waits exactly load-cycles for it. Power-up is power cycles of NOPs (200 µs), a precharge of all banks, 8 refreshes and the mode register; the core's boot-cycles waits that long before its first fetch, a count from reset that is the same in every run, so Zkt is unchanged.
The chip's geometry and timings are parameters, in cycles of the core's clock. The defaults are the ULX3S's chip at 15 MHz, where every limit is one cycle except tWR and tRFC (two). Another board's chip is another set of numbers. Pick a request and whether a refresh is due in its cycle, and see the commands the controller puts on the pins:
xd_valid). Commands are on the pins from the cycle after the controller chooses them; a read's beats come cl cycles after its command and shift into rdata, and a write's go out from its command on. Green marks where the core reads rdata (a load's last cycle, c + load-cycles − 1) or may make its next request (c + store-cycles). The defaults: trcd 1, cl 2, trp 1, twr 2, trfc 2; loads of 11 cycles, stores of 10.What is proven about it
timing is the Zkt of the memory. Which cycles carry a command, which drive the data lines, and whether a request is dropped are determined by when requests come and whether they are stores, never by an address or data. refresh-prompt says a refresh is never later than the end of the operation under way. Unnamed invariants keep every counter in range and the power-up sequence in order. 26 obligations, with the chip's model. Two planted bugs were caught: an access one cycle longer in bank 0 (timing), and requests let ahead of a due refresh (refresh-prompt).
The chip's model, sdram-chip, is what the SoC uses in simulation. It stores the doublewords, delivers a read's beats cl cycles after its command, and checks the datasheet's rules. A command before power-up breaks them, and so does an activate, refresh or mode set while a bank is open or precharging, or a read or write to a bank that is not open, before tRCD, before the mode is set or without auto-precharge. So do the wrong mode, both sides driving the data lines, and a refresh more than refi + slack cycles late. A broken rule sets bad, as a dropped request sets the controller's fault. The testbench reports both, and the ISS has neither, so either fails the comparison. programs/sdram.s makes 600 rounds of stores and loads, their phase against the refreshes varied, and reads everything back.
The SD card: devices/sd.sysr
The board's microSD slot is driven in SPI mode by a polled host at 0x10010000 (sysr 042). Its registers are SiFive's SPI controller's (FU540-C000 manual, chapter 19), at the same offsets with the same meanings, so a driver written for that one runs here, and QEMU's model of it (with a card behind it) is a second implementation to try a driver against. Of SiFive's registers it keeps the polled part: sckdiv (SCK is the clock / (2 (sckdiv + 1)): at 15 MHz, 18 gives 395 kHz for a card's start, 0 gives 7.5 MHz), csdef, csmode (AUTO selects the card during each frame, HOLD from a frame on, OFF never), fmt (8 bits, most significant first, read only), txdata (bit 31 full) and rxdata (bit 31 empty). Each FIFO holds one byte. A frame does not start while the byte received before is unread, so no byte is ever lost and a driver's loop is the obvious one: wait while full, write, wait while empty, read. There is no interrupt and no card-detect: a driver finds a card by CMD0's answer.
Pick a byte to send, the byte the card sends back, and sckdiv, and see a frame on the pins. The timing is exact so that the ISS can model it to the cycle: a byte written in cycle w starts its frame in cycle s = w + 1 when nothing is under way and the byte before was read, the frame is busy from s + 1 to s + 16 (sckdiv + 1), and its byte is in rxdata the cycle after.
What is proven about it
timing is the host's Zkt: when SCK and the chip select move, and when a byte may be written or read, are determined by when the program wrote and read which registers and by the settings it wrote, never by the bytes sent or received. A key in a block on the card does not change when anything happens on the pins. A planted bug, a byte of 0 starting its frame a cycle late, fails it with a counterexample. one-at-a-time is why no byte is lost.
The card, sd-card, is for simulation: an SDHC card in SPI mode as the Physical Layer Simplified Specification's chapter 7 has it, reduced to what a driver needs. It waits for 74 clocks unselected; then CMD0 with its CRC puts it in SPI mode, idle; CMD8 echoes its check pattern; ACMD41 answers idle warm times, then ready; CMD58 gives the OCR (high capacity); CMD17 reads a block (a byte of 0xFF, the token 0xFE, 512 bytes and their CRC-16) and CMD24 writes one (the token, 512 bytes, two CRC bytes, then the data response 0x05 and busy bytes of busy). CRC-7 is checked for CMD0 and CMD8, as a card does by default, and both CRCs are computed a bit at a time as the bits go by. A block past the card's end, or a command it does not have, gets R1's parameter or illegal-command bit. virt puts a card of sd-blocks blocks on the host's pins, the ISS has the same card (tools/sd.rkt), and both report the card's memory, so programs/sd.s, which drives the card as a driver would and checks the CRC-16 of a block of 0xFF against the specification's own 0x7FA1, is compared cycle for cycle. run.rkt --sd-image FILE starts the card with a disk image.
One SoC
cores/rv64im/soc.sysr's soc puts the UART, the PLIC and the SD card's host on the core's I/O bus with the test device, and the SDRAM controller on its external data port with the chip's pins as its ports; virt is soc with the chip's model on those pins, for simulation, and the board puts soc on its real ones (sysr 035). On the bus: the UART at 0x10000000, the PLIC at 0x0C000000, the SD card's host at 0x10010000, decoding address bits with the same uart-base and plic-base functions that cores/rv64im/platform.sysr defines. The UART's interrupt line is PLIC source uart-irq, and the SoC proves that as a named invariant, soc.uart-source. The ISS models both devices to the cycle, and every run of the SoC, sysk's boot included, is compared with it register for register and byte for byte on the serial line (The ISS and the comparisons).
The platform: what a kernel compiles against
A kernel needs the hardware's numbers: where RAM is and how big, the UART's address and register offsets, the PLIC's offsets, which source the UART is. Written by hand, they can drift from the hardware. tools/platform.rkt reads them from the sysr sources the SoC is built from, with sysr's own reader, so they are the numbers the hardware decodes with, not a description of them. The sources are:
It writes one directory per platform, platform/virt (QEMU's virt machine, which the SoC was built to match) and platform/ulx3s (the board), and only after sysr check has proven the platform's top. Each file starts with its provenance: the sysr version, the platform, and the first 16 hex digits of a SHA-256 over the sources.
| File | For |
|---|---|
devices.sysk | sysk's device list: each device a system may hand to a task, with the page its driver's PMP entry covers and its PLIC source |
platform.sysp | the numbers as sysp functions whose contract is their value, and the custom instructions (Custom instructions) |
platform.inc | the same numbers as .equ lines for the trusted assembly |
CONTRACT.md | what a kernel may rely on: the map, the ways in (below), the custom instructions, and the named properties with their text |
custom.S | ulx3s only: the custom instructions as functions |
make platform also writes one file that is the same for every platform, cores/rv64im/isa.sysp (tools/platform.rkt --isa): the ISA's instructions as sysp predicates, for code proven to meet them (Custom instructions). Every generated sysp file passes through sysp's own formatter, so sysp fmt --check accepts it as written (sysr 026).
Every constant of platform.inc, where it comes from, and its value on each platform, read from the generated files. They differ only where the boards do: RAM's size, and the SD card's host, which the board has and QEMU's virt does not. The board's RAM comes from its ram-words; mtime is 10 MHz on both, QEMU's timebase on virt and 2 of every 3 cycles of the 15 MHz clock on the ULX3S (On a ULX3S).
| platform.inc | from | virt | ulx3s |
|---|
Copied, checked, required
sysk copies a platform directory into its own tree rather than reading ../sysr, so it builds without sysr, and a change of hardware arrives as a diff it can review. --check-dir DIR regenerates the files without proving and reports each one that differs or is missing; make platform-check SYSK=../sysk runs it on every copy it finds. --check SYSK instead compares numbers sysk still writes by hand (its devices.sysk, constants and plic-write offsets in kernel/sched.sysp, the .equ lines of its assembly) with the hardware's.
The kernel states what it relies on in its own file, requires.sysk: each statement in its words, with the properties that carry it (platform/requires.example.sysk is sysr's example). With --requires, CONTRACT.md lists exactly those statements, and generation fails if a property they name is not in the hardware, so a property renamed in sysr shows up as a failed regeneration in sysk, not as a silent gap.
Ways in
Each CONTRACT.md says what reaches the machine other than the program in its RAM (sysr 047), so that a kernel and an auditor read it rather than assume it. First, whether a debug module is present: the RISC-V debug specification's Debug Module halts a hart and reads and writes its registers and memory from outside, the most a pin can do. In sysr such a module would be named debug-module, and tools/platform.rkt walks the modules the platform's top instantiates (instantiated) and says whether it is among them, with how many it looked at: the answer is read from the design the bitstream is built from, not declared, so adding one changes the contract. Today neither platform has one. Then the top's inputs, the only signals from outside the design besides its clock and reset, and what reaches the machine from outside the sysr design, said per platform: on the ULX3S, top.v's clock and reset button, the ECP5's JTAG port and the board's ESP32, either of which can load another bitstream and so replace the whole machine; on virt, QEMU's own debugger stub. Whether the ECP5's JTAG and configuration flash can be locked is not yet checked.
What moves out of sysk's trusted base
sysk's docs/trusted.md assumes, about QEMU's virt machine, the PLIC's layout; that a claimed source forwards nothing more until it is completed with the same number, and a completion the PLIC did not issue is ignored; that the UART raises its interrupt while its receive FIFO holds data; and that its device list gives each device's page as the machine has it. On the SoC, the layout and the device list are generated from the hardware's sources, and the behaviour is proven: plic.claim-quiets, plic.claimed-silent, plic.complete-releases, plic.complete-only-own, plic.unissued-ignored, uart.rx-level and the rest, which CONTRACT.md cites.
What stays trusted. The assembly that touches the registers must do what its comments say, with these numbers. And on QEMU, where sysk also runs, the statements remain assumptions about QEMU: the numbers are QEMU virt's (the SoC was built to its map), but the properties are the SoC's devices'. That QEMU's devices behave the same in what sysk uses is tested, by sysk running on the ISS's models of them, not proven.
tests/platform-test.rkt checks that both directories are what the sources generate now, that every file carries the provenance, that the platforms differ only in RAM size, that a missing property in the requirements is an error, that an edited or missing copy is reported as drift, that the ISS (written independently) has the hardware's map, and that --check finds the three wrong numbers planted in a small sysk tree.