[circt-mc] WIP: Introduce the circt-mc tool

[TaoBi22]

This is a WIP PR, created for the purpose of discussion as mentioned here

This PR is stacked on #4544 (and therefore transitively stacked on #3991), and introduces circt-mc, a bounded model checker for (currently) CIRCT's RTL dialects. This builds upon the circt-lec codebase substantially, using z3, but adds support for seq dialect register operations. There are a few remaining changes to make - some LEC specific artifacts remain in the SMT library and CMake files, the algorithm likely needs some fixes (e.g. it currently assumes all comb operations in the IR are topologically sorted) and crucially there is currently no front-end to specify properties to check. This omission is deliberate as in my opinion the front-end warrants some discussion.

I would personally argue that a new dialect for specifying properties would be appropriate here - the set of properties we'd be looking to represent is probably similar to the set of properties representable with SystemVerilog Assertions. This would probably require operations to represent adding a property, along with temporal operators - it might be wise to take some inspiration from SVA here. This dialect could also contain the appropriate logical operators, but I would say it may be nicer to wrap around a generic SMT dialect - I'm sure some of you will be aware there's been some discussion about such a thing in MLIR, and there is currently some work on implementing something along these lines. However, this is something I'd very much appreciate some more opinions on, so I'd be eager to hear your thoughts about how to best represent these properties!

A few more design decisions worth noting:

• Currently, only one clock in a design is supported. It would be nice to improve this in the future, but multiple clock support leads to very rapid explosion in clause size, since state updates must be modelled symbolically. With just one clock cycle, each transition between states can be a clock update - however, with arbitrary clocks each clock must be represented as a symbol, with the new state of registers becoming ite(clk_edge, new_state, old_state) (where clk_edge indicates a posedge on this register's clock - something like clk && !prev_clk). When this happens every single transition, the slowdown after a large number of clock cycles becomes enormous. This might be manageable by use of an inductive model checking algorithm, but IMO that's a point for future improvement

• Similarly, only synchronous resets are currently supported. In certain circuits, the order of resets is important - this means that for full generality every possible order of resets should be simulated. Naturally this gets problematic if you have a lot of registers that are reset by distinct module inputs. It might be possible to do some kind of smart detection on the design to see whether this is actually a concern, cleaning things up, but there's no obvious nice way to handle this as far as I can think.

• The transformations represented by combinatorial operations all have to be reapplied every transition (for now - this could potentially be optimised), of which there may be a huge amount. Given this, it seemed that using a visitor to visit each of these operations on every transition would involve a significant amount of overhead. Instead, I traded this off for memory footprint - the combinatorial transformations are stored in a list of pairs, containing the necessary values and a lambda function for the transformation. However, this will lead to a pretty big memory footprint when considering large designs. This tradeoff seems most likely worthwhile to me considering the potentially incredibly vast number of iterations that will be performed by this tool, but I'd appreciate thoughts on this, and probably need to do some experimentation. If it turns out the overhead of a visitor is minimal enough that this isn't necessary, or that a longer runtime is preferred over intense memory usage, I'll change this to simply visit the operations.

I'll try and clear up some of the obvious changes that this still needs in the next few weeks - in the meantime, any thoughts/questions appreciated!

[TaoBi22]

Tracking the information above, this tool now has a front-end with the verif dialect - thanks @fabianschuiki!

[mikeurbach]

@TaoBi22 there has been a lot of recent interest in bounded model checking. I'm proposing we talk about this at the CIRCT ODM on 11/29 at 11am PST (19:00 UTC). Would you and anyone from your group who is interested on this be able to join, or have a different day / time in mind that would work?

[TaoBi22]

@mikeurbach Sounds great, I can be there! (Status update on this: got pretty sidelined so left it hanging for much longer than I meant to, finding time where I can at the moment to fix one final memory organisation issue as it's pretty horribly memory-inefficient at the moment then it should finally be ready for review)

[TaoBi22]

Superseding this PR with #6467 now it's ready for review since there's a lot of bloat here!