[libre-riscv-dev] BlueSpec Floating Point

Luke Kenneth Casson Leighton lkcl at lkcl.net
Sun Mar 29 20:05:58 BST 2020

On Sunday, March 29, 2020, Immanuel, Yehowshua U <yimmanuel3 at gatech.edu>

> On Mar 29, 2020, at 2:46 PM, Luke Kenneth Casson Leighton <lkcl at lkcl.net>
> wrote:
> >
> > we have an NLNet budget for FP.Formal proof work btw.
> Ok. I’ll see what I can do for floating point in BSV and how well formal
> can work.

if nothing else we can lift what they did and replicate it.

can you raise a bugreport and crossreference this discussion?

sublink it under the IEEE754 Formal Proof milestone.


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

More information about the libre-riscv-dev mailing list