SCA Verification

This website provides formal verification solutions based on Symbolic Computer Algebra (SCA) for complex arithmetic circuits, such as multipliers.

Papers

Multiplier Verification

• Formal verification of modular multipliers using symbolic computer algebra and boolean satisfiability (DAC 2022)
• RevSCA-2.0: SCA-based formal verification of non-trivial multipliers using reverse engineering and local vanishing removal (TCAD 2022)
• Towards formal verification of optimized and industrial multipliers (DATE 2020)
• RevSCA: Using reverse engineering to bring light into backward rewriting for big and dirty multipliers (DAC 2019)
• PolyCleaner: clean your polynomials before backward rewriting to verify million-gate multipliers (ICCAD 2018) (Received Best Paper Award)
• Formal verification of integer multipliers by combining Gröbner basis with logic reduction (DATE 2016) (Best Paper Candidate)

Divider Verification

• Divider verification using symbolic computer algebra and delayed don’t care optimization (FMCAD 2022)
• Verifying dividers using symbolic computer algebra and don’t care optimization (DATE 2021)

Equivalence Checking

• Equivalence checking using Gröbner bases (FMCAD 2016)

Multiplier Generator GenMul

For GenMul, our multiplier generator, which outputs multiplier circuits in Verilog, please visit: sca-verifcation.org/genmul.

SCA Verification Tools and Benchmarks

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!