[libre-riscv-dev] [Bug 274] Investigate how BSV performs Formal Verification and what can be Applied to FPUs

[libre-riscv-dev] [Bug 274] Investigate how BSV performs Formal Verification and what can be Applied to FPUs

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=274

--- Comment #1 from Yehowshua <yimmanuel3@gatech.edu> ---
From what I can tell, formal is mostly applied in BSV to make sure that rules
are activated once their conditions are met.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 274] Investigate how BSV performs Formal Verification and what can be Applied to FPUs

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=274

--- Comment #2 from Yehowshua <yimmanuel3@gatech.edu> ---
The bsc source for generating a floating point adder is here:
https://github.com/B-Lang-org/bsc/blob/master/src/Libraries/Base3-Math/FloatingPoint.bsv#L1822

I'm not sure if it is formally verified.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 274] Investigate how BSV performs Formal Verification and what can be Applied to FPUs

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=274

--- Comment #3 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev