2024-12-16 - 2025-12-16
Overview
2 pull requests merged by 1 user
Merged
#23 switch to use server's new actions org
Merged
#1 fill out grant tracking structure
3 issues closed from 1 user
Closed
#4 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).
Closed
#6 NLnet 2024-12-324 Add support for the Arty A7 100T since that's what we're using for CI.
Closed
#7 NLnet 2024-12-324 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.
21 issues created by 1 user
Opened
#2 NLnet 2024-12-324 Figure out how exactly we should represent HDL in Rocq
Opened
#3 NLnet 2024-12-324 Write the code to do the translation in Fayalite.
Opened
#4 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).
Opened
#5 NLnet 2024-12-324 Add support for the Orange Crab since both Cesar and Jacob have one.
Opened
#6 NLnet 2024-12-324 Add support for the Arty A7 100T since that's what we're using for CI.
Opened
#7 NLnet 2024-12-324 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.
Opened
#8 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.
Opened
#9 NLnet 2024-12-324 Translate the procedural model to use actual synthesizeable HDL
Opened
#10 NLnet 2024-12-324 Create the next-instruction logic
Opened
#11 NLnet 2024-12-324 Create the fetch and i-cache logic.
Opened
#12 NLnet 2024-12-324 Create the PowerISA decoder
Opened
#13 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.
Opened
#14 NLnet 2024-12-324 Translate the procedural model to use actual synthesizeable HDL.
Opened
#15 NLnet 2024-12-324 memory system: main memory and IO devices
Opened
#16 NLnet 2024-12-324 d-cache
Opened
#17 NLnet 2024-12-324 memory load execution unit (we'll want to be able to do more than one load at once)
Opened
#18 NLnet 2024-12-324 memory store execution unit
Opened
#19 NLnet 2024-12-324 adding atomics: lr/sc, atomic fetch-add (or other fetch-op)
Opened
#20 NLnet 2024-12-324 adding order-violation detection logic
Opened
#21 NLnet 2024-12-324 Write Rocq and HDL logic for tracking which instructions will eventually be cancelled and which will eventually be retired.
Opened
#22 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