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
- Building bitvectors
- Deconstructing bitvectors
Numeric operations on bitvectors
Polynomial multiplication and modulus

Description

A collection of higher-level operations (mostly various 2's complement arithmetic operations) that can be build 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

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

zipWithM :: (l -> l -> IO l) -> BV l -> BV l -> IO (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.

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

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

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.

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.

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.

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.

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.

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.

Extensions

sext :: BV l -> Int -> BV l 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.

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.