[libre-riscv-dev] BlueSpec Floating Point

[Luke Kenneth Casson Leighton]

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

>
>
> Sent from my iPad
>
> > On Mar 29, 2020, at 2:46 PM, Luke Kenneth Casson Leighton <lkcl at 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