@MISC{FTACELL1.MIZ,
  AUTHOR = {Wasaki, Katsumi},
  TITLE = {Stability of the 4-2 Binary Addition Circuit Cells. Part {I}},
  SECTION1 = {Stability of 4-2 Binary Addition Circuit Cell (TYPE-0)},
  SECTION2 = {Stability of 4-2 Binary Addition Circuit Cell (TYPE-1)},
  SECTION3 = {Stability of 4-2 Binary Addition Circuit Cell (TYPE-2)},
  SECTION4 = {Stability of 4-2 Binary Addition Circuit Cell (TYPE-3)},
  DAY = {28},
  MONTH = {August},
  YEAR = {2008},
  ADDRESS1 = {Shinshu University\\Nagano, Japan},
  SUMMARY = {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 \cite{Vuillemin1983}. 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 \cite{GFACIRC1}.
  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.}}

@article{Vuillemin1983,
 author={Vuillemin, E. Jean},
 journal={the VLSI Journal},
 pages={39--52},
 title={A Very Fast Multiplication Algorithm for VLSI Implementation, Integration},
 volume={1},
 number={1},
 year={1983}}
