diff --git a/aig.cabal b/aig.cabal
--- a/aig.cabal
+++ b/aig.cabal
@@ -1,10 +1,10 @@
 Name:               aig
-Version:            0.2.4
+Version:            0.2.5
 License:            BSD3
 License-file:       LICENSE
 Author:             Galois Inc.
 Maintainer:         jhendrix@galois.com
-Copyright:          (c) 2014-2015 Galois Inc.
+Copyright:          (c) 2014-2017 Galois Inc.
 Category:           Data
 build-type:         Simple
 cabal-Version:      >= 1.10
@@ -38,4 +38,23 @@
     base-compat >= 0.6.0,
     mtl,
     vector,
+    QuickCheck >= 2.7
+
+test-suite aig-test
+  type: exitcode-stdio-1.0
+  hs-source-dirs: tests
+
+  ghc-options: -Wall
+  default-language: Haskell2010
+
+  main-is: aig-test.hs
+  other-modules:
+    Tests.Operations
+
+  build-depends:
+    base == 4.*,
+    aig,
+    tasty,
+    tasty-ant-xml,
+    tasty-quickcheck >= 0.8.1,
     QuickCheck >= 2.7
diff --git a/src/Data/AIG/Interface.hs b/src/Data/AIG/Interface.hs
--- a/src/Data/AIG/Interface.hs
+++ b/src/Data/AIG/Interface.hs
@@ -1,6 +1,6 @@
 {- |
 Module      : Data.AIG.Interface
-Copyright   : (c) Galois, Inc. 2014
+Copyright   : (c) Galois, Inc. 2014-2017
 License     : BSD3
 Maintainer  : jhendrix@galois.com
 Stability   : experimental
@@ -28,6 +28,7 @@
   , networkOutputCount
   -- * Literal representations
   , LitView(..)
+  , negateLitView
   , LitTree(..)
   , toLitTree
   , fromLitTree
@@ -50,11 +51,16 @@
   , getMaxInput
   , buildNetwork
   , randomNetwork
+  , BasicGraph
+  , BasicLit
+  , basicProxy
+  , newBasicGraph
   ) where
 
+import qualified Prelude as Prelude
 import Control.Applicative
 import Control.Monad
-import Prelude()
+import Data.IORef
 import Prelude.Compat hiding (not, and, or, mapM)
 import Test.QuickCheck (Gen, Arbitrary(..), generate, oneof, sized, choose)
 
@@ -69,6 +75,16 @@
   | FalseLit
  deriving (Eq,Show,Ord,Functor,Foldable,Traversable)
 
+negateLitView :: LitView a -> LitView a
+negateLitView l = case l of
+     TrueLit    -> FalseLit
+     FalseLit   -> TrueLit
+     Input i    -> NotInput i
+     NotInput i -> Input i
+     And x y    -> NotAnd x y
+     NotAnd x y -> And x y
+
+
 newtype LitTree = LitTree { unLitTree :: LitView LitTree }
  deriving (Eq,Show,Ord)
 
@@ -391,3 +407,105 @@
 --   and using that to construct a network.
 randomNetwork :: IsAIG l g => Proxy l g -> IO (Network l g)
 randomNetwork proxy = generate arbitrary >>= buildNetwork proxy
