diff --git a/CHANGELOG b/CHANGELOG
new file mode 100644
--- /dev/null
+++ b/CHANGELOG
@@ -0,0 +1,3 @@
+2024-03-08
+        * Version bump (3.19). (#5)
+        * Create new library for Bluespec backend.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+2009
+BSD3 License terms
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+
+Redistributions in binary form must reproduce the above copyright
+notice, this list of conditions and the following disclaimer in the
+documentation and/or other materials provided with the distribution.
+
+Neither the name of the developers nor the names of its contributors
+may be used to endorse or promote products derived from this software
+without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT OWNER OR
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,38 @@
+[![Build Status](https://github.com/Copilot-Language/copilot-bluespec/workflows/copilot-bluespec/badge.svg)](https://github.com/Copilot-Language/copilot-bluespec/actions?query=workflow%3Acopilot-bluespec)
+
+# Copilot: a stream DSL
+Copilot-Bluespec implements a Bluespec backend for Copilot, producing code that
+is suitable for FPGAs.
+
+Copilot is a runtime verification framework written in Haskell. It allows the
+user to write programs in a simple but powerful way using a stream-based
+approach.
+
+Programs can be interpreted for testing, or translated Bluespec code to be
+incorporated in a project, or as a standalone application. The Bluespec backend
+ensures us that the output is constant in memory and time, making it suitable
+for systems with hard realtime requirements.
+
+## Installation
+Copilot-Bluespec can be found on
+[Hackage](https://hackage.haskell.org/package/copilot-bluespec). It is
+typically only installed as part of the complete Copilot distribution. For
+installation instructions, please refer to the [Copilot
+website](https://copilot-language.github.io).
+
+The generated Bluespec code requires `bsc` (the Bluespec compiler) in order to
+be compiled. `bsc` can be downloaded
+[here](https://github.com/B-Lang-org/bsc/releases).
+
+## Further information
+For further information, install instructions and documentation, please visit
+the Copilot website:
+[https://copilot-language.github.io](https://copilot-language.github.io)
+
+There is also an implementation-focused design document
+[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-bluespec/DESIGN.md).
+
+
+## License
+Copilot is distributed under the BSD-3-Clause license, which can be found
+[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-bluespec/LICENSE).
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/copilot-bluespec.cabal b/copilot-bluespec.cabal
new file mode 100644
--- /dev/null
+++ b/copilot-bluespec.cabal
@@ -0,0 +1,96 @@
+cabal-version             : >= 1.10
+name                      : copilot-bluespec
+version                   : 3.19
+synopsis                  : A compiler for Copilot targeting FPGAs.
+description               :
+  This package is a back-end from Copilot to FPGAs in Bluespec.
+  .
+  Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in
+  Haskell. Copilot contains an interpreter, multiple back-end compilers, and
+  other verification tools.
+  .
+  A tutorial, examples, and other information are available at
+  <https://copilot-language.github.io>.
+
+license                   : BSD3
+license-file              : LICENSE
+maintainer                : Ryan Scott <rscott@galois.com>
+homepage                  : https://copilot-language.github.io
+bug-reports               : https://github.com/Copilot-Language/copilot-bluespec/issues
+stability                 : Experimental
+category                  : Language, Embedded
+build-type                : Simple
+extra-source-files        : README.md
+                          , CHANGELOG
+
+author                    : Frank Dedden
+                          , Alwyn Goodloe
+                          , Ivan Perez
+                          , Ryan Scott
+
+x-curation: uncurated
+
+source-repository head
+    type:       git
+    location:   https://github.com/Copilot-Language/copilot-bluespec.git
+
+library
+  default-language        : Haskell2010
+  hs-source-dirs          : src, shared
+
+  ghc-options             : -Wall
+  build-depends           : base              >= 4.9    && < 5
+                          , directory         >= 1.3    && < 1.4
+                          , filepath          >= 1.4    && < 1.5
+                          , pretty            >= 1.1.2  && < 1.2
+
+                          , copilot-core      >= 3.19   && < 3.20
+                          , language-bluespec >= 0.1    && < 0.2
+
+  exposed-modules         : Copilot.Compile.Bluespec
+
+  other-modules           : Copilot.Compile.Bluespec.CodeGen
+                          , Copilot.Compile.Bluespec.Compile
+                          , Copilot.Compile.Bluespec.Error
+                          , Copilot.Compile.Bluespec.Expr
+                          , Copilot.Compile.Bluespec.External
+                          , Copilot.Compile.Bluespec.Name
+                          , Copilot.Compile.Bluespec.Settings
+                          , Copilot.Compile.Bluespec.Type
+
+test-suite unit-tests
+  type:
+    exitcode-stdio-1.0
+
+  main-is:
+    Main.hs
+
+  other-modules:
+   Test.Copilot.Compile.Bluespec
+
+   Copilot.Compile.Bluespec.External
+
+  build-depends:
+      base
+    , directory
+    , HUnit
+    , QuickCheck
+    , pretty
+    , process
+    , random
+    , test-framework
+    , test-framework-hunit
+    , test-framework-quickcheck2
+    , unix
+
+    , copilot-core
+    , copilot-bluespec
+
+  hs-source-dirs:
+    tests, shared
+
+  default-language:
+    Haskell2010
+
+  ghc-options:
+    -Wall
diff --git a/shared/Copilot/Compile/Bluespec/External.hs b/shared/Copilot/Compile/Bluespec/External.hs
new file mode 100644
--- /dev/null
+++ b/shared/Copilot/Compile/Bluespec/External.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE ExistentialQuantification #-}
+
+-- | Represent information about externs needed in the generation of Bluespec
+-- code for stream declarations and triggers.
+module Copilot.Compile.Bluespec.External
+  ( External(..)
+  , gatherExts
+  ) where
+
+-- External imports
+import Data.List (unionBy)
+
+-- Internal imports: Copilot
+import Copilot.Core ( Expr (..), Stream (..), Trigger (..), Type, UExpr (..) )
+
+-- | Representation of external variables.
+data External = forall a. External
+  { extName :: String
+  , extType :: Type a
+  }
+
+-- | Collect all external variables from the streams and triggers.
+--
+-- Although Copilot specifications can contain also properties and theorems,
+-- the C99 backend currently only generates code for streams and triggers.
+gatherExts :: [Stream] -> [Trigger] -> [External]
+gatherExts streams triggers = streamsExts `extUnion` triggersExts
+  where
+    streamsExts  = foldr (extUnion . streamExts) mempty streams
+    triggersExts = foldr (extUnion . triggerExts) mempty triggers
+
+    streamExts :: Stream -> [External]
+    streamExts (Stream _ _ expr _) = exprExts expr
+
+    triggerExts :: Trigger -> [External]
+    triggerExts (Trigger _ guard args) = guardExts `extUnion` argExts
+      where
+        guardExts = exprExts guard
+        argExts   = concatMap uExprExts args
+
+    uExprExts :: UExpr -> [External]
+    uExprExts (UExpr _ expr) = exprExts expr
+
+    exprExts :: Expr a -> [External]
+    exprExts (Local _ _ _ e1 e2)   = exprExts e1 `extUnion` exprExts e2
+    exprExts (ExternVar ty name _) = [External name ty]
+    exprExts (Op1 _ e)             = exprExts e
+    exprExts (Op2 _ e1 e2)         = exprExts e1 `extUnion` exprExts e2
+    exprExts (Op3 _ e1 e2 e3)      = exprExts e1 `extUnion` exprExts e2
+                                       `extUnion` exprExts e3
+    exprExts (Label _ _ e)         = exprExts e
+    exprExts _                     = []
+
+    -- | Union over lists of External, we solely base the equality on the
+    -- extName's.
+    extUnion :: [External] -> [External] -> [External]
+    extUnion = unionBy (\a b -> extName a == extName b)
diff --git a/src/Copilot/Compile/Bluespec.hs b/src/Copilot/Compile/Bluespec.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Compile/Bluespec.hs
@@ -0,0 +1,12 @@
+-- | Compile Copilot specifications to Bluespec code.
+module Copilot.Compile.Bluespec
+  ( compile
+  , compileWith
+  , BluespecSettings(..)
+  , mkDefaultBluespecSettings
+  ) where
+
+-- Internal imports
+import Copilot.Compile.Bluespec.Compile ( compile, compileWith )
+import Copilot.Compile.Bluespec.Settings ( BluespecSettings (..),
+                                           mkDefaultBluespecSettings )
diff --git a/src/Copilot/Compile/Bluespec/CodeGen.hs b/src/Copilot/Compile/Bluespec/CodeGen.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Compile/Bluespec/CodeGen.hs
@@ -0,0 +1,259 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+-- | High-level translation of Copilot Core into Bluespec.
+module Copilot.Compile.Bluespec.CodeGen
+  ( -- * Type declarations
+    mkStructDecln
+
+    -- * Ring buffers
+  , mkBuffDecln
+  , mkIndexDecln
+  , mkAccessDecln
+
+    -- * Stream generators
+  , mkGenFun
+
+    -- * Monitor processing
+  , mkStepRule
+  , mkTriggerRule
+
+    -- * Module interface specifications
+  , mkSpecIfcFields
+  ) where
+
+-- External imports
+import Data.String (IsString (..))
+import qualified Language.Bluespec.Classic.AST as BS
+import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS
+import qualified Language.Bluespec.Classic.AST.Builtin.Types as BS
+
+-- Internal imports: Copilot
+import Copilot.Core
+
+-- Internal imports
+import Copilot.Compile.Bluespec.Expr
+import Copilot.Compile.Bluespec.External
+import Copilot.Compile.Bluespec.Name
+import Copilot.Compile.Bluespec.Type
+
+-- | Write a generator function for a stream.
+mkGenFun :: String -> Expr a -> Type a -> BS.CDefl
+mkGenFun name expr ty =
+    -- name :: ty
+    -- name = expr
+    BS.CLValueSign
+      (BS.CDef nameId (BS.CQType [] (transType ty)) [def])
+      []
+  where
+    nameId = BS.mkId BS.NoPos $ fromString $ lowercaseName name
+    def = BS.CClause [] [] (transExpr expr)
+
+-- | Bind a buffer variable and initialise it with the stream buffer.
+mkBuffDecln :: forall a. Id -> Type a -> [a] -> [BS.CStmt]
+mkBuffDecln sId ty xs =
+    initVals ++ [BS.CSletrec [initBufSig]]
+  where
+    -- sId_0     :: Reg <ty> <- mkReg xs_0
+    -- ...
+    -- sId_(n-1) :: Reg <ty> <- mkReg xs_(n-1)
+    initVals = zipWith mkInitVal xs [0..]
+    -- sId :: Vector n (Reg <ty>)
+    -- sId = update (... (update newVector 0 sId_0) ...) (n-1) sId_(n-1)
+    initBufSig = BS.CLValueSign
+                   (BS.CDef nameId (BS.CQType [] vecTy) [initBufDef])
+                   []
+    initBufDef = BS.CClause
+                   []
+                   []
+                   (genVector
+                     (\idx _ -> BS.CVar $ BS.mkId BS.NoPos $
+                                fromString $ streamElemName sId idx)
+                     xs)
+
+    nameId   = BS.mkId BS.NoPos $ fromString $ streamName sId
+    bsTy     = tReg `BS.TAp` transType ty
+    vecTy    = tVector `BS.TAp` BS.cTNum numElems BS.NoPos `BS.TAp` bsTy
+    numElems = toInteger $ length xs
+
+    mkInitVal :: a -> Int -> BS.CStmt
+    mkInitVal x elemNum =
+        BS.CSBindT
+          (BS.CPVar elemId)
+          Nothing
+          []
+          (BS.CQType [] bsTy)
+          (BS.CApply (BS.CVar (BS.mkId BS.NoPos "mkReg")) [constTy ty x])
+      where
+        elemName = streamElemName sId elemNum
+        elemId   = BS.mkId BS.NoPos $ fromString elemName
+
+-- | Make an index variable and initialise it to 0.
+mkIndexDecln :: Id -> BS.CStmt
+mkIndexDecln sId =
+  -- sId_idx :: Reg (Bit 64) <- mkReg 0
+  BS.CSBindT
+    (BS.CPVar nameId)
+    Nothing
+    []
+    (BS.CQType [] bsTy)
+    (BS.CApply (BS.CVar (BS.mkId BS.NoPos "mkReg"))
+               [cLit $ BS.LInt $ BS.ilDec 0])
+  where
+    nameId = BS.mkId BS.NoPos $ fromString $ indexName sId
+    bsTy   = tReg `BS.TAp` BS.tBitN 64 BS.NoPos
+
+-- | Define an accessor function for the ring buffer associated with a stream
+mkAccessDecln :: Id -> Type a -> [a] -> BS.CDefl
+mkAccessDecln sId ty xs =
+    -- sId_get :: Bits 64 -> ty
+    -- sId_get x = (select sId ((sId_idx + x) % buffLength))._read
+    BS.CLValueSign (BS.CDef nameId (BS.CQType [] funTy) [def]) []
+  where
+    def        = BS.CClause [BS.CPVar argId] [] expr
+    argTy      = BS.tBit `BS.TAp` BS.cTNum 64 BS.NoPos
+    retTy      = transType ty
+    funTy      = BS.tArrow `BS.TAp` argTy `BS.TAp` retTy
+    name       = streamAccessorName sId
+    nameId     = BS.mkId BS.NoPos $ fromString name
+    buffLength = cLit $ BS.LInt $ BS.ilDec $ toInteger $ length xs
+    argId      = BS.mkId BS.NoPos "x"
+    index      = BS.CApply (BS.CVar (BS.idPercentAt BS.NoPos))
+                   [ BS.CApply (BS.CVar BS.idPlus)
+                       [ BS.CVar (BS.mkId BS.NoPos (fromString (indexName sId)))
+                       , BS.CVar argId
+                       ]
+                   , buffLength
+                   ]
+    indexExpr  = cIndexVector
+                   (BS.CVar (BS.mkId BS.NoPos (fromString (streamName sId))))
+                   index
+    expr       = BS.CSelect indexExpr (BS.id_read BS.NoPos)
+
+-- | Define fields for a module interface containing a specification's trigger
+-- functions and external variables.
+mkSpecIfcFields :: [Trigger] -> [External] -> [BS.CField]
+mkSpecIfcFields triggers exts =
+    map mkTriggerField triggers ++ map mkExtField exts
+  where
+    -- trigger :: args_1 -> ... -> args_n -> Action
+    mkTriggerField :: Trigger -> BS.CField
+    mkTriggerField (Trigger name _ args) =
+      mkField name $
+      foldr
+        (\(UExpr arg _) res -> BS.tArrow `BS.TAp` transType arg `BS.TAp` res)
+        BS.tAction
+        args
+
+    -- ext :: Reg ty
+    mkExtField :: External -> BS.CField
+    mkExtField (External name ty) =
+      mkField name $ tReg `BS.TAp` transType ty
+
+-- | Define a rule for a trigger function.
+mkTriggerRule :: Trigger -> BS.CRule
+mkTriggerRule (Trigger name _ args) =
+    BS.CRule
+      []
+      (Just $ cLit $ BS.LString name)
+      [ BS.CQFilter $
+        BS.CVar $ BS.mkId BS.NoPos $
+        fromString $ guardName name
+      ]
+      (BS.CApply nameExpr args')
+  where
+    ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName
+    nameId   = BS.mkId BS.NoPos $ fromString $ lowercaseName name
+    nameExpr = BS.CSelect (BS.CVar ifcArgId) nameId
+
+    args'   = take (length args) (map argCall (argNames name))
+    argCall = BS.CVar . BS.mkId BS.NoPos . fromString
+
+-- | Writes the @step@ rule that updates all streams.
+mkStepRule :: [Stream] -> Maybe BS.CRule
+mkStepRule streams
+  | null allUpdates
+  = -- If there is nothing to update, don't bother creating a step rule.
+    -- Doing so wouldn't harm anything, but bsc will generate a warning
+    -- when compiling such an empty rule.
+    Nothing
+  | otherwise
+  = Just $
+    BS.CRule
+      []
+      (Just $ cLit $ BS.LString "step")
+      [BS.CQFilter $ BS.CCon BS.idTrue []]
+      (BS.Caction BS.NoPos allUpdates)
+  where
+    allUpdates = bufferUpdates ++ indexUpdates
+    (bufferUpdates, indexUpdates) = unzip $ map mkUpdateGlobals streams
+
+    -- Write code to update global stream buffers and index.
+    mkUpdateGlobals :: Stream -> (BS.CStmt, BS.CStmt)
+    mkUpdateGlobals (Stream sId buff _ _) =
+        (bufferUpdate, indexUpdate)
+      where
+        bufferUpdate =
+          BS.CSExpr Nothing $
+          BS.Cwrite
+            BS.NoPos
+            (cIndexVector (BS.CVar buffId) (BS.CVar indexId))
+            (BS.CVar genId)
+
+        indexUpdate =
+          BS.CSExpr Nothing $
+          BS.Cwrite
+            BS.NoPos
+            (BS.CVar indexId)
+            (BS.CApply (BS.CVar (BS.idPercentAt BS.NoPos))
+                       [incIndex, buffLength])
+          where
+            buffLength = cLit $ BS.LInt $ BS.ilDec $ toInteger $ length buff
+            incIndex   = BS.CApply (BS.CVar BS.idPlus)
+                           [ BS.CVar indexId
+                           , cLit $ BS.LInt $ BS.ilDec 1
+                           ]
+
+        buffId  = BS.mkId BS.NoPos $ fromString $ streamName sId
+        genId   = BS.mkId BS.NoPos $ fromString $ generatorName sId
+        indexId = BS.mkId BS.NoPos $ fromString $ indexName sId
+
+-- | Write a struct declaration based on its definition.
+mkStructDecln :: Struct a => a -> BS.CDefn
+mkStructDecln x =
+    BS.Cstruct
+      True
+      BS.SStruct
+      (BS.IdK structId)
+      [] -- No type variables
+      structFields
+      -- Derive a Bits instance so that we can put this struct in a Reg
+      [BS.CTypeclass BS.idBits]
+  where
+    structId = BS.mkId BS.NoPos $ fromString $ uppercaseName $ typeName x
+    structFields = map mkStructField $ toValues x
+
+    mkStructField :: Value a -> BS.CField
+    mkStructField (Value ty field) =
+      mkField (fieldName field) (transType ty)
+
+-- | Write a field of a struct or interface, along with its type.
+mkField :: String -> BS.CType -> BS.CField
+mkField name ty =
+  BS.CField
+    { BS.cf_name = BS.mkId BS.NoPos $ fromString $ lowercaseName name
+    , BS.cf_pragmas = Nothing
+    , BS.cf_type = BS.CQType [] ty
+    , BS.cf_default = []
+    , BS.cf_orig_type = Nothing
+    }
+
+-- | The @Reg@ Bluespec interface type.
+tReg :: BS.CType
+tReg = BS.TCon $
+  BS.TyCon
+    { BS.tcon_name = BS.idReg
+    , BS.tcon_kind = Just (BS.Kfun BS.KStar BS.KStar)
+    , BS.tcon_sort = BS.TIstruct (BS.SInterface [])
+                                 [BS.id_write BS.NoPos, BS.id_read BS.NoPos]
+    }
diff --git a/src/Copilot/Compile/Bluespec/Compile.hs b/src/Copilot/Compile/Bluespec/Compile.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Compile/Bluespec/Compile.hs
@@ -0,0 +1,294 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+-- | Compile Copilot specifications to Bluespec code.
+module Copilot.Compile.Bluespec.Compile
+  ( compile
+  , compileWith
+  ) where
+
+-- External imports
+import Data.List                      (nub, union)
+import Data.Maybe                     (catMaybes, maybeToList)
+import Data.String                    (IsString (..))
+import Data.Typeable                  (Typeable)
+import qualified Language.Bluespec.Classic.AST as BS
+import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS
+import qualified Language.Bluespec.Classic.AST.Builtin.Types as BS
+import Text.PrettyPrint.HughesPJClass (Pretty (..), render)
+import System.Directory               (createDirectoryIfMissing)
+import System.Exit                    (exitFailure)
+import System.FilePath                ((</>))
+import System.IO                      (hPutStrLn, stderr)
+
+-- Internal imports: Copilot
+import Copilot.Core
+
+-- Internal imports
+import Copilot.Compile.Bluespec.CodeGen
+import Copilot.Compile.Bluespec.External
+import Copilot.Compile.Bluespec.Name
+import Copilot.Compile.Bluespec.Settings
+
+-- | Compile a specification to a Bluespec file.
+--
+-- The first argument is the settings for the Bluespec code generated.
+--
+-- The second argument is used as a module name and the prefix for the .bs files
+-- that are generated.
+compileWith :: BluespecSettings -> String -> Spec -> IO ()
+compileWith bsSettings prefix spec
+  | null (specTriggers spec)
+  = do hPutStrLn stderr $
+         "Copilot error: attempt at compiling empty specification.\n"
+         ++ "You must define at least one trigger to generate Bluespec monitors."
+       exitFailure
+
+  | otherwise
+  = do let typesBsFile = render $ pPrint $ compileTypesBS bsSettings prefix spec
+           ifcBsFile   = render $ pPrint $ compileIfcBS   bsSettings prefix spec
+           bsFile      = render $ pPrint $ compileBS      bsSettings prefix spec
+
+       let dir = bluespecSettingsOutputDirectory bsSettings
+       createDirectoryIfMissing True dir
+       writeFile (dir </> specTypesPkgName prefix ++ ".bs") typesBsFile
+       writeFile (dir </> specIfcPkgName prefix ++ ".bs") ifcBsFile
+       writeFile (dir </> prefix ++ ".bs") bsFile
+
+-- | Compile a specification to a Bluespec.
+--
+-- The first argument is used as a prefix for the generated .bs files.
+compile :: String -> Spec -> IO ()
+compile = compileWith mkDefaultBluespecSettings
+
+-- | Generate a @<prefix>.bs@ file from a 'Spec'. This is the main payload of
+-- the Bluespec backend.
+--
+-- The generated Bluespec file will import a handful of files from the standard
+-- library, as well as the following generated files:
+--
+-- * @<prefix>Ifc.bs@, which defines the interface containing the trigger
+--   functions and external variables.
+--
+-- * @<prefix>Types.bs@, which defines any structs used in the 'Spec'.
+--
+-- It will also generate a @mk<prefix> :: Module <prefix>Ifc -> Module Empty@
+-- function, which defines the module structure for this 'Spec'. The
+-- @mk<prefix>@ function has the following structure:
+--
+-- * First, bind the argument of type @Module <prefix>Ifc@ so that trigger
+--   functions can be invoked and external variables can be used.
+--
+-- * Next, declare stream buffers and indices.
+--
+-- * Next, declare generator functions for streams, accessor functions for
+--   streams, and guard functions for triggers.
+--
+-- * Next, declare rules for each trigger function.
+--
+-- * Finally, declare a single rule that updates the stream buffers and
+--   indices.
+compileBS :: BluespecSettings -> String -> Spec -> BS.CPackage
+compileBS _bsSettings prefix spec =
+    BS.CPackage
+      (BS.mkId BS.NoPos (fromString prefix))
+      (Right [])
+      (stdLibImports ++ genImports)
+      []
+      [moduleDef]
+      []
+  where
+    -- import <prefix>Types
+    -- import <prefix>Ifc
+    genImports :: [BS.CImport]
+    genImports =
+      [ BS.CImpId False $ BS.mkId BS.NoPos $ fromString
+                        $ specTypesPkgName prefix
+      , BS.CImpId False $ BS.mkId BS.NoPos $ fromString
+                        $ specIfcPkgName prefix
+      ]
+
+    moduleDef :: BS.CDefn
+    moduleDef = BS.CValueSign $
+      BS.CDef
+        (BS.mkId BS.NoPos $ fromString $ "mk" ++ prefix)
+        -- :: Module <prefix>Ifc -> Module Empty
+        (BS.CQType
+          []
+          (BS.tArrow
+            `BS.TAp` (BS.tModule `BS.TAp` ifcTy)
+            `BS.TAp` (BS.tModule `BS.TAp` emptyTy)))
+        [ BS.CClause [BS.CPVar ifcModId] [] $
+          BS.Cmodule BS.NoPos $
+              BS.CMStmt
+                (BS.CSBind (BS.CPVar ifcArgId) Nothing [] (BS.CVar ifcModId))
+            : map BS.CMStmt mkGlobals ++
+            [ BS.CMStmt $ BS.CSletrec genFuns
+            , BS.CMrules $ BS.Crules [] rules
+            ]
+        ]
+
+    ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName
+    ifcModId = BS.mkId BS.NoPos "ifcMod"
+
+    rules :: [BS.CRule]
+    rules = map mkTriggerRule triggers ++ maybeToList (mkStepRule streams)
+
+    streams  = specStreams spec
+    triggers = specTriggers spec
+    exts     = gatherExts streams triggers
+
+    ifcId     = BS.mkId BS.NoPos $ fromString $ specIfcName prefix
+    ifcFields = mkSpecIfcFields triggers exts
+    ifcTy     = BS.TCon (BS.TyCon
+                  { BS.tcon_name = ifcId
+                  , BS.tcon_kind = Just BS.KStar
+                  , BS.tcon_sort = BS.TIstruct
+                                     (BS.SInterface [])
+                                     (map BS.cf_name ifcFields)
+                  })
+
+    emptyTy = BS.TCon (BS.TyCon
+                { BS.tcon_name = BS.idEmpty
+                , BS.tcon_kind = Just BS.KStar
+                , BS.tcon_sort = BS.TIstruct (BS.SInterface []) []
+                })
+
+    -- Make buffer and index declarations for streams.
+    mkGlobals :: [BS.CStmt]
+    mkGlobals = concatMap buffDecln streams ++ map indexDecln streams
+      where
+        buffDecln  (Stream sId buff _ ty) = mkBuffDecln  sId ty buff
+        indexDecln (Stream sId _    _ _ ) = mkIndexDecln sId
+
+    -- Make generator functions, including trigger arguments.
+    genFuns :: [BS.CDefl]
+    genFuns =  map accessDecln streams
+            ++ map streamGen streams
+            ++ concatMap triggerGen triggers
+      where
+        accessDecln :: Stream -> BS.CDefl
+        accessDecln (Stream sId buff _ ty) = mkAccessDecln sId ty buff
+
+        streamGen :: Stream -> BS.CDefl
+        streamGen (Stream sId _ expr ty) = mkGenFun (generatorName sId) expr ty
+
+        triggerGen :: Trigger -> [BS.CDefl]
+        triggerGen (Trigger name guard args) = guardDef : argDefs
+          where
+            guardDef = mkGenFun (guardName name) guard Bool
+            argDefs  = map argGen (zip (argNames name) args)
+
+            argGen :: (String, UExpr) -> BS.CDefl
+            argGen (argName, UExpr ty expr) = mkGenFun argName expr ty
+
+-- | Generate a @<prefix>Ifc.bs@ file from a 'Spec'. This contains the
+-- definition of the @<prefix>Ifc@ interface, which declares the types of all
+-- trigger functions and external variables. This is put in a separate file so
+-- that larger applications can use it separately.
+compileIfcBS :: BluespecSettings -> String -> Spec -> BS.CPackage
+compileIfcBS _bsSettings prefix spec =
+    BS.CPackage
+      ifcPkgId
+      (Right [])
+      (stdLibImports ++ genImports)
+      []
+      [ifcDef]
+      []
+  where
+    -- import <prefix>Types
+    genImports :: [BS.CImport]
+    genImports =
+      [ BS.CImpId False $ BS.mkId BS.NoPos $ fromString
+                        $ specTypesPkgName prefix
+      ]
+
+    ifcId     = BS.mkId BS.NoPos $ fromString $ specIfcName prefix
+    ifcPkgId  = BS.mkId BS.NoPos $ fromString $ specIfcPkgName prefix
+    ifcFields = mkSpecIfcFields triggers exts
+
+    streams  = specStreams spec
+    triggers = specTriggers spec
+    exts     = gatherExts streams triggers
+
+    ifcDef :: BS.CDefn
+    ifcDef = BS.Cstruct
+               True
+               (BS.SInterface [])
+               (BS.IdK ifcId)
+               [] -- No type variables
+               ifcFields
+               [] -- No derived instances
+
+-- | Generate a @<prefix>Types.bs@ file from a 'Spec'. This declares the types
+-- of any structs used by the Copilot specification. This is put in a separate
+-- file so that larger applications can more easily substitute their own struct
+-- definitions if desired.
+compileTypesBS :: BluespecSettings -> String -> Spec -> BS.CPackage
+compileTypesBS _bsSettings prefix spec =
+    BS.CPackage
+      typesId
+      (Right [])
+      stdLibImports
+      []
+      structDefs
+      []
+  where
+    typesId = BS.mkId BS.NoPos $ fromString $ specTypesPkgName prefix
+
+    structDefs = mkTypeDeclns exprs
+
+    exprs    = gatherExprs streams triggers
+    streams  = specStreams spec
+    triggers = specTriggers spec
+
+    -- Generate type declarations.
+    mkTypeDeclns :: [UExpr] -> [BS.CDefn]
+    mkTypeDeclns es = catMaybes $ map mkTypeDecln uTypes
+      where
+        uTypes = nub $ concatMap (\(UExpr _ e) -> exprTypes e) es
+
+        mkTypeDecln (UType ty) = case ty of
+          Struct x -> Just $ mkStructDecln x
+          _        -> Nothing
+
+-- | Imports from the Bluespec standard library.
+stdLibImports :: [BS.CImport]
+stdLibImports =
+  [ BS.CImpId False $ BS.mkId BS.NoPos "FloatingPoint"
+  , BS.CImpId False $ BS.mkId BS.NoPos "Vector"
+  ]
+
+-- ** Obtain information from Copilot Core Exprs and Types.
+
+-- | List all types of an expression, returns items uniquely.
+exprTypes :: Typeable a => Expr a -> [UType]
+exprTypes e = case e of
+  Const ty _            -> typeTypes ty
+  Local ty1 ty2 _ e1 e2 -> typeTypes ty1 `union` typeTypes ty2
+                             `union` exprTypes e1 `union` exprTypes e2
+  Var ty _              -> typeTypes ty
+  Drop ty _ _           -> typeTypes ty
+  ExternVar ty _ _      -> typeTypes ty
+  Op1 _ e1              -> exprTypes e1
+  Op2 _ e1 e2           -> exprTypes e1 `union` exprTypes e2
+  Op3 _ e1 e2 e3        -> exprTypes e1 `union` exprTypes e2
+                             `union` exprTypes e3
+  Label ty _ _          -> typeTypes ty
+
+-- | List all types of a type, returns items uniquely.
+typeTypes :: Typeable a => Type a -> [UType]
+typeTypes ty = case ty of
+  Array ty' -> typeTypes ty' `union` [UType ty]
+  Struct x  -> concatMap (\(Value ty' _) -> typeTypes ty') (toValues x)
+                 `union` [UType ty]
+  _         -> [UType ty]
+
+-- | Collect all expression of a list of streams and triggers and wrap them
+-- into an UEXpr.
+gatherExprs :: [Stream] -> [Trigger] -> [UExpr]
+gatherExprs streams triggers =  map streamUExpr streams
+                             ++ concatMap triggerUExpr triggers
+  where
+    streamUExpr  (Stream _ _ expr ty)   = UExpr ty expr
+    triggerUExpr (Trigger _ guard args) = UExpr Bool guard : args
diff --git a/src/Copilot/Compile/Bluespec/Error.hs b/src/Copilot/Compile/Bluespec/Error.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Compile/Bluespec/Error.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE Safe #-}
+
+-- |
+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
+--
+-- Custom functions to report error messages to users.
+module Copilot.Compile.Bluespec.Error
+    ( impossible )
+  where
+
+-- | Report an error due to a bug in Copilot.
+impossible :: String -- ^ Name of the function in which the error was detected.
+           -> String -- ^ Name of the package in which the function is located.
+           -> a
+impossible function package =
+  error $ "Impossible error in function "
+    ++ function ++ ", in package " ++ package
+    ++ ". Please file an issue at "
+    ++ "https://github.com/Copilot-Language/copilot/issues"
+    ++ " or email the maintainers at <ivan.perezdominguez@nasa.gov>"
diff --git a/src/Copilot/Compile/Bluespec/Expr.hs b/src/Copilot/Compile/Bluespec/Expr.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Compile/Bluespec/Expr.hs
@@ -0,0 +1,465 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+-- | Translate Copilot Core expressions and operators to Bluespec.
+module Copilot.Compile.Bluespec.Expr
+  ( transExpr
+  , cIndexVector
+  , cLit
+  , constTy
+  , genVector
+  ) where
+
+-- External imports
+import Data.Foldable (foldl')
+import Data.String (IsString (..))
+import qualified Language.Bluespec.Classic.AST as BS
+import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS
+
+-- Internal imports: Copilot
+import Copilot.Core
+
+-- Internal imports
+import Copilot.Compile.Bluespec.Error (impossible)
+import Copilot.Compile.Bluespec.Name
+import Copilot.Compile.Bluespec.Type
+
+-- | Translates a Copilot Core expression into a Bluespec expression.
+transExpr :: Expr a -> BS.CExpr
+transExpr (Const ty x) = constTy ty x
+
+transExpr (Local ty1 _ name e1 e2) =
+  let nameId = BS.mkId BS.NoPos $ fromString name
+      e1'    = transExpr e1
+      ty1'   = transType ty1
+      e2'    = transExpr e2 in
+  BS.Cletrec
+    [ BS.CLValueSign
+        (BS.CDef nameId (BS.CQType [] ty1') [BS.CClause [] [] e1'])
+        []
+    ]
+    e2'
+
+transExpr (Var _ n) = BS.CVar $ BS.mkId BS.NoPos $ fromString n
+
+transExpr (Drop _ amount sid) =
+  let accessVar = streamAccessorName sid
+      index     = BS.LInt $ BS.ilDec $ fromIntegral amount in
+  BS.CApply (BS.CVar $ BS.mkId BS.NoPos $ fromString accessVar)
+            [BS.CLit $ BS.CLiteral BS.NoPos index]
+
+transExpr (ExternVar _ name _) =
+  let ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName in
+  BS.CSelect
+    (BS.CSelect
+      (BS.CVar ifcArgId)
+      (BS.mkId BS.NoPos $ fromString $ lowercaseName name))
+    (BS.id_read BS.NoPos)
+
+transExpr (Label _ _ e) = transExpr e -- ignore label
+
+transExpr (Op1 op e) = transOp1 op (transExpr e)
+
+transExpr (Op2 op e1 e2) = transOp2 op (transExpr e1) (transExpr e2)
+
+transExpr (Op3 op e1 e2 e3) =
+  transOp3 op (transExpr e1) (transExpr e2) (transExpr e3)
+
+-- | Translates a Copilot unary operator and its argument into a Bluespec
+-- function.
+transOp1 :: Op1 a b -> BS.CExpr -> BS.CExpr
+transOp1 op e =
+  case op of
+    Not         -> app BS.idNot
+    Abs     _ty -> app $ BS.mkId BS.NoPos "abs"
+    Sign    _ty -> app $ BS.mkId BS.NoPos "signum"
+    -- Bluespec's Arith class does not have a `recip` method corresponding to
+    -- Haskell's `recip` in the `Fractional` class, so we implement it
+    -- ourselves.
+    Recip    ty -> BS.CApply
+                     (BS.CVar (BS.idSlashAt BS.NoPos))
+                     [constNumTy ty 1, e]
+    BwNot   _ty -> app $ BS.idInvertAt BS.NoPos
+    Sqrt    _ty -> BS.CSelect
+                     (BS.CApply
+                       (BS.CVar (BS.mkId BS.NoPos "sqrtFP"))
+                       [e, fpRM])
+                     BS.idPrimFst
+
+    Cast fromTy toTy -> transCast fromTy toTy e
+    GetField (Struct _)  _ f -> BS.CSelect e $ BS.mkId BS.NoPos $
+                                fromString $ lowercaseName $ accessorName f
+    GetField _ _ _ -> impossible "transOp1" "copilot-bluespec"
+
+    -- Unsupported operations (see
+    -- https://github.com/B-Lang-org/bsc/discussions/534)
+    Exp     _ty -> unsupportedFPOp "exp"
+    Log     _ty -> unsupportedFPOp "log"
+    Acos    _ty -> unsupportedFPOp "acos"
+    Asin    _ty -> unsupportedFPOp "asin"
+    Atan    _ty -> unsupportedFPOp "atan"
+    Cos     _ty -> unsupportedFPOp "cos"
+    Sin     _ty -> unsupportedFPOp "sin"
+    Tan     _ty -> unsupportedFPOp "tan"
+    Acosh   _ty -> unsupportedFPOp "acosh"
+    Asinh   _ty -> unsupportedFPOp "asinh"
+    Atanh   _ty -> unsupportedFPOp "atanh"
+    Cosh    _ty -> unsupportedFPOp "cosh"
+    Sinh    _ty -> unsupportedFPOp "sinh"
+    Tanh    _ty -> unsupportedFPOp "tanh"
+    Ceiling _ty -> unsupportedFPOp "ceiling"
+    Floor   _ty -> unsupportedFPOp "floor"
+  where
+    app i = BS.CApply (BS.CVar i) [e]
+
+-- | Translates a Copilot binary operator and its arguments into a Bluespec
+-- function.
+transOp2 :: Op2 a b c -> BS.CExpr -> BS.CExpr -> BS.CExpr
+transOp2 op e1 e2 =
+  case op of
+    And          -> app BS.idAnd
+    Or           -> app $ BS.idOrAt BS.NoPos
+    Add      _ty -> app BS.idPlus
+    Sub      _ty -> app BS.idMinus
+    Mul      _ty -> app $ BS.idStarAt BS.NoPos
+    Mod      _ty -> app $ BS.idPercentAt BS.NoPos
+    Div      _ty -> app $ BS.idSlashAt BS.NoPos
+    Fdiv     _ty -> app $ BS.idSlashAt BS.NoPos
+    Eq       _   -> app BS.idEqual
+    Ne       _   -> app BS.idNotEqual
+    Le       _   -> app $ BS.idLtEqAt BS.NoPos
+    Ge       _   -> app $ BS.idGtEqAt BS.NoPos
+    Lt       _   -> app $ BS.idLtAt BS.NoPos
+    Gt       _   -> app $ BS.idGtAt BS.NoPos
+    BwAnd    _   -> app $ BS.idBitAndAt BS.NoPos
+    BwOr     _   -> app $ BS.idBitOrAt BS.NoPos
+    BwXor    _   -> app $ BS.idCaretAt BS.NoPos
+    BwShiftL _ _ -> app $ BS.idLshAt BS.NoPos
+    BwShiftR _ _ -> app $ BS.idRshAt BS.NoPos
+    Index    _   -> cIndexVector e1 e2
+
+    -- Unsupported operations (see
+    -- https://github.com/B-Lang-org/bsc/discussions/534)
+    Pow      _ty -> unsupportedFPOp "(**)"
+    Logb     _ty -> unsupportedFPOp "logb"
+    Atan2    _ty -> unsupportedFPOp "atan2"
+  where
+    app i = BS.CApply (BS.CVar i) [e1, e2]
+
+-- | Translates a Copilot ternary operator and its arguments into a Bluespec
+-- function.
+transOp3 :: Op3 a b c d -> BS.CExpr -> BS.CExpr -> BS.CExpr -> BS.CExpr
+transOp3 op e1 e2 e3 =
+  case op of
+    Mux _ -> BS.Cif BS.NoPos e1 e2 e3
+
+-- | Bluespec does not have a general-purpose casting operation, so we must
+-- handle casts on a case-by-case basis.
+transCast :: Type a -> Type b -> BS.CExpr -> BS.CExpr
+transCast fromTy toTy =
+  case (fromTy, toTy) of
+    -----
+    -- "safe" casts that cannot lose information
+    -----
+
+    (Bool,  Bool)    -> id
+    (Bool,  Word8)   -> upcastBool
+    (Bool,  Word16)  -> upcastBool
+    (Bool,  Word32)  -> upcastBool
+    (Bool,  Word64)  -> upcastBool
+    (Bool,  Int8)    -> upcastBool
+    (Bool,  Int16)   -> upcastBool
+    (Bool,  Int32)   -> upcastBool
+    (Bool,  Int64)   -> upcastBool
+
+    (Int8,  Int8)    -> id
+    (Int8,  Int16)   -> upcast
+    (Int8,  Int32)   -> upcast
+    (Int8,  Int64)   -> upcast
+    (Int16, Int16)   -> id
+    (Int16, Int32)   -> upcast
+    (Int16, Int64)   -> upcast
+    (Int32, Int32)   -> id
+    (Int32, Int64)   -> upcast
+    (Int64, Int64)   -> id
+
+    (Word8,  Int16)  -> unpackPackUpcast Word16
+    (Word8,  Int32)  -> unpackPackUpcast Word32
+    (Word8,  Int64)  -> unpackPackUpcast Word64
+    (Word8,  Word8)  -> id
+    (Word8,  Word16) -> upcast
+    (Word8,  Word32) -> upcast
+    (Word8,  Word64) -> upcast
+    (Word16, Int32)  -> unpackPackUpcast Word32
+    (Word16, Int64)  -> unpackPackUpcast Word64
+    (Word16, Word16) -> id
+    (Word16, Word32) -> upcast
+    (Word16, Word64) -> upcast
+    (Word32, Int64)  -> unpackPackUpcast Word64
+    (Word32, Word32) -> id
+    (Word32, Word64) -> upcast
+    (Word64, Word64) -> id
+
+    -----
+    -- "unsafe" casts, which may lose information
+    -----
+
+    -- unsigned truncations
+    (Word64, Word32) -> downcast
+    (Word64, Word16) -> downcast
+    (Word64, Word8)  -> downcast
+    (Word32, Word16) -> downcast
+    (Word32, Word8)  -> downcast
+    (Word16, Word8)  -> downcast
+
+    -- signed truncations
+    (Int64, Int32)   -> downcast
+    (Int64, Int16)   -> downcast
+    (Int64, Int8)    -> downcast
+    (Int32, Int16)   -> downcast
+    (Int32, Int8)    -> downcast
+    (Int16, Int8)    -> downcast
+
+    -- signed integer to float
+    (Int64, Float)   -> castIntegralToFloatingPoint
+    (Int32, Float)   -> castIntegralToFloatingPoint
+    (Int16, Float)   -> castIntegralToFloatingPoint
+    (Int8,  Float)   -> castIntegralToFloatingPoint
+
+    -- unsigned integer to float
+    (Word64, Float)  -> castIntegralToFloatingPoint
+    (Word32, Float)  -> castIntegralToFloatingPoint
+    (Word16, Float)  -> castIntegralToFloatingPoint
+    (Word8,  Float)  -> castIntegralToFloatingPoint
+
+    -- signed integer to double
+    (Int64, Double)  -> castIntegralToFloatingPoint
+    (Int32, Double)  -> castIntegralToFloatingPoint
+    (Int16, Double)  -> castIntegralToFloatingPoint
+    (Int8,  Double)  -> castIntegralToFloatingPoint
+
+    -- unsigned integer to double
+    (Word64, Double) -> castIntegralToFloatingPoint
+    (Word32, Double) -> castIntegralToFloatingPoint
+    (Word16, Double) -> castIntegralToFloatingPoint
+    (Word8,  Double) -> castIntegralToFloatingPoint
+
+    -- unsigned to signed conversion
+    (Word64, Int64)  -> unpackPack
+    (Word32, Int32)  -> unpackPack
+    (Word16, Int16)  -> unpackPack
+    (Word8,  Int8)   -> unpackPack
+
+    -- signed to unsigned conversion
+    (Int64, Word64)  -> unpackPack
+    (Int32, Word32)  -> unpackPack
+    (Int16, Word16)  -> unpackPack
+    (Int8,  Word8)   -> unpackPack
+
+    _ -> impossible "transCast" "copilot-bluespec"
+  where
+    -- unpackPack :: (Bits fromTy n, Bits toTy n) => fromTy -> toTy
+    -- unpackPack e = (unpack (pack e)) :: toTy
+    --
+    -- The most basic cast. Used when fromTy and toTy are both integral types
+    -- with the same number of bits.
+    unpackPack :: BS.CExpr -> BS.CExpr
+    unpackPack e = withTypeAnnotation toTy $
+                   BS.CApply
+                     (BS.CVar BS.idUnpack)
+                     [BS.CApply (BS.CVar BS.idPack) [e]]
+
+    -- upcastBool :: (Add k 1 n, Bits toTy n) => Bool -> toTy
+    -- upcastBool b = (unpack (extend (pack b))) :: toTy
+    --
+    -- Cast a Bool to a `Bits 1` value, extend it to `Bits n`, and then
+    -- convert it back to an integral type.
+    upcastBool :: BS.CExpr -> BS.CExpr
+    upcastBool e = withTypeAnnotation toTy $
+                   BS.CApply
+                     (BS.CVar BS.idUnpack)
+                     [BS.CApply extendExpr [BS.CApply (BS.CVar BS.idPack) [e]]]
+
+    -- upcast :: (BitExtend m n x) => x m -> x n
+    -- upcast e = (extend e) :: ty
+    --
+    -- Convert a narrower integral type to a wider integral type (e.g.,
+    -- `UInt 8` to `UInt 64` or `Int 8` to `Int 64`). Note that the `extend`
+    -- operation is smart enough to choose between sign-extension and
+    -- zero-extension depending on whether `x m` (i.e., fromTy) is a signed
+    -- or unsigned type, respectively.
+    upcast :: BS.CExpr -> BS.CExpr
+    upcast e = withTypeAnnotation toTy $ BS.CApply extendExpr [e]
+
+    -- downcast :: (BitExtend m n x) => x n -> x m
+    -- downcast e = (truncate e) :: ty
+    --
+    -- Convert a wider integral type to a narrow integral type (e.g.,
+    -- `UInt 64` to `UInt 8` or `Int 64` to `Int 8`) by truncating the most
+    -- significant bits.
+    downcast :: BS.CExpr -> BS.CExpr
+    downcast e = withTypeAnnotation toTy $ BS.CApply truncateExpr [e]
+
+    -- Apply upcast followed by unpackPack. This requires supplying the type to
+    -- upcast to for type disambiguation purposes.
+    unpackPackUpcast :: Type a -> BS.CExpr -> BS.CExpr
+    unpackPackUpcast upcastTy e = unpackPack $
+      withTypeAnnotation upcastTy $ BS.CApply extendExpr [e]
+
+    -- castIntegralToFloatingPoint :: (FixedFloatCVT fromTy toTy) => fromTy toTy
+    -- castIntegralToFloatingPoint e =
+    --   ((vFixedToFloat e (0 :: UInt 64) Rnd_Nearest_Even).fst) :: tfl
+    --
+    -- While FloatingPoint does have a Bits instance, we don't want to convert
+    -- an integral type to a FloatingPoint type using the Bits class, as the
+    -- bit representation of an integral value differs quite a bit from the bit
+    -- representation of a FloatingPoint value. Instead, we use the
+    -- special-purpose FixedFloatCVT class for this task.
+    castIntegralToFloatingPoint :: BS.CExpr -> BS.CExpr
+    castIntegralToFloatingPoint e =
+      withTypeAnnotation toTy $
+      BS.CSelect
+        (BS.CApply
+          (BS.CVar (BS.mkId BS.NoPos "vFixedToFloat"))
+          [ e
+          , constNumTy Word64 0
+          , fpRM
+          ])
+        BS.idPrimFst
+
+    extendExpr   = BS.CVar $ BS.mkId BS.NoPos "extend"
+    truncateExpr = BS.CVar $ BS.mkId BS.NoPos "truncate"
+
+-- | Transform a Copilot Core literal, based on its value and type, into a
+-- Bluespec expression.
+constTy :: Type a -> a -> BS.CExpr
+constTy ty =
+  case ty of
+    -- The treatment of scalar types is relatively straightforward. Note that
+    -- Bool is an enum, so we must construct it using a CCon rather than with
+    -- a CLit.
+    Bool      -> \v -> BS.CCon (if v then BS.idTrue else BS.idFalse) []
+    Int8      -> constInt ty . toInteger
+    Int16     -> constInt ty . toInteger
+    Int32     -> constInt ty . toInteger
+    Int64     -> constInt ty . toInteger
+    Word8     -> constInt ty . toInteger
+    Word16    -> constInt ty . toInteger
+    Word32    -> constInt ty . toInteger
+    Word64    -> constInt ty . toInteger
+    Float     -> constFP ty . realToFrac
+    Double    -> constFP ty
+
+    -- Translating a Copilot array literal to a Bluespec Vector is somewhat
+    -- involved. Given a Copilot array {x_0, ..., x_(n-1)}, the
+    -- corresponding Bluespec Vector will look something like:
+    --
+    --   let arr = update (... (update newVector 0 x_0)) (n-1) x_(n-1)
+    --
+    -- We use the `update` function instead of the := syntax (e.g.,
+    -- { array_temp[0] := x; array_temp[1] := y; ...}) so that we can construct
+    -- a Vector in a pure context.
+    Array ty' -> constVector ty' . arrayElems
+
+    -- Converting a Copilot struct { field_0 = x_0, ..., field_(n-1) = x_(n-1) }
+    -- to a Bluespec struct is quite straightforward, given Bluespec's struct
+    -- initialization syntax.
+    Struct s -> \v ->
+      BS.CStruct
+        (Just True)
+        (BS.mkId BS.NoPos $ fromString $ uppercaseName $ typeName s)
+        (map (\(Value ty'' field@(Field val)) ->
+               ( BS.mkId BS.NoPos $ fromString
+                                  $ lowercaseName
+                                  $ fieldName field
+               , constTy ty'' val
+               ))
+             (toValues v))
+
+-- | Transform a list of Copilot Core expressions of a given 'Type' into a
+-- Bluespec @Vector@ expression.
+constVector :: Type a -> [a] -> BS.CExpr
+constVector ty = genVector (\_ -> constTy ty)
+
+-- | Transform a list of Copilot Core expressions into a Bluespec @Vector@
+-- expression. When invoking @genVector f es@, where @es@ has length @n@, the
+-- resulting @Vector@ will consist of
+-- @[f 0 (es !! 0), f 1 (es !! 1), ..., f (n-1) (es !! (n-1))]@.
+genVector :: (Int -> a -> BS.CExpr) -> [a] -> BS.CExpr
+genVector f vec =
+  snd $
+  foldl'
+    (\(!i, !v) x ->
+      ( i+1
+      , BS.CApply
+          (BS.CVar (BS.mkId BS.NoPos "update"))
+          [ v
+          , cLit (BS.LInt (BS.ilDec (toInteger i)))
+          , f i x
+          ]
+      ))
+    (0, BS.CVar (BS.mkId BS.NoPos "newVector"))
+    vec
+
+-- | Translate a literal number of type @ty@ into a Bluespec expression.
+--
+-- PRE: The type of PRE is numeric (integer or floating-point), that
+-- is, not boolean, struct or array.
+constNumTy :: Type a -> Integer -> BS.CExpr
+constNumTy ty =
+  case ty of
+    Float  -> constFP ty . fromInteger
+    Double -> constFP ty . fromInteger
+    _      -> constInt ty
+
+-- | Translate a Copilot integer literal into a Bluespec expression.
+constInt :: Type a -> Integer -> BS.CExpr
+constInt ty i
+    -- Bluespec intentionally does not support negative literal syntax (e.g.,
+    -- -42), so we must create negative integer literals using the `negate`
+    -- function.
+    | i >= 0    = withTypeAnnotation ty $ cLit $ BS.LInt $ BS.ilDec i
+    | otherwise = withTypeAnnotation ty $
+                  BS.CApply
+                    (BS.CVar $ BS.idNegateAt BS.NoPos)
+                    [cLit $ BS.LInt $ BS.ilDec $ negate i]
+
+-- | Translate a Copilot floating-point literal into a Bluespec expression.
+constFP :: Type ty -> Double -> BS.CExpr
+constFP ty d
+    -- Bluespec intentionally does not support negative literal syntax (e.g.,
+    -- -42.5), so we must create negative floating-point literals using the
+    -- `negate` function.
+    | d >= 0    = withTypeAnnotation ty $ cLit $ BS.LReal d
+    | otherwise = withTypeAnnotation ty $
+                  BS.CApply
+                    (BS.CVar $ BS.idNegateAt BS.NoPos)
+                    [cLit $ BS.LReal $ negate d]
+
+-- | Create a Bluespec expression consisting of a literal.
+cLit :: BS.Literal -> BS.CExpr
+cLit = BS.CLit . BS.CLiteral BS.NoPos
+
+-- | Create a Bluespec expression that indexes into a @Vector@.
+cIndexVector :: BS.CExpr -> BS.CExpr -> BS.CExpr
+cIndexVector vec idx =
+  BS.CApply (BS.CVar (BS.mkId BS.NoPos "select")) [vec, idx]
+
+-- | Explicitly annotate an expression with a type signature. This is necessary
+-- to prevent expressions from having ambiguous types in certain situations.
+withTypeAnnotation :: Type a -> BS.CExpr -> BS.CExpr
+withTypeAnnotation ty e = e `BS.CHasType` BS.CQType [] (transType ty)
+
+-- | Throw an error if attempting to use a floating-point operation that
+-- Bluespec does not currently support.
+unsupportedFPOp :: String -> a
+unsupportedFPOp op =
+  error $ "Bluespec's FloatingPoint type does not support the " ++ op ++
+          " operation."
+
+-- | We assume round-near-even throughout, but this variable can be changed if
+-- needed. This matches the behavior of @fpRM@ in @copilot-theorem@'s
+-- @Copilot.Theorem.What4.Translate@ module.
+fpRM :: BS.CExpr
+fpRM = BS.CCon (BS.mkId BS.NoPos "Rnd_Nearest_Even") []
diff --git a/src/Copilot/Compile/Bluespec/Name.hs b/src/Copilot/Compile/Bluespec/Name.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Compile/Bluespec/Name.hs
@@ -0,0 +1,95 @@
+-- | Naming of variables and functions in Bluespec.
+module Copilot.Compile.Bluespec.Name
+  ( argNames
+  , generatorName
+  , guardName
+  , ifcArgName
+  , indexName
+  , lowercaseName
+  , specIfcName
+  , specIfcPkgName
+  , specTypesPkgName
+  , streamAccessorName
+  , streamElemName
+  , streamName
+  , uppercaseName
+  ) where
+
+-- External imports
+import Data.Char (isLower, isUpper)
+
+-- External imports: Copilot
+import Copilot.Core (Id)
+
+-- | Turn a specification name into the name of its module interface.
+specIfcName :: String -> String
+specIfcName prefix = uppercaseName (specIfcPkgName prefix)
+
+-- | Turn a specification name into the name of the package that declares its
+-- module interface. Note that 'specIfcPkgName' is not necessarily the same name
+-- as 'specIfcName', as the former does not need to begin with an uppercase
+-- letter, but the latter does.
+specIfcPkgName :: String -> String
+specIfcPkgName prefix = prefix ++ "Ifc"
+
+-- | Turn a specification name into the name of the package that declares its
+-- struct types.
+specTypesPkgName :: String -> String
+specTypesPkgName prefix = prefix ++ "Types"
+
+-- | Turn a stream id into a stream element name.
+streamElemName :: Id -> Int -> String
+streamElemName sId n = streamName sId ++ "_" ++ show n
+
+-- | The name of the variable of type @<prefix>Ifc@. This is used to select
+-- trigger functions and external variables.
+ifcArgName :: String
+ifcArgName = "ifc"
+
+-- | Create a Bluespec name that must start with an uppercase letter (e.g., a
+-- struct or interface name). If the supplied name already begins with an
+-- uppercase letter, this function returns the name unchanged. Otherwise, this
+-- function prepends a @BS_@ prefix (short for \"Bluespec\") at the front.
+uppercaseName :: String -> String
+uppercaseName [] = []
+uppercaseName n@(c:_)
+  | isUpper c = n
+  | otherwise = "BS_" ++ n
+
+-- | Create a Bluespec name that must start with a lowercase letter (e.g., a
+-- function or method name). If the supplied name already begins with a
+-- lowercase letter, this function returns the name unchanged. Otherwise, this
+-- function prepends a @bs_@ prefix (short for \"Bluespec\") at the front.
+lowercaseName :: String -> String
+lowercaseName [] = []
+lowercaseName n@(c:_)
+  | isLower c = n
+  | otherwise = "bs_" ++ n
+
+-- | Turn a stream id into a suitable Bluespec variable name.
+streamName :: Id -> String
+streamName sId = "s" ++ show sId
+
+-- | Turn a stream id into the global varname for indices.
+indexName :: Id -> String
+indexName sId = streamName sId ++ "_idx"
+
+-- | Turn a stream id into the name of its accessor function
+streamAccessorName :: Id -> String
+streamAccessorName sId = streamName sId ++ "_get"
+
+-- | Turn stream id into name of its generator function.
+generatorName :: Id -> String
+generatorName sId = streamName sId ++ "_gen"
+
+-- | Turn the name of a trigger into a guard generator.
+guardName :: String -> String
+guardName name = lowercaseName name ++ "_guard"
+
+-- | Turn a trigger name into a an trigger argument name.
+argName :: String -> Int -> String
+argName name n = lowercaseName name ++ "_arg" ++ show n
+
+-- | Enumerate all argument names based on trigger name.
+argNames :: String -> [String]
+argNames base = map (argName base) [0..]
diff --git a/src/Copilot/Compile/Bluespec/Settings.hs b/src/Copilot/Compile/Bluespec/Settings.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Compile/Bluespec/Settings.hs
@@ -0,0 +1,14 @@
+-- | Settings used by the code generator to customize the code.
+module Copilot.Compile.Bluespec.Settings
+  ( BluespecSettings(..)
+  , mkDefaultBluespecSettings
+  ) where
+
+-- | Settings used to customize the code generated.
+newtype BluespecSettings = BluespecSettings
+  { bluespecSettingsOutputDirectory :: FilePath
+  }
+
+-- | Default Bluespec settings. Output to the current directory.
+mkDefaultBluespecSettings :: BluespecSettings
+mkDefaultBluespecSettings = BluespecSettings "."
diff --git a/src/Copilot/Compile/Bluespec/Type.hs b/src/Copilot/Compile/Bluespec/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Compile/Bluespec/Type.hs
@@ -0,0 +1,95 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+-- | Translate Copilot Core expressions and operators to Bluespec.
+module Copilot.Compile.Bluespec.Type
+  ( transType
+  , tVector
+  ) where
+
+-- External imports
+import Data.String (IsString (..))
+import qualified Language.Bluespec.Classic.AST as BS
+import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS
+import qualified Language.Bluespec.Classic.AST.Builtin.Types as BS
+
+-- Internal imports: Copilot
+import Copilot.Core
+
+-- Internal imports
+import Copilot.Compile.Bluespec.Name
+
+-- | Translate a Copilot type to a Bluespec type.
+transType :: Type a -> BS.CType
+transType ty = case ty of
+  Bool   -> BS.tBool
+  Int8   -> BS.tInt  `BS.TAp` BS.cTNum  8 BS.NoPos
+  Int16  -> BS.tInt  `BS.TAp` BS.cTNum 16 BS.NoPos
+  Int32  -> BS.tInt  `BS.TAp` BS.cTNum 32 BS.NoPos
+  Int64  -> BS.tInt  `BS.TAp` BS.cTNum 64 BS.NoPos
+  Word8  -> BS.tUInt `BS.TAp` BS.cTNum  8 BS.NoPos
+  Word16 -> BS.tUInt `BS.TAp` BS.cTNum 16 BS.NoPos
+  Word32 -> BS.tUInt `BS.TAp` BS.cTNum 32 BS.NoPos
+  Word64 -> BS.tUInt `BS.TAp` BS.cTNum 64 BS.NoPos
+
+  Float -> BS.TCon $
+    BS.TyCon
+      { BS.tcon_name = BS.mkId BS.NoPos "Float"
+      , BS.tcon_kind = Just BS.KStar
+      , BS.tcon_sort = BS.TItype 0 $ tFloatingPoint `BS.TAp`
+                                     BS.cTNum  8 BS.NoPos `BS.TAp`
+                                     BS.cTNum 23 BS.NoPos
+      }
+  Double -> BS.TCon $
+    BS.TyCon
+      { BS.tcon_name = BS.mkId BS.NoPos "Double"
+      , BS.tcon_kind = Just BS.KStar
+      , BS.tcon_sort = BS.TItype 0 $ tFloatingPoint `BS.TAp`
+                                     BS.cTNum 11 BS.NoPos `BS.TAp`
+                                     BS.cTNum 52 BS.NoPos
+      }
+  Array ty' -> tVector `BS.TAp` BS.cTNum len BS.NoPos `BS.TAp` transType ty'
+    where
+      len = toInteger $ typeLength ty
+  Struct s -> BS.TCon $
+    BS.TyCon
+      { BS.tcon_name = BS.mkId BS.NoPos $
+                       fromString $
+                       uppercaseName $
+                       typeName s
+      , BS.tcon_kind = Just BS.KStar
+      , BS.tcon_sort =
+          BS.TIstruct BS.SStruct $
+          map (\(Value _tu field) ->
+                BS.mkId BS.NoPos $
+                fromString $
+                lowercaseName $
+                fieldName field)
+              (toValues s)
+      }
+
+-- | The @Vector@ Bluespec data type.
+tVector :: BS.CType
+tVector = BS.TCon $
+  BS.TyCon
+    { BS.tcon_name = BS.idVector
+    , BS.tcon_kind = Just (BS.Kfun BS.KNum (BS.Kfun BS.KStar BS.KStar))
+    , BS.tcon_sort =
+        BS.TIdata
+          { BS.tidata_cons = [BS.mkId BS.NoPos "V"]
+          , BS.tidata_enum = False
+          }
+    }
+
+-- | The @FloatingPoint@ Bluespec struct type.
+tFloatingPoint :: BS.CType
+tFloatingPoint = BS.TCon $
+  BS.TyCon
+    { BS.tcon_name = BS.mkId BS.NoPos "FloatingPoint"
+    , BS.tcon_kind = Just (BS.Kfun BS.KNum (BS.Kfun BS.KNum BS.KStar))
+    , BS.tcon_sort =
+        BS.TIstruct BS.SStruct [ BS.mkId BS.NoPos "sign"
+                               , BS.mkId BS.NoPos "exp"
+                               , BS.mkId BS.NoPos "sfd"
+                               ]
+    }
diff --git a/tests/Main.hs b/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Main.hs
@@ -0,0 +1,18 @@
+-- | Test copilot-bluespec.
+module Main where
+
+-- External imports
+import Test.Framework (Test, defaultMain)
+
+-- Internal library modules being tested
+import qualified Test.Copilot.Compile.Bluespec
+
+-- | Run all unit tests on copilot-bluespec.
+main :: IO ()
+main = defaultMain tests
+
+-- | All unit tests in copilot-bluespec.
+tests :: [Test.Framework.Test]
+tests =
+  [ Test.Copilot.Compile.Bluespec.tests
+  ]
diff --git a/tests/Test/Copilot/Compile/Bluespec.hs b/tests/Test/Copilot/Compile/Bluespec.hs
new file mode 100644
--- /dev/null
+++ b/tests/Test/Copilot/Compile/Bluespec.hs
@@ -0,0 +1,971 @@
+{-# LANGUAGE BangPatterns        #-}
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+-- | Test copilot-bluespec:Copilot.Compile.Bluespec.
+module Test.Copilot.Compile.Bluespec
+    ( tests )
+  where
+
+-- External imports
+import Control.Arrow                        ((&&&))
+import Control.Exception                    (IOException, catch)
+import Control.Monad                        (when)
+import Data.Bits                            (Bits, complement)
+import Data.Foldable                        (foldl')
+import Data.List                            (intercalate)
+import Data.Type.Equality                   (testEquality)
+import Data.Typeable                        (Proxy (..), (:~:) (Refl))
+import GHC.TypeLits                         (KnownNat, natVal)
+import System.Directory                     (doesFileExist,
+                                             getTemporaryDirectory,
+                                             removeDirectoryRecursive,
+                                             setCurrentDirectory)
+import System.IO                            (hPutStrLn, stderr)
+import System.Posix.Temp                    (mkdtemp)
+import System.Process                       (callProcess, readProcess)
+import System.Random                        (Random)
+import Test.Framework                       (Test, testGroup)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.QuickCheck                      (Arbitrary, Gen, Property,
+                                             arbitrary, choose, elements,
+                                             forAll, forAllBlind, frequency,
+                                             getPositive, ioProperty, oneof,
+                                             vectorOf, withMaxSuccess, (.&&.))
+import Test.QuickCheck.Gen                  (chooseAny, chooseBoundedIntegral)
+
+-- External imports: Copilot
+import Copilot.Core hiding (Property)
+
+-- External imports: Modules being tested
+import Copilot.Compile.Bluespec          (bluespecSettingsOutputDirectory,
+                                          compile, compileWith,
+                                          mkDefaultBluespecSettings)
+import Copilot.Compile.Bluespec.External (External (extName), gatherExts)
+
+-- * Constants
+
+-- | All unit tests for copilot-bluespec:Copilot.Compile.Bluespec.
+tests :: Test.Framework.Test
+tests =
+  testGroup "Copilot.Compile.Bluespec"
+    [ testProperty "Compile specification"               testCompile
+    , testProperty "Compile specification in custom dir" testCompileCustomDir
+    , testProperty "Run specification"                   testRun
+    , testProperty "Run and compare results"             testRunCompare
+    ]
+
+-- * Individual tests
+
+-- | Test compiling a spec.
+testCompile :: Property
+testCompile = ioProperty $ do
+    tmpDir <- getTemporaryDirectory
+    setCurrentDirectory tmpDir
+
+    testDir <- mkdtemp "CopilotTest"
+    setCurrentDirectory testDir
+
+    compile "CopilotTest" spec
+    r <- compileBluespec "CopilotTest" []
+
+    setCurrentDirectory tmpDir
+    removeDirectoryRecursive testDir
+
+    return r
+
+  where
+
+    spec = Spec streams observers triggers properties
+
+    streams    = []
+    observers  = []
+    triggers   = [ Trigger function guard args ]
+    properties = []
+
+    function = "func"
+
+    guard = Const Bool True
+
+    args = []
+
+-- | Test compiling a spec in a custom directory.
+testCompileCustomDir :: Property
+testCompileCustomDir = ioProperty $ do
+    tmpDir <- getTemporaryDirectory
+    setCurrentDirectory tmpDir
+
+    testDir <- mkdtemp "CopilotTest"
+
+    compileWith (mkDefaultBluespecSettings
+                   { bluespecSettingsOutputDirectory = testDir })
+                "CopilotTest"
+                spec
+
+    setCurrentDirectory testDir
+    r <- compileBluespec "CopilotTest" []
+
+    setCurrentDirectory tmpDir
+    removeDirectoryRecursive testDir
+
+    return r
+
+  where
+
+    spec = Spec streams observers triggers properties
+
+    streams    = []
+    observers  = []
+    triggers   = [ Trigger function guard args ]
+    properties = []
+
+    function = "nop"
+
+    guard = Const Bool True
+
+    args = []
+
+-- | Test compiling a spec and running the resulting program.
+--
+-- The actual behavior is ignored.
+testRun :: Property
+testRun = ioProperty $ do
+    tmpDir <- getTemporaryDirectory
+    setCurrentDirectory tmpDir
+
+    testDir <- mkdtemp "CopilotTest"
+    setCurrentDirectory testDir
+
+    let bluespecProgram = unlines
+          [ "package Top where"
+          , ""
+          , "import CopilotTest"
+          , "import CopilotTestIfc"
+          , "import CopilotTestTypes"
+          , ""
+          , "copilotTestIfc :: Module CopilotTestIfc"
+          , "copilotTestIfc ="
+          , "  module"
+          , "    interface"
+          , "      nop :: Action"
+          , "      nop = return ()"
+          , ""
+          , "mkTop :: Module Empty"
+          , "mkTop = mkCopilotTest copilotTestIfc"
+          ]
+
+    writeFile "Top.bs" bluespecProgram
+
+    compile "CopilotTest" spec
+    r <- compileBluespec "Top" ["-g", "mkTop"]
+
+    -- Compile a main program
+    r2 <- compileExecutable "mkTop"
+    callProcess "./mkTop" ["-m", "2"]
+
+    setCurrentDirectory tmpDir
+    removeDirectoryRecursive testDir
+
+    return $ r && r2
+
+  where
+
+    spec = Spec streams observers triggers properties
+
+    streams    = []
+    observers  = []
+    triggers   = [ Trigger function guard args ]
+    properties = []
+
+    function = "nop"
+
+    guard = Const Bool True
+
+    args = []
+
+-- | Test running compiled spec and comparing the results to the
+-- expectation.
+testRunCompare :: Property
+testRunCompare =
+  -- It takes a pretty long time to run these tests, so we set the maximum
+  -- number of successful tests to 5 instead of the default (100) for the sake
+  -- of making the test suite complete in a more reasonable amount of time.
+  withMaxSuccess 5 $
+       testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int8   Bool))
+  .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int16  Bool))
+  .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int32  Bool))
+  .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int64  Bool))
+  .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word8  Bool))
+  .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word16 Bool))
+  .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word32 Bool))
+  .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word64 Bool))
+  .&&. testRunCompare1 (arbitraryOpFloatingBool :: Gen (TestCase1 Float  Bool))
+  .&&. testRunCompare1 (arbitraryOpFloatingBool :: Gen (TestCase1 Double Bool))
+  .&&. testRunCompare1 (arbitraryOpStruct       :: Gen (TestCase1 MyStruct Int8))
+  .&&. testRunCompare2 (arbitraryArrayNum       :: Gen (TestCase2 (Array 2 Int8) Word32 Int8))
+  .&&. testRunCompare2 (arbitraryArrayNum       :: Gen (TestCase2 (Array 2 Int16) Word32 Int16))
+
+-- * Random generators
+
+-- ** Random function generators
+
+-- | Generator of functions that produce booleans.
+arbitraryOpBool :: Typed a => Gen (Fun a Bool, [a] -> [Bool])
+arbitraryOpBool =
+  frequency
+    [ (5, arbitraryOp1Any)
+    , (5, funCompose1 <$> arbitraryOp1Bool <*> arbitraryOpBool)
+    , (2, funCompose2 <$> arbitraryOp2Bool <*> arbitraryOpBool <*> arbitraryOpBool)
+    , (1, funCompose2 <$> arbitraryOp2Eq   <*> arbitraryOpBool <*> arbitraryOpBool)
+    ]
+
+-- | Generator of functions that take Bits and produce booleans.
+arbitraryOpBoolBits :: (Typed a, Bits a) => Gen (Fun a Bool, [a] -> [Bool])
+arbitraryOpBoolBits =
+  frequency
+    [ (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpBits <*> arbitraryOpBits)
+    ]
+
+-- | Generator of functions that take Nums and produce booleans.
+arbitaryOpBoolOrdEqNum :: (Typed a, Eq a, Ord a, Num a)
+                       => Gen (Fun a Bool, [a] -> [Bool])
+arbitaryOpBoolOrdEqNum =
+  frequency
+    [ (1, funCompose2 <$> arbitraryOp2Eq  <*> arbitraryOpNum <*> arbitraryOpNum)
+    , (1, funCompose2 <$> arbitraryOp2Ord <*> arbitraryOpNum <*> arbitraryOpNum)
+    ]
+
+-- | Generator of functions that take Floating point numbers and produce
+-- booleans.
+arbitraryOpBoolEqNumFloat :: (Typed t, Eq t, Num t, Floating t)
+                          => Gen (Fun t Bool, [t] -> [Bool])
+arbitraryOpBoolEqNumFloat =
+  frequency
+    [ (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpNum   <*> arbitraryOpFloat)
+    , (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpFloat <*> arbitraryOpNum)
+    ]
+
+-- | Generator of functions that take and produce Bits.
+arbitraryOpBits :: (Bits t, Typed t)
+                => Gen (Fun t t, [t] -> [t])
+arbitraryOpBits = elements
+  [ (Op1 (BwNot typeOf), fmap complement)
+  ]
+
+-- | Generator of functions that take and produce Nums.
+arbitraryOpNum :: (Typed t, Num t) => Gen (Fun t t, [t] -> [t])
+arbitraryOpNum = elements
+  [ (Op1 (Abs typeOf),  fmap abs)
+  , (Op1 (Sign typeOf), fmap signum)
+  ]
+
+-- | Generator of functions that take an arrays and indicates and produce
+-- elements from the array.
+arbitraryArrayIx :: forall t n . (Typed t, KnownNat n, Num t)
+                 => Gen ( Fun2 (Array n t) Word32 t
+                        , [Array n t] -> [Word32] -> [t]
+                        )
+arbitraryArrayIx = return
+  (Op2 (Index typeOf), zipWith (\x y -> arrayElems x !! fromIntegral y))
+
+-- | Generator of functions that take structs produce fields of the struct.
+arbitraryStructField :: Gen ( Fun MyStruct Int8
+                            , [MyStruct] -> [Int8]
+                            )
+arbitraryStructField = elements
+  [ (Op1 (GetField typeOf typeOf myStruct1), fmap (unField . myStruct1))
+  , (Op1 (GetField typeOf typeOf myStruct2), fmap (unField . myStruct2))
+  ]
+
+-- | Generator of functions on Floating point numbers.
+arbitraryOpFloat :: (Floating t, Typed t) => Gen (Fun t t, [t] -> [t])
+arbitraryOpFloat = elements
+  [ (Op1 (Sqrt typeOf),  fmap sqrt)
+  , (Op1 (Recip typeOf), fmap recip)
+  ]
+
+-- | Generator of functions on that produce elements of any type.
+arbitraryOp1Any :: forall a b
+                .  (Arbitrary b, Typed a, Typed b)
+                => Gen (Fun a b, [a] -> [b])
+arbitraryOp1Any = oneof $
+    [ (\v -> (\_ -> Const typeOf v, fmap (const v))) <$> arbitrary ]
+    ++
+    rest
+  where
+    rest | Just Refl <- testEquality t1 t2
+         = [return (id, id)]
+         | otherwise
+         = []
+
+    t1 :: Type a
+    t1 = typeOf
+
+    t2 :: Type b
+    t2 = typeOf
+
+-- | Generator of functions on Booleans.
+arbitraryOp1Bool :: Gen (Fun Bool Bool, [Bool] -> [Bool])
+arbitraryOp1Bool = elements
+  [ (Op1 Not, fmap not)
+  ]
+
+-- | Generator of binary functions on Booleans.
+arbitraryOp2Bool :: Gen (Fun2 Bool Bool Bool, [Bool] -> [Bool] -> [Bool])
+arbitraryOp2Bool = elements
+  [ (Op2 And, zipWith (&&))
+  , (Op2 Or,  zipWith (||))
+  ]
+
+-- | Generator of binary functions that take two Eq elements of the same type
+-- and return a Bool.
+arbitraryOp2Eq :: (Typed t, Eq t)
+               => Gen (Fun2 t t Bool, [t] -> [t] -> [Bool])
+arbitraryOp2Eq = elements
+  [ (Op2 (Eq typeOf), zipWith (==))
+  , (Op2 (Ne typeOf), zipWith (/=))
+  ]
+
+-- | Generator of binary functions that take two Ord elements of the same type
+-- and return a Bool.
+arbitraryOp2Ord :: (Typed t, Ord t)
+                => Gen (Fun2 t t Bool, [t] -> [t] -> [Bool])
+arbitraryOp2Ord = elements
+  [ (Op2 (Le typeOf), zipWith (<=))
+  , (Op2 (Lt typeOf), zipWith (<))
+  , (Op2 (Ge typeOf), zipWith (>=))
+  , (Op2 (Gt typeOf), zipWith (>))
+  ]
+
+-- ** Random data generators
+
+-- | Random array generator.
+arbitraryArray :: forall n t . (KnownNat n, Random t) => Gen (Array n t)
+arbitraryArray = array <$> vectorOf len chooseAny
+  where
+   len :: Int
+   len = fromIntegral $ natVal (Proxy :: Proxy n)
+
+-- | Random struct generator.
+arbitraryStruct :: Gen MyStruct
+arbitraryStruct = do
+   fld1 <- Field <$> gen
+   fld2 <- Field <$> gen
+   return $ MyStruct fld1 fld2
+  where
+   gen :: Gen Int8
+   gen = chooseBoundedIntegral (minBound, maxBound)
+
+-- ** Random test case generators
+
+-- | Generator for test cases on integral numbers that produce booleans.
+arbitraryOpIntegralBool :: (Typed t, Bounded t, Integral t, Bits t)
+                        => Gen (TestCase1 t Bool)
+arbitraryOpIntegralBool = frequency
+  [ (5, mkTestCase1
+          arbitraryOpBool
+          (chooseBoundedIntegral (minBound, maxBound)))
+
+  , (2, mkTestCase1
+          arbitraryOpBoolBits
+          (chooseBoundedIntegral (minBound, maxBound)))
+
+    -- we need to use +1 because certain operations overflow the number
+  , (2, mkTestCase1
+          arbitaryOpBoolOrdEqNum
+          (chooseBoundedIntegral (minBound + 1, maxBound)))
+  ]
+
+-- | Generator for test cases on floating-point numbers that produce booleans.
+arbitraryOpFloatingBool :: (Random t, Typed t, Floating t, Eq t)
+                        => Gen (TestCase1 t Bool)
+arbitraryOpFloatingBool = oneof
+  [ mkTestCase1 arbitraryOpBoolEqNumFloat chooseAny
+  ]
+
+-- | Generator for test cases on Arrays selection producing values of the
+-- array.
+arbitraryArrayNum :: forall n a
+                  .  (KnownNat n, Num a, Random a, Typed a)
+                  => Gen (TestCase2 (Array n a) Word32 a)
+arbitraryArrayNum = oneof
+    [ mkTestCase2 arbitraryArrayIx arbitraryArray gen
+    ]
+  where
+   gen :: Gen Word32
+   gen = choose (0, len - 1)
+
+   len :: Word32
+   len = fromIntegral $ natVal (Proxy :: Proxy n)
+
+-- | Generator for test cases on structs that produce fields of the struct.
+arbitraryOpStruct :: Gen (TestCase1 MyStruct Int8)
+arbitraryOpStruct = oneof
+    [ mkTestCase1
+        arbitraryStructField
+        arbitraryStruct
+    ]
+
+-- * Semantics
+
+-- ** Functions
+
+-- | Unary Copilot function.
+type Fun a b = Expr a -> Expr b
+
+-- | Binary Copilot function.
+type Fun2 a b c = Expr a -> Expr b -> Expr c
+
+-- | Compose functions, paired with the Haskell functions that define their
+-- idealized meaning.
+funCompose1 :: (Fun b c, [b] -> [c])
+            -> (Fun a b, [a] -> [b])
+            -> (Fun a c, [a] -> [c])
+funCompose1 (f1, g1) (f2, g2) = (f1 . f2, g1 . g2)
+
+-- | Compose a binary function, with two functions, one for each argument.
+funCompose2 :: (Fun2 b c d, [b] -> [c] -> [d])
+            -> (Fun a b, [a] -> [b])
+            -> (Fun a c, [a] -> [c])
+            -> (Fun a d, [a] -> [d])
+funCompose2 (f1, g1) (f2, g2) (f3, g3) =
+  (uncurry f1 . (f2 &&& f3), uncurry g1 . (g2 &&& g3))
+
+-- ** Test cases
+
+-- | Test case specification for specs with one input variable and one output.
+data TestCase1 a b = TestCase1
+  { wrapTC1Expr :: Spec
+    -- ^ Specification containing a trigger an extern of type 'a' and a trigger
+    -- with an argument of type 'b'.
+
+  , wrapTC1Fun :: [a] -> [b]
+    -- ^ Function expected to function in the same way as the Spec being
+    -- tested.
+
+  , wrapTC1CopInp :: (Type a, String, Gen a)
+    -- ^ Input specification.
+    --
+    -- - The first element contains the type of the input in Bluespec.
+    --
+    -- - The second contains the variable name in Bluespec.
+    --
+    -- - The latter contains a randomized generator for values of the given
+    -- type.
+
+  , wrapTC1CopOut :: Type b
+    -- ^ The type of the output in Bluespec.
+  }
+
+-- | Test case specification for specs with two input variables and one output.
+data TestCase2 a b c = TestCase2
+  { wrapTC2Expr :: Spec
+    -- ^ Specification containing a trigger an extern of type 'a' and a trigger
+    -- with an argument of type 'b'.
+
+  , wrapTC2Fun :: [a] -> [b] -> [c]
+    -- ^ Function expected to function in the same way as the Spec being
+    -- tested.
+
+  , wrapTC2CopInp1 :: (Type a, String, Gen a)
+    -- ^ Input specification for the first input.
+    --
+    -- - The first element contains the type of the input in Bluespec.
+    --
+    -- - The second contains the variable name in Bluespec.
+    --
+    -- - The latter contains a randomized generator for values of the given
+    -- type.
+
+  , wrapTC2CopInp2 :: (Type b, String, Gen b)
+    -- ^ Input specification for the second input.
+    --
+    -- - The first element contains the type of the input in Bluespec.
+    --
+    -- - The second contains the variable name in Bluespec.
+    --
+    -- - The latter contains a randomized generator for values of the given
+    -- type.
+
+  , wrapTC2CopOut :: Type c
+    -- ^ The type of the output in Bluespec.
+  }
+
+-- | Generate test cases for expressions that behave like unary functions.
+mkTestCase1 :: (Typed a, Typed b)
+            => Gen (Fun a b, [a] -> [b])
+            -> Gen a
+            -> Gen (TestCase1 a b)
+mkTestCase1 genO gen = do
+    (copilotF, semF) <- genO
+
+    let spec = alwaysTriggerArg1 (UExpr t2 appliedOp)
+        appliedOp = copilotF (ExternVar t1 varName Nothing)
+
+    return $
+      TestCase1
+        { wrapTC1Expr = spec
+        , wrapTC1Fun = semF
+        , wrapTC1CopInp = ( t1, varName, gen )
+        , wrapTC1CopOut = t2
+        }
+
+  where
+
+    t1 = typeOf
+    t2 = typeOf
+
+    varName = "input"
+
+-- | Generate test cases for expressions that behave like binary functions.
+mkTestCase2 :: (Typed a, Typed b, Typed c)
+            => Gen (Fun2 a b c, [a] -> [b] -> [c])
+            -> Gen a
+            -> Gen b
+            -> Gen (TestCase2 a b c)
+mkTestCase2 genO genA genB = do
+    (copilotF, semF) <- genO
+
+    let spec = alwaysTriggerArg1 (UExpr t3 appliedOp)
+        appliedOp = copilotF (ExternVar t1 varName1 Nothing)
+                             (ExternVar t2 varName2 Nothing)
+
+    return $
+      TestCase2
+        { wrapTC2Expr = spec
+        , wrapTC2Fun = semF
+        , wrapTC2CopInp1 = ( t1, varName1, genA )
+        , wrapTC2CopInp2 = ( t2, varName2, genB )
+        , wrapTC2CopOut = t3
+        }
+
+  where
+
+    t1 = typeOf
+    t2 = typeOf
+    t3 = typeOf
+
+    varName1 = "input1"
+    varName2 = "input2"
+
+-- | Test running a compiled Bluespec program and comparing the results.
+testRunCompare1 :: (Show a, Typed a, ReadableFromBluespec b, Eq b, Typed b)
+                => Gen (TestCase1 a b) -> Property
+testRunCompare1 ops =
+  forAllBlind ops $ \testCase ->
+    let (TestCase1
+           { wrapTC1Expr = copilotSpec
+           , wrapTC1Fun = haskellFun
+           , wrapTC1CopInp = inputVar
+           , wrapTC1CopOut = outputType
+           }) = testCase
+        (bluespecTypeInput, bluespecInputName, gen) = inputVar
+
+    in forAll (getPositive <$> arbitrary) $ \len ->
+
+         forAll (vectorOf len gen) $ \nums -> do
+
+         let inputs  = filterOutUnusedExts
+                         copilotSpec
+                         [ (typeBluespec bluespecTypeInput,
+                            fmap (bluespecShow bluespecTypeInput) nums,
+                            bluespecInputName)
+                         ]
+             outputs = haskellFun nums
+
+         testRunCompareArg
+           inputs len outputs copilotSpec (typeBluespec outputType)
+
+-- | Test running a compiled Bluespec program and comparing the results.
+testRunCompare2 :: (Show a1, Typed a1, Show a2, Typed a2,
+                    ReadableFromBluespec b, Eq b, Typed b)
+                => Gen (TestCase2 a1 a2 b) -> Property
+testRunCompare2 ops =
+  forAllBlind ops $ \testCase ->
+    let (TestCase2
+           { wrapTC2Expr = copilotSpec
+           , wrapTC2Fun = haskellFun
+           , wrapTC2CopInp1 = inputVar1
+           , wrapTC2CopInp2 = inputVar2
+           , wrapTC2CopOut = outputType
+           }) =
+          testCase
+
+        (bluespecTypeInput1, bluespecInputName1, gen1) = inputVar1
+        (bluespecTypeInput2, bluespecInputName2, gen2) = inputVar2
+
+    in forAll (getPositive <$> arbitrary) $ \len ->
+       forAll (vectorOf len gen1) $ \nums1 ->
+       forAll (vectorOf len gen2) $ \nums2 -> do
+         let inputs  = filterOutUnusedExts
+                         copilotSpec
+                         [ (typeBluespec bluespecTypeInput1,
+                            fmap (bluespecShow bluespecTypeInput1) nums1,
+                            bluespecInputName1)
+                         , (typeBluespec bluespecTypeInput2,
+                            fmap (bluespecShow bluespecTypeInput2) nums2,
+                            bluespecInputName2)
+                         ]
+             outputs = haskellFun nums1 nums2
+
+         testRunCompareArg
+           inputs len outputs copilotSpec (typeBluespec outputType)
+
+-- | Test running a compiled Bluespec program and comparing the results, when
+-- the program produces one output as an argument to a trigger that always
+-- fires.
+--
+-- PRE: all lists (second argument) of inputs have the length given as second
+-- argument.
+--
+-- PRE: the monitoring code this is linked against uses the function
+-- @printBack@ with exactly one argument to pass the results.
+testRunCompareArg :: (ReadableFromBluespec b, Eq b)
+                  => [(String, [String], String)]
+                  -> Int
+                  -> [b]
+                  -> Spec
+                  -> String
+                  -> Property
+testRunCompareArg inputs numInputs nums spec outputType =
+  ioProperty $ do
+    tmpDir <- getTemporaryDirectory
+    setCurrentDirectory tmpDir
+
+    -- Operate in temporary directory
+    testDir <- mkdtemp "CopilotTest"
+    setCurrentDirectory testDir
+
+    -- Produce wrapper program
+    let bluespecProgram =
+          testRunCompareArgBluespecProgram inputs outputType
+    writeFile "Top.bs" bluespecProgram
+
+    -- Produce copilot monitoring code
+    compile "CopilotTest" spec
+    r <- compileBluespec "Top" ["-g", "mkTop"]
+
+    -- Compile main program
+    r2 <- compileExecutable "mkTop"
+
+    -- Print result so far (for debugging purposes only)
+    {-
+    print r2
+    print testDir
+    -}
+
+    -- Run program and compare result
+    out <- readProcess "./mkTop" ["-m", show (numInputs + 2)] ""
+    let outNums = readFromBluespec <$> lines out
+        comparison = outNums == nums
+
+    -- Only clean up if the test succeeded; otherwise, we want to inspect it.
+    when comparison $ do
+      -- Remove temporary directory
+      setCurrentDirectory tmpDir
+      removeDirectoryRecursive testDir
+
+    return $ r && r2 && comparison
+
+-- | Return a wrapper Bluespec program that runs for a number of clock cycles,
+-- updating external stream registers on every cycle, running the monitors, and
+-- publishing the results of any outputs.
+testRunCompareArgBluespecProgram
+  :: [(String, [String], String)]
+  -> String
+  -> String
+testRunCompareArgBluespecProgram inputs outputType = unlines $
+    [ "package Top where"
+    , ""
+    , "import FloatingPoint"
+    , "import Vector"
+    , ""
+    , "import CopilotTest"
+    , "import CopilotTestIfc"
+    , "import CopilotTestTypes"
+    , ""
+    ]
+    ++ inputVecDecls ++
+    [ ""
+    , "copilotTestIfc :: Module CopilotTestIfc"
+    , "copilotTestIfc ="
+    , "  module"
+    ]
+    ++ inputRegs ++
+    [ "    i :: Reg (Bit 64) <- mkReg 0"
+    , "    ready :: Reg Bool <- mkReg False"
+    , "    interface"
+    , "      printBack :: " ++ outputType ++ " -> Action"
+    , "      printBack num = $display (fshow num)"
+    , "                      when ready"
+    , ""
+    ]
+    ++ inputMethods ++
+    [ ""
+    , "    rules"
+    , "      \"inputs\": when True ==> do"
+    ]
+    ++ inputUpdates ++
+    [ "        i := i + 1"
+    , "        ready := True"
+    , ""
+    , "mkTop :: Module Empty"
+    , "mkTop = mkCopilotTest copilotTestIfc"
+    ]
+  where
+    inputVecDecls :: [String]
+    inputVecDecls =
+      concatMap
+        (\(bluespecType, _varName, _regName, inputVecName, inputVals) ->
+          [ inputVecName ++ " :: Vector " ++ show (length inputVals) ++
+            " (" ++ bluespecType ++ ")"
+          , inputVecName ++ " = " ++ genVector inputVals
+          ])
+        vars
+
+    inputRegs :: [String]
+    inputRegs =
+      map
+        (\(bluespecType, _varName, regName, _inputVecName, _inputVals) ->
+          "    " ++ regName ++ " :: Reg (" ++ bluespecType ++ ") <- mkRegU")
+        vars
+
+    inputMethods :: [String]
+    inputMethods =
+      concatMap
+        (\(bluespecType, varName, regName, _inputVecName, _inputVals) ->
+          [ "      " ++ varName ++ " :: Reg (" ++ bluespecType ++ ")"
+          , "      " ++ varName ++ " = " ++ regName
+          ])
+        vars
+
+    inputUpdates :: [String]
+    inputUpdates =
+      map
+        (\(_bluespecType, _varName, regName, inputVecName, _inputVals) ->
+          "        " ++ regName ++ " := select " ++ inputVecName ++ " i")
+        vars
+
+    vars = map oneInput inputs
+    oneInput (bluespecTypeInput, inputVals, bluespecInputName) =
+        (bluespecTypeInput, inputVarName, inputRegVarName, inputVecVarName,
+         inputVals)
+      where
+        inputVarName    = bluespecInputName
+        inputRegVarName = bluespecInputName ++ "Impl"
+        inputVecVarName = bluespecInputName ++ "Inputs"
+
+-- * Auxiliary functions
+
+-- ** Specs handling
+
+-- | Build a 'Spec' that triggers at every step, passing the given expression
+-- as argument, and execution a function 'printBack'.
+alwaysTriggerArg1 :: UExpr -> Spec
+alwaysTriggerArg1 = triggerArg1 (Const Bool True)
+
+  where
+
+    -- | Build a 'Spec' that triggers based on a given boolean stream, passing
+    -- the given expression as argument, and execution a function 'printBack'.
+    triggerArg1 :: Expr Bool -> UExpr -> Spec
+    triggerArg1 guard expr = Spec streams observers triggers properties
+
+      where
+
+        streams    = []
+        observers  = []
+        properties = []
+
+        triggers = [ Trigger function guard args ]
+        function = "printBack"
+        args     = [ expr ]
+
+-- | Filter out any elements in the input list (of type @[(a, b, String)]@)
+-- whose first element (the name of an external stream) does not correspond to
+-- the name of an external stream in the supplied 'Spec'. For example, a Copilot
+-- source program may declare external streams, but if none of them are used in
+-- the 'Spec', then the 'Spec' value itself will not contain any external stream
+-- definitions. As a result, we want to ensure that the input list also does not
+-- contain any external streams.
+filterOutUnusedExts :: Spec -> [(a, b, String)] -> [(a, b, String)]
+filterOutUnusedExts spec = filter (\(_, _, name) -> name `elem` extNames)
+  where
+    extNames = map extName $ gatherExts (specStreams spec) (specTriggers spec)
+
+-- ** Compilation of Bluespec programs
+
+-- | Compile a Bluespec file given its basename.
+compileBluespec :: String -> [String] -> IO Bool
+compileBluespec baseName extraArgs = do
+  result <- catch (do callProcess "bsc" $ extraArgs ++
+                                          [ "-sim", "-quiet", "-u",
+                                            -- We suppress the G0023 warning,
+                                            -- which arises due to the `nop`
+                                            -- triggers defined above. See the
+                                            -- DESIGN.md document for more
+                                            -- details on what these warning
+                                            -- codes mean.
+                                            "-suppress-warnings", "G0023:S0080",
+                                            baseName ++ ".bs" ]
+                      return True
+                  )
+                  (\e -> do
+                     hPutStrLn stderr $
+                       "copilot-bluespec: error: compileBluespec: "
+                         ++ "cannot compile " ++ baseName ++ ".bs with bsc"
+                     hPutStrLn stderr $
+                       "copilot-bluespec: exception: " ++ show (e :: IOException)
+                     return False
+                  )
+  if result
+    then doesFileExist $ baseName ++ ".bo"
+    else return False
+
+-- | Compile a Bluespec file into an executable given its basename.
+compileExecutable :: String -> IO Bool
+compileExecutable topExe = do
+  result <- catch (do callProcess "bsc" $ [ "-sim", "-quiet" ]
+                                          ++ [ "-e", topExe ]
+                                          ++ [ "-o", topExe ]
+                      return True
+                  )
+                  (\e -> do
+                     hPutStrLn stderr $
+                       "copilot-bluespec: error: compileExecutable: "
+                         ++ "cannot compile " ++ topExe ++ " with bsc"
+                     hPutStrLn stderr $
+                       "copilot-bluespec: exception: "
+                         ++ show (e :: IOException)
+                     return False
+                  )
+  if result
+    then doesFileExist topExe
+    else return False
+
+-- ** Interfacing between Haskell and Bluespec
+
+-- | Bluespec type used to store values of a given type.
+typeBluespec :: Typed a => Type a -> String
+typeBluespec Bool         = "Bool"
+typeBluespec Int8         = "Int 8"
+typeBluespec Int16        = "Int 16"
+typeBluespec Int32        = "Int 32"
+typeBluespec Int64        = "Int 64"
+typeBluespec Word8        = "UInt 8"
+typeBluespec Word16       = "UInt 16"
+typeBluespec Word32       = "UInt 32"
+typeBluespec Word64       = "UInt 64"
+typeBluespec Float        = "Float"
+typeBluespec Double       = "Double"
+typeBluespec t@(Array tE) =
+  "Vector " ++ show (typeLength t)  ++ "(" ++ typeBluespec tE ++ ")"
+typeBluespec (Struct s)   = typeName s
+
+-- | Show a value of a given type in Bluespec.
+bluespecShow :: Type a -> a -> String
+bluespecShow Bool       x = show x
+bluespecShow Int8       x = bluespecShowIntegral x
+bluespecShow Int16      x = bluespecShowIntegral x
+bluespecShow Int32      x = bluespecShowIntegral x
+bluespecShow Int64      x = bluespecShowIntegral x
+bluespecShow Word8      x = bluespecShowIntegral x
+bluespecShow Word16     x = bluespecShowIntegral x
+bluespecShow Word32     x = bluespecShowIntegral x
+bluespecShow Word64     x = bluespecShowIntegral x
+bluespecShow Float      x = bluespecShowRealFrac x
+bluespecShow Double     x = bluespecShowRealFrac x
+bluespecShow (Array tE) x = genVector $ map (bluespecShow tE) $ arrayElems x
+bluespecShow (Struct s) x =
+  typeName s
+    ++ "{ "
+    ++ intercalate ";"
+         (map
+           (\(Value fldTy fld@(Field val)) ->
+             fieldName fld ++ " = " ++ bluespecShow fldTy val)
+           (toValues x))
+    ++ "}"
+
+-- | Show a value of a integral type (e.g., 'Int8' or 'Word8').
+bluespecShowIntegral :: (Integral a, Num a, Ord a, Show a) => a -> String
+bluespecShowIntegral x
+  | x >= 0    = show x
+  -- Bluespec Haskell doesn't have negative integer literals, so something like
+  -- "-42" won't parse. Instead, we must rely on Bluespec's `negate` function.
+  --
+  -- We must be careful to negate an Integer literal rather than than a
+  -- fixed-precision literal. For instance, suppose we wanted to display
+  -- (-128 :: Int8). We wouldn't want to do this by displaying `negate 128`,
+  -- since 128 isn't a valid Int8 value—the maximum Int8 value is 127!
+  -- Instead, we want to display `fromInteger (negate 128)`, where 128 is an
+  -- Integer. This way, `negate` can turn `128` to `-128` without issues.
+  | otherwise = "fromInteger (negate " ++ show (abs (toInteger x)) ++ ")"
+
+-- | Show a value of a fractional type (e.g., 'Float' or 'Double').
+bluespecShowRealFrac :: (Num a, Ord a, Show a) => a -> String
+bluespecShowRealFrac x
+  | x >= 0    = show x
+  | otherwise = "negate " ++ show x
+
+-- | Given a list of elements as arguments, show a @Vector@ expression. For
+-- example, @'genVector' [\"27\", \"42\"]@ will return
+-- @\"updateVector (updateVector newVector 0 27) 1 42)\"@.
+genVector :: [String] -> String
+genVector vals =
+  snd $
+  foldl'
+    (\(!i, !v) x ->
+      (i+1, "update (" ++ v ++ ") " ++ show i ++ " (" ++ x ++ ")"))
+    (0 :: Int, "newVector")
+    vals
+
+-- | Read a value of a given type in Bluespec.
+class ReadableFromBluespec a where
+  readFromBluespec :: String -> a
+
+instance ReadableFromBluespec Bool where
+  readFromBluespec = read
+
+instance ReadableFromBluespec Int8 where
+  readFromBluespec = read
+
+instance ReadableFromBluespec Int16 where
+  readFromBluespec = read
+
+instance ReadableFromBluespec Int32 where
+  readFromBluespec = read
+
+instance ReadableFromBluespec Int64 where
+  readFromBluespec = read
+
+instance ReadableFromBluespec Word8 where
+  readFromBluespec = read
+
+instance ReadableFromBluespec Word16 where
+  readFromBluespec = read
+
+instance ReadableFromBluespec Word32 where
+  readFromBluespec = read
+
+instance ReadableFromBluespec Word64 where
+  readFromBluespec = read
+
+-- ** A simple struct definition for unit testing purposes
+
+data MyStruct = MyStruct
+  { myStruct1 :: Field "myStruct1" Int8
+  , myStruct2 :: Field "myStruct2" Int8
+  }
+
+instance Struct MyStruct where
+  typeName _ = "MyStruct"
+  toValues ms = [ Value Int8 (myStruct1 ms)
+                , Value Int8 (myStruct2 ms)
+                ]
+
+instance Typed MyStruct where
+  typeOf = Struct (MyStruct (Field 0) (Field 0))
+
+-- | Unwrap a 'Field' to obtain the underlying value.
+unField :: Field s t -> t
+unField (Field val) = val