Bug 274 - Investigate how BSV performs Formal Verification and what can be Applied to FPUs
Summary: Investigate how BSV performs Formal Verification and what can be Applied to FPUs
Status: CONFIRMED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: Lowest minor
Assignee: Yehowshua
URL:
Depends on:
Blocks:
 
Reported: 2020-04-01 17:26 BST by Yehowshua
Modified: 2020-06-07 00:22 BST (History)
1 user (show)

See Also:
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:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
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.