2008 | OriginalPaper | Buchkapitel
An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
verfasst von : Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, Gert-Martin Greuel
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
This paper proposes a new approach for proving arithmetic correctness of data paths in System-on-Chip modules. It complements existing techniques which are, for reasons of complexity, restricted to verifying only the control behavior. The circuit is modeled at the arithmetic bit level (ABL) so that our approach is well adapted to current industrial design styles for high performance data paths. Normalization at the ABL is combined with the techniques of computer algebra. We compute normal forms with respect to Gröbner bases over rings ℤ/
$\left\langle{2^n}\right\rangle$
. Our approach proves tractable for industrial data path designs where standard property checking techniques fail.