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
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.