meetings/sync_up/sync_up_2023-11-15.mdwn

   1 # Wednesday 15th November 09:00 UTC
   2
   3 * Previous week's notes: [[meetings/sync_up/sync_up_2023-11-07]]
   4 * Yesterday's notes: [[meetings/sync_up/sync_up_2023-11-14]]
   5 * Next week's notes: [[meetings/sync_up/sync_up_2023-11-21]]
   6
   7 ## Cesar
   8
   9 - Working through the formal correctness proof for the ld/st unit.
  10   - Says will be similar to compunit.
  11   - Need to fetch operands, store results.
  12 - There are 2 compunits in two files:
  13   - ALU Compunit does everything but ld/st.
  14   - LD/ST Compunit is for mem-reg/reg-mem.
  15 (Only the ld/st proof is covered by current grant, see
  16 [bug #1036](https://bugs.libre-soc.org/show_bug.cgi?id=1036))
  17
  18 On future grant:
  19
  20 - Make sure future grants include budget for formal verification.
  21
  22 When doing HDL design:
  23
  24 - Ideally should be able to switch between *design, verification, simulation.*
  25
  26 On Fosdem:
  27
  28 - What to do about talk submissions which use the unauthorised for of nMigen?...
  29
  30
  31 [[!tag meeting2023]]
  32 [[!tag meeting_sync_up]]