Proving formal properties

[yupferris]

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!

[ekiwi]

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.

[yupferris]

Thanks for the info!

[Gallagator]

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 :^).

[ekiwi]

• 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.