diff --git a/nlnet-2025-12-681/plan.txt b/nlnet-2025-12-681/plan.txt deleted file mode 100644 index b1f86ed..0000000 --- a/nlnet-2025-12-681/plan.txt +++ /dev/null @@ -1,60 +0,0 @@ -takentaal v1.0 - -# {120000} Libre-Chip Programmable Decoder - -Modern computers are built on several different mutually-incompatible -instruction sets such as x86, ARM, PowerISA, and RISC-V. Many of the most -popular instruction sets have no high-speed libre/open-source CPUs, which -makes those CPUs much harder to trust since you can't inspect their -source-code to look for bugs or secret backdoors. Additionally, there are -basically no existing modern CPUs which can run more than one of those ISAs -without requiring software emulation, which is slow and can often be buggy. -To solve those issues, this project is building a fast libre-licensed CPU that -will support a programmable decoder - so the CPU can run nearly any -instruction set at full speed. Another goal is to be able to prove that the -resulting CPU doesn't have speculative-execution security flaws -("Spectre"-style bugs). - -## {45000} Adding missing features to our CPU, such as floating-point instructions, and better compatibility with the PowerISA specification. - -- {5750} Floating-point Add/Sub -- {7650} Floating-point Mul/FMA -- {11500} Floating-point Div/Sqrt -- {2850} Floating-point Comparison -- {5750} Floating-point Conversion from/to Integers and Rounding to Integer (floor/ceil/etc.) -- {11500} Handling Floating-point control/status and PowerISA's OV/SO - -## {20000} Add the programmable decoder and µOp cache to our CPU design. - -This task I don't actually expect to be all that complex, since -the programmable decoder will be pretty straightforward, basically a -pipeline of adders and muxes. the µOp cache will be a bit more -complex, but probably simpler than the d-cache. - -- {10000} Add the programmable decoder -- {10000} Add the µOp cache - -## {20000} Build a compiler that can extract the decoder portion of QEMU using pattern matching and some symbolic execution of LLVM IR, converting to a HDL IR more suitable for hardware. - -- {10000} Make the compiler be able to symbolically execute QEMU up to where it can run QEMU's x86 and/or powerpc decoder -- {10000} Make the compiler be able to extract HDL IR from symbolically executing the decoder - -## {25000} Write code to convert the HDL IR to a bitstream we can program into the decoder. - -I expect this to be mostly running a FPGA toolchain like normal and invoking -nextpnr with the appropriate custom FPGA model, since IIRC you can supply that -with a config file. - -- {5000} Investigate what is needed for getting nextpnr to work for our programmable decoder. -- {10000} Write a custom FPGA model for nextpnr for our programmable decoder. -- {10000} Write code to translate from the HDL IR produced by our compiler and run the HDL through nextpnr, generating a working bitstream for our programmable decoder. - -## {10000} Work towards the Formal Proof of No Spectre bugs - -This covers working on the Formal Proof of No Spectre bugs as well -as improvements to other software/hardware needed for that. A major -portion of this is to figure out what exact properties we need to -formally prove for each part of the CPU, so we can put those parts -together to make a working proof for the entire CPU. - -- {10000} Work towards the Formal Proof of No Spectre bugs diff --git a/nlnet-2025-12-681/progress.md b/nlnet-2025-12-681/progress.md deleted file mode 100644 index c874f9c..0000000 --- a/nlnet-2025-12-681/progress.md +++ /dev/null @@ -1,71 +0,0 @@ - -# NLnet 2025-12-681 Grant Progress - -[Forgejo Project for this grant. TODO](https://git.libre-chip.org/libre-chip/grant-tracking/projects/TODO) - -# € 120000 Libre-Chip Programmable Decoder - -Modern computers are built on several different mutually-incompatible -instruction sets such as x86, ARM, PowerISA, and RISC-V. Many of the most -popular instruction sets have no high-speed libre/open-source CPUs, which -makes those CPUs much harder to trust since you can't inspect their -source-code to look for bugs or secret backdoors. Additionally, there are -basically no existing modern CPUs which can run more than one of those ISAs -without requiring software emulation, which is slow and can often be buggy. -To solve those issues, this project is building a fast libre-licensed CPU that -will support a programmable decoder - so the CPU can run nearly any -instruction set at full speed. Another goal is to be able to prove that the -resulting CPU doesn't have speculative-execution security flaws -("Spectre"-style bugs). - -## € 45000 Adding missing features to our CPU, such as floating-point instructions, and better compatibility with the PowerISA specification. - -- € 5750 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Floating-point Add/Sub - -- € 7650 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Floating-point Mul/FMA - -- € 11500 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Floating-point Div/Sqrt - -- € 2850 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Floating-point Comparison - -- € 5750 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Floating-point Conversion from/to Integers and Rounding to Integer (floor/ceil/etc.) - -- € 11500 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Handling Floating-point control/status and PowerISA's OV/SO - -## € 20000 Add the programmable decoder and µOp cache to our CPU design. - -This task I don't actually expect to be all that complex, since -the programmable decoder will be pretty straightforward, basically a -pipeline of adders and muxes. the µOp cache will be a bit more -complex, but probably simpler than the d-cache. - -- € 10000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Add the programmable decoder -- € 10000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Add the µOp cache - -## € 20000 Build a compiler that can extract the decoder portion of QEMU using pattern matching and some symbolic execution of LLVM IR, converting to a HDL IR more suitable for hardware. - -- € 10000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Make the compiler be able to symbolically execute QEMU up to where it can run QEMU's x86 and/or powerpc decoder -- € 10000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Make the compiler be able to extract HDL IR from symbolically executing the decoder - -## € 25000 Write code to convert the HDL IR to a bitstream we can program into the decoder. - -I expect this to be mostly running a FPGA toolchain like normal and invoking -nextpnr with the appropriate custom FPGA model, since IIRC you can supply that -with a config file. - -- € 5000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Investigate what is needed for getting nextpnr to work for our programmable decoder -- € 10000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Write a custom FPGA model for nextpnr for our programmable decoder. -- € 10000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Write code to translate from the HDL IR produced by our compiler and run the HDL through nextpnr, generating a working bitstream for our programmable decoder. - -## € 10000 Work towards the Formal Proof of No Spectre bugs - -This covers working on the Formal Proof of No Spectre bugs as well -as improvements to other software/hardware needed for that. A major -portion of this is to figure out what exact properties we need to -formally prove for each part of the CPU, so we can put those parts -together to make a working proof for the entire CPU. - -- € 10000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Work towards the Formal Proof of No Spectre bugs