1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
-----------------------------------------------------------------------------
-- |
-- 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 = 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 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 = compileToC (Just "crcUSB2") "crcUSB2" $ do
msg <- cgInput "msg"
cgOutput "crc" (crcUSB' msg)
|
