Copyright	(c) Galois, Inc. 2014
License	BSD3
Maintainer	jhendrix@galois.com
Stability	experimental
Portability	portable
Safe Haskell	None
Language	Haskell2010

Data.AIG.Operations

Contents

Bitvectors
Numeric operations on bitvectors
Polynomial multiplication and modulus

Description

A collection of higher-level operations (mostly 2's complement arithmetic operations) that can be built from the primitive And-Inverter Graph interface.

Synopsis

Bitvectors

data BV l Source

A BitVector consists of a sequence of symbolic bits and can be used for symbolic machine-word arithmetic.

Instances

Functor BV
Eq l => Eq (BV l)
Ord l => Ord (BV l)
Show l => Show (BV l)

empty :: BV l Source

Empty bitvector

length :: BV l -> Int Source

Number of bits in a bit vector

at :: BV l -> Int -> l Source

Project the individual bits of a BitVector. x at 0 is the most significant bit. It is an error to request an out-of-bounds bit.

(!) :: BV l -> Int -> l Source

Select bits from a bitvector, starting from the least significant bit. x ! 0 is the least significant bit. It is an error to request an out-of-bounds bit.

(++) :: BV l -> BV l -> BV l Source

Append two bitvectors, with the most significant bitvector given first.

concat :: [BV l] -> BV l Source

Concatenate a list of bitvectors, with the most significant bitvector at the head of the list.

take :: Int -> BV l -> BV l Source

Project out the n most significant bits from a bitvector.

drop :: Int -> BV l -> BV l Source

Drop the n most significant bits from a bitvector.

slice Source

Arguments

:: BV l
-> Int	`i`, 0-based start index
-> Int	`n`, bits to take
-> BV l	a vector consisting of the bits from `i` to `i+n-1`

Extract n bits starting at index i. The vector must contain at least i+n elements

sliceRev Source

Arguments

:: BV l
-> Int	`i`, 0-based start index from the end of the vector
-> Int	`n`, bits to take
-> BV l

Extract n bits starting at index i, counting from the end of the vector instead of the beginning. The vector must contain at least i+n elements.

mapM :: Monad m => (a -> m b) -> BV a -> m (BV b) Source

Apply a monadic operation to each element of a bitvector in sequence

zipWith :: (l -> l -> l) -> BV l -> BV l -> BV l Source

Combine two bitvectors with a bitwise function

zipWithM :: Monad m => (l -> l -> m l) -> BV l -> BV l -> m (BV l) Source

Combine two bitvectors with a bitwise monadic combiner action.

msb :: BV l -> l Source

Retrieve the most significant bit of a bitvector.

lsb :: BV l -> l Source

Retrieve the least significant bit of a bitvector.

bvSame :: IsLit l => BV (l s) -> BV (l s) -> Bool Source

Test syntactic equalify of two bitvectors using the === operation

bvShow :: IsAIG l g => g s -> BV (l s) -> String Source

Display a bitvector as a string of bits with most significant bits first. Concrete literals are displayed as '0' or '1', whereas symbolic literals are displayed as x.

Building bitvectors

generateM_msb0 Source

Arguments

:: Monad m
=> Int	`n`, length of the generated bitvector
-> (Int -> m l)	`f`, computation to generate a bit literal
-> m (BV l)

Generate a bitvector of length n, using monadic function f to generate the bit literals. The indexes to f are given in MSB-first order, i.e., f 0 is the most significant bit.

generate_msb0 Source

Arguments

:: Int	`n`, length of the generated bitvector
-> (Int -> l)	`f`, function to calculate bit literals
-> BV l

Generate a bitvector of length n, using function f to specify the bit literals. The indexes to f are given in MSB-first order, i.e., f 0 is the most significant bit.

generateM_lsb0 Source

Arguments

:: MonadIO m
=> Int	`n`, length of the generated bitvector
-> (Int -> m l)	`f`, computation to generate a bit literal
-> m (BV l)

Generate a bitvector of length n, using monadic function f to generate the bit literals. The indexes to f are given in LSB-first order, i.e., f 0 is the least significant bit.

generate_lsb0 Source

Arguments

:: Int	`n`, length of the generated bitvector
-> (Int -> l)	`f`, function to calculate bit literals
-> BV l

Generate a bitvector of length n, using function f to specify the bit literals. The indexes to f are given in LSB-first order, i.e., f 0 is the least significant bit.

replicate Source

Arguments

:: Int	`n`, length of the bitvector
-> l	`l`, the value to replicate
-> BV l

Generate a bit vector of length n where every bit value is literal l.

replicateM Source

Arguments

:: Monad m
=> Int	`n`, length of the bitvector
-> m l	`m`, the computation to produce a literal
-> m (BV l)

Generate a bit vector of length n where every bit value is generated in turn by m.

bvFromInteger Source

Arguments

:: IsAIG l g
=> g s
-> Int	number of bits in the resulting bitvector
-> Integer	integer value
-> BV (l s)

Generate a bitvector from an integer value, using 2's complement representation.

bvFromList :: [l] -> BV l Source

Convert a list to a bitvector, assuming big-endian bit order.

muxInteger Source

Arguments

:: (Integral i, Monad m)
=> (l -> m a -> m a -> m a)
-> i	Maximum value input vector is allowed to take.
-> BV l	Input vector
-> (i -> m a)
-> m a

muxInteger mergeFn maxValue lv valueFn returns a circuit whose result is valueFn v when lv has value v.

singleton :: l -> BV l Source

Generate a one-element bitvector containing the given literal

Lazy operators

lAnd :: IsAIG l g => g s -> IO (l s) -> IO (l s) -> IO (l s) Source

Build a short-cut AND circuit. If the left argument evaluates to the constant false, the right argument will not be evaluated.

lAnd' :: IsAIG l g => g s -> l s -> l s -> IO (l s) Source

lOr :: IsAIG l g => g s -> IO (l s) -> IO (l s) -> IO (l s) Source

Build a short-cut OR circuit. If the left argument evaluates to the constant true, the right argument will not be evaluated.

lOr' :: IsAIG l g => g s -> l s -> l s -> IO (l s) Source

lXor :: IsAIG l g => g s -> IO (l s) -> IO (l s) -> IO (l s) Source

Construct a lazy xor. If both arguments are constants, the output will also be a constant.

lXor' :: IsAIG l g => g s -> l s -> l s -> IO (l s) Source

lEq :: IsAIG l g => g s -> IO (l s) -> IO (l s) -> IO (l s) Source

Construct a lazy equality test. If both arguments are constants, the output will also be a constant.

lEq' :: IsAIG l g => g s -> l s -> l s -> IO (l s) Source

lNot :: IsAIG l g => g s -> IO (l s) -> IO (l s) Source

Lazy negation of a circuit.

lNot' :: IsAIG l g => g s -> l s -> l s Source

Conditionals

ite Source

Arguments

:: IsAIG l g
=> g s
-> l s	test bit
-> BV (l s)	then bitvector
-> BV (l s)	else bitvector
-> IO (BV (l s))

If-then-else combinator for bitvectors.

iteM Source

Arguments

:: IsAIG l g
=> g s
-> l s	test bit
-> IO (BV (l s))	then circuit computation
-> IO (BV (l s))	else circuit computation
-> IO (BV (l s))

If-then-else combinator for bitvector computations with optimistic shortcutting. If the test bit is concrete, we can avoid generating either the if or the else circuit.

Deconstructing bitvectors

asUnsigned :: IsAIG l g => g s -> BV (l s) -> Maybe Integer Source

Interpret a bitvector as an unsigned integer. Return Nothing if the bitvector is not concrete.

asSigned :: IsAIG l g => g s -> BV (l s) -> Maybe Integer Source

Interpret a bitvector as a signed integer. Return Nothing if the bitvector is not concrete.

bvToList :: BV l -> [l] Source

Convert a bitvector to a list, most significant bit first.

Numeric operations on bitvectors

Addition and subtraction

neg :: IsAIG l g => g s -> BV (l s) -> IO (BV (l s)) Source

Compute the 2's complement negation of a bitvector

add :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s)) Source

