SCA Verification - GENMUL

GenMul

We present the multiplier generator GenMul, which outputs multiplier circuits in Verilog. The input size of a multiplier and each multiplier stage can be configured with GenMul. In addition, GenMul is open source under MIT-license to ease for adding new architectures. Overall, this allows to challenge formal methods as shown by experiments which compare recent verification approaches.

GenMul has been developed in the context of work on formal verification solutions based on Symbolic Computer Algebra (SCA). For an overview see here: sca-verifcation.org.

How to get GenMul

• The C++ code of GenMul is available at GitHub.
• If you just want to generate Verilog files you can also use the web-based version below. We have used the Emscripten toolchain to compile Javascript from our C++ implementation of GenMul.

GenMul Web Generation