    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Documentation.SBV.Examples.CodeGeneration.CRC_USB5
    -- Copyright   :  (c) Levent Erkok
    -- License     :  BSD3
    -- Maintainer  :  erkokl@gmail.com
    -- Stability   :  experimental
    --
    -- 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.
    -----------------------------------------------------------------------------

    module Documentation.SBV.Examples.CodeGeneration.CRC_USB5 where

    import Data.SBV
    import Data.SBV.Tools.CodeGen
    import Data.SBV.Tools.Polynomial

    -----------------------------------------------------------------------------
    -- * 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
    -- purposes.
    usb5 :: SWord16
    usb5 = polynomial [5, 2, 0]

    -----------------------------------------------------------------------------
    -- * Computing CRCs
    -----------------------------------------------------------------------------

    -- | 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
    crcUSB i = fromBitsBE (ib ++ cb)
      where ib = drop 5  (blastBE i)    -- only the last 11 bits needed
            pb = drop 11 (blastBE usb5) -- only the last  5 bits needed
            cb = crcBV 5 ib pb

    -- | 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.
    crcUSB' :: SWord16 -> SWord16
    crcUSB' i' = i .|. pMod i usb5
      where i = i' `shiftL` 5

    -----------------------------------------------------------------------------
    -- * Correctness
    -----------------------------------------------------------------------------

    -- | 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.
    crcGood :: IO ThmResult
    crcGood = prove $ \i -> crcUSB i .== crcUSB' i

    -----------------------------------------------------------------------------
    -- * Code generation
    -----------------------------------------------------------------------------

    -- | Generate a C function to compute the USB CRC, using the internal CRC
    -- function.
    cg1 :: IO ()
    cg1 = compileToC (Just "crcUSB1") "crcUSB1" $ do
            msg <- cgInput "msg"
            cgOutput "crc" (crcUSB msg)

    -- | 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.
    cg2 :: IO ()
    cg2 = compileToC (Just "crcUSB2") "crcUSB2" $ do
            msg <- cgInput "msg"
            cgOutput "crc" (crcUSB' msg)