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

Correctness of a Cyclic Redundancy Check Code Generator


Yuguang Yang
Shinshu University, Nagano
Katsumi Wasaki
Shinshu University, Nagano
Yasushi Fuwa
Shinshu University, Nagano
Yatsuka Nakamura
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.

MML Identifier: GATE_4

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

Contents (PDF format)

  1. Correctness of Division Circuits with 12-bit Register and 16-bit Register
  2. Correctness of CRC Circuits with Generator Polynomial of Degree 12 and 16

Bibliography

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

Received April 16, 1999

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