2 changed files with 0 additions and 131 deletions
--- a/nlnet-2025-12-681/plan.txt
+++ b/nlnet-2025-12-681/plan.txt
@ -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
--- a/nlnet-2025-12-681/progress.md
+++ b/nlnet-2025-12-681/progress.md
@ -1,71 +0,0 @@
 <!--
 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