Add pono backend to chisel formal for bmc

[Gallagator]

The code is fairly straightforward as much of the existing btor code can be reused. The only real difference between the two btor2 backends is their command line invocation.

---

From here, it should be trivial to add k-induction as one will only need to change the engine from bmc to ind when running pono.

---

Testing

I've run the Keepmax tests on the pono engine as well as btormc and they both succeed. I have also verified that upon editing KeepMax to fail, a counterexample is generated by both engines.

[CLAassistant]

All committers have signed the CLA.

[ekiwi]

This looks really good!

The last remaining step is to add the pono backend to the CI tests. There are two files you need to modify:

1. chiseltest/src/test/scala/chiseltest/formal/FormalBackendOption.scala

   Line 23 in b2d8908

   case Some(unknown) => throw new RuntimeException(s"Unknown formal engine: $unknown")

2. chiseltest/.github/workflows/test.yml

   Line 131 in b2d8908

   backend: [z3, cvc4, btormc, bitwuzla]

In both places, please add pono to the list of backends.

[ekiwi]

Looks like now a couple of tests are failing. You can run the tests locally by launching sbt and then running the following command in the sbt shell:

testOnly chiseltest.** -- -n Formal -Dformal_engine=pono

[Gallagator]

I've noticed the tests are failing - pono seems to be acting very weirdly... I've rerun one of the tests on the .btor file for KeepMax and it's returning 255 when the output is unknown. Here is the output when runing:

