From d0aadb36969367d56150d9808e53295723c4045a Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 24 Dec 2025 15:04:30 +0100 Subject: [PATCH 1/4] spec: init BRANCH chip --- spec/book.typ | 1 + spec/branch.typ | 30 ++++++++++++ spec/src/branch.toml | 110 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 141 insertions(+) create mode 100644 spec/branch.typ create mode 100644 spec/src/branch.toml diff --git a/spec/book.typ b/spec/book.typ index c4c3a8c6d..af747c88c 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("cpu.typ")[CPU chip] + #chapter("branch.typ")[BRANCH] ] ) diff --git a/spec/branch.typ b/spec/branch.typ new file mode 100644 index 000000000..94a330d47 --- /dev/null +++ b/spec/branch.typ @@ -0,0 +1,30 @@ +#import "/book.typ": book-page +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_column_table, + total_nr_variables, + total_nr_instantiated_columns, + render_constraint_table, +) + +#let config = load_config() +#let chip = load_chip("src/branch.toml", config) + +#show: book-page.with(title: "BRANCH chip") + +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The `BRANCH` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_column_table(chip, config) + +== Constraints + +We constrain `next_pc` to be `base_address + offset`, +where `base_address` is `pc` when `JALR = 0` and `register` otherwise. +#render_constraint_table(chip, config, groups: "all") + +This chip contributes the following to the lookup argument. +#render_constraint_table(chip, config, groups: "output") + diff --git a/spec/src/branch.toml b/spec/src/branch.toml new file mode 100644 index 000000000..8df09cf16 --- /dev/null +++ b/spec/src/branch.toml @@ -0,0 +1,110 @@ +name = "BRANCH" + + +# Input + +[[variables.input]] +name = "pc" +type = "DWordWL" +desc = "The current pc, used as base address when `!JALR`" + +[[variables.input]] +name = "offset" +type = "Word" +desc = "The offset from the base address to jump to" + +[[variables.input]] +name = "register" +type = "DWordWL" +desc = "The base address to use when `JALR`" + +[[variables.input]] +name = "JALR" +type = "Bit" +desc = "Selects between `pc` and `register` as base address, needed for the `JALR` instruction" + + +# Output + +[[variables.output]] +name = "next_pc_high" +type = "Half[3]" +desc = "The upper part of the next pc" + + +# Auxiliary + +[[variables.auxiliary]] +name = "raw_add_low" +type = "Byte[2]" +desc = "The low part of the raw addition" + +[[variables.auxiliary]] +name = "masked_add_low" +type = "Byte" +desc = "The low part of `raw_add_low`, with it's LSB cleared" + + +# Virtual + +[[variables.virtual]] +name = "add_result" +type = "DWordWL" +desc = "The combination of `next_pc_high` and `raw_add_low` to constrain the addition" +polys = [ + ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 0]], ["*", ["^", 2, 8], ["idx", "raw_add_low", 1]], ["idx", "raw_add_low", 0]], + ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 2]], ["idx", "next_pc_high", 1]], +] + + +# Multiplicity + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" + + + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "template" +tag = "ADD" +input = ["pc", "offset"] # TODO: offset should be "extended" to DWord +output = "add_result" +cond = ["not", "JALR"] + +[[constraints.all]] +kind = "template" +tag = "ADD" +input = ["register", "offset"] # TODO: offset should still be extended +output = "add_result" +cond = "JALR" + +[[constraints.all]] +kind = "interaction" +tag = "IS_BYTE" +input = [["idx", "raw_add_low", "i"]] +range = ["i", 0, 1] +multiplicity = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "AND_BYTE" +input = [["idx", "raw_add_low", 0]] +output = "masked_add_low" +multiplicity = "μ" + + +[[constraint_groups]] +name = "output" +desc = "Each row contributes the following to the LogUp sum" + +[[constraints.output]] +kind = "interaction" +tag = "BRANCH" +input = ["pc", "offset", "register", "JALR"] +output = ["+", ["*", ["^", 2, 16], "next_pc_high"], ["*", ["^", 2, 8], ["idx", "raw_add_low", 1]], "masked_add_low"] # TODO: cleanup +multiplicity = "-μ" From df7f0b591f796b850dfbd5189ab85b21b98ff6dd Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 2 Jan 2026 12:51:29 +0100 Subject: [PATCH 2/4] Small cleanup --- spec/branch.typ | 3 ++- spec/src/branch.toml | 11 ++++++----- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/spec/branch.typ b/spec/branch.typ index 94a330d47..8789a60f2 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page +#import "/book.typ": book-page, rj #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_column_table, @@ -21,6 +21,7 @@ The `BRANCH` chip is comprised of #nr_variables variables that are expressed usi == Constraints +#rj[Check correspondence with CPU for passing in `offset` as word or dword] We constrain `next_pc` to be `base_address + offset`, where `base_address` is `pc` when `JALR = 0` and `register` otherwise. #render_constraint_table(chip, config, groups: "all") diff --git a/spec/src/branch.toml b/spec/src/branch.toml index 8df09cf16..07be672d0 100644 --- a/spec/src/branch.toml +++ b/spec/src/branch.toml @@ -28,7 +28,7 @@ desc = "Selects between `pc` and `register` as base address, needed for the `JAL [[variables.output]] name = "next_pc_high" -type = "Half[3]" +type = ["Half", 3] desc = "The upper part of the next pc" @@ -36,7 +36,7 @@ desc = "The upper part of the next pc" [[variables.auxiliary]] name = "raw_add_low" -type = "Byte[2]" +type = ["Byte", 2] desc = "The low part of the raw addition" [[variables.auxiliary]] @@ -72,14 +72,14 @@ name = "all" [[constraints.all]] kind = "template" tag = "ADD" -input = ["pc", "offset"] # TODO: offset should be "extended" to DWord +input = ["pc", ["cast", "offset", "DWordWL"]] output = "add_result" cond = ["not", "JALR"] [[constraints.all]] kind = "template" tag = "ADD" -input = ["register", "offset"] # TODO: offset should still be extended +input = ["register", ["cast", "offset", "DWordWL"]] output = "add_result" cond = "JALR" @@ -106,5 +106,6 @@ desc = "Each row contributes the following to the LogUp sum" kind = "interaction" tag = "BRANCH" input = ["pc", "offset", "register", "JALR"] -output = ["+", ["*", ["^", 2, 16], "next_pc_high"], ["*", ["^", 2, 8], ["idx", "raw_add_low", 1]], "masked_add_low"] # TODO: cleanup +# TODO? Update with summation notation once it lands +output = ["+", ["*", ["^", 2, 48], ["idx", "next_pc_high", 2]], ["*", ["^", 2, 32], ["idx", "next_pc_high", 1]], ["*", ["^", 2, 16], ["idx", "next_pc_high", 0]], ["*", ["^", 2, 8], ["idx", "raw_add_low", 1]], "masked_add_low"] multiplicity = "-μ" From e68335e1210cd8f705289e8db799b0e5ed117bcc Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 2 Jan 2026 17:20:03 +0100 Subject: [PATCH 3/4] Clean up variable naming and generally address review comments --- spec/branch.typ | 11 +++++-- spec/src/branch.toml | 70 +++++++++++++++++++++++++++++++------------- 2 files changed, 59 insertions(+), 22 deletions(-) diff --git a/spec/branch.typ b/spec/branch.typ index 8789a60f2..d01e9fa03 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -1,6 +1,7 @@ #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, @@ -19,11 +20,17 @@ The `BRANCH` 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 #rj[Check correspondence with CPU for passing in `offset` as word or dword] -We constrain `next_pc` to be `base_address + offset`, -where `base_address` is `pc` when `JALR = 0` and `register` otherwise. +We constrain `next_pc` to be $#`base_address` + #`offset`$, +where `base_address` equals `pc` when $#`JALR` = 0$ and `register` otherwise. + +The range checks on `unmasked_low_byte` and `next_pc_low[0]` are performed implicitly by the `AND_BYTE` lookup. #render_constraint_table(chip, config, groups: "all") This chip contributes the following to the lookup argument. diff --git a/spec/src/branch.toml b/spec/src/branch.toml index 07be672d0..8966f3bc2 100644 --- a/spec/src/branch.toml +++ b/spec/src/branch.toml @@ -31,30 +31,39 @@ name = "next_pc_high" type = ["Half", 3] desc = "The upper part of the next pc" +[[variables.output]] +name = "next_pc_low" +type = ["Byte", 2] +desc = "The lower part of the next pc" -# Auxiliary -[[variables.auxiliary]] -name = "raw_add_low" -type = ["Byte", 2] -desc = "The low part of the raw addition" +# Auxiliary [[variables.auxiliary]] -name = "masked_add_low" +name = "unmasked_low_byte" type = "Byte" -desc = "The low part of `raw_add_low`, with it's LSB cleared" +desc = "The low byte of the next pc, before masking the LSB. Used to constraint the raw addition." # Virtual [[variables.virtual]] -name = "add_result" +name = "next_pc_unmasked" type = "DWordWL" -desc = "The combination of `next_pc_high` and `raw_add_low` to constrain the addition" -polys = [ - ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 0]], ["*", ["^", 2, 8], ["idx", "raw_add_low", 1]], ["idx", "raw_add_low", 0]], - ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 2]], ["idx", "next_pc_high", 1]], -] +desc = "The combination of `next_pc_high`, `next_pc_low[1]` and `unmasked_low_byte` to constrain the addition. This is the computed value for the next pc, before masking off the LSB as required by the ISA." +def = {idx = "i", polys = [ + {range = [0], poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 0]], ["*", ["^", 2, 8], ["idx", "next_pc_low", 1]], ["idx", "unmasked_low_byte", 0]]}, + {range = [1], poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 2]], ["idx", "next_pc_high", 1]]}, +]} + +[[variables.virtual]] +name = "next_pc" +type = "DWordWL" +desc = "The computed next pc, after masking off the LSB as required by the ISA." +def = {idx = "i", polys = [ + {range = [0], poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 0]], ["*", ["^", 2, 8], ["idx", "next_pc_low", 1]], ["idx", "next_pc_low", 0]]}, + {range = [1], poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 2]], ["idx", "next_pc_high", 1]]}, +]} # Multiplicity @@ -65,6 +74,21 @@ type = "Bit" desc = "" +[[assumptions]] +desc = "`pc` is range checked, `IS_WORD[pc[i]]`" +range = ["i", 0, 1] + +[[assumptions]] +desc = "`offset` is range checked, `IS_WORD[offset]`" + +[[assumptions]] +desc = "`register` is range checked, `IS_WORD[register[i]]`" +range = ["i", 0, 1] + +[[assumptions]] +desc = "`IS_BIT`" + + [[constraint_groups]] name = "all" @@ -73,28 +97,34 @@ name = "all" kind = "template" tag = "ADD" input = ["pc", ["cast", "offset", "DWordWL"]] -output = "add_result" +output = "next_pc_unmasked" cond = ["not", "JALR"] [[constraints.all]] kind = "template" tag = "ADD" input = ["register", ["cast", "offset", "DWordWL"]] -output = "add_result" +output = "next_pc_unmasked" cond = "JALR" [[constraints.all]] kind = "interaction" tag = "IS_BYTE" -input = [["idx", "raw_add_low", "i"]] -range = ["i", 0, 1] +input = [["idx", "next_pc_low", 1]] multiplicity = "μ" [[constraints.all]] kind = "interaction" tag = "AND_BYTE" -input = [["idx", "raw_add_low", 0]] -output = "masked_add_low" +input = [["idx", "unmasked_low_byte", 0], 254] +output = ["idx", "next_pc_low", 0] +multiplicity = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "IS_HALFWORD" +input = [["idx", "next_pc_high", "i"]] +range = ["i", 0, 2] multiplicity = "μ" @@ -107,5 +137,5 @@ kind = "interaction" tag = "BRANCH" input = ["pc", "offset", "register", "JALR"] # TODO? Update with summation notation once it lands -output = ["+", ["*", ["^", 2, 48], ["idx", "next_pc_high", 2]], ["*", ["^", 2, 32], ["idx", "next_pc_high", 1]], ["*", ["^", 2, 16], ["idx", "next_pc_high", 0]], ["*", ["^", 2, 8], ["idx", "raw_add_low", 1]], "masked_add_low"] +output = "next_pc" multiplicity = "-μ" From 60038a37545e65302210ab0a65c5285437dfdaaf Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 2 Jan 2026 17:21:42 +0100 Subject: [PATCH 4/4] outdated comment --- spec/src/branch.toml | 1 - 1 file changed, 1 deletion(-) diff --git a/spec/src/branch.toml b/spec/src/branch.toml index 8966f3bc2..b93639602 100644 --- a/spec/src/branch.toml +++ b/spec/src/branch.toml @@ -136,6 +136,5 @@ desc = "Each row contributes the following to the LogUp sum" kind = "interaction" tag = "BRANCH" input = ["pc", "offset", "register", "JALR"] -# TODO? Update with summation notation once it lands output = "next_pc" multiplicity = "-μ"