Till innehåll på sidan

Daniela Ritirc: On the problem of arithmetic circuit verification using computer algebra

Tid: Må 2018-04-23 kl 12.00

Plats: Room 4523, Lindstedtsvägen 5, KTH

Medverkande: Daniela Ritirc, Johannes Kepler Universität Linz

Exportera till kalender

PRACTICALITIES

 Lunch is served at 12:00 noon (register at tinyurl.com/TCS180423  at the latest the Saturday before, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for 1½-2 hours of more technical discussions.

ABSTRACT

Verification of arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still needs substantial manual effort. Approaches based on SAT or on decision diagrams seem to be unable to solve this problem in a reasonable amount of time. The currently most effective approach uses techniques from computer algebra. In this approach a circuit is modeled as a set of pseudo-boolean polynomials and it is checked if the given word-level specification is implied by these circuit polynomials. We give a rigorous formalization of this approach including soundness and completeness arguments. We improve this approach using an incremental column-wise verification technique which splits the verification problem into smaller more manageable sub-problems. Furthermore rewriting techniques are used which eliminate internal variables from the circuit and thus have a tremendous effect on computation time.