## CircuitSynthesis Module

This file implements functions for translating expressions of finite type to an equivalent circuit representation. The overall idea is that the circuit is generated as a side effect when calling a generator function with input bitvectors. The generator function is thereby given the input and output bitvectors as BoolExpr list.

### Types

 Type Description This type provides basic gates for implementing circuits of finite type Quartz expressions. For the encoding of NatExpr and IntExpr, we use radix-2 and 2-complement numbers which are represented by lists of boolean variables [b[0],...,b[n-1]] where b[0] is the least significant bit. We also have word-level gates that obtain bitvectors with the same type. The outputs of these gates are generated by their abbreviation in the circuit map which associates each gate with a BoolExpr list which are its outputs. In particular, we have: NOT(b) = [!b] AND(b1,b2) = [b1∧b2] XOR(b1,b2) = [b1⊕b2] OR(b1,b2) = [b1∨b2] HA(b1,b2) = [b1⊕b2;b1∧b2] FA(b1,b2,cIn) = [b1⊕b2⊕cIn;b1∧b2∨cIn∧(b1⊕b2)] PG(g1,p1,g2,p2) = [g2∨(p2∧g1);p2∧p1] BvNOT(bv) = [!bv[0]..!bv[n-1]] BvAND(bv1,bv2) = [b1[0]∧b2[0]..b1[n-1]∧b2[n-1]] BvXOR(bv1,bv2) = [b1[0]⊕b2[0]..b1[n-1]⊕b2[n-1]] BvOR(bv1,bv2) = [b1[0]∨b2[0]..b1[n-1]∨b2[n-1]] bv2nat(BvHA(bv1,bv2)) = bv2nat(bv1)+bv2nat(bv2) bv2nat(BvFA(bv1,bv2,cIn)) = bv2nat(bv1)+bv2nat(bv2)+bv2nat(cIn) MX(c,bv0,bv1) = [(c?bv1[0]:bv0[0]);...;(c?bv1[n-1]:bv0[n-1]);] SW(c,bv0,bv1) = [(c?bv1[0]:bv0[0]);...;(c?bv1[n-1]:bv0[n-1]); (c?bv0[0]:bv1[0]);...;(c?bv0[n-1]:bv1[n-1])] type of leveled circuits; levels = independent microsteps to define depth

### Functions and values

Function or value Description
 AddNewGate g 
Full Usage: AddNewGate g

Parameters:
g : CircuitGate

Returns: BoolExpr list

add a new gate to the circuit and return its output vector; if the gate already exists, no gate is added, and the existing outputs are returned

g : CircuitGate
Returns: BoolExpr list
 Batc68Concentrator rmMSB x 
Full Usage: Batc68Concentrator rmMSB x

Parameters:
rmMSB : bool
x : BoolExpr list list

Returns: BoolExpr list list

This concentrator is derived from Batcher's bitonic sorting network by just comparing the most significant address bits, and removing these from the outputs in case rmMSB is true (so that the next bits are considered in the next stage of the radix-based sorting network). It leads to a binary sorter of depth O(log(n)^2) and size O(nlog(n)^2). See also

rmMSB : bool
x : BoolExpr list list
Returns: BoolExpr list list
 BatcherBanyan x 
Full Usage: BatcherBanyan x

Parameters:
x : BoolExpr list list

Returns: BoolExpr list list

This circuit implements a Batcher-Banyan network (see [Nara88]) which consists of a (Batcher) sorting network that sorts the inputs by their addresses

x : BoolExpr list list
Returns: BoolExpr list list
 BitBlastBoolExpr expr 
Full Usage: BitBlastBoolExpr expr

Parameters:
expr : BoolExpr

Returns: BoolExpr

expr : BoolExpr
Returns: BoolExpr
 BitBlastBtvExpr expr 
Full Usage: BitBlastBtvExpr expr

Parameters:
expr : BtvExpr

Returns: BtvExpr

expr : BtvExpr
Returns: BtvExpr
 BitBlastIntExpr expr 
Full Usage: BitBlastIntExpr expr

Parameters:
expr : IntExpr

Returns: IntExpr

expr : IntExpr
Returns: IntExpr
 BitBlastLhsExpr lhsExpr 
Full Usage: BitBlastLhsExpr lhsExpr

Parameters:
lhsExpr : LhsExpr

Returns: LhsExpr

lhsExpr : LhsExpr
Returns: LhsExpr
 BitBlastNatExpr expr 
Full Usage: BitBlastNatExpr expr

Parameters:
expr : NatExpr

Returns: NatExpr

expr : NatExpr
Returns: NatExpr
 BitonicMerger addCmpSwap inputs 
Full Usage: BitonicMerger addCmpSwap inputs

Parameters:
addCmpSwap : BoolExpr list * BoolExpr list -> BoolExpr list * BoolExpr list
inputs : BoolExpr list list

Returns: BoolExpr list list

This circuit implements Batcher's bitonic merge network that is based on a network with compare-and-swap modules which are combined in half cleaners. Essentially, Batcher's bitonic merge network is a binary tree whose nodes are half cleaners whose width is doubled in each level of the tree (the leftmost half cleaner in the root node should reverse the second half of its input which is done in the call in BitonicSorter). See also

addCmpSwap : BoolExpr list * BoolExpr list -> BoolExpr list * BoolExpr list
inputs : BoolExpr list list
Returns: BoolExpr list list
 BitonicSorter addCmpSwap x 
Full Usage: BitonicSorter addCmpSwap x

Parameters:
addCmpSwap : BoolExpr list * BoolExpr list -> BoolExpr list * BoolExpr list
x : BoolExpr list list

Returns: BoolExpr list list

This circuit implements Batcher's bitonic sorting network that is based on the merge sort paradigm, i.e., first splitting the given list into halves, sorting these recursively with the same algorithm, and then merging the sorted halves into a single sorted list. The merging step is done here by Batcher's bitonic merge network (function BitonicMerger) where however the second half of its input has to be reversed to obtain a bitonic sequence. See also

addCmpSwap : BoolExpr list * BoolExpr list -> BoolExpr list * BoolExpr list
x : BoolExpr list list
Returns: BoolExpr list list
 ChCh96Concentrator rmMSB x 
Full Usage: ChCh96Concentrator rmMSB x

Parameters:
rmMSB : bool
x : BoolExpr list list

Returns: BoolExpr list list

This concentrator is defined in [ChCh96] and recursively implements a binary sorter that is based on the observation that all internal vectors can be made compact vectors in the sense that all 1s in these vectors occur as a contiguous sequence. The concentrator is based on the generalized cube network which is the BY-BF-FS (banyan/butterfly network with outgoing flip shuffle permutation). The network used is isomorphic to the Omega-network and also to Batcher's bitonic merger.

To route the input vector to a sorted binary vector, all internal results are becoming compact sequences [ChCh96]. The configuration is obtained by first splitting the input vector successively in halves in that we put a binary tree above it, and then compute for each node the number of 1s it covers. Using carry ripple adders requires 2*log(n)+1 steps to do this. The routing is then based on these numbers; details can be found in

rmMSB : bool
x : BoolExpr list list
Returns: BoolExpr list list
 ChOr94Concentrator rmMSB x 
Full Usage: ChOr94Concentrator rmMSB x

Parameters:
rmMSB : bool
x : BoolExpr list list

Returns: BoolExpr list list

This concentrator is defined in [ChOr94] and implements recursively a binary sorter using the parallel merge sort paradigm (see ChOr94Merger). Hence, the given input vector is split into two halves which are sorted recursively, and are then merged by ChOr94Merger for n>2. See also function ChOr94Merger and

