Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

Correctness of Johnson Counter Circuits

Yuguang Yang
Shinshu University, Nagano
Katsumi Wasaki
Shinshu University, Nagano
Yasushi Fuwa
Shinshu University, Nagano
Yatsuka Nakamura
Shinshu University, Nagano


This article introduces the verification of the correctness for the operations and the specification of the Johnson counter. We formalize the concepts of 2-bit, 3-bit and 4-bit Johnson counter circuits with a reset input, and define the specification of the state transitions without the minor loop.

MML Identifier: GATE_3

The terminology and notation used in this paper have been introduced in the following articles [1]

Contents (PDF format)


[1] Yatsuka Nakamura. Logic gates and logical equivalence of adders. Journal of Formalized Mathematics, 11, 1999.

Received March 13, 1999

[ Download a postscript version, MML identifier index, Mizar home page]