search

riscv / sail-riscv

Sail RISC-V model
https://lists.riscv.org/g/tech-golden-model
Other
409 stars 150 forks source link

Functional equivalency checking between models #150

Open billmcspadden-riscv opened 2 years ago

billmcspadden-riscv commented 2 years ago

I would like to start a discussion about the need for a method to do a functional equivalency check between 2 models.

As I've started playing around with the RISC-V Sail model, I can see places where I might want to make (what I consider to be) benign changes in the code. As I started doing this, I began to realize the risk in doing so; I might be making something more than an innocuous change in the model, IN THE GOLDEN MODEL THAT DICTATES WHAT THE RISC_V ARCHITECTURE IS. Yes, fear and dread fell upon me

It seems to me that we really need a method that can identify functional changes between 2 models.

In the RTL world, we have tools that allow us to verify that 2 different models (an RTL specification and a logic netlist) are equivalent. This is the kind of check that I'm talking about.

I know this is not an easy problem, but I'm pretty well convinced that we need something of this sort.

Comments are welcome, as always.

Bill Mc.

jrtc27 commented 2 years ago

That's called the theorem prover backends? Part of the whole point of Sail is being able to generate output to feed into theorem provers and formally (in the mathematical sense, not the directed random testing sense) verify whatever you like.

billmcspadden-riscv commented 2 years ago

RIght. Does such a prover exist? I certainly have no desire to do directed random testing; I've left that world.

If such a prover does exist (specifically for the RISCV model), where is it and how do I use it?

If such a prover does not exist, how do I go about learning how to make one?

Inquiring minds want to know....

allenjbaum commented 2 years ago

Ooh, good questions. Specifically, here, it's proving equivalency between two Sail models, which might make life a bit easier.

On Mon, Feb 7, 2022 at 11:50 AM billmcspadden-riscv < @.***> wrote:

RIght. Does such a prover exist? I certainly have no desire to do directed random testing; I've left that world.

If such a prover does exist (specifically for the RISCV model), where is it and how do I use it?

If such a prover does not exist, how do I go about learning how to make one?

Inquiring minds want to know....

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/150#issuecomment-1031854760, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJUKXLHJ52BCGS7RE2DU2APBLANCNFSM5NYMYT4Q . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you are subscribed to this thread.Message ID: @.***>

martinberger commented 2 years ago

Sail currently compiles to the following provers:

They are interactive provers. I imagine you want to prove equivalence between individual functions that you changed, rather than the full model (which is big). There is also some work on a translation to SMT-LIB, which targets SMT-solvers like Z3, but I don't think that can currently translate the full model.

PeterSewell commented 2 years ago

There is also the Isla symbolic execution engine https://github.com/rems-project/isla, which in some cases might be used for this.

peter

On Mon, 7 Feb 2022 at 23:24, Martin Berger @.***> wrote:

Sail currently compiles to HOL4 https://github.com/HOL-Theorem-Prover/HOL Isabelle/HOL https://isabelle.in.tum.de/ Coq https://coq.inria.fr/

They are interactive provers. I imagine you want to prove equivalence between individual functions that you changed, rather than the full model (which is big).

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/150#issuecomment-1032039838, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZUWGMO6LYDS26YZ4ITU2BIEBANCNFSM5NYMYT4Q . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you are subscribed to this thread.Message ID: @.***>

martinberger commented 2 years ago

@PeterSewell Does Isla handle unrestricted recursion?

PeterSewell commented 2 years ago

no - but why would you want to?

On Tue, 8 Feb 2022 at 10:23, Martin Berger @.***> wrote:

@PeterSewell https://github.com/PeterSewell Does Isla handle unrestricted recursion?

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/150#issuecomment-1032446798, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZRJRDJS2MPPGKP3X5LU2DVJRANCNFSM5NYMYT4Q . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you were mentioned.Message ID: @.***>

martinberger commented 2 years ago

Bill wants to prove equivalence of two full models ...

One of the interns I had last summer had some Sail code that was naturally expressed using recursion and wanted to use an SMT solver for equivalence checks.

PeterSewell commented 2 years ago

On Tue, 8 Feb 2022 at 10:36, Martin Berger @.***> wrote:

Bill wants to prove equivalence of two full models ..

Some refactorings would just be of a small part - and in any case, in most architecture specs, there's no general unbounded recursion except (if one has this, which one doesn't always) in the top-level loop. Recursion down the levels of a page table is the most I've seen, bounded by depth 5 or so.

Peter

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/150#issuecomment-1032458184, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZRCYTIFVBFVOHWGAFDU2DWW5ANCNFSM5NYMYT4Q . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you were mentioned.Message ID: @.***>

martinberger commented 2 years ago

I think there is a lot of recursion 'under the hood' in the infinite precision arithmetic and other helpers, that handled by C, Coq etc, depending on backend.

bacam commented 2 years ago

We already use Isla for equivalence checking a particular optimisation inside Isla, although I think it's still limited to pure functions. It would probably be possible to build a more general Isla-based tool for checking some notion of trace equivalence.

Recursion "under the hood" isn't a problem because Isla is passing these built-in operations on to the SMT solver. Of course, if the equivalence is subtle enough then the solver might run into difficulty.