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!