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

by
Yuguang Yang,
Katsumi Wasaki,
Yasushi Fuwa, and
Yatsuka Nakamura

MML identifier: GATE_4
[ Mizar article, MML identifier index ]

```environ

vocabulary GATE_1;
notation GATE_1;
constructors GATE_1, XBOOLE_0;

begin

::g0,g1,g2,g3:

:: Correctness of Division Circuits with 12-bit Register and 16-bit Register
::
:: Assumptions:
:: g0,g1,g2,...,g12: the coefficients of divident polynomial;
:: a0,a1,a2,...,a11: the present state of register;
:: p: input;
:: b0,b1,b2,...,b11: the state of register with input p;
:: A=(a11, a10, ..., a1, a0), B=(b11, b10, ..., b1,b0);
:: G=(g12,g11,g10,...,g1,g0);
:: A + B = (a11+b11, a10+b10, ..., a1+b1, a0+b0);
:: note: the operator + here means exclusive or.
::
:: In a division circuit, a shift is expected to complete one step division by
:: divident polynomial. So we can derive the relation of A, B, G and p as following:
::   A*2+p=G*a11+B
:: here, A*2=(a11, a10, ..., a1, a0)*2=(a11, a10, ..., a1, a0,0),
::       G*a11=(g12 & a11, g11 & a11, g10 & a11,...,g1 & a11, g0 & a11).

theorem :: GATE_4:1
for g0,g1,g2,g3,g4,g5,g6,g7,g8,g9,g10,g11,g12,
a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,
b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,
p being set holds
\$g0 & \$g12 &
(\$b0 iff \$XOR2(p,AND2(g0,a11)))&
(\$b1 iff \$XOR2(a0,AND2(g1,a11)))&
(\$b2 iff \$XOR2(a1,AND2(g2,a11)))&
(\$b3 iff \$XOR2(a2,AND2(g3,a11)))&
(\$b4 iff \$XOR2(a3,AND2(g4,a11)))&
(\$b5 iff \$XOR2(a4,AND2(g5,a11)))&
(\$b6 iff \$XOR2(a5,AND2(g6,a11)))&
(\$b7 iff \$XOR2(a6,AND2(g7,a11)))&
(\$b8 iff \$XOR2(a7,AND2(g8,a11)))&
(\$b9 iff \$XOR2(a8,AND2(g9,a11)))&
(\$b10 iff \$XOR2(a9,AND2(g10,a11)))&
(\$b11 iff \$XOR2(a10,AND2(g11,a11)))
implies
(\$a11 iff \$AND2(g12,a11)) &
(\$a10 iff \$XOR2(b11,AND2(g11,a11)))&
(\$a9 iff \$XOR2(b10,AND2(g10,a11)))&
(\$a8 iff \$XOR2(b9,AND2(g9,a11)))&
(\$a7 iff \$XOR2(b8,AND2(g8,a11)))&
(\$a6 iff \$XOR2(b7,AND2(g7,a11)))&
(\$a5 iff \$XOR2(b6,AND2(g6,a11)))&
(\$a4 iff \$XOR2(b5,AND2(g5,a11)))&
(\$a3 iff \$XOR2(b4,AND2(g4,a11)))&
(\$a2 iff \$XOR2(b3,AND2(g3,a11)))&
(\$a1 iff \$XOR2(b2,AND2(g2,a11)))&
(\$a0 iff \$XOR2(b1,AND2(g1,a11)))&
(\$p iff \$XOR2(b0,AND2(g0,a11)));

:: Assumptions:
:: g0,g1,g2,...,g16: the coefficients of divident polynomial;
:: a0,a1,a2,...,a15: the present state of register;
:: p: input;
:: b0,b1,b2,...,b15: the state of register with input p;
:: A=(a15, a14, ..., a1, a0), B=(b15, b14, ..., b1,b0);
:: G=(g16,g15,g14,...,g1,g0);
:: A + B = (a15+b15, a14+b14, ..., a1+b1, a0+b0);
:: note: the operator + here means exclusive or.
::
:: In a division circuit, a shift is expected to complete one step division by
:: divident polynomial. So we can derive the relation of A, B, G and p as following:
::   A*2+p=G*a15+B
:: here, A*2=(a15, a14, ..., a1, a0)*2=(a15, a14, ..., a1, a0,0),
::       G*a15=(g16 & a15, g15 & a15, g14 & a15,...,g1 & a15, g0 & a15).

theorem :: GATE_4:2
for g0,g1,g2,g3,g4,g5,g6,g7,g8,g9,g10,g11,g12,g13,g14,g15,g16,
a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,
b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15,
p
being set holds
\$g0 & \$g16 &
(\$b0 iff \$XOR2(p,AND2(g0,a15)))&
(\$b1 iff \$XOR2(a0,AND2(g1,a15)))&
(\$b2 iff \$XOR2(a1,AND2(g2,a15)))&
(\$b3 iff \$XOR2(a2,AND2(g3,a15)))&
(\$b4 iff \$XOR2(a3,AND2(g4,a15)))&
(\$b5 iff \$XOR2(a4,AND2(g5,a15)))&
(\$b6 iff \$XOR2(a5,AND2(g6,a15)))&
(\$b7 iff \$XOR2(a6,AND2(g7,a15)))&
(\$b8 iff \$XOR2(a7,AND2(g8,a15)))&
(\$b9 iff \$XOR2(a8,AND2(g9,a15)))&
(\$b10 iff \$XOR2(a9,AND2(g10,a15)))&
(\$b11 iff \$XOR2(a10,AND2(g11,a15)))&
(\$b12 iff \$XOR2(a11,AND2(g12,a15)))&
(\$b13 iff \$XOR2(a12,AND2(g13,a15)))&
(\$b14 iff \$XOR2(a13,AND2(g14,a15)))&
(\$b15 iff \$XOR2(a14,AND2(g15,a15)))

implies
(\$a15 iff \$AND2(g16,a15)) &
(\$a14 iff \$XOR2(b15,AND2(g15,a15)))&
(\$a13 iff \$XOR2(b14,AND2(g14,a15)))&
(\$a12 iff \$XOR2(b13,AND2(g13,a15)))&
(\$a11 iff \$XOR2(b12,AND2(g12,a15)))&
(\$a10 iff \$XOR2(b11,AND2(g11,a15)))&
(\$a9 iff \$XOR2(b10,AND2(g10,a15)))&
(\$a8 iff \$XOR2(b9,AND2(g9,a15)))&
(\$a7 iff \$XOR2(b8,AND2(g8,a15)))&
(\$a6 iff \$XOR2(b7,AND2(g7,a15)))&
(\$a5 iff \$XOR2(b6,AND2(g6,a15)))&
(\$a4 iff \$XOR2(b5,AND2(g5,a15)))&
(\$a3 iff \$XOR2(b4,AND2(g4,a15)))&
(\$a2 iff \$XOR2(b3,AND2(g3,a15)))&
(\$a1 iff \$XOR2(b2,AND2(g2,a15)))&
(\$a0 iff \$XOR2(b1,AND2(g1,a15)))&
(\$p iff \$XOR2(b0,AND2(g0,a15)));

begin:: Correctness of CRC Circuits with Generator Polynomial of
:: Degree 12 and 16

:: Assumptions:
:: g0,g1,g2,...,g12: the coefficients of generator polynomial;
:: a0,a1,a2,...,a11: the present state of register;
:: p: input;
:: b0,b1,b2,...,b11: the state of register after a shift with input p;
:: A=(a11, a10, ..., a1, a0), B=(b11, b10, ..., b1,b0);
:: G=(g12,g11,g10,...,g1,g0)
:: A + B=(a11+b11, a10+b10, ..., a1+b1, a0+b0);
:: note: the operator + here means exclusive or;
:: A*2=(a11, a10, ..., a1, a0)*2=(a11, a10, ..., a1, a0,0);
:: G*a11=(g12 & a11, g11 & a11, g10 & a11,...,g1 & a11, g0 & a11);
:: 2^11 means 2 to the 11th power.
::
::
:: In a CRC circuit, with assumption that A is the remainder of message M*2^11
:: divided by G, B which is the contents of register after one shift is expected
:: to be the remainder of (M*2 + p)*2^11 divided by G. That means
:: B= mod((M*2 + p)*2^11,G)
::  = mod(M*2^12+ p*2^11,G)
::  = mod(M*2^12,G) + mod(p*2^11,G)
::  = mod(A*2,G) + mod(p*2^11,G)
::  = (A*2+G*a11)+(p*2^11 + G*p);
::
:: Note: The initial state of register can be regarded as M=0.

theorem :: GATE_4:3
for g0,g1,g2,g3,g4,g5,g6,g7,g8,g9,g10,g11,g12,
a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,
b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,
z,p
being set holds
\$g0 & \$g12 & not \$z &
(\$b0 iff \$XOR2(p,a11))&
(\$b1 iff \$XOR2(a0,AND2(g1,b0)))&
(\$b2 iff \$XOR2(a1,AND2(g2,b0)))&
(\$b3 iff \$XOR2(a2,AND2(g3,b0)))&
(\$b4 iff \$XOR2(a3,AND2(g4,b0)))&
(\$b5 iff \$XOR2(a4,AND2(g5,b0)))&
(\$b6 iff \$XOR2(a5,AND2(g6,b0)))&
(\$b7 iff \$XOR2(a6,AND2(g7,b0)))&
(\$b8 iff \$XOR2(a7,AND2(g8,b0)))&
(\$b9 iff \$XOR2(a8,AND2(g9,b0)))&
(\$b10 iff \$XOR2(a9,AND2(g10,b0)))&
(\$b11 iff \$XOR2(a10,AND2(g11,b0)))
implies
(\$b11 iff \$XOR2(XOR2(a10,AND2(g11,a11)),XOR2(z,AND2(g11,p)))) &
(\$b10 iff \$XOR2(XOR2(a9,AND2(g10,a11)),XOR2(z,AND2(g10,p)))) &
(\$b9 iff \$XOR2(XOR2(a8,AND2(g9,a11)),XOR2(z,AND2(g9,p)))) &
(\$b8 iff \$XOR2(XOR2(a7,AND2(g8,a11)),XOR2(z,AND2(g8,p)))) &
(\$b7 iff \$XOR2(XOR2(a6,AND2(g7,a11)),XOR2(z,AND2(g7,p)))) &
(\$b6 iff \$XOR2(XOR2(a5,AND2(g6,a11)),XOR2(z,AND2(g6,p)))) &
(\$b5 iff \$XOR2(XOR2(a4,AND2(g5,a11)),XOR2(z,AND2(g5,p)))) &
(\$b4 iff \$XOR2(XOR2(a3,AND2(g4,a11)),XOR2(z,AND2(g4,p)))) &
(\$b3 iff \$XOR2(XOR2(a2,AND2(g3,a11)),XOR2(z,AND2(g3,p)))) &
(\$b2 iff \$XOR2(XOR2(a1,AND2(g2,a11)),XOR2(z,AND2(g2,p)))) &
(\$b1 iff \$XOR2(XOR2(a0,AND2(g1,a11)),XOR2(z,AND2(g1,p)))) &
(\$b0 iff \$XOR2(XOR2(z, AND2(g0,a11)),XOR2(z,AND2(g0,p))));

:: Assumptions:
:: g0,g1,g2,...,g16: the coefficients of generator polynomial;
:: a0,a1,a2,...,a15: the present state of register;
:: p: input;
:: b0,b1,b2,...,b15: the state of register with input p;
:: A=(a15, a10, ..., a1, a0), B=(b11, b10, ..., b1,b0);
:: G=(g16,g15,g14,...,g1,g0)
:: A + B=(a15+b15, a14+b14, ..., a1+b1, a0+b0);
:: note: the operator + here means exclusive or;
:: A*2= (a15, a14, ..., a1, a0)*2=(a15, a14, ..., a1, a0,0);
:: G*a15=(g16 & a15, g15 & a15, g14 & a15,...,g1 & a15, g0 & a15);
:: 2^15 means 2 to the 15th power.
::
:: In a CRC circuit, with assumption that A is the remainder of message M*2^15
:: divided by G, B which is the contents of register after one shift is expected
:: to be the remainder of (M*2 + p)*2^15 divided by G. That means
:: B= mod((M*2 + p)*2^15,G)
::  = mod(M*2^16+ p*2^15,G)
::  = mod(M*2^16,G) + mod(p*2^15,G)
::  = mod(A*2,G) + mod(p*2^15,G)
::  = (A*2+G*a15)+(p*2^15 + G*p);
::
:: Note: The initial state of register can be regarded as M=0.

theorem :: GATE_4:4
for g0,g1,g2,g3,g4,g5,g6,g7,g8,g9,g10,g11,g12,g13,g14,g15,g16,
a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,
b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15,
z,p
being set holds
\$g0 & \$g16 & not \$z &
(\$b0 iff \$XOR2(p,a15))&
(\$b1 iff \$XOR2(a0,AND2(g1,b0)))&
(\$b2 iff \$XOR2(a1,AND2(g2,b0)))&
(\$b3 iff \$XOR2(a2,AND2(g3,b0)))&
(\$b4 iff \$XOR2(a3,AND2(g4,b0)))&
(\$b5 iff \$XOR2(a4,AND2(g5,b0)))&
(\$b6 iff \$XOR2(a5,AND2(g6,b0)))&
(\$b7 iff \$XOR2(a6,AND2(g7,b0)))&
(\$b8 iff \$XOR2(a7,AND2(g8,b0)))&
(\$b9 iff \$XOR2(a8,AND2(g9,b0)))&
(\$b10 iff \$XOR2(a9,AND2(g10,b0)))&
(\$b11 iff \$XOR2(a10,AND2(g11,b0)))&
(\$b12 iff \$XOR2(a11,AND2(g12,b0)))&
(\$b13 iff \$XOR2(a12,AND2(g13,b0)))&
(\$b14 iff \$XOR2(a13,AND2(g14,b0)))&
(\$b15 iff \$XOR2(a14,AND2(g15,b0)))
implies
(\$b15 iff \$XOR2(XOR2(a14,AND2(g15,a15)),XOR2(z,AND2(g15,p)))) &
(\$b14 iff \$XOR2(XOR2(a13,AND2(g14,a15)),XOR2(z,AND2(g14,p)))) &
(\$b13 iff \$XOR2(XOR2(a12,AND2(g13,a15)),XOR2(z,AND2(g13,p)))) &
(\$b12 iff \$XOR2(XOR2(a11,AND2(g12,a15)),XOR2(z,AND2(g12,p)))) &
(\$b11 iff \$XOR2(XOR2(a10,AND2(g11,a15)),XOR2(z,AND2(g11,p)))) &
(\$b10 iff \$XOR2(XOR2(a9,AND2(g10,a15)),XOR2(z,AND2(g10,p)))) &
(\$b9 iff \$XOR2(XOR2(a8,AND2(g9,a15)),XOR2(z,AND2(g9,p)))) &
(\$b8 iff \$XOR2(XOR2(a7,AND2(g8,a15)),XOR2(z,AND2(g8,p)))) &
(\$b7 iff \$XOR2(XOR2(a6,AND2(g7,a15)),XOR2(z,AND2(g7,p)))) &
(\$b6 iff \$XOR2(XOR2(a5,AND2(g6,a15)),XOR2(z,AND2(g6,p)))) &
(\$b5 iff \$XOR2(XOR2(a4,AND2(g5,a15)),XOR2(z,AND2(g5,p)))) &
(\$b4 iff \$XOR2(XOR2(a3,AND2(g4,a15)),XOR2(z,AND2(g4,p)))) &
(\$b3 iff \$XOR2(XOR2(a2,AND2(g3,a15)),XOR2(z,AND2(g3,p)))) &
(\$b2 iff \$XOR2(XOR2(a1,AND2(g2,a15)),XOR2(z,AND2(g2,p)))) &
(\$b1 iff \$XOR2(XOR2(a0,AND2(g1,a15)),XOR2(z,AND2(g1,p)))) &
(\$b0 iff \$XOR2(XOR2(z, AND2(g0,a15)),XOR2(z,AND2(g0,p))));

```