KIT | KIT-Bibliothek | Impressum | Datenschutz

Verification of a GF(2supra(m)) multiplier-circuit for digital signal processing

Hoffmann, Dirk W.; Kropf, Thomas


Hard-wired solutions for Finite Field Arithmetic have become
increasingly important in recent years and are mostly part
of domain specific Digital Signal Processors (DSPs).
We have specified and verified a real-life example of an
array-type multiplier for Finite Field multiplication in
GF(2^m) [1].
The multiplier has been specified in higher-order logic and
correctness has been proven using the HOL98 theorem prover.
Since our model is generic, the correctness results hold for
arbitrary scaled circuits.

Volltext §
DOI: 10.5445/IR/176698
Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Rechnerentwurf und Fehlertoleranz (IRF)
Publikationstyp Forschungsbericht/Preprint
Publikationsjahr 1998
Sprache Englisch
Identifikator ISSN: 1432-7864
KITopen-ID: 176698
Verlag Universität Karlsruhe (TH)
Umfang 17 S.
Serie Interner Bericht. Universität Karlsruhe, Fakultät für Informatik ; 1998, 22
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page