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, with the rotates of Zbb and Zbkb, Zknh's SHA-256 functions and Zkr's seed (its source modelled cycle by cycle, with the testbench's noise), Smepmp (its table with MML written out as the specification prints it, MML-TABLE, apart from both isa.sysr's form and the hardware's), the attention button (pressed for 16 cycles from #:attn-at, as the testbench's +attn), every load taking load-cycles and every store store-cycles as the core does (#:load-cycles, #:store-cycles, and #:fetch-bytes for the block RAM within a larger RAM; run.rkt's --load-cycles, --store-cycles, --xram-words; sysr 033), and its first fetch #:boot-cycles after reset (--boot-cycles; sysr 034), written from the unprivileged (20191213), privileged (20211203), bit-manipulation (1.0.0) and scalar cryptography (1.0.1) 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 and fab: it evaluates their spec functions from custom.sysr and fabric.sysr through tools/custom.rkt, the definition being their manual (for fab, fabric-eval: the loaded configuration's three layers in turn; The fabric).
It is cycle-exact for this core on purpose: cycle 0 after reset fetches (cycle boot-cycles, when it is set) and the first instruction runs in the next, from 0x80000000; an instruction takes 1 cycle, a load 2, a multiplication or a fab 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, the PLIC's claim picks the source the hardware does, and the SD card's host starts each frame in the cycle devices/sd.sysr says, exchanging a byte with a card that answers as sd-card does (tools/sd.rkt, sysr 042).
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, the rotates, the SHA-256 instructions, fence.t, Zicsr, mret and wfi, the custom instructions of custom.sysr (their names and funct3 from tools/custom.rkt), the fabric's fab rd, rs1, rs2, rs3 and its CSRs fab0–fab11, 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.soc.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, 28 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, # attention: N and # console: TEXT lines in a program change the expected code, give the UART input, press the attention button for 16 cycles from cycle N 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, the SD card's host and a card behind it, a store into the next instruction, the RAM's end, the custom instructions, the fabric with SHA-256's Ch, Maj and T2 loaded, 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.
A paste at the prompt
A 16550 holds 16 received bytes; at 115,200 baud that is about 1.4 ms, and a driver that is not run within that time loses the rest. QEMU never shows this, because its serial line waits for the guest. run.rkt --elf can: --input-file FILE gives the bytes, --input-after TEXT starts them in the first cycle after the output so far ends with TEXT and has left the line (as a person pastes at a prompt; the ISS finds that cycle in a run without input, and both machines then get the input from there), and --iss leaves out the core, so a run of millions of cycles takes seconds. The console goes to stdout; stderr ends with a line such as uart: 16 received, 24 lost (overrun), 16 read. The lost bytes are counted by both machines (the testbench's rxlost, the ISS's virt-lost) and compared with the rest of the devices, so the ISS's count is the core's. tests/core-test.rkt pastes 40 bytes into a program that computes for longer than they take to arrive: 16 are kept, 24 lost.
racket cores/rv64im/run.rkt --elf IMAGE --ram-words 131072 --tick 2/3 --uart-div 130 --iss \ --input-file paste.txt --input-after '/% ' --cycles 4000000