Correctness of Binary 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 3-bit counter. Both cases: without reset input and with reset input are considered. The proof was proposed by Y. Nakamura in [1].

MML Identifier: GATE_2

Contents (PDF format)

Bibliography

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