[Comb] Add Truth Table Simplification Pass

[MrRoy09]

Adds dedicated Simplification Pass and tests for comb.truth_table op:

• Simplifies truth tables with constant output (all true or all false entries) into hw.constant
• Simplifies truth tables that depend on a single input to the corresponding input value
• Adds tests verifying correctness of simplification for comb.truth_table

Related to #9214
Closes #8925

[MrRoy09]

Not sure if isOpTriviallyRecursive is necessary here but I stuck to the original implementation in pr #9214.

[uenoku]

LGTM! Thank you for implementing it as a pass. Maybe in a follow up we can remove operands that don't affect outputs instead of keeping a single operand (e.g. 5 input LUT -> 2 input LUT) but I think the current implementation looks good to me.

Do you mind if you could check few tests case with LEC to make sure the transformation is semantically correct?

circt-opt test/Dialect/Comb/simplify-truth-table.mlir -convert-comb -o before.mlir
circt-opt test/Dialect/Comb/simplify-truth-table.mlir --comb-simplify-tt -convert-comb  -o after.mlir
circt-lec --c1 truth_table_middle_input_inverted --c2 truth_table_middle_input_inverted  before.mlir after.mlir --shared-libs=<path_to_libz3.so>

[MrRoy09]

LGTM! Thank you for implementing it as a pass. Maybe in a follow up we can remove operands that don't affect outputs instead of keeping a single operand (e.g. 5 input LUT -> 2 input LUT) but I think the current implementation looks good to me.

Do you mind if you could check few tests case with LEC to make sure the transformation is semantically correct?

circt-opt test/Dialect/Comb/simplify-truth-table.mlir -convert-comb -o before.mlir
circt-opt test/Dialect/Comb/simplify-truth-table.mlir --comb-simplify-tt -convert-comb  -o after.mlir
circt-lec --c1 truth_table_middle_input_inverted --c2 truth_table_middle_input_inverted  before.mlir after.mlir --shared-libs=<path_to_libz3.so>

I got an error when running with -convert-comb (unknown option). I used the following to check for equivalence (--lower-comb instead of -convert-comb) and it passed for all testcases.

circt-opt test/Dialect/Comb/simplify-truth-table.mlir --lower-comb -o before.mlir
circt-opt test/Dialect/Comb/simplify-truth-table.mlir --comb-simplify-tt --lower-comb -o after.mlir
circt-lec --c1=truth_table_middle_input_inverted --c2=truth_table_middle_input_inverted before.mlir after.mlir --shared-libs=/usr/lib/x86_64-linux-gnu/libz3.so
c1 == c2

Please let me know if I need to run the check any other way

[uenoku]

Thanks! I'm going to merge. Thank you for the PR :)