A Formal Approach to Designing Multiple-Valued Arithmetic Circuits
Kazuya Saito, Naofumi Homma and Takafumi Aoki
This paper proposes a formal approach to designing multiple-valued arithmetic circuits over Galois Fields (GFs). Our method introduces a high-level multiple-valued graph specified by variables and arithmetic formulae over specific GFs. The graph represents arithmetic circuits over GFs in a hierarchical manner. The proposed circuit description is formally verified by symbolic computations such as polynomial reduction using Gröbner Bases. In this paper, we propose the graph representation and show an example of its description and verification. The advantageous effects of the proposed approach are demonstrated through experimental designs of parallel multipliers over Galois field GF(2m) for different word-lengths and irreducible polynomials. An inversion circuit consisting of some multipliers is also designed and verified as a further application. The result shows that the proposed approach has a definite possibility of verifying practical arithmetic circuits where the conventional simulation and verification techniques failed.
Keywords: Arithmetic circuits, formal verification, galois field, computer algebra