| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.Existentials.CRCPolynomial
Contents
Description
This program demonstrates the use of the existentials and the QBVF (quantified bit-vector solver). We generate CRC polynomials of degree 16 that can be used for messages of size 48-bits. The query finds all such polynomials that have hamming distance is at least 4. That is, if the CRC can't tell two different 48-bit messages apart, then they must differ in at least 4 bits.
Modeling 48 bit words
type SWord48 = (SWord32, SWord16) Source #
SBV doesn't support 48 bit words natively. So, we represent them as a tuple, 32 high-bits and 16 low-bits.
crc_48_16 :: SWord48 -> SWord16 -> [SBool] Source #
Compute the 16 bit CRC of a 48 bit message, using the given polynomial
diffCount :: (SWord48, [SBool]) -> (SWord48, [SBool]) -> SWord8 Source #
Count the differing bits in the message and the corresponding CRC
crcGood :: SWord8 -> SWord16 -> SWord48 -> SWord48 -> SBool Source #
Given a hamming distance value hd, crcGood returns true if
the 16 bit polynomial can distinguish all messages that has at most
hd different bits. Note that we express this conversely: If the
sent and received messages are different, then it must be the
case that that must differ from each other (including CRCs), in
more than hd bits.
genPoly :: SWord8 -> IO () Source #
Generate good CRC polynomials for 48-bit words, given the hamming distance hd.
findHD4Polynomials :: IO () Source #
Find and display all degree 16 polynomials with hamming distance at least 4, for 48 bit messages.
When run, this function prints:
Polynomial #1. x^16 + x^2 + x + 1 Polynomial #2. x^16 + x^15 + x^2 + 1 Polynomial #3. x^16 + x^15 + x^2 + x + 1 Polynomial #4. x^16 + x^14 + x^10 + 1 Polynomial #5. x^16 + x^14 + x^9 + 1 ...
Note that different runs can produce different results, depending on the random numbers used by the solver, solver version, etc. (Also, the solver will take some time to generate these results. On my machine, the first five polynomials were generated in about 5 minutes.)