rmMSB : bool
x : BoolExpr list list
Returns: BoolExpr list list
 ChOr94Merger isFinal x 
Full Usage: ChOr94Merger isFinal x

Parameters:
isFinal : bool
x : BoolExpr list list

Returns: BoolExpr list list

This concentrator is defined in [ChOr94] and implements recursively a binary sorter using the parallel merge-sort paradigm. Merging is done here for so-called bi-sorted binary sequences, i.e., sequences whose two halves are sorted sequences. The merging circuit used in the design is able to merge two bi-sorted sequences into a single sorted sequence. This is done by the observation that if two sorted binary lists xUpp and xLow are split into halves, i.e., xUpp=x1*x2 and xLow=x3*x4, then two of these halves are clean, i.e. contain only 0s or only 1s, and the other two halves are sorted. The merging circuit has to identify the clean and the sorted quaters and forwards the sorted quarters to a recursive merge module. Finally, it concatenates the already clean quarters with the sorted result of the recursive call. See also

isFinal : bool
x : BoolExpr list list
Returns: BoolExpr list list
 CheckConcentrator checkSorter checkTernary checkRBS circ 
Full Usage: CheckConcentrator checkSorter checkTernary checkRBS circ

Parameters:
checkSorter : bool
checkTernary : bool
checkRBS : bool
circ : LeveledCircuit

Returns: (Map<BoolExpr, bool> * int list * int list) option

Checking the correctness of a binary/ternary sorter/concentrator: The function simulates the given LeveledCircuit for all possible inputs and will check whether it is a binary/ternary sorter/concentrator. The result will be an optional tuple (env,xVec,yVec) holding a potential counterexample where 0,1,2 means 0,⊥,1 in ternary and 0,1 obviously means 0,1 in binary. For binary inputs, all bits of an input are constant so that 2**n vectors have to be checked. Their length is log2(n)+1 since we use one message bit. Ternary inputs look like |v0;v1;|v0|v1...v1| using two message bits, one validity bit v0, and log(n) address bits. If input checkSorter holds, it is checked that the output sequence is of the form 0..0⊥..⊥1..1, and otherwise, it is checked that it is a concentrated vector, i.e., 0s are only allowed in the upper half if the lower half is full of 0s, and 1s are only allowed in the lower half if the upper half is full of 1s. Finally, if checkRBS is true, then all input vectors are ignored where the number of 0s or the number of 1s exceeds n/2.

checkSorter : bool
checkTernary : bool
checkRBS : bool
circ : LeveledCircuit
Returns: (Map<BoolExpr, bool> * int list * int list) option
 CheckFunction genCircuit checkFun n1 n2 
Full Usage: CheckFunction genCircuit checkFun n1 n2

Parameters:
genCircuit : BoolExpr list -> BoolExpr list -> BoolExpr list
checkFun : bool list -> bool list -> bool list -> bool
n1 : int
n2 : int

Returns: (bool list * bool list * bool list) list

Check correctness of an arithmetic circuit generator genCircuit: This function will generate all bitvectors with n1 and n2 bits, respectively, as arguments, and will then evaluate the circuit on all input vectors. It then checks whether the given function checkFun yields true when given the input and output bitvectors.

genCircuit : BoolExpr list -> BoolExpr list -> BoolExpr list
checkFun : bool list -> bool list -> bool list -> bool
n1 : int
n2 : int
Returns: (bool list * bool list * bool list) list
 CheckInterconnectionNetworkPartial circ 
Full Usage: CheckInterconnectionNetworkPartial circ

Parameters:
circ : LeveledCircuit

Returns: (int option list * Map<BoolExpr, bool>) option

Checking whether an interconnection network given as a circuit can route all partial permutations correctly. The function simulates the circuit with all partial permutations where the circuit with n inputs is expected to have inputs x[i] with 2*(log2 n)+1 bits since the target address will have log2(n) bits, and it is also used as the message for each x[i]. Morever, each input has a valid bit so that each x[i] consists of the message x[i][0..q-1]*x[i][q]*x[i][q+1..2q+1] with q:=log2(n). Note that the number of partial permutations of n objects is given as sum_{i=0}^{n} i!*binom(n,i)^2 (see function Global.PartialPermutations). The result is an optional pair (perm,env) where perm is the input vector of type (int option)[], and env the variable environment obtained by the simulation in case a counterexample has been found. If the circuit correctly routes all partial permutations the result is None.

circ : LeveledCircuit
Returns: (int option list * Map<BoolExpr, bool>) option
 CheckLeveledCircuit c spec 
Full Usage: CheckLeveledCircuit c spec

Parameters:
c : LeveledCircuit
spec : bool list list -> bool list list -> bool

Returns: Map<BoolExpr, bool> list

This function verifies a given leveled circuit in that it simulates it on all possible inputs and checks whether the given F# function spec satisfies the input/output combination. It returns all variable assignments where the specification failed.

c : LeveledCircuit
spec : bool list list -> bool list list -> bool
Returns: Map<BoolExpr, bool> list
 CheckRankingCircuit firstRank rankGen n 
Full Usage: CheckRankingCircuit firstRank rankGen n

Parameters:
firstRank : int
rankGen : BoolExpr list -> BoolExpr list list
n : int

Returns: bool list list

checking the correctness of a ranking circuit that starts with firstRank for the first valid entry (RankingTree0 needs 1, others 0), e.g. you may use this as follows

• List.map (CheckRankingCircuit 1 RankingTree0) [2;4;8;16];;
• List.map (CheckRankingCircuit 0 RankingTree1) [2;4;8;16];;
• List.map (CheckRankingCircuit 0 RankingTree2) [2;4;8;16];;

firstRank : int
rankGen : BoolExpr list -> BoolExpr list list
n : int
Returns: bool list list
 CircBoolExpr expr 
Full Usage: CircBoolExpr expr

Parameters:
expr : BoolExpr

Returns: BoolExpr

generate a circuit for a BoolExpr

expr : BoolExpr
Returns: BoolExpr
 CircBtvExpr expr 
Full Usage: CircBtvExpr expr

Parameters:
expr : BtvExpr

Returns: BoolExpr list

generate a circuit for a BtvExpr

expr : BtvExpr
Returns: BoolExpr list
 CircExpr expr 
Full Usage: CircExpr expr

Parameters:
expr : Expr

Returns: BoolExpr list

generate a circuit for an Expr

expr : Expr
Returns: BoolExpr list
 CircIntAbs natAddCirc x 
Full Usage: CircIntAbs natAddCirc x

Parameters:
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> 'a
x : BoolExpr list

Returns: 'a

generate a circuit to compute the absolute value of a 2-complement number with n-bits (the result is a radix-2 number with n-bits); in case of negative numbers, an addition is required so that the circuit is parameterized by a circuit generator for radix-2 adders

natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> 'a
x : BoolExpr list
Returns: 'a
 CircIntAddCLA parPrefix x1 x2 cIn 
Full Usage: CircIntAddCLA parPrefix x1 x2 cIn

Parameters:
parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list
cIn : BoolExpr option

Returns: BoolExpr list

generate a circuit for carry-lookahead addition of 2-complement numbers with size O(n) and depth O(log(n))

parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list
cIn : BoolExpr option
Returns: BoolExpr list
 CircIntAddCRA x1 x2 cIn 
Full Usage: CircIntAddCRA x1 x2 cIn

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list
cIn : BoolExpr option

Returns: BoolExpr list

generate a circuit for carry-ripple subtraction of 2-complement numbers with size O(n) and depth O(n)

x1 : BoolExpr list
x2 : BoolExpr list
cIn : BoolExpr option
Returns: BoolExpr list
 CircIntDiv natDivModCirc natAddCirc x1 x2 
