From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
To: Libre-RISCV General Development <libre-riscv-dev@lists.libre-riscv.org>
Subject: Re: [libre-riscv-dev] BlueSpec Floating Point
Date: Sun, 29 Mar 2020 18:45:36 +0000
Message-ID: <CAPweEDx6eo5TS1DJH0XcqLkRQn930RFM=Ve4Q=0maJkgL6b7pA@mail.gmail.com> (raw)
In-Reply-To: <DE994CBE-320B-4F0D-BFBE-D885E6F620EA@gatech.edu>
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
next prev parent reply index
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
2020-03-29 16:09 Immanuel, Yehowshua U
2020-03-29 18:45 ` Luke Kenneth Casson Leighton [this message]
2020-03-29 19:02 ` Immanuel, Yehowshua U
2020-03-29 19:03 ` Luke Kenneth Casson Leighton
2020-03-29 19:03 ` Immanuel, Yehowshua U
2020-03-29 19:05 ` Luke Kenneth Casson Leighton
2020-03-29 19:32 ` Immanuel, Yehowshua U
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to='CAPweEDx6eo5TS1DJH0XcqLkRQn930RFM=Ve4Q=0maJkgL6b7pA@mail.gmail.com' \
--to=lkcl@lkcl.net \
--cc=libre-riscv-dev@lists.libre-riscv.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Libre RISC-V Mailing list Archives (accessible via public-inbox)
Archives are clonable: git clone --mirror https://inbox.libre-soc.org/libre-riscv-dev
Example config snippet for mirrors
AGPL code for this site: git clone https://public-inbox.org/public-inbox.git