Add k-induction for SmtModelCheckers

[Gallagator]

Reused much of the BMC code.

• Perform BMC for cycles [0..k-1]
• Asserted constraints for cycles [n..n + k]
• Asserted assumptions for cycles [n..n + k-1]
• Checked the negation of the assertions for cycle n + k

I think I've done much of the initial work to support k-induction for SmtModelCheckers. I believe I initially said I'd support it for btormc first but I was unable to generate a witness for my counter test I introduced which should fail. I have verified that the counter test creates a reasonable witness.

One thing I'm not too sure on is the filtering out of the _resetActive constraint during the inductive step because it does seem like a reasonable constraint that someone could write them self. That said, if the constraint were present, the search space would be far too limited. Have I made the correct choice?

There are a few things I'd like to do before this unmarking this as a draft

• Fix TODOs - One being that I filter out the _resetActive constraint by hardcoding its name - I don't think this is great. The other is that there is some code that shares common functionality.
• Add additional testing. I believe there are quite a few zipcpu tests/quizzes I can implement

As a final note, this repo has been a joy to work with and thanks for the guidance so far!

[Gallagator]

Hi @ekiwi, it seems one of the tests in Continuous Integration / sbt test on mac (pull_request) fails though I didn't modify anything to do with the test that failed as it doesn't use formal. I'm guessing this is a spurious error.

I'd also like to get some advice on the _resetActive constraint. I'm thinking it shouldn't be present in the induction check as it limits the search space too much. If we truly do need to filter it out, I'm not sure what the best way of doing so is, I could pass it through the call chain to the checkInduction method which would get rid of the hard coding of its name (It also needs to be filtered out when we get the witness).

As a little backstory, I initially tried supporting k-induction through btormc but I was unable to get a sat when running induction. I'm now thinking that's because I gave it the btor model with the _resetActive constraint. I'm thinking I could run the bmc check with that constraint and then the induction check without it.

[ekiwi]

Hi @ekiwi, it seems one of the tests in Continuous Integration / sbt test on mac (pull_request) fails though I didn't modify anything to do with the test that failed as it doesn't use formal. I'm guessing this is a spurious error.

Yes, should be spurious. I am rerunning the jobs.

[ekiwi]

I'd also like to get some advice on the _resetActive constraint.

You should not have to remove any constraints. However, when you do the induction check, you need to remove all initial values. The way that the reset constraint works is that it creates a state which is initialized to a concrete value in order to denote the first cycle of execution. We then use this state to formulate a constraint that says that reset has to be active in the first cycle.

Now when you do the induction check, you are not starting from the first, but from an arbitrary step. Thus you need to make sure that none of the states have an initial value. To do so you have two options:

1. You could modify the enc.init(ctx) method to take a parameter that says whether initial state values should be applied. You then will have to change

   chiseltest/src/main/scala/chiseltest/formal/backends/smt/CompactSmtEncoding.scala

   Line 30 in 0783f27

   ctx.assert(BVFunctionCall(stateInitFun, List(s0), 1))

   and

   chiseltest/src/main/scala/chiseltest/formal/backends/smt/UnrollSmtEncoding.scala

   Line 25 in 0783f27

   ctx.runCommand(DefineFunction(at(state.name, 0), Seq(), signalsAndStatesAt(value, 0)))

   .
2. You make a modified copy of the transition system in which you set all init fields of all states to None.

[Gallagator]

When the simulator is run, the _resetActive constraint is violated in the induction case as we start from an arbitrary step. The message ERROR: Constraint #_resetActive was violated! will be printed every time an induction check fails. I suppose this ok, but I'm not sure we can prevent it from noticing the constraints are violated unless we remove the _resetActive constraint. Maybe it could be classed as something entirely different.

[Gallagator]

Hi @ekiwi, any chance I could get a review on this? I think the verilator checks timed out again but I think everything else is fine. I understand you're very busy so no rush!

[ekiwi]

Thanks for the reminder! I will try to have a look at the PR tomorrow. Please ping me again if I do not respond by Thursday.

Thanks and sorry I haven't responded sooner

[ekiwi]

This looks great! Thanks a lot!

[Gallagator]

Happy to have helped!