HOME | CONTACT | Switch DE

Logo Universtity of Bremen
LOGO AGRA | AG Rechnerarchitektur



Group of Computer Architecture / AGRA | Computer Science | Faculty 03 | University of Bremen

SCA Verification


You can select information about our approaches for:

PolyCleaner

RevSCA

DyPoSub

GenMul



PolyCleaner

Screenshot PolyCleaner The paper introduces a verification method based on Symbolic Computer Algebra (SCA) and presents a new theory for the origin of vanishing monomials, redundant monomials which lead to an monomial explosion for non-trivial multipliers. The implemented SCA-verifier PolyCleaner is able to prove the correctness for non-trivial million-gate multipliers where the other state-of-the-art methods failed.

For PolyCleaner we received the Best Paper Award at the International Conference on Computer Aided Design (ICCAD) 2018.

How to get PolyCleaner
  • The binary of PolyCleaner and the benchmarks are avialable at GitHub!
References





RevSCA

Screenshot RevSCA RevSCA proposes a fast and robust SCA-based verification method integrating dedicated reverse engineering to verify big and dirty multipliers.

How to get RevSCA
  • The binary of RevSCA and the benchmarks are avialable at GitHub!

Recently, we have improved RevSCA to also support signed multipliers and we have also optimized the implementation. This new version is called RevSCA-2.0.

How to get RevSCA-2.0
  • The binary of RevSCA-2.0 and the extended set of benchmarks are avialable at GitHub!
References





DyPoSub

DyPoSub takes advantage of dynamic substitution ordering in combination with local vanishing removal and reverse engineering to verify optimitzed and industrial multipliers.

How to get DyPoSub
  • We make DyPoSub available on GitHub soon.
References




GenMul

Screenshot 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.


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

Multiplier size:


Multiplicand size:


Partial product generator:


Partial Product Accumulator:


Final stage adder:



Press the generate button to start the generation.
Attention: In case of large multiplier/multiplicand sizes your browser may runs for several minutes.


©2023 | Group of Computer Architecture | Contact | Legal & Data Privacy