From 113aa9a17002ad1d95afdc8bdd1945441c2ad458 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 29 Dec 2025 15:55:38 +0100 Subject: [PATCH 1/4] spec: Initial CPU version to handle RV64IMC --- spec/book.typ | 2 +- spec/cpu.typ | 84 ++++++ spec/src/config.toml | 16 +- spec/src/cpu.toml | 696 +++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 796 insertions(+), 2 deletions(-) create mode 100644 spec/cpu.typ create mode 100644 spec/src/cpu.toml diff --git a/spec/book.typ b/spec/book.typ index dcf1d0c1b..c4c3a8c6d 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -1,4 +1,3 @@ - #import "@preview/shiroa:0.3.1": * #show: book @@ -8,6 +7,7 @@ summary: [ #chapter("variables.typ")[Variables] #chapter("is_bit.typ")[IS_BIT template] + #chapter("cpu.typ")[CPU chip] ] ) diff --git a/spec/cpu.typ b/spec/cpu.typ new file mode 100644 index 000000000..09b8c00ad --- /dev/null +++ b/spec/cpu.typ @@ -0,0 +1,84 @@ +#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/cpu.toml", config) + +#show: book-page.with(title: "CPU chip") + +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The `CPU` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_column_table(chip, config) + +== Assumptions +#render_chip_assumptions(chip, config) + +== Constraints +First, we perform a decoding lookup for the current PC. + +#render_constraint_table(chip, config, groups: "decode") + +#rj[All casts for interactions will have to be reviewed once other chip interfaces stabilise] + +=== Range checks + +We constrain all columns to have the appropriate ranges. +The flags and register indices looked up from the decoding need to be checked, +as they are communicated through the interaction in a packed form. +In contrast, we know ahead of time that decoding will ensure proper range checks for `pc` and `imm`. +Similarly, since `next_pc` will propagate through the memory argument and be looked up +in the instruction decoding on the next cycle, it is forced to be in the correct range.#rj[is this true, do we need this elsewhere for chip assumptions?] +For the auxiliary columns, we need to check the limbs of `arg1`, `arg2`, and `res`. +The ranges of the other auxiliary columns are enforced through later constraints. +#rj[Make sure we argue for every column here] +#rj[is `rvd` still sufficiently constrained? (can also be done through the memory argument like `pc`?)] + +#render_constraint_table(chip, config, groups: "range") + +=== ALU + +The ALU functionality is then obtained through judicious dispatching to the corresponding chips. + +#render_constraint_table(chip, config, groups: "alu") + +=== Memory + +The interactions with the memory, both for register loading and storing, as for `LOAD` and `STORE` instructions are handled. +Note that since registers need no byte-addressing, we store them in the memory argument with `Word` limbs. +The timestamps are ensured to be disjoint for disjoint memory locations. +One consequence of that is that `next_pc` is written at `timestamp + 1` +to ensure the access is disjoint with the `pc` read into `rv1` as part of the `AUIPC` instruction. + +#render_constraint_table(chip, config, groups: "mem") + +=== System + +The interactions with the wider system. + +#render_constraint_table(chip, config, groups: "sys") + +=== Input and output to the ALU + +We constraint `arg1`, `arg2` and `rvd` to correspond to the wanted values, +including the appropriate sign/zero extension, depending on `word_instruction`. + +#render_constraint_table(chip, config, groups: "ext") + +=== Other constraints + +#rj[proper ref to IsZero/IsEqual] +For @cpu:c:is_equal, refer to the logic of IsZero or IsEqual, in combination with the subtraction of @cpu:c:sub. + +#render_constraint_table(chip, config, groups: "misc") + +#rj[Document the choice to not have a multiplicity column here for padding] diff --git a/spec/src/config.toml b/spec/src/config.toml index 28abdcbfc..b66639e2a 100644 --- a/spec/src/config.toml +++ b/spec/src/config.toml @@ -78,9 +78,23 @@ subtypes = ["Word", "Half", "Half"] desc = """\ Variable that can only assume values in the range $[0, 2^64)$. \\ Represented as a `Word` and two `Half` variables.\ - The `Word` is the least significant digit. + The `Word` is the *least* significant digit. """ +[[variables.types]] +label = "DWordWHH" +subtypes = ["Half", "Half", "Word"] +desc = """\ + Variable that can only assume values in the range $[0, 2^64)$. \\ + Represented as a `Word` and two `Half` variables.\ + The `Word` is the *most* significant digit. + """ + +[[variables.types]] +label = "Timestamp" +subtypes = ["DWordWL"] +desc = "A preprocessed column holding timestamps as `DWordWL`. Row `i` of the column contains the value $2^2 dot (i + 1)$. Used in the CPU chip, see there for more details about the magic number." + [variables.categories] all = ["input", "output", "auxiliary", "virtual", "multiplicity", "condition"] instantiated = ["input", "output", "auxiliary", "multiplicity"] diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml new file mode 100644 index 000000000..8f4074cd2 --- /dev/null +++ b/spec/src/cpu.toml @@ -0,0 +1,696 @@ +name = "CPU" + + +# Input +# Let's call the variables coming from DECODE input + +[[variables.input]] +name = "timestamp" +type = "Timestamp" +desc = "A preprocessed timestamp to coordinate the memory argument. Since we have at most 3 non-disjoint memory accesses (`(rs1, rs2, rd)`, `(rs1, pc, pc)`, `(LOAD)` or `(STORE)`) a maximum of 4 slots is enough." + +[[variables.input]] +name = "pc" +type = "DWordWL" +desc = "The program counter" + +[[variables.input]] +name = "rs1" +type = "Byte" +desc = "Source register 1 index" + +[[variables.input]] +name = "rs2" +type = "Byte" +desc = "Source register 2 index" + +[[variables.input]] +name = "rd" +type = "Byte" +desc = "Destination register index" + +[[variables.input]] +name = "write_register" +type = "Bit" +desc = "Whether to write back to the destination register" + +# 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 at least 2 bytes" + +[[variables.input]] +name = "memory_4bytes" +type = "Bit" +desc = "Whether the memory access (read or write) touches at least 4 bytes" + +[[variables.input]] +name = "memory_8bytes" +type = "Bit" +desc = "Whether the memory access (read or write) touches at least 8 bytes" + +# 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" + +# 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_instruction?) +[[variables.input]] +name = "imm" +type = "DWordWL" +desc = "The fully extended 64-bit version of the immediate" + +[[variables.input]] +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`)""" + +[[variables.input]] +name = "muldiv_selector" +type = "Bit" +desc = "Selects which output of `MUL` (lo/hi) or `DIV` (quo/rem) is wanted" + +[[variables.input]] +name = "word_instruction" +type = "Bit" +desc = "Whether the instruction is a \\*W instruction, requiring the inputs and outputs to be (sign) extended" + +[[variables.input]] +name = "ADD" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "SUB" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "SLT" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "AND" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "OR" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "XOR" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "SHIFT" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "JALR" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "BEQ" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "BLT" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "LOAD" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "STORE" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "MUL" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "DIVREM" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "ECALL" +type = "Bit" +desc = "One-hot ALU selector flag" + +[[variables.input]] +name = "EBREAK" +type = "Bit" +desc = "One-hot ALU selector flag" + + +# Output +[[variables.output]] +name = "next_pc" +type = "DWordWL" +desc = "The program counter for the next instruction" + +[[variables.output]] +name = "rvd" +type = "DWordWL" +desc = "The value to (maybe) be written back to rvd" + +# Auxiliary +[[variables.auxiliary]] +name = "rv1" +type = "DWordWHH" +desc = "The value of register `rs1`" + +[[variables.auxiliary]] +name = "rv2" +type = "DWordWHH" +desc = "The value of register `rs2`" + +[[variables.auxiliary]] +name = "rv1_sign_bit" +type = "Bit" +desc = "The sign bit of `rv1` if seen as a 32-bit word" + +[[variables.auxiliary]] +name = "arg1" +type = "DWordBL" +desc = "The extended version of `rv1`, depending on `c_type_instruction`" + +[[variables.auxiliary]] +name = "arg2_sign_bit" +type = "Bit" +desc = "The sign bit of `arg2` if seen as a 32-bit word" + +[[variables.auxiliary]] +name = "arg2" +type = "DWordBL" +desc = "A multiplexed version of `rv2` and `imm`, to be used as second argument to ALU calls" + +[[variables.auxiliary]] +name = "res_sign_bit" +type = "Bit" +desc = "The sign bit of `res`, if seen as a 32-bit word" + +[[variables.auxiliary]] +name = "res" +type = "DWordBL" +desc = "The ALU result" + +[[variables.auxiliary]] +name = "is_equal" +type = "Bit" +desc = "Whether `rv1` and `arg2` are equal" + +[[variables.auxiliary]] +name = "branch_cond" +type = "Bit" +desc = "Whether a branch is taken, i.e., the branch condition" + +# 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], "mp_selector"], + ["*", ["^", 2, 6], "muldiv_selector"], + ["*", ["^", 2, 7], "word_instruction"], + ["*", ["^", 2, 8], "ADD"], + ["*", ["^", 2, 9], "SUB"], + ["*", ["^", 2, 10], "SLT"], + ["*", ["^", 2, 11], "AND"], + ["*", ["^", 2, 12], "OR"], + ["*", ["^", 2, 13], "XOR"], + ["*", ["^", 2, 14], "SHIFT"], + ["*", ["^", 2, 15], "JALR"], + ["*", ["^", 2, 16], "BEQ"], + ["*", ["^", 2, 17], "BLT"], + ["*", ["^", 2, 18], "LOAD"], + ["*", ["^", 2, 19], "STORE"], + ["*", ["^", 2, 20], "MUL"], + ["*", ["^", 2, 21], "DIVREM"], + ["*", ["^", 2, 22], "ECALL"], + ["*", ["^", 2, 23], "EBREAK"], + ["*", ["^", 2, 24], "rs1"], + ["*", ["^", 2, 32], "rs2"], + ["*", ["^", 2, 40], "rd"], +] + + +[[assumptions]] +desc = "The flags are a one-hot vector in the decoding" +ref = "cpu:a:one-hot" + +[[assumptions]] +desc = "When `STORE + LOAD + BEQ + BLT = 0`, either `rs2 = 0` or `imm = 0` should be enforced by the decoding. This is needed for `arg2`." +ref = "cpu:a:arg2-multiplex" + +[[constraint_groups]] +name = "decode" + +[[constraints.decode]] +kind = "interaction" +tag = "DECODE" +input = ["pc", "imm", "packed_decode"] + + +[[constraint_groups]] +name = "range" +prefix = "R" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["write_register"] +ref = "cpu:c:range_write_register" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["memory_2bytes"] +ref = "cpu:c:range_memory_2bytes" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["memory_4bytes"] +ref = "cpu:c:range_memory_4bytes" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["memory_8bytes"] +ref = "cpu:c:range_memory_8bytes" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["c_kind_instruction"] +ref = "cpu:c:range_c_kind_instruction" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["mp_selector"] +ref = "cpu:c:range_mp_selector" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["muldiv_selector"] +ref = "cpu:c:range_muldiv_selector" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["word_instruction"] +ref = "cpu:c:range_word_instruction" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["ADD"] +ref = "cpu:c:range_ADD" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["SUB"] +ref = "cpu:c:range_SUB" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["SLT"] +ref = "cpu:c:range_SLT" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["AND"] +ref = "cpu:c:range_AND" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["OR"] +ref = "cpu:c:range_OR" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["XOR"] +ref = "cpu:c:range_XOR" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["SHIFT"] +ref = "cpu:c:range_SHIFT" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["JALR"] +ref = "cpu:c:range_JALR" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["BEQ"] +ref = "cpu:c:range_BEQ" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["BLT"] +ref = "cpu:c:range_BLT" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["LOAD"] +ref = "cpu:c:range_LOAD" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["STORE"] +ref = "cpu:c:range_STORE" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["MUL"] +ref = "cpu:c:range_MUL" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["DIVREM"] +ref = "cpu:c:range_DIVREM" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["ECALL"] +ref = "cpu:c:range_ECALL" + +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["EBREAK"] +ref = "cpu:c:range_EBREAK" + +[[constraints.range]] +kind = "interaction" +tag = "IS_BYTE" +input = ["rs1"] + +[[constraints.range]] +kind = "interaction" +tag = "IS_BYTE" +input = ["rs2"] + +[[constraints.range]] +kind = "interaction" +tag = "IS_BYTE" +input = ["rd"] + + +[[constraint_groups]] +name = "alu" +prefix = "A" + +[[constraints.alu]] +kind = "template" +tag = "ADD" +cond = ["+", "ADD", "LOAD", "STORE"] +input = [["cast", "arg1", "DWordWL"], ["cast", "arg2", "DWordWL"]] +output = ["cast", "res", "DWordWL"] + +[[constraints.alu]] +kind = "template" +tag = "SUB" +cond = ["+", "SUB", "BEQ"] +input = [["cast", "arg1", "DWordWL"], ["cast", "arg2", "DWordWL"]] +output = ["cast", "res", "DWordWL"] +ref = "cpu:c:sub" + +[[constraints.alu]] +kind = "interaction" +tag = "LT" +input = [["cast", "arg1", "DWordHHW"], ["cast", "arg2", "DWordHHW"], "signed"] +output = ["idx", "res", 0] +multiplicity = ["+", "SLT", "BLT"] + +[[constraints.alu]] +kind = "arith" +constraint = "$#`SLT` + #`BLT` => #`res[i]` = 0$" +poly = ["*", ["+", "SLT", "BLT"], ["idx", "res", "i"]] +range = ["i", 1, 7] + +[[constraints.alu]] +kind = "interaction" +tag = "AND_BYTE" +input = [["idx", "arg1", "i"], ["idx", "arg2", "i"]] +output = ["idx", "res", "i"] +multiplicity = "AND" +range = ["i", 0, 7] + +[[constraints.alu]] +kind = "interaction" +tag = "OR_BYTE" +input = [["idx", "arg1", "i"], ["idx", "arg2", "i"]] +output = ["idx", "res", "i"] +multiplicity = "OR" +range = ["i", 0, 7] + +[[constraints.alu]] +kind = "interaction" +tag = "XOR_BYTE" +input = [["idx", "arg1", "i"], ["idx", "arg2", "i"]] +output = ["idx", "res", "i"] +multiplicity = "XOR" +range = ["i", 0, 7] + +[[constraints.alu]] +kind = "interaction" +tag = "SHIFT" +input = [["cast", "arg1", "DWordHL"], ["idx", "arg2", 0], "mp_selector", "signed"] +output = ["cast", "res", "DWordHL"] +multiplicity = "SHIFT" + +[[constraints.alu]] +kind = "template" +tag = "ADD" +input = ["pc", ["cast", ["+", ["*", 2, "c_type_instruction"], ["*", 4, ["not", "c_type_instruction"]]], "DWordWL"]] +output = ["cast", "DWordWL", "res"] +cond = "JALR" + +# TODO: no types available, so no casting yet +[[constraints.alu]] +kind = "interaction" +tag = "MUL" +input = ["arg1", "signed", "arg2", "mp_selector", "muldiv_selector"] +output = "res" +multiplicity = "MUL" + +# TODO: no types available, so no casting yet +[[constraints.alu]] +kind = "interaction" +tag = "DVRM" +input = ["arg1", "arg2", "signed", "muldiv_selector"] +output = "res" +multiplicity = "DIVREM" + + +[[constraint_groups]] +name = "mem" +prefix = "M" + +# TODO: no types available, so no casting yet +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [1, ["*", 2, "rs1"], "rv1", ["+", "timestamp", 0], 1, 0, 0] +output = "rv1" + +# TODO: no types available, so no casting yet +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [1, ["*", 2, "rs2"], "rv2", ["+", "timestamp", 1], 1, 0, 0] +output = "rv2" + +# TODO: no types available, so no casting yet +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [1, ["*", 2, "rd"], "rvd", ["+", "timestamp", 2], 1, 0, 0] + +# TODO: no types available, so no casting yet +[[constraints.mem]] +kind = "interaction" +tag = "LOAD" +input = [0, "res", ["+", "timestamp", 0], "memory_2bytes", "memory_4bytes", "memory_8bytes", "signed"] +output = "rvd" +multiplicity = "LOAD" + +# TODO: no types available, so no casting yet +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [0, "res", "rv2", ["+", "timestamp", 1], "memory_2bytes", "memory_4bytes", "memory_8bytes"] +multiplicity = "STORE" + +# TODO: no types available, so no casting yet +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [1, ["*", 2, 255], "next_pc", ["+", "timestamp", 1], 1, 0, 0] +output = "pc" + + +[[constraint_groups]] +name = "sys" +prefix = "S" + +[[constraints.sys]] +kind = "arith" +constraint = "`!EBREAK`" +desc = "We treat `EBREAK` as an unprovable trap" +poly = ["not", "EBREAK"] + +# TODO: no types available, so no casting yet +[[constraints.sys]] +kind = "interaction" +tag = "ECALL" +input = ["rv1", "pc", "timestamp", "rv2"] +output = "rvd" +multiplicity = "ECALL" + + +[[constraint_groups]] +name = "ext" +prefix = "E" + +[[constraints.ext]] +kind = "arith" +constraint = "$(#`rv1_sign_bit` or #`arg2_sign_bit` or #`res_sign_bit`) => #`word_instruction`$" +poly = ["*", ["+", "rv1_sign_bit", "arg2_sign_bit", "res_sign_bit"], ["not", "word_instruction"]] + +[[constraints.ext]] +kind = "interaction" +tag = "MSB16" +input = [["idx", "rv1", 1]] +output = "rv1_sign_bit" +multiplicity = "word_instruction" + +[[constraints.ext]] +kind = "arith" +constraint = "$#`arg1[:4]` = #`rv1[:2]`$" +poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 0], ["idx", ["cast", "rv1", "DWordWL"], 0]] + +[[constraints.ext]] +kind = "arith" +constraint = "$#`arg1[4:]` = #`rv1[2]` dot (1 - #`word_instruction`) + (2^(32) - 1) dot #`rv1_sign_bit` dot #`signed`$" +poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 1], ["*", ["not", "word_instruction"], ["idx", "rv1", 2]], ["*", "signed", "rv1_sign_bit", ["-", ["^", 2, 32], 1]]] + +[[constraints.ext]] +kind = "interaction" +tag = "MSB16" +input = [["idx", "rv2", 1]] +output = "arg2_sign_bit" +multiplicity = "word_instruction" + +[[constraints.ext]] +kind = "arith" +constraint = "$#`arg2[:4]` = (1 - #`STORE` - #`LOAD`) dot #`rv2[:2]` + (1 - #`BEQ` - #`BLT`) dot #`imm[0]`$" +poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 0], ["*", ["-", 1, "STORE", "LOAD"], ["idx", ["cast", "rv2", "DWordWL"], 0]], ["*", ["-", 1, "BEQ", "BLT"], ["idx", "imm", 0]]] + +[[constraints.ext]] +kind = "arith" +constraint = "$#`arg2[4:]` = (1 - #`STORE` - #`LOAD`) dot ((1 - #`word_instruction`) dot #`rv2[2]` + #`signed` dot #`arg2_sign_bit` dot (2^(32) - 1)) + (1 - #`BEQ` - #`BLT`) dot #`imm[1]`$" +poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 1], ["*", ["-", 1, "STORE", "LOAD"], ["not", "word_instruction"], ["idx", "rv2", 2]], ["*", ["-", 1, "STORE", "LOAD"], "signed", "arg2_sign_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT"], ["idx", "imm", 1]]] + +[[constraints.ext]] +kind = "interaction" +tag = "MSB8" +input = [["idx", "res", 3]] +output = "res_sign_bit" +multiplicity = "word_instruction" + +[[constraints.ext]] +kind = "arith" +constraint = "$#`!LOAD` => #`rvd[0]` = #`res[:4]`$" +poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 0], ["idx", ["cast", "res", "DWordWL"], 0]]] + +[[constraints.ext]] +kind = "arith" +constraint = "$#`!LOAD` => #`rvd[1]` = (1 - #`word_instruction`) dot #`res[4:]` + #`res_sign_bit` dot (2^(32) - 1)$" +desc = "_Sign_ extend the output if it wasn't a `LOAD`. Only `LOAD` has both `write_register = 1` and `rvd ≠ res`. `LOAD` and `word_instruction` are disjoint" +poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 1], ["*", ["not", "word_instruction"], ["idx", ["cast", "res", "DWordWL"], 1]], ["*", "res_sign_bit", ["-", ["^", 2, 32], 1]]]] + + + +[[constraint_groups]] +name = "misc" +prefix = "O" + +[[constraints.misc]] +kind = "interaction" +tag = "ZERO" +input = [["+", ["idx", "res", 0], ["idx", "res", 1], ["idx", "res", 2], ["idx", "res", 3], ["idx", "res", 4], ["idx", "res", 5], ["idx", "res", 6], ["idx", "res", 7]]] +output = "is_equal" +multiplicity = "BEQ" +ref = "cpu:c:is_equal" + +[[constraints.misc]] +kind = "arith" +constraint = "$#`branch_cond` = #`JALR` or (#`BLT` and (#`res` xor #`invert`)) or (#`BEQ` and (#`is_equal` xor #`invert`))$" +desc = "where `invert` is represented by `mp_selector`" +poly = ["+", + ["-", "branch_cond"], + "JALR", + ["*", ["idx", "res", 0], ["not", "mp_selector"], "BLT"], + ["*", ["not", ["idx", "res", 0]], "mp_selector", "BLT"], + ["*", "is_equal", ["not", "mp_selector"], "BEQ"], + ["*", ["not", "is_equal"], "mp_selector", "BEQ"] + ] + +[[constraints.misc]] +kind = "interaction" +tag = "BRANCH" +input = ["pc", ["idx", "imm", 0], ["cast", "arg1", "DWordWL"], "JALR"] +output = "next_pc" +multiplicity = "branch_cond" + +[[constraints.misc]] +kind = "template" +tag = "ADD" +input = ["pc", ["cast", ["+", ["*", 2, "c_type_instruction"], ["*", 4, ["not", "c_type_instruction"]]], "DWordWL"]] +output = "next_pc" +desc = "Increment `pc` to `next_pc` if we're not branching" From 718b5f057488b0f1333c301ade800baed187152c Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Wed, 31 Dec 2025 12:25:48 +0100 Subject: [PATCH 2/4] Update spec/cpu.typ Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/cpu.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/cpu.typ b/spec/cpu.typ index 09b8c00ad..56fa02129 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -69,7 +69,7 @@ The interactions with the wider system. === Input and output to the ALU -We constraint `arg1`, `arg2` and `rvd` to correspond to the wanted values, +We constrain `arg1`, `arg2` and `rvd` to correspond to the wanted values, including the appropriate sign/zero extension, depending on `word_instruction`. #render_constraint_table(chip, config, groups: "ext") From 95c5fa4459864af1f68c1b6af06566f6ed26cd8d Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Wed, 31 Dec 2025 13:11:13 +0100 Subject: [PATCH 3/4] Address review comments --- spec/cpu.typ | 2 +- spec/src/cpu.toml | 109 +++++++++++++++++++++++++++++----------------- 2 files changed, 71 insertions(+), 40 deletions(-) diff --git a/spec/cpu.typ b/spec/cpu.typ index 56fa02129..00a33f5a2 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -70,7 +70,7 @@ The interactions with the wider system. === Input and output to the ALU We constrain `arg1`, `arg2` and `rvd` to correspond to the wanted values, -including the appropriate sign/zero extension, depending on `word_instruction`. +including the appropriate sign/zero extension, depending on `word_instr`. #render_constraint_table(chip, config, groups: "ext") diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 8f4074cd2..ebf14a002 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -57,18 +57,24 @@ type = "Bit" desc = "Whether the instruction is of C type, i.e., whether it is 2 bytes long instead of 4" # 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_instruction?) +# TODO: make sure decode correctly extends this (may be zero for unsigned and word_instr?) [[variables.input]] name = "imm" type = "DWordWL" desc = "The fully extended 64-bit version of the immediate" +[[variables.input]] +name = "signed" +type = "Bit" +desc = "Indicates whether we're dealing with a signed or unsigned instruction" + [[variables.input]] 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 flag for inverting the condition of conditional branches (see `branch_cond`) + - as direction (left or right) for `SHIFT`""" [[variables.input]] name = "muldiv_selector" @@ -76,7 +82,7 @@ type = "Bit" desc = "Selects which output of `MUL` (lo/hi) or `DIV` (quo/rem) is wanted" [[variables.input]] -name = "word_instruction" +name = "word_instr" type = "Bit" desc = "Whether the instruction is a \\*W instruction, requiring the inputs and outputs to be (sign) extended" @@ -234,28 +240,29 @@ poly = ["+", ["*", ["^", 2, 2], "memory_4bytes"], ["*", ["^", 2, 3], "memory_8bytes"], ["*", ["^", 2, 4], "c_type_instruction"], - ["*", ["^", 2, 5], "mp_selector"], - ["*", ["^", 2, 6], "muldiv_selector"], - ["*", ["^", 2, 7], "word_instruction"], - ["*", ["^", 2, 8], "ADD"], - ["*", ["^", 2, 9], "SUB"], - ["*", ["^", 2, 10], "SLT"], - ["*", ["^", 2, 11], "AND"], - ["*", ["^", 2, 12], "OR"], - ["*", ["^", 2, 13], "XOR"], - ["*", ["^", 2, 14], "SHIFT"], - ["*", ["^", 2, 15], "JALR"], - ["*", ["^", 2, 16], "BEQ"], - ["*", ["^", 2, 17], "BLT"], - ["*", ["^", 2, 18], "LOAD"], - ["*", ["^", 2, 19], "STORE"], - ["*", ["^", 2, 20], "MUL"], - ["*", ["^", 2, 21], "DIVREM"], - ["*", ["^", 2, 22], "ECALL"], - ["*", ["^", 2, 23], "EBREAK"], - ["*", ["^", 2, 24], "rs1"], - ["*", ["^", 2, 32], "rs2"], - ["*", ["^", 2, 40], "rd"], + ["*", ["^", 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"], ] @@ -310,6 +317,12 @@ tag = "IS_BIT" input = ["c_kind_instruction"] ref = "cpu:c:range_c_kind_instruction" +[[constraints.range]] +kind = "template" +tag = "IS_BIT" +input = ["signed"] +ref = "cpu:c:range_signed" + [[constraints.range]] kind = "template" tag = "IS_BIT" @@ -325,8 +338,8 @@ ref = "cpu:c:range_muldiv_selector" [[constraints.range]] kind = "template" tag = "IS_BIT" -input = ["word_instruction"] -ref = "cpu:c:range_word_instruction" +input = ["word_instr"] +ref = "cpu:c:range_word_instr" [[constraints.range]] kind = "template" @@ -439,6 +452,24 @@ kind = "interaction" tag = "IS_BYTE" input = ["rd"] +[[constraints.range]] +kind = "interaction" +tag = "IS_BYTE" +input = [["idx", "arg1", "i"]] +range = ["i", 0, 7] + +[[constraints.range]] +kind = "interaction" +tag = "IS_BYTE" +input = [["idx", "arg2", "i"]] +range = ["i", 0, 7] + +[[constraints.range]] +kind = "interaction" +tag = "IS_BYTE" +input = [["idx", "res", "i"]] +range = ["i", 0, 7] + [[constraint_groups]] name = "alu" @@ -599,15 +630,15 @@ prefix = "E" [[constraints.ext]] kind = "arith" -constraint = "$(#`rv1_sign_bit` or #`arg2_sign_bit` or #`res_sign_bit`) => #`word_instruction`$" -poly = ["*", ["+", "rv1_sign_bit", "arg2_sign_bit", "res_sign_bit"], ["not", "word_instruction"]] +constraint = "$(#`rv1_sign_bit` or #`arg2_sign_bit` or #`res_sign_bit`) => #`word_instr`$" +poly = ["*", ["+", "rv1_sign_bit", "arg2_sign_bit", "res_sign_bit"], ["not", "word_instr"]] [[constraints.ext]] kind = "interaction" tag = "MSB16" input = [["idx", "rv1", 1]] output = "rv1_sign_bit" -multiplicity = "word_instruction" +multiplicity = "word_instr" [[constraints.ext]] kind = "arith" @@ -616,15 +647,15 @@ poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 0], ["idx", ["cast", "rv1", "D [[constraints.ext]] kind = "arith" -constraint = "$#`arg1[4:]` = #`rv1[2]` dot (1 - #`word_instruction`) + (2^(32) - 1) dot #`rv1_sign_bit` dot #`signed`$" -poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 1], ["*", ["not", "word_instruction"], ["idx", "rv1", 2]], ["*", "signed", "rv1_sign_bit", ["-", ["^", 2, 32], 1]]] +constraint = "$#`arg1[4:]` = #`rv1[2]` dot (1 - #`word_instr`) + (2^(32) - 1) dot #`rv1_sign_bit` dot #`signed`$" +poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 1], ["*", ["not", "word_instr"], ["idx", "rv1", 2]], ["*", "signed", "rv1_sign_bit", ["-", ["^", 2, 32], 1]]] [[constraints.ext]] kind = "interaction" tag = "MSB16" input = [["idx", "rv2", 1]] output = "arg2_sign_bit" -multiplicity = "word_instruction" +multiplicity = "word_instr" [[constraints.ext]] kind = "arith" @@ -633,15 +664,15 @@ poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 0], ["*", ["-", 1, "STORE", "L [[constraints.ext]] kind = "arith" -constraint = "$#`arg2[4:]` = (1 - #`STORE` - #`LOAD`) dot ((1 - #`word_instruction`) dot #`rv2[2]` + #`signed` dot #`arg2_sign_bit` dot (2^(32) - 1)) + (1 - #`BEQ` - #`BLT`) dot #`imm[1]`$" -poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 1], ["*", ["-", 1, "STORE", "LOAD"], ["not", "word_instruction"], ["idx", "rv2", 2]], ["*", ["-", 1, "STORE", "LOAD"], "signed", "arg2_sign_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT"], ["idx", "imm", 1]]] +constraint = "$#`arg2[4:]` = (1 - #`STORE` - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[2]` + #`signed` dot #`arg2_sign_bit` dot (2^(32) - 1)) + (1 - #`BEQ` - #`BLT`) dot #`imm[1]`$" +poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 1], ["*", ["-", 1, "STORE", "LOAD"], ["not", "word_instr"], ["idx", "rv2", 2]], ["*", ["-", 1, "STORE", "LOAD"], "signed", "arg2_sign_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT"], ["idx", "imm", 1]]] [[constraints.ext]] kind = "interaction" tag = "MSB8" input = [["idx", "res", 3]] output = "res_sign_bit" -multiplicity = "word_instruction" +multiplicity = "word_instr" [[constraints.ext]] kind = "arith" @@ -650,9 +681,9 @@ poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 0], ["idx", ["cast", "res", " [[constraints.ext]] kind = "arith" -constraint = "$#`!LOAD` => #`rvd[1]` = (1 - #`word_instruction`) dot #`res[4:]` + #`res_sign_bit` dot (2^(32) - 1)$" -desc = "_Sign_ extend the output if it wasn't a `LOAD`. Only `LOAD` has both `write_register = 1` and `rvd ≠ res`. `LOAD` and `word_instruction` are disjoint" -poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 1], ["*", ["not", "word_instruction"], ["idx", ["cast", "res", "DWordWL"], 1]], ["*", "res_sign_bit", ["-", ["^", 2, 32], 1]]]] +constraint = "$#`!LOAD` => #`rvd[1]` = (1 - #`word_instr`) dot #`res[4:]` + #`res_sign_bit` dot (2^(32) - 1)$" +desc = "_Sign_ extend the output if it wasn't a `LOAD`. Only `LOAD` has both `write_register = 1` and `rvd ≠ res`. `LOAD` and `word_instr` are disjoint" +poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 1], ["*", ["not", "word_instr"], ["idx", ["cast", "res", "DWordWL"], 1]], ["*", "res_sign_bit", ["-", ["^", 2, 32], 1]]]] From 0178f7a1443135644e81540633934c7765da0377 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 5 Jan 2026 11:20:11 +0100 Subject: [PATCH 4/4] Add word_instr as input to SHIFT --- spec/src/cpu.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index ebf14a002..562a657d0 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -530,7 +530,7 @@ range = ["i", 0, 7] [[constraints.alu]] kind = "interaction" tag = "SHIFT" -input = [["cast", "arg1", "DWordHL"], ["idx", "arg2", 0], "mp_selector", "signed"] +input = [["cast", "arg1", "DWordHL"], ["idx", "arg2", 0], "mp_selector", "signed", "word_instr"] output = ["cast", "res", "DWordHL"] multiplicity = "SHIFT"