Computing the CRC symbolically, using the USB polynomial. We also
generating C code for it as well. This example demonstrates the
use of the
crcBV function, along with how CRC's can be computed
mathematically using polynomial division. While the results are the
same (i.e., proven equivalent, see
crcGood below), the internal
CRC implementation generates much better code, compare
The USB polynomial
The USB CRC polynomial:
x^5 + x^2 + 1.
Although this polynomial needs just 6 bits to represent (5 if higher
order bit is implicitly assumed to be set), we'll simply use a 16 bit
number for its representation to keep things simple for code generation
Given an 11 bit message, compute the CRC of it using the USB polynomial, which is 5 bits, and then append it to the msg to get a 16-bit word. Again, the incoming 11-bits is represented as a 16-bit word, with 5 highest bits essentially ignored for input purposes.
Alternate method for computing the CRC, mathematically. We shift the number to the left by 5, and then compute the remainder from the polynomial division by the USB polynomial. The result is then appended to the end of the message.
Prove that the custom
crcBV function is equivalent to the mathematical
definition of CRC's for 11 bit messages. We have: