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

Jacob Lifshay programmerjake at gmail.com
Tue Aug 2 12:30:23 BST 2022

On Tue, Aug 2, 2022, 03:57 Luke Kenneth Casson Leighton <lkcl at lkcl.net>

> ---
> 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".

i did not. 5min of googling gave me:
Formal verification of a fully IEEE compliant floating point unit
which links to the source for their VAMP cpu:
I couldn't find the copyright for the whole thing, but the PVS/hw subfolder
is under the 2-clause BSD license:

looking around for a git repo, i found this:

> > also the FP used by the
> > RISC-V Rocket core also likely have formal proofs.
> where is the publicly-available source code?

i didn't look, hence why I said likely. I could be wrong.


More information about the Libre-soc-dev mailing list