Add two bitvectors with the same size. Discard carry bit.

addC :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s), l s) Source

Add two bitvectors with the same size with carry.

sub :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s)) Source

Subtract one bitvector from another with the same size. Discard carry bit.

subC :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s), l s) Source

Subtract one bitvector from another with the same size with carry.

addConst :: IsAIG l g => g s -> BV (l s) -> Integer -> IO (BV (l s)) Source

Add a constant value to a bitvector

subConst :: IsAIG l g => g s -> BV (l s) -> Integer -> IO (BV (l s)) Source

Add a constant value to a bitvector

Multiplication and division

mul :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s)) Source

Multiply two bitvectors with the same size, with result of the same size as the arguments. Overflow is silently discarded.

mulFull :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s)) Source

Unsigned multiply two bitvectors with size m and size n, resulting in a vector of size m+n.

smulFull :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s)) Source

Signed multiply two bitvectors with size m and size n, resulting in a vector of size m+n.

squot :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s)) Source

Compute the signed quotient of two signed bitvectors with the same size.

srem :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s)) Source

Compute the signed division remainder of two signed bitvectors with the same size.

uquot :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s)) Source

Compute the unsigned quotient of two unsigned bitvectors with the same size.

urem :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s)) Source

Compute the unsigned division remainder of two unsigned bitvectors with the same size.

