docs: update docs for element-addressable memory #1616

plafer · 2025-01-08T20:57:09Z

Updates the docs for element-addressable memory

Al-Kindi-0

Did an initial review and things look good.

Al-Kindi-0 · 2025-01-10T10:00:35Z

docs/src/assets/design/stack/io_ops/MLOAD.png

Maybe we should just remove the helper registers as they have no use with the recent changes. For someone without any historical knowledge of the changes, having helper registers in the drawing will just be confusing, I believe.

Al-Kindi-0 · 2025-01-10T10:01:17Z

docs/src/assets/design/stack/io_ops/MSTORE.png

Same here, and everywhere there are unused helper registers.

Al-Kindi-0 · 2025-01-10T10:02:09Z

docs/src/assets/design/chiplets/memory/memory_miden_vm_layout.png

Proposal: would waddr or w_addr work better here and potentially everywhere?

I find word_addr to be more descriptive, but I'm also okay with changing it

Al-Kindi-0 · 2025-01-10T10:37:46Z

docs/src/design/chiplets/memory.md

-  - When both the context and the address remain the same, this column contains the inverse of $(i' - i - 1)$.
+  - When the context remains the same but the word address changes, this column contains the inverse of $(a' - a)$.
+  - When both the context and the word address remain the same, this column contains the inverse of $(clk' - clk - 1)$.
+- Column `f_scw` stands for "flag same context and word address", which is set to $1$ when the current and next rows have the same context and word address, and $0$ otherwise.


should this be "current and previous row" given the usage below?

Good catch, fixed

Al-Kindi-0 · 2025-01-10T10:41:45Z

docs/src/design/chiplets/memory.md

 - Column `t` contains the inverse of the delta between two consecutive context IDs, addresses, or clock cycles. Specifically:
  - When the context changes, this column contains the inverse of $(c' - c)$.


Not related to this PR, but is this definition of t congruent with how n0 and n1 are defined?

Hmmm not sure I follow, could you rephrase?

Basically, the above sentence says that t contains the inverse of c' - c but n0 is defined as n0 = (c' - c) . t'.

The current way it's written, it doesn't mention whether the "current" or "next" row in a frame contains the deltas. d0 and d1 are described in a similar manner.

I updated both to say that the "next" row contains the delta.

Al-Kindi-0 · 2025-01-10T10:45:57Z

docs/src/design/chiplets/memory.md

+- For the first row of the chiplet (in the "next" position of the frame), for $0 \leq i < 4$,
+


Should we add the selector, or at least a comment about it, for first row?
Similar comment about selector for within memory chiplet

Agreed, I added the flags to all constraints

Al-Kindi-0 · 2025-01-10T11:00:32Z

docs/src/design/chiplets/memory.md

+c_i = rw' + (1 - rw') \cdot (1 - ew') \cdot (1 - f_i') \text{ | degree} = 4\\
+$$


There is a naming collision with regards to $c$.

Changed all c to ctx

bobbinth

Looks good! Thank you. I left some comments inline. Assuming I didn't make too many mistakes, we should review the constraints more carefully.

@Al-Kindi-0 @paracetamolo - could you take another look as well?

docs/src/design/chiplets/memory.md

bobbinth · 2025-01-12T02:17:30Z

Also, would be good to rebase this PR to get rid of the changes carried over from the previously merged PR.

bobbinth

Looks good! Thank you! I left a few small comments inline.

Also, a question: are the memory chiplet bus constraints not implemented yet? (asking because even though we changed the description of constraints, nothing changed in the code).

docs/src/design/chiplets/memory.md

Al-Kindi-0

Looks good, thank you!

Al-Kindi-0 · 2025-01-14T10:18:05Z

processor/src/chiplets/memory/mod.rs

+/// - `idx0` and `idx1` are selector columns used to identify which element in the word is being
+///   accessed. Specifically, the index within the word is computed as `idx1 * 2 + idx0`.


nit: probably worth adding that this is only when the op is an element op. Else, they are probably set to zero

This is what we have in the sub-bullet point:

- However, when `ew` is set to $1$ (indicating that a word is accessed), these columns are meaningless and are set to $0$.

Al-Kindi-0 · 2025-01-14T10:29:42Z

docs/src/design/chiplets/memory.md

+- For all rows of the chiplet except the first, and when there is new context or word address, for $0 \leq i < 4$,
+


should probably be updated after the merge of constraints

Right; fixed

plafer · 2025-01-14T14:17:43Z

Also, a question: are the memory chiplet bus constraints not implemented yet? (asking because even though we changed the description of constraints, nothing changed in the code).

The bus was modified in the previous PR (see

miden-vm/processor/src/chiplets/aux_trace/mod.rs

Lines 900 to 944 in 0e7c1d6

    
           let is_word_access = main_trace.chiplet_selector_4(row); 
        
           let header = { 
        
               let is_read = main_trace.chiplet_selector_3(row); 
        
               let op_label = get_memory_op_label(is_read, is_word_access); 
        
               let ctx = main_trace.chiplet_memory_ctx(row); 
        
               let clk = main_trace.chiplet_memory_clk(row); 
        
               let address = { 
        
                   let word = main_trace.chiplet_memory_word(row); 
        
                   let idx0 = main_trace.chiplet_memory_idx0(row); 
        
                   let idx1 = main_trace.chiplet_memory_idx1(row); 
        
                   word + idx1.mul_small(2) + idx0 
        
               }; 
        
               alphas[0] + build_value(&alphas[1..5], [op_label, ctx, address, clk]) 
        
           }; 
        
           if is_word_access == MEMORY_ACCESS_ELEMENT { 
        
               let idx0 = main_trace.chiplet_memory_idx0(row); 
        
               let idx1 = main_trace.chiplet_memory_idx1(row); 
        
               let value = if idx1 == ZERO && idx0 == ZERO { 
        
                   main_trace.chiplet_memory_value_0(row) 
        
               } else if idx1 == ZERO && idx0 == ONE { 
        
                   main_trace.chiplet_memory_value_1(row) 
        
               } else if idx1 == ONE && idx0 == ZERO { 
        
                   main_trace.chiplet_memory_value_2(row) 
        
               } else if idx1 == ONE && idx0 == ONE { 
        
                   main_trace.chiplet_memory_value_3(row) 
        
               } else { 
        
                   panic!("Invalid word indices. idx0: {idx0}, idx1: {idx1}"); 
        
               }; 
        
               header + alphas[5].mul_base(value) 
        
           } else if is_word_access == MEMORY_ACCESS_WORD { 
        
               let value0 = main_trace.chiplet_memory_value_0(row); 
        
               let value1 = main_trace.chiplet_memory_value_1(row); 
        
               let value2 = main_trace.chiplet_memory_value_2(row); 
        
               let value3 = main_trace.chiplet_memory_value_3(row); 
        
               header + build_value(&alphas[5..9], [value0, value1, value2, value3]) 
        
           } else { 
        
               panic!("Invalid memory element/word column value: {is_word_access}"); 
        
           }

) - what we did in this PR is properly document what is already implemented.

plafer mentioned this pull request Jan 9, 2025

Implement element-addressable memory #1598

Merged

plafer added the no changelog This PR does not require an entry in the `CHANGELOG.md` file label Jan 9, 2025

plafer force-pushed the plafer-docs-eam branch from bbe0410 to 1c233c6 Compare January 9, 2025 21:51

plafer marked this pull request as ready for review January 9, 2025 21:51

plafer requested review from bobbinth and Al-Kindi-0 January 9, 2025 21:51

Al-Kindi-0 reviewed Jan 10, 2025

View reviewed changes

Base automatically changed from plafer-1064-element-addressable-mem to element-addressable-memory January 10, 2025 16:56

plafer changed the base branch from element-addressable-memory to next January 10, 2025 16:56

plafer changed the base branch from next to element-addressable-memory January 10, 2025 16:56

plafer force-pushed the plafer-docs-eam branch from 8fe0133 to 42a5bc6 Compare January 10, 2025 17:19

bobbinth requested changes Jan 12, 2025

View reviewed changes

plafer changed the base branch from element-addressable-memory to next January 13, 2025 14:32

plafer changed the base branch from next to element-addressable-memory January 13, 2025 14:32

plafer added 4 commits January 13, 2025 09:38

docs: update docs for element-addressable memory

7f3028e

PR fixes

c36b85c

docs(mem): update all constraints with memory flags

0d6f5a8

c -> ctx

3717045

plafer force-pushed the plafer-docs-eam branch from 42a5bc6 to 3717045 Compare January 13, 2025 14:42

plafer added 4 commits January 13, 2025 10:35

docs: PR fixes

a25eca6

fix: merge 8 -> 4 constraints together

5c0ca5c

more PR fixes

91b447d

PR fixes

b085365

plafer requested review from bobbinth and Al-Kindi-0 January 13, 2025 19:29

bobbinth approved these changes Jan 14, 2025

View reviewed changes

docs/src/design/chiplets/memory.md Outdated Show resolved Hide resolved

docs/src/design/chiplets/memory.md Outdated Show resolved Hide resolved

docs/src/design/chiplets/memory.md Outdated Show resolved Hide resolved

docs/src/design/chiplets/memory.md Outdated Show resolved Hide resolved

Al-Kindi-0 approved these changes Jan 14, 2025

View reviewed changes

plafer mentioned this pull request Jan 14, 2025

Memory: allow for multiple memory reads in the same clock cycle #1622

Closed

PR fixes

2741b8a

plafer merged commit 29ef925 into element-addressable-memory Jan 14, 2025
9 checks passed

plafer deleted the plafer-docs-eam branch January 14, 2025 14:37

bobbinth mentioned this pull request Jan 22, 2025

RFC: Extend the behavior of load/store ops to allow addressing all elements of a word #1064

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

docs: update docs for element-addressable memory #1616

docs: update docs for element-addressable memory #1616

plafer commented Jan 8, 2025 •

edited

Loading

Al-Kindi-0 left a comment

Al-Kindi-0 Jan 10, 2025

plafer Jan 10, 2025

Al-Kindi-0 Jan 10, 2025

plafer Jan 10, 2025

Al-Kindi-0 Jan 10, 2025

plafer Jan 10, 2025

Al-Kindi-0 Jan 10, 2025

plafer Jan 10, 2025

Al-Kindi-0 Jan 10, 2025

plafer Jan 13, 2025

Al-Kindi-0 Jan 14, 2025

plafer Jan 14, 2025

Al-Kindi-0 Jan 10, 2025

plafer Jan 10, 2025

Al-Kindi-0 Jan 10, 2025

plafer Jan 10, 2025

bobbinth left a comment

bobbinth commented Jan 12, 2025

bobbinth left a comment

Al-Kindi-0 left a comment

Al-Kindi-0 Jan 14, 2025

plafer Jan 14, 2025

Al-Kindi-0 Jan 14, 2025

plafer Jan 14, 2025

plafer commented Jan 14, 2025

		- Column `t` contains the inverse of the delta between two consecutive context IDs, addresses, or clock cycles. Specifically:
		- When the context changes, this column contains the inverse of $(c' - c)$.

		- For the first row of the chiplet (in the "next" position of the frame), for $0 \leq i < 4$,

		c_i = rw' + (1 - rw') \cdot (1 - ew') \cdot (1 - f_i') \text{ \| degree} = 4\\
		$$

		/// - `idx0` and `idx1` are selector columns used to identify which element in the word is being
		/// accessed. Specifically, the index within the word is computed as `idx1 * 2 + idx0`.

		- For all rows of the chiplet except the first, and when there is new context or word address, for $0 \leq i < 4$,

docs: update docs for element-addressable memory #1616

docs: update docs for element-addressable memory #1616

Conversation

plafer commented Jan 8, 2025 • edited Loading

Al-Kindi-0 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bobbinth left a comment

Choose a reason for hiding this comment

bobbinth commented Jan 12, 2025

bobbinth left a comment

Choose a reason for hiding this comment

Al-Kindi-0 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

plafer commented Jan 14, 2025

plafer commented Jan 8, 2025 •

edited

Loading