Combining of Multi Cell Circuits

Grzegorz Bancerek

Bialystok Technical University

Shin'nosuke Yamaguchi

Shinshu University, Nagano

Yasunari Shidama

Shinshu University, Nagano

Summary.

In this article we continue the investigations from [10] and [2] of verification of a circuit design. We concentrate on the combination of multi cell circuits from given cells (circuit modules). Namely, we formalize a design of the form \\ \input CIRCCMB2.PIC and prove its stability. The formalization proposed consists in a series of schemes which allow to define multi cells circuits and prove their properties. Our goal is to achive mathematical formalization which will allow to verify designs of real circuits.

MML Identifier: CIRCCMB2

Contents (PDF format)

1. One Gate Circuits
2. Defining Multi Cell Circuit Structures
3. Input of Multi Cell Circuit
4. Defining Multi Cell Circuits
5. Stability of Multi Cell Circuit

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek and Yatsuka Nakamura. Full adder circuit. Part I. Journal of Formalized Mathematics, 7, 1995.

[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[4] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[5] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.

[6] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.

[7] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.

[8] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[9] Jaroslaw Kotowicz. The limit of a real function at infinity. Journal of Formalized Mathematics, 2, 1990.

[10] Yatsuka Nakamura and Grzegorz Bancerek. Combining of circuits. Journal of Formalized Mathematics, 7, 1995.

[11] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, I. Journal of Formalized Mathematics, 6, 1994.

[12] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, II. Journal of Formalized Mathematics, 6, 1994.

[13] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, II. Journal of Formalized Mathematics, 7, 1995.

[14] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[15] Andrzej Trybulec. Many-sorted sets. Journal of Formalized Mathematics, 5, 1993.

[16] Andrzej Trybulec. Many sorted algebras. Journal of Formalized Mathematics, 6, 1994.

[17] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[18] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.