Custom instructions

One definition, read five ways

Each instruction NAME is three definitions in custom.sysr: NAME-funct3, a constant; NAME-spec, its meaning, a spec function of a (rs1) and b (rs2); and NAME, the hardware, an ordinary function. Everything else is derived from those definitions. Nothing outside custom.sysr restates what an instruction does.

Try the definitions

The two instructions so far are made for byte work eight bytes at a time. bsum rd, rs1, rs2 is rs2 plus the sum of rs1's eight bytes, modulo 2⁶⁴: bsum s, w, s adds the bytes of a word to a running checksum. bfind rd, rs1, rs2 is the index of rs1's first byte, counting from the least significant (the lowest address, as RV64 loads them), equal to rs2's low byte, or 8 if there is none. Type two values and the figure computes both exactly as the spec functions on the right say: the sum of the bytes, each widened to 11 bits, added to b with wrapping; and a chain of eight comparisons, the first that holds deciding.

The hardware, proven equal to the definition

The definitions are written for reading; the hardware is written for speed. bsum-spec adds the eight bytes in a chain, while bsum adds pairs of bytes, then pairs of pairs: a tree of adders three deep. bfind-spec is eight nested ifs; bfind is eight comparators whose results go to lowest-set, which finds the lowest set bit by halves. custom-unit states that each is equal to its spec, for every input, and sysr check proves it with z3 (13 obligations when this page was written).

The unit is a part of the core. rv64im.sysr instantiates it in the execute stage, and the execute stage as a whole is proven equal to the ISA's exec-spec. In isa.sysr, the value a custom-0 instruction writes is custom-spec, which picks the instruction's spec by funct3:

An instruction is legal only on opcode 0001011, with funct7 0 and a funct3 that custom-legal accepts; any other funct3 or funct7 is an illegal instruction, on the core and in the ISS. Each takes one cycle, like the ALU. Because the ISA and the core read the same spec functions, an error in a definition is the instruction's meaning, not a disagreement: what the proofs guarantee is that every reader agrees with the one text.

The ISS and the assembler: tools/custom.rkt

tools/custom.rkt reads custom.sysr with sysr's own checker (check-sources, without proving) and takes the checked functions it hands back. An instruction is any NAME-spec that has a matching NAME-funct3; it must take two (bits 64) and return (bits 64), and two instructions may not share a funct3. From there:

• insn-eval evaluates a spec on two numbers, walking the typed expression and masking each result to its width. It understands literals, the parameters, slice, zext, sext, +, +%, -, -%, *%, and, or, xor, not, ==, !=, =>, if, cat, bit and shifts; anything else is refused by name. The ISS calls it for every custom-0 instruction.
• insn-mnemonic and the funct3 give the assembler its table: bsum a0, a1, a2 assembles to the word LLVM's .insn r 0xb, 0, 0, a0, a1, a2 gives.
• spec->sysp translates a spec into a sysp expression over 64-bit words, each value masked to its sysr width. sysp's words have no order, so a definition that compares with < or > cannot be translated and is refused; shifts and bit need constant amounts.

The tests check the parts against each other: the definitions give the values worked out by hand; the evaluator gives the same answer for each spec and for its implementation on 300 random inputs each (two differently built expressions agreeing); the assembler matches LLVM's encoding; the ISS runs both instructions from their definitions and traps on an unused funct3; and the translation and the generated platform files have the expected text.

From sysp: a function whose contract is the definition

make platform (tools/platform.rkt, see Devices and the platform) writes, for each platform, a predicate NAME-is that is the definition in sysp and a function NAME that ensures it. The two platforms differ in who computes it:

On the ULX3S, bsum is an extern fn. sysp trusts its contract (warning W002), and the hardware is what proves it: custom.S implements each extern as the one instruction, then a return. On QEMU's virt machine, which has no such instructions, bsum is an ordinary sysp function whose body is the same translated definition, and sysp proves it meets its contract. A program written against platform.sysp therefore checks the same way on both.

The demo: examples/custom

demo.sysp uses both instructions. checksum sums a message eight bytes an instruction with bsum, then the remaining bytes one at a time; find-byte looks for a newline eight bytes at a time with bfind (through scan), then byte by byte. word-at assembles eight bytes into a word the way a doubleword load does, and its contract says so byte by byte, which is what lets sysp connect the instruction's definition to the bytes of the message.

rt.S is the demo's runtime on the SoC: a 4 KB stack, the call to demo_main, its result to the test device, put_byte on the UART, and the three functions a freestanding sysp build may call (sysp_alloc and sysp_panic fail; the demo allocates nothing). It includes the platform's platform.inc for every address. link.ld places the program at 0x80000000, where the core starts. make custom-demo checks and builds the demo against each platform's platform.sysp with sysp and clang, then runs the ulx3s build on the core against the ISS and the virt build on the ISS. Both print the following and exit 0, each answer compared with the plain byte-at-a-time one:

$ make custom-demo
checksum 6275, first newline at 35
checksum 5217, first newline at 57
checksum 2080, first newline at none

This output is from the examples' README, rebuilt and rerun for this page (it is not one of the runs make docs records). The core agreed with the ISS at the exit after 20,296 cycles; the virt build, whose software versions clang inlines, took 19,911 on the ISS.

In place: sysi's --insn

Called through custom.S, each instruction costs a call and a return, so on the demo's short messages the instruction build is no faster than the software one. The instruction pays off when the compiler emits it in place. sysp does not do that yet. sysi, the compiler between sysp and the machine, does: sysi asm --insn bsum=0x0b,0,0 --insn bfind=0x0b,1,0 turns every call to those externs into the R-type instruction itself, with no custom.S, and its validation reads the instruction's meaning from the same isa.sysr.

Adding an instruction

The header of custom.sysr gives the recipe. For an instruction NAME:

1. (fn NAME-funct3 () (bits 3) N), with an unused N.
2. (spec NAME-spec ((a (bits 64)) (b (bits 64))) (bits 64) ...): the meaning, using only what tools/custom.rkt evaluates and translates (bit operations, +, +%, equality comparisons, if).
3. (fn NAME ...): the hardware, written however it is fastest.
4. One line in each of custom-legal, custom-spec, custom-exec, and an ensures NAME in custom-unit.

Then sysr check proves the hardware against the meaning, and the ISS, the assembler and make platform pick it up with no further change. Using the instructions in sysk is sysk's change, and has not been made.