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
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
Depends on:
Reported: 2020-03-02 13:09 GMT by Luke Kenneth Casson Leighton
Modified: 2022-05-16 10:17 BST (History)
1 user (show)

See Also:
NLnet milestone: NLNet.2019.10.032.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:


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 the Directors
of the RISC-V Foundation 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.  This constitutes
direct violation of Anti-Trust Legislation.

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.

The Members of the RISCV Foundation who publicly engaged in deliberate and
systematic attacks violated Anti-Trust Law.

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