[libre-riscv-dev] BlueSpec Floating Point

[libre-riscv-dev] BlueSpec Floating Point

[Immanuel, Yehowshua U]

I have recently been playing with BlueSpec and they have some libraries for generating floating point that also come with some formal methods I think.

We should look into this as it might save some time for reconfigurable FP. Also, Bluespec compiler is now open source under a license that’s basically the BSD license, see here: https://github.com/B-Lang-org/bsc/blob/master/LICENSES/LICENSE.hbc

I’ve successfully built BSC on MacOS too, so its pretty flexible - not to mention fast.
We can take emitted BSC Verilog and perhaps convert it into nMigen once we’ve ran all the formal tests on the FP unit in BSV.

If you guys want - I can actually work on the FP unit in BSV and see how that goes.

Yehowshua
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] BlueSpec Floating Point

[Luke Kenneth Casson Leighton]

On Sunday, March 29, 2020, Immanuel, Yehowshua U <yimmanuel3@gatech.edu>
wrote:

> I have recently been playing with BlueSpec and they have some libraries
> for generating floating point that also come with some formal methods I
> think.


ah good.


>
> We should look into this as it might save some time for reconfigurable FP.


maybe, maybe not.  the ieee754 fp library, in nmigen, is not just
reconfigureable at the bit level, the pipelines are reconfigureable as
well.  i just described that partly only yesterday.



>  Also, Bluespec compiler is now open source under a license that’s
> basically the BSD license, see here: https://github.com/B-Lang-org/
> bsc/blob/master/LICENSES/LICENSE.hbc


good... the problem is, that doesn't help with the actual programmability.

i worked in india with one of the best people in this field (see pinmux
code) and it was hell.  really.


>
> I’ve successfully built BSC on MacOS too, so its pretty flexible - not to
> mention fast.
> We can take emitted BSC Verilog and perhaps convert it into nMigen once
> we’ve ran all the formal tests on the FP unit in BSV.


the unprogrammability and learning curve, right at a pressure point where
we are about to start using code that took over six months to design and
verify, makes this not a viable idea.

however *cross* verification, running them side by side, *is* i think
viable and useful.

the reasoning there is that we can use them, running side by side, in the
unit tests, and seek out discrepancies.

it'll take a week to run but that's ok.


>
> If you guys want - I can actually work on the FP unit in BSV and see how
> that goes.


yes please.

also if you can work out how the formal proofs work, and how to extract the
links into the BSV code or plug in the nmigen library, that would be really
handy.

we have an NLNet budget for FP.Formal proof work btw.

l.





-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] BlueSpec Floating Point

[Immanuel, Yehowshua U]

Sent from my iPad

> On Mar 29, 2020, at 2:46 PM, Luke Kenneth Casson Leighton <lkcl@lkcl.net> wrote:
> 
> also if you can work out how the formal proofs work, and how to extract the
> links into the BSV code or plug in the nmigen library, that would be really
> handy.

Currently, BSV uses the SMT Yices solver.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] BlueSpec Floating Point

[Immanuel, Yehowshua U]

On Mar 29, 2020, at 2:46 PM, Luke Kenneth Casson Leighton <lkcl@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.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] BlueSpec Floating Point

[Luke Kenneth Casson Leighton]

On Sunday, March 29, 2020, Immanuel, Yehowshua U <yimmanuel3@gatech.edu>
wrote:

>
>
> Sent from my iPad
>
> > On Mar 29, 2020, at 2:46 PM, Luke Kenneth Casson Leighton <lkcl@lkcl.net>
> wrote:
> >
> > also if you can work out how the formal proofs work, and how to extract
> the
> > links into the BSV code or plug in the nmigen library, that would be
> really
> > handy.
>
> Currently, BSV uses the SMT Yices solver


excellent.

same as yosys.

did they do DIRECT to yices or did they go via symbiyosis?

l.



-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] BlueSpec Floating Point

[Luke Kenneth Casson Leighton]

On Sunday, March 29, 2020, Immanuel, Yehowshua U <yimmanuel3@gatech.edu>
wrote:

>
> On Mar 29, 2020, at 2:46 PM, Luke Kenneth Casson Leighton <lkcl@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.

l.



-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] BlueSpec Floating Point

[Immanuel, Yehowshua U]

Yep. I have an assignment due Wednesday - so I’ll tackle this after that.
Yehowshua
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev