[libre-riscv-dev] POWER9 formal correctness proofs collaboration

[Luke Kenneth Casson Leighton]

example:

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/formal/proof_main_stage.py;hb=HEAD

one of the critical aspects of LibreSOC is that we do not want to be the
ones who declare our code to be "correct" to our customers: we want our
customers to be in a position to independently confirm it for themselves,
at every level.

consequently, we have to develop Formal Correctness proofs not as an
afterthought but as part of the real time day to day development process.

this leaves behind a morass of code that, strategically, is of enormous
value to other teams.

yet because of there being no defined interfaces, we are "getting on with
it" and consequently the code is designed to interface to LibreSOC's
internal data structures.

as thinge stand, other teams, therefore, would need to do quite a lot of
work before being able to take advantage of the proofs.

in RISC-V, SymbioticEDA set about defining a de-facto industry standard
interface, through which access to the internals of the core to be tested
could "plug in" any given Formal Proof. full access to registers,
pipelines, instructions, memory subsystem, everything, in a well-defined
fashion.

https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/rvfi.md

would anyone like to collaborate on defining a similar such interface, for
POWER9 teams to be able to formally validate their cores?

if so, we have tax deductible donations from NLNet if code is written that
happens to be directly useable for our project.  if we take EUR as the
unit, i believe there are up to around 9,000 such gifts available :)

also, second question, has a Compliance Working Group (and mailing list)
been established, as this is the kind of thing that should probably be
raised there (defining an interface, that is).

l.




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