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