diff --git a/spec/book.typ b/spec/book.typ index 1bf944862..277e652b5 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -13,6 +13,7 @@ #chapter("branch.typ")[BRANCH] #chapter("lt.typ")[LT] #chapter("mul.typ")[MUL chip] + #chapter("load.typ")[LOAD chip] #chapter("bitwise.typ")[BITWISE] ] ) diff --git a/spec/load.typ b/spec/load.typ new file mode 100644 index 000000000..931611108 --- /dev/null +++ b/spec/load.typ @@ -0,0 +1,42 @@ +#import "/book.typ": book-page, rj +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_column_table, + render_chip_padding_table, + render_constraint_table, + total_nr_instantiated_columns, + total_nr_variables, +) + +#let config = load_config() +#let chip = load_chip("src/load.toml", config) + +#show: book-page.with(title: "LOAD chip") + +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The `LOAD` 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 +The chip delegates the actual memory interaction to the `MEMW` chip, +and ensures correctness of the requested sign/zero extension. +The output `res` is correctly range-checked as long as the memory contents are. + +#render_constraint_table(chip, config, groups: "all") + +The chip contributes the following to the lookup argument. + +#render_constraint_table(chip, config, groups: "output") + +== Padding + +The table can be padded to the next power of two with the following value assignments: + +#render_chip_padding_table(chip, config) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 747497d44..1bd46ac00 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -582,7 +582,6 @@ 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" diff --git a/spec/src/load.toml b/spec/src/load.toml new file mode 100644 index 000000000..fcbd2b87f --- /dev/null +++ b/spec/src/load.toml @@ -0,0 +1,160 @@ +name = "LOAD" + +# Input + +[[variables.input]] +name = "base_address" +type = "DWordWL" +desc = "The base address to read/write from/to, gets offset by $[0, 7]$, depending on how big the access is" +pad = 0 + +[[variables.input]] +name = "timestamp" +type = "DWordWL" +desc = "The timestamp at which this memory access is said to occur" +pad = 0 + +[[variables.input]] +name = "read2" +type = "Bit" +desc = "Whether to read exactly 2 bytes" +pad = 0 + +[[variables.input]] +name = "read4" +type = "Bit" +desc = "Whether to read exactly 4 bytes" +pad = 0 + +[[variables.input]] +name = "read8" +type = "Bit" +desc = "Whether to read exactly 8 bytes" +pad = 0 + +[[variables.input]] +name = "signed" +type = "Bit" +desc = "Whether to sign-extend (1) or zero-extend (0)" +pad = 0 + +# Output + +[[variables.output]] +name = "res" +type = "DWordBL" +desc = "The result of reading (up to) 8 bytes from `base_address`, extended corresponding to `signed`." +pad = 0 + +# Auxiliary + +[[variables.auxiliary]] +name = "sign_bit" +type = "Bit" +desc = "The sign bit extracted from the bytes retrieved from memory" +pad = 0 + +# Virtual + +[[variables.virtual]] +name = "read1" +type = "Bit" +desc = "Whether to read exactly 1 byte" +def = ["-", "μ", "read2", "read4", "read8"] + +# Multiplicity + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" +pad = 0 + + +[[assumptions]] +desc = "`IS_WORD[base_address[i]]`" +iter = ["i", 0, 1] + +[[assumptions]] +desc = "`IS_BIT`" + +[[assumptions]] +desc = "`IS_BIT`" + +[[assumptions]] +desc = "`IS_BIT`" + +[[assumptions]] +desc = "`IS_BIT`" + +[[assumptions]] +desc = "`IS_BIT`" + +[[assumptions]] +desc = "`IS_WORD[timestamp[i]]`" +iter = ["i", 0, 1] + + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "arith" +constraint = "$#`read2` + #`read4` + #`read8` => #`μ`$" +poly = ["*", ["+", "read2", "read4", "read8"], ["not", "μ"]] + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [0, "base_address", ["cast", "res", ["BaseField", 8]], "timestamp", "read2", "read4", "read8"] +output = "res" +multiplicity = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "MSB8" +input = [["idx", "res", 0]] +output = "sign_bit" +multiplicity = "read1" + +[[constraints.all]] +kind = "interaction" +tag = "MSB8" +input = [["idx", "res", 1]] +output = "sign_bit" +multiplicity = "read2" + +[[constraints.all]] +kind = "interaction" +tag = "MSB8" +input = [["idx", "res", 3]] +output = "sign_bit" +multiplicity = "read4" + +[[constraints.all]] +kind = "arith" +constraint = "$!#`read8` => #`res`_i = #`signed` dot #`sign_bit` dot 255$" +poly = ["*", ["not", "read8"], ["-", ["idx", "res", "i"], ["*", "signed", "sign_bit", 255]]] +iter = ["i", 4, 7] + +[[constraints.all]] +kind = "arith" +constraint = "$!(#`read4` + #`read8`) => #`res`_i = #`signed` dot #`sign_bit` dot 255$" +poly = ["*", ["-", 1, "read4", "read8"], ["-", ["idx", "res", "i"], ["*", "signed", "sign_bit", 255]]] +iter = ["i", 2, 3] + +[[constraints.all]] +kind = "arith" +constraint = "$!(#`read2` + #`read4` + #`read8`) => #`res`_1 = #`signed` dot #`sign_bit` dot 255$" +poly = ["*", ["-", 1, "read2", "read4", "read8"], ["-", ["idx", "res", 1], ["*", "signed", "sign_bit", 255]]] + + +[[constraint_groups]] +name = "output" + +[[constraints.output]] +kind = "interaction" +tag = "LOAD" +input = ["base_address", "timestamp", "read2", "read4", "read8"] +output = ["cast", "res", "DWordWL"] +multiplicity = ["-", "μ"]