# Wednesday 15th November 09:00 UTC

* Previous week's notes: [[meetings/sync_up/sync_up_2023-11-07]]
* Yesterday's notes: [[meetings/sync_up/sync_up_2023-11-14]]
* Next week's notes: [[meetings/sync_up/sync_up_2023-11-21]]

## Cesar

- Working through the formal correctness proof for the ld/st unit.
  - Says will be similar to compunit.
  - Need to fetch operands, store results.
- There are 2 compunits in two files:
  - ALU Compunit does everything but ld/st.
  - LD/ST Compunit is for mem-reg/reg-mem.
(Only the ld/st proof is covered by current grant, see
[bug #1036](https://bugs.libre-soc.org/show_bug.cgi?id=1036)) 

On future grant:

- Make sure future grants include budget for formal verification.

When doing HDL design:

- Ideally should be able to switch between *design, verification, simulation.*

On Fosdem:

- What to do about talk submissions which use the unauthorised for of nMigen?...


[[!tag meeting2023]]
[[!tag meeting_sync_up]]