Data.AIG.Operations

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

Bitvectors

data BV l

A BitVector consists of a sequence of symbolic bits and can be used for symbolic machine-word arithmetic. Bits are stored in most-significant-bit first order.

Instances

Functor BV

Foldable BV

Traversable BV

Eq l => Eq (BV l)

Ord l => Ord (BV l)

Show l => Show (BV l)

empty :: BV l

Empty bitvector

length :: BV l -> Int

Number of bits in a bit vector

at :: BV l -> Int -> l

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

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

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

concat :: [BV l] -> BV l

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

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

Project out the n most significant bits from a bitvector.

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

Drop the n most significant bits from a bitvector.

slice

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

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.

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

Combine two bitvectors with a bitwise function

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

Combine two bitvectors with a bitwise monadic combiner action.

msb :: BV l -> l

Retrieve the most significant bit of a bitvector.

lsb :: BV l -> l

Retrieve the least significant bit of a bitvector.

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

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

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

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

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

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

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

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

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

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

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

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

muxInteger

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

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)

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)

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

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)

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

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)

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

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)

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

Lazy negation of a circuit.

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

Conditionals

ite

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

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

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

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

bvToList :: BV l -> [l]

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))

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))

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)

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))

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)

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))

Add a constant value to a bitvector

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

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))

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))

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))

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))

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))

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))

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))

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

Shifts and rolls

shl

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

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

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

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

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)

Test equality of two bitvectors with the same size.

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

Test if a bitvector is equal to zero

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

Test if a bitvector is distinct from zero

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

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)

Signed less-than on bitvector with the same size.

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

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)

Unsigned less-than on bitvector with the same size.

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

Return absolute value of signed bitvector.

Extensions

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

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)

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)

Truncate the given bit vector to the specified length

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

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)

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

Priority encoder, lg2, and related functions

priorityEncode

Arguments

:: IsAIG l g

=> g s

-> Int

width of the output bitvector

-> BV (l s)

input bitvector

-> IO (l s, BV (l s))

Valid bit and position bitvector

Priority encoder. Given a bitvector, calculate the bit position of the most-significant 1 bit, with position 0 corresponding to the least-significant-bit. Return the "valid" bit, which is set iff at least one bit in the input is set; and the calcuated bit position. If no bits are set in the input (i.e. if the valid bit is false), the calculated bit position is zero. The indicated bitwidth must be large enough to hold the answer; in particular, we must have (length bv <= 2^w).

logBase2_down

Arguments

:: IsAIG l g

=> g s

-> BV (l s)

input bitvector

-> IO (BV (l s))

Compute the rounded-down base2 logarithm of the input bitvector. For x > 0, this uniquely satisfies 2^(logBase2_down(x)) <= x < 2^(logBase2_down(x)+1). For x = 0, we set logBase2(x) = -1. The output bitvector has the same width as the input bitvector.

logBase2_up

Arguments

:: IsAIG l g

=> g s

-> BV (l s)

input bitvector

-> IO (BV (l s))

Compute the rounded-up base2 logarithm of the input bitvector. For x > 1, this uniquely satisfies 2^(logBase2_up(x) - 1) < x <= 2^(logBase2_up(x)). For x = 1, logBase2_up 1 = 0. For x = 0, we get logBase2_up 0 = bitvector length; this just happens to work out from the defining fomula `logBase2_up x = logBase2_down (x-1) + 1` when interpreted in 2's complement. The output bitvector has the same width as the input bitvector.

countLeadingZeros

Arguments

:: IsAIG l g

=> g s

-> BV (l s)

input bitvector

-> IO (BV (l s))

Count the number of leading zeros in the input vector; that is, the number of more-significant digits set to 0 above the most significant digit that is set. If the input vector is 0, the output of this function is the length of the bitvector (i.e., all digits are counted as leading zeros). The output bitvector has the same width as the input bitvector.

countTrailingZeros

Arguments

:: IsAIG l g

=> g s

-> BV (l s)

input bitvector

-> IO (BV (l s))

Count the number of trailing zeros in the input vector; that is, the number of less-significant digits set to 0 below the least significant digit which is set. If the input vector is 0, the output of this function is the length of the bitvector (i.e., all digits are counted as trailing zeros). The output bitvector has the same width as the input bitvector.

Polynomial multiplication, division and modulus in the finite

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

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.

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

Polynomial division. Return value has length equal to the first argument.

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

Polynomial mod with symbolic modulus. Return value has length one less than the length of the modulus. This implementation is optimized for the (common) case where the modulus is concrete.