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

[Luke Kenneth Casson Leighton]

---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68

On Tue, Aug 2, 2022 at 6:48 AM Jacob Lifshay <programmerjake at gmail.com> wrote:

> 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,

you missed the significance of the qualifier "FOSSHW".

> also the FP used by the
> RISC-V Rocket core also likely have formal proofs.

where is the publicly-available source 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...

again, look at the qualifier-word: in-place.  i spent somewhere around
8 weeks looking, i couldn't find anything.  it was very frustrating.

there were plenty of SIMD DCT papers and algorithms: all of them
absolutely had to be non-in-place because of copying the data from
gray-code to binary numbering.

all scalar implementations *cannot* be in-place because they use
a tmp variable for the swapping of the butterfly.  or they create an
entire new (non-in-place) 2nd output vector.

hardware-ASIC ones i discounted entirely.

it's that combination of the butterfly (3in-2out) instructions plus
the Gray-Coding on REMAP that makes it possible to legitimately
make this claim of being world's first in-place DCT implementation.

l.