This website provides formal verification solutions based on Symbolic Computer Algebra (SCA) for complex arithmetic circuits, such as multipliers.
Papers
Multiplier Verification
Divider Verification
Equivalence Checking
Multiplier Generator GenMul
For GenMul, our multiplier generator, which outputs multiplier circuits in Verilog, please visit: sca-verifcation.org/genmul.
PolyCleaner
- The binary of PolyCleaner and the benchmarks are avialable at GitHub!
RevSCA
- RevSCA proposes a fast and robust SCA-based verification method integrating dedicated reverse engineering to verify big and dirty multipliers.
- 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.
RevSCA-2.0
- The binary of RevSCA-2.0 and the extended set of benchmarks are avialable at GitHub!