Shifts and rolls

shl Source

Arguments

:: IsAIG l g
=> g s
-> BV (l s)	the value to shift
-> BV (l s)	how many places to shift
-> IO (BV (l s))

Shift left. The least significant bit becomes 0.

sshr Source

Arguments

:: IsAIG l g
=> g s
-> BV (l s)	the value to shift
-> BV (l s)	how many places to shift
-> IO (BV (l s))

Signed right shift. The most significant bit is copied.

ushr Source

Arguments

:: IsAIG l g
=> g s
-> BV (l s)	the value to shift
-> BV (l s)	how many places to shift
-> IO (BV (l s))

Unsigned right shift. The most significant bit becomes 0.

rol Source

Arguments

:: IsAIG l g
=> g s
-> BV (l s)	the value to rotate
-> BV (l s)	how many places to rotate
-> IO (BV (l s))

Rotate left.

ror Source

Arguments

:: IsAIG l g
=> g s
-> BV (l s)	the value to rotate
-> BV (l s)	how many places to rotate
-> IO (BV (l s))

Rotate right.

Numeric comparisons

bvEq :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s) Source

Test equality of two bitvectors with the same size.

isZero :: IsAIG l g => g s -> BV (l s) -> IO (l s) Source

Test if a bitvector is equal to zero

nonZero :: IsAIG l g => g s -> BV (l s) -> IO (l s) Source

Test if a bitvector is distinct from zero

sle :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s) Source

Signed less-than-or-equal on bitvector with the same size.

slt :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s) Source

Signed less-than on bitvector with the same size.

ule :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s) Source

Unsigned less-than-or-equal on bitvector with the same size.

ult :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (l s) Source

Unsigned less-than on bitvector with the same size.

sabs :: IsAIG l g => g s -> BV (l s) -> IO (BV (l s)) Source

Return absolute value of signed bitvector.

Extensions

sext :: IsAIG l g => g s -> BV (l s) -> Int -> BV (l s) Source

sext v n sign extends v to be a vector with length n. This function requires that n >= length v and length v > 0.

zext :: IsAIG l g => g s -> BV (l s) -> Int -> BV (l s) Source

zext g v n zero extends v to be a vector with length n. This function requires that n >= length v.

trunc :: Int -> BV (l s) -> BV (l s) Source

Truncate the given bit vector to the specified length

zeroIntCoerce :: IsAIG l g => g s -> Int -> BV (l s) -> BV (l s) Source

Truncate or zero-extend a bitvector to have the specified number of bits

signIntCoerce :: IsAIG l g => g s -> Int -> BV (l s) -> BV (l s) Source

Truncate or sign-extend a bitvector to have the specified number of bits

Polynomial multiplication and modulus

pmul :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s)) Source

Polynomial multiplication. Note that the algorithm works the same no matter which endianness convention is used. Result length is max 0 (m+n-1), where m and n are the lengths of the inputs.

pmod :: forall l g s. IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s)) Source

Polynomial mod with symbolic modulus. Return value has length one less than the length of the modulus.