ics.jku.at Open in urlscan Pro
140.78.104.153  Public Scan

Form analysis
0 forms found in the DOM

Text Content

 * Home
 * Team
 * Research
 * Projects
 * Publications
 * Teaching
 * Awards


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: theory and practical implementation (Form. Methods Syst. Des.
   2024)
 * 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: www.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!

JKU Institute for Complex Systems, Altenberger Straße 69, 4040 Linz, Austria,
Tel.: +43 732 2468 4561 – Imprint