Issues - libre-chip/grant-tracking - Libre-Chip.org

libre-chip/grant-tracking

New issue

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 NLnet 2024-12-324 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

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 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

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 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

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 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

NLnet 2024-12-324 memory store execution unit

#18 opened 2025-08-26 07:11:20 +00:00 by programmerjake NLnet 2024-12-324 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

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 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

NLnet 2024-12-324 d-cache

#16 opened 2025-08-26 07:09:31 +00:00 by programmerjake NLnet 2024-12-324 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

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 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

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 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

NLnet 2024-12-324 Create the PowerISA decoder

#12 opened 2025-08-26 07:04:24 +00:00 by programmerjake NLnet 2024-12-324 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

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 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

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 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

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 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

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 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

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 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs

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 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs