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..d01e9fa03 --- /dev/null +++ b/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") + diff --git a/spec/src/branch.toml b/spec/src/branch.toml new file mode 100644 index 000000000..b93639602 --- /dev/null +++ b/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`" + + + +[[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 = "-μ"