Verification of a GF(2supra(m)) multiplier-circuit for digital signal processing
Abstract:
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.
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.
| 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 urn:nbn:de:swb:90-AAA1766981 KITopen-ID: 176698 |
| Verlag | Universität Karlsruhe (TH) |
| Umfang | 17 S. |
| Serie | Interner Bericht. Universität Karlsruhe, Fakultät für Informatik ; 1998, 22 |