[libre-riscv-dev] formal verification

[Jacob Lifshay]

On Wed, Mar 20, 2019, 00:27 Luke Kenneth Casson Leighton <lkcl at lkcl.net>
wrote:

> On Wed, Mar 20, 2019 at 7:14 AM Jacob Lifshay <programmerjake at gmail.com>
> wrote:
>
> > All the legalese aside, we're going to try to be compliant with the
> RISC-V
> > specs.
>
> it's more than that, jacob: where it is not necessary for us to be
> non-compliant (because there is no business case for doing so), we
> must *not* be non-compliant.  to reiterate: where we have no *need* to
> be non-compliant, we *cannot* be non-compliant.
>

Just to be clear, ogurksjnv, we are specifically aiming for RV64GC
compatibility (legal issues notwithstanding). We are going to be
implementing additional standard/custom extensions as well, one of which is
SimpleV (or some variant thereof). We are planning on implementing the S
extension from the privileged spec.
We will most likely implement either the B extension or some similar custom
extension (only if the B extension is not ready in time).

We are most likely going to not implement the V extension.

We will be testing our processor, and, most likely will use formal methods
to mathematically prove that we implemented the processor and memory system
correctly.

Jacob

>