The ISS and the comparisons
What the proofs do not cover, comparison does. An instruction-set simulator written separately from the manuals runs every program first; then the core, as the Verilog sysr generates, runs it in Icarus; then everything the two machines hold is compared, down to the cycle count. A counter read or an interrupt one cycle off is a failure.
tools/rviss.rkt, the ISStools/rvasm.rkt, the assemblerThe ISS: tools/rviss.rkt
The ISS is an RV64IM interpreter in Racket, written from the unprivileged (20191213) and privileged (20211203) manuals, not from isa.sysr or the core, so that agreeing with it means two readings of the manuals agree. It implements everything the core does: machine and user mode, PMP, traps, the CSRs, interrupts, and the platform the SoC is, QEMU's virt as sysk uses it. The only instructions it does not write out are the custom ones: it evaluates their spec functions from custom.sysr through tools/custom.rkt, the definition being their manual.
It is cycle-exact for this core on purpose: cycle 0 after reset fetches and the first instruction runs in cycle 1, from 0x80000000; an instruction takes 1 cycle, a load 2, a multiplication 2, a division or remainder 66, a trap 1. mcycle counts cycles, mtime counts tick-num of every tick-den of them, and interrupts are checked when an instruction would execute, before it. Its device models are exact too: the UART's bytes take 10 bit times of uart-div cycles on the line, an input byte enters the FIFO in the cycle devices/uart.sysr says, and the PLIC's claim picks the source the hardware does.
A machine is one Racket struct (machine: registers, memory, pc, cycle, the CSRs, the timer, and a virt struct for the devices). step! does one step, an interrupt, an exception or an instruction, and adds its cycles; run! steps until the program exits through the test device or a cycle limit is reached. load-elf loads an executable's segments at their physical addresses (the entry must be 0x80000000). From the command line it runs a .s file, an ELF or a hex image and prints what the program sent to the UART, the exit, the cycles, the instructions retired and the registers. Here is cores/rv64im/programs/hello.s, which polls the UART's line status register before each byte:
Most of those 1,851 cycles are the polling loop: the transmitter is busy for 10 bits of 16 cycles after each byte (uart-div 16 in the default build), and the program waits for it before writing the next.
The assembler: tools/rvasm.rkt
A small two-pass RV64IM assembler: the base and M instructions, Zicsr, mret and wfi, the custom instructions of custom.sysr (their names and funct3 from tools/custom.rkt), the usual pseudo-instructions (li, la, mv, j, call, ret, beqz, …), labels, .word, .dword, .zero, .align and .equ. It writes one flat image from address 0, one 32-bit word per line for $readmemh, and its errors name the line. tests/core-test.rkt assembles tests/fixtures/asm/encodings.s with it and with LLVM (llvm-mc -triple=riscv64 -mattr=+m,-c,-relax), where installed, and requires the 115 words to be identical.
li builds any 64-bit value as LLVM does, recursively: a value that fits in 32 signed bits is lui and addiw (or lui alone, or an addi); a larger one is the value above its low 12 bits, built the same way and shifted into place with slli, plus those bits with addi. The test checks at most 8 instructions for a set of hard values, and that each one ends up in the register on the ISS. Try a value (this is the page's transcription of li-words):
tools/hexbytes.rkt is the smallest tool here: it turns a text (with \n and \004) into one hex byte a line, padded with xx to 4096, for the ULX3S board testbench's $readmemh input (On a ULX3S).
Running a program on both: run.rkt and tb.v
cores/rv64im/run.rkt runs a program on the ISS and on the SoC and compares the two. Step through what happens to one program:
The ISS
The core (Icarus)
What is compared
After both runs, compare lists every difference; a test passes only with none. Select a kind of state to see where each side gets it: the testbench prints the core's state from inside the simulation (hierarchical names such as dut.core.cs.mcause), and the ISS dumps the same names from its struct (machine-csr-dump).
cores/rv64im/tb.v
tools/rviss.rkt
Self-checking programs and random programs
The test programs (cores/rv64im/programs/*.s, 17 today; core-test.rkt requires at least 15) each check their own results and end through the test device with code 0, or with the number of the check that failed; # expect: exit=N, # input: TEXT and # console: TEXT lines in a program change the expected code, give the UART input and check the console. They cover the ALU at 64 bits, branches, loads and stores of every width, calls and a sort, every exception with its mcause/mepc/mtval, the CSR rules, timer and external interrupts (UART input through the PLIC), the UART itself, a store into the next instruction, the RAM's end, the custom instructions, user mode and PMP, the W instructions and every M instruction with division by zero and overflow. Each must pass on the core and agree with the ISS on everything.
Random programs (random-program) find what nobody thought to write a test for. A prologue installs a trap handler and schedules a timer interrupt at cycle 40; the body is 80 random instructions; the handler skips any instruction that faulted and moves the timer a few dozen cycles ahead. Every branch and jump goes forward, so every program ends. Half of them first drop to user mode behind random PMP regions, with mcounteren random, so access faults of every kind happen too. The mix of the body, read from the thresholds in run.rkt:
make core-test runs the test programs, then 200 random programs (seed 1); tests/core-test.rkt runs the test programs and 100 random programs with seed 7. A failing random program is kept in a file, so it can be run again and shrunk by hand.
sysk on the core
The largest program compared is sysk itself, built by sysk's Makefile, unchanged: make sysk runs it with 512 KB of RAM (--ram-words 65536), the input hello, sysk\n\004 on the serial line at 16 cycles per bit, and compares the core with the ISS at cycle 700,000, just past its first answer. The README records the results:
- On the ISS, the whole run: it boots, starts its eight tasks, runs the pipeline, answers
hello, syskwithHELLO, SYSK(the UART driver woken by the UART's interrupt through the PLIC), lets its spinners finish and exits with the test device's pass code: 220 million cycles, 182 million instructions, 21,854 timer interrupts, about 85 s. - On the SoC in Icarus, about 5,500 cycles a second: the same output, and agreement with the ISS on everything (registers, CSRs, the devices, all 512 KB of memory, every I/O store, every byte decoded from the serial line) at cycle 700,000; the first answer's last byte is written in cycle 683,446. The whole run would take Icarus about 11 hours, which is why it is compared over a prefix.
- The ISS's device models were checked against sysk before the core ran it: on the ISS, sysk printed the same lines as QEMU gives, apart from their interleaving and the count of timer interrupts, which depend on timing.
tests/core-test.rkt also boots sysk on the ISS up to its first answer when ../sysk/build/sysk.elf is built, and runs a small ELF (tests/fixtures/elf: code, read-only data, .bss) on both machines.