[libre-riscv-dev] formal verification

[Luke Kenneth Casson Leighton]

---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68

On Wed, Feb 27, 2019 at 2:46 PM Hendrik Boom <hendrik at topoi.pooq.com> wrote:

> Formal verification means to produce a machine-checked mathematical
> proof of correctness.
>
> It's not trivial to do.

 indeed.  it's why bluespec decided to write a formal spec in BSV,
which as you no doubt know is written in haskell.  valid programs
written in BSV that compile successfully to verilog are formally
*guaranteed* mathematically 100% to be synthesiseable.

 honestly don't know the answer here: therefore, your help really appreciated.

l.