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
Priority encoder, lg2, and related functions
Polynomial multiplication, division and modulus in the finite

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. Bits are stored in most-significant-bit first order.

Instances

Functor BV Source
Foldable BV Source
Traversable BV Source
Eq l => Eq (BV l) Source
Ord l => Ord (BV l) Source
Show l => Show (BV l) Source

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.

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

Priority encoder, lg2, and related functions

priorityEncode Source

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 Source

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 Source

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 Source

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 Source

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

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

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

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.