Published Online: May 29, 2020
Page range: 65 - 77
Accepted: Dec 30, 2019
DOI: https://doi.org/10.2478/forma-2020-0005
Keywords
© 2020 Katsumi Wasaki, published by Sciendo
This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 License.
To evaluate our formal verification method on a real-size calculation circuit, in this article, we continue to formalize the concept of the 7-3 Compressor (STC) Circuit [6] for Wallace Tree [11], to define the structures of calculation units for a very fast multiplication algorithm for VLSI implementation [10]. We define the circuit structure of the tree constructions of the Generalized Full Adder Circuits (GFAs). We then successfully prove its circuit stability of the calculation outputs after four and six steps. The motivation for this research is to establish a technique based on formalized mathematics and its applications for calculation circuits with high reliability, and to implement the applications of the reliable logic synthesizer and hardware compiler [5].