Bug 194 - A nmigen-based RISC-V Formal correctness proof suite is needed
Summary: A nmigen-based RISC-V Formal correctness proof suite is needed
Status: RESOLVED INVALID
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
URL:
Depends on:
Blocks: 158
  Show dependency treegraph
 
Reported: 2020-03-02 13:09 GMT by Luke Kenneth Casson Leighton
Modified: 2021-01-08 06:10 GMT (History)
1 user (show)

See Also:
NLnet milestone: NLNet.2019.10.Formal
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: 158
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 Luke Kenneth Casson Leighton 2020-03-02 13:09:59 GMT
A general-purpose Formal correctness test suite is needed for
RISC-V, improving on https://github.com/SymbioticEDA/riscv-formal
Comment 1 Luke Kenneth Casson Leighton 2021-01-08 06:09:50 GMT
the decision not to do RISCV was long after the MoU was signed.  at the time it was signed we were still sending in-good faith requests to resolve conflicts of interest with our transparency and funding obligations to NLnet.

the RISCV Foundation repeatedly failed under Trademark Law requirements to respond to in-good faith responsible requests to allow participation in the augmentation of the RISCV ISA, without compromising our obligations to NLnet.

individuals not acting on behalf of the RISCV Foundation but with close ties to the Founders and the RISCV Board of Directors repeatedly disregarded our rationale that "Custom Extensions" for something as high profile as a hybrid 3D GPU which requires upstreaming of all software components is clearly not appropriate (Custom RISCV Extensions are prohibited from upstreaming and must remain privately maintained: clearly this conflicts with high profile public 3D GPU APIs and drivers developed as "Works for the Public Good").  these individuals' unthinking responses, publicly visible and clearly accessible and readable by Members of the RISCV Foundation Board of Directors, actively interfered with our efforts to resolve the conflicts.

To proceed without being included in the process that was available to all other RISCV participants (once they had signed an agreement containing secrecy clauses that conflict with our obligations to NLnet) would have been irresponsible.
The repeated failures to respond left us discriminated against under Trademark Law, yet unless we were included we could not begin the process of proposing our augmentations to the RISCV ISA needed to support the creation of a Hybrid 3D CPU/GPU/VPU, because access to even the documentation on how to begin that process was shrouded in secrecy and required signing an agreement that contained conflicts of interest.

All of this was explained reasonably, in good faith, multiple times.

Not once in 18 months did we receive a response.

The RISCV Foundation repeated systematic failures to respond, in direct violation of Trademark Law obligations to act in a FRAND manner regarding our enquiries even as to how we may proceed to resolve these conflicts left us no choice but to abandon 18+ months work, much of it funded by NLnet and the underlying EU Horizon 2020 Grant, and some of it personally funded.

We have no choice but to close this bugreport as invalid.