spec: DECODE

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]

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,

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(<note_w_reg>, <note_word_instr>)]),
+  ([`SLTI[U]   rd, rs1, imm`], [`SLT`], [$#`rd` eq.not 0$], [], [#sym.not`[U]`], [], [#ref_note(<note_w_reg>, <note_signed>)]),
+  ([`ANDI      rd, rs1, imm`], [`AND`], [$#`rd` eq.not 0$], [], [], [], [#ref_note(<note_w_reg>)]),
+  ([`ORI       rd, rs1, imm`], [`OR`],  [$#`rd` eq.not 0$],  [], [], [], [#ref_note(<note_w_reg>)]),
+  ([`XORI      rd, rs1, imm`], [`XOR`], [$#`rd` eq.not 0$], [], [], [], [#ref_note(<note_w_reg>)]),
+  ([`SLLI[W]   rd, rs1, imm`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [], [#ref_note(<note_w_reg>)]),
+  ([`SRLI[W]   rd, rs1, imm`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [`mp_selector`], [#ref_note(<note_w_reg>, <note_word_instr>)]),
+  ([`SRAI[W]   rd, rs1, imm`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [1], [`mp_selector`], [#ref_note(<note_w_reg>, <note_word_instr>)]),
+  // OP
+  ([`ADD[W]    rd, rs1, rs2`], [`ADD`], [$#`rd` eq.not 0$], [`[W]`], [], [], [#ref_note(<note_w_reg>, <note_word_instr>)]),
+  ([`SUB[W]    rd, rs1, rs2`], [`SUB`], [$#`rd` eq.not 0$], [`[W]`], [], [], [#ref_note(<note_w_reg>, <note_word_instr>)]),
+  ([`SLT[U]    rd, rs1, rs2`], [`SLT`], [$#`rd` eq.not 0$], [], [#sym.not`[U]`], [], [#ref_note(<note_w_reg>, <note_signed>)]),
+  ([`AND       rd, rs1, rs2`], [`AND`], [$#`rd` eq.not 0$], [], [], [], [#ref_note(<note_w_reg>)]),
+  ([`OR        rd, rs1, rs2`], [`OR`], [$#`rd` eq.not 0$], [], [], [], [#ref_note(<note_w_reg>)]),
+  ([`XOR       rd, rs1, rs2`], [`XOR`], [$#`rd` eq.not 0$], [], [], [], [#ref_note(<note_w_reg>)]),
+  ([`SLL[W]    rd, rs1, rs2`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [], [#ref_note(<note_w_reg>, <note_word_instr>)]),
+  ([`SRL[W]    rd, rs1, rs2`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [], [`mp_selector`], [#ref_note(<note_w_reg>, <note_word_instr>)]),
+  ([`SRA[W]    rd, rs1, rs2`], [`SHIFT`], [$#`rd` eq.not 0$], [`[W]`], [1], [`mp_selector`], [#ref_note(<note_w_reg>, <note_word_instr>)]),
+  // OP - M
+  ([`MUL[W]    rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [`[W]`], [1], [`mp_selector`], [#ref_note(<note_w_reg>, <note_word_instr>)]),
+  ([`MULH      rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [], [1], [`mp_selector`, `muldiv_selector`], [#ref_note(<note_w_reg>)]),
+  ([`MULHU     rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [], [], [`muldiv_selector`], [#ref_note(<note_w_reg>)]),
+  ([`MULHSU    rd, rs1, rs2`], [`MUL`], [$#`rd` eq.not 0$], [], [1], [`muldiv_selector`], [#ref_note(<note_w_reg>)]),
+  ([`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`rd` eq.not 0$], [`[W]`], [#sym.not`[U]`], [], [#ref_note(<note_w_reg>, <note_word_instr>, <note_signed>)]),
+  ([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [$#`rd` eq.not 0$], [`[W]`], [#sym.not`[U]`], [`muldiv_selector`], [#ref_note(<note_w_reg>, <note_word_instr>, <note_signed>)]),
+  // LUI/AUIPC
+  ([`LUI       rd, imm`], [`ADD`], [$#`rd` eq.not 0$], [], [], [], [#ref_note(<note_w_reg>, <note-lui>)]),
+  ([`AUIPC     rd, imm`], [`ADD`], [$#`rd` eq.not 0$], [], [], [`rs1 := x255`], [#ref_note(<note_w_reg>, <note-auipc>)]),
+  ([`JAL       rd, imm`], [`JALR`], [$#`rd` eq.not 0$], [], [], [`rs1 := x255`], [#ref_note(<note_w_reg>, <note-jal>)]),
+  // Branching
+  ([`JALR      rd, rs1, imm`], [`JALR`], [$#`rd` eq.not 0$], [], [], [], [#ref_note(<note_w_reg>)]),
+  ([`BEQ      rs1, rs2, imm`], [`BEQ`], [], [], [], [], []),
+  ([`BNE      rs1, rs2, imm`], [`BEQ`], [], [], [], [`mp_selector`], []),
+  ([`BLT[U]   rs1, rs2, imm`], [`BLT`], [], [], [#sym.not`[U]`], [], [#ref_note(<note_signed>)]),
+  ([`BGE[U]   rs1, rs2, imm`], [`BLT`], [], [], [#sym.not`[U]`], [`mp_selector`], [#ref_note(<note_signed>)]),
+  // LOAD
+  ([`LD        rd, rs1, imm`], [`LOAD`], [], [], [], [`mem_8B`], []),
+  ([`LW[U]     rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [`mem_4B`], [#ref_note(<note_signed>)]),
+  ([`LH[U]     rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [`mem_2B`], [#ref_note(<note_signed>)]),
+  ([`LB[U]     rd, rs1, imm`], [`LOAD`], [], [], [#sym.not`[U]`], [], [#ref_note(<note_signed>)]),
+  // 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(<note-ecall>)]),
+  ([`EBREAK`], [`EBREAK`], [], [], [], [], []),
+  // FENCE
+  ([`FENCE`], [`ADD`], [], [], [], [], [#ref_note(<note-fence>)]),
+)
+
+#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.]
+    )
+  )
+)

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