CRC.hs

-- | Implement USB5 CRC over a stream of 16-bit words.  The USB5 algorithm
-- itself is implemented in SBV; see
-- https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Examples/CodeGeneration/CRC_USB5.hs
-- .

{-

> runhaskell CRC.hs
> cd copilot-sbv-codegen

Add a main function to driver.c; something like

  int main(void) {
    int i;
    for(i = 0; i < 10; i++) {
      step();
    }
    return 1;
  }

Define a trigger function (look in copilot.h for the prototype), e.g., 

  void chksum(uint16_t words, uint16_t current, uint16_t output) {
    printf("words: %u, current: %u, output: %u\n", words, current, output); 
  }

> make driver
> ./driver

-}

module CRC where

import Prelude ()
import Language.Copilot hiding (words)
import qualified Copilot.Compile.SBV as S

import qualified Data.SBV as V
import Data.SBV.Examples.CodeGeneration.CRC_USB5 (crcUSB)

-- | Incoming stream of words: 1,2,3, ..., 2047,0,1,2, ...
words :: Stream Word16
words = [1] ++ words `mod` 2047 -- USB5 is for 11-bit words.

-- | Call the CRC function generated by the SBV package.  (The Nothing argument
-- says "no interpreter values given.)
current :: Stream Word16
current = externFun "crc_sbv" [arg words] Nothing

-- | xor the CRC of the current word and the CRC of the stream so far.
output :: Stream Word16
output = [0] ++ current .^. output

-- | The trigger specifies a C function with the prototype 
-- void chksum(Word16, Word16, Word16);
spec :: Spec
spec = 
  trigger "chksum" true [ arg words
                        , arg current
                        , arg output
                        ]

main :: IO ()
main = 
  reify spec >>=
    S.compileWithSBV 
      S.defaultParams
      [("crc_sbv", sbv)]
    
  where
  sbv = do word <- V.cgInput "word"
           V.cgReturn (crcUSB word)