spec: Inline PC memory access into CPU

Author: RobinJadoul

spec/cpu.typ

@@ -60,9 +60,12 @@ The ALU functionality is then obtained through judicious dispatching to the corr
 
 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 `pc` register behaves very predictably with respect to its timestamps and when it is being read,
+so for performance reasons, we inline its memory interactions directly into the #cpu chip.
 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.
+#rj[We can try to do a bit more, and move `double_pc_read` into decoding, so that `AUIPC` could set `read_register1 = 0`.]
 
 #render_constraint_table(chip, config, groups: "mem")
 

spec/src/cpu.toml

@@ -221,6 +221,18 @@ desc = "The value to (maybe) be written back to rvd"
 pad = 0
 
 # Auxiliary
+[[variables.auxiliary]]
+name = "prev_pc_timestamp_borrow"
+type = "Bit"
+desc = "The borrow bit for computing the previous timestamp the PC was accessed"
+pad = 0
+
+[[variables.auxiliary]]
+name = "pc_double_read"
+type = "Bit"
+desc = "Whether the PC is being read as a general purpose register (rs1) this cycle"
+pad = 0
+
 [[variables.auxiliary]]
 name = "rv1"
 type = "DWordWHH"
@@ -691,12 +703,39 @@ tag = "MEMW"
 input = [0, ["cast", "res", "DWordWL"], ["cast", "arg2", ["Byte", 8]], ["+", "timestamp", ["cast", 1, "DWordWL"]], "memory_2bytes", "memory_4bytes", "memory_8bytes"]
 multiplicity = "STORE"
 
+[[constraints.mem]]
+kind = "arith"
+constraint = "$#`pc_double_read` => #`rs1` = 255$"
+poly = ["*", ["-", 1, "pc_double_read"], ["-", "rs1", 255]]
+
+[[constraints.mem]]
+kind = "template"
+tag = "IS_BIT"
+input = ["pc_double_read"]
+
+[[constraints.mem]]
+kind = "template"
+tag = "IS_BIT"
+input = ["prev_pc_timestamp_borrow"]
+
+[[constraints.mem]]
+kind = "arith"
+constraint = "$#`pc_double_read` => #`prev_pc_timestamp_borrow` = 0$"
+poly = ["*", ["-", 1, "pc_double_read"], "prev_pc_timestamp_borrow"]
+
 [[constraints.mem]]
 kind = "interaction"
-tag = "MEMW"
-input = [1, ["cast", ["*", 2, 255], "DWordWL"], ["arr", ["idx", "next_pc", 0], ["idx", "next_pc", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0]
-output = ["arr", ["idx", "pc", 0], ["idx", "pc", 1], 0, 0, 0, 0, 0, 0]
+tag = "memory"
+input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["arr", ["+", ["-", ["idx", "timestamp", 0], ["*", 3, ["not", "pc_double_read"]]], ["*", ["^", 2, 32], "prev_pc_timestamp_borrow"]], ["-", ["idx", "timestamp", 1], "prev_pc_timestamp_borrow"]], ["idx", "pc", "i"]]
 multiplicity = ["not", "pad"]
+iter = ["i", 0, 1]
+
+[[constraints.mem]]
+kind = "interaction"
+tag = "memory"
+input = [1, ["arr", ["+", ["*", 2, 255], "i"], 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], ["idx", "next_pc", "i"]]
+multiplicity = ["-", ["not", "pad"]]
+iter = ["i", 0, 1]
 
 
 [[constraint_groups]]