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

[Jacob Lifshay]

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

> ---
> 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
https://publikationen.sulb.uni-saarland.de/bitstream/20.500.11880/25760/1/ChristianJacobi_ProfDrWolfgangJPaul.pdf
which links to the source for their VAMP cpu:
https://www-wjp.cs.uni-sb.de/forschung/projekte/VAMP/?lang=en
I couldn't find the copyright for the whole thing, but the PVS/hw subfolder
is under the 2-clause BSD license:
https://www-wjp.cs.uni-sb.de/forschung/projekte/VAMP/PVS/hw/COPYRIGHT

looking around for a git repo, i found this:
https://alastairreid.github.io/RelatedWork/papers/beyer:ijsttt:2006/

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

Jacob