Address review comments

Author: RobinJadoul

spec/cpu.typ

@@ -62,12 +62,13 @@ The interactions with the memory, both for register loading and storing, as for
 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.
+
+Potentially overlapping memory accesses are ensured to have disjoint timestamps.
 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.
-Constraints on `pc_double_read` corresponding to an `AUIPC` instruction are not necessary,
+to ensure the access is disjoint with the `pc` read into `rv1` as part of the `AUIPC` instruction (see @cpu:c:read_rv1 and @decode:decoding-overview).
+Constraints regarding whether `pc_double_read` corresponds to an `AUIPC` instruction are not necessary,
 as regardless of its value, the old timestamp is guaranteed smaller than the new timestamp,
-and the integrity of the memory argument therefor ensures the correctness of this bit.
+and the integrity of the memory argument therefore ensures the correctness of this bit.
 
 #render_constraint_table(chip, config, groups: "mem")
 

spec/decode.typ

@@ -39,7 +39,7 @@ Given that `CPU` asserts that `EBREAK = 0` (see @cpu:c:ebreak_traps), using this
 Note moreover that the `pc` is set to $7$.
 This value is the _smallest odd number_ (i.e., not reachable during regular execution) that is more than _$4$_ (i.e., the max `pc`-increment) greater than _$1$_ (i.e., the `pc`-value used in the #link(<cpu-padding-decode-row>)[additional instruction] referred to by `CPU`-padding lines).
 
-= Decoding
+= Decoding<decode:decoding-overview>
 For the purposes of explaining decoding, we decompress #decode's `packed_decode` variable into its constituent variables.
 Note that the below table is _not_ used in practice: it is solely used for the purposes of this explanation.
 
@@ -64,12 +64,6 @@ For the purpose of brevity and readability, the table uses the following rules-o
 
 Further clarification is provided in the notes following the table.
 
-== C-type instructions
-The `RV64C` extension for compressed instructions specifies that \~50% of all instructions can be represented using a 16-bit instruction (rather than 32-bits), saving \~25% in code size.
-This execution of assembly code is _not_ agnostic to an instruction's compression state; after executing a compressed instruction, the `pc` should be incremented by $2$ rather than $4$.
-To indicate an instruction is provided in compressed form, the `c_type` flag is introduced.
-*This flag should be set to $1$ whenever the decoded instruction is provided in compressed form and $0$ otherwise.*
-
 /// Add a reference to one or more notes following this table.
 #let ref_note(..refs) = {
   super("[" + refs.pos().map(r => ref(r)).join(",") + "]")
@@ -152,6 +146,12 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is
 
 #decoding_table(decoding)
 
+== C-type instructions
+The `RV64C` extension for compressed instructions specifies that \~50% of all instructions can be represented using a 16-bit instruction (rather than 32-bits), saving \~25% in code size.
+This execution of assembly code is _not_ agnostic to an instruction's compression state; after executing a compressed instruction, the `pc` should be incremented by $2$ rather than $4$.
+To indicate an instruction is provided in compressed form, the `c_type` flag is introduced.
+*This flag should be set to $1$ whenever the decoded instruction is provided in compressed form and $0$ otherwise.*
+
 // Construct a note that can be referenced through `lbl`
 #let referenceable_note(lbl, note) = {
   show figure: (it) => align(left, [#it])

spec/src/cpu.toml

@@ -664,6 +664,7 @@ tag = "MEMW"
 input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", ["cast", "rv1", "DWordWL"], 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0]
 output = ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", ["cast", "rv1", "DWordWL"], 1], 0, 0, 0, 0, 0, 0]
 multiplicity = "read_register1"
+ref = "cpu:c:read_rv1"
 
 [[constraints.mem]]
 kind = "arith"