1 # Tuesday 14th November
3 * Previous weeks' notes: [[meetings/sync_up/2023-11-07_08]]
4 * Next weeks' notes: [[meetings/sync_up/2023-11-21_22]]
8 - Planning to start making snippets of Poly-1305, asked for advice on
9 how to setup test file (examples
13 - Created budget estimates for
14 [bug #1169](https://bugs.libre-soc.org/show_bug.cgi?id=1169).
15 Asked for approval whether can proceed or not.
17 - Asked for the reason of the budget distribution in
18 [bug #983](https://bugs.libre-soc.org/show_bug.cgi?id=983)
19 (This bug's budget will be used to fund bug #1169.)
23 - Luke and I in conversation with Michiel to query about FOSDEM costs.
24 Later this week on another call to finalise the ongoing grant MoU.
25 *(The MoU was signed the following week.)*
27 - Continued to work on Libre-SOC documentation included in [[HDL_workflow]]
28 and [[HDL_workflow/libresoc_bug_process]]. See
29 [bug #1126](https://bugs.libre-soc.org/show_bug.cgi?id=1126) for updates.
31 - Looked at list of tasks under bug #1169 and gave Jacob the go-ahead
32 to proceed with tasks that are definitely required, and wait for Luke's
34 *(Given my lack of understanding and background, this was a mistake, and
35 I should have waited for Luke's comments on the task list. This is noted
38 # Wednesday 15th November
42 - Working through the formal correctness proof for the ld/st unit.
43 - Says will be similar to compunit.
44 - Need to fetch operands, store results.
45 - There are 2 compunits in two files:
46 - ALU Compunit does everything but ld/st.
47 - LD/ST Compunit is for mem-reg/reg-mem.
48 (Only the ld/st proof is covered by current grant, see
49 [bug #1036](https://bugs.libre-soc.org/show_bug.cgi?id=1036))
53 - Make sure future grants include budget for formal verification.
55 When doing HDL design:
57 - Ideally should be able to switch between *design, verification, simulation.*
61 - What to do about talk submissions which use the unauthorised for of nMigen?...
65 [[!tag meeting_sync_up]]