Stability of the 4-2 Binary Addition Circuit Cells. Part I

Katsumi Wasaki

Formalized Mathematics (2008)

  • Volume: 16, Issue: 4, page 377-387
  • ISSN: 1426-2630

Abstract

top
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

How to cite

top

Katsumi Wasaki. "Stability of the 4-2 Binary Addition Circuit Cells. Part I." Formalized Mathematics 16.4 (2008): 377-387. <http://eudml.org/doc/266881>.

@article{KatsumiWasaki2008,
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},
author = {Katsumi Wasaki},
journal = {Formalized Mathematics},
language = {eng},
number = {4},
pages = {377-387},
title = {Stability of the 4-2 Binary Addition Circuit Cells. Part I},
url = {http://eudml.org/doc/266881},
volume = {16},
year = {2008},
}

TY - JOUR
AU - Katsumi Wasaki
TI - Stability of the 4-2 Binary Addition Circuit Cells. Part I
JO - Formalized Mathematics
PY - 2008
VL - 16
IS - 4
SP - 377
EP - 387
AB - 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
LA - eng
UR - http://eudml.org/doc/266881
ER -

References

top
  1. [1] Grzegorz Bancerek. König's theorem. Formalized Mathematics, 1(3):589-593, 1990. 
  2. [2] Grzegorz Bancerek and Yatsuka Nakamura. Full adder circuit. Part I. Formalized Mathematics, 5(3):367-380, 1996. 
  3. [3] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. 
  4. [4] Yatsuka Nakamura and Grzegorz Bancerek. Combining of circuits. Formalized Mathematics, 5(2):283-295, 1996. 
  5. [5] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, II. Formalized Mathematics, 5(2):273-278, 1996. 
  6. [6] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, II. Formalized Mathematics, 5(2):215-220, 1996. 
  7. [7] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Formalized Mathematics, 4(1):83-86, 1993. 
  8. [8] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25-34, 1990. 
  9. [9] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37-42, 1996. 
  10. [10] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  11. [11] E. Jean Vuillemin. A very fast multiplication algorithm for VLSI implementation, integration. The VLSI Journal, 1(1):39-52, 1983. 
  12. [12] Katsumi Wasaki and Pauline N. Kawamoto. 2's complement circuit. Formalized Mathematics, 6(2):189-197, 1997. 
  13. [13] Edmund Woronowicz. Many-argument relations. Formalized Mathematics, 1(4):733-737, 1990. 
  14. [14] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990. 
  15. [15] Shin'nosuke Yamaguchi, Katsumi Wasaki, and Nobuhiro Shimoi. Generalized full adder circuits (GFAs). Part I. Formalized Mathematics, 13(4):549-571, 2005. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.