Research
- Formal verification of sequential Galois Field arithmetic circuits using algebraic geometry
- Successfully verifying 99-bit Reyhani-Hasan multiplier which was intractable;SINGUALR codes here
- Expand to FSM rechability checking;Download benchmarks not fully automated
- UNSAT core extraction for polynomials using Groebner basis algorithm
- Invent an UNSAT core extraction method with heuristics working in any polynomial ring;CNF benchmarks(with automated tool) and non-CNF benchmarks(please use the tool manually) Note: both require Singular installed!
Publication
- Formal Verification of Sequential Galois Field Arithmetic Circuits using Algebraic Geometry.
Xiaojun Sun, Priyank Kalla, Tim Pruss, Florian Enescu. In IEEE Design, Automation and
Test in Europe Conference (DATE) 2015, Grenoble
- Finding Unsatisfiable Cores of a Set of Polynomials using the Groebner Basis Algorithm.
Xiaojun Sun, Irina Ilioaea, Priyank Kalla, Florian Enescu. In Principles and Practice of Constraint Programming (CP) 2016, Accepted, to be presented in September 2016, Toulouse
- Word-level Traversal of Finite States Machines using Algebraic Geometry.
Xiaojun Sun, Priyank Kalla, Florian Enescu. In IEEE High-Level Design Validation and Test Workshop (HLDVT) 2016,
Accepted, to be presented in October 2016, Santa Cruz