Full Usage: CircIntDiv natDivModCirc natAddCirc x1 x2

Parameters:
natDivModCirc : BoolExpr list option -> (BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list) -> BoolExpr list -> BoolExpr list -> BoolExpr list * 'a
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

natDivModCirc : BoolExpr list option -> (BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list) -> BoolExpr list -> BoolExpr list -> BoolExpr list * 'a
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntDivMod natDivModCirc natAddCirc x1 x2 
Full Usage: CircIntDivMod natDivModCirc natAddCirc x1 x2

Parameters:
natDivModCirc : BoolExpr list option -> (BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list) -> BoolExpr list -> BoolExpr list -> BoolExpr list * 'a
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list * 'a

Given a circuit generators for division and addition of radix-2 numbers, CircIntDivMod generates a circuit for division of 2-complement numbers.

natDivModCirc : BoolExpr list option -> (BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list) -> BoolExpr list -> BoolExpr list -> BoolExpr list * 'a
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list * 'a
 CircIntDivNPF natAddCirc x1 x2 
Full Usage: CircIntDivNPF natAddCirc x1 x2

Parameters:
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a circuit for non-performing 2-complement division using the specified circuit for radix-2 addition

natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntDivNRL natAddCirc x1 x2 
Full Usage: CircIntDivNRL natAddCirc x1 x2

Parameters:
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a circuit for non-restoring 2-complement division using the specified circuit for radix-2 addition

natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntDivNRS natAddCirc x1 x2 
Full Usage: CircIntDivNRS natAddCirc x1 x2

Parameters:
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a circuit for non-restoring 2-complement division using the specified circuit for radix-2 addition with only

natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntDivRST natAddCirc x1 x2 
Full Usage: CircIntDivRST natAddCirc x1 x2

Parameters:
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a circuit for restoring 2-complement division using the specified circuit for radix-2 addition

natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntEqu x1 x2 
Full Usage: CircIntEqu x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr

generate a circuit to check equality of 2-complement numbers with size O(n) and depth O(log(n))

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr
 CircIntExp cIntMul x1 x2 
Full Usage: CircIntExp cIntMul x1 x2

Parameters:
cIntMul : BoolExpr list -> BoolExpr list -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

CircIntExp computes the power of x1 by x2 using the given multiplier generator where x2 is a radix-2 number and x1 is a 2-complement number.

cIntMul : BoolExpr list -> BoolExpr list -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntExpr expr 
Full Usage: CircIntExpr expr

Parameters:
expr : IntExpr

Returns: BoolExpr list

generate a circuit for an IntExpr

expr : IntExpr
Returns: BoolExpr list
 CircIntLeq x1 x2 
Full Usage: CircIntLeq x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr

generate a circuit to compare (less than or equal) radix-2 numbers; size O(n) and depth O(log(n))

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr
 CircIntLes x1 x2 
Full Usage: CircIntLes x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr

generate a circuit to compare (less than) 2-complement numbers with size O(n) and depth O(log(n))

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr
 CircIntMod natDivModCirc natAddCirc x1 x2 
Full Usage: CircIntMod natDivModCirc natAddCirc x1 x2

Parameters:
natDivModCirc : BoolExpr list option -> (BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list) -> BoolExpr list -> BoolExpr list -> BoolExpr list * 'a
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: 'a

natDivModCirc : BoolExpr list option -> (BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list) -> BoolExpr list -> BoolExpr list -> BoolExpr list * 'a
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: 'a
 CircIntModNPF natAddCirc x1 x2 
Full Usage: CircIntModNPF natAddCirc x1 x2

Parameters:
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a circuit for non-performing 2-complement remainder using the specified circuit for radix-2 addition

natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntModNRL natAddCirc x1 x2 
Full Usage: CircIntModNRL natAddCirc x1 x2

Parameters:
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a circuit for non-restoring 2-complement remainder using the specified circuit for radix-2 addition

natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntModNRS natAddCirc x1 x2 
Full Usage: CircIntModNRS natAddCirc x1 x2

Parameters:
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a circuit for non-restoring 2-complement remainder using the specified circuit for radix-2 addition with only

natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntModRST natAddCirc x1 x2 
Full Usage: CircIntModRST natAddCirc x1 x2

Parameters:
natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a circuit for restoring 2-complement remainder using the specified circuit for radix-2 addition

natAddCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntMulCRA x1 x2 
Full Usage: CircIntMulCRA x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

IntMulCRA is a simple paper-and-pencil multiplier for 2-complement numbers that adds up the partial products row by row using carry-ripple adders.

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntMulCSA x1 x2 
Full Usage: CircIntMulCSA x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

Generate a multiplier for 2-complement numbers using carry-save adders. After generating rows of partial products, we always pick the first three rows and reduce them using a carry save adder in a single step to two rows keeping the other rows untouched. The final two rows are added by a carry-ripple adder so that the circuit has a size of O(n*m) and a depth of O(m+n).

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntMulDadda parPrefix x1 x2 
Full Usage: CircIntMulDadda parPrefix x1 x2

Parameters:
parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

CircIntMulDadda generates a Dadda multiplier for 2-complement numbers. It has a size of O(n*m) and a depth of O(log(n+m)) and requires typically less gates than other logarithmic-depth multipliers.

parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntMulGreedy parPrefix x1 x2 
Full Usage: CircIntMulGreedy parPrefix x1 x2

Parameters:
parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

CircIntMulGreedy is a logarithmic depth multiplier that first generates all partial products and then aggressively reduces the columns as much as possible using full and half adders.

parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntMulWallace parPrefix x1 x2 
Full Usage: CircIntMulWallace parPrefix x1 x2

Parameters:
parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

Generate a Wallace multiplier for 2-complement numbers, which works by a repeated reduction of the summands (rows of partial products) in that groups of three rows are compressed to two rows using a CSA adder. The obtained circuit has a depth of O(log(n+m)) and a size of O(n*m).

parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntNeq x1 x2 
Full Usage: CircIntNeq x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr

generate a circuit to check inequality of 2-complement numbers with size O(n) and depth O(log(n))

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr
 CircIntSubCLA parPrefix x1 x2 
Full Usage: CircIntSubCLA parPrefix x1 x2

Parameters:
parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

The function adds gates for a carry-lookahead subtraction of 2-complement numbers x1 and x2 of the same length n and returns the n+1 bits of the sum bitvector.

parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircIntSubCRA x1 x2 
Full Usage: CircIntSubCRA x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a circuit for carry-ripple subtraction of 2-complement numbers with size O(n) and depth O(n)

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircMulCSA useInt x1 x2 
Full Usage: CircMulCSA useInt x1 x2

Parameters:
useInt : bool
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

Generate a multiplier with carry-save adders. After generating rows of partial products, we always pick the first three rows and reduce them using a carry save adder in a single step to two rows keeping the other rows untouched. The final two rows are added by a carry-ripple adder so that the circuit has a size of O(n*m) and a depth of O(m+n).

useInt : bool
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircMulWallace parPrefix useInt x1 x2 
Full Usage: CircMulWallace parPrefix useInt x1 x2

Parameters:
parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
useInt : bool
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

Generate a Wallace multiplier for radix-2 numbers, which works by a repeated reduction of the summands (rows of partial products) in that groups of three rows are compressed to two rows using a CSA adder. This way, the number of rows row[i] for multiplying n by m bits is defined as row[0] := m and row[j+1] := 2*(row[j] div 3) + (row[j] mod 3). At the end, the final two summands are added by a carry-lookahead adder, so that the obtained circuit has a depth of O(log(n+m)) and a size of O(n*m).

parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
useInt : bool
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatAddCLA parPrefix x1 x2 cIn 
Full Usage: CircNatAddCLA parPrefix x1 x2 cIn

Parameters:
parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list
cIn : BoolExpr option

Returns: BoolExpr list

parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list
cIn : BoolExpr option
Returns: BoolExpr list
 CircNatAddCRA x1 x2 cIn 
Full Usage: CircNatAddCRA x1 x2 cIn

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list
cIn : BoolExpr option

Returns: BoolExpr list

generate a circuit for carry-ripple addition of radix-2 numbers with size O(n) and depth O(n)

x1 : BoolExpr list
x2 : BoolExpr list
cIn : BoolExpr option
Returns: BoolExpr list
 CircNatDivModNPF rInit addCirc x1 x2 
Full Usage: CircNatDivModNPF rInit addCirc x1 x2

Parameters:
rInit : BoolExpr list option
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list * BoolExpr list

CircNatDivModNPF generates a circuit for non-performing radix-2 division, i.e., a division algorithm that first checks if the shifted divisor is less than or equal to the dividend. If so, it is subtracted, otherwise, the divisor is just shifted. If a subtraction takes place, the corresponding quotient bit is 1, and otherwise 0. The algorithm uses subtraction with x2Len-1 operands. To be used also for integer division, the circuit is given a rInit parameter that is determined by CircIntDivMod and is a bitvector with x2Length zeros for radix-2 division (which is generated by the function in case of value None).

rInit : BoolExpr list option
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list * BoolExpr list
 CircNatDivModNRL rInit addCirc x1 x2 
Full Usage: CircNatDivModNRL rInit addCirc x1 x2

Parameters:
rInit : BoolExpr list option
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list * BoolExpr list

CircNatDivModNonRestoreLong generates a circuit for non-restoring radix-2 division, i.e., by either subtracting or adding the second operand, depending on the sign of the previous result which also determines the previous bit obtained for the quotient. The generated circuit uses x2Len+1 bits for the subtraction/addition operations which is easier to understand compared with the more efficient version CircNatDivModNonRestore.

rInit : BoolExpr list option
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list * BoolExpr list
 CircNatDivModNRS rInit addCirc x1 x2 
Full Usage: CircNatDivModNRS rInit addCirc x1 x2

Parameters:
rInit : BoolExpr list option
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list * BoolExpr list

CircNatDivModNonRestoring generates a circuit for non-restoring radix-2 division, i.e., by either subtracting or adding the second operand, depending on the sign of the previous result which also determines the previous bit obtained for the quotient. The generated circuit uses x2Len bits for the subtraction/addition operations. To be used also for integer division, the circuit is given a rInit parameter that is determined by CircIntDivMod and is a bitvector with x2Length zeros for radix-2 division (which is generated by the function in case of value None).

rInit : BoolExpr list option
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list * BoolExpr list
 CircNatDivModRST rInit addCirc x1 x2 
Full Usage: CircNatDivModRST rInit addCirc x1 x2

Parameters:
rInit : BoolExpr list option
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list * BoolExpr list

CircNatDivModRST generates a circuit for a restoring radix-2 division, i.e., a division algorithm that first subtracts the shifted divisor to check whether it was less than the dividend. If so, the result of the subtraction is the new dividend, otherwise, the previous one is retained. otherwise, the divisor is just shifted. To be used also for integer division, the circuit is given a rInit parameter that is determined by CircIntDivMod and is a bitvector with x2Length zeros for radix-2 division (which is generated by the function in case of value None).

rInit : BoolExpr list option
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list * BoolExpr list
 CircNatDivNPF addCirc x1 x2 
Full Usage: CircNatDivNPF addCirc x1 x2

Parameters:
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a nonperforming division with given adders for the quotient

addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatDivNRL addCirc x1 x2 
Full Usage: CircNatDivNRL addCirc x1 x2

Parameters:
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a nonrestoring division with given adders for the quotient

addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatDivNRS addCirc x1 x2 
Full Usage: CircNatDivNRS addCirc x1 x2

Parameters:
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a non-restoring division with given adders for the quotient

addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatDivRST addCirc x1 x2 
Full Usage: CircNatDivRST addCirc x1 x2

Parameters:
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a restoring division with given adders for the quotient

addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatEqu x1 x2 
Full Usage: CircNatEqu x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr

generate a circuit to check equality of radix-2 numbers with size O(n) and depth O(log(n))

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr
 CircNatExp cNatMul x1 x2 
Full Usage: CircNatExp cNatMul x1 x2

Parameters:
cNatMul : BoolExpr list -> BoolExpr list -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

CircNatExp computes the power of x1 by x2 using the given multiplier generator. The circuits has (2^{x2Len+1}-1)*x1Len many output bits.

cNatMul : BoolExpr list -> BoolExpr list -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatExpr expr 
Full Usage: CircNatExpr expr

Parameters:
expr : NatExpr

Returns: BoolExpr list

generate a circuit for a NatExpr

expr : NatExpr
Returns: BoolExpr list
 CircNatLeq x1 x2 
Full Usage: CircNatLeq x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr

generate a circuit to compare (less than or equal) radix-2 numbers with size O(n) and depth O(log(n))

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr
 CircNatLes x1 x2 
Full Usage: CircNatLes x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr

generate a circuit to compare (less than) radix-2 numbers with size O(n) and depth O(log(n))

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr
 CircNatModNPF addCirc x1 x2 
Full Usage: CircNatModNPF addCirc x1 x2

Parameters:
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a nonperforming division with given adders for the remainder

addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatModNRL addCirc x1 x2 
Full Usage: CircNatModNRL addCirc x1 x2

Parameters:
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a nonrestoring division with given adders for the remainder

addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatModNRS addCirc x1 x2 
Full Usage: CircNatModNRS addCirc x1 x2

Parameters:
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a non-restoring division with given adders for the remainder

addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatModRST addCirc x1 x2 
Full Usage: CircNatModRST addCirc x1 x2

Parameters:
addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a restoring division with given adders for the remainder

addCirc : BoolExpr list -> BoolExpr list -> BoolExpr option -> BoolExpr list
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatMulCRA x1 x2 
Full Usage: CircNatMulCRA x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a circuit for paper-and-pencil multiplication of radix-2 numbers; i.e., generate all n*m partial products and add the rows using NatAddCRA; size O(n*n) and depth O(log(n)), for a nxn multiplier is 3(n-1), the number of AND gates is n*n for the partial products, and n-1 half adders, and (n-1)^2 full adders are used.

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatMulCSA x1 x2 
Full Usage: CircNatMulCSA x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

Generate a multiplier for radix-2 numbers using carry-save adders. After generating rows of partial products, we always pick the first three rows and reduce them using a carry save adder in a single step to two rows keeping the other rows untouched. The final two rows are added by a carry-ripple adder so that the circuit has a size of O(n*m) and a depth of O(m+n).

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatMulDadda parPrefix x1 x2 
Full Usage: CircNatMulDadda parPrefix x1 x2

Parameters:
parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

CircNatMulDadda generates a Dadda multiplier for radix-2 numbers. It has a size of O(n*m) and a depth of O(log(n+m)) and requires typically less gates than other logarithmic-depth multipliers.

parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatMulGreedy parPrefix x1 x2 
Full Usage: CircNatMulGreedy parPrefix x1 x2

Parameters:
parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

CircNatMulGreedy is a logarithmic depth multiplier that first generates all partial products and then aggressively reduces the columns as much as possible using full and half adders.

parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatMulWallace parPrefix x1 x2 
Full Usage: CircNatMulWallace parPrefix x1 x2

