* [libre-riscv-dev] BlueSpec Floating Point @ 2020-03-29 16:09 Immanuel, Yehowshua U 2020-03-29 18:45 ` Luke Kenneth Casson Leighton 0 siblings, 1 reply; 7+ messages in thread From: Immanuel, Yehowshua U @ 2020-03-29 16:09 UTC (permalink / raw) To: Libre-RISCV General Development 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [libre-riscv-dev] BlueSpec Floating Point 2020-03-29 16:09 [libre-riscv-dev] BlueSpec Floating Point Immanuel, Yehowshua U @ 2020-03-29 18:45 ` Luke Kenneth Casson Leighton 2020-03-29 19:02 ` Immanuel, Yehowshua U 2020-03-29 19:03 ` Immanuel, Yehowshua U 0 siblings, 2 replies; 7+ messages in thread From: Luke Kenneth Casson Leighton @ 2020-03-29 18:45 UTC (permalink / raw) To: Libre-RISCV General Development 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [libre-riscv-dev] BlueSpec Floating Point 2020-03-29 18:45 ` Luke Kenneth Casson Leighton @ 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 1 sibling, 1 reply; 7+ messages in thread From: Immanuel, Yehowshua U @ 2020-03-29 19:02 UTC (permalink / raw) To: Libre-RISCV General Development 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [libre-riscv-dev] BlueSpec Floating Point 2020-03-29 19:02 ` Immanuel, Yehowshua U @ 2020-03-29 19:03 ` Luke Kenneth Casson Leighton 0 siblings, 0 replies; 7+ messages in thread From: Luke Kenneth Casson Leighton @ 2020-03-29 19:03 UTC (permalink / raw) To: Libre-RISCV General Development 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [libre-riscv-dev] BlueSpec Floating Point 2020-03-29 18:45 ` Luke Kenneth Casson Leighton 2020-03-29 19:02 ` Immanuel, Yehowshua U @ 2020-03-29 19:03 ` Immanuel, Yehowshua U 2020-03-29 19:05 ` Luke Kenneth Casson Leighton 1 sibling, 1 reply; 7+ messages in thread From: Immanuel, Yehowshua U @ 2020-03-29 19:03 UTC (permalink / raw) To: Libre-RISCV General Development 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [libre-riscv-dev] BlueSpec Floating Point 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 0 siblings, 1 reply; 7+ messages in thread From: Luke Kenneth Casson Leighton @ 2020-03-29 19:05 UTC (permalink / raw) To: Libre-RISCV General Development 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [libre-riscv-dev] BlueSpec Floating Point 2020-03-29 19:05 ` Luke Kenneth Casson Leighton @ 2020-03-29 19:32 ` Immanuel, Yehowshua U 0 siblings, 0 replies; 7+ messages in thread From: Immanuel, Yehowshua U @ 2020-03-29 19:32 UTC (permalink / raw) To: Libre-RISCV General Development 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
end of thread, back to index Thread overview: 7+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2020-03-29 16:09 [libre-riscv-dev] BlueSpec Floating Point Immanuel, Yehowshua U 2020-03-29 18:45 ` Luke Kenneth Casson Leighton 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
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