The core · cores/rv64im/isa.sysr

isa.sysr: what is proven

The RISC-V manuals, as far as this core implements them, written as sysr spec functions: what one instruction does, instruction by instruction, with no regard for hardware. The core's execute stage, ALUs, multiplier, load/store unit and PMP are proven equal to them. sysi reads the same file to know what each instruction in a compiled program means, so the meaning of an instruction is written once.

Spec functions

A spec is written like a fn, but it can only be used in properties and in other specs, never in hardware (Writing hardware). So isa.sysr can say what an instruction means in the plainest form the manual allows, and the hardware is free to compute it differently: a proof then says the two agree. The file states its own choices, the ones the ISS makes too: every exception traps (no misaligned access is performed), fence, fence.i and wfi do nothing, and PMP's granularity is 8 bytes.

The center is exec-spec: given the pc, the 32-bit instruction word, the values of rs1 and rs2 and whether the hart is in user mode, it returns an Exec, everything one instruction decides before memory, the CSRs and the M unit:

Its body is one chain of ifs on the opcode, and each arm is built from small specs: go (continue at a target, writing rd if asked; a target that is not a multiple of 4 traps), then (continue at pc + 4 when the value comes from elsewhere), access (a load or store, which traps if misaligned), system, illegal and fault. exec-val gives the value written to rd for the instructions whose value the execute stage computes. Here is every function in the file, grouped, as it is now:

Pick an instruction

Choose an instruction, or type any 32-bit word, and set the operands. The page decodes the word with isa.sysr's field layout and follows exec-spec arm by arm: the path it takes, the Exec it returns, and which proven units of the core compute each part. The evaluator is this page's own transcription of exec-spec, exec-val, alu-op, alu-w, m-mul, store-mask, store-data and the custom specs into JavaScript, written from the file; the spec functions themselves are what the proofs use.

What is proven equal to it

Each row is a module whose properties name spec functions, read from rv64im.sysr and custom.sysr as they are now. Every one is proven by k-induction for all inputs (they are combinational, or nearly: the multiplier's property is about its registered result one cycle later), so "equal" means for every instruction word, every pc, every register value and every privilege level, not for the cases a test happened to try.

• The execute stage (exec) is written as hardware: decoded controls, one 64-bit ALU with a shared adder, a 32-bit ALU for the W forms, one adder for every jump target. Its trap, cause, mtval, next pc, register write, load/store, CSR, MRET and M flags and its address are each proven equal to exec-spec's. Because it is not a copy of the spec, this is an equivalence proof, and the hardest obligation of the core: the written value. That one is compared with exec-val, a single-ALU form of the spec's value, and exec-val-lemma proves that wherever exec-spec writes rd (not a load, CSR or M instruction) and does not trap, its value is exec-val. Even so, cores/rv64im/run.rkt notes that this obligation takes the z3 it was tested with about 95 s, hence its --timeout-ms 300000.
• The multiplier (mul) is written in the spec's own form, one 128-bit *% on extended operands: proving a different multiplier equal would mean comparing multipliers bit by bit, which is beyond z3 at 64 bits.
• PMP is proven entry by entry (pmp-entry against pmp-match and pmp-grant), then the priority among the eight entries (pmp against pmp-allows). The hardware's NAPOT match uses the specification's own formula; the comment above pmp-hit notes that an equivalent form took z3 46 s.

Other modules prove properties of their own rather than equality with a spec: the register file (x0 reads 0; in the cycle after a write, reading the written register gives the written value), the CSR file (mtvec and mepc are always 4-byte aligned; no CSR write and no MRET in a trap cycle, which the core proves where it uses it), and the core itself (the pc is always a multiple of 4; every index and every + or - in range, at the memory size it is built with). The CSR instructions' new values come from two plain functions in isa.sysr, csr-new and csr-writes, which the CSR file uses as they are.

The bugs these proofs caught

While the core was written, bugs were planted on purpose to see that the proofs reject them. The README records these, each caught by a proof above before anything ran: in features 004 to 006, a swapped load/store misaligned cause, an unaligned mtvec, a lock bit ignored for machine mode, and an off-by-one TOR bound; in feature 007, a W result zero-extended instead of sign-extended, MULHSU's operand signs swapped with MULHU's, LWU sign-extending, and an inclusive TOR top bound. Each is the kind of mistake that runs most programs correctly. (These were one-off experiments; no test plants them again.)

Beyond the core

isa.sysr is checked by sysr's checker like any design, and its functions can be handed out to other programs (the driver's #:functions-box). Two use them:

• sysi validate. sysi's sysi/isa.rkt loads platform.sysr, isa.sysr and custom.sysr with sysr's checker and evaluates exec-spec (in machine mode), load-value, store-mask, store-data, m-mul, branch-taken and imm-b on each instruction word of a compiled program, with symbolic register values: what the word decides is computed, the rest becomes SMT terms. That is how sysi validate gives each instruction its meaning when it checks machine code against sysi, so the core and the compiler's checker cannot disagree about what an instruction does without one of the proofs failing.
• The custom instructions. tools/custom.rkt evaluates their spec functions for the ISS and translates them into sysp contracts (Custom instructions).

The ISS does not read isa.sysr for the base ISA: tools/rviss.rkt was written independently from the manuals, so that comparing it with the core checks one reading of the manuals against another (The ISS and the comparisons).

The tests: tests/core-test.rkt

The proofs cover what isa.sysr specifies; the tests cover the rest, and the tools. core-test.rkt checks the assembler against LLVM, the ISS's platform and timing on small programs, the RAM's byte lanes, ELF loading and, where ../sysk/build/sysk.elf is built, sysk's boot on the ISS. Then it builds the SoC (sysr build proves it first) and runs every test program and 100 random programs (seed 7) on the core in Icarus and on the ISS, requiring agreement on everything. Its cases, read from the file: