# Have you been involved with projects or organisations relevant to this project before? And if so, can you tell us a bit about your contributions?
A lot! a full list is maintained here <https://libre-soc.org/nlnet_proposals/>
-and includes the world's first FOSSHW IEEE754 Formal Correctness Proofs for fadd, fsub, and fma; the world's first in-place Discrete Cosine Transform algorithm;
+and includes the world's first FOSSHW IEEE754 Formal Correctness Proofs for fadd, fsub, and fma, with support for FP Formal Proofs added to symbiyosis;
+the world's first in-place Discrete Cosine Transform algorithm;
Significant improvements to Europe's only silicon-proven FOSSHW VLSI toolchain (coriolis2, by LIP6 Labs) to do an 800,000 transistor fully automated RTL2GDSII
tape-out; the side-benefits alone are enormous.
# Explain what the requested budget will be used for?
+* ongoing communication with the OpenPOWER Foundation ISA Working Group
+* preparation of a large number of RFCs (380 pages total so far) through
+ the External RFC Process
+* for each RFC accepted, work needs to be done with IBM to submit Power ISA Spec
+ changes
+* for each RFC accepted, a Compliance Test Suite must be written
+* for each Compliance Test Suite written the results must be
+ confirmed correct by inspection (hence the Simulator) which has
+ as we already discovered been quite a lot of work
+* Along the way we aim to continue developing the "Test API" which
+ allows running thousands of unit tests on multiple systems and
+ cross-checking the results. Currently we have Simulator, some
+ "Expected Results", and the Libre-SOC HDL as well as qemu.
+ We aim to add cavatools, gem5, Microwatt and stand-alone binary
+ auto-generation for running on IBM POWER9 as well as Libre-SOC
+ and Microwatt FPGAs.
# Compare your own project with existing or historical efforts.