Parameters:
parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

Generate a Wallace multiplier for radix-2 numbers, which works by a repeated reduction of the summands (rows of partial products) in that groups of three rows are compressed to two rows using a CSA adder. The obtained circuit has a depth of O(log(n+m)) and a size of O(n*m).

parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatNeq x1 x2 
Full Usage: CircNatNeq x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr

generate a circuit to check inequality of radix-2 numbers with size O(n) and depth O(log(n))

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr
 CircNatSubCLA parPrefix x1 x2 
Full Usage: CircNatSubCLA parPrefix x1 x2

Parameters:
parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a circuit for carry-lookahead subtraction of radix-2 numbers with size O(n) and depth O(log(n))

parPrefix : ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> 'a
x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 CircNatSubCRA x1 x2 
Full Usage: CircNatSubCRA x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list

generate a circuit for carry-ripple subtraction of radix-2 numbers with size O(n) and depth O(n)

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list
 Circuit2BddInit circ 
Full Usage: Circuit2BddInit circ

Parameters:
circ : LeveledCircuit

Initialize the BDD package with the input variables of the given circuit.

circ : LeveledCircuit
 Circuit2Bdds garbageCollect circ 
Full Usage: Circuit2Bdds garbageCollect circ

Parameters:
garbageCollect : bool
circ : LeveledCircuit

Returns: int list list

Compute BDDs for the outputs of a given circuit. The function retains also all BDDs that have been computed for the internal wires of the circuit and could be optimized in that these are put into the garbage when no longer needed. If optFlag is true, the function will do garbage collection after every level of the circuit.

garbageCollect : bool
circ : LeveledCircuit
Returns: int list list
 ComputeComplexity c 
Full Usage: ComputeComplexity c

Parameters:
c : LeveledCircuit

Returns: int * int * int * int * int * int * int * int * int * int * int

Compute complexity measures of a leveled circuit: This function returns a tuple (depth,numAND,numXOR,numOR,numHA,numFA,numPG,size) where all components have the obvious meaning, and size is the gate count in terms of 2-input, 1-output gates (where HA, FA, PG, SW are expanded to 2, 5, 3, and 8 gates, respectively).

c : LeveledCircuit
Returns: int * int * int * int * int * int * int * int * int * int * int
 Crossbar mkPartial x 
Full Usage: Crossbar mkPartial x

Parameters:
mkPartial : bool
x : BoolExpr list list

Returns: BoolExpr list list

This generator constructs a crossbar circuit that can connect anyone of its n inputs with anyone of its n outputs as long as the mapping of the inputs to the outputs is a (partial) permutation. To this end, the n input vectors consist of q=x[i].Length-log2(n) bits of the message concatenated with log2(n) bits of the target address. Note that we do not have to distinguish partial permutations here.

mkPartial : bool
x : BoolExpr list list
Returns: BoolExpr list list
 EnumerateBitvectors n 
Full Usage: EnumerateBitvectors n

Parameters:
n : int

Returns: bool list list

enumerate all bitvectors with n digits for a full simulation

n : int
Returns: bool list list
 EvalComplement2 x 
Full Usage: EvalComplement2 x

Parameters:
x : bool list

Returns: BigInteger

evaluate a bitvector as a B-complement number

x : bool list
Returns: BigInteger
 EvalRadix2 x 
Full Usage: EvalRadix2 x

Parameters:
x : bool list

Returns: BigInteger

evaluate a bitvector as a radix-B number

x : bool list
Returns: BigInteger
 EvaluateLeveledCircuit varAssign c 
Full Usage: EvaluateLeveledCircuit varAssign c

Parameters:
varAssign : Map<BoolExpr, bool>
c : LeveledCircuit

Returns: Map<BoolExpr, bool>

Evaluate a leveled circuit based on a variable assignment varAssign that initially only holds values for the input variables. Based on these input values, the function evaluates each level and adds the values of all variables to the variable assignment that is finally returned.

varAssign : Map<BoolExpr, bool>
c : LeveledCircuit
Returns: Map<BoolExpr, bool>
 GetLeveledCircuit name inputs outputs 
Full Usage: GetLeveledCircuit name inputs outputs

Parameters:
name : string
inputs : BoolExpr list list
outputs : BoolExpr list list

Returns: LeveledCircuit

Levelize the circuit in the global circuit map into microstep levels

name : string
inputs : BoolExpr list list
outputs : BoolExpr list list
Returns: LeveledCircuit
 HalfCleanerBinaryOpt sortGen rmMSB x 
Full Usage: HalfCleanerBinaryOpt sortGen rmMSB x

Parameters:
sortGen : bool -> BoolExpr list list -> BoolExpr list list
rmMSB : bool
x : BoolExpr list list

Returns: BoolExpr list list

The following function takes a generator sortGen for a binary sorter and constructs a binary concentrator of it by using two sorters of half the size and a further half cleaner column as reported in [KoOr90,Nara88] and explicitly in [JaSc18,JaSJ17b]. The construction is therefore as follows:

where the half cleaner module (HC) consists of one column of compare-and-swap modules (the arrows show where the bigger input is moved to) in addition to an ingoing perfect shuffle permutation and an outgoing flip shuffle permutation:

The result is no longer a sorter, but still a concentrator which means that 0s and 1s are put in the preferred halves, so that one half will become clean (only consisting of 0s and 1s) as soon as possible. In general, for the two halves yLow and yUpp of its output vector y, we also have max(yLow) ≤ min(yUpp) but that becomes meaningless as soon as we have more than n/2 0s or 1s.

sortGen : bool -> BoolExpr list list -> BoolExpr list list
rmMSB : bool
x : BoolExpr list list
Returns: BoolExpr list list
 HalfCleanerTernaryOpt sortGen rmMSB x 
Full Usage: HalfCleanerTernaryOpt sortGen rmMSB x

Parameters:
sortGen : bool -> BoolExpr list list -> BoolExpr list list
rmMSB : bool
x : BoolExpr list list

Returns: BoolExpr list list

The following function takes a generator sortGen for a ternary sorter and constructs a concentrator of it by generating two sorters of half the size and a further half cleaner column as reported in [KoOr90,Nara88] and explicitly in [JaSc18,JaSJ17b]:

where the half cleaner module (HC) consists of one column of compare-and-swap modules (the arrows show where the bigger input is moved to) in addition to an ingoing perfect shuffle permutation and an outgoing flip shuffle permutation:

The result is no longer a sorter, but still a concentrator which means that 0s and 1s are put in the preferred halves, so that one half will become clean (only consisting of 0s and 1s) as soon as possible. In contrast to HalfCleanerBinaryOpt which only considers the msbs of the input vectors in the half cleaner, this function also considers their valid bit (bits 0..q-1 form the message, bit q is the valid bit, and bits q+1..q+log2(n) are the address bits with q+log2(n) as msb).

sortGen : bool -> BoolExpr list list -> BoolExpr list list
rmMSB : bool
x : BoolExpr list list
Returns: BoolExpr list list
 InitializeCircuit w 
Full Usage: InitializeCircuit w

Parameters:
w : string

reset the circuit generator with a name stub for the internal wires

w : string
 JaSJ17Concentrator rmMSB x 
Full Usage: JaSJ17Concentrator rmMSB x

Parameters:
rmMSB : bool
x : BoolExpr list list

Returns: BoolExpr list list