+
+------------------------------------------------------------------
+-- | A basic "Graph" datastructure based on LitTrees.  This is a totally
+--   naive implementation of the AIG structure that exists
+--   exclusively for testing purposes.
+newtype BasicGraph s = BasicGraph (IORef Int)
+
+------------------------------------------------------------------
+-- | A basic AIG literal datastructure based on LitTrees.
+--   This is a totally
+--   naive implementation of the AIG structure that exists
+--   exclusively for testing purposes.
+newtype BasicLit s = BasicLit LitTree
+ deriving (Show)
+
+basicProxy :: Proxy BasicLit BasicGraph
+basicProxy = Proxy (\x -> x)
+
+notTree :: LitTree -> LitTree
+notTree (LitTree x) = LitTree . negateLitView $ x
+
+andTree :: LitTree -> LitTree -> LitTree
+andTree (LitTree FalseLit) _    = LitTree FalseLit
+andTree _ (LitTree FalseLit)    = LitTree FalseLit
+andTree (LitTree TrueLit) y     = y
+andTree x (LitTree TrueLit)     = x
+andTree x y                     = LitTree (And x y)
+
+newBasicGraph :: IO (BasicGraph s)
+newBasicGraph =
+  do r <- newIORef 0
+     return (BasicGraph r)
+
+instance IsLit BasicLit where
+  not (BasicLit x) = BasicLit . notTree $ x
+  (BasicLit x) === (BasicLit y) = x == y
+
+instance IsAIG BasicLit BasicGraph where
+  withNewGraph _proxy k = k =<< newBasicGraph
+
+  aigerNetwork _proxy _fp =
+    fail "Cannot read AIGER files from the BasicGraph implementation"
+
+  trueLit  _g = BasicLit . LitTree $ TrueLit
+  falseLit _g = BasicLit . LitTree $ FalseLit
+
+  newInput (BasicGraph r) =
+     atomicModifyIORef' r (\n -> (n+1, BasicLit . LitTree . Input $ n))
+
+  and _g (BasicLit x) (BasicLit  y) = return . BasicLit $ andTree x y
+
+  inputCount (BasicGraph r) = readIORef r
+
+  -- | Get input at given index in the graph.
+  getInput _g i = return . BasicLit . LitTree . Input $ i
+
+  writeAiger _fp _ntk =
+     fail "Cannot write AIGER files from the BasicGraph implementation"
+
+  writeCNF _g _l _fp =
+     fail "Cannot write CNF files from the BasicGraph implementation"
+
+  checkSat _g _l =
+     fail "Cannot SAT check graphs in the BasicGraph implementation"
+
+  cec _g1 _g2 =
+     fail "Cannot CEC graphs in the BasicGraph implementation"
+
+  asConstant _g (BasicLit bl) = go bl
+    where
+     go (LitTree l) = go' l
+
+     go' l = case l of
+         TrueLit    -> pure True
+         FalseLit   -> pure False
+         And x y    -> (&&) <$> go x <*> go y
+         NotAnd x y -> Prelude.not <$> go' (And x y)
+         Input _    -> Nothing
+         NotInput _ -> Nothing
+
+  -- | Evaluate the network on a set of concrete inputs.
+  evaluator _g xs = return (\(BasicLit x) -> eval x)
+    where
+     eval :: LitTree -> Bool
+     eval (LitTree x) = eval' x
+
+     eval' :: LitView LitTree -> Bool
+     eval' TrueLit      = True
+     eval' FalseLit     = False
+     eval' (And x y)    = eval x && eval y
+     eval' (NotAnd x y) = Prelude.not (eval' (And x y))
+     eval' (Input i)    = case drop i xs of
+                            (b:_) -> b
+                            []    -> error $ unwords ["Input value out of bounds", show i]
+     eval' (NotInput i) = Prelude.not (eval' (Input i))
+
+  -- | Examine the outermost structure of a literal to see how it was constructed
+  litView _ (BasicLit (LitTree x)) = return (fmap BasicLit x)
+
+  -- | Build an evaluation function over an AIG using the provided view function
+  abstractEvaluateAIG _g f = return (\(BasicLit x) -> h x)
+   where h (LitTree x) = f =<< traverse h x
diff --git a/src/Data/AIG/Operations.hs b/src/Data/AIG/Operations.hs
--- a/src/Data/AIG/Operations.hs
+++ b/src/Data/AIG/Operations.hs
@@ -877,9 +877,12 @@
     -> BV (l s)    -- ^ the value to rotate
     -> BV (l s)    -- ^ how many places to rotate
     -> IO (BV (l s))
-rol g x y = do
-  r <- urem g y (bvFromInteger g (length y) (toInteger (length x)))
-  muxInteger (iteM g) (length x - 1) r (return . rolC x)
+rol g x0 (BV ys) = fst <$> V.foldM f (x0, 1) (V.reverse ys)
+  where
+    f (x, p) y = do
+      x' <- ite g y (rolC x p) x
+      let p' = (2*p) `mod` length x0
+      return (x', p')
 
 -- | Rotate right.
 ror :: IsAIG l g
@@ -887,9 +890,12 @@
     -> BV (l s)    -- ^ the value to rotate
     -> BV (l s)    -- ^ how many places to rotate
     -> IO (BV (l s))
-ror g x y = do
-  r <- urem g y (bvFromInteger g (length y) (toInteger (length x)))
-  muxInteger (iteM g) (length x - 1) r (return . rorC x)
+ror g x0 (BV ys) = fst <$> V.foldM f (x0, 1) (V.reverse ys)
+  where
+    f (x, p) y = do
+      x' <- ite g y (rorC x p) x
+      let p' = (2*p) `mod` length x0
+      return (x', p')
 
 
 -- | Compute the rounded-down base2 logarithm of the input bitvector.
