[SMT] Add HWToSMT and CombToSMT conversion passes

[maerhart]

After adding all the tablegen definitions for the operations, finally, an actual lowering pass!
The documentation of comb semantics is quite sparse (e.g., does the sign of the result of comb.mods follow the dividend or the divisor?; what about division by zero? -> currently div by 0 is defined to be 1 and remainder by 0 returns the first operand), so I just went with the most straightforward lowering that (hopefully) does not violate any of the documented semantics.

[fabianschuiki]

LGTM! Any idea how we would deal with 4- and 9-valued integer types in the future?

[fabianschuiki]

That's a very neat and compact way of getting lots of conversion patterns with similar behavior going. 💯

[maerhart]

Any idea how we would deal with 4- and 9-valued integer types in the future?

I haven't really thought about this yet, but I'm sure there are quite a few ways to encode this in SMT, likely leading to very different solver performance that I cannot really predict. It probably also depends on the semantics of the ops, e.g., does one X in an operand of an addition mean that the whole result is X or only the bits it can strictly affect? The earlier might allow for a more efficient encoding. And I guess there is also some existing literature about this to read through first.

[ekiwi]

I haven't really thought about this yet, but I'm sure there are quite a few ways to encode this in SMT, likely leading to very different solver performance that I cannot really predict.

Afaik most formal tools do not fully model X. If you look at yosys, it generally treats a source of an X as a source of an arbitrary value (i.e. a free variable). This is similar to the gate-level semantics. It makes no attempt to try and replicate the X semantics of the original Verilog. I have heard that the same is true for commercial tools, besides OneSpin which apparently has an optional mode in which is models Verilog X-propagation semantics, however, that mode seems to lead to pretty big performance degradation.

In the firrtl compiler, we would model arbitrary values through a custom IR statement which would yield an arbitrary value on each clock event and we had passes to add these statements around memories and expressions to model their worst case behavior: https://github.com/ucb-bar/firrtl2/tree/main/src/main/scala/firrtl2/backends/experimental/smt/random

So for example a:

node c = div(a, b)

becomes something like:

rand r_0 : clockof(a, b)
node c = mux(eq(b, 0), r_0, div(a, b))

[math-fehr]

Really nice!

[math-fehr]

Is this include required?

[maerhart]

The Passes.h.inc include below includes a unique_ptr, so <memory> has to come from somewhere. Strictly speaking, it still works if we remove this here, but only because circt/Support/LLVM.h transitively includes <memory> via the casting header included in MLIRs support header. Not sure if we should rely on that.

[math-fehr]

Same here

[math-fehr]

Is there a reason for not using BVSub here?

[maerhart]

We don't have a BVSub operation. We can add one, but having both sub and neg is probably not worth it? I chose neg because it's part of the theory, sub is only a syntactic sugar op in the QF_BV logic.