1. Formal Verification of Divider Circuits by Hardware Reduction
- Author
-
Yasin, Atif, Su, Tiankai, Pillement, Sébastien, Ciesielski, Maciej, University of Massachusetts [Amherst] (UMass Amherst), University of Massachusetts System (UMASS), Institut d'Électronique et des Technologies du numéRique (IETR), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ), and Grant from the National Science Foundation, award No. CCF-2006465.
- Subjects
[SPI.OTHER]Engineering Sciences [physics]/Other ,[SPI.TRON]Engineering Sciences [physics]/Electronics - Abstract
International audience; The paper introduces a novel verification methodof gate-level hardware implementation of divider circuits. Themethod, called hardware reduction, accomplishes the verificationby appending the divider circuit with another circuit, which implementsits arithmetic inverse, followed by logic synthesis. If thecircuit under verification is correct, the resulting resynthesizedcircuit becomes trivially redundant (composed of wires or buffersonly). This method outperforms the established SAT-based andequivalence checking techniques and does not require a referencedesign.
- Published
- 2023