Abstract
To evaluate our formal verification method on a real-size calculation circuit, in this article, we continue to formalize the concept of the 4-2 Binary Addition Cell primitives (FTAs) to define the structures of calculation units for a very fast multiplication algorithm for VLSI implementation [11]. We define the circuit structure of four-types FTAs, TYPE-0 to TYPE-3, using the series constructions of the Generalized Full Adder Circuits (GFAs) that generalized adder to have for each positive and negative weights to inputs and outputs [15]. We then successfully prove its circuit stability of the calculation outputs after four-steps. The motivation for this research is to establish a technique based on formalized mathematics and its applications for calculation circuits with high reliability.
MML identifier: FTACELL1, version: 7.9.03 4.108.1028