[libre-riscv-dev] BlueSpec Floating Point

Immanuel, Yehowshua U yimmanuel3 at gatech.edu
Sun Mar 29 20:02:01 BST 2020

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.

More information about the libre-riscv-dev mailing list