From: Andrey Miroshnikov Date: Fri, 24 Nov 2023 18:55:42 +0000 (+0000) Subject: Forgot to remove section, already in next day's notes X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2db2f4b7a515014988bfdfefdd2976461653e3c7;p=libreriscv.git Forgot to remove section, already in next day's notes --- diff --git a/meetings/sync_up/sync_up_2023-11-14.mdwn b/meetings/sync_up/sync_up_2023-11-14.mdwn index 355b996f3..8a1fbc23e 100644 --- a/meetings/sync_up/sync_up_2023-11-14.mdwn +++ b/meetings/sync_up/sync_up_2023-11-14.mdwn @@ -36,31 +36,5 @@ response on the rest. I should have waited for Luke's comments on the task list. This is noted for future bugs.)* -# Wednesday 15th November - -## 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]]