sbv-5.9: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Examples.CodeGeneration.CRC_USB5

Contents

- The USB polynomial
- Computing CRCs
- Correctness
- Code generation

Description

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 `cg1` vs `cg2` below.

Synopsis

- usb5 :: SWord16
- crcUSB :: SWord16 -> SWord16
- crcUSB' :: SWord16 -> SWord16
- crcGood :: IO ThmResult
- cg1 :: IO ()
- cg2 :: IO ()

# The USB polynomial

usb5 :: SWord16 Source

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 purposes.

# Computing CRCs

crcUSB :: SWord16 -> SWord16 Source

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.

crcUSB' :: SWord16 -> SWord16 Source

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.

# Correctness

crcGood :: IO ThmResult Source

Prove that the custom `crcBV` function is equivalent to the mathematical definition of CRC's for 11 bit messages. We have:

    >>> crcGood
    Q.E.D.

# Code generation

cg1 :: IO () Source

Generate a C function to compute the USB CRC, using the internal CRC function.

cg2 :: IO () Source

Generate a C function to compute the USB CRC, using the mathematical definition of the CRCs. While this version generates functionally eqivalent C code, it's less efficient; it has about 30% more code. So, the above version is preferable for code generation purposes.