Checking formal properties over multiple tests

[yupferris]

Hi! I'm trying out chiseltest's formal capabilities. It's quite easy to set up and use, and I'm able to check some simple properties. Yay!

However, I'm a bit concerned with debugging workflow. For example, if I have a particular property I'd like to focus on, it would be nice to only verify that property in a specific test, similar to how unit tests are usually only focused on a single thing. As it is now, it seems like verify will check all properties, and some might be red herrings and/or TODOs while focusing on another, so it'd be nice to rule those out (without having to comment them out or something like that).

Somewhat related is scalability. As I understand it, BMC problems in general scale exponentially in the size of the design. It seems like it would be a good idea to segregate tests which need a large BMC depth from ones that don't to mitigate potential scaling problems (assuming only the cone of influence for the properties is considered, and the rest is culled).

I believe both of the above can be alleviated by wrapping my DUT in other modules and adding specific properties/tests on those, which might not be so bad, but seems a bit indirect.

Are there any other recommendations/ideas here?

Thanks!

[ekiwi]

Thanks for your feedback! Right now, if you want to enable/disable assertions without changing the RTL is to make a wrapper module like we do here:

chiseltest/src/test/scala/chiseltest/formal/examples/VGBComparisonOfFormalAndSimulation.scala

Line 25 in b999920

class ShapeProcessorProps extends Module {

It would be possible to add a mechanism to enable / disable properties. However, no one is working on that.

[yupferris]

OK, sounds good, cheers for the linked example/info!