spec: BRANCH chip

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]
   ]
 )
 

spec/branch.typ

@@ -0,0 +1,38 @@
+#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/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)
+
+== 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` 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.
+#render_constraint_table(chip, config, groups: "output")
+

spec/src/branch.toml

@@ -0,0 +1,140 @@
+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"
+
+[[variables.output]]
+name = "next_pc_low"
+type = ["Byte", 2]
+desc = "The lower part of the next pc"
+
+
+# Auxiliary
+
+[[variables.auxiliary]]
+name = "unmasked_low_byte"
+type = "Byte"
+desc = "The low byte of the next pc, before masking the LSB. Used to constraint the raw addition."
+
+
+# Virtual
+
+[[variables.virtual]]
+name = "next_pc_unmasked"
+type = "DWordWL"
+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
+
+[[variables.multiplicity]]
+name = "μ"
+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<JALR>`"
+
+
+
+[[constraint_groups]]
+name = "all"
+
+[[constraints.all]]
+kind = "template"
+tag = "ADD"
+input = ["pc", ["cast", "offset", "DWordWL"]]
+output = "next_pc_unmasked"
+cond = ["not", "JALR"]
+
+[[constraints.all]]
+kind = "template"
+tag = "ADD"
+input = ["register", ["cast", "offset", "DWordWL"]]
+output = "next_pc_unmasked"
+cond = "JALR"
+
+[[constraints.all]]
+kind = "interaction"
+tag = "IS_BYTE"
+input = [["idx", "next_pc_low", 1]]
+multiplicity = "μ"
+
+[[constraints.all]]
+kind = "interaction"
+tag = "AND_BYTE"
+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 = "μ"
+
+
+[[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 = "next_pc"
+multiplicity = "-μ"