From abd41726a6ab839bd77f14f317b95bd474d05779 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Mon, 22 Jun 2026 23:40:40 -0700 Subject: [PATCH] nlnet-2025-12-681: create proposed plan --- nlnet-2025-12-681/plan.txt | 59 +++++++++++++++++++++++++++++ nlnet-2025-12-681/progress.md | 70 +++++++++++++++++++++++++++++++++++ 2 files changed, 129 insertions(+) create mode 100644 nlnet-2025-12-681/plan.txt create mode 100644 nlnet-2025-12-681/progress.md diff --git a/nlnet-2025-12-681/plan.txt b/nlnet-2025-12-681/plan.txt new file mode 100644 index 0000000..2c73e6a --- /dev/null +++ b/nlnet-2025-12-681/plan.txt @@ -0,0 +1,59 @@ +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. + +- {15000} 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 new file mode 100644 index 0000000..0be192f --- /dev/null +++ b/nlnet-2025-12-681/progress.md @@ -0,0 +1,70 @@ + +# 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. + +- € 15000 [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