@MISC{GATE_4.MIZ,
  AUTHOR = {Yang, Yuguang and Wasaki, Katsumi and Fuwa, Yasushi and Nakamura, Yatsuka},
  TITLE = {Correctness of a Cyclic Redundancy Check Code Generator},
  SECTION1 = {Correctness of Division Circuits with 12-bit Register and 16-bit Register},
  SECTION2 = {Correctness of CRC Circuits with Generator Polynomial of Degree 12 and 16},
  DAY = {16},
  MONTH = {April},
  YEAR = {1999},
  ADDRESS1 = {Shinshu University\\Nagano},
  ADDRESS2 = {Shinshu University\\Nagano},
  ADDRESS3 = {Shinshu University\\Nagano},
  ADDRESS4 = {Shinshu University\\Nagano},
  SUMMARY = {We prove the correctness of the division circuit and the CRC (cyclic redundancy
   checks) circuit by verifying the contents of the register after one shift.
   Circuits with 12-bit register and 16-bit register are taken as examples.
   All the proofs are done formally.}}

