spec: CPU padding

spec/cpu.typ

@@ -6,6 +6,7 @@
   total_nr_variables,
   total_nr_instantiated_columns,
   render_constraint_table,
+  render_chip_padding_table,
 )
 
 #let config = load_config()
@@ -82,3 +83,12 @@ For @cpu:c:is_equal, refer to the logic of IsZero or IsEqual, in combination wit
 #render_constraint_table(chip, config, groups: "misc")
 
 #rj[Document the choice to not have a multiplicity column here for padding]
+
+== Padding
+
+The CPU can be padded with the following values, which have a corresponding row
+in the DECODE table, at the _odd_ address 1, only reachable through a HALT ecall.
+
+#render_chip_padding_table(chip, config)
+
+This approach minimizes the number of dependent lookups, increasing only multiplicities in the DECODE table and the IS_BYTE lookup.

spec/decode.typ

@@ -32,8 +32,13 @@ The #decode table is comprised of #nr_variables variables that are expressed usi
 == 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)
 
+Note that this row sets the `EBREAK` flag.
+Given that `CPU` asserts that `EBREAK = 0` (see @cpu:c:ebreak_traps), using this "padding-instruction" would immediately make the CPU table unprovable.
+Note moreover that the `pc` is set to $7$.
+This value is the _smallest odd number_ (i.e., not reachable during regular execution) that is more than _$4$_ (i.e., the max `pc`-increment) greater than _$1$_ (i.e., the `pc`-value used in the #link(<cpu-padding-decode-row>)[additional instruction] referred to by `CPU`-padding lines).
 
 == Decoding
 For the purposes of explaining decoding, we decompress #decode's `packed_decode` variable into its constituent variables.
@@ -46,16 +51,17 @@ Note that the below table is _not_ used in practice: it is solely used for the p
 
 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,
+- *`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,
+- *`w_instr`*, *`signed`*: whether to set the `word_instr` and `signed` flags, 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$.
++ `read_register1`, `read_register2` and `write_register` are set to $1$ when respectively $#`rs1` != 0$, $#`rs2` != 0$, or  $#`rd` != 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.
+  *The `c_type` flag is set independently of the below table*, as explained next.
 
 Further clarification is provided in the notes following the table.
 
@@ -74,76 +80,76 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is
   show figure: set block(breakable: true)
 
   figure(table(
-    columns: (auto, auto, 40pt, 40pt, 40pt, 1fr, 15pt),
+    columns: (auto, auto, 40pt, 40pt, 1fr, 15pt),
     stroke: 0pt,
     inset: (right: .5em),
-    align: (left, right, center, center, center, left, right),
+    align: (left, right, 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.header([*Operation*], [*op-flag*], [*`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*]),
+    table.footer([*Operation*], [*op-flag*], [*`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>)]),
+  ([`ADDI[W]   rd, rs1, imm`], [`ADD`], [`[W]`], [], [], [#ref_note(<note_word_instr>)]),
+  ([`SLTI[U]   rd, rs1, imm`], [`SLT`], [], [#sym.not`[U]`], [], [#ref_note(<note_signed>)]),
+  ([`ANDI      rd, rs1, imm`], [`AND`], [], [], [], []),
+  ([`ORI       rd, rs1, imm`], [`OR`],   [], [], [], []),
+  ([`XORI      rd, rs1, imm`], [`XOR`], [], [], [], []),
+  ([`SLLI[W]   rd, rs1, imm`], [`SHIFT`], [`[W]`], [], [], []),
+  ([`SRLI[W]   rd, rs1, imm`], [`SHIFT`], [`[W]`], [], [`mp_selector`], [#ref_note(<note_word_instr>)]),
+  ([`SRAI[W]   rd, rs1, imm`], [`SHIFT`], [`[W]`], [1], [`mp_selector`], [#ref_note(<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>)]),
+  ([`ADD[W]    rd, rs1, rs2`], [`ADD`], [`[W]`], [], [], [#ref_note(<note_word_instr>)]),
+  ([`SUB[W]    rd, rs1, rs2`], [`SUB`], [`[W]`], [], [], [#ref_note(<note_word_instr>)]),
+  ([`SLT[U]    rd, rs1, rs2`], [`SLT`], [], [#sym.not`[U]`], [], [#ref_note(<note_signed>)]),
+  ([`AND       rd, rs1, rs2`], [`AND`], [], [], [], []),
+  ([`OR        rd, rs1, rs2`], [`OR`], [], [], [], []),
+  ([`XOR       rd, rs1, rs2`], [`XOR`], [], [], [], []),
+  ([`SLL[W]    rd, rs1, rs2`], [`SHIFT`], [`[W]`], [], [], [#ref_note(<note_word_instr>)]),
+  ([`SRL[W]    rd, rs1, rs2`], [`SHIFT`], [`[W]`], [], [`mp_selector`], [#ref_note(<note_word_instr>)]),
+  ([`SRA[W]    rd, rs1, rs2`], [`SHIFT`], [`[W]`], [1], [`mp_selector`], [#ref_note(<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>)]),
+  ([`MUL[W]    rd, rs1, rs2`], [`MUL`], [`[W]`], [1], [`mp_selector`], [#ref_note(<note_word_instr>)]),
+  ([`MULH      rd, rs1, rs2`], [`MUL`], [], [1], [`mp_selector`, `muldiv_selector`], []),
+  ([`MULHU     rd, rs1, rs2`], [`MUL`], [], [], [`muldiv_selector`], []),
+  ([`MULHSU    rd, rs1, rs2`], [`MUL`], [], [1], [`muldiv_selector`], []),
+  ([`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [], [#ref_note(<note_word_instr>, <note_signed>)]),
+  ([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [`muldiv_selector`], [#ref_note(<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>)]),
+  ([`LUI       rd, imm`], [`ADD`], [], [], [], [#ref_note(<note-lui>)]),
+  ([`AUIPC     rd, imm`], [`ADD`], [], [], [`rs1 := x255`], [#ref_note(<note-auipc>)]),
+  ([`JAL       rd, imm`], [`JALR`], [], [], [`rs1 := x255`], [#ref_note(<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>)]),
+  ([`JALR      rd, rs1, imm`], [`JALR`], [], [], [], []),
+  ([`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>)]),
+  ([`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`], [], [], [], [], []),
+  ([`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`], [], [], [], [], []),
+  ([`ECALL`], [`ECALL`], [], [], [$#`rs1` := #`x17`$, $#`rs2` := #`x10`$, $#`rd` := #`x10`$], [#ref_note(<note-ecall>)]),
+  ([`EBREAK`], [`EBREAK`], [], [], [], []),
   // FENCE
-  ([`FENCE`], [`ADD`], [], [], [], [], [#ref_note(<note-fence>)]),
+  ([`FENCE`], [`ADD`], [], [], [], [#ref_note(<note-fence>)]),
 )
 
 #decoding_table(decoding)
@@ -157,16 +163,10 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is
 ==== 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.]
+      [`word_instr`: `[W]` indicates that $#`word_instr` = 1$ for the `W`-variant of the operation, and $0$ for the non-`W`-variant.]
     )
   ),
   enum.item(
@@ -194,9 +194,9 @@ We note the following about the above decoding table:
   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`.
+      [`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.*]
+      As such, *we expect the decoding to take care of writing the immediate in bit range $[1:21]$ of `imm` and extending it to 64 bits; the least significant bit should always be 0.*]
     )
   ),
   enum.item(
@@ -206,7 +206,7 @@ We note the following about the above decoding table:
       "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`)
+      - first syscall argument in A0 (= register `x10`)
       - syscall output in A0 (= register `x10`)]
     )
   ),
@@ -217,3 +217,10 @@ We note the following about the above decoding table:
     )
   )
 )
+
+== One more instruction <cpu-padding-decode-row>
+In addition to decoding all instructions provided in the ELF and adding a corresponding entry to the #decode table, one must include an entry that has $#`pc` = 1$ and every other variable set to $0$.
+Note that this will never conflict with any entry in the ELF, since it has an odd `pc` value.
+
+This entry is used to pad the `CPU` table.
+More details on this matter are provided in the `CPU` chip.