nlnet-2025-12-681: create proposed plan

nlnet-2025-12-681/plan.txt

@@ -0,0 +1,60 @@
+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

nlnet-2025-12-681/progress.md

@@ -0,0 +1,71 @@
+<!--
+SPDX-License-Identifier: LGPL-3.0-or-later
+See Notices.txt for copyright information
+-->
+# NLnet 2025-12-681 Grant Progress
+
+[Forgejo Project for this grant. TODO](https://git.libre-chip.org/libre-chip/grant-tracking/projects/TODO)
+
+# &euro; 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).
+
+## &euro; 45000 Adding missing features to our CPU, such as floating-point instructions, and better compatibility with the PowerISA specification.
+
+- &euro; 5750 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Floating-point Add/Sub
+
+- &euro; 7650 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Floating-point Mul/FMA
+
+- &euro; 11500 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Floating-point Div/Sqrt
+
+- &euro; 2850 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Floating-point Comparison
+
+- &euro; 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.)
+
+- &euro; 11500 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Handling Floating-point control/status and PowerISA's OV/SO
+
+## &euro; 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.
+
+- &euro; 10000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Add the programmable decoder
+- &euro; 10000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Add the µOp cache
+
+## &euro; 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.
+
+- &euro; 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
+- &euro; 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
+
+## &euro; 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.
+
+- &euro; 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
+- &euro; 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.
+- &euro; 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.
+
+## &euro; 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.
+
+- &euro; 10000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/N) Work towards the Formal Proof of No Spectre bugs