Add CIRCT datapath synthesis benchmarks 2025

[cowardsa]

A collection of QF_BV benchmarks generated by the CIRCT digital circuit synthesis project. The generated SMT problems check the correctness of lowering Verilog benchmarks to efficient gate-level implementations particularly for arithmetic circuits. The digital circuit synthesis makes use of compressor trees (e.g. Wallace/Dadda trees) to perform addition of many inputs in parallel and as part of multiplication circuits.

Each benchmark is sampled at increasing bitwidth (4-bit, 8-bit and 12-bit), to demonstrate the poor scalability of current bit-blasting tools tested (primarily bitwuzla).