Wednesday 15th November 09:00 UTC

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)

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?...