I finally got around to working on the NLnet grant budget some more, there are a few TODOs still though.
Subdivided budget so far:
€ 6000 -- Adding Rocq output in Fayalite
€ 2000 -- Figure out how exactly we should represent HDL in Rocq, writing down a manually-translated version of common HDL components (e.g. how to translate a register, a memory, an add/sub/mul/div, etc.).
€ 4000 -- Write the code to do the translation in Fayalite.
€ 4000 -- Adding supporting code for generating FPGA bitstreams from Fayalite
€ 2000 -- Write support for board interface descriptions and the code for running the FPGA toolchain (similar to the existing code for running SymbiYosys -- the current formal verification toolchain).
€ 1000 -- Add support for the Orange Crab since both Cesar and Jacob have one.
€ 1000 -- Add support for the Arty A7 100T since that's what we're using for CI.
€ 10000 -- Register Renaming, Execution, and Instruction Retire
€ 1500 -- Add to the simulator in Fayalite the ability to transfer non-HDL data (e.g. HashMap) through the digital signalling mechanism, this allows using those data types when writing procedural models.
€ 6000 -- Create a model of the whole rename/execute/retire control system, using procedural implementations of the most complex HDL modules where appropriate.
€ 2500 -- Translate the procedural model to use actual synthesizeable HDL. includes a proof of correctness of the out-of-order CPU in relation to a sequential CPU (probably most easily done by adding the proof to the retire stage).
€ 8000 -- Instruction Fetch/Decode
€ 1000 -- Create the next-instruction logic -- includes some sort of branch prediction or branch target buffer so we can actually keep the rest of the CPU pipeline full. This should support fetching more than one instruction per clock.
€ 1000 -- Create the fetch and i-cache logic.
€ 2000 -- Create the PowerISA decoder -- it translates to the internal microcode. For now, only needs to support a reasonable subset of 64-bit LE integer instructions in problem mode (aka. user mode), FP and VMX/VSX can be disabled.
€ 2000 -- Create a model of the instruction fetch/decode control system, using procedural implementations of the most complex HDL modules where appropriate.
€ 2000 -- Translate the procedural model to use actual synthesizeable HDL.
€ 10000 -- Load/Store instructions
should include d-cache, some kind of memory, and at least one IO device.
should include at least lr/sc, some atomic fetch-op, cached load/store, and IO load/store (IO needs to wait until non-speculative to start executing).
€ 1000 memory system: main memory and IO devices -- I'm expecting just a big sram to be good enough for simulation of memory, on the fpga we could probably get away with a relatively small sram and put off a dram interface for later. for the IO device, I'm thinking we'd have a simple fixed-frequency uart.
€ 1000 d-cache
€ 2500 memory load execution unit (we'll want to be able to do more than one load at once)
€ 2500 memory store execution unit
€ 2000 adding atomics: lr/sc, atomic fetch-add (or other fetch-op)
€ 1000 adding order-violation detection logic, so we can make memory look like it has total-store-order (for x86), or even sequential consistency (meaning we can ignore all non-IO fences)
€ 12000 -- Work towards the Formal Proof of No Spectre bugs
€ 3000 -- Write Rocq and HDL logic for tracking which instructions will eventually be cancelled and which will eventually be retired.
€ 9000 -- Attempt Proof that our CPU but with zeroed outputs for all eventually-cancelled instructions is equivalent to our real CPU design. This may need significant modifications to the CPU. This task may be too big and need further subdividing once we've made some progress on the proof so we know where to subdivide it.
updated "Load/Store instructions" and "Register Renaming, Execution, and Instruction Retire"/"Translate the procedural model to use actual synthesizeable HDL" from the meeting today.
So, for the last item ("Work towards the Formal Proof of No Spectre bugs"), I think we should split it up like so:
€ 12000 -- Work towards the Formal Proof of No Spectre bugs
€ 3000 -- Write Rocq and HDL logic for tracking which instructions will eventually be cancelled and which will eventually be retired.
€ 9000 -- Attempt Proof that our CPU but with zeroed outputs for all eventually-cancelled instructions is equivalent to our real CPU design. This may need significant modifications to the CPU. This task may be too big and need further subdividing once we've made some progress on the proof so we know where to subdivide it.
Does this look good? Is it all ready to submit to NLnet?