$ pono -e bmc -k 3 -v10 --vcd proof.vcd  KeepMax.btor
Parsing BTOR2 file: KeepMax.btor
Solving property: (bvnot (bvand (ite (bvult max out_1) #b1 #b0) (bvand (bvnot reset) _cycles)))
INIT:
(bvand reset (bvnot _resetCount))
TRANS:
(bvand (bvand (bvand (bvand (bvand (bvnot (bvand (bvnot reset) (bvnot _resetCount))) (bvnot (bvand (bvnot _resetCount.next) (bvnot reset.next)))) (ite (= _cycles.next (bvand (bvnot reset) (bvnot (bvand (bvnot _cycles) (bvnot ((_ extract 0 0) (bvadd (concat #b0 _cycles) #b01))))))) #b1 #b0)) (ite (= max.next (ite (= #b1 reset) #b00000000 (ite (bvult max in) in max))) #b1 #b0)) (ite (= max out_1.next) #b1 #b0)) (ite (= _resetCount.next (bvnot (bvand (bvnot _resetCount) (bvnot ((_ extract 0 0) (bvadd #b01 (concat #b0 _resetCount))))))) #b1 #b0))
BMC adding init constraint for step 0
BMC bound_start_: 0
BMC bound_step_: 1

BMC checking at bound: 0
  BMC adding bad state constraint for j = 0
  BMC check at bound 0 unsatisfiable

BMC checking at bound: 1
  BMC reached_k = 0, i = 1
  BMC adding transition for j-1 = 0
  BMC adding bad state constraint for j = 1
  BMC check at bound 1 unsatisfiable

BMC checking at bound: 2
  BMC reached_k = 1, i = 2
  BMC adding transition for j-1 = 1
  BMC adding bad state constraint for j = 2
  BMC check at bound 2 unsatisfiable

BMC checking at bound: 3
  BMC reached_k = 2, i = 3
  BMC adding transition for j-1 = 2
  BMC adding bad state constraint for j = 3
  BMC check at bound 3 unsatisfiable
unknown
b0

$echo $?
255

It's found that the the property is unsatisfiable for each step but somehow returns unknown. This seems like a bug in pono (though I'm a bit wary of saying that). When running with the induction engine -e ind pono returns unsat as we expect.

(thanks for the testing tip and the positive feedback, I'm newish to scala and only use it for chisel)

[ekiwi]

It's found that the the property is unsatisfiable for each step but somehow returns unknown.

It might be worth investigating why it returns that. It is possible that they return unknown because checking that the property holds for k checks does not proof that it always holds. It could also be that something is going wrong with pono.

[ekiwi]

Another thing to be aware of: Last time I checked, which is now about 3 years ago, pono did not support checking more than one property at once. I thus had to combine all properties into one before dispatching to cosa2 (which is what pono used to be called): https://github.com/ucb-bar/maltese-smt/blob/497f7ba057609bf637de6e4fa2de2a80826c0a0f/src/maltese/mc/Btor2ModelChecker.scala#L68

At least that was the idea. Looking at the code it seems like I never actually implemented that part of the system: https://github.com/ucb-bar/maltese-smt/blob/497f7ba057609bf637de6e4fa2de2a80826c0a0f/src/maltese/mc/TransitionSystem.scala#L88

[Gallagator]

Your former suggestion seems to be the case - it returns UNKNOWN for bmc: https://github.com/stanford-centaur/pono/blob/master/engines/bmc.cpp#L53-L77

I verified that this is the offending function by adding a print before the return.

I think I'll need to add a function for the Solver trait which will process the return code and turn the unknown to a pass for bmc. Might not get this done till tommorow, it's getting late over here.

[ekiwi]

I think I'll need to add a function for the Solver trait which will process the return code and turn the unknown to a pass for bmc. Might not get this done till tommorow, it's getting late over here.

No worries. Take your time please and let me know if there are any other things I can help with. Thanks!

[ekiwi]

I think I'll need to add a function for the Solver trait which will process the return code and turn the unknown to a pass for bmc.

Another thought: If the difference between btormc and pono gets too big, it might also make sense to just duplicate the code in Btor2ModelChecker, i.e., split it into a BtormcModelChecker and a PonoModelChecker class and get rid of the whole solver: Solver parameter.

[Gallagator]

I've managed to fix most of the tests by allowing pono to return 255 but some tests are failing assertions because they don't fail at the right step: https://github.com/ucb-bar/chiseltest/blob/main/src/test/scala/chiseltest/formal/UndefinedValuesTests.scala#L21.
I'm not sure much can be done to make pono fail specific steps. Is it not enough for the engine to simply fail?

[ekiwi]

I'm not sure much can be done to make pono fail specific steps. Is it not enough for the engine to simply fail?

BMC should always fail at the exact same step, no matter which engine we are using. If pono fails at a different step than btormc, then that could mean that there is a bug in pono.

It might be a good idea to get the .btor file for one of the tests where pono fails in the wrong cycle (try to find the simplest one). Then run that file manually through btormc and pono to make sure that you get results of different lengths. If that is the case then you could file an issue with pono, presenting your findings.

[Gallagator]

Thanks for the explanation! I've made an issue on pono here: stanford-centaur/pono#320 - unfortunately, it does seem to be producing witnesses of incorrect size (usually one - offs) but it does seem to get to the bad state in the correct step (I think).

Looking at the repo, there has been no activity for at least 2 years so I'm doubtful this will be fixed. What are the next steps? I could take a look into pono to see why it isn't producing a witness with an additional step but I don't fancy my chances.

[ekiwi]

What are the next steps? I could take a look into pono to see why it isn't producing a witness with an additional step but I don't fancy my chances.

Unfortunately that might be the next step. You will definitely learn a lot and I assume that the needed change is going to be fairly small. Maybe if you make a PR with that change we can get someone at Stanford to merge it.

The alternative would be that if you find that pono always returns one step too many, then you could add code to chiseltest that drops the last step from any pono result in order to make things compatible.

[Gallagator]

I've pushed my current changes though not all the tests pass as I've mentioned. I've looked into pono but I haven't yet been able to figure out the cause of the issues. Further, there is a problem I didn't notice before where pono is unable to give an undefined value when the access to memory is out of bounds. Just leaving this comment here in case I make no more progress...

[ekiwi]

I've pushed my current changes though not all the tests pass as I've mentioned.

Awesome. Thanks!

Further, there is a problem I didn't notice before where pono is unable to give an undefined value when the access to memory is out of bounds.

Could you elaborate on that? Which test exactly fails and in what manner?

[Gallagator]

Apologies for the slow response and also being a little vague.

Could you elaborate on that? Which test exactly fails and in what manner?

This is the test I was refering to: https://github.com/ucb-bar/chiseltest/actions/runs/7602647013/job/20703458234?pr=702#step:5:570.
Pono produces an unsat output. I believe this is the test file:

chiseltest/src/test/scala/chiseltest/formal/MemoryTests.scala

Line 200 in b2d8908

class OutOfBoundsValueIs(value: Int) extends Module {

There's also a problem when using shiftregs instead of past where the engine should also fail:
https://github.com/ucb-bar/chiseltest/actions/runs/7602647013/job/20703458234?pr=702#step:5:510

[ekiwi]

This sounds like a lot of problems and - as you said - pono does not seem to be actively maintained, so you would have to debug all of this on your own.

I do remember that your initial goal was to add proofs to chiseltest. If you are still interested in this, you could try to explore one of two alternatives routes:

1. You could try to add support for k-induction with btormc. Proving things with k-induction can be a lot more manual than using PDR, but it can be a lot more reliable and it is supported by btormc (whereas PDR is only supported by pono and some other tools)
2. You could try to make a custom k-induction implementation in chiseltest, similar to how we already implement bmc.

You can find some more information on k-induction in this blog post: https://zipcpu.com/blog/2018/03/10/induction-exercise.html

Please let me know how you want to proceed and how I can help you! Thanks for all the work you already have done!

[Gallagator]

Yes, unfortunately this seemingly easy task has blown up right in my face. I did indeed only want k induction! I think I'll try to add k-induction support to btormc as that seems to be the easiest way forward. After which I may give custom k-induction a go but it's probably best to go one step at a time.

Thanks for all your guidance and support thus far! I'll see what I can do for chiseltest in the coming week(s).

[ekiwi]

Thanks for all your guidance and support thus far! I'll see what I can do for chiseltest in the coming week(s).

Sounds great! Please feel free to ask if there is anything blocking you or you get stuck. Feel free to email me as well.

[Gallagator]

Closing as we've reached a bit of a dead end - may be worth visiting in future if pono sees any future activity.