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

    {-# OPTIONS_GHC -Wall -Werror #-}

    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 :: SWord16
    usb5 = [Int] -> SWord16
    forall a. Polynomial a => [Int] -> a
    polynomial [Int
    5, Int
    2, Int
    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 :: SWord16 -> SWord16
    crcUSB SWord16
    i = [SBool] -> SWord16
    forall a. SFiniteBits a => [SBool] -> SBV a
    fromBitsBE ([SBool]
    ib [SBool] -> [SBool] -> [SBool]
    forall a. [a] -> [a] -> [a]
    ++ [SBool]
    cb)
      where ib :: [SBool]
    ib = Int -> [SBool] -> [SBool]
    forall a. Int -> [a] -> [a]
    drop Int
    5  (SWord16 -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastBE SWord16
    i)    -- only the last 11 bits needed
            pb :: [SBool]
    pb = Int -> [SBool] -> [SBool]
    forall a. Int -> [a] -> [a]
    drop Int
    11 (SWord16 -> [SBool]
    forall a. SFiniteBits a => SBV a -> [SBool]
    blastBE SWord16
    usb5) -- only the last  5 bits needed
            cb :: [SBool]
    cb = Int -> [SBool] -> [SBool] -> [SBool]
    crcBV Int
    5 [SBool]
    ib [SBool]
    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' :: SWord16 -> SWord16
    crcUSB' SWord16
    i' = SWord16
    i SWord16 -> SWord16 -> SWord16
    forall a. Bits a => a -> a -> a
    .|. SWord16 -> SWord16 -> SWord16
    forall a. Polynomial a => a -> a -> a
    pMod SWord16
    i SWord16
    usb5
      where i :: SWord16
    i = SWord16
    i' SWord16 -> Int -> SWord16
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    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 :: IO ThmResult
    crcGood = (SWord16 -> SBool) -> IO ThmResult
    forall a. Provable a => a -> IO ThmResult
    prove ((SWord16 -> SBool) -> IO ThmResult)
    -> (SWord16 -> SBool) -> IO ThmResult
    forall a b. (a -> b) -> a -> b
    $ \SWord16
    i -> SWord16 -> SWord16
    crcUSB SWord16
    i SWord16 -> SWord16 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SWord16 -> SWord16
    crcUSB' SWord16
    i

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

    -- | Generate a C function to compute the USB CRC, using the internal CRC
    -- function.
    cg1 :: IO ()
    cg1 :: IO ()
    cg1 = Maybe FilePath -> FilePath -> SBVCodeGen () -> IO ()
    forall a. Maybe FilePath -> FilePath -> SBVCodeGen a -> IO a
    compileToC (FilePath -> Maybe FilePath
    forall a. a -> Maybe a
    Just FilePath
    "crcUSB1") FilePath
    "crcUSB1" (SBVCodeGen () -> IO ()) -> SBVCodeGen () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ do
            SWord16
    msg <- FilePath -> SBVCodeGen SWord16
    forall a. SymVal a => FilePath -> SBVCodeGen (SBV a)
    cgInput FilePath
    "msg"
            FilePath -> SWord16 -> SBVCodeGen ()
    forall a. FilePath -> SBV a -> SBVCodeGen ()
    cgOutput FilePath
    "crc" (SWord16 -> SWord16
    crcUSB SWord16
    msg)

    -- | Generate a C function to compute the USB CRC, using the mathematical
    -- definition of the CRCs. While this version generates functionally equivalent
    -- 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 :: IO ()
    cg2 = Maybe FilePath -> FilePath -> SBVCodeGen () -> IO ()
    forall a. Maybe FilePath -> FilePath -> SBVCodeGen a -> IO a
    compileToC (FilePath -> Maybe FilePath
    forall a. a -> Maybe a
    Just FilePath
    "crcUSB2") FilePath
    "crcUSB2" (SBVCodeGen () -> IO ()) -> SBVCodeGen () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ do
            SWord16
    msg <- FilePath -> SBVCodeGen SWord16
    forall a. SymVal a => FilePath -> SBVCodeGen (SBV a)
    cgInput FilePath
    "msg"
            FilePath -> SWord16 -> SBVCodeGen ()
    forall a. FilePath -> SBV a -> SBVCodeGen ()
    cgOutput FilePath
    "crc" (SWord16 -> SWord16
    crcUSB' SWord16
    msg)