I believe BSV can generate formally verified adders.
I will soon take a look at how it handles formal verification.
This is mainly a research/investigation bug.
From what I can tell, formal is mostly applied in BSV to make sure that rules are activated once their conditions are met.
The bsc source for generating a floating point adder is here:
I'm not sure if it is formally verified.
(In reply to Yehowshua from comment #1)
> From what I can tell, formal is mostly applied in BSV to make sure that
> rules are activated once their conditions are met.
it's... complicated. the "rules" are a bit like pre-conditions from
advanced (very obscure) software engineering languages.
in combination with extremely strict (strong) typing (which i can tell
you from experience MASSIVELY interferes with and impedes development
progress), the end result is code that is absolutely 100% guaranteed
to be synthesiseable.
it's actually stronger than that: because they are using Haskell, they
have an internal Formal Correctness Proof that a program that compiles
is 100% *mathematically* guaranteed to be gate-level synthesiseable.
verilog as you know is completely incapable of making such guarantees.
this tends to fit with what you've heard about it being "able to
generate formally verified adders".
*actual* formal verification however i believe is done slightly differently,
and i've not investigated it, other than i saw a talk by Nihil for a
RVF presentation, and the code that he wrote looked extremely obvious and
easy to understand and read. the "magic" i expect was happening somewhere
behind the scenes.