[libre-riscv-dev] BlueSpec Floating Point

[Luke Kenneth Casson Leighton]

On Sunday, March 29, 2020, Immanuel, Yehowshua U <yimmanuel3 at 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