[libre-riscv-dev] formal verification

[Luke Kenneth Casson Leighton]

On Wed, Mar 20, 2019 at 7:58 AM Jacob Lifshay <programmerjake at gmail.com> wrote:

> We will most likely implement either the B extension or some similar custom
> extension (only if the B extension is not ready in time).

 just realised that here we also have to be extra-careful:

* if the B extension happens to fit our requirements, and is ready,
great.  we implement it, conform to it, all is good.

* If the B extension is *not* ready, then we implement a custom extension.

* If the B extension happens **NOT** repeat **NOT** to fit our
requirements, then we have two options:

(1) to implement full compliance with the B extension with ADDITIONAL
and SEPARATE custom instructions that have absolutely nothing to do
with the B extension

(2) to implement a VARIATION of the B extension that does NOT conform
to the B extension standard.

(2) is an absolute last resort option, where it will potentially be
possible to use something that i developed called
"mvendorid-marchid-isamux" which, in an identical fashion to how
PowerPC and other systems may *dynamically* switch the meaning of
instructions between big-endian and little-endian *at runtime*, would
allow us to flip between "conformant" and "non-conformant" instruction
meanings.  this however would be a royal nuisance to implement.

if we are forced into a situation of having to go down this route, it
is absolutely, absolutely essential that we give full, public and
formal notice of having been forced to proceed in this fashion, wait
for there to be absolute stone-cold silence from the RISC-V Foundation
(which will be an indication of their violation of the FRAND
requirements of Trademark Law), and *only then* would we be free and
clear to RELUCTANTLY and OUT OF NECESSITY ONLY, to proceed with a
conflicting variant.

avoiding this route is... how to say... "A Good Idea (tm)" as it will
be a pain in the neck.

however, given that we have not been able to participate in the
xBitManip Working Group (or any Working Group of any kind), we have
absolutely no idea if the B Extension is suitable for the hybrid
requirements of a CPU / GPU / VPU.

l.