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

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