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/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, diff --git a/spec/decode.typ b/spec/decode.typ new file mode 100644 index 000000000..24846d2c1 --- /dev/null +++ b/spec/decode.typ @@ -0,0 +1,219 @@ +#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, + render_chip_padding_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 table +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. +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 table is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_column_table(chip, config) + +== 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) + + +== 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/src/decode.toml b/spec/src/decode.toml new file mode 100644 index 000000000..6c01e4f6c --- /dev/null +++ b/spec/src/decode.toml @@ -0,0 +1,58 @@ +name = "DECODE" + +[[variables.output]] +name = "pc" +type = "DWordWL" +desc = "value of the program counter this instruction is associated with." +# TODO(#136): fix this when padding the CPU +pad = 1 + +[[variables.output]] +name = "packed_decode" +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:\\ +[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`; \\ +the remaining bits are set to zero. +""" +pad = 0 + +[[variables.output]] +name = "imm" +type = "DWordWL" +desc = "the *fully extended (!)* 64-bit version of the immediate." +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..8457005f8 --- /dev/null +++ b/spec/src/decode_uncompressed.toml @@ -0,0 +1,157 @@ +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 exactly $2$ bytes." + +[[variables.output]] +name = "mem_4B" +type = "Bit" +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 exactly $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." + +[[variables.output]] +name = "mp_selector" +type = "Bit" +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" +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."