libre-chip/grant-tracking
2
0
Fork 1
Code Issues 20 Pull requests Projects 1 Activity Actions
Labels Milestones
New issue

NLnet 2024-12-324 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

https://git.libre-chip.org/libre-chip/grant-tracking/src/branch/master/nlnet-2024-12-324/progress.md

Modern computers suffer from a constant stream of new speculative-execution security flaws (Spectre-style bugs). To address this major category of flaws, we are working towards building a high-performance computer processor (CPU) with speculative execution and working on a mathematical proof that it doesn't suffer from any speculative-execution data leaks, thereby demonstrating that this major category of flaws can be eliminated without crippling the computer's performance.

https://en.wikipedia.org/wiki/Transient_execution_CPU_vulnerability#Timeline

20
Not Yet Started
NLnet 2024-12-324 Figure out how exactly we should represent HDL in Rocq
#2 opened 2025-08-26 02:28:40 +00:00 by programmerjake
NLnet 2024-12-324 Write the code to do the translation in Fayalite.
#3 opened 2025-08-26 06:23:51 +00:00 by programmerjake
NLnet 2024-12-324 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).
#4 opened 2025-08-26 06:25:23 +00:00 by programmerjake
NLnet 2024-12-324 Add support for the Orange Crab since both Cesar and Jacob have one.
#5 opened 2025-08-26 06:49:11 +00:00 by programmerjake
NLnet 2024-12-324 Create a model of the whole rename/execute/retire control system, using procedural implementations of the most complex HDL modules where appropriate.
#8 opened 2025-08-26 06:51:21 +00:00 by programmerjake
NLnet 2024-12-324 Add support for the Arty A7 100T since that's what we're using for CI.
#6 opened 2025-08-26 06:49:54 +00:00 by programmerjake
NLnet 2024-12-324 Translate the procedural model to use actual synthesizeable HDL
#9 opened 2025-08-26 06:53:40 +00:00 by programmerjake
NLnet 2024-12-324 Create the next-instruction logic
#10 opened 2025-08-26 06:54:41 +00:00 by programmerjake
NLnet 2024-12-324 Create the fetch and i-cache logic.
#11 opened 2025-08-26 07:03:00 +00:00 by programmerjake
NLnet 2024-12-324 Create the PowerISA decoder
#12 opened 2025-08-26 07:04:24 +00:00 by programmerjake
NLnet 2024-12-324 Create a model of the instruction fetch/decode control system, using procedural implementations of the most complex HDL modules where appropriate.
#13 opened 2025-08-26 07:05:13 +00:00 by programmerjake
NLnet 2024-12-324 Translate the procedural model to use actual synthesizeable HDL.
#14 opened 2025-08-26 07:06:13 +00:00 by programmerjake
NLnet 2024-12-324 memory system: main memory and IO devices
#15 opened 2025-08-26 07:08:39 +00:00 by programmerjake
NLnet 2024-12-324 d-cache
#16 opened 2025-08-26 07:09:31 +00:00 by programmerjake
NLnet 2024-12-324 memory load execution unit (we'll want to be able to do more than one load at once)
#17 opened 2025-08-26 07:10:37 +00:00 by programmerjake
NLnet 2024-12-324 memory store execution unit
#18 opened 2025-08-26 07:11:20 +00:00 by programmerjake
NLnet 2024-12-324 adding atomics: lr/sc, atomic fetch-add (or other fetch-op)
#19 opened 2025-08-26 07:12:03 +00:00 by programmerjake
NLnet 2024-12-324 adding order-violation detection logic
#20 opened 2025-08-26 07:13:12 +00:00 by programmerjake
NLnet 2024-12-324 Write Rocq and HDL logic for tracking which instructions will eventually be cancelled and which will eventually be retired.
#21 opened 2025-08-26 07:14:28 +00:00 by programmerjake
NLnet 2024-12-324 Attempt Proof that our CPU but with zeroed outputs for all eventually-cancelled instructions is equivalent to our real CPU design
#22 opened 2025-08-26 07:15:34 +00:00 by programmerjake
1
Work in Progress
0
Done