From 7d1dfa9e85953814c976f600520a5460da93a9f4 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 14 Jan 2026 11:02:07 +0100 Subject: [PATCH 01/14] spec: DECODE: decode basics --- spec/book.typ | 1 + spec/decode.typ | 181 +++++++++++++++++++++++++++++++++++++++++++ spec/src/decode.toml | 87 +++++++++++++++++++++ 3 files changed, 269 insertions(+) create mode 100644 spec/decode.typ create mode 100644 spec/src/decode.toml diff --git a/spec/book.typ b/spec/book.typ index 1bf944862..935c8f777 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -8,6 +8,7 @@ #chapter("variables.typ")[Variables] #chapter("is_bit.typ")[IS_BIT template] #chapter("add.typ")[ADD template] + #chapter("decode.typ")[DECODE chip] #chapter("cpu.typ")[CPU chip] #chapter("shift.typ")[SHIFT chip] #chapter("branch.typ")[BRANCH] diff --git a/spec/decode.typ b/spec/decode.typ new file mode 100644 index 000000000..e01828488 --- /dev/null +++ b/spec/decode.typ @@ -0,0 +1,181 @@ +#import "/book.typ": book-page, rj +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_column_table, + total_nr_variables, + total_nr_instantiated_columns, + render_constraint_table, +) + +#let config = load_config() +#let chip = load_chip("src/decode.toml", config) +#show: book-page.with(title: "DECODE chip") + +#let decode = raw(chip.name) + += #decode chip + +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The #decode chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_column_table(chip, config) + +== Decoding +We specify how each instruction should be expressed in the decoding table. Unspecified values are either ++ the corresponding element of the instruction (e.g. `rs1`), or ++ set to $0$ otherwise. + +=== OP-IMM +In general: ++ $#`rs2` = 0$ ++ $#`write_register` = min(1, #`rd`)$ +#table( + columns: (auto, auto, auto), + stroke: 0pt, + inset: (right: 1em), + table.header([*Operation*], [*Op-flag*], [*Other*]), + table.hline(stroke: 1.5pt), + [`ADDI rd, rs1, imm`], [`ADD`], [], + [`SLTI rd, rs1, imm`], [`SLT`], [`signed`], + [`SLTIU rd, rs1, imm`], [`SLT`], [], + [`ANDI rd, rs1, imm`], [`AND`], [], + [`ORI rd, rs1, imm`], [`OR`], [], + [`XORI rd, rs1, imm`], [`XOR`], [], + [`SLLI rd, rs1, imm`], [`SHIFT`], [], + [`SRLI rd, rs1, imm`], [`SHIFT`], [`mp_selector` ], + [`SRAI rd, rs1, imm`], [`SHIFT`], [`mp_selector`, `signed`], +) + +=== LUI / AUIPC +Note: these operations load/add `imm` in/to the upper bits of `rd`/`pc`. +As such, *we expect the decoding to take care of writing the immediate in the upper bits of `imm`*. + +- `LUI rd, imm` #sym.arrow.double.r `ADDI rd, x0, imm` +- `AUIPC rd, imm` #sym.arrow.double.r `ADDI rd, 255, imm` + - Note: PC index $= 255$ + +=== OP +In general: ++ $#`imm` = 0$ ++ $#`write_register` = min(1, #`rd`)$ +#table( + columns: (auto, auto, auto), + stroke: 0pt, + inset: (right: 1em), + table.header([*Operation*], [*Op-flag*], [*Other*]), + table.hline(stroke: 1.5pt), + [`ADD rd, rs1, rs2`], [`ADD`], [], + [`SUB rd, rs1, rs2`], [`SUB`], [], + [`SLT rd, rs1, rs2`], [`SLT`], [`signed`], + [`SLTU rd, rs1, rs2`], [`SLT`], [], + [`AND rd, rs1, rs2`], [`AND`], [], + [`OR rd, rs1, rs2`], [`OR`], [], + [`XOR rd, rs1, rs2`], [`XOR`], [], + [`SLL rd, rs1, rs2`], [`SHIFT`], [], + [`SRL rd, rs1, rs2`], [`SHIFT`], [`mp_selector` ], + [`SRA rd, rs1, rs2`], [`SHIFT`], [`mp_selector`, `signed`], +) + +=== BRANCH +- `JAL rd, imm` #sym.arrow.double.r `JALR rd, 255, imm` + - Note: PC index $= 255$ + +// TODO: JALR + +In general: ++ $#`imm` = 0$ ++ $#`write_register` = 0$ +#table( + columns: (auto, auto, auto), + stroke: 0pt, + inset: (right: 1em), + table.header([*Operation*], [*Op-flag*], [*Other*]), + table.hline(stroke: 1.5pt), + [`BEQ pc, rs1, rs2, imm`], [`BEQ`], [], + [`BNE pc, rs1, rs2, imm`], [`BEQ`], [`mp_selector`], + [`BLT pc, rs1, rs2, imm`], [`BLT`], [`signed`], + [`BLTU pc, rs1, rs2, imm`], [`BLT`], [], + [`BGE pc, rs1, rs2, imm`], [`BLT`], [`signed`, `mp_selector`], + [`BGEU pc, rs1, rs2, imm`], [`BLT`], [`mp_selector`], +) +*Note*: "BGT, BGTU, BLE, and BLEU can be synthesized by reversing the operands to BLT, BLTU, BGE, and BGEU, respectively", RISC-V unprivileged ISA, page 32. In other words, these four operations are pseudo-instructions. + + +=== LOAD +#table( + columns: (auto, auto, auto), + stroke: 0pt, + inset: (right: 1em), + table.header([*Operation*], [*Op-flag*], [*Other*]), + table.hline(stroke: 1.5pt), + [`LOAD rd, rs1, imm, width, sign_extend`], [`LOAD`], [ + $#`memory_2bytes` := #`width` >= 2$\ + $#`memory_4bytes` := #`width` >= 4$\ + $#`memory_8bytes` := #`width` >= 8$\ + $#`signed` := #`sign_extend`$ + ], +) + +=== STORE +#table( + columns: (auto, auto, auto), + stroke: 0pt, + inset: (right: 1em), + table.header([*Operation*], [*Op-flag*], [*Other*]), + table.hline(stroke: 1.5pt), + [`STORE rs1, rs2, imm, width`], [`STORE`], [ + $#`memory_2bytes` := #`width` >= 2$\ + $#`memory_4bytes` := #`width` >= 4$\ + $#`memory_8bytes` := #`width` >= 8$ + ], +) + + +=== MISC-MEM +- `FENCE` #sym.arrow.double.r `ADDI 0, x0, 0` + - Note: this is a NOP + +=== System +#table( + columns: (auto, auto, auto), + stroke: 0pt, + inset: (right: 1em), + table.header([*Operation*], [*Op-flag*], [*Other*]), + table.hline(stroke: 1.5pt), + [`ECALL`], [`ECALL`], [`write_register`, $#`rs1` := 17$, $#`rs2` := 11$, $#`rd` := 10$], + [`EBREAK`], [`EBREAK`], [], +) + +Note for `ECALL`: +*“On RISC-V a system call has its own instruction: `ECALL`. A system call can have up to 7 arguments and has 1 return value. The arguments are in registers A0-A6, in that order, and the return value is written into A0 before giving back control to the guest. A7 contains the system call number.”* [[src](https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi)] +- syscall number in A7 (= register `x17`) +- first syscall argument in A1 (= register `x11`) +- syscall output in A0 (= register `x10`) + +=== OP (M - extension) +#table( + columns: (auto, auto, auto), + stroke: 0pt, + inset: (right: 1em), + table.header([*Operation*], [*Op-flag*], [*Other*]), + table.hline(stroke: 1.5pt), + [`MUL rd, rs1, rs2`], [`MUL`], [`signed`, `mp_selector`], + [`MULH rd, rs1, rs2`], [`MUL`], [`signed`, `mp_selector`, `muldiv_selector`], + [`MULHU rd, rs1, rs2`], [`MUL`], [`muldiv_selector`], + [`MULHSU rd, rs1, rs2`], [`MUL`], [`signed`, `muldiv_selector`], +) + +#table( + columns: (auto, auto, auto), + stroke: 0pt, + inset: (right: 1em), + table.header([*Operation*], [*Op-flag*], [*Other*]), + table.hline(stroke: 1.5pt), + [`DIV rd, rs1, rs2`], [`DIVREM`], [`signed`], + [`DIVU rd, rs1, rs2`], [`DIVREM`], [], + [`REM rd, rs1, rs2`], [`DIVREM`], [`signed`, `muldiv_selector`], + [`REMU rd, rs1, rs2`], [`DIVREM`], [`muldiv_selector`], +) \ No newline at end of file diff --git a/spec/src/decode.toml b/spec/src/decode.toml new file mode 100644 index 000000000..7490e688a --- /dev/null +++ b/spec/src/decode.toml @@ -0,0 +1,87 @@ +name = "DECODE" + +[[variables.output]] +name = "pc" +type = "DWordWL" +desc = "value of the program counter this instruction is associated with." + +[[variables.output]] +name = "rs1" +type = "Byte" +desc = "index of source register 1." + +[[variables.output]] +name = "rs2" +type = "Byte" +desc = "index of source register 2." + +[[variables.output]] +name = "rd" +type = "Byte" +desc = "index of destination register." + +[[variables.output]] +name = "write_register" +type = "Bit" +desc = "whether the result should be written to `rd` ($=0$ for memory write and when $#`rd` = #`x0`$." + +[[variables.output]] +name = "memory_2bytes" +type = "Bit" +desc = "whether the memory access (read or write) touches at least $2$ bytes." + +[[variables.output]] +name = "memory_4bytes" +type = "Bit" +desc = "whether the memory access (read or write) touches at least $4$ bytes." + +[[variables.output]] +name = "memory_8bytes" +type = "Bit" +desc = "whether the memory access (read or write) touches at least $8$ bytes." + +[[variables.output]] +name = "c_type" +type = "Bit" +desc = "Whether the instruction is of type `C`, i.e., whether it is $2$ bytes long instead of $4$." + +[[variables.output]] +name = "imm" +type = "DWordWL" +desc = "the *fully extended (!)* 64-bit version of the immediate." + +[[variables.output]] +name = "signed" +type = "Bit" +desc = "selector used to indicate signed or unsigned input interpretation. Currently, this is used to choose between ." + +[[variables.output]] +name = "mp_selector" +type = "Bit" +desc = """Multi-purpose selector used by different ALU operations for different purposes. Currently, it is used + - by the `MUL` chip to select between `MUL`/`MULH` and `MULH[S]U`, and + - as flag for inverting the condition of conditional branches (see `branch_cond`) + - as direction (left or right) for `SHIFT`""" + +[[variables.output]] +name = "muldiv_selector" +type = "Bit" +desc = "selects which output of `MUL` (lo/hi) or `DVRM` (quo/rem) is wanted." + +[[variables.output]] +name = "word_instr" +type = "Bit" +desc = "Whether the instruction is a `*W` instruction, requiring the inputs and outputs to be (sign) extended" + +[[variables.output]] +name = "one_hot" +type = ["Bit", 16] +desc = "A 16-column vector comprised of the flags `(ADD, SUB, SLT, AND, OR, XOR, SHIFT, JALR, BEQ, BLT, LOAD, STORE, MUL, DIVREM, ECALL, EBREAK)`. The vector is 'one-hot', meaning that in every row exactly one element is $1$; the others are $0$." + +[[variables.multiplicity]] +name = "μ" +type = "BaseField" +desc = "The multiplicity with which this instruction is looked up in the `CPU` table." + + + From a46c087315c33198d9ef2a6d2ac5a8c77bbbb6a0 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 14 Jan 2026 12:30:39 +0100 Subject: [PATCH 02/14] spec: DECODE: update table + add *W instructions --- spec/decode.typ | 233 +++++++++++++++++++------------------------ spec/src/decode.toml | 2 +- 2 files changed, 104 insertions(+), 131 deletions(-) diff --git a/spec/decode.typ b/spec/decode.typ index e01828488..38bf9409a 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -23,159 +23,132 @@ The #decode chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: #render_chip_column_table(chip, config) +#pagebreak() == Decoding We specify how each instruction should be expressed in the decoding table. Unspecified values are either + the corresponding element of the instruction (e.g. `rs1`), or + set to $0$ otherwise. -=== OP-IMM -In general: -+ $#`rs2` = 0$ -+ $#`write_register` = min(1, #`rd`)$ +// Subheader for the following table +#let subheader(title, common) = { + ( + table.header( + level: 2, + table.cell(colspan:2, [#emph(title)]), + if common != [] { + [_Common: #(common)_] + } else { + [] + } + ), + table.hline(stroke: .5pt) + ) +} + #table( - columns: (auto, auto, auto), + columns: (110pt, auto, auto), stroke: 0pt, inset: (right: 1em), + align: left + bottom, table.header([*Operation*], [*Op-flag*], [*Other*]), table.hline(stroke: 1.5pt), + + ..subheader("OP-IMM", [$#`rs2`:=0$, $#`write_register` := (#`rd` eq.not 0)$]), + table.hline(stroke: .5pt), [`ADDI rd, rs1, imm`], [`ADD`], [], + [`ADDIW rd, rs1, imm`], [`ADD`], [`word_instr`], [`SLTI rd, rs1, imm`], [`SLT`], [`signed`], [`SLTIU rd, rs1, imm`], [`SLT`], [], [`ANDI rd, rs1, imm`], [`AND`], [], [`ORI rd, rs1, imm`], [`OR`], [], [`XORI rd, rs1, imm`], [`XOR`], [], [`SLLI rd, rs1, imm`], [`SHIFT`], [], - [`SRLI rd, rs1, imm`], [`SHIFT`], [`mp_selector` ], + [`SLLIW rd, rs1, imm`], [`SHIFT`], [`word_instr`], + [`SRLI rd, rs1, imm`], [`SHIFT`], [`mp_selector`], + [`SRLIW rd, rs1, imm`], [`SHIFT`], [`mp_selector`, `word_instr`], [`SRAI rd, rs1, imm`], [`SHIFT`], [`mp_selector`, `signed`], -) - -=== LUI / AUIPC -Note: these operations load/add `imm` in/to the upper bits of `rd`/`pc`. -As such, *we expect the decoding to take care of writing the immediate in the upper bits of `imm`*. - -- `LUI rd, imm` #sym.arrow.double.r `ADDI rd, x0, imm` -- `AUIPC rd, imm` #sym.arrow.double.r `ADDI rd, 255, imm` - - Note: PC index $= 255$ - -=== OP -In general: -+ $#`imm` = 0$ -+ $#`write_register` = min(1, #`rd`)$ -#table( - columns: (auto, auto, auto), - stroke: 0pt, - inset: (right: 1em), - table.header([*Operation*], [*Op-flag*], [*Other*]), - table.hline(stroke: 1.5pt), - [`ADD rd, rs1, rs2`], [`ADD`], [], - [`SUB rd, rs1, rs2`], [`SUB`], [], - [`SLT rd, rs1, rs2`], [`SLT`], [`signed`], - [`SLTU rd, rs1, rs2`], [`SLT`], [], - [`AND rd, rs1, rs2`], [`AND`], [], - [`OR rd, rs1, rs2`], [`OR`], [], - [`XOR rd, rs1, rs2`], [`XOR`], [], - [`SLL rd, rs1, rs2`], [`SHIFT`], [], - [`SRL rd, rs1, rs2`], [`SHIFT`], [`mp_selector` ], - [`SRA rd, rs1, rs2`], [`SHIFT`], [`mp_selector`, `signed`], -) - -=== BRANCH -- `JAL rd, imm` #sym.arrow.double.r `JALR rd, 255, imm` - - Note: PC index $= 255$ - -// TODO: JALR - -In general: -+ $#`imm` = 0$ -+ $#`write_register` = 0$ -#table( - columns: (auto, auto, auto), - stroke: 0pt, - inset: (right: 1em), - table.header([*Operation*], [*Op-flag*], [*Other*]), - table.hline(stroke: 1.5pt), - [`BEQ pc, rs1, rs2, imm`], [`BEQ`], [], - [`BNE pc, rs1, rs2, imm`], [`BEQ`], [`mp_selector`], - [`BLT pc, rs1, rs2, imm`], [`BLT`], [`signed`], - [`BLTU pc, rs1, rs2, imm`], [`BLT`], [], - [`BGE pc, rs1, rs2, imm`], [`BLT`], [`signed`, `mp_selector`], - [`BGEU pc, rs1, rs2, imm`], [`BLT`], [`mp_selector`], -) -*Note*: "BGT, BGTU, BLE, and BLEU can be synthesized by reversing the operands to BLT, BLTU, BGE, and BGEU, respectively", RISC-V unprivileged ISA, page 32. In other words, these four operations are pseudo-instructions. - - -=== LOAD -#table( - columns: (auto, auto, auto), - stroke: 0pt, - inset: (right: 1em), - table.header([*Operation*], [*Op-flag*], [*Other*]), - table.hline(stroke: 1.5pt), - [`LOAD rd, rs1, imm, width, sign_extend`], [`LOAD`], [ - $#`memory_2bytes` := #`width` >= 2$\ - $#`memory_4bytes` := #`width` >= 4$\ - $#`memory_8bytes` := #`width` >= 8$\ - $#`signed` := #`sign_extend`$ - ], -) - -=== STORE -#table( - columns: (auto, auto, auto), - stroke: 0pt, - inset: (right: 1em), - table.header([*Operation*], [*Op-flag*], [*Other*]), - table.hline(stroke: 1.5pt), - [`STORE rs1, rs2, imm, width`], [`STORE`], [ - $#`memory_2bytes` := #`width` >= 2$\ - $#`memory_4bytes` := #`width` >= 4$\ - $#`memory_8bytes` := #`width` >= 8$ - ], -) - - -=== MISC-MEM -- `FENCE` #sym.arrow.double.r `ADDI 0, x0, 0` - - Note: this is a NOP - -=== System -#table( - columns: (auto, auto, auto), - stroke: 0pt, - inset: (right: 1em), - table.header([*Operation*], [*Op-flag*], [*Other*]), - table.hline(stroke: 1.5pt), - [`ECALL`], [`ECALL`], [`write_register`, $#`rs1` := 17$, $#`rs2` := 11$, $#`rd` := 10$], + [`SRAIW rd, rs1, imm`], [`SHIFT`], [`mp_selector`, `signed`, `word_instr`], + + ..subheader("LUI/AUIPC", []), + [`LUI rd, imm`], [#sym.arrow.double.r], [`ADDI rd, x0, imm`], + [`AUIPC rd, imm`], [#sym.arrow.double.r#footnote("The program counter (pc) is stored in register 255.")], [`ADDI rd, 255, imm`], + + ..subheader("OP", [$#`imm`:=0$, $#`write_register` := (#`rd` eq.not 0)$]), + [`ADD rd, rs1, rs2`], [`ADD`], [], + [`ADDW rd, rs1, rs2`], [`ADD`], [`word_instr`], + [`SUB rd, rs1, rs2`], [`SUB`], [], + [`SUBW rd, rs1, rs2`], [`SUB`], [`word_instr`], + [`SLT rd, rs1, rs2`], [`SLT`], [`signed`], + [`SLTU rd, rs1, rs2`], [`SLT`], [], + [`AND rd, rs1, rs2`], [`AND`], [], + [`OR rd, rs1, rs2`], [`OR`], [], + [`XOR rd, rs1, rs2`], [`XOR`], [], + [`SLL rd, rs1, rs2`], [`SHIFT`], [], + [`SLLW rd, rs1, rs2`], [`SHIFT`], [`word_instr`], + [`SRL rd, rs1, rs2`], [`SHIFT`], [`mp_selector`], + [`SRLW rd, rs1, rs2`], [`SHIFT`], [`mp_selector`, `word_instr`], + [`SRA rd, rs1, rs2`], [`SHIFT`], [`mp_selector`, `signed`], + [`SRAW rd, rs1, rs2`], [`SHIFT`], [`mp_selector`, `signed`, `word_instr`], + + ..subheader("BRANCHING (unconditional)", []), + [`JAL rd, imm`], [#sym.arrow.double.r#footnote()], [`JALR rd, 255, imm`], + [`JALR rd, rs1, imm`], [`JALR`], [$#`write_register` := #`rd` eq.not 0$], + + ..subheader("BRANCHING (conditional)", [$#`write_register` := 0$]), + [`BEQ rs1, rs2, imm`], [`BEQ`], [], + [`BNE rs1, rs2, imm`], [`BEQ`], [`mp_selector`], + [`BLT rs1, rs2, imm`], [`BLT`], [`signed`], + [`BLTU rs1, rs2, imm`], [`BLT`], [], + [`BGE rs1, rs2, imm`], [`BLT`], [`signed`, `mp_selector`], + [`BGEU rs1, rs2, imm`], [`BLT`], [`mp_selector`], + [`BGT rs1, rs2, imm`], [#sym.arrow.double.r #footnote["BGT, BGTU, BLE, and BLEU can be synthesized by reversing the operands to BLT, BLTU, BGE, and BGEU, respectively", RISC-V unprivileged ISA, page 32.] ], [`BLT ` *`rs2, rs1`*,` imm`], + [`BGTU rs1, rs2, imm`], [#sym.arrow.double.r #footnote()], [`BLTU` *`rs2, rs1`*,` imm`], + [`BLE rs1, rs2, imm`], [#sym.arrow.double.r #footnote()], [`BGE ` *`rs2, rs1`*,` imm`], + [`BLEU rs1, rs2, imm`], [#sym.arrow.double.r #footnote()], [`BGEU` *`rs2, rs1`*,` imm`], + + ..subheader("LOAD", []), + [`LD rd, rs1, imm`], [`LOAD`], [`memory_2bytes`, `memory_4bytes`, `memory_8bytes`], + [`LW rd, rs1, imm`], [`LOAD`], [`memory_2bytes`, `memory_4bytes`, `signed`], + [`LWU rd, rs1, imm`], [`LOAD`], [`memory_2bytes`, `memory_4bytes`], + [`LH rd, rs1, imm`], [`LOAD`], [`memory_2bytes`, `signed`], + [`LHU rd, rs1, imm`], [`LOAD`], [`memory_2bytes`], + [`LB rd, rs1, imm`], [`LOAD`], [`signed`], + [`LBU rd, rs1, imm`], [`LOAD`], [], + + ..subheader("STORE", []), + [`SD rs1, rs2, imm`], [`STORE`], [`memory_2bytes`, `memory_4bytes`, `memory_8bytes`], + [`SW rs1, rs2, imm`], [`STORE`], [`memory_2bytes`, `memory_4bytes`], + [`SH rs1, rs2, imm`], [`STORE`], [`memory_2bytes`], + [`SB rs1, rs2, imm`], [`STORE`], [], + + ..subheader("SYSTEM", []), + [`ECALL`], [`ECALL`], [`write_register`, $#`rs1` := #`x17`$, $#`rs2` := #`x11`$, $#`rd` := #`x10`$], [`EBREAK`], [`EBREAK`], [], -) - -Note for `ECALL`: -*“On RISC-V a system call has its own instruction: `ECALL`. A system call can have up to 7 arguments and has 1 return value. The arguments are in registers A0-A6, in that order, and the return value is written into A0 before giving back control to the guest. A7 contains the system call number.”* [[src](https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi)] -- syscall number in A7 (= register `x17`) -- first syscall argument in A1 (= register `x11`) -- syscall output in A0 (= register `x10`) -=== OP (M - extension) -#table( - columns: (auto, auto, auto), - stroke: 0pt, - inset: (right: 1em), - table.header([*Operation*], [*Op-flag*], [*Other*]), - table.hline(stroke: 1.5pt), + ..subheader("OP (M-extension)", [$#`imm` := 0$, $#`write_register` := #`rd` eq.not 0$]), [`MUL rd, rs1, rs2`], [`MUL`], [`signed`, `mp_selector`], + [`MULW rd, rs1, rs2`], [`MUL`], [`signed`, `mp_selector`, `word_instr`], [`MULH rd, rs1, rs2`], [`MUL`], [`signed`, `mp_selector`, `muldiv_selector`], [`MULHU rd, rs1, rs2`], [`MUL`], [`muldiv_selector`], [`MULHSU rd, rs1, rs2`], [`MUL`], [`signed`, `muldiv_selector`], + [`DIV rd, rs1, rs2`], [`DIVREM`], [`signed`], + [`DIVW rd, rs1, rs2`], [`DIVREM`], [`signed`, `word_instr`], + [`DIVU rd, rs1, rs2`], [`DIVREM`], [], + [`DIVUW rd, rs1, rs2`], [`DIVREM`], [`word_instr`], + [`REM rd, rs1, rs2`], [`DIVREM`], [`signed`, `muldiv_selector`], + [`REMW rd, rs1, rs2`], [`DIVREM`], [`signed`, `muldiv_selector`, `word_instr`], + [`REMU rd, rs1, rs2`], [`DIVREM`], [`muldiv_selector`], + [`REMUW rd, rs1, rs2`], [`DIVREM`], [`muldiv_selector`, `word_instr`], + + ..subheader("MISC", []), + [`FENCE`], [#sym.arrow.double.r#footnote("Note: this is a no-op")], [`ADDI 0, x0, 0`], ) -#table( - columns: (auto, auto, auto), - stroke: 0pt, - inset: (right: 1em), - table.header([*Operation*], [*Op-flag*], [*Other*]), - table.hline(stroke: 1.5pt), - [`DIV rd, rs1, rs2`], [`DIVREM`], [`signed`], - [`DIVU rd, rs1, rs2`], [`DIVREM`], [], - [`REM rd, rs1, rs2`], [`DIVREM`], [`signed`, `muldiv_selector`], - [`REMU rd, rs1, rs2`], [`DIVREM`], [`muldiv_selector`], -) \ No newline at end of file +=== Notes +- LUI/AUIPC: these operations load/add `imm` in/to the upper bits of `rd`/`pc`. As such, *we expect the decoding to take care of writing the immediate in the upper bits of `imm`*. +- ECALL: + "On RISC-V a system call has its own instruction: `ECALL`. A system call can have up to 7 arguments and has 1 return value. The arguments are in registers A0-A6, in that order, and the return value is written into A0 before giving back control to the guest. A7 contains the system call number." #link("https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[source]] + As such, + - syscall number in A7 (= register `x17`) + - first syscall argument in A1 (= register `x11`) + - syscall output in A0 (= register `x10`) diff --git a/spec/src/decode.toml b/spec/src/decode.toml index 7490e688a..0d7882853 100644 --- a/spec/src/decode.toml +++ b/spec/src/decode.toml @@ -71,7 +71,7 @@ desc = "selects which output of `MUL` (lo/hi) or `DVRM` (quo/rem) is wanted." [[variables.output]] name = "word_instr" type = "Bit" -desc = "Whether the instruction is a `*W` instruction, requiring the inputs and outputs to be (sign) extended" +desc = "Whether the instruction is a `*W` instruction, requiring the inputs and outputs to be (sign) extended." [[variables.output]] name = "one_hot" From b84731c60adc6572d49dadd730b36bdaa814d153 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 15 Jan 2026 16:50:22 +0100 Subject: [PATCH 03/14] spec: fix padding table for chips that don't have all types of variables --- spec/chip.typ | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/spec/chip.typ b/spec/chip.typ index 4e7d6a143..83b99e8ec 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -57,7 +57,7 @@ .all(t => t.at("preprocessed", default: false)) } - let instantiated_vars = config.variables.categories.instantiated.map(c => chip.variables.at(c)).flatten() + let instantiated_vars = config.variables.categories.instantiated.map(c => chip.variables.at(c, default: ())).flatten() show figure: set block(breakable: true) figure(table( @@ -197,6 +197,7 @@ cref(assumption)[#figure(kind: chip.name + "assumption", numbering: (i) => [#lbl#i], supplement: [], [])] } + show figure: set block(breakable: true) figure(table( columns: (auto, auto, 1fr), inset: 6pt, From 1cce50c8c6e7ddeb66b453d31ef1217819cb9354 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 15 Jan 2026 16:50:34 +0100 Subject: [PATCH 04/14] spec: introduce B49 --- spec/src/config.toml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/spec/src/config.toml b/spec/src/config.toml index 68f1683de..bbdb0d548 100644 --- a/spec/src/config.toml +++ b/spec/src/config.toml @@ -58,6 +58,11 @@ label = "B35" subtypes = ["BaseField"] desc = "Variable that can only assume values in the range $[0, 2^35)$." +[[variables.types]] +label = "B49" +subtypes = ["BaseField"] +desc = "Variable that can only assume values in the range $[0, 2^49)$." + [[variables.types]] label = "B51" subtypes = ["BaseField"] From a1171ee88d242ef686d97fdd0938078f5b9c637f Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 15 Jan 2026 16:50:58 +0100 Subject: [PATCH 05/14] spec: DECODE: split-off decode uncompressed --- spec/book.typ | 1 + spec/decode.typ | 139 ++------------------------ spec/decode_uncompressed.typ | 125 +++++++++++++++++++++++ spec/src/decode.toml | 111 ++++++++------------- spec/src/decode_uncompressed.toml | 159 ++++++++++++++++++++++++++++++ 5 files changed, 334 insertions(+), 201 deletions(-) create mode 100644 spec/decode_uncompressed.typ create mode 100644 spec/src/decode_uncompressed.toml diff --git a/spec/book.typ b/spec/book.typ index 935c8f777..c65ff2e1b 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -9,6 +9,7 @@ #chapter("is_bit.typ")[IS_BIT template] #chapter("add.typ")[ADD template] #chapter("decode.typ")[DECODE chip] + #chapter("decode_uncompressed.typ")[DECODE (uncompressed) chip] #chapter("cpu.typ")[CPU chip] #chapter("shift.typ")[SHIFT chip] #chapter("branch.typ")[BRANCH] diff --git a/spec/decode.typ b/spec/decode.typ index 38bf9409a..5379b2e6b 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -6,6 +6,7 @@ total_nr_variables, total_nr_instantiated_columns, render_constraint_table, + render_chip_padding_table, ) #let config = load_config() @@ -14,7 +15,10 @@ #let decode = raw(chip.name) -= #decode chip += #decode table +All `RV64IM` instruction are to be encoded in a format that can be interpreted by the VM. +This section outlines the decoding table in its compressed form, as it is being used in the VM. +Since reasoning about this compressed form is needlessly complex, the `decode (uncompressed)` section presents the same table in uncompressed form, and explains how a construct the table from `RV64IM` assembly instructions. == Columns #let nr_variables = total_nr_variables(chip) @@ -23,132 +27,7 @@ The #decode chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: #render_chip_column_table(chip, config) -#pagebreak() -== Decoding -We specify how each instruction should be expressed in the decoding table. Unspecified values are either -+ the corresponding element of the instruction (e.g. `rs1`), or -+ set to $0$ otherwise. - -// Subheader for the following table -#let subheader(title, common) = { - ( - table.header( - level: 2, - table.cell(colspan:2, [#emph(title)]), - if common != [] { - [_Common: #(common)_] - } else { - [] - } - ), - table.hline(stroke: .5pt) - ) -} - -#table( - columns: (110pt, auto, auto), - stroke: 0pt, - inset: (right: 1em), - align: left + bottom, - table.header([*Operation*], [*Op-flag*], [*Other*]), - table.hline(stroke: 1.5pt), - - ..subheader("OP-IMM", [$#`rs2`:=0$, $#`write_register` := (#`rd` eq.not 0)$]), - table.hline(stroke: .5pt), - [`ADDI rd, rs1, imm`], [`ADD`], [], - [`ADDIW rd, rs1, imm`], [`ADD`], [`word_instr`], - [`SLTI rd, rs1, imm`], [`SLT`], [`signed`], - [`SLTIU rd, rs1, imm`], [`SLT`], [], - [`ANDI rd, rs1, imm`], [`AND`], [], - [`ORI rd, rs1, imm`], [`OR`], [], - [`XORI rd, rs1, imm`], [`XOR`], [], - [`SLLI rd, rs1, imm`], [`SHIFT`], [], - [`SLLIW rd, rs1, imm`], [`SHIFT`], [`word_instr`], - [`SRLI rd, rs1, imm`], [`SHIFT`], [`mp_selector`], - [`SRLIW rd, rs1, imm`], [`SHIFT`], [`mp_selector`, `word_instr`], - [`SRAI rd, rs1, imm`], [`SHIFT`], [`mp_selector`, `signed`], - [`SRAIW rd, rs1, imm`], [`SHIFT`], [`mp_selector`, `signed`, `word_instr`], - - ..subheader("LUI/AUIPC", []), - [`LUI rd, imm`], [#sym.arrow.double.r], [`ADDI rd, x0, imm`], - [`AUIPC rd, imm`], [#sym.arrow.double.r#footnote("The program counter (pc) is stored in register 255.")], [`ADDI rd, 255, imm`], - - ..subheader("OP", [$#`imm`:=0$, $#`write_register` := (#`rd` eq.not 0)$]), - [`ADD rd, rs1, rs2`], [`ADD`], [], - [`ADDW rd, rs1, rs2`], [`ADD`], [`word_instr`], - [`SUB rd, rs1, rs2`], [`SUB`], [], - [`SUBW rd, rs1, rs2`], [`SUB`], [`word_instr`], - [`SLT rd, rs1, rs2`], [`SLT`], [`signed`], - [`SLTU rd, rs1, rs2`], [`SLT`], [], - [`AND rd, rs1, rs2`], [`AND`], [], - [`OR rd, rs1, rs2`], [`OR`], [], - [`XOR rd, rs1, rs2`], [`XOR`], [], - [`SLL rd, rs1, rs2`], [`SHIFT`], [], - [`SLLW rd, rs1, rs2`], [`SHIFT`], [`word_instr`], - [`SRL rd, rs1, rs2`], [`SHIFT`], [`mp_selector`], - [`SRLW rd, rs1, rs2`], [`SHIFT`], [`mp_selector`, `word_instr`], - [`SRA rd, rs1, rs2`], [`SHIFT`], [`mp_selector`, `signed`], - [`SRAW rd, rs1, rs2`], [`SHIFT`], [`mp_selector`, `signed`, `word_instr`], - - ..subheader("BRANCHING (unconditional)", []), - [`JAL rd, imm`], [#sym.arrow.double.r#footnote()], [`JALR rd, 255, imm`], - [`JALR rd, rs1, imm`], [`JALR`], [$#`write_register` := #`rd` eq.not 0$], - - ..subheader("BRANCHING (conditional)", [$#`write_register` := 0$]), - [`BEQ rs1, rs2, imm`], [`BEQ`], [], - [`BNE rs1, rs2, imm`], [`BEQ`], [`mp_selector`], - [`BLT rs1, rs2, imm`], [`BLT`], [`signed`], - [`BLTU rs1, rs2, imm`], [`BLT`], [], - [`BGE rs1, rs2, imm`], [`BLT`], [`signed`, `mp_selector`], - [`BGEU rs1, rs2, imm`], [`BLT`], [`mp_selector`], - [`BGT rs1, rs2, imm`], [#sym.arrow.double.r #footnote["BGT, BGTU, BLE, and BLEU can be synthesized by reversing the operands to BLT, BLTU, BGE, and BGEU, respectively", RISC-V unprivileged ISA, page 32.] ], [`BLT ` *`rs2, rs1`*,` imm`], - [`BGTU rs1, rs2, imm`], [#sym.arrow.double.r #footnote()], [`BLTU` *`rs2, rs1`*,` imm`], - [`BLE rs1, rs2, imm`], [#sym.arrow.double.r #footnote()], [`BGE ` *`rs2, rs1`*,` imm`], - [`BLEU rs1, rs2, imm`], [#sym.arrow.double.r #footnote()], [`BGEU` *`rs2, rs1`*,` imm`], - - ..subheader("LOAD", []), - [`LD rd, rs1, imm`], [`LOAD`], [`memory_2bytes`, `memory_4bytes`, `memory_8bytes`], - [`LW rd, rs1, imm`], [`LOAD`], [`memory_2bytes`, `memory_4bytes`, `signed`], - [`LWU rd, rs1, imm`], [`LOAD`], [`memory_2bytes`, `memory_4bytes`], - [`LH rd, rs1, imm`], [`LOAD`], [`memory_2bytes`, `signed`], - [`LHU rd, rs1, imm`], [`LOAD`], [`memory_2bytes`], - [`LB rd, rs1, imm`], [`LOAD`], [`signed`], - [`LBU rd, rs1, imm`], [`LOAD`], [], - - ..subheader("STORE", []), - [`SD rs1, rs2, imm`], [`STORE`], [`memory_2bytes`, `memory_4bytes`, `memory_8bytes`], - [`SW rs1, rs2, imm`], [`STORE`], [`memory_2bytes`, `memory_4bytes`], - [`SH rs1, rs2, imm`], [`STORE`], [`memory_2bytes`], - [`SB rs1, rs2, imm`], [`STORE`], [], - - ..subheader("SYSTEM", []), - [`ECALL`], [`ECALL`], [`write_register`, $#`rs1` := #`x17`$, $#`rs2` := #`x11`$, $#`rd` := #`x10`$], - [`EBREAK`], [`EBREAK`], [], - - ..subheader("OP (M-extension)", [$#`imm` := 0$, $#`write_register` := #`rd` eq.not 0$]), - [`MUL rd, rs1, rs2`], [`MUL`], [`signed`, `mp_selector`], - [`MULW rd, rs1, rs2`], [`MUL`], [`signed`, `mp_selector`, `word_instr`], - [`MULH rd, rs1, rs2`], [`MUL`], [`signed`, `mp_selector`, `muldiv_selector`], - [`MULHU rd, rs1, rs2`], [`MUL`], [`muldiv_selector`], - [`MULHSU rd, rs1, rs2`], [`MUL`], [`signed`, `muldiv_selector`], - [`DIV rd, rs1, rs2`], [`DIVREM`], [`signed`], - [`DIVW rd, rs1, rs2`], [`DIVREM`], [`signed`, `word_instr`], - [`DIVU rd, rs1, rs2`], [`DIVREM`], [], - [`DIVUW rd, rs1, rs2`], [`DIVREM`], [`word_instr`], - [`REM rd, rs1, rs2`], [`DIVREM`], [`signed`, `muldiv_selector`], - [`REMW rd, rs1, rs2`], [`DIVREM`], [`signed`, `muldiv_selector`, `word_instr`], - [`REMU rd, rs1, rs2`], [`DIVREM`], [`muldiv_selector`], - [`REMUW rd, rs1, rs2`], [`DIVREM`], [`muldiv_selector`, `word_instr`], - - ..subheader("MISC", []), - [`FENCE`], [#sym.arrow.double.r#footnote("Note: this is a no-op")], [`ADDI 0, x0, 0`], -) - -=== Notes -- LUI/AUIPC: these operations load/add `imm` in/to the upper bits of `rd`/`pc`. As such, *we expect the decoding to take care of writing the immediate in the upper bits of `imm`*. -- ECALL: - "On RISC-V a system call has its own instruction: `ECALL`. A system call can have up to 7 arguments and has 1 return value. The arguments are in registers A0-A6, in that order, and the return value is written into A0 before giving back control to the guest. A7 contains the system call number." #link("https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[source]] - As such, - - syscall number in A7 (= register `x17`) - - first syscall argument in A1 (= register `x11`) - - syscall output in A0 (= register `x10`) +== Padding +The #decode table must be padded to a length that is a power of two. +Empty rows with the following content can be added to achieve this: +#render_chip_padding_table(chip, config) diff --git a/spec/decode_uncompressed.typ b/spec/decode_uncompressed.typ new file mode 100644 index 000000000..ace63cdb4 --- /dev/null +++ b/spec/decode_uncompressed.typ @@ -0,0 +1,125 @@ +#import "/book.typ": book-page, rj +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_column_table, + total_nr_variables, + total_nr_instantiated_columns, + render_constraint_table, +) + +#let config = load_config() +#let chip = load_chip("src/decode_uncompressed.toml", config) +#show: book-page.with(title: "DECODE chip") + +#let decode = raw(chip.name) + += #decode table (uncompressed) +This table is not used in practice: it is solely used to explain how one is to fill the (compressed) #decode table. + +== Columns +For the purposes of this explanation, we decompress the `packed_decode` column into its constituent variables: +#render_chip_column_table(chip, config) + +== Decoding +The following table illustrates how each instruction should be expressed in the decoding table. +For the purpose of brevity, some values are not explicitly specified. +Here, ++ the corresponding element of the instruction (in the case of `rs1`, `rs2`, `rd`), or ++ set to $0$ otherwise. + +// Subheader for the following table +#let subheader(title, common) = { + ( + table.header( + level: 2, + table.cell(colspan:2, [#emph(title)]), + if common != [] { + [_Common: #(common)_] + } else { + [] + } + ), + table.hline(stroke: .5pt) + ) +} + +#table( + columns: (130pt, auto, auto), + stroke: 0pt, + inset: (right: 1em), + align: left + bottom, + table.header([*Operation*], [*Op-flag*], [*Other*]), + table.hline(stroke: 1.5pt), + + ..subheader("OP-IMM", [$#`rs2`:=0$, $#`write_register` := (#`rd` eq.not 0)$]), + [`ADDI[W] rd, rs1, imm`], [`ADD`], [$#`word_instr` := #`[W]`$], + [`SLTI[U] rd, rs1, imm`], [`SLT`], [$#`signed` := not#`[U]`$], + [`ANDI rd, rs1, imm`], [`AND`], [], + [`ORI rd, rs1, imm`], [`OR`], [], + [`XORI rd, rs1, imm`], [`XOR`], [], + [`SLLI[W] rd, rs1, imm`], [`SHIFT`], [$#`word_instr` := #`[W]`$], + [`SRLI[W] rd, rs1, imm`], [`SHIFT`], [$#`word_instr` := #`[W]`$, $#`mp_selector` := #`1`$], + [`SRAI[W] rd, rs1, imm`], [`SHIFT`], [$#`word_instr` := #`[W]`$, $#`mp_selector` := #`1`$, $#`signed` := #`1`$], + + ..subheader("LUI/AUIPC", []), + [`LUI rd, imm`], [#sym.arrow.double.r], [`ADDI rd, x0, imm`], + [`AUIPC rd, imm`], [#sym.arrow.double.r#footnote("The program counter (pc) is stored in register 255.")], [`ADDI rd, 255, imm`], + + ..subheader("OP", [$#`imm`:=0$, $#`write_register` := (#`rd` eq.not 0)$]), + [`ADD[W] rd, rs1, rs2`], [`ADD`], [$#`word_instr` := #`[W]`$], + [`SUB[W] rd, rs1, rs2`], [`SUB`], [$#`word_instr` := #`[W]`$], + [`SLT[U] rd, rs1, rs2`], [`SLT`], [$#`signed` := not#`[U]`$], + [`AND rd, rs1, rs2`], [`AND`], [], + [`OR rd, rs1, rs2`], [`OR`], [], + [`XOR rd, rs1, rs2`], [`XOR`], [], + [`SLL[W] rd, rs1, rs2`], [`SHIFT`], [$#`word_instr` := #`[W]`$], + [`SRL[W] rd, rs1, rs2`], [`SHIFT`], [$#`word_instr` := #`[W]`$, $#`mp_selector` := #`1`$], + [`SRA[W] rd, rs1, rs2`], [`SHIFT`], [$#`word_instr` := #`[W]`$, $#`mp_selector` := #`1`$, $#`signed` := #`1`$], + + ..subheader("BRANCHING (unconditional)", [$#`write_register` := #`rd` eq.not 0$]), + [`JAL rd, imm`], [#sym.arrow.double.r#footnote()], [`JALR rd, 255, imm`], + [`JALR rd, rs1, imm`], [`JALR`], [], + + ..subheader("BRANCHING (conditional)", [$#`rd` := 0$, $#`write_register` := 0$]), + [`BEQ rs1, rs2, imm`], [`BEQ`], [], + [`BNE rs1, rs2, imm`], [`BEQ`], [`mp_selector`], + [`BLT[U] rs1, rs2, imm`], [`BLT`], [$#`signed` := not#`[U]`$], + [`BGE[U] rs1, rs2, imm`], [`BLT`], [$#`signed` := not#`[U]`$, $#`mp_selector` := 1$], + + ..subheader("LOAD", [$#`rs2` := 0$]), + [`LD rd, rs1, imm`], [`LOAD`], [$#`mem_2b` := 1$, $#`mem_4b` := 1$, $#`mem_8b` := 1$], + [`LW[U] rd, rs1, imm`], [`LOAD`], [$#`signed` := not#`[U]`$, $#`mem_2b` := 1$, $#`mem_4b` := 1$], + [`LH[U] rd, rs1, imm`], [`LOAD`], [$#`signed` := not#`[U]`$, $#`mem_2b` := 1$], + [`LB[U] rd, rs1, imm`], [`LOAD`], [$#`signed` := not#`[U]`$], + + ..subheader("STORE", [$#`rd` := 0$]), + [`SD rs1, rs2, imm`], [`STORE`], [`mem_2b`, `mem_4b`, `mem_8b`], + [`SW rs1, rs2, imm`], [`STORE`], [`mem_2b`, `mem_4b`], + [`SH rs1, rs2, imm`], [`STORE`], [`mem_2b`], + [`SB rs1, rs2, imm`], [`STORE`], [], + + ..subheader("SYSTEM", []), + [`ECALL`], [`ECALL`], [`write_register`, $#`rs1` := #`x17`$, $#`rs2` := #`x11`$, $#`rd` := #`x10`$], + [`EBREAK`], [`EBREAK`], [], + + ..subheader("OP (M-extension)", [$#`imm` := 0$, $#`write_register` := #`rd` eq.not 0$]), + [`MUL[W] rd, rs1, rs2`], [`MUL`], [$#`word_instr` := #`[W]`$, `signed := 1`, `mp_selector`], + [`MULH rd, rs1, rs2`], [`MUL`], [`muldiv_selector`, `signed`, `mp_selector`], + [`MULHU rd, rs1, rs2`], [`MUL`], [`muldiv_selector`], + [`MULHSU rd, rs1, rs2`], [`MUL`], [`muldiv_selector`, `signed`], + [`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`word_instr` := #`[W]`$, $#`signed` := not#`[U]`$], + [`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`word_instr` := #`[W]`$, $#`signed` := not#`[U]`$, `muldiv_selector := 1`], + + ..subheader("MISC", []), + [`FENCE`], [#sym.arrow.double.r#footnote("Note: this is a no-op")], [`ADDI 0, x0, 0`], +) + +=== Notes +- LUI/AUIPC: these operations load/add `imm` in/to the upper bits of `rd`/`pc`. As such, *we expect the decoding to take care of writing the immediate in the upper bits of `imm`*. +- ECALL: + "On RISC-V a system call has its own instruction: `ECALL`. A system call can have up to 7 arguments and has 1 return value. The arguments are in registers A0-A6, in that order, and the return value is written into A0 before giving back control to the guest. A7 contains the system call number." #link("https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[source]] + As such, + - syscall number in A7 (= register `x17`) + - first syscall argument in A1 (= register `x11`) + - syscall output in A0 (= register `x10`) diff --git a/spec/src/decode.toml b/spec/src/decode.toml index 0d7882853..53134404d 100644 --- a/spec/src/decode.toml +++ b/spec/src/decode.toml @@ -4,84 +4,53 @@ name = "DECODE" name = "pc" type = "DWordWL" desc = "value of the program counter this instruction is associated with." - -[[variables.output]] -name = "rs1" -type = "Byte" -desc = "index of source register 1." - -[[variables.output]] -name = "rs2" -type = "Byte" -desc = "index of source register 2." - -[[variables.output]] -name = "rd" -type = "Byte" -desc = "index of destination register." - -[[variables.output]] -name = "write_register" -type = "Bit" -desc = "whether the result should be written to `rd` ($=0$ for memory write and when $#`rd` = #`x0`$." - -[[variables.output]] -name = "memory_2bytes" -type = "Bit" -desc = "whether the memory access (read or write) touches at least $2$ bytes." - -[[variables.output]] -name = "memory_4bytes" -type = "Bit" -desc = "whether the memory access (read or write) touches at least $4$ bytes." - -[[variables.output]] -name = "memory_8bytes" -type = "Bit" -desc = "whether the memory access (read or write) touches at least $8$ bytes." - -[[variables.output]] -name = "c_type" -type = "Bit" -desc = "Whether the instruction is of type `C`, i.e., whether it is $2$ bytes long instead of $4$." +pad = 0 + +[[variables.output]] +name = "packed_decode" +type = "B49" +desc = """Ordered concatenation of several small variables. +The `decode (uncompressed)` section explains the purpose of each variable.\\ +A list of each variable and the bit(-range) in which it is located:\\ +[0:7] `rs1`, \\ +[8:15] `rs2`, \\ +[16:23] `rd`, \\ +[24] `write_register`, \\ +[25] `memory_2bytes`, \\ +[26] `memory_4bytes`, \\ +[27] `memory_8bytes`, \\ +[28] `c_type`, \\ +[29] `signed`, \\ +[30] `mp_selector`, \\ +[31] `muldiv_selector`, \\ +[32] `word_instr`, \\ +[33] `ADD`, \\ +[34] `SUB`, \\ +[35] `SLT`, \\ +[36] `AND`, \\ +[37] `OR`, \\ +[38] `XOR`, \\ +[39] `SHIFT`, \\ +[40] `JALR`, \\ +[41] `BEQ`, \\ +[42] `BLT`, \\ +[43] `LOAD`, \\ +[44] `STORE`, \\ +[45] `MUL`, \\ +[46] `DIVREM`, \\ +[47] `ECALL`, \\ +[48] `EBREAK`. \\ +""" +pad = 0 [[variables.output]] name = "imm" type = "DWordWL" desc = "the *fully extended (!)* 64-bit version of the immediate." - -[[variables.output]] -name = "signed" -type = "Bit" -desc = "selector used to indicate signed or unsigned input interpretation. Currently, this is used to choose between ." - -[[variables.output]] -name = "mp_selector" -type = "Bit" -desc = """Multi-purpose selector used by different ALU operations for different purposes. Currently, it is used - - by the `MUL` chip to select between `MUL`/`MULH` and `MULH[S]U`, and - - as flag for inverting the condition of conditional branches (see `branch_cond`) - - as direction (left or right) for `SHIFT`""" - -[[variables.output]] -name = "muldiv_selector" -type = "Bit" -desc = "selects which output of `MUL` (lo/hi) or `DVRM` (quo/rem) is wanted." - -[[variables.output]] -name = "word_instr" -type = "Bit" -desc = "Whether the instruction is a `*W` instruction, requiring the inputs and outputs to be (sign) extended." - -[[variables.output]] -name = "one_hot" -type = ["Bit", 16] -desc = "A 16-column vector comprised of the flags `(ADD, SUB, SLT, AND, OR, XOR, SHIFT, JALR, BEQ, BLT, LOAD, STORE, MUL, DIVREM, ECALL, EBREAK)`. The vector is 'one-hot', meaning that in every row exactly one element is $1$; the others are $0$." +pad = 0 [[variables.multiplicity]] name = "μ" type = "BaseField" desc = "The multiplicity with which this instruction is looked up in the `CPU` table." - - - +pad = 0 diff --git a/spec/src/decode_uncompressed.toml b/spec/src/decode_uncompressed.toml new file mode 100644 index 000000000..c1084a964 --- /dev/null +++ b/spec/src/decode_uncompressed.toml @@ -0,0 +1,159 @@ +name = "DECODE" + +[[variables.output]] +name = "pc" +type = "DWordWL" +desc = "value of the program counter this instruction is associated with." + +[[variables.output]] +name = "rs1" +type = "Byte" +desc = "index of source register 1." + +[[variables.output]] +name = "rs2" +type = "Byte" +desc = "index of source register 2." + +[[variables.output]] +name = "rd" +type = "Byte" +desc = "index of destination register." + +[[variables.output]] +name = "write_register" +type = "Bit" +desc = "whether the result should be written to `rd` ($=0$ for memory write and when $#`rd` = #`x0`$." + +[[variables.output]] +name = "mem_2b" +type = "Bit" +desc = "whether the memory access (read or write) touches at least $2$ bytes." + +[[variables.output]] +name = "mem_4b" +type = "Bit" +desc = "whether the memory access (read or write) touches at least $4$ bytes." + +[[variables.output]] +name = "mem_8b" +type = "Bit" +desc = "whether the memory access (read or write) touches at least $8$ bytes." + +[[variables.output]] +name = "c_type" +type = "Bit" +desc = "Whether the instruction is of type `C`, i.e., whether it is $2$ bytes long instead of $4$." + +[[variables.output]] +name = "imm" +type = "DWordWL" +desc = "the *fully extended (!)* 64-bit version of the immediate." + +[[variables.output]] +name = "signed" +type = "Bit" +desc = "selector used to indicate signed or unsigned input interpretation. Currently, this is used to choose between ." + +[[variables.output]] +name = "mp_selector" +type = "Bit" +desc = """Multi-purpose selector used by different ALU operations for different purposes. Currently, it is used + - by the `MUL` chip to select between `MUL`/`MULH` and `MULH[S]U`, and + - as flag for inverting the condition of conditional branches (see `branch_cond`) + - as direction (left or right) for `SHIFT`""" + +[[variables.output]] +name = "muldiv_selector" +type = "Bit" +desc = "selects which output of `MUL` (lo/hi) or `DVRM` (quo/rem) is wanted." + +[[variables.output]] +name = "word_instr" +type = "Bit" +desc = "Whether the instruction is a `*W` instruction, requiring the inputs and outputs to be (sign) extended." + +[[variables.output]] +name = "ADD" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "SUB" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "SLT" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "AND" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "OR" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "XOR" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "SHIFT" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "JALR" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "BEQ" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "BLT" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "LOAD" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "STORE" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "MUL" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "DIVREM" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "ECALL" +type = "Bit" +desc = "ALU selector flag" + +[[variables.output]] +name = "EBREAK" +type = "Bit" +desc = "ALU selector flag" + +[[variables.multiplicity]] +name = "μ" +type = "BaseField" +desc = "The multiplicity with which this instruction is looked up in the `CPU` table." From c885c2c7d30a4f0abe920120f2bff0d6976ac92c Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 16 Jan 2026 15:49:06 +0100 Subject: [PATCH 06/14] spec: DECODE: overhaul decode --- spec/decode.typ | 10 +- spec/decode_uncompressed.typ | 254 ++++++++++++++++++------------ spec/src/decode_uncompressed.toml | 6 +- 3 files changed, 166 insertions(+), 104 deletions(-) diff --git a/spec/decode.typ b/spec/decode.typ index 5379b2e6b..346e269c5 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -16,15 +16,17 @@ #let decode = raw(chip.name) = #decode table -All `RV64IM` instruction are to be encoded in a format that can be interpreted by the VM. -This section outlines the decoding table in its compressed form, as it is being used in the VM. -Since reasoning about this compressed form is needlessly complex, the `decode (uncompressed)` section presents the same table in uncompressed form, and explains how a construct the table from `RV64IM` assembly instructions. +All `RV64ACIM` instruction are to be decoded to a format that can be interpreted by the VM. +This section outlines the decoding table being used in the VM. +For reasons of efficiency, data in this table is significantly compressed. +Since reasoning about this compressed form is needlessly complex, the `decode (uncompressed)` section presents the same table in uncompressed form, and explains how to decode `RV64IM` the assembly instructions to it. +Instructions on how to compress the uncompressed table to form the compressed decode table, can be derived from the `packed_decode` variable provided below. == Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) -The #decode chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +The #decode table is comprised of #nr_variables variables that are expressed using #nr_columns columns: #render_chip_column_table(chip, config) == Padding diff --git a/spec/decode_uncompressed.typ b/spec/decode_uncompressed.typ index ace63cdb4..31c2a6d21 100644 --- a/spec/decode_uncompressed.typ +++ b/spec/decode_uncompressed.typ @@ -15,111 +15,171 @@ #let decode = raw(chip.name) = #decode table (uncompressed) -This table is not used in practice: it is solely used to explain how one is to fill the (compressed) #decode table. +This section outlines how to decode `RV64IM` assembly to a VM-readable table. +Note that this table is not used in practice: it is solely used to explain how one is to fill the (compressed) #decode table. == Columns -For the purposes of this explanation, we decompress the `packed_decode` column into its constituent variables: +For the purposes of this explanation, we decompress the (uncompressed) #decode table's `packed_decode` variable into its constituent variables: #render_chip_column_table(chip, config) == Decoding -The following table illustrates how each instruction should be expressed in the decoding table. -For the purpose of brevity, some values are not explicitly specified. -Here, -+ the corresponding element of the instruction (in the case of `rs1`, `rs2`, `rd`), or -+ set to $0$ otherwise. - -// Subheader for the following table -#let subheader(title, common) = { - ( - table.header( - level: 2, - table.cell(colspan:2, [#emph(title)]), - if common != [] { - [_Common: #(common)_] - } else { - [] - } - ), - table.hline(stroke: .5pt) +The below table illustrates how each instruction should be expressed in the decoding table. +The columns of the table represent the following: +- *`operation`*: the assembly operation being encoded, +- *`op-flag`*: which of the "`ALU` selector flags" operation flags to set. Each operation sets exactly one. +- *`w_reg`*, *`w_inst`*, *`signed`*: whether to set the `write_register`, `word_inst` or `signed` flag, respectively, +- *other*: the other flags that should be set or variables that should be given specific values. + +For the purpose of brevity and readability, the table uses the following rules-of-thumb: +- `rd`, `rs1`, `rs2`, and `imm` are mapped to the values provided by the instruction. + When an instruction does not provide a value, it is set to $0$. +- When a flag's cell is empty / is not listed in `other`, it is set to $0$. +- $#`rd` eq.not 0$ indicates that $#`write_register` = 1$ when $#`rd` eq.not 0$ and $0$ otherwise. +- `[W]` indicates that $#`write_register` = 0$ for the `W`-variant of the operation, and $0$ for the non-`W`-variant. +- #sym.not`[U]` indicates that $#`signed` = 1$ for the *non-`U`*-variant of the operation, and $0$ for the `U`-variant. +- *The `c_type` flag is set independently of the below table.* (see next paragraph) + +Further clarification is provided in the notes following the table. + +=== C-type instructions +The `RV64C` extension for compressed instructions specifies that \~50% of all instructions can be represented using a 16-bit instruction (rather than 32-bits), saving \~25% in code size. +This execution of assembly code is _not_ agnostic to an instruction's compression state; after executing a compressed instruction, the `pc` should be incremented by $2$ rather than $4$. +To indicate an instruction is provided in compressed form, the `c_type` flag is introduced. +*This flag should be set to $1$ whenever the decoded instruction is provided in compressed form and $0$ otherwise.* + +/// Add a reference to one or more notes following this table. +#let ref_note(..refs) = { + super("[" + refs.pos().map(r => ref(r)).join(",") + "]") +} + +#let decoding_table(lines) = { + show figure: set block(breakable: true) + + figure(table( + columns: (auto, auto, 40pt, 40pt, 40pt, 1fr, 15pt), + stroke: 0pt, + inset: (right: .5em), + align: (left, right, center, center, center, left, right), + fill: (_, y) => + if calc.odd(y) and y <= lines.len() { luma(245) } + else { white }, + table.header([*Operation*], [*op-flag*], [*`w_reg`*], [*`w_instr`*], [*`signed`*], [*other*], []), + table.hline(stroke: 1.5pt), + table.vline(x: 1, start: 1, end: lines.len() + 1, stroke: .5pt), + ..lines.flatten(), + table.hline(stroke: 1.5pt), + table.footer([*Operation*], [*op-flag*], [*`w_reg`*], [*`w_instr`*], [*`signed`*], [*other*]), + ), + caption: [Decoding table] ) } -#table( - columns: (130pt, auto, auto), - stroke: 0pt, - inset: (right: 1em), - align: left + bottom, - table.header([*Operation*], [*Op-flag*], [*Other*]), - table.hline(stroke: 1.5pt), - - ..subheader("OP-IMM", [$#`rs2`:=0$, $#`write_register` := (#`rd` eq.not 0)$]), - [`ADDI[W] rd, rs1, imm`], [`ADD`], [$#`word_instr` := #`[W]`$], - [`SLTI[U] rd, rs1, imm`], [`SLT`], [$#`signed` := not#`[U]`$], - [`ANDI rd, rs1, imm`], [`AND`], [], - [`ORI rd, rs1, imm`], [`OR`], [], - [`XORI rd, rs1, imm`], [`XOR`], [], - [`SLLI[W] rd, rs1, imm`], [`SHIFT`], [$#`word_instr` := #`[W]`$], - [`SRLI[W] rd, rs1, imm`], [`SHIFT`], [$#`word_instr` := #`[W]`$, $#`mp_selector` := #`1`$], - [`SRAI[W] rd, rs1, imm`], [`SHIFT`], [$#`word_instr` := #`[W]`$, $#`mp_selector` := #`1`$, $#`signed` := #`1`$], - - ..subheader("LUI/AUIPC", []), - [`LUI rd, imm`], [#sym.arrow.double.r], [`ADDI rd, x0, imm`], - [`AUIPC rd, imm`], [#sym.arrow.double.r#footnote("The program counter (pc) is stored in register 255.")], [`ADDI rd, 255, imm`], - - ..subheader("OP", [$#`imm`:=0$, $#`write_register` := (#`rd` eq.not 0)$]), - [`ADD[W] rd, rs1, rs2`], [`ADD`], [$#`word_instr` := #`[W]`$], - [`SUB[W] rd, rs1, rs2`], [`SUB`], [$#`word_instr` := #`[W]`$], - [`SLT[U] rd, rs1, rs2`], [`SLT`], [$#`signed` := not#`[U]`$], - [`AND rd, rs1, rs2`], [`AND`], [], - [`OR rd, rs1, rs2`], [`OR`], [], - [`XOR rd, rs1, rs2`], [`XOR`], [], - [`SLL[W] rd, rs1, rs2`], [`SHIFT`], [$#`word_instr` := #`[W]`$], - [`SRL[W] rd, rs1, rs2`], [`SHIFT`], [$#`word_instr` := #`[W]`$, $#`mp_selector` := #`1`$], - [`SRA[W] rd, rs1, rs2`], [`SHIFT`], [$#`word_instr` := #`[W]`$, $#`mp_selector` := #`1`$, $#`signed` := #`1`$], - - ..subheader("BRANCHING (unconditional)", [$#`write_register` := #`rd` eq.not 0$]), - [`JAL rd, imm`], [#sym.arrow.double.r#footnote()], [`JALR rd, 255, imm`], - [`JALR rd, rs1, imm`], [`JALR`], [], - - ..subheader("BRANCHING (conditional)", [$#`rd` := 0$, $#`write_register` := 0$]), - [`BEQ rs1, rs2, imm`], [`BEQ`], [], - [`BNE rs1, rs2, imm`], [`BEQ`], [`mp_selector`], - [`BLT[U] rs1, rs2, imm`], [`BLT`], [$#`signed` := not#`[U]`$], - [`BGE[U] rs1, rs2, imm`], [`BLT`], [$#`signed` := not#`[U]`$, $#`mp_selector` := 1$], - - ..subheader("LOAD", [$#`rs2` := 0$]), - [`LD rd, rs1, imm`], [`LOAD`], [$#`mem_2b` := 1$, $#`mem_4b` := 1$, $#`mem_8b` := 1$], - [`LW[U] rd, rs1, imm`], [`LOAD`], [$#`signed` := not#`[U]`$, $#`mem_2b` := 1$, $#`mem_4b` := 1$], - [`LH[U] rd, rs1, imm`], [`LOAD`], [$#`signed` := not#`[U]`$, $#`mem_2b` := 1$], - [`LB[U] rd, rs1, imm`], [`LOAD`], [$#`signed` := not#`[U]`$], - - ..subheader("STORE", [$#`rd` := 0$]), - [`SD rs1, rs2, imm`], [`STORE`], [`mem_2b`, `mem_4b`, `mem_8b`], - [`SW rs1, rs2, imm`], [`STORE`], [`mem_2b`, `mem_4b`], - [`SH rs1, rs2, imm`], [`STORE`], [`mem_2b`], - [`SB rs1, rs2, imm`], [`STORE`], [], - - ..subheader("SYSTEM", []), - [`ECALL`], [`ECALL`], [`write_register`, $#`rs1` := #`x17`$, $#`rs2` := #`x11`$, $#`rd` := #`x10`$], - [`EBREAK`], [`EBREAK`], [], - - ..subheader("OP (M-extension)", [$#`imm` := 0$, $#`write_register` := #`rd` eq.not 0$]), - [`MUL[W] rd, rs1, rs2`], [`MUL`], [$#`word_instr` := #`[W]`$, `signed := 1`, `mp_selector`], - [`MULH rd, rs1, rs2`], [`MUL`], [`muldiv_selector`, `signed`, `mp_selector`], - [`MULHU rd, rs1, rs2`], [`MUL`], [`muldiv_selector`], - [`MULHSU rd, rs1, rs2`], [`MUL`], [`muldiv_selector`, `signed`], - [`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`word_instr` := #`[W]`$, $#`signed` := not#`[U]`$], - [`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`word_instr` := #`[W]`$, $#`signed` := not#`[U]`$, `muldiv_selector := 1`], - - ..subheader("MISC", []), - [`FENCE`], [#sym.arrow.double.r#footnote("Note: this is a no-op")], [`ADDI 0, x0, 0`], +#let decoding = ( + // OP-IMM + ([`ADDI[W] rd, rs1, imm`], [`ADD`], [$#`rd` eq.not 0$], [`[W]`], [], [], []), + ([`SLTI[U] rd, rs1, imm`], [`SLT`], [$#`rd` eq.not 0$], [], [#sym.not`[U]`], [], []), + ([`ANDI rd, rs1, imm`], [`AND`], [$#`rd` eq.not 0$], [], [], [], []), + ([`ORI rd, rs1, imm`], [`OR`], [$#`rd` eq.not 0$], [], [], [], []), + ([`XORI rd, rs1, imm`], [`XOR`], [$#`rd` eq.not 0$], [], [], [], []), + ([`SLLI[W] rd, rs1, imm`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [], []), + ([`SRLI[W] rd, rs1, imm`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [`mp_selector`], []), + ([`SRAI[W] rd, rs1, imm`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [1], [`mp_selector`], []), + // OP + ([`ADD[W] rd, rs1, rs2`], [`ADD`], [$#`rd` eq.not 0$], [`[W]`], [], [], []), + ([`SUB[W] rd, rs1, rs2`], [`SUB`], [$#`rd` eq.not 0$], [`[W]`], [], [], []), + ([`SLT[U] rd, rs1, rs2`], [`SLT`], [$#`rd` eq.not 0$], [], [#sym.not`[U]`], [], []), + ([`AND rd, rs1, rs2`], [`AND`], [$#`rd` eq.not 0$], [], [], [], []), + ([`OR rd, rs1, rs2`], [`OR`], [$#`rd` eq.not 0$], [], [], [], []), + ([`XOR rd, rs1, rs2`], [`XOR`], [$#`rd` eq.not 0$], [], [], [], []), + ([`SLL[W] rd, rs1, rs2`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [], []), + ([`SRL[W] rd, rs1, rs2`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [`mp_selector`], []), + ([`SRA[W] rd, rs1, rs2`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [1], [`mp_selector`], []), + // OP - M + ([`MUL[W] rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [`[W]`], [1], [`mp_selector`], []), + ([`MULH rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [], [1], [`mp_selector`, `muldiv_selector`], []), + ([`MULHU rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [], [], [`muldiv_selector`], []), + ([`MULHSU rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [], [1], [`muldiv_selector`], []), + ([`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`rd` eq.not 0$], [`[W]`], [#sym.not`[U]`], [], []), + ([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`rd` eq.not 0$], [`[W]`], [#sym.not`[U]`], [`muldiv_selector`], []), + // LUI/AUIPC + ([`LUI rd, imm`], [`ADDI`], [$#`rd` eq.not 0$], [], [], [], [#ref_note()]), + ([`AUIPC rd, imm`], [`ADDI`], [$#`rd` eq.not 0$], [], [], [`rs1 := x255`], [#ref_note()]), + ([`JAL rd, imm`], [`JALR`], [$#`rd` eq.not 0$], [], [], [`rs1 := x255`], [#ref_note()]), + // Branching + ([`JALR rd, rs1, imm`], [`JALR`], [$#`rd` eq.not 0$], [], [], [], []), + ([`BEQ rs1, rs2, imm`], [`BEQ`], [], [], [], [], []), + ([`BNE rs1, rs2, imm`], [`BEQ`], [], [], [], [`mp_selector`], []), + ([`BLT[U] rs1, rs2, imm`], [`BLT`], [], [], [#sym.not`[U]`], [], []), + ([`BGE[U] rs1, rs2, imm`], [`BLT`], [], [], [#sym.not`[U]`], [`mp_selector`], []), + // LOAD + ([`LD rd, rs1, imm`], [`LOAD`], [], [], [], [`mem_2B`, `mem_4B`, `mem_8B`], []), + ([`LW[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [`mem_2B`, `mem_4B`], []), + ([`LH[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [`mem_2B`], []), + ([`LB[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [], []), + // STORE + ([`SD rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_2B`, `mem_4B`, `mem_8B`], []), + ([`SW rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_2B`, `mem_4B`], []), + ([`SH rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_2B`], []), + ([`SB rs1, rs2, imm`], [`STORE`], [], [], [], [], []), + // ECALL/EBREAK + ([`ECALL`], [`ECALL`], [1], [], [], [$#`rs1` := #`x17`$, $#`rs2` := #`x11`$, $#`rd` := #`x10`$], [#ref_note()]), + ([`EBREAK`], [`EBREAK`], [], [], [], [], []), + // FENCE + ([`FENCE`], [`ADDI`], [], [], [], [], [#ref_note()]), ) + +#pagebreak() +#decoding_table(decoding) + +// Construct a note that can be referenced through `lbl` +#let referenceable_note(lbl, note) = { + show figure: (it) => align(left, [#it]) + [#figure(kind: "note", supplement: [], [#note]) #label(lbl)] +} + === Notes -- LUI/AUIPC: these operations load/add `imm` in/to the upper bits of `rd`/`pc`. As such, *we expect the decoding to take care of writing the immediate in the upper bits of `imm`*. -- ECALL: - "On RISC-V a system call has its own instruction: `ECALL`. A system call can have up to 7 arguments and has 1 return value. The arguments are in registers A0-A6, in that order, and the return value is written into A0 before giving back control to the guest. A7 contains the system call number." #link("https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[source]] - As such, - - syscall number in A7 (= register `x17`) - - first syscall argument in A1 (= register `x11`) - - syscall output in A0 (= register `x10`) +We note the following about the above decoding table: +#enum(numbering: "[1]", + enum.item( + referenceable_note( + "note-lui", + [`LUI`: this operation loads the 20-bit `imm` in the upper bits of `rd`. + Observe that this can be represented using `ADDI rd, x0, imm`. + As such, *we expect the decoding to take care of writing the immediate in bit range $[12:32]$ of `imm` and extending it to 64 bits.*] + ) + ), + enum.item( + referenceable_note( + "note-auipc", + [`AUIPC`: this operation adds the 20-bit immediate to the upper bits of `pc` and stores the result in `rd`. + Given that the `pc` is stored in `x255`, this operation can be represented using `ADDI rd, x255, imm`. + As such, *we expect the decoding to take care of writing the immediate in bit range $[12:32]$ of `imm` and extending it to 64 bits.*] + ) + ), + enum.item( + referenceable_note( + "note-jal", + [`JAL`: this operation stores `pc + 4` in `rd` and adds two times the sign-extended 20-bit immediate to the `pc`. + Note that this can be represented using `JALR rd, x255, imm`. + As such, *we expect the decoding to take care of writing the immediate in bit range $[1:13]$ of `imm` and extending it to 64 bits; the least significant bit should always be 0.*] + ) + ), + enum.item( + referenceable_note( + "note-ecall", + [`ECALL`: + "On RISC-V a system call has its own instruction: `ECALL`. A system call can have up to 7 arguments and has 1 return value. The arguments are in registers A0-A6, in that order, and the return value is written into A0 before giving back control to the guest. A7 contains the system call number." #link("https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[source]] + As such, + - syscall number in A7 (= register `x17`) + - first syscall argument in A1 (= register `x11`) + - syscall output in A0 (= register `x10`)] + ) + ), + enum.item( + referenceable_note( + "note-fence", + [`FENCE`: currently, the VM interprets this operation as `ADDI x0 x0 0`; a no-op.] + ) + ) +) diff --git a/spec/src/decode_uncompressed.toml b/spec/src/decode_uncompressed.toml index c1084a964..ac6418568 100644 --- a/spec/src/decode_uncompressed.toml +++ b/spec/src/decode_uncompressed.toml @@ -26,17 +26,17 @@ type = "Bit" desc = "whether the result should be written to `rd` ($=0$ for memory write and when $#`rd` = #`x0`$." [[variables.output]] -name = "mem_2b" +name = "mem_2B" type = "Bit" desc = "whether the memory access (read or write) touches at least $2$ bytes." [[variables.output]] -name = "mem_4b" +name = "mem_4B" type = "Bit" desc = "whether the memory access (read or write) touches at least $4$ bytes." [[variables.output]] -name = "mem_8b" +name = "mem_8B" type = "Bit" desc = "whether the memory access (read or write) touches at least $8$ bytes." From 21487ec4bc317cb6920630e9793bedb32d09e0df Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Tue, 20 Jan 2026 09:59:17 +0100 Subject: [PATCH 07/14] Apply suggestions from code review Co-authored-by: Robin Jadoul --- spec/decode.typ | 2 +- spec/src/decode_uncompressed.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/decode.typ b/spec/decode.typ index 346e269c5..248adb5f5 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -19,7 +19,7 @@ All `RV64ACIM` instruction are to be decoded to a format that can be interpreted by the VM. This section outlines the decoding table being used in the VM. For reasons of efficiency, data in this table is significantly compressed. -Since reasoning about this compressed form is needlessly complex, the `decode (uncompressed)` section presents the same table in uncompressed form, and explains how to decode `RV64IM` the assembly instructions to it. +Since reasoning about this compressed form is needlessly complex, the `decode (uncompressed)` section presents the same table in uncompressed form, and explains how to decode `RV64IM` assembly instructions to it. Instructions on how to compress the uncompressed table to form the compressed decode table, can be derived from the `packed_decode` variable provided below. == Columns diff --git a/spec/src/decode_uncompressed.toml b/spec/src/decode_uncompressed.toml index ac6418568..ee76f6c18 100644 --- a/spec/src/decode_uncompressed.toml +++ b/spec/src/decode_uncompressed.toml @@ -53,7 +53,7 @@ desc = "the *fully extended (!)* 64-bit version of the immediate." [[variables.output]] name = "signed" type = "Bit" -desc = "selector used to indicate signed or unsigned input interpretation. Currently, this is used to choose between ." +desc = "selector used to indicate signed or unsigned input interpretation." [[variables.output]] name = "mp_selector" From 02b2494ad6e91081e0153cc3ea7f902dbae7f3c2 Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Tue, 20 Jan 2026 11:27:21 +0100 Subject: [PATCH 08/14] Apply suggestion from @RobinJadoul Co-authored-by: Robin Jadoul --- spec/decode_uncompressed.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/decode_uncompressed.typ b/spec/decode_uncompressed.typ index 31c2a6d21..1f6c49c86 100644 --- a/spec/decode_uncompressed.typ +++ b/spec/decode_uncompressed.typ @@ -27,7 +27,7 @@ The below table illustrates how each instruction should be expressed in the deco The columns of the table represent the following: - *`operation`*: the assembly operation being encoded, - *`op-flag`*: which of the "`ALU` selector flags" operation flags to set. Each operation sets exactly one. -- *`w_reg`*, *`w_inst`*, *`signed`*: whether to set the `write_register`, `word_inst` or `signed` flag, respectively, +- *`w_reg`*, *`w_instr`*, *`signed`*: whether to set the `write_register`, `word_instr` or `signed` flag, respectively, - *other*: the other flags that should be set or variables that should be given specific values. For the purpose of brevity and readability, the table uses the following rules-of-thumb: From da3e9db969e51b5706f1f1255a49e200f614636b Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Tue, 20 Jan 2026 11:28:36 +0100 Subject: [PATCH 09/14] Fix `ADDI` flag mistakes --- spec/decode_uncompressed.typ | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/spec/decode_uncompressed.typ b/spec/decode_uncompressed.typ index 1f6c49c86..a5e1f67fc 100644 --- a/spec/decode_uncompressed.typ +++ b/spec/decode_uncompressed.typ @@ -102,8 +102,8 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is ([`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`rd` eq.not 0$], [`[W]`], [#sym.not`[U]`], [], []), ([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`rd` eq.not 0$], [`[W]`], [#sym.not`[U]`], [`muldiv_selector`], []), // LUI/AUIPC - ([`LUI rd, imm`], [`ADDI`], [$#`rd` eq.not 0$], [], [], [], [#ref_note()]), - ([`AUIPC rd, imm`], [`ADDI`], [$#`rd` eq.not 0$], [], [], [`rs1 := x255`], [#ref_note()]), + ([`LUI rd, imm`], [`ADD`], [$#`rd` eq.not 0$], [], [], [], [#ref_note()]), + ([`AUIPC rd, imm`], [`ADD`], [$#`rd` eq.not 0$], [], [], [`rs1 := x255`], [#ref_note()]), ([`JAL rd, imm`], [`JALR`], [$#`rd` eq.not 0$], [], [], [`rs1 := x255`], [#ref_note()]), // Branching ([`JALR rd, rs1, imm`], [`JALR`], [$#`rd` eq.not 0$], [], [], [], []), @@ -125,7 +125,7 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is ([`ECALL`], [`ECALL`], [1], [], [], [$#`rs1` := #`x17`$, $#`rs2` := #`x11`$, $#`rd` := #`x10`$], [#ref_note()]), ([`EBREAK`], [`EBREAK`], [], [], [], [], []), // FENCE - ([`FENCE`], [`ADDI`], [], [], [], [], [#ref_note()]), + ([`FENCE`], [`ADD`], [], [], [], [], [#ref_note()]), ) From 72ea1d50ebf0a908e7c071b85a6ca0200b512ef6 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 20 Jan 2026 13:25:39 +0100 Subject: [PATCH 10/14] spec: DECODE: make `packed_encode` a `BaseField`; remove superfluous `B49` --- spec/src/config.toml | 5 ----- spec/src/decode.toml | 5 +++-- 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/spec/src/config.toml b/spec/src/config.toml index bbdb0d548..68f1683de 100644 --- a/spec/src/config.toml +++ b/spec/src/config.toml @@ -58,11 +58,6 @@ label = "B35" subtypes = ["BaseField"] desc = "Variable that can only assume values in the range $[0, 2^35)$." -[[variables.types]] -label = "B49" -subtypes = ["BaseField"] -desc = "Variable that can only assume values in the range $[0, 2^49)$." - [[variables.types]] label = "B51" subtypes = ["BaseField"] diff --git a/spec/src/decode.toml b/spec/src/decode.toml index 53134404d..3663625c5 100644 --- a/spec/src/decode.toml +++ b/spec/src/decode.toml @@ -8,7 +8,7 @@ pad = 0 [[variables.output]] name = "packed_decode" -type = "B49" +type = "BaseField" desc = """Ordered concatenation of several small variables. The `decode (uncompressed)` section explains the purpose of each variable.\\ A list of each variable and the bit(-range) in which it is located:\\ @@ -39,7 +39,8 @@ A list of each variable and the bit(-range) in which it is located:\\ [45] `MUL`, \\ [46] `DIVREM`, \\ [47] `ECALL`, \\ -[48] `EBREAK`. \\ +[48] `EBREAK`; \\ +the remaining bits are set to zero. """ pad = 0 From 4555407966018f71794488ccb67499aa2f7e4ff3 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 20 Jan 2026 13:28:28 +0100 Subject: [PATCH 11/14] spec: DECODE: set `mem_xB` when reading/writing _exactly_ `x` bytes --- spec/decode_uncompressed.typ | 8 ++++---- spec/src/decode_uncompressed.toml | 6 +++--- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/spec/decode_uncompressed.typ b/spec/decode_uncompressed.typ index a5e1f67fc..1d9c80d92 100644 --- a/spec/decode_uncompressed.typ +++ b/spec/decode_uncompressed.typ @@ -112,13 +112,13 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is ([`BLT[U] rs1, rs2, imm`], [`BLT`], [], [], [#sym.not`[U]`], [], []), ([`BGE[U] rs1, rs2, imm`], [`BLT`], [], [], [#sym.not`[U]`], [`mp_selector`], []), // LOAD - ([`LD rd, rs1, imm`], [`LOAD`], [], [], [], [`mem_2B`, `mem_4B`, `mem_8B`], []), - ([`LW[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [`mem_2B`, `mem_4B`], []), + ([`LD rd, rs1, imm`], [`LOAD`], [], [], [], [`mem_8B`], []), + ([`LW[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [`mem_4B`], []), ([`LH[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [`mem_2B`], []), ([`LB[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [], []), // STORE - ([`SD rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_2B`, `mem_4B`, `mem_8B`], []), - ([`SW rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_2B`, `mem_4B`], []), + ([`SD rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_8B`], []), + ([`SW rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_4B`], []), ([`SH rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_2B`], []), ([`SB rs1, rs2, imm`], [`STORE`], [], [], [], [], []), // ECALL/EBREAK diff --git a/spec/src/decode_uncompressed.toml b/spec/src/decode_uncompressed.toml index ee76f6c18..8cd296425 100644 --- a/spec/src/decode_uncompressed.toml +++ b/spec/src/decode_uncompressed.toml @@ -28,17 +28,17 @@ desc = "whether the result should be written to `rd` ($=0$ for memory write and [[variables.output]] name = "mem_2B" type = "Bit" -desc = "whether the memory access (read or write) touches at least $2$ bytes." +desc = "whether the memory access (read or write) touches exactly $2$ bytes." [[variables.output]] name = "mem_4B" type = "Bit" -desc = "whether the memory access (read or write) touches at least $4$ bytes." +desc = "whether the memory access (read or write) touches exactly $4$ bytes." [[variables.output]] name = "mem_8B" type = "Bit" -desc = "whether the memory access (read or write) touches at least $8$ bytes." +desc = "whether the memory access (read or write) touches exactly $8$ bytes." [[variables.output]] name = "c_type" From 32932604e619b2fa3d949182b6314661c70a6585 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 20 Jan 2026 13:30:37 +0100 Subject: [PATCH 12/14] spec: DECODE: update `mp_selector` description. --- spec/src/decode_uncompressed.toml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/spec/src/decode_uncompressed.toml b/spec/src/decode_uncompressed.toml index 8cd296425..8457005f8 100644 --- a/spec/src/decode_uncompressed.toml +++ b/spec/src/decode_uncompressed.toml @@ -58,10 +58,8 @@ desc = "selector used to indicate signed or unsigned input interpretation." [[variables.output]] name = "mp_selector" type = "Bit" -desc = """Multi-purpose selector used by different ALU operations for different purposes. Currently, it is used - - by the `MUL` chip to select between `MUL`/`MULH` and `MULH[S]U`, and - - as flag for inverting the condition of conditional branches (see `branch_cond`) - - as direction (left or right) for `SHIFT`""" +desc = """Multi-purpose selector used by the CPU to to configure several ALU operations in different ways. + See the `CPU` chip for more details.""" [[variables.output]] name = "muldiv_selector" From c93e28949f4120ec43776c08ebbaa050cbeb4562 Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Tue, 20 Jan 2026 13:31:42 +0100 Subject: [PATCH 13/14] Apply suggestions from code review --- spec/decode.typ | 2 +- spec/src/decode.toml | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/spec/decode.typ b/spec/decode.typ index 248adb5f5..bbbbfd69f 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -16,7 +16,7 @@ #let decode = raw(chip.name) = #decode table -All `RV64ACIM` instruction are to be decoded to a format that can be interpreted by the VM. +All `RV64IMC` instruction are to be decoded to a format that can be interpreted by the VM. This section outlines the decoding table being used in the VM. For reasons of efficiency, data in this table is significantly compressed. Since reasoning about this compressed form is needlessly complex, the `decode (uncompressed)` section presents the same table in uncompressed form, and explains how to decode `RV64IM` assembly instructions to it. diff --git a/spec/src/decode.toml b/spec/src/decode.toml index 3663625c5..6c01e4f6c 100644 --- a/spec/src/decode.toml +++ b/spec/src/decode.toml @@ -4,7 +4,8 @@ name = "DECODE" name = "pc" type = "DWordWL" desc = "value of the program counter this instruction is associated with." -pad = 0 +# TODO(#136): fix this when padding the CPU +pad = 1 [[variables.output]] name = "packed_decode" From 2c30f4c13cce217f6b23c06d263ecafe27a104c3 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 20 Jan 2026 13:54:06 +0100 Subject: [PATCH 14/14] spec: DECODE: merge uncompressed page into decode.typ --- spec/book.typ | 1 - spec/decode.typ | 184 ++++++++++++++++++++++++++++++++++ spec/decode_uncompressed.typ | 185 ----------------------------------- 3 files changed, 184 insertions(+), 186 deletions(-) delete mode 100644 spec/decode_uncompressed.typ diff --git a/spec/book.typ b/spec/book.typ index c65ff2e1b..935c8f777 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -9,7 +9,6 @@ #chapter("is_bit.typ")[IS_BIT template] #chapter("add.typ")[ADD template] #chapter("decode.typ")[DECODE chip] - #chapter("decode_uncompressed.typ")[DECODE (uncompressed) chip] #chapter("cpu.typ")[CPU chip] #chapter("shift.typ")[SHIFT chip] #chapter("branch.typ")[BRANCH] diff --git a/spec/decode.typ b/spec/decode.typ index bbbbfd69f..24846d2c1 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -33,3 +33,187 @@ The #decode table is comprised of #nr_variables variables that are expressed usi The #decode table must be padded to a length that is a power of two. Empty rows with the following content can be added to achieve this: #render_chip_padding_table(chip, config) + + +== Decoding +For the purposes of explaining decoding, we decompress #decode's `packed_decode` variable into its constituent variables. +Note that the below table is _not_ used in practice: it is solely used for the purposes of this explanation. + +#let config = load_config() +#let uncompressed_chip = load_chip("src/decode_uncompressed.toml", config) + +#render_chip_column_table(uncompressed_chip, config) + +We will illustrate how each instruction should be expressed in this (uncompressed) decoding table. +The columns of the accompanying table represent the following: +- *`operation`*: the assembly operation being encoded, +- *`op-flag`*: which of the "`ALU` selector flags" operation flags to set. Each operation sets exactly one. +- *`w_reg`*, *`w_instr`*, *`signed`*: whether to set the `write_register`, `word_instr` or `signed` flag, respectively, +- *other*: the other flags that should be set or variables that should be given specific values. + +For the purpose of brevity and readability, the table uses the following rules-of-thumb: ++ `rd`, `rs1`, `rs2`, and `imm` are mapped to the values provided by the instruction; + when a value is not specified by an instruction it defaults to $0$. ++ Any flag that is not listed is set to $0$, with the exception of the `c_type` flag. + *The `c_type` flag is set independently of the below table*, as explained below. + +Further clarification is provided in the notes following the table. + +=== C-type instructions +The `RV64C` extension for compressed instructions specifies that \~50% of all instructions can be represented using a 16-bit instruction (rather than 32-bits), saving \~25% in code size. +This execution of assembly code is _not_ agnostic to an instruction's compression state; after executing a compressed instruction, the `pc` should be incremented by $2$ rather than $4$. +To indicate an instruction is provided in compressed form, the `c_type` flag is introduced. +*This flag should be set to $1$ whenever the decoded instruction is provided in compressed form and $0$ otherwise.* + +/// Add a reference to one or more notes following this table. +#let ref_note(..refs) = { + super("[" + refs.pos().map(r => ref(r)).join(",") + "]") +} + +#let decoding_table(lines) = { + show figure: set block(breakable: true) + + figure(table( + columns: (auto, auto, 40pt, 40pt, 40pt, 1fr, 15pt), + stroke: 0pt, + inset: (right: .5em), + align: (left, right, center, center, center, left, right), + fill: (_, y) => + if calc.odd(y) and y <= lines.len() { luma(245) } + else { white }, + table.header([*Operation*], [*op-flag*], [*`w_reg`*], [*`w_instr`*], [*`signed`*], [*other*], []), + table.hline(stroke: 1.5pt), + table.vline(x: 1, start: 1, end: lines.len() + 1, stroke: .5pt), + ..lines.flatten(), + table.hline(stroke: 1.5pt), + table.footer([*Operation*], [*op-flag*], [*`w_reg`*], [*`w_instr`*], [*`signed`*], [*other*]), + ), + caption: [Decoding table] + ) +} + +#let decoding = ( + // OP-IMM + ([`ADDI[W] rd, rs1, imm`], [`ADD`], [$#`rd` eq.not 0$], [`[W]`], [], [], [#ref_note(, )]), + ([`SLTI[U] rd, rs1, imm`], [`SLT`], [$#`rd` eq.not 0$], [], [#sym.not`[U]`], [], [#ref_note(, )]), + ([`ANDI rd, rs1, imm`], [`AND`], [$#`rd` eq.not 0$], [], [], [], [#ref_note()]), + ([`ORI rd, rs1, imm`], [`OR`], [$#`rd` eq.not 0$], [], [], [], [#ref_note()]), + ([`XORI rd, rs1, imm`], [`XOR`], [$#`rd` eq.not 0$], [], [], [], [#ref_note()]), + ([`SLLI[W] rd, rs1, imm`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [], [#ref_note()]), + ([`SRLI[W] rd, rs1, imm`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [`mp_selector`], [#ref_note(, )]), + ([`SRAI[W] rd, rs1, imm`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [1], [`mp_selector`], [#ref_note(, )]), + // OP + ([`ADD[W] rd, rs1, rs2`], [`ADD`], [$#`rd` eq.not 0$], [`[W]`], [], [], [#ref_note(, )]), + ([`SUB[W] rd, rs1, rs2`], [`SUB`], [$#`rd` eq.not 0$], [`[W]`], [], [], [#ref_note(, )]), + ([`SLT[U] rd, rs1, rs2`], [`SLT`], [$#`rd` eq.not 0$], [], [#sym.not`[U]`], [], [#ref_note(, )]), + ([`AND rd, rs1, rs2`], [`AND`], [$#`rd` eq.not 0$], [], [], [], [#ref_note()]), + ([`OR rd, rs1, rs2`], [`OR`], [$#`rd` eq.not 0$], [], [], [], [#ref_note()]), + ([`XOR rd, rs1, rs2`], [`XOR`], [$#`rd` eq.not 0$], [], [], [], [#ref_note()]), + ([`SLL[W] rd, rs1, rs2`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [], [#ref_note(, )]), + ([`SRL[W] rd, rs1, rs2`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [`mp_selector`], [#ref_note(, )]), + ([`SRA[W] rd, rs1, rs2`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [1], [`mp_selector`], [#ref_note(, )]), + // OP - M + ([`MUL[W] rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [`[W]`], [1], [`mp_selector`], [#ref_note(, )]), + ([`MULH rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [], [1], [`mp_selector`, `muldiv_selector`], [#ref_note()]), + ([`MULHU rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [], [], [`muldiv_selector`], [#ref_note()]), + ([`MULHSU rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [], [1], [`muldiv_selector`], [#ref_note()]), + ([`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`rd` eq.not 0$], [`[W]`], [#sym.not`[U]`], [], [#ref_note(, , )]), + ([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`rd` eq.not 0$], [`[W]`], [#sym.not`[U]`], [`muldiv_selector`], [#ref_note(, , )]), + // LUI/AUIPC + ([`LUI rd, imm`], [`ADD`], [$#`rd` eq.not 0$], [], [], [], [#ref_note(, )]), + ([`AUIPC rd, imm`], [`ADD`], [$#`rd` eq.not 0$], [], [], [`rs1 := x255`], [#ref_note(, )]), + ([`JAL rd, imm`], [`JALR`], [$#`rd` eq.not 0$], [], [], [`rs1 := x255`], [#ref_note(, )]), + // Branching + ([`JALR rd, rs1, imm`], [`JALR`], [$#`rd` eq.not 0$], [], [], [], [#ref_note()]), + ([`BEQ rs1, rs2, imm`], [`BEQ`], [], [], [], [], []), + ([`BNE rs1, rs2, imm`], [`BEQ`], [], [], [], [`mp_selector`], []), + ([`BLT[U] rs1, rs2, imm`], [`BLT`], [], [], [#sym.not`[U]`], [], [#ref_note()]), + ([`BGE[U] rs1, rs2, imm`], [`BLT`], [], [], [#sym.not`[U]`], [`mp_selector`], [#ref_note()]), + // LOAD + ([`LD rd, rs1, imm`], [`LOAD`], [], [], [], [`mem_8B`], []), + ([`LW[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [`mem_4B`], [#ref_note()]), + ([`LH[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [`mem_2B`], [#ref_note()]), + ([`LB[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [], [#ref_note()]), + // STORE + ([`SD rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_8B`], []), + ([`SW rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_4B`], []), + ([`SH rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_2B`], []), + ([`SB rs1, rs2, imm`], [`STORE`], [], [], [], [], []), + // ECALL/EBREAK + ([`ECALL`], [`ECALL`], [1], [], [], [$#`rs1` := #`x17`$, $#`rs2` := #`x11`$, $#`rd` := #`x10`$], [#ref_note()]), + ([`EBREAK`], [`EBREAK`], [], [], [], [], []), + // FENCE + ([`FENCE`], [`ADD`], [], [], [], [], [#ref_note()]), +) + +#decoding_table(decoding) + +// Construct a note that can be referenced through `lbl` +#let referenceable_note(lbl, note) = { + show figure: (it) => align(left, [#it]) + [#figure(kind: "note", supplement: [], [#note]) #label(lbl)] +} + +==== Notes +We note the following about the above decoding table: +#enum(numbering: "[1]", + enum.item( + referenceable_note( + "note_w_reg", + [`write_register`: $#`rd` eq.not 0$ indicates that $#`write_register` = 1$ when $#`rd` eq.not 0$ and $0$ otherwise.] + ) + ), + enum.item( + referenceable_note( + "note_word_instr", + [`word_instr`: `[W]` indicates that $#`word_instr` = 0$ for the `W`-variant of the operation, and $0$ for the non-`W`-variant.] + ) + ), + enum.item( + referenceable_note( + "note_signed", + [`signed`: #sym.not`[U]` indicates that $#`signed` = 1$ for the *non-`U`*-variant of the operation, and $0$ for the `U`-variant.] + ) + ), + enum.item( + referenceable_note( + "note-lui", + [`LUI`: this operation loads the 20-bit `imm` in the upper bits of `rd`. + Observe that this can be represented using `ADDI rd, x0, imm`. + As such, *we expect the decoding to take care of writing the immediate in bit range $[12:32]$ of `imm` and extending it to 64 bits.*] + ) + ), + enum.item( + referenceable_note( + "note-auipc", + [`AUIPC`: this operation adds the 20-bit immediate to the upper bits of `pc` and stores the result in `rd`. + Given that the `pc` is stored in `x255`, this operation can be represented using `ADDI rd, x255, imm`. + As such, *we expect the decoding to take care of writing the immediate in bit range $[12:32]$ of `imm` and extending it to 64 bits.*] + ) + ), + enum.item( + referenceable_note( + "note-jal", + [`JAL`: this operation stores `pc + 4` in `rd` and adds two times the sign-extended 20-bit immediate to the `pc`. + Note that this can be represented using `JALR rd, x255, imm`. + As such, *we expect the decoding to take care of writing the immediate in bit range $[1:13]$ of `imm` and extending it to 64 bits; the least significant bit should always be 0.*] + ) + ), + enum.item( + referenceable_note( + "note-ecall", + [`ECALL`: + "On RISC-V a system call has its own instruction: `ECALL`. A system call can have up to 7 arguments and has 1 return value. The arguments are in registers A0-A6, in that order, and the return value is written into A0 before giving back control to the guest. A7 contains the system call number." #link("https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[source]] + As such, + - syscall number in A7 (= register `x17`) + - first syscall argument in A1 (= register `x11`) + - syscall output in A0 (= register `x10`)] + ) + ), + enum.item( + referenceable_note( + "note-fence", + [`FENCE`: currently, the VM interprets this operation as `ADDI x0 x0 0`; a no-op.] + ) + ) +) diff --git a/spec/decode_uncompressed.typ b/spec/decode_uncompressed.typ deleted file mode 100644 index 1d9c80d92..000000000 --- a/spec/decode_uncompressed.typ +++ /dev/null @@ -1,185 +0,0 @@ -#import "/book.typ": book-page, rj -#import "/src.typ": load_config, load_chip -#import "/chip.typ": ( - render_chip_assumptions, - render_chip_column_table, - total_nr_variables, - total_nr_instantiated_columns, - render_constraint_table, -) - -#let config = load_config() -#let chip = load_chip("src/decode_uncompressed.toml", config) -#show: book-page.with(title: "DECODE chip") - -#let decode = raw(chip.name) - -= #decode table (uncompressed) -This section outlines how to decode `RV64IM` assembly to a VM-readable table. -Note that this table is not used in practice: it is solely used to explain how one is to fill the (compressed) #decode table. - -== Columns -For the purposes of this explanation, we decompress the (uncompressed) #decode table's `packed_decode` variable into its constituent variables: -#render_chip_column_table(chip, config) - -== Decoding -The below table illustrates how each instruction should be expressed in the decoding table. -The columns of the table represent the following: -- *`operation`*: the assembly operation being encoded, -- *`op-flag`*: which of the "`ALU` selector flags" operation flags to set. Each operation sets exactly one. -- *`w_reg`*, *`w_instr`*, *`signed`*: whether to set the `write_register`, `word_instr` or `signed` flag, respectively, -- *other*: the other flags that should be set or variables that should be given specific values. - -For the purpose of brevity and readability, the table uses the following rules-of-thumb: -- `rd`, `rs1`, `rs2`, and `imm` are mapped to the values provided by the instruction. - When an instruction does not provide a value, it is set to $0$. -- When a flag's cell is empty / is not listed in `other`, it is set to $0$. -- $#`rd` eq.not 0$ indicates that $#`write_register` = 1$ when $#`rd` eq.not 0$ and $0$ otherwise. -- `[W]` indicates that $#`write_register` = 0$ for the `W`-variant of the operation, and $0$ for the non-`W`-variant. -- #sym.not`[U]` indicates that $#`signed` = 1$ for the *non-`U`*-variant of the operation, and $0$ for the `U`-variant. -- *The `c_type` flag is set independently of the below table.* (see next paragraph) - -Further clarification is provided in the notes following the table. - -=== C-type instructions -The `RV64C` extension for compressed instructions specifies that \~50% of all instructions can be represented using a 16-bit instruction (rather than 32-bits), saving \~25% in code size. -This execution of assembly code is _not_ agnostic to an instruction's compression state; after executing a compressed instruction, the `pc` should be incremented by $2$ rather than $4$. -To indicate an instruction is provided in compressed form, the `c_type` flag is introduced. -*This flag should be set to $1$ whenever the decoded instruction is provided in compressed form and $0$ otherwise.* - -/// Add a reference to one or more notes following this table. -#let ref_note(..refs) = { - super("[" + refs.pos().map(r => ref(r)).join(",") + "]") -} - -#let decoding_table(lines) = { - show figure: set block(breakable: true) - - figure(table( - columns: (auto, auto, 40pt, 40pt, 40pt, 1fr, 15pt), - stroke: 0pt, - inset: (right: .5em), - align: (left, right, center, center, center, left, right), - fill: (_, y) => - if calc.odd(y) and y <= lines.len() { luma(245) } - else { white }, - table.header([*Operation*], [*op-flag*], [*`w_reg`*], [*`w_instr`*], [*`signed`*], [*other*], []), - table.hline(stroke: 1.5pt), - table.vline(x: 1, start: 1, end: lines.len() + 1, stroke: .5pt), - ..lines.flatten(), - table.hline(stroke: 1.5pt), - table.footer([*Operation*], [*op-flag*], [*`w_reg`*], [*`w_instr`*], [*`signed`*], [*other*]), - ), - caption: [Decoding table] - ) -} - -#let decoding = ( - // OP-IMM - ([`ADDI[W] rd, rs1, imm`], [`ADD`], [$#`rd` eq.not 0$], [`[W]`], [], [], []), - ([`SLTI[U] rd, rs1, imm`], [`SLT`], [$#`rd` eq.not 0$], [], [#sym.not`[U]`], [], []), - ([`ANDI rd, rs1, imm`], [`AND`], [$#`rd` eq.not 0$], [], [], [], []), - ([`ORI rd, rs1, imm`], [`OR`], [$#`rd` eq.not 0$], [], [], [], []), - ([`XORI rd, rs1, imm`], [`XOR`], [$#`rd` eq.not 0$], [], [], [], []), - ([`SLLI[W] rd, rs1, imm`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [], []), - ([`SRLI[W] rd, rs1, imm`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [`mp_selector`], []), - ([`SRAI[W] rd, rs1, imm`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [1], [`mp_selector`], []), - // OP - ([`ADD[W] rd, rs1, rs2`], [`ADD`], [$#`rd` eq.not 0$], [`[W]`], [], [], []), - ([`SUB[W] rd, rs1, rs2`], [`SUB`], [$#`rd` eq.not 0$], [`[W]`], [], [], []), - ([`SLT[U] rd, rs1, rs2`], [`SLT`], [$#`rd` eq.not 0$], [], [#sym.not`[U]`], [], []), - ([`AND rd, rs1, rs2`], [`AND`], [$#`rd` eq.not 0$], [], [], [], []), - ([`OR rd, rs1, rs2`], [`OR`], [$#`rd` eq.not 0$], [], [], [], []), - ([`XOR rd, rs1, rs2`], [`XOR`], [$#`rd` eq.not 0$], [], [], [], []), - ([`SLL[W] rd, rs1, rs2`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [], []), - ([`SRL[W] rd, rs1, rs2`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [`mp_selector`], []), - ([`SRA[W] rd, rs1, rs2`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [1], [`mp_selector`], []), - // OP - M - ([`MUL[W] rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [`[W]`], [1], [`mp_selector`], []), - ([`MULH rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [], [1], [`mp_selector`, `muldiv_selector`], []), - ([`MULHU rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [], [], [`muldiv_selector`], []), - ([`MULHSU rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [], [1], [`muldiv_selector`], []), - ([`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`rd` eq.not 0$], [`[W]`], [#sym.not`[U]`], [], []), - ([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`rd` eq.not 0$], [`[W]`], [#sym.not`[U]`], [`muldiv_selector`], []), - // LUI/AUIPC - ([`LUI rd, imm`], [`ADD`], [$#`rd` eq.not 0$], [], [], [], [#ref_note()]), - ([`AUIPC rd, imm`], [`ADD`], [$#`rd` eq.not 0$], [], [], [`rs1 := x255`], [#ref_note()]), - ([`JAL rd, imm`], [`JALR`], [$#`rd` eq.not 0$], [], [], [`rs1 := x255`], [#ref_note()]), - // Branching - ([`JALR rd, rs1, imm`], [`JALR`], [$#`rd` eq.not 0$], [], [], [], []), - ([`BEQ rs1, rs2, imm`], [`BEQ`], [], [], [], [], []), - ([`BNE rs1, rs2, imm`], [`BEQ`], [], [], [], [`mp_selector`], []), - ([`BLT[U] rs1, rs2, imm`], [`BLT`], [], [], [#sym.not`[U]`], [], []), - ([`BGE[U] rs1, rs2, imm`], [`BLT`], [], [], [#sym.not`[U]`], [`mp_selector`], []), - // LOAD - ([`LD rd, rs1, imm`], [`LOAD`], [], [], [], [`mem_8B`], []), - ([`LW[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [`mem_4B`], []), - ([`LH[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [`mem_2B`], []), - ([`LB[U] rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [], []), - // STORE - ([`SD rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_8B`], []), - ([`SW rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_4B`], []), - ([`SH rs1, rs2, imm`], [`STORE`], [], [], [], [`mem_2B`], []), - ([`SB rs1, rs2, imm`], [`STORE`], [], [], [], [], []), - // ECALL/EBREAK - ([`ECALL`], [`ECALL`], [1], [], [], [$#`rs1` := #`x17`$, $#`rs2` := #`x11`$, $#`rd` := #`x10`$], [#ref_note()]), - ([`EBREAK`], [`EBREAK`], [], [], [], [], []), - // FENCE - ([`FENCE`], [`ADD`], [], [], [], [], [#ref_note()]), -) - - -#pagebreak() -#decoding_table(decoding) - -// Construct a note that can be referenced through `lbl` -#let referenceable_note(lbl, note) = { - show figure: (it) => align(left, [#it]) - [#figure(kind: "note", supplement: [], [#note]) #label(lbl)] -} - -=== Notes -We note the following about the above decoding table: -#enum(numbering: "[1]", - enum.item( - referenceable_note( - "note-lui", - [`LUI`: this operation loads the 20-bit `imm` in the upper bits of `rd`. - Observe that this can be represented using `ADDI rd, x0, imm`. - As such, *we expect the decoding to take care of writing the immediate in bit range $[12:32]$ of `imm` and extending it to 64 bits.*] - ) - ), - enum.item( - referenceable_note( - "note-auipc", - [`AUIPC`: this operation adds the 20-bit immediate to the upper bits of `pc` and stores the result in `rd`. - Given that the `pc` is stored in `x255`, this operation can be represented using `ADDI rd, x255, imm`. - As such, *we expect the decoding to take care of writing the immediate in bit range $[12:32]$ of `imm` and extending it to 64 bits.*] - ) - ), - enum.item( - referenceable_note( - "note-jal", - [`JAL`: this operation stores `pc + 4` in `rd` and adds two times the sign-extended 20-bit immediate to the `pc`. - Note that this can be represented using `JALR rd, x255, imm`. - As such, *we expect the decoding to take care of writing the immediate in bit range $[1:13]$ of `imm` and extending it to 64 bits; the least significant bit should always be 0.*] - ) - ), - enum.item( - referenceable_note( - "note-ecall", - [`ECALL`: - "On RISC-V a system call has its own instruction: `ECALL`. A system call can have up to 7 arguments and has 1 return value. The arguments are in registers A0-A6, in that order, and the return value is written into A0 before giving back control to the guest. A7 contains the system call number." #link("https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[source]] - As such, - - syscall number in A7 (= register `x17`) - - first syscall argument in A1 (= register `x11`) - - syscall output in A0 (= register `x10`)] - ) - ), - enum.item( - referenceable_note( - "note-fence", - [`FENCE`: currently, the VM interprets this operation as `ADDI x0 x0 0`; a no-op.] - ) - ) -)