diff --git a/spec/cpu.typ b/spec/cpu.typ index 00a33f5a2..784d750d2 100644 --- a/spec/cpu.typ +++ b/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. diff --git a/spec/decode.typ b/spec/decode.typ index 24846d2c1..d8332e033 100644 --- a/spec/decode.typ +++ b/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()[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,19 +80,19 @@ 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] ) @@ -94,56 +100,56 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is #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(, )]), + ([`ADDI[W] rd, rs1, imm`], [`ADD`], [`[W]`], [], [], [#ref_note()]), + ([`SLTI[U] rd, rs1, imm`], [`SLT`], [], [#sym.not`[U]`], [], [#ref_note()]), + ([`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()]), + ([`SRAI[W] rd, rs1, imm`], [`SHIFT`], [`[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(, )]), + ([`ADD[W] rd, rs1, rs2`], [`ADD`], [`[W]`], [], [], [#ref_note()]), + ([`SUB[W] rd, rs1, rs2`], [`SUB`], [`[W]`], [], [], [#ref_note()]), + ([`SLT[U] rd, rs1, rs2`], [`SLT`], [], [#sym.not`[U]`], [], [#ref_note()]), + ([`AND rd, rs1, rs2`], [`AND`], [], [], [], []), + ([`OR rd, rs1, rs2`], [`OR`], [], [], [], []), + ([`XOR rd, rs1, rs2`], [`XOR`], [], [], [], []), + ([`SLL[W] rd, rs1, rs2`], [`SHIFT`], [`[W]`], [], [], [#ref_note()]), + ([`SRL[W] rd, rs1, rs2`], [`SHIFT`], [`[W]`], [], [`mp_selector`], [#ref_note()]), + ([`SRA[W] rd, rs1, rs2`], [`SHIFT`], [`[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(, , )]), + ([`MUL[W] rd, rs1, rs2`], [`MUL`], [`[W]`], [1], [`mp_selector`], [#ref_note()]), + ([`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(, )]), + ([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [`[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(, )]), + ([`LUI rd, imm`], [`ADD`], [], [], [], [#ref_note()]), + ([`AUIPC rd, imm`], [`ADD`], [], [], [`rs1 := x255`], [#ref_note()]), + ([`JAL rd, imm`], [`JALR`], [], [], [`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()]), + ([`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()]), + ([`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()]), + ([`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`], [], [], [], [], []), + ([`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`], [], [], [], [], []), + ([`ECALL`], [`ECALL`], [], [], [$#`rs1` := #`x17`$, $#`rs2` := #`x10`$, $#`rd` := #`x10`$], [#ref_note()]), + ([`EBREAK`], [`EBREAK`], [], [], [], []), // FENCE - ([`FENCE`], [`ADD`], [], [], [], [], [#ref_note()]), + ([`FENCE`], [`ADD`], [], [], [], [#ref_note()]), ) #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 +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. \ No newline at end of file diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 63ed2005f..b7c79d62d 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -13,48 +13,69 @@ desc = "A preprocessed timestamp to coordinate the memory argument. Since we hav name = "pc" type = "DWordWL" desc = "The program counter" +pad = 1 [[variables.input]] name = "rs1" type = "Byte" desc = "Source register 1 index" +pad = 0 [[variables.input]] name = "rs2" type = "Byte" desc = "Source register 2 index" +pad = 0 [[variables.input]] name = "rd" type = "Byte" desc = "Destination register index" +pad = 0 + +[[variables.input]] +name = "read_register1" +type = "Bit" +desc = "Whether to read from `rs1` (1) or to place a 0 in `rv1` (0)" +pad = 0 + +[[variables.input]] +name = "read_register2" +type = "Bit" +desc = "Whether to read from `rs2` (1) or to place a 0 in `rv2` (0)" +pad = 0 [[variables.input]] name = "write_register" type = "Bit" desc = "Whether to write back to the destination register" +pad = 0 # TODO: can we compress this to a single value? (1: is it worth it, 2: does it work) [[variables.input]] name = "memory_2bytes" type = "Bit" desc = "Whether the memory access (read or write) touches exactly 2 bytes" +pad = 0 [[variables.input]] name = "memory_4bytes" type = "Bit" desc = "Whether the memory access (read or write) touches exactly 4 bytes" +pad = 0 [[variables.input]] name = "memory_8bytes" type = "Bit" desc = "Whether the memory access (read or write) touches exactly 8 bytes" +pad = 0 # TODO: Are there usecases where it's nicer to just have this as a length constant? [[variables.input]] name = "c_type_instruction" type = "Bit" desc = "Whether the instruction is of C type, i.e., whether it is 2 bytes long instead of 4" +pad = 0 # TODO: Should this just be a word? (CHECK: effect on computation/extension of arg2) # TODO: make sure decode correctly extends this (may be zero for unsigned and word_instr?) @@ -62,11 +83,13 @@ desc = "Whether the instruction is of C type, i.e., whether it is 2 bytes long i name = "imm" type = "DWordWL" desc = "The fully extended 64-bit version of the immediate" +pad = 0 [[variables.input]] name = "signed" type = "Bit" desc = "Indicates whether we're dealing with a signed or unsigned instruction" +pad = 0 [[variables.input]] name = "mp_selector" @@ -75,96 +98,115 @@ desc = """Multi-purpose selector used by different ALU operations for different - 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`""" +pad = 0 [[variables.input]] name = "muldiv_selector" type = "Bit" desc = "Selects which output of `MUL` (lo/hi) or `DIV` (quo/rem) is wanted" +pad = 0 [[variables.input]] name = "word_instr" type = "Bit" desc = "Whether the instruction is a \\*W instruction, requiring the inputs and outputs to be (sign) extended" +pad = 0 [[variables.input]] name = "ADD" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "SUB" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "SLT" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "AND" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "OR" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "XOR" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "SHIFT" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "JALR" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "BEQ" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "BLT" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "LOAD" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "STORE" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "MUL" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "DIVREM" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "ECALL" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 [[variables.input]] name = "EBREAK" type = "Bit" desc = "One-hot ALU selector flag" +pad = 0 # Output @@ -172,102 +214,122 @@ desc = "One-hot ALU selector flag" name = "next_pc" type = "DWordWL" desc = "The program counter for the next instruction" +pad = 5 [[variables.output]] name = "rvd" type = "DWordWL" desc = "The value to (maybe) be written back to rvd" +pad = 0 # Auxiliary [[variables.auxiliary]] name = "rv1" type = "DWordWHH" desc = "The value of register `rs1`" +pad = 0 [[variables.auxiliary]] name = "rv2" type = "DWordWHH" desc = "The value of register `rs2`" +pad = 0 [[variables.auxiliary]] name = "rv1_sign_bit" type = "Bit" desc = "The sign bit of `rv1` if seen as a 32-bit word" +pad = 0 [[variables.auxiliary]] name = "arg1" type = "DWordBL" -desc = "The extended version of `rv1`, depending on `c_type_instruction`" +desc = "The extended version of `rv1`, depending on `word_instr`" +pad = 0 [[variables.auxiliary]] name = "arg2_sign_bit" type = "Bit" desc = "The sign bit of `arg2` if seen as a 32-bit word" +pad = 0 [[variables.auxiliary]] name = "arg2" type = "DWordBL" desc = "A multiplexed version of `rv2` and `imm`, to be used as second argument to ALU calls" +pad = 0 [[variables.auxiliary]] name = "res_sign_bit" type = "Bit" desc = "The sign bit of `res`, if seen as a 32-bit word" +pad = 0 [[variables.auxiliary]] name = "res" type = "DWordBL" desc = "The ALU result" +pad = 0 [[variables.auxiliary]] name = "is_equal" type = "Bit" desc = "Whether `rv1` and `arg2` are equal" +pad = 0 [[variables.auxiliary]] name = "branch_cond" type = "Bit" desc = "Whether a branch is taken, i.e., the branch condition" +pad = 0 # Virtual [[variables.virtual]] name = "packed_decode" type = "BaseField" desc = "A packed representation of all bit flags and register indices obtained from the decoding" -poly = ["+", - ["*", ["^", 2, 0], "write_register"], - ["*", ["^", 2, 1], "memory_2bytes"], - ["*", ["^", 2, 2], "memory_4bytes"], - ["*", ["^", 2, 3], "memory_8bytes"], - ["*", ["^", 2, 4], "c_type_instruction"], - ["*", ["^", 2, 5], "signed"], - ["*", ["^", 2, 6], "mp_selector"], - ["*", ["^", 2, 7], "muldiv_selector"], - ["*", ["^", 2, 8], "word_instr"], - ["*", ["^", 2, 9], "ADD"], - ["*", ["^", 2, 10], "SUB"], - ["*", ["^", 2, 11], "SLT"], - ["*", ["^", 2, 12], "AND"], - ["*", ["^", 2, 13], "OR"], - ["*", ["^", 2, 14], "XOR"], - ["*", ["^", 2, 15], "SHIFT"], - ["*", ["^", 2, 16], "JALR"], - ["*", ["^", 2, 17], "BEQ"], - ["*", ["^", 2, 18], "BLT"], - ["*", ["^", 2, 19], "LOAD"], - ["*", ["^", 2, 20], "STORE"], - ["*", ["^", 2, 21], "MUL"], - ["*", ["^", 2, 22], "DIVREM"], - ["*", ["^", 2, 23], "ECALL"], - ["*", ["^", 2, 24], "EBREAK"], - ["*", ["^", 2, 25], "rs1"], - ["*", ["^", 2, 33], "rs2"], - ["*", ["^", 2, 41], "rd"], +def = ["+", + ["*", ["^", 2, 0], "read_register1"], + ["*", ["^", 2, 1], "read_register2"], + ["*", ["^", 2, 2], "write_register"], + ["*", ["^", 2, 3], "memory_2bytes"], + ["*", ["^", 2, 4], "memory_4bytes"], + ["*", ["^", 2, 5], "memory_8bytes"], + ["*", ["^", 2, 6], "c_type_instruction"], + ["*", ["^", 2, 7], "signed"], + ["*", ["^", 2, 8], "mp_selector"], + ["*", ["^", 2, 9], "muldiv_selector"], + ["*", ["^", 2, 10], "word_instr"], + ["*", ["^", 2, 11], "ADD"], + ["*", ["^", 2, 12], "SUB"], + ["*", ["^", 2, 13], "SLT"], + ["*", ["^", 2, 14], "AND"], + ["*", ["^", 2, 15], "OR"], + ["*", ["^", 2, 16], "XOR"], + ["*", ["^", 2, 17], "SHIFT"], + ["*", ["^", 2, 18], "JALR"], + ["*", ["^", 2, 19], "BEQ"], + ["*", ["^", 2, 20], "BLT"], + ["*", ["^", 2, 21], "LOAD"], + ["*", ["^", 2, 22], "STORE"], + ["*", ["^", 2, 23], "MUL"], + ["*", ["^", 2, 24], "DIVREM"], + ["*", ["^", 2, 25], "ECALL"], + ["*", ["^", 2, 26], "EBREAK"], + ["*", ["^", 2, 27], "rs1"], + ["*", ["^", 2, 35], "rs2"], + ["*", ["^", 2, 43], "rd"], ] +[[variables.virtual]] +name = "pad" +type = "Bit" +desc = "When no flags are set, we must be in a padding row." +def = ["-", 1, "ADD", "SUB", "SLT", "AND", "OR", "XOR", "SHIFT", "JALR", "BEQ", "BLT", "LOAD", "STORE", "MUL", "DIVREM", "ECALL", "EBREAK"] + [[assumptions]] -desc = "The flags are a one-hot vector in the decoding" +desc = "At most one ALU selector flag is 1 by the decoding, and every other flag is 0." ref = "cpu:a:one-hot" [[assumptions]] @@ -287,6 +349,18 @@ input = ["pc", "imm", "packed_decode"] name = "range" prefix = "R" +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["read_register1"] +ref = "cpu:c:range_read_register1" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["read_register2"] +ref = "cpu:c:range_read_register2" + [[constraints.range]] kind = "template" tag = "IS_BIT" @@ -314,8 +388,8 @@ ref = "cpu:c:range_memory_8bytes" [[constraints.range]] kind = "template" tag = "IS_BIT" -input = ["c_kind_instruction"] -ref = "cpu:c:range_c_kind_instruction" +input = ["c_type_instruction"] +ref = "cpu:c:range_c_type_instruction" [[constraints.range]] kind = "template" @@ -568,6 +642,13 @@ kind = "interaction" tag = "MEMW" input = [1, ["*", 2, "rs1"], "rv1", ["+", "timestamp", 0], 1, 0, 0] output = "rv1" +multiplicity = "read_register1" + +[[constraints.mem]] +kind = "arith" +constraint = "$#`!read_register1` => #`rv1[i]` = 0$" +poly = ["*", ["not", "read_register1"], ["idx", "rv1", "i"]] +iter = ["i", 0, 2] # TODO: no types available, so no casting yet [[constraints.mem]] @@ -575,6 +656,13 @@ kind = "interaction" tag = "MEMW" input = [1, ["*", 2, "rs2"], "rv2", ["+", "timestamp", 1], 1, 0, 0] output = "rv2" +multiplicity = "read_register2" + +[[constraints.mem]] +kind = "arith" +constraint = "$#`!read_register2` => #`rv2[i]` = 0$" +poly = ["*", ["not", "read_register2"], ["idx", "rv2", "i"]] +iter = ["i", 0, 2] # TODO: no types available, so no casting yet [[constraints.mem]] @@ -602,6 +690,7 @@ kind = "interaction" tag = "MEMW" input = [1, ["*", 2, 255], "next_pc", ["+", "timestamp", 1], 1, 0, 0] output = "pc" +multiplicity = ["not", "pad"] [[constraint_groups]] @@ -613,6 +702,7 @@ kind = "arith" constraint = "`!EBREAK`" desc = "We treat `EBREAK` as an unprovable trap" poly = ["not", "EBREAK"] +ref = "cpu:c:ebreak_traps" # TODO: no types available, so no casting yet [[constraints.sys]] diff --git a/spec/src/decode.toml b/spec/src/decode.toml index 6c01e4f6c..367db1568 100644 --- a/spec/src/decode.toml +++ b/spec/src/decode.toml @@ -4,8 +4,7 @@ name = "DECODE" 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 +pad = 7 [[variables.output]] name = "packed_decode" @@ -13,37 +12,39 @@ 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`; \\ +[0] `read_register1`, \\ +[1] `read_register2`, \\ +[2] `write_register`, \\ +[3] `memory_2bytes`, \\ +[4] `memory_4bytes`, \\ +[5] `memory_8bytes`, \\ +[6] `c_type`, \\ +[7] `signed`, \\ +[8] `mp_selector`, \\ +[9] `muldiv_selector`, \\ +[10] `word_instr`, \\ +[11] `ADD`, \\ +[12] `SUB`, \\ +[13] `SLT`, \\ +[14] `AND`, \\ +[15] `OR`, \\ +[16] `XOR`, \\ +[17] `SHIFT`, \\ +[18] `JALR`, \\ +[19] `BEQ`, \\ +[20] `BLT`, \\ +[21] `LOAD`, \\ +[22] `STORE`, \\ +[23] `MUL`, \\ +[24] `DIVREM`, \\ +[25] `ECALL`, \\ +[26] `EBREAK`; \\ +[27:35] `rs1`, \\ +[35:43] `rs2`, \\ +[43:51] `rd`, \\ the remaining bits are set to zero. """ -pad = 0 +pad = ["^", 2, 26] [[variables.output]] name = "imm" diff --git a/spec/src/decode_uncompressed.toml b/spec/src/decode_uncompressed.toml index 8457005f8..0f6c931c2 100644 --- a/spec/src/decode_uncompressed.toml +++ b/spec/src/decode_uncompressed.toml @@ -20,6 +20,16 @@ name = "rd" type = "Byte" desc = "index of destination register." +[[variables.output]] +name = "read_register1" +type = "Bit" +desc = "whether to load the contents of address `rs1` (1) or `0` (0) into `rv1`." + +[[variables.output]] +name = "read_register2" +type = "Bit" +desc = "whether to load the contents of address `rs2` (1) or `0` (0) into `rv2`." + [[variables.output]] name = "write_register" type = "Bit"