chiseltest icon indicating copy to clipboard operation
chiseltest copied to clipboard

Published 20 hours ago • verified publisher icon ucb-bar

Proving formal properties

Open yupferris opened this issue 1 year ago • 4 comments

Hi! Is there any work/experiments underway to prove formal properties, via eg. k-induction/PDR? From what I've seen so far, the API can only describe safety properties (please correct if I'm wrong), so it seems like at least implementing k-induction isn't that far away from what's currently there for BMC.

Thanks!

yupferris avatar Jun 20 '23 12:06 yupferris

From what I've seen so far, the API can only describe safety properties (please correct if I'm wrong), so it seems like at least implementing k-induction isn't that far away from what's currently there for BMC.

k-induction would totally be doable to implement. We could also try to interface with model checkers that implement PDR (like pono). However, currently no one is working on this.

ekiwi avatar Jun 20 '23 14:06 ekiwi

Thanks for the info!

yupferris avatar Jun 27 '23 12:06 yupferris

Hi, I'd be interested in picking this issue up. I've been looking around for how to do this and it seems pono has a few APIs:

  • C++: seems least desirable as I reckon C++ interop will be painful.
  • Python: The API seems nice and could potentially be interacted with using scalapy.
  • BTOR2: Potentially the easiest way of integrating the engine as chiseltest seems to already be able to emit .btor2s.

I don't think pono uses an smt-lib interface as the other engines in chiseltest do. So, given these options, I'm leaning towards using the python API but do let me know if you disagree! The formal verification world is certainly a new thing to me!

Let me know if I'm leaving out anything! I'm super keen to help :^).

Gallagator avatar Jan 02 '24 22:01 Gallagator

  • BTOR2: Potentially the easiest way of integrating the engine as chiseltest seems to already be able to emit .btor2s.

That would be the way to go.

I don't think pono uses an smt-lib interface as the other engines in chiseltest do.

There is one engine, btormc which already consumes btor for BMC.

As a first step I would recommend that you try adding pono as a BMC backend. You can look at the code for btormc as a template. There will probably be some peculiarities about pono that you will have to add some code for. Then you could make a PR with your changes and after that you could investigate how to use pono in "proof-mode" instead of only doing BMC.

ekiwi avatar Jan 03 '24 00:01 ekiwi