libre-chip/grant-tracking
2
0
Fork 1
Code Issues 21 Pull requests Projects 1 Activity Actions

link to issue and project

Browse source
This commit is contained in:
Jacob Lifshay 2025-08-25 23:01:46 -07:00
parent c54a130dac
commit d02476d925
Signed by: programmerjake
SSH key fingerprint: SHA256:HnFTLGpSm4Q4Fj502oCFisjZSoakwEuTsJJMSke63RQ
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
nlnet-2024-12-324/progress.md
View file

@ -4,6 +4,8 @@ See Notices.txt for copyright information
--> -->
# NLnet 2024-12-324 Grant Progress # NLnet 2024-12-324 Grant Progress
[Forgejo Project for this grant.](https://git.libre-chip.org/libre-chip/grant-tracking/projects/1)
# € 50000 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs # € 50000 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs
Modern computers suffer from a constant stream of new speculative-execution security flaws (Spectre-style bugs). To address this major category of flaws, we are working towards building a high-performance computer processor (CPU) with speculative execution and working on a mathematical proof that it doesn't suffer from any speculative-execution data leaks, thereby demonstrating that this major category of flaws can be eliminated without crippling the computer's performance. Modern computers suffer from a constant stream of new speculative-execution security flaws (Spectre-style bugs). To address this major category of flaws, we are working towards building a high-performance computer processor (CPU) with speculative execution and working on a mathematical proof that it doesn't suffer from any speculative-execution data leaks, thereby demonstrating that this major category of flaws can be eliminated without crippling the computer's performance.
@ -14,7 +16,7 @@ https://en.wikipedia.org/wiki/Transient_execution_CPU_vulnerability#Timeline
This is for adding the code for translating Fayalite HDL to Rocq, as well as determining how exactly we'll describe HDL in Rocq. I expect the translation code to be of comparable size to the compiler portion of the simulator (the simulator is broken into three main parts, a compiler to an IR optimized for interpretation, the interpreter itself, and the code for reading/writing simulator I/O and handling time simulation), so somewhere around 5000 LoC. This is for adding the code for translating Fayalite HDL to Rocq, as well as determining how exactly we'll describe HDL in Rocq. I expect the translation code to be of comparable size to the compiler portion of the simulator (the simulator is broken into three main parts, a compiler to an IR optimized for interpretation, the interpreter itself, and the code for reading/writing simulator I/O and handling time simulation), so somewhere around 5000 LoC.
- € 2000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Figure out how exactly we should represent HDL in Rocq, writing down a manually-translated version of common HDL components (e.g. how to translate a register, a memory, an add/sub/mul/div, etc.). - € 2000 [Issue #2](https://git.libre-chip.org/libre-chip/grant-tracking/issues/2) Figure out how exactly we should represent HDL in Rocq, writing down a manually-translated version of common HDL components (e.g. how to translate a register, a memory, an add/sub/mul/div, etc.).
- € 4000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Write the code to do the translation in Fayalite. - € 4000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Write the code to do the translation in Fayalite.
## € 4000 Adding supporting code for generating FPGA bitstreams from Fayalite ## € 4000 Adding supporting code for generating FPGA bitstreams from Fayalite