[Libre-soc-dev] https://libre-soc.org/nlnet_2022_ongoing/

Jacob Lifshay programmerjake at gmail.com
Tue Aug 2 06:48:03 BST 2022

On Sun, Jul 31, 2022 at 9:06 AM Luke Kenneth Casson Leighton via
Libre-soc-dev <libre-soc-dev at lists.libre-soc.org> wrote:
> the 2nd NLnet grant request is in, this one is "concrete on-the-ground"
> for SVP64 where the OPF ISA WG one is more focussed on the Standard.
> the reason it is possible to put in EUR 100,000 is because we completed
> 2019-02-012


some corrections:
symbiyosis is mis-spelled -- should be SymbiYosys.

the claims of "the world's first":

the world's first FOSSHW IEEE754 Formal Correctness Proofs for fadd,
fsub, and fma, with support for FP Formal Proofs added to SymbiYosys;

I doubt we're the first, I'd expect that Coq and smtlib2's support for
ieee754 has been used for hardware before, also the FP used by the
RISC-V Rocket core also likely have formal proofs. Also, most of the
work for FP Formal Proofs went into nmigen and yosys, the changes in
SymbiYosys are on the order of 10 lines of code.

the world's first in-place Discrete Cosine Transform algorithm

I'd doubt that's the first one, someone probably has an obscure paper on that...

> l.
> ---
> crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
> _______________________________________________
> Libre-soc-dev mailing list
> Libre-soc-dev at lists.libre-soc.org
> http://lists.libre-soc.org/mailman/listinfo/libre-soc-dev

More information about the Libre-soc-dev mailing list