diff --git a/tests/Tests/Operations.hs b/tests/Tests/Operations.hs
new file mode 100644
--- /dev/null
+++ b/tests/Tests/Operations.hs
@@ -0,0 +1,271 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}
+module Tests.Operations (op_tests) where
+
+import Test.Tasty
+import Test.Tasty.QuickCheck
+--import Test.QuickCheck
+
+import           Data.AIG.Interface (BasicGraph, BasicLit, newBasicGraph)
+import qualified Data.AIG.Interface as AIG
+import qualified Data.AIG.Operations as AIG
+import Data.Bits
+import Data.Int
+import Data.Word
+
+type BV s = AIG.BV (BasicLit s)
+
+--------------------------------------------------------------------------
+-- Some test harness stuff to make writing down unit tests easier
+
+class Precond x where
+  precond :: x -> Bool
+  precond _ = True
+
+class Arbitrary x => AIGTestableValue g x y where
+  injectArg  :: g -> x -> y
+  extractArg :: g -> y -> Maybe x
+
+class PushIO y where
+  pushIO  :: (a -> y) -> IO a -> y
+
+instance PushIO (IO b) where
+  pushIO f x = x >>= f
+
+instance PushIO b => PushIO (a -> b) where
+  pushIO f x a = pushIO (\x' -> f x' a) x
+
+class (Testable p, PushIO y) => AIGTestable g x y p | g x y -> p where
+  runTest :: IO g -> x -> y -> Bool -> p
+
+newtype Denom a = Denom a
+ deriving (Eq, Ord, Show)
+
+instance Precond Bool
+instance Precond Word32
+instance Precond Word64
+instance Precond Int32
+instance Precond Int64
+instance Precond Integer
+
+instance (Integral a, Eq a) => Precond (Denom a) where
+  precond (Denom x) = x /= 0
+instance Precond Int where
+  precond x = 0 <= x && x < 64
+
+instance Arbitrary a => Arbitrary (Denom a) where
+  arbitrary = Denom <$> arbitrary
+
+instance (AIGTestableValue g a x, AIGTestableValue g b y) =>
+    AIGTestableValue g (a,b) (x,y) where
+  injectArg g (a,b) = (injectArg g a, injectArg g b)
+  extractArg g (x,y) = (,) <$> extractArg g x <*> extractArg g y
+
+instance AIGTestableValue g a b => AIGTestableValue g (Denom a) b where
+  injectArg g (Denom x) = injectArg g x
+  extractArg g x = Denom <$> extractArg g x
+
+instance AIGTestableValue (BasicGraph s) Int (BV s) where
+  injectArg g x  = AIG.bvFromInteger g (finiteBitSize x) (toInteger x)
+  extractArg g x = fromInteger <$> AIG.asSigned g x
+
+instance AIGTestableValue (BasicGraph s) Word32 (BV s) where
+  injectArg g x  = AIG.bvFromInteger g (finiteBitSize x) (toInteger x)
+  extractArg g x = fromInteger <$> AIG.asUnsigned g x
+
+instance AIGTestableValue (BasicGraph s) Word64 (BV s) where
+  injectArg g x  = AIG.bvFromInteger g (finiteBitSize x) (toInteger x)
+  extractArg g x = fromInteger <$> AIG.asUnsigned g x
+
+instance AIGTestableValue (BasicGraph s) Int32 (BV s) where
+  injectArg g x  = AIG.bvFromInteger g (finiteBitSize x) (toInteger x)
+  extractArg g x = fromInteger <$> AIG.asSigned g x
+
+instance AIGTestableValue (BasicGraph s) Int64 (BV s) where
+  injectArg g x  = AIG.bvFromInteger g (finiteBitSize x) (toInteger x)
+  extractArg g x = fromInteger <$> AIG.asSigned g x
+
+instance AIGTestableValue (BasicGraph s) Integer Integer where
+  injectArg _g x = x
+  extractArg _g x = Just x
+
+instance AIGTestableValue (BasicGraph s) Bool (BasicLit s) where
+  injectArg g x  = AIG.constant g x
+  extractArg g x = AIG.asConstant g x
+
+instance (Eq x, Show x, AIGTestableValue g x y) => AIGTestable g x (IO y) Property
+ where
+   runTest gph x y pre = pre ==> ioProperty $
+     do gph' <- gph
+        y' <- y
+        case extractArg gph' y' of
+          Nothing -> fail $ unwords ["Expected concrete output"]
+          Just z
+            | x == z    -> return True
+            | otherwise -> fail $ unwords ["Expected", show x, "but got", show z]
+
+instance
+   (Precond x, Show x, AIGTestableValue g x y, AIGTestable g a b p) =>
+   AIGTestable g (x -> a) (y -> b) (x -> p)
+ where
+   runTest gph f g pre = \x ->
+     let y = (gph >>= \gph' -> return $ injectArg gph' x)
+      in runTest gph (f x) (pushIO g y) (precond x && pre)
+
+
+------------------------------------------------------------------------------------
+-- Make a unit test from a concrete operation and an operation on AIGs
+
+mkTest :: forall a b p
+        . (Testable p, AIGTestable (BasicGraph ()) a b p)
+       => String
+       -> a
+       -> (BasicGraph () -> b)
+       -> TestTree
+mkTest nm a b =
+  withResource newBasicGraph (\_ -> return ()) $ \(g :: IO (BasicGraph ())) ->
+    testProperty nm $ (runTest g a (pushIO b g) True :: p)
+
+
+op_tests :: [TestTree]
+op_tests =
+  [ mkTest "ite"  (\b (x :: Word64) y -> if b then x else y) AIG.ite
+
+  , mkTest "neg"  (negate :: Int64 -> Int64) AIG.neg
+  , mkTest "add"  ((+)  :: Word64 -> Word64 -> Word64) AIG.add
+  , mkTest "addC" addC AIG.addC
+  , mkTest "sub"  ((-)  :: Word64 -> Word64 -> Word64) AIG.sub
+  , mkTest "subC" subC AIG.subC
+  , mkTest "addConst" addConst AIG.addConst
+  , mkTest "subConst" subConst AIG.subConst
+
+  , mkTest "mul"  ((*)  :: Word64 -> Word64 -> Word64) AIG.mul
+  , mkTest "mulFull"  mulFull  AIG.mulFull
+  , mkTest "smulFull" smulFull AIG.smulFull
+  , mkTest "squot" squot AIG.squot
+  , mkTest "srem"  srem  AIG.srem
+  , mkTest "uquot" uquot AIG.uquot
+  , mkTest "urem"  urem  AIG.urem
+
+  , mkTest "shl"  (shiftL  :: Word64 -> Int -> Word64) AIG.shl
+  , mkTest "ushr" (shiftR  :: Word64 -> Int -> Word64) AIG.ushr
+  , mkTest "sshr" (shiftR  :: Int64  -> Int -> Int64)  AIG.sshr
+  , mkTest "rol"  (rotateL :: Word64 -> Int -> Word64) AIG.rol
+  , mkTest "ror"  (rotateR :: Word64 -> Int -> Word64) AIG.ror
+
+  , mkTest "bvEq"    ((==) :: Word64 -> Word64 -> Bool) AIG.bvEq
+  , mkTest "isZero"  (\x -> (x :: Word64) == 0) AIG.isZero
+  , mkTest "nonZero" (\x -> (x :: Word64) /= 0) AIG.nonZero
+  , mkTest "sle"  ((<=) :: Int64 -> Int64 -> Bool) AIG.sle
+  , mkTest "slt"  ((<)  :: Int64 -> Int64 -> Bool) AIG.slt
+  , mkTest "ule"  ((<=) :: Word64 -> Word64 -> Bool) AIG.ule
+  , mkTest "ult"  ((<)  :: Word64 -> Word64 -> Bool) AIG.ult
+  , mkTest "sabs" (abs  :: Int64 -> Int64) AIG.sabs
+
+  , mkTest "sext" sext (\g x -> (return $ AIG.sext g x 64) :: IO _)
+  , mkTest "zext" zext (\g x -> (return $ AIG.zext g x 64) :: IO _)
+  , mkTest "trunc" trunc (\(_ :: BasicGraph ()) (x :: BV ()) -> (return $ AIG.trunc 64 x) :: IO _)
+
+  , mkTest "priorityEncode" priorityEncode (\g -> AIG.priorityEncode g 32)
+  , mkTest "logBase2_down" log2down AIG.logBase2_down
+  , mkTest "logBase2_up"   log2up   AIG.logBase2_up
+  , mkTest "clz"  clz AIG.countLeadingZeros
+  , mkTest "ctz"  ctz AIG.countTrailingZeros
+
+  , mkTest "pmul" pmul AIG.pmul
+  , mkTest "pdiv" pdiv AIG.pdiv
+  , mkTest "pmod" pmod AIG.pmod
+  ]
+
+addC :: Word32 -> Word32 -> (Word32, Bool)
+addC x y = ( fromIntegral z, testBit z 32 )
+ where z :: Word64
+       z = fromIntegral x + fromIntegral y
+
+subC :: Word32 -> Word32 -> (Word32, Bool)
+subC x y = ( fromIntegral z, testBit z 32 )
+ where z :: Word64
+       z = fromIntegral x - fromIntegral y
+
+addConst :: Word64 -> Integer -> Word64
+addConst x y = x + fromInteger y
+
+subConst :: Word64 -> Integer -> Word64
+subConst x y = x - fromInteger y
+
+mulFull :: Word32 -> Word32 -> Word64
+mulFull x y = fromIntegral x * fromIntegral y
+
+smulFull :: Int32 -> Int32 -> Int64
+smulFull x y = fromIntegral x * fromIntegral y
+
+uquot :: Word64 -> Denom Word64 -> Word64
+uquot x (Denom y) = quot x y
+
+urem :: Word64 -> Denom Word64 -> Word64
+urem x (Denom y) = rem x y
+
+squot :: Int64 -> Denom Int64 -> Int64
+squot x (Denom y) = quot x y
+
+srem :: Int64 -> Denom Int64 -> Int64
+srem x (Denom y) = rem x y
+
+sext :: Int32 -> Int64
+sext = fromIntegral
+
+zext :: Word32 -> Word64
+zext = fromIntegral
+
+trunc :: Word64 -> Word32
+trunc = fromIntegral
+
+log2down :: Word64 -> Int64
+log2down x = fromIntegral (finiteBitSize x) - 1 - fromIntegral (countLeadingZeros x)
+
+log2up :: Word64 -> Int64
+log2up x = log2down (x - 1) + 1
+
+clz :: Word64 -> Word64
+clz = fromIntegral . countLeadingZeros
+
+ctz :: Word64 -> Word64
+ctz = fromIntegral . countTrailingZeros
+
+pmul :: Word32 -> Word32 -> Word64
+pmul x y = foldr xor zeroBits pprods
+ where
+  pprods = [ if testBit y i
+                then shiftL (fromIntegral x) i
+                else 0
+           | i <- [0 .. finiteBitSize y - 1]
+           ]
+
+priorityEncode :: Word64 -> (Bool, Word32)
+priorityEncode x
+  | x == 0    = (False, 0)
+  | otherwise = (True, fromIntegral (finiteBitSize x) - 1 - fromIntegral (countLeadingZeros x))
+
+pdiv :: Word64 -> Denom Word32 -> Word64
+pdiv x (Denom y) = fst $ pdivmod x y
+
+pmod :: Word64 -> Denom Word32 -> Word32
+pmod x (Denom y) = snd $ pdivmod x y
+
+pdivmod :: Word64 -> Word32 -> (Word64, Word32)
+pdivmod x y = go 0 x (finiteBitSize x - 1) start
+  where
+   start = finiteBitSize x - finiteBitSize y + countLeadingZeros y
+   y'    = fromIntegral y
+
+   go q r i j
+     | j <  0      = (q,fromIntegral r)
+     | testBit r i = go (setBit q j) (r `xor` (y' `shiftL` j)) (i-1) (j-1)
+     | otherwise   = go q            r                         (i-1) (j-1)
diff --git a/tests/aig-test.hs b/tests/aig-test.hs
new file mode 100644
--- /dev/null
+++ b/tests/aig-test.hs
@@ -0,0 +1,29 @@
+module Main (main) where
+
+import Test.Tasty
+import Test.Tasty.Ingredients
+import Test.Tasty.Runners.AntXML
+
+import Tests.Operations
+
+------------------------------------------------------------------------
+-- Runner
+------------------------------------------------------------------------
+
+main :: IO ()
+main = do
+  defaultMainWithIngredients ingrs tests
+
+ingrs :: [Ingredient]
+ingrs =
+   [ antXMLRunner
+   ]
+   ++
+   defaultIngredients
+
+
+tests :: TestTree
+tests =
+    testGroup "AIG"
+    [ testGroup "Bitvector operations" $ op_tests
+    ]