Report assert message with FailedBoundedCheckException

[yupferris]

When using BMC with more than one assert in a design, the model checker can correctly identify violations, but it's difficult to identify which assertion failed. Example output:

[info] - should pass formal checks *** FAILED ***
[info]   chiseltest.formal.FailedBoundedCheckException: [<omitted>] found an assertion violation 0 steps after reset!
[info]   at chiseltest.formal.FailedBoundedCheckException$.apply(Formal.scala:26)
[info]   at chiseltest.formal.backends.Maltese$.bmc(Maltese.scala:84)
[info]   at chiseltest.formal.Formal$.executeOp(Formal.scala:82)
[info]   at chiseltest.formal.Formal$.$anonfun$verify$2(Formal.scala:62)
[info]   at chiseltest.formal.Formal$.$anonfun$verify$2$adapted(Formal.scala:62)
[info]   at scala.collection.immutable.List.foreach(List.scala:333)
[info]   at chiseltest.formal.Formal$.verify(Formal.scala:62)
[info]   at chiseltest.formal.Formal.verify(Formal.scala:34)
[info]   at chiseltest.formal.Formal.verify$(Formal.scala:32)
[info]   at tse.SliceLoadStoreUnitTests.verify(<omitted>.scala:17)
[info]   ...

We previously discussed ways of working around this (particularly, making specific test bench wrappers around the DUT and specifying formal properties on those instead of the DUT itself), but I've since noticed that assert can also accept a message string. Unfortunately, even with a message specified, the above output doesn't change. It would be excellent if that string could be presented as part of the error message.

[Gallagator]

Maybe this is a tad late for you but, looking at this, functionality seems to be mostly written, it's just not accessible by the user. See here.

It seems all SMTModelCheckers are created with performance settings see here but it should be trivial to pass a parameter through to Maltese and instantiate the model checkers so they check each assertion one at a time. (This is where they are created). Note that .btor based engines would be difficult to support.

I think the difficulty with adding this is deciding how we want the user to specify this. Do we want something like:

verify((new MyModule), CVC4EngineAnnotation, CheckAssertionsIndividually)

The engine annotation may need to report back whether it's capable of checking assertions individually and the verification being aborted if not. This would be the case for btormc I believe.