Bug 274

Summary:	Investigate how BSV performs Formal Verification and what can be Applied to FPUs
Product:	Libre-SOC's first SoC	Reporter:	Yehowshua <yimmanuel3>
Component:	Formal Verification	Assignee:	Yehowshua <yimmanuel3>
Status:	RESOLVED FIXED
Severity:	minor	CC:	libre-soc-bugs, lkcl
Priority:	Lowest
Version:	unspecified
Hardware:	PC
OS:	Linux
NLnet milestone:	---	total budget (EUR) for completion of task and all subtasks:	0
budget (EUR) for this task, excluding subtasks' budget:	0	parent task for budget allocation:
child tasks for budget allocation:		The table of payments (in EUR) for this task; TOML format:

Description Yehowshua 2020-04-01 17:26:59 BST

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.

Comment 1 Yehowshua 2020-06-07 00:11:24 BST

From what I can tell, formal is mostly applied in BSV to make sure that rules are activated once their conditions are met.

Comment 2 Yehowshua 2020-06-07 00:19:37 BST

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.

Comment 3 Luke Kenneth Casson Leighton 2020-06-07 00:22:21 BST

(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.