This circuit generator is a parallel version of Narasimha's concentrator [Nara94] that is published in [JaSJ17]: As Narasimha's concentrator, this circuit is based on a RB-FS-RV permutation network (reverse banyan/ flip shuffle with reverse output permutation) and configures switch i of each column by the parity of the input vector's prefix x[0..2i], so that half of the 0s in x[0..2i+1] are send to the lower and upper subnetworks (same with the 1s since each prefix x[0..2i+1] consists of an even number of inputs). In case that the prefix x[0..2i+1] contains an odd number of 0s (and therefore also an odd number of 1s, the additional 0 is sent to the lower and the additional 1 is sent to the upper subnetwork. See also

The difference between JaSJ17 and Nara94 is that the computations of the parity bits to configure the switches in JaSJ17 is done by a parallel prefix tree that reduces the depth of the concentrator from O(n) to only O(log(n)^2).

As for all the concentrator circuits implemented in this F# modules, each input x[i] is an input bitvector that is the concatenation of a message x[i][0..q-1] with q bits, a valid bit x[i][q] (that is viewed as part of the message for the binary sorters/concentrators/networks), and a destination address x[i][q+1..q+k] such that x[i][q+k] is the most significant bit of the destination address. Clearly, we have k=log2(x.Length). Also, all the concentrators/binary sorters concentrate the inputs according to the most significant bit x[i][q+k-1] and may or may not remove this bit during or after the concentration which is determined by the input parameter rmMSB. For constructing interconnection networks based on radix-based sorting, it is required to remove the msb so that the different stages sort by the different address bits, but if other constructions like HalfCleanerBinaryOpt or HalfCleanerTernaryOpt are used, the msb has to be retained for the latter.

rmMSB : bool
x : BoolExpr list list
Returns: BoolExpr list list
 KoOr90Concentrator rmMSB x 
Full Usage: KoOr90Concentrator rmMSB x

Parameters:
rmMSB : bool
x : BoolExpr list list

Returns: BoolExpr list list

Koppelman-Oruc-like Concentrator [KoOr90], i.e., binary sorting by first computing ranks and then self-routing by using the ranks as local target addresses. This version of the KoOr90 idea first computes the ranks of the 0s (by ranking the negated inputs) so that it can also be used with RadixBasedTernaryInterconnect to implement partial permutations. For routing the 0s to their local target address, i.e., their rank, we use a RB-FS-RV (reverse-banyan/flip-shuffle network with reverse output) permutation network, as used in Nara94 and JaSJ17 whose configuration is however determined in a different way using the ranks: Inputs are partitioned by the least significant bit of their rank. So, we first obtain two partitions with rank ...0 rank ...1, and after that, we have four partitions with ranks ...00, ...10, ...01, and ...11. In each stage, each group is split into two further groups with new address bits 0 and 1, respectively. Finally, we obtain for example for 8 inputs the ranks 000, 100, 010, 110, 001, 101, 011, and 111 so that the reverse output permutation (reversing the address bits) will map them to the right output.

The configuration of switch i based on the least significant bits r[2i][0] and r[2i+1][0] of the ranks as well as on the most significant bits xb[2i] and xb[2i+1] of inputs x[2i] and x[2i+1] is explained by the following truth table:

xb[2i] xb[2i+1] r[2i][0] r[2i+1][0] config
0 0 0 1 0 -> x[2i] to low-net, x[2i+1] to upp-net
0 0 1 0 1 -> x[2i] to upp-net, x[2i+1] to low-net
0 1 1 * 1 -> x[2i] to upp-net
0 1 0 * 0 -> x[2i] to low-net
1 0 * 1 0 -> x[2i+1] to upp-net
1 0 * 0 1 -> x[2i+1] to low-net
1 1 * * * -> don't care

Explanation: The goal is to route the 0s to the local target address given by their rank, hence,
• we have to send xb[2i]=0 to the low-net if r[2i][0]=0 holds
• we have to send xb[2i]=0 to the upp-net if r[2i][0]=1 holds
• we have to send xb[2i+1]=0 to the low-net if r[2i+1][0]=0 holds
• we have to send xb[2i+1]=0 to the upp-net if r[2i+1][0]=1 holds
If both inputs x[2i] x[2i+1] are 0, the bits of the ranks must be inequal by construction so that we only have to consider the two cases in the above table (the other two are don't cares). This way, the boolean function p[i] := (x[2i] ? !r[2i+1][0] : r[2i][0]) or equivalent p[i] := (x[2i+1] ? r[2i][0] : !r[2i+1][0]) is obtained for the configuration of the switches. Note further that we need the most significant bits xb[2i] and xb[2i+1] of the inputs for this purpose, so that they can only be removed at the end of the concentrator. Finally, note that for binary sorting, we could also rank and route the 1s and reverse the output, but that not work well with the construction of an interconnection network with RadixBasedTernaryInterconnect that can handle partial permutations. The depth of this binary sorter/concentrator is only O(log(n)) and its size is O(n*log(n)).

rmMSB : bool
x : BoolExpr list list
Returns: BoolExpr list list
 LeveledCircuit2Dot ostr c 
Full Usage: LeveledCircuit2Dot ostr c

Parameters:
ostr : TextWriter
c : LeveledCircuit

write a leveled circuit to a dot (graphviz) graph

ostr : TextWriter
c : LeveledCircuit
 MkInterconnectCircuit modName aryName optName cncName q n 
Full Usage: MkInterconnectCircuit modName aryName optName cncName q n

Parameters:
modName : string
aryName : string
optName : string
cncName : string
q : int
n : int

Returns: LeveledCircuit

This function will generate either a concentrator/sorter or an entire interconnection network based on radix-based sorting. It combines all other generator functions for concentrators and RBS interconnection networks including their optimization by half cleaners. To this end, the following inputs are expected:

• modName:
• TNT (RadixBasedTernaryInterconnect): for an entire RBS interconnection network with a front-end concentrator
• NET (RadixBasedInterconnect): for an entire RBS interconnection network
• CNC: for the construction of a concentrator
• aryName:
• BIN: binary sorter (splitters' inputs are booleans)
• TRP (TernaryParSorter): ternary sorter by parallel composition and a MUX stage
• TRC (TernaryParConcentrator): ternary sorter for RBS inputs by parallel composition
• TRS (TernarySeqSorter): ternary sorter by sequential composition [Nara94]
• optName:
• HC0: no optimization applied
• HC1: apply optimization by half cleaner lemma (uses HalfCleanerBinaryOpt in case of aryName=BIN and HalfCleanerTernaryOpt otherwise)
• cncName:
• Batc68: binary sorter by [Batc68]
• ChCh96: binary sorter by [ChCh96]
• ChOr94: binary sorter by [ChOr94]
• JaSJ17: binary sorter by [JaSJ17]
• KoOr90: binary sorter by [KoOr90]
• Nara94: binary sorter by [Nara94]
• q is the number of message bits
• n is the number of inputs/outputs

modName : string
aryName : string
optName : string
cncName : string
q : int
n : int
Returns: LeveledCircuit
 Nara94Concentrator rmMSB x 
Full Usage: Nara94Concentrator rmMSB x

Parameters:
rmMSB : bool
x : BoolExpr list list

Returns: BoolExpr list list

This circuit generator constructs Narasimha's concentrator [Nara94] which is actually a binary sorter: The circuit is based on a RB-FS-RV permutation network (reverse banyan/flip shuffle with reverse output permutation) and configures switch i of each column by the parity of the input vector's prefix x[0..2i], so that half of the 0s in x[0..2i+1] are send to the lower and upper subnetworks (same with the 1s since each prefix x[0..2i+1] consists of an even number of inputs). In case that the prefix x[0..2i+1] contains an odd number of 0s (and therefore also an odd number of 1s, the additional 0 is sent to the lower and the additional 1 is sent to the upper subnetwork. See also

As for all the concentrator circuits implemented in this F# modules, each input x[i] is an input bitvector that is the concatenation of a message x[i][0..q-1] with q bits, a valid bit x[i][q] (that is viewed as part of the message for the binary sorters/concentrators/networks), and a destination address x[i][q+1..q+k] such that x[i][q+k] is the most significant bit of the destination address. Clearly, we have k=log2(x.Length). Also, all the concentrators/binary sorters concentrate the inputs according to the most significant bit x[i][q+k-1] and may or may not remove this bit during or after the concentration which is determined by the input parameter rmMSB. For constructing interconnection networks based on radix-based sorting, it is required to remove the msb so that the different stages sort by the different address bits, but if other constructions like HalfCleanerBinaryOpt or HalfCleanerTernaryOpt are used, the msb has to be retained for the latter.

rmMSB : bool
x : BoolExpr list list
Returns: BoolExpr list list
 NewWireVector n 
Full Usage: NewWireVector n

Parameters:
n : int

Returns: BoolExpr list

generate a new vector of length n with names of new internal wires

n : int
Returns: BoolExpr list
 ParseLeveledCircuit istr 
Full Usage: ParseLeveledCircuit istr

Parameters:
istr : TextReader

Returns: LeveledCircuit

parse a leveled circuit from a TextReader

istr : TextReader
Returns: LeveledCircuit
 ParseLeveledCircuitFromFile filename 
Full Usage: ParseLeveledCircuitFromFile filename

Parameters:
filename : string

Returns: LeveledCircuit

parse a leveled circuit from a file

filename : string
Returns: LeveledCircuit
 ParseLeveledCircuitFromString s 
Full Usage: ParseLeveledCircuitFromString s

Parameters:
s : string

Returns: LeveledCircuit

parse a leveled circuit from a string

s : string
Returns: LeveledCircuit
 PrintComplexityTable circuitList nMin nMax step 
Full Usage: PrintComplexityTable circuitList nMin nMax step

Parameters:
circuitList : seq<string * 'a * (BoolExpr list -> BoolExpr list -> BoolExpr list)>
nMin : int
nMax : int
step : int

Returns: (string * (int * int * int) list) list

print complexity table in Latex

circuitList : seq<string * 'a * (BoolExpr list -> BoolExpr list -> BoolExpr list)>
nMin : int
nMax : int
step : int
Returns: (string * (int * int * int) list) list
 PrintGates () 
Full Usage: PrintGates ()

Parameters:
() : unit

print all gates of the circuit stored in the global map where generators have added gates so far

() : unit
 PrintLeveledCircuit ostr env c 
Full Usage: PrintLeveledCircuit ostr env c

Parameters:
ostr : TextWriter
env : Map<BoolExpr, bool> option
c : LeveledCircuit

print a leveled circuit to output stream ostr; if also a variable environment is given, the values of the variables in the circuit are printed as comments in each line of the definition of these variables.

ostr : TextWriter
env : Map<BoolExpr, bool> option
c : LeveledCircuit
 PrintLeveledCircuitInVHDL ostr c 
Full Usage: PrintLeveledCircuitInVHDL ostr c

Parameters:
ostr : TextWriter
c : LeveledCircuit

print a leveled circuit in VHDL

ostr : TextWriter
c : LeveledCircuit
 RadixBasedInterconnect split x 
Full Usage: RadixBasedInterconnect split x

Parameters:
split : BoolExpr list list -> BoolExpr list list
x : BoolExpr list list

Returns: BoolExpr list list

This generator function constructs an interconnection network based on radix-based sorting. As inputs, it first requires a function split that maps an input array x[0..n-1] to an output array z[0..n-1] such that the lower half z[0..n/2-1] and upper half z[n/2..n-1] are treated recursively with the same function. Finally, the outputs of these recursive calls are appended.

As split function, any concentrator with rmMSB=true can be used, as well as their optimization by HalfCleanerBinaryOpt, and also all combinations with functions TernaryParConcentrator, TernaryParSorter, and also TernarySeqSorter can be used. This can all be done conveniently by function MkInterconnectCircuit. As for all the concentrator circuits implemented in this F# module, each input x[i] is an input bitvector that is the concatenation of a message x[i][0..q-1] with q bits, a valid bit x[i][q], and a destination address x[i][q+1..q+k] such that x[i][q+k] is the most significant bit of the destination address. Clearly, we have k=log2(x.Length).

split : BoolExpr list list -> BoolExpr list list
x : BoolExpr list list
Returns: BoolExpr list list
 RadixBasedTernaryInterconnect split x 
Full Usage: RadixBasedTernaryInterconnect split x

Parameters:
split : BoolExpr list list -> BoolExpr list list
x : BoolExpr list list

Returns: BoolExpr list list

This generator function constructs an interconnection network based on radix-based sorting that is capable of routing partial permutations [Nara94] for KoOr90, JaSJ17, and Nara94. As inputs, it first requires a function split that maps an input array x[0..n-1] to an output array z[0..n-1] such that the lower half z[0..n/2-1] and upper half z[n/2..n-1] should contain the inputs with most significant address bits 0 and 1, respectively. In contrast to RadixBasedInterconnect, a first binary sorter is used to sort the inputs by their validity bits, such that the invalid inputs appear after the valid ones. Then, the target addresses of the invalid inputs are set to zero so that a further radix-based sorting with a certain binary sorting algorithm will move the inputs with most significant address bit 1 through the invalid ones. If we cut the RBS-network after its leftmost splitter, we would obtain exactly the circuit generated by TernarySeqSorter. As can be seen there, the outputs will be sorted as 0...0⊥...⊥1...1 by their msbs. Thus, the special RBS-network used here will cut that output into two halves, and will reverse the second one, so that 0...0⊥...⊥ and 1...1⊥...⊥ are obtained. Removing the msb allows then to recursively continue this way. CAUTION: This construction does not work with arbitrary binary sorters, the used binary sorters must either be stable so that they never flip real 0s with ⊥s (that have also address bits 0) or where the output index of all prefixes x[0..i] are only determined by the values in that prefix. Examples for such prefix-defined binary sorting algorithms are KoOr90, JaSJ17 and Nara94.

As for all the concentrator circuits implemented in this F# module, each input x[i] is an input bitvector that is the concatenation of a message x[i][0..q-1] with q bits, a valid bit x[i][q], and a destination address x[i][q+1..q+k] such that x[i][q+k] is the most significant bit of the destination address. Clearly, we have k=log2(x.Length).

split : BoolExpr list list -> BoolExpr list list
x : BoolExpr list list
Returns: BoolExpr list list
 RankingTree0 x 
Full Usage: RankingTree0 x

Parameters:
x : BoolExpr list

Returns: BoolExpr list list

Generate a circuit for a ranking, i.e., a circuit with n boolean inputs x[0..n-1], and n outputs y[i] of length ceil(log2(n+1)) such that y[i] is the rank of each valid input x[i]. In case of this circuit, rank[i] is simply the number of 1s in the prefix x[0..i], thus the first 1 will have rank 1, the second 1 will have rank 2, etc. Rank entries rank[i] for x[i]=0 have no meaning. The maximal possible rank is thus n. The circuit uses a parallel prefix computation of depth 2*log(n)-1 with 2*n-log(n)-2 carry ripple adders. The width of the used adders is adapted to the maximal width of the expected numbers.

x : BoolExpr list
Returns: BoolExpr list list
 RankingTree1 x 
Full Usage: RankingTree1 x

Parameters:
x : BoolExpr list

Returns: BoolExpr list list

Generate a circuit for a ranking, i.e., a circuit with n boolean inputs x[0..n-1], and n outputs y[i] of length ceil(log2(n)) such that y[i] is the rank of each valid input x[i]. In case of this circuit, rank[i] is simply the number of 1s in the prefix x[0..i] minus 1, thus the first 1 will have rank 0, the second 1 will have rank 1, etc. Rank entries rank[i] for x[i]=0 have no meaning. The maximal possible rank is n-1. The circuit uses a parallel prefix computation of depth 2*log(n)-1 with 2*n-log(n)-2 carry ripple adders. The width of the used adders is adapted to the maximal width of the expected numbers. This circuit is just derived by decrementing all ranks computed by RankingTree0.

x : BoolExpr list
Returns: BoolExpr list list
 RankingTree2 x 
Full Usage: RankingTree2 x

Parameters:
x : BoolExpr list

Returns: BoolExpr list list

Generate a circuit for a ranking, i.e., a circuit with n boolean inputs x[0..n-1], and n outputs y[i] of length ceil(log(n)) such that y[i] is the rank of each valid input x[i] which means that the leftmost valid x[i] will have rank 0, the next one has rank 1 and so on. This ranking circuit works with 2-complement numbers where initially all bits are prepended with a BoolConst false except for x[0] which will become [BoolConst true;BoolConst true]=-1 and [BoolConst false;BoolConst false]=0 for x[0]=0 and x[0]=1, respectively. Using these initial values, the same adder tree is applied as in the other ranking circuits of this module.

x : BoolExpr list
Returns: BoolExpr list list
 SignExtend x1 x2 
Full Usage: SignExtend x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list * BoolExpr list

sign-extend the shorter list so that they have equal length

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list * BoolExpr list
 TernaryParConcentrator sortGen rmMSB x 
Full Usage: TernaryParConcentrator sortGen rmMSB x

Parameters:
sortGen : bool -> BoolExpr list list -> BoolExpr list list
rmMSB : bool
x : BoolExpr list list

Returns: BoolExpr list list

This function (TRC) constructs a concentrator for ternary inputs using two binary sorters generated by sortGen. It is similar to TernaryParSorter, but does not make use of the multiplexers to select the 0s and 1s from the 0- and 1-sorter. Instead, it simply takes the lower half from the 0-sorter and the upper half from the 1-sorter, but remaps the 1 and 0 first back to ⊥ so that it will never take a 1 from the 0-sorter and never it will take a 0 from the 1-sorter (as TRP). However, this only works correctly if the numbers of 0s and 1s are less than or equal to n/2. If so, the circuit is even a ternary sorter, otherwise it is not even a correct concentrator.

sortGen : bool -> BoolExpr list list -> BoolExpr list list
rmMSB : bool
x : BoolExpr list list
Returns: BoolExpr list list
 TernaryParSorter sortGen rmMSB x 
Full Usage: TernaryParSorter sortGen rmMSB x

Parameters:
sortGen : bool -> BoolExpr list list -> BoolExpr list list
rmMSB : bool
x : BoolExpr list list

Returns: BoolExpr list list

This function (TRP) constructs a sorter for ternary inputs using two binary sorters generated by sortGen. The two binary sorters are thereby put in parallel where one (called the 1-sorter) considers ⊥ as 0 while the other one (called the 0-sorter) considers ⊥ as 1 for sorting. Hence, the 1-sorter's outputs 1 and the 0-sorter's outputs 0 are at the right places, so that the final output is obtained by taking the 1s from the 1-sorter and the 0s from the 0-sorter, leaving the remaining outputs ⊥.

As for all the concentrator circuits implemented in this F# module, each input x[i] is an input bitvector that is the concatenation of a message x[i][0..q-1] with q bits, a valid bit x[i][q], and a destination address x[i][q+1..q+k] such that x[i][q+k] is the most significant bit of the destination address. Clearly, we have k=log2(x.Length). Also, all the concentrators concentrate the inputs according to the most significant bit x[i][q+k-1] and may or may not remove this bit during or after the concentration which is determined by the input parameter rmMSB. For radix-based sorting/routing, it is required to remove the msb, but if HalfCleanerOpt is applied, it has to be retained for the latter.

sortGen : bool -> BoolExpr list list -> BoolExpr list list
rmMSB : bool
x : BoolExpr list list
Returns: BoolExpr list list
 TernarySeqSorter sortGen rmMSB x 
Full Usage: TernarySeqSorter sortGen rmMSB x

Parameters:
sortGen : bool -> BoolExpr list list -> BoolExpr list list
rmMSB : bool
x : BoolExpr list list

Returns: BoolExpr list list

This function (TRS) constructs a sorter for ternary inputs using two binary sorters generated by sortGen. The two binary sorters are thereby put in sequence as shown below where the first sorter sorts the inputs according to their validity, i.e., it maps 0 and 1 to 1, and ⊥ to 0. After that, an input sequence {⊥}^j{0,1}^i is obtained that is then reversed so that a sequence of the form {0,1}^i{⊥}^j is given to the second sorter. The second sorter maps 0, and ⊥ to 0, and 1 to 1 so that the 1s must move through the ⊥s to abtain a sorted sequence 0^i ⊥^j 1^k.

As for all the concentrator circuits implemented in this F# module, each input x[i] is an input bitvector that is the concatenation of a message x[i][0..q-1] with q bits, a valid bit x[i][q], and a destination address x[i][q+1..q+k] such that x[i][q+k] is the most significant bit of the destination address. Clearly, we have k=log2(x.Length). Also, all the concentrators concentrate the inputs according to the most significant bit x[i][q+k-1] and may or may not remove this bit during or after the concentration which is determined by the input parameter rmMSB. For radix-based sorting/routing, it is required to remove the msb, but if HalfCleanerOpt is applied, it has to be retained for the latter. CAUTION: This work correctly for JaSJ17, KoOr90 and Nara94, but not for Batc68, ChCh96 and ChOr94 since it is required that the second sorter will not modify the relative positions of the inputs 0 and ⊥ even though both are viewed as 0.

sortGen : bool -> BoolExpr list list -> BoolExpr list list
rmMSB : bool
x : BoolExpr list list
Returns: BoolExpr list list
 VerifyCircuits circuitList n m 
Full Usage: VerifyCircuits circuitList n m

Parameters:
circuitList : seq<string * (bool list -> bool list -> bool list -> bool) * (BoolExpr list -> BoolExpr list -> BoolExpr list)>
n : int
m : int

Returns: (string * (bool list * bool list * bool list) list) list

verify all circuits in the given list for the given size

circuitList : seq<string * (bool list -> bool list -> bool list -> bool) * (BoolExpr list -> BoolExpr list -> BoolExpr list)>
n : int
m : int
Returns: (string * (bool list * bool list * bool list) list) list
 ZeroExtend x1 x2 
Full Usage: ZeroExtend x1 x2

Parameters:
x1 : BoolExpr list
x2 : BoolExpr list

Returns: BoolExpr list * BoolExpr list

zero-extend the shorter list so that they have equal length

x1 : BoolExpr list
x2 : BoolExpr list
Returns: BoolExpr list * BoolExpr list
 circuitList 
Full Usage: circuitList

Returns: (string * (bool list -> bool list -> bool list -> bool) * (BoolExpr list -> BoolExpr list -> BoolExpr list)) list

Returns: (string * (bool list -> bool list -> bool list -> bool) * (BoolExpr list -> BoolExpr list -> BoolExpr list)) list
 parPrefixForBitBlast 
Full Usage: parPrefixForBitBlast

Returns: ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> seq<BoolExpr * BoolExpr>

Returns: ((BoolExpr * BoolExpr) * (BoolExpr * BoolExpr) -> BoolExpr * BoolExpr) -> (BoolExpr * BoolExpr) list -> seq<BoolExpr * BoolExpr>