The core · feature 043

The fabric

A custom instruction's meaning is fixed when the core is built. The fabric's is loaded: twelve word-wide cells beside the core, configured through CSRs and read by one instruction, fab. The hardware is proven equal to the fabric's meaning once, for every configuration. A function is then moved into logic by a configuration and one more proof: that under this meaning, the configuration computes the function. This is the first step of the suite's research note docs/research/harden.md.

One instruction, a loaded meaning

fab rd, rs1, rs2, rs3 is R-type with a fourth register (R4, as RISC-V's fused multiply-add is) on the custom-2 opcode, 1011011, with funct3 and funct2 0; any other funct3 or funct2 there is an illegal instruction. Its value is the last cell's for a = rs1, b = rs2 and c = rs3. Three operands, because the first functions it hardens, SHA-256's Ch and Maj, take three words, and packing two words into one register would make the caller differ from the software it replaces.

Each cell reads three sources, x, y and z: zero, a, b, c, or one of the previous layer's four cells. It applies one of four operations on 64-bit words:

• logic: bit i of the result is bit (4 x_i + 2 y_i + z_i) of an 8-bit table, applied to every bit, as AVX-512's vpternlog does. Ch is the table 0xCA, Maj 0xE8, x ^ y ^ z 0x96, and x alone 0xF0.
• add: x + y + z, modulo 2⁶⁴.
• add32: the same on the low 32 bits, sign-extended, as RV64's W instructions are.
• rotate or shift x right by a constant, on 64 bits or on the low 32 (sign-extended), the core's own rotate.

A cell's configuration is 19 bits: op (1:0), the sources (4:2, 7:5, 10:8) and an 8-bit immediate (18:11), the table or the shift. Cell i is CSR 0x7C0 + i, which only machine mode can reach, and a cell keeps only its 19 bits. Until a configuration is written every cell is 0, a table of zeros, so fab gives 0. It is never illegal for want of one.

Try a configuration

The three configurations are read from fabric.sysr as it is now. Pick one, change the operands, or type a cell's 19 bits in hex: the figure evaluates each cell as fabric-cell says, layer by layer, and marks the cells the result depends on. For the SHA-256 configurations it also computes the function the way FIPS 180-4 writes it, on the operands' low words, for comparison.

a (rs1) b (rs2) c (rs3)

Proven once, then once per configuration

The meaning is fabric-layer: four applications of fabric-cell to the operands and the previous layer's values. The proofs climb from a cell to the whole fabric. Each module is known to the one above it only by its contract, so each proof is small:

The last proof goes through the layers' contracts, so it is about the meaning, not the gates: the configuration computes the function under fabric-layer, and the hardware computes fabric-layer. A compiler that makes configurations need not be trusted, since each of its outputs is checked this way. That is how sysi treats its own outputs (translation validation).

The meaning is stated layer by layer and never as one function of the whole configuration. Written as one spec, each layer is inlined into the next, and each copy of a source appears a dozen times in the cell that reads it. That is more than sysr's checker can expand. Stated per layer, the layers' values are wires that the next layer's contract names.

In the core

fab is one of the M unit's instructions. isa.sysr's exec-spec decodes it and says only that its value comes from elsewhere, as for a multiplication. The core reads a third register (a third port on the register file) in the cycle fab executes. The fabric unit registers the net's value then, and the value is written back in the next cycle. A fab takes two cycles whatever its configuration and operands, so the core's Zkt promise, that which cycles execute an instruction is decided by the instructions alone, still proves. The configuration CSRs are fabric-csrs, inside the CSR file.

The ISS, the assembler and the tests

The ISS does not restate the fabric. tools/custom.rkt's fabric-eval evaluates fabric-inputs and then fabric-layer three times, from fabric.sysr itself, layer by layer for the same reason the proofs are stated that way. It charges two cycles. The assembler knows fab rd, rs1, rs2, rs3 and the CSR names fab0 to fab11. programs/fabric.s checks values worked out by hand from FIPS 180-4, not from the fabric's definitions: 0 before a configuration is loaded, then Ch, Maj and T2 on two sets of operands, a cell keeping 19 bits, rd = x0, and the two illegal encodings. The core and the ISS run it and agree cycle for cycle. Random programs configure cells from random registers and run fab and the illegal encodings among everything else. tests/fabric-test.rkt checks the evaluator against the header's description of each operation and against FIPS 180-4 on random operands, and the assembler's encoding.

What comes next

The research note orders the rest. Second, a compiler from a pure sysp function to a configuration, untrusted, with each output proven as fabric-sha256 proves its three. Third, sysk holds configurations as resources and switches a function's calls to fab while the software version stays, proven equal to the same spec. Neither is here. Nor is a sysp contract for fab in isa.sysp: it comes with the compiler, when a caller wants it, since every part that links isa.sysp would prove again. A larger fabric, several configurations kept at once, and real partial reconfiguration of the ECP5 are left for later.