Affordable Access

SPEAR: Hardware-based Implicit Rewriting for Square-root Circuit Verification

Authors
  • Yasin, Atif
  • Su, Tiankai
  • Pillement, Sébastien
  • Ciesielski, Maciej
Publication Date
Mar 09, 2020
Source
HAL-SHS
Keywords
Language
English
License
Unknown
External links

Abstract

The paper addresses formal verification of gate-levelsquare-root circuits. Division and square root functions are alltied to the basic Intel architecture and proving the correctnessof their hardware implementation is of great importance. Incontrast to standard approaches that use SAT or equivalencechecking, our method verifies whether the gate-level square-rootcircuit actually performs a root operation, instead of checkingequivalence with a reference design. The method extends thealgebraic rewriting technique developed earlier for multipliersand significantly improves its efficiency by introducing theconcept of hardware-based rewriting. The tool called SPEAR,developed in this work enables the verification of a 256-bit gatelevelsquare-root circuit with 0.26 million gates in under 18minutes.

Report this publication

Statistics

Seen <100 times