Professur für Betriebssysteme - Universität Freiburg

Name	Alexander Konrad
Adresse	Technische Fakultät Albert-Ludwigs-Universität Georges-Köhler-Allee 51 79110 Freiburg
Büro	Gebäude 51, Raum 02...031
Telefon	+49 (0) 761 203 8088
eMail	konrada@informatik.uni-freiburg.de

Alexander Konrad

Jahre: 2023 | 2022 | 2021 | 2020

2023

Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler
Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization (extended abstract)
2023 MBMV
KurzfassungRecent methods based on Symbolic Computer Algebra (SCA) have shown great success in formal verification of multipliers and -- more recently -- of dividers as well. Here we give an overview of our work published in [1-3] which enhances SCA-based verification by the computation of satisfiability don't cares for so-called (Extended) Atomic Blocks (EABs) and by Delayed Don't Care Optimization (DDCO) for optimizing polynomials during backward rewriting. The optimization is reduced to Integer Linear Programming (ILP). Whereas the basic methods using SCA failed for divider verification, using those novel methods we are able to verify (formally and fully automatically) large gate level implementations of several divider architectures (with bit widths up to 512).

Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler
Divider Verification Using Symbolic Computer Algebra and Delayed Don't Care Optimization
2022 Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD), TU Wien Academic Press
KurzfassungRecent methods based on Symbolic Computer Algebra (SCA) have shown great success in formal verification of multipliers and - more recently - of dividers as well. In this paper we enhance known approaches by the computation of satisfiability don't cares of so-called Extended Atomic Blocks (EABs) and by Delayed Don't Care Optimization (DDCO) for optimizing polynomials during backward rewriting. Using those novel methods we are able to extend the applicability of SCA-based methods to further divider architectures which could not be handled by previous approaches. We successfully apply the approach to the fully automatic formal verification of large dividers (with bit widths up to 512).

Christoph Scholl, Alexander Konrad, Alireza Mahzoon, Daniel Große, Rolf Drechsler
Verifying Dividers Using Symbolic Computer Algebra and Don’t Care Optimization
2021 DATE, IEEE
KurzfassungOur experimental results show that this method is the key for enabling the verification of large and optimized non-restoring dividers (with bit widths up to 512).

Christoph Scholl, Alexander Konrad
Symbolic Computer Algebra and SAT Based Information Forwarding for Fully Automatic Divider Verification
2020 Design Automation Conf., Seiten: 1 - 6
Kurzfassungthe opposite direction. We successfully apply the method to the fully automatic formal verification of large non-restoring dividers.