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

Summary.

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

Contents (PDF format)

Bibliography

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