@MISC{GATE_3.MIZ,
  AUTHOR = {Yang, Yuguang and Wasaki, Katsumi and Fuwa, Yasushi and Nakamura, Yatsuka},
  TITLE = {Correctness of {J}ohnson Counter Circuits},
  DAY = {13},
  MONTH = {March},
  YEAR = {1999},
  ADDRESS1 = {Shinshu University\\Nagano},
  ADDRESS2 = {Shinshu University\\Nagano},
  ADDRESS3 = {Shinshu University\\Nagano},
  ADDRESS4 = {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.}}

