/**CFile*********************************************************************** FileName [AigNode.c] PackageName [Aig] Synopsis [Routines to access node data structure of the And/Inverter graph.] Author [Mohammad Awedh, HoonSang Jin] Copyright [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] ******************************************************************************/ #include "aig.h" #include "aigInt.h" static char rcsid[] UNUSED = "$Id: aigNode.c,v 1.2 2009-04-10 16:33:36 hhkim Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static void connectOutput(Aig_Manager_t *bm, AigEdge_t from, AigEdge_t to, int inputIndex); static AigEdge_t HashTableLookup(Aig_Manager_t *bm, AigEdge_t node1, AigEdge_t node2); static int HashTableAdd(Aig_Manager_t *bm, AigEdge_t nodeIndexParent, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2); /* static int HashTableDelete(Aig_Manager_t *bm, AigEdge_t node); */ /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Read Node's name.] Description [Read the name of a node given its index.] SideEffects [] SeeAlso [] ******************************************************************************/ nameType_t * Aig_NodeReadName( Aig_Manager_t *bm, AigEdge_t node) { return bm->nameList[AigNodeID(node)]; } /**Function******************************************************************** Synopsis [Set Node's name.] Description [Set the name of node in Symbol table and name List] SideEffects [] SeeAlso [] ******************************************************************************/ void Aig_NodeSetName( Aig_Manager_t *bm, AigEdge_t node, nameType_t *name) { nameType_t *tmpName = bm->nameList[AigNodeID(node)]; FREE(tmpName); st_insert(bm->SymbolTable, name, (char*) (long) node); bm->nameList[AigNodeID(node)] = name; } /**Function******************************************************************** Synopsis [Returns the index of the right node.] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ int Aig_NodeReadIndexOfRightChild( Aig_Manager_t *bm, AigEdge_t nodeIndex) { return rightChild(nodeIndex); } /**Function******************************************************************** Synopsis [Returns the index of the left node.] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_NodeReadIndexOfLeftChild( Aig_Manager_t *bm, AigEdge_t nodeIndex) { return leftChild(nodeIndex); } /**Function******************************************************************** Synopsis [Get canonical node of given node.] Description [This function find node index that is functionally equivalent with given node index.] SideEffects [] SeeAlso [] ******************************************************************************/ #if 1 AigEdge_t Aig_GetCanonical( Aig_Manager_t *bm, AigEdge_t nodeIndex) { AigEdge_t next; /* Bing */ if(nodeIndex == Aig_NULL|| nodeIndex == Aig_One || nodeIndex == Aig_Zero) return(nodeIndex); while(AigGetPassFlag(bm, nodeIndex)) { next = canonical(nodeIndex); if(Aig_IsInverted(nodeIndex)) next = Aig_Not(next); nodeIndex = next; } return(nodeIndex); } #endif /**Function******************************************************************** Synopsis [Merge two functionally equivalent node.] Description [This function merges the equivalent two nodes. ] SideEffects [] SeeAlso [] ******************************************************************************/ /** int Aig_Merge( Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2) { AigEdge_t newNodeIndex, nodeIndex, tnodeIndex; AigEdge_t leftIndex, rightIndex; AigEdge_t outIndex, *pfan; int id1, id2; AigEdge_t cur; bdd_t **bddArray; array_t *nodeArray; int i, ii, iii; long *ManagerNodesArray; nodeIndex1 = Aig_GetCanonical(bm, nodeIndex1); nodeIndex2 = Aig_GetCanonical(bm, nodeIndex2); if(nodeIndex1 == nodeIndex2) return(nodeIndex1); ManagerNodesArray = bm->NodesArray; newNodeIndex = nodeIndex1; if (Aig_NonInvertedEdge(nodeIndex1) > Aig_NonInvertedEdge(nodeIndex2)){ nodeIndex1 = nodeIndex2; nodeIndex2 = newNodeIndex; } if(Aig_IsInverted(nodeIndex2)) { nodeIndex1 = Aig_Not(nodeIndex1); nodeIndex2 = Aig_Not(nodeIndex2); } nodeArray = array_alloc(AigEdge_t, 0); nodeIndex = nodeIndex2; array_insert_last(AigEdge_t, nodeArray, nodeIndex); while(Aig_NonInvertedEdge(canonical(nodeIndex)) != Aig_NonInvertedEdge(nodeIndex2)){ if(Aig_IsInverted(nodeIndex)) nodeIndex = Aig_Not(canonical(nodeIndex)); else nodeIndex = canonical(nodeIndex); array_insert_last(AigEdge_t, nodeArray, nodeIndex); } AigSetPassFlag(bm, nodeIndex2); nodeIndex = nodeIndex1; while(Aig_NonInvertedEdge(canonical(nodeIndex)) != Aig_NonInvertedEdge(nodeIndex1)) { if(Aig_IsInverted(nodeIndex)) nodeIndex = Aig_Not(canonical(nodeIndex)); else nodeIndex = canonical(nodeIndex); } for(i=0; i> 1; cur = Aig_NonInvertedEdge(cur); array_insert_last(AigEdge_t, nodeArray, cur); } for(i=0; ibddArray; id1 = AigNodeID(nodeIndex1); id2 = AigNodeID(nodeIndex2); if(bddArray[id1] == 0 && bddArray[id2]){ if(Aig_IsInverted(nodeIndex2)) { if(Aig_IsInverted(nodeIndex1)) { bddArray[id1] = bdd_dup(bddArray[id2]); } else { bddArray[id1] = bdd_not(bddArray[id2]); } } else { if(Aig_IsInverted(nodeIndex1)) { bddArray[id1] = bdd_not(bddArray[id2]); } else { bddArray[id1] = bdd_dup(bddArray[id2]); } } } return(nodeIndex1); } **/ /**Function******************************************************************** Synopsis [Print node information.] Description [Print node information.] SideEffects [] SeeAlso [] ******************************************************************************/ void Aig_PrintNode( Aig_Manager_t *bm, AigEdge_t i) { int j, size; long cur, *pfan; fprintf(stdout, "nodeIndex : %ld (%ld)\n", i, AigNodeID(i)); fprintf(stdout, "child : %ld%c, %ld%c\n", Aig_NonInvertedEdge(leftChild(i)), Aig_IsInverted(leftChild(i)) ? '\'' : ' ', Aig_NonInvertedEdge(rightChild(i)), Aig_IsInverted(rightChild(i)) ? '\'' : ' '); fprintf(stdout, "refCount : %ld\n", nFanout(i)); fprintf(stdout, " : "); size = nFanout(i); for(j=0, pfan = (AigEdge_t *)fanout(i); j> 1; fprintf(stdout, " %ld", cur); } fprintf(stdout, "\n"); fprintf(stdout, "next : %ld\n", aig_next(i)); fflush(stdout); } /**Function******************************************************************** Synopsis [Performs the Logical AND of two nodes.] Description [This function performs the Logical AND of two nodes. The inputs are the indices of the two nodes. This function returns the index of the result node.] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_And( Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2) { AigEdge_t newNodeIndex; nodeIndex1 = Aig_GetCanonical(bm, nodeIndex1); nodeIndex2 = Aig_GetCanonical(bm, nodeIndex2); newNodeIndex = nodeIndex1; /* The left node has the smallest index */ if (Aig_NonInvertedEdge(nodeIndex1) > Aig_NonInvertedEdge(nodeIndex2)){ nodeIndex1 = nodeIndex2; nodeIndex2 = newNodeIndex; } if ( nodeIndex2 == Aig_Zero ) { return Aig_Zero; } if ( nodeIndex1 == Aig_Zero ) { return Aig_Zero; } if ( nodeIndex2 == Aig_One ) { return nodeIndex1; } if ( nodeIndex1 == Aig_One ) { return nodeIndex2; } if ( nodeIndex1 == nodeIndex2 ) { return nodeIndex1; } if ( nodeIndex1 == Aig_Not(nodeIndex2) ) { return Aig_Zero; } /* Look for the new node in the Hash table */ newNodeIndex = HashTableLookup(bm, nodeIndex1, nodeIndex2); if (newNodeIndex == Aig_NULL){ if(AigIsVar(bm, nodeIndex1) && AigIsVar(bm, nodeIndex2)) newNodeIndex = Aig_And2(bm, nodeIndex1, nodeIndex2); else if(AigIsVar(bm, nodeIndex1)) newNodeIndex = Aig_And3(bm, nodeIndex1, nodeIndex2); else if(AigIsVar(bm, nodeIndex2)) newNodeIndex = Aig_And3(bm, nodeIndex2, nodeIndex1); else { newNodeIndex = Aig_And4(bm, nodeIndex1, nodeIndex2); } } return newNodeIndex; } /**Function******************************************************************** Synopsis [Structural hashing for and2] Description [Structural hashing for and2] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_And2( Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2) { AigEdge_t newNodeIndex; nodeIndex1 = Aig_GetCanonical(bm, nodeIndex1); nodeIndex2 = Aig_GetCanonical(bm, nodeIndex2); newNodeIndex = nodeIndex1; /* The left node has the smallest index */ if (Aig_NonInvertedEdge(nodeIndex1) > Aig_NonInvertedEdge(nodeIndex2)){ nodeIndex1 = nodeIndex2; nodeIndex2 = newNodeIndex; } if ( nodeIndex2 == Aig_Zero ) { return Aig_Zero; } if ( nodeIndex1 == Aig_Zero ) { return Aig_Zero; } if ( nodeIndex2 == Aig_One ) { return nodeIndex1; } if ( nodeIndex1 == Aig_One ) { return nodeIndex2; } if ( nodeIndex1 == nodeIndex2 ) { return nodeIndex1; } if ( nodeIndex1 == Aig_Not(nodeIndex2) ) { return Aig_Zero; } newNodeIndex = HashTableLookup(bm, nodeIndex1, nodeIndex2); if (newNodeIndex == Aig_NULL){ newNodeIndex = AigCreateAndNode(bm, nodeIndex1, nodeIndex2) ; HashTableAdd(bm, newNodeIndex, nodeIndex1, nodeIndex2); connectOutput(bm, nodeIndex1, newNodeIndex, 0); connectOutput(bm, nodeIndex2, newNodeIndex, 1); #if 0 #ifdef LEARNING_ tNodeIndex = HashTableLookup(bm, Aig_Not(nodeIndex1), nodeIndex2); if(tNodeIndex) Aig_Learn(bm, nodeIndex1, nodeIndex2); tNodeIndex = HashTableLookup(bm, nodeIndex1, Aig_Not(nodeIndex2)); if(tNodeIndex) Aig_Learn(bm, nodeIndex2, nodeIndex1); #endif #endif } return newNodeIndex; } /**Function******************************************************************** Synopsis [Performs the Logical AND of multiple nodes.] Description [This function performs the Logical AND of multiple nodes. The input is the array of the node indices. This function returns the index of the result node.] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_AndsInBFSManner( Aig_Manager_t *bm, array_t * nodeIndexArray) { AigEdge_t nodeIndex1, nodeIndex2, nodeIndex3, newNodeIndex; array_t * tmpNodeIndexArray; int i; nodeIndex1 = 0; nodeIndex2 = 0; nodeIndex3 = 0; newNodeIndex = 0; tmpNodeIndexArray = array_alloc(AigEdge_t, nodeIndexArray->num/2 + 1); if (nodeIndexArray->num == 1) { newNodeIndex = array_fetch(AigEdge_t, nodeIndexArray, 0); array_free(tmpNodeIndexArray); return newNodeIndex; } else if (nodeIndexArray->num == 0) { array_free(tmpNodeIndexArray); return Aig_NULL; } for(i = 0; i < nodeIndexArray->num; i=i+2) { nodeIndex1 = array_fetch(AigEdge_t, nodeIndexArray, i); if (i < nodeIndexArray->num-1) { nodeIndex2 = array_fetch(AigEdge_t, nodeIndexArray, i+1); nodeIndex3 = Aig_And(bm, nodeIndex1, nodeIndex2); } else nodeIndex3 = nodeIndex1; array_insert_last(AigEdge_t, tmpNodeIndexArray, nodeIndex3); } if (tmpNodeIndexArray->num > 1) newNodeIndex = Aig_AndsInBFSManner(bm, tmpNodeIndexArray); else newNodeIndex = nodeIndex3; array_free(tmpNodeIndexArray); return newNodeIndex; } /**Function******************************************************************** Synopsis [Performs the Logical OR of two nodes.] Description [This function performs the Logical OR of two nodes. The inputs are the indices of the two nodes. This function returns the index of the result node.] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_Or( Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2) { AigEdge_t NotNodeIndex1; AigEdge_t NotNodeIndex2; AigEdge_t AndNodeIndex; AigEdge_t NotNodeIndex; NotNodeIndex1 = Aig_Not(nodeIndex1); NotNodeIndex2 = Aig_Not(nodeIndex2); AndNodeIndex = Aig_And(bm, NotNodeIndex1, NotNodeIndex2); NotNodeIndex = Aig_Not(AndNodeIndex); return NotNodeIndex; } /**Function******************************************************************** Synopsis [Performs the Logical OR of multiple nodes.] Description [This function performs the Logical OR of multiple nodes. The input is the array of the node indices. This function returns the index of the result node.] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_OrsInBFSManner( Aig_Manager_t *bm, array_t * nodeIndexArray) { int i; AigEdge_t nodeIndex1, nodeIndex2, nodeIndex3, newNodeIndex; array_t * tmpNodeIndexArray; nodeIndex1 = 0; nodeIndex2 = 0; nodeIndex3 = 0; newNodeIndex = 0; tmpNodeIndexArray = array_alloc(AigEdge_t, nodeIndexArray->num/2 + 1); if (nodeIndexArray->num == 1) { newNodeIndex = array_fetch(AigEdge_t, nodeIndexArray, 0); array_free(tmpNodeIndexArray); return newNodeIndex; } else if (nodeIndexArray->num == 0) { array_free(tmpNodeIndexArray); return Aig_NULL; } for(i = 0; i < nodeIndexArray->num; i=i+2) { nodeIndex1 = array_fetch(AigEdge_t, nodeIndexArray, i); if (i < nodeIndexArray->num-1) { nodeIndex2 = array_fetch(AigEdge_t, nodeIndexArray, i+1); nodeIndex3 = Aig_Or(bm, nodeIndex1, nodeIndex2); } else nodeIndex3 = nodeIndex1; array_insert_last(AigEdge_t, tmpNodeIndexArray, nodeIndex3); } if (tmpNodeIndexArray->num > 1) newNodeIndex = Aig_OrsInBFSManner(bm, tmpNodeIndexArray); else newNodeIndex = nodeIndex3; array_free(tmpNodeIndexArray); return newNodeIndex; } /**Function******************************************************************** Synopsis [Performs the Logical XOR of two nodes.] Description [This function performs the Logical XOR of two nodes. The inputs are the indices of the two nodes. This function returns the index of the result node.] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_Xor( Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2) { AigEdge_t NotNodeIndex1; AigEdge_t NotNodeIndex2; AigEdge_t AndNodeIndex1; AigEdge_t AndNodeIndex2; AigEdge_t OrNodeIndex; NotNodeIndex1 = Aig_Not(nodeIndex1); NotNodeIndex2 = Aig_Not(nodeIndex2); AndNodeIndex1 = Aig_And(bm, nodeIndex1, NotNodeIndex2); AndNodeIndex2 = Aig_And(bm, NotNodeIndex1, nodeIndex2); OrNodeIndex = Aig_Or(bm, AndNodeIndex1, AndNodeIndex2); return OrNodeIndex; } /**Function******************************************************************** Synopsis [Performs the Logical Equal ( <--> XNOR) of two nodes.] Description [This function performs the Logical XNOR of two nodes. The inputs are the indices of the two nodes. This function returns the index of the result node.] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_Eq( Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2) { return Aig_Not( Aig_Xor(bm, nodeIndex1, nodeIndex2) ); } /**Function******************************************************************** Synopsis [Performs the Logical Then (--> Implies) of two nodes.] Description [This function performs the Logical Implies of two nodes. The inputs are the indices of the two nodes. This function returns the index of the result node.] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_Then( Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2) { return Aig_Or(bm, Aig_Not(nodeIndex1), nodeIndex2); } /**Function******************************************************************** Synopsis [Performs the Logical nand of two nodes.] Description [This function performs the Logical NAND of two nodes. The inputs are the indices of the two nodes. This function returns the index of the result node.] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_Nand( Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2) { return Aig_Not( Aig_And(bm, nodeIndex1, nodeIndex2) ); } /**Function******************************************************************** Synopsis [Performs the Logical ITE of three nodes.] Description [This function performs the Logical ITE of three nodes. The inputs are the indices of the three nodes. This function returns the index of the result node.] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_Ite( Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2, AigEdge_t nodeIndex3) { AigEdge_t rIndex, nodeIndex4, nodeIndex5; nodeIndex4 = Aig_Then(bm, nodeIndex1, nodeIndex2); nodeIndex5 = Aig_Or(bm, nodeIndex1, nodeIndex3); rIndex = Aig_And(bm, nodeIndex4, nodeIndex5); return rIndex; } /**Function******************************************************************** Synopsis [Generates a Aig for the function x - y ≥ c.] Description [This function generates a Aig for the function x -y ≥ c. Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. The BDD is built bottom-up. It has a linear number of nodes if the variables are ordered as follows: x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].] SideEffects [None] SeeAlso [] ******************************************************************************/ #if 0 AigEdge_t Aig_Inequality( Aig_Manager_t *bm, int N /* number of x and y variables */, int c /* right-hand side constant */, AigEdge_t *x /* array of x variables */, AigEdge_t *y /* array of y variables */) { /* The nodes at level i represent values of the difference that are ** multiples of 2^i. We use variables with names starting with k ** to denote the multipliers of 2^i in such multiples. */ int kTrue = c; int kFalse = c - 1; /* Mask used to compute the ceiling function. Since we divide by 2^i, ** we want to know whether the dividend is a multiple of 2^i. If it is, ** then ceiling and floor coincide; otherwise, they differ by one. */ int mask = 1; int i; AigEdge_t f = Aig_NULL; /* the eventual result */ /* Two x-labeled nodes are created at most at each iteration. They are ** stored, along with their k values, in these variables. At each level, ** the old nodes are freed and the new nodes are copied into the old map. */ AigEdge_t map[2]; int invalidIndex = (1 << N)-1; int index[2] = {invalidIndex, invalidIndex}; /* This should never happen. */ if (N < 0) return(Aig_NULL); /* If there are no bits, both operands are 0. The result depends on c. */ if (N == 0) { if (c >= 0) return(Aig_One); else return(Aig_Zero); } /* The maximum or the minimum difference comparing to c can generate the terminal case */ if ((1 << N) - 1 < c) return(Aig_Zero); else if ((-(1 << N) + 1) >= c) return(Aig_One); /* Build the result bottom up. */ for (i = 1; i <= N; i++) { int kTrueLower, kFalseLower; int leftChild, middleChild, rightChild; AigEdge_t g0, g1, fplus, fequal, fminus; int j; AigEdge_t newMap[2]; int newIndex[2]; kTrueLower = kTrue; /** 2, **/ kFalseLower = kFalse; /** 1, **/ /* kTrue = ceiling((c-1)/2^i) + 1 */ kTrue = ((c-1) >> i) + ((c & mask) != 1) + 1; /** 2, **/ mask = (mask << 1) | 1; /** 0x11, **/ /* kFalse = floor(c/2^i) - 1 */ kFalse = (c >> i) - 1; /** 0, **/ newIndex[0] = invalidIndex; newIndex[1] = invalidIndex; for (j = kFalse + 1; j < kTrue; j++) { /* Skip if node is not reachable from top of AIG. */ if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue; /* Find f- */ leftChild = (j << 1) - 1; if (leftChild >= kTrueLower) { fminus = Aig_One; } else if (leftChild <= kFalseLower) { fminus = Aig_Zero; } else { assert(leftChild == index[0] || leftChild == index[1]); if (leftChild == index[0]) { fminus = map[0]; } else { fminus = map[1]; } } /* Find f= */ middleChild = j << 1; if (middleChild >= kTrueLower) { fequal = Aig_One; } else if (middleChild <= kFalseLower) { fequal = Aig_Zero; } else { assert(middleChild == index[0] || middleChild == index[1]); if (middleChild == index[0]) { fequal = map[0]; } else { fequal = map[1]; } } /* Find f+ */ rightChild = (j << 1) + 1; if (rightChild >= kTrueLower) { fplus = Aig_One; } else if (rightChild <= kFalseLower) { fplus = Aig_Zero; } else { assert(rightChild == index[0] || rightChild == index[1]); if (rightChild == index[0]) { fplus = map[0]; } else { fplus = map[1]; } } /* Build new nodes. */ g1 = Aig_Ite(bm, y[N - i], fequal, fplus); if (g1 == Aig_NULL) return(Aig_NULL); g0 = Aig_Ite(bm, y[N - i], fminus, fequal); if (g0 == Aig_NULL) return(Aig_NULL); f = Aig_Ite(bm, x[N - i], g1, g0); if (f == Aig_NULL) return(Aig_NULL); /* Save newly computed node in map. */ assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex); if (newIndex[0] == invalidIndex) { newIndex[0] = j; newMap[0] = f; } else { newIndex[1] = j; newMap[1] = f; } } /* Copy new map to map. */ map[0] = newMap[0]; map[1] = newMap[1]; index[0] = newIndex[0]; index[1] = newIndex[1]; } return(f); } /* end of Aig_Inequality */ #endif AigEdge_t Aig_Inequality( Aig_Manager_t *bm, int N /* number of x and y variables */, int nx /* number of x variables */, int ny /* number of y variables */, int c /* right-hand side constant */, AigEdge_t *x /* array of x variables */, AigEdge_t *y /* array of y variables */) { /* The nodes at level i represent values of the difference that are ** multiples of 2^i. We use variables with names starting with k ** to denote the multipliers of 2^i in such multiples. */ int kTrue = c; int kFalse = c - 1; /* Mask used to compute the ceiling function. Since we divide by 2^i, ** we want to know whether the dividend is a multiple of 2^i. If it is, ** then ceiling and floor coincide; otherwise, they differ by one. */ int mask = 1; int i; AigEdge_t f = Aig_NULL; /* the eventual result */ /* Two x-labeled nodes are created at most at each iteration. They are ** stored, along with their k values, in these variables. At each level, ** the old nodes are freed and the new nodes are copied into the old map. */ AigEdge_t map[2]; int invalidIndex = (1 << N)-1; int index[2] = {invalidIndex, invalidIndex}; int kTrueLower, kFalseLower; int leftChild, middleChild, rightChild; AigEdge_t g0, g1, fplus, fequal, fminus; int j; AigEdge_t newMap[2]; int newIndex[2]; map[0] = 0; map[1] = 0; newMap[0] = 0; newMap[1] = 0; /* This should never happen. */ if (N < 0) return(Aig_NULL); /* If there are no bits, both operands are 0. The result depends on c. */ if (N == 0) { if (c >= 0) return(Aig_One); else return(Aig_Zero); } /* The maximum or the minimum difference comparing to c can generate the terminal case */ if ((1 << N) - 1 < c) return(Aig_Zero); else if ((-(1 << N) + 1) >= c) return(Aig_One); /* Build the result bottom up. */ for (i = 1; i <= N; i++) { kTrueLower = kTrue; /** 2, **/ kFalseLower = kFalse; /** 1, **/ /* kTrue = ceiling((c-1)/2^i) + 1 */ kTrue = ((c-1) >> i) + ((c & mask) != 1) + 1; /** 2, **/ mask = (mask << 1) | 1; /** 0x11, **/ /* kFalse = floor(c/2^i) - 1 */ kFalse = (c >> i) - 1; /** 0, **/ newIndex[0] = invalidIndex; newIndex[1] = invalidIndex; for (j = kFalse + 1; j < kTrue; j++) { /* Skip if node is not reachable from top of AIG. */ if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue; /* Find f- */ leftChild = (j << 1) - 1; if (leftChild >= kTrueLower) { fminus = Aig_One; } else if (leftChild <= kFalseLower) { fminus = Aig_Zero; } else { assert(leftChild == index[0] || leftChild == index[1]); if (leftChild == index[0]) { fminus = map[0]; } else { fminus = map[1]; } } /* Find f= */ middleChild = j << 1; if (middleChild >= kTrueLower) { fequal = Aig_One; } else if (middleChild <= kFalseLower) { fequal = Aig_Zero; } else { assert(middleChild == index[0] || middleChild == index[1]); if (middleChild == index[0]) { fequal = map[0]; } else { fequal = map[1]; } } /* Find f+ */ rightChild = (j << 1) + 1; if (rightChild >= kTrueLower) { fplus = Aig_One; } else if (rightChild <= kFalseLower) { fplus = Aig_Zero; } else { assert(rightChild == index[0] || rightChild == index[1]); if (rightChild == index[0]) { fplus = map[0]; } else { fplus = map[1]; } } /* Build new nodes. */ if (i > ny) g1 = fplus; else g1 = Aig_Ite(bm, y[i-1], fequal, fplus); if (g1 == Aig_NULL) return(Aig_NULL); if (i > ny) g0 = fequal; else g0 = Aig_Ite(bm, y[i-1], fminus, fequal); if (g0 == Aig_NULL) return(Aig_NULL); if (i > nx) f = g0; else f = Aig_Ite(bm, x[i-1], g1, g0); if (f == Aig_NULL) return(Aig_NULL); /* Save newly computed node in map. */ assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex); if (newIndex[0] == invalidIndex) { newIndex[0] = j; newMap[0] = f; } else { newIndex[1] = j; newMap[1] = f; } } /* Copy new map to map. */ map[0] = newMap[0]; map[1] = newMap[1]; index[0] = newIndex[0]; index[1] = newIndex[1]; } return(f); } /* end of Aig_Inequality */ /**Function******************************************************************** Synopsis [Generates a AIG for the function x - y = c.] Description [This function generates a AIG for the function x -y = c. Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. The AIG is built bottom-up. It has a linear number of nodes if the variables are ordered as follows: x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].] SideEffects [None] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_Equality( Aig_Manager_t *bm, int N /* number of max variables */, int nx /* number of x variables */, int ny /* number of y variables */, int c /* right-hand side constant */, AigEdge_t *x /* array of x variables */, AigEdge_t *y /* array of y variables */) { /* The nodes at level i represent values of the difference that are ** multiples of 2^i. We use variables with names starting with k ** to denote the multipliers of 2^i in such multiples. */ int kTrueLb = c + 1; int kTrueUb = c - 1; int kTrue = c; /* Mask used to compute the ceiling function. Since we divide by 2^i, ** we want to know whether the dividend is a multiple of 2^i. If it is, ** then ceiling and floor coincide; otherwise, they differ by one. */ int mask = 1; int i; AigEdge_t f = Aig_NULL; /* the eventual result */ /* Two x-labeled nodes are created at most at each iteration. They are ** stored, along with their k values, in these variables. At each level, ** the old nodes are freed and the new nodes are copied into the old map. */ AigEdge_t map[2]; int invalidIndex = (1 << N)-1; int index[2] = {invalidIndex, invalidIndex}; int kTrueLbLower, kTrueUbLower; int leftChild, middleChild, rightChild; AigEdge_t g0, g1, fplus, fequal, fminus; int j; AigEdge_t newMap[2]; int newIndex[2]; map[0] = 0; map[1] = 0; newMap[0] = 0; newMap[1] = 0; /* This should never happen. */ if (N < 0) return(Aig_NULL); /* If there are no bits, both operands are 0. The result depends on c. */ if (N == 0) { if (c != 0) return(Aig_Zero); else return(Aig_One); } /* The maximum or the minimum difference comparing to c can generate the terminal case */ if ((1 << N) - 1 < c || (-(1 << N) + 1) > c) return(Aig_Zero); /* Build the result bottom up. */ for (i = 1; i <= N; i++) { kTrueLbLower = kTrueLb; kTrueUbLower = kTrueUb; /* kTrueLb = floor((c-1)/2^i) + 2 */ kTrueLb = ((c-1) >> i) + 2; /* kTrueUb = ceiling((c+1)/2^i) - 2 */ kTrueUb = ((c+1) >> i) + (((c+2) & mask) != 1) - 2; mask = (mask << 1) | 1; newIndex[0] = invalidIndex; newIndex[1] = invalidIndex; for (j = kTrueUb + 1; j < kTrueLb; j++) { /* Skip if node is not reachable from top of AIG. */ if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue; /* Find f- */ leftChild = (j << 1) - 1; if (leftChild >= kTrueLbLower || leftChild <= kTrueUbLower) { fminus = Aig_Zero; } else if (i == 1 && leftChild == kTrue) { fminus = Aig_One; } else { assert(leftChild == index[0] || leftChild == index[1]); if (leftChild == index[0]) { fminus = map[0]; } else { fminus = map[1]; } } /* Find f= */ middleChild = j << 1; if (middleChild >= kTrueLbLower || middleChild <= kTrueUbLower) { fequal = Aig_Zero; } else if (i == 1 && middleChild == kTrue) { fequal = Aig_One; } else { assert(middleChild == index[0] || middleChild == index[1]); if (middleChild == index[0]) { fequal = map[0]; } else { fequal = map[1]; } } /* Find f+ */ rightChild = (j << 1) + 1; if (rightChild >= kTrueLbLower || rightChild <= kTrueUbLower) { fplus = Aig_Zero; } else if (i == 1 && rightChild == kTrue) { fplus = Aig_One; } else { assert(rightChild == index[0] || rightChild == index[1]); if (rightChild == index[0]) { fplus = map[0]; } else { fplus = map[1]; } } /* Build new nodes. */ if (i > ny) g1 = fplus; else { g1 = Aig_Ite(bm, y[i-1], fequal, fplus); } if (g1 == Aig_NULL) return(Aig_NULL); if (i > ny) g0 = fequal; else { g0 = Aig_Ite(bm, y[i-1], fminus, fequal); } if (g0 == Aig_NULL) return(Aig_NULL); if (i > nx) /* number of bits in x is less than N */ f = g0; /* x[N - i] is false */ else { f = Aig_Ite(bm, x[i-1], g1, g0); } if (f == Aig_NULL) return(Aig_NULL); /* Save newly computed node in map. */ assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex); if (newIndex[0] == invalidIndex) { newIndex[0] = j; newMap[0] = f; } else { newIndex[1] = j; newMap[1] = f; } } /* Copy new map to map. */ map[0] = newMap[0]; map[1] = newMap[1]; index[0] = newIndex[0]; index[1] = newIndex[1]; } return(f); } /* end of Aig_Equality */ /**Function******************************************************************** Synopsis [Generates a AIG for the function x - y != c.] Description [This function generates a AIG for the function x -y != c. Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. The BDD is built bottom-up. It has a linear number of nodes if the variables are ordered as follows: x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].] SideEffects [None] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_Disequality( Aig_Manager_t *bm, int N /* number of x and y variables */, int c /* right-hand side constant */, AigEdge_t *x /* array of x variables */, AigEdge_t *y /* array of y variables */) { /* The nodes at level i represent values of the difference that are ** multiples of 2^i. We use variables with names starting with k ** to denote the multipliers of 2^i in such multiples. */ int kTrueLb = c + 1; int kTrueUb = c - 1; int kFalse = c; /* Mask used to compute the ceiling function. Since we divide by 2^i, ** we want to know whether the dividend is a multiple of 2^i. If it is, ** then ceiling and floor coincide; otherwise, they differ by one. */ int mask = 1; int i; AigEdge_t f = Aig_NULL; /* the eventual result */ /* Two x-labeled nodes are created at most at each iteration. They are ** stored, along with their k values, in these variables. At each level, ** the old nodes are freed and the new nodes are copied into the old map. */ AigEdge_t map[2]; int invalidIndex = (1 << N)-1; int index[2] = {invalidIndex, invalidIndex}; int kTrueLbLower, kTrueUbLower; int leftChild, middleChild, rightChild; AigEdge_t g0, g1, fplus, fequal, fminus; int j; AigEdge_t newMap[2]; int newIndex[2]; map[0] = 0; map[1] = 0; newMap[0] = 0; newMap[1] = 0; /* This should never happen. */ if (N < 0) return(Aig_NULL); /* If there are no bits, both operands are 0. The result depends on c. */ if (N == 0) { if (c != 0) return(Aig_One); else return(Aig_Zero); } /* The maximum or the minimum difference comparing to c can generate the terminal case */ if ((1 << N) - 1 < c || (-(1 << N) + 1) > c) return(Aig_One); /* Build the result bottom up. */ for (i = 1; i <= N; i++) { kTrueLbLower = kTrueLb; kTrueUbLower = kTrueUb; /* kTrueLb = floor((c-1)/2^i) + 2 */ kTrueLb = ((c-1) >> i) + 2; /* kTrueUb = ceiling((c+1)/2^i) - 2 */ kTrueUb = ((c+1) >> i) + (((c+2) & mask) != 1) - 2; mask = (mask << 1) | 1; newIndex[0] = invalidIndex; newIndex[1] = invalidIndex; for (j = kTrueUb + 1; j < kTrueLb; j++) { /* Skip if node is not reachable from top of AIG. */ if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue; /* Find f- */ leftChild = (j << 1) - 1; if (leftChild >= kTrueLbLower || leftChild <= kTrueUbLower) { fminus = Aig_One; } else if (i == 1 && leftChild == kFalse) { fminus = Aig_Zero; } else { assert(leftChild == index[0] || leftChild == index[1]); if (leftChild == index[0]) { fminus = map[0]; } else { fminus = map[1]; } } /* Find f= */ middleChild = j << 1; if (middleChild >= kTrueLbLower || middleChild <= kTrueUbLower) { fequal = Aig_One; } else if (i == 1 && middleChild == kFalse) { fequal = Aig_Zero; } else { assert(middleChild == index[0] || middleChild == index[1]); if (middleChild == index[0]) { fequal = map[0]; } else { fequal = map[1]; } } /* Find f+ */ rightChild = (j << 1) + 1; if (rightChild >= kTrueLbLower || rightChild <= kTrueUbLower) { fplus = Aig_One; } else if (i == 1 && rightChild == kFalse) { fplus = Aig_Zero; } else { assert(rightChild == index[0] || rightChild == index[1]); if (rightChild == index[0]) { fplus = map[0]; } else { fplus = map[1]; } } /* Build new nodes. */ g1 = Aig_Ite(bm, y[N - i], fequal, fplus); if (g1 == Aig_NULL) return(Aig_NULL); g0 = Aig_Ite(bm, y[N - i], fminus, fequal); if (g0 == Aig_NULL) return(Aig_NULL); f = Aig_Ite(bm, x[N - i], g1, g0); if (f == Aig_NULL) return(Aig_NULL); /* Save newly computed node in map. */ assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex); if (newIndex[0] == invalidIndex) { newIndex[0] = j; newMap[0] = f; } else { newIndex[1] = j; newMap[1] = f; } } /* Copy new map to map. */ map[0] = newMap[0]; map[1] = newMap[1]; index[0] = newIndex[0]; index[1] = newIndex[1]; } return(f); } /* end of Aig_Disequality */ /**Function******************************************************************** Synopsis [Generates a Aig for the function lb ≤ x ≥ ub.] Description [This function generates a Aig for the function lb ≤ x ≥ ub. x is N-bit number, x\[0\] x\[1\] ... x\[N-1\] and with 0 the most significant bit. The BDD is built bottom-up. It has a linear number of nodes if the variables are ordered as follows: x\[0\] x\[1\] ... x\[N-1\].] SideEffects [None] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_Bound( Aig_Manager_t *bm, int N /* number of x variables */, int lb /* lower bound */, int ub /* upper bound */, AigEdge_t *x /* array of x variables */) { /* The nodes at level i represent values of the difference that are ** multiples of 2^i. We use variables with names starting with k ** to denote the multipliers of 2^i in such multiples. */ int kTrueLb = lb; int kTrueUb = ub; int kFalseLb = ub + 1; int kFalseUb = lb - 1; /* Mask used to compute the ceiling function. Since we divide by 2^i, ** we want to know whether the dividend is a multiple of 2^i. If it is, ** then ceiling and floor coincide; otherwise, they differ by one. */ int mask = 1; int i; AigEdge_t f = Aig_NULL; /* the eventual result */ /* Two x-labeled nodes are created at most at each iteration. They are ** stored, along with their k values, in these variables. At each level, ** the old nodes are freed and the new nodes are copied into the old map. */ AigEdge_t map[2]; int invalidIndex = (1 << N)-1; /** int invalidValue = (1 << N)-1; **/ int index[2] = {invalidIndex, invalidIndex}; int max, min; int kTrueLbLower, kTrueUbLower, kFalseLbLower, kFalseUbLower; int leftChild, rightChild; AigEdge_t f1, f0; int j; AigEdge_t newMap[2]; int newIndex[2]; map[0] = 0; map[1] = 0; newMap[0] = 0; newMap[1] = 0; /* This should never happen. */ if (N < 0) return(Aig_NULL); /* If there are no bits, both operands are 0. The result depends on c. */ if (N == 0) { if (lb <= 0 && ub >= 0) return(Aig_One); else return(Aig_Zero); } /* The maximum or the minimum difference comparing to c generates the terminal case */ { max = (1 << N) - 1; min = 0; if (max < lb || min > ub) return(Aig_Zero); else if (max <= ub && min >= lb) return(Aig_One); /* Build the result bottom up. */ for (i = 1; i <= N; i++) { kTrueLbLower = kTrueLb; kTrueUbLower = kTrueUb; kFalseLbLower = kFalseLb; kFalseUbLower = kFalseUb; /* kTrueLb = ceiling(lb/2^i) */ kTrueLb = (lb >> i) + (((lb+1) & mask) != 1); /* kTrueUb = floor((ub+1)/2^i) - 1 */ kTrueUb = ((ub+1) >> i) - 1; /* kFalseLb = ceiling((ub+1)/2^i) */ kFalseLb = ((ub+1) >> i) + (((ub+2) & mask) != 1); /* kFalseUb = floor(lb/2^i) - 1 */ kFalseUb = (lb >> i) - 1; mask = (mask << 1) | 1; newIndex[0] = invalidIndex; newIndex[1] = invalidIndex; j = kTrueUb + 1; if (j >= 0 && j < (1 << (N - i)) && j < kFalseLb) { /* Find f1 */ leftChild = (j << 1) + 1; if (leftChild >= kTrueLbLower && leftChild <= kTrueUbLower) { f1 = Aig_One; } else if (leftChild <= kFalseUbLower || leftChild >= kFalseLbLower) { f1 = Aig_Zero; } else { assert(leftChild == index[0] || leftChild == index[1]); if (leftChild == index[0]) { f1 = map[0]; } else { f1 = map[1]; } } /* Find f0 */ rightChild = j << 1; if (rightChild >= kTrueLbLower && rightChild <= kTrueUbLower) { f0 = Aig_One; } else if (rightChild <= kFalseUbLower || rightChild >= kFalseLbLower) { f0 = Aig_Zero; } else { assert(rightChild == index[0] || rightChild == index[1]); if (rightChild == index[0]) { f0 = map[0]; } else { f0 = map[1]; } } /* Build new nodes. */ f = Aig_Ite(bm, x[i-1], f1, f0); if (f == Aig_NULL) return(Aig_NULL); /* Save newly computed node in map. */ assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex); if (newIndex[0] == invalidIndex) { newIndex[0] = j; newMap[0] = f; } else { newIndex[1] = j; newMap[1] = f; } } j = kFalseUb + 1; if (kTrueUb != kFalseUb && j >= 0 && j < (1 << (N - i)) && j < kTrueLb) { /* Find f1 */ leftChild = (j << 1) + 1; if (leftChild >= kTrueLbLower && leftChild <= kTrueUbLower) { f1 = Aig_One; } else if (leftChild <= kFalseUbLower || leftChild >= kFalseLbLower) { f1 = Aig_Zero; } else { assert(leftChild == index[0] || leftChild == index[1]); if (leftChild == index[0]) { f1 = map[0]; } else { f1 = map[1]; } } /* Find f0 */ rightChild = j << 1; if (rightChild >= kTrueLbLower && rightChild <= kTrueUbLower) { f0 = Aig_One; } else if (rightChild <= kFalseUbLower || rightChild >= kFalseLbLower) { f0 = Aig_Zero; } else { assert(rightChild == index[0] || rightChild == index[1]); if (rightChild == index[0]) { f0 = map[0]; } else { f0 = map[1]; } } /* Build new nodes. */ f = Aig_Ite(bm, x[i-1], f1, f0); if (f == Aig_NULL) return(Aig_NULL); /* Save newly computed node in map. */ assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex); if (newIndex[0] == invalidIndex) { newIndex[0] = j; newMap[0] = f; } else { newIndex[1] = j; newMap[1] = f; } } /* Copy new map to map. */ map[0] = newMap[0]; map[1] = newMap[1]; index[0] = newIndex[0]; index[1] = newIndex[1]; } } return(f); } /* end of Aig_Inequality */ /**Function******************************************************************** Synopsis [create new node] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_CreateNode( Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2) { AigEdge_t newNode = bm->nodesArraySize; if (bm->nodesArraySize >= bm->maxNodesArraySize ){ bm->maxNodesArraySize = 2* bm->maxNodesArraySize; bm->NodesArray = REALLOC(AigEdge_t, bm->NodesArray, bm->maxNodesArraySize); bm->nameList = REALLOC(char *, bm->nameList , bm->maxNodesArraySize/AigNodeSize); } bm->NodesArray[Aig_NonInvertedEdge(newNode)+AigRight] = nodeIndex2; bm->NodesArray[Aig_NonInvertedEdge(newNode)+AigLeft] = nodeIndex1; aig_next(newNode) = Aig_NULL; fanout(newNode) = 0; canonical(newNode) = newNode; flags(newNode) = 0; nFanout(newNode) = 0; bm->nodesArraySize +=AigNodeSize; return(newNode); } /**Function******************************************************************** Synopsis [Return the Aig node given its name.] SideEffects [] ******************************************************************************/ AigEdge_t Aig_FindNodeByName( Aig_Manager_t *bm, nameType_t *name) { AigEdge_t node; if (!st_lookup(bm->SymbolTable, name, &node)){ node = Aig_NULL; } return Aig_GetCanonical(bm, node); } /**Function******************************************************************** Synopsis [create var node ] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_CreateVarNode( Aig_Manager_t *bm, nameType_t *name) { AigEdge_t varIndex; if (!st_lookup(bm->SymbolTable, name, &varIndex)){ varIndex = Aig_CreateNode(bm, Aig_NULL, Aig_NULL); if (varIndex == Aig_NULL){ return (varIndex); } /* Insert the varaible in the Symbol Table */ st_insert(bm->SymbolTable, name, (char*) (long) varIndex); bm->nameList[AigNodeID(varIndex)] = name; return(varIndex); } else { return (varIndex); } } /**Function******************************************************************** Synopsis [Return True if this node is Variable node] SideEffects [] ******************************************************************************/ int Aig_isVarNode( Aig_Manager_t *bm, AigEdge_t node) { if((rightChild(node) == Aig_NULL) && (leftChild(node) == Aig_NULL)) { return 1; } return 0; } /**Function******************************************************************** Synopsis [Build the binary AND/INVERTER graph for a given bdd function] SideEffects [Build the binary AND/INVERTER graph for a given bdd function. We assume that the return bdd nodes from the foreach_bdd_node are in the order from childeren to parent. i.e all the childeren nodes are returned before the parent node.] SideEffects [] SeeAlso [] ******************************************************************************/ #if 0 AigEdge_t Aig_bddToAig( Aig_Manager_t *AigManager, bdd_t *fn) { bdd_gen *gen; bdd_node *node, *thenNode, *elseNode, *funcNode; bdd_manager *bddManager = bdd_get_manager(fn); /* Used to read the variable name of a bdd node. */ array_t *mvar_list = mdd_ret_mvar_list(bddManager); array_t *bvar_list = mdd_ret_bvar_list(bddManager); bvar_type bv; mvar_type mv; bdd_node *one = bdd_read_one(bddManager); int is_complemented; int flag; AigEdge_t var, left, right, result; char name[100]; st_table *bddTOAigTable; if (fn == NULL){ return Aig_NULL; } funcNode = bdd_get_node(fn, &is_complemented); if (bdd_is_constant(funcNode)){ return (is_complemented?Aig_Zero:Aig_One); } bddTOAigTable = st_init_table(st_numcmp, st_numhash); st_insert(bddTOAigTable, (char *) (long) bdd_regular(one), (char *) Aig_One); foreach_bdd_node(fn, gen, node){ int nodeIndex = bdd_node_read_index(node); int index, rtnNodeIndex; if (bdd_is_constant(node)){ continue; } bv = array_fetch(bvar_type, bvar_list, nodeIndex); /* get the multi-valued varaible. */ mv = array_fetch(mvar_type, mvar_list, bv.mvar_id); arrayForEachItem(int, mv.bvars, index, rtnNodeIndex) { if (nodeIndex == rtnNodeIndex){ break; } } assert(index < mv.encode_length); /* printf("Name of bdd node %s %d\n", mv.name, index); */ sprintf(name, "%s_%d", mv.name, index); /* Create or Retrieve the AigEdge_t w.r.t. 'name' */ var = Aig_CreateVarNode(AigManager, util_strsav(name)); thenNode = bdd_bdd_T(node); flag = st_lookup(bddTOAigTable, (char *) (long) bdd_regular(thenNode), &left); assert(flag); elseNode = bdd_bdd_E(node); flag = st_lookup(bddTOAigTable, (char *) (long) bdd_regular(elseNode), &right); assert(flag); /* test if the elseNode is complemented arc? */ if (bdd_is_complement(elseNode)){ right = Aig_Not(right); } if (right == Aig_Zero){ /* result = var*then */ result = Aig_And(AigManager, var, left); } else if (right == Aig_One){ /* result = then + not(var) */ result = Aig_Or(AigManager, left, Aig_Not(var)); } else if (left == Aig_One) { /* result = var + else */ result = Aig_Or(AigManager, var, right); } else { /* result = var * then + not(var)*else */ result = Aig_Or(AigManager, Aig_And(AigManager, var, left), Aig_And(AigManager, Aig_Not(var), right)); } st_insert(bddTOAigTable, (char *) (long) bdd_regular(node), (char *) (long) result); } flag = st_lookup(bddTOAigTable, (char *) (long) bdd_regular(funcNode), &result); assert(flag); st_free_table(bddTOAigTable); if (is_complemented){ return Aig_Not(result); } else { return result; } } /* end of Aig_bddtoAig() */ #endif /**Function******************************************************************** Synopsis [Print dot file for AIG nodes] SideEffects [] ******************************************************************************/ int Aig_PrintDot( FILE *fp, Aig_Manager_t *bm) { long i; /* * Write out the header for the output file. */ (void) fprintf(fp, "digraph \"AndInv\" {\n rotate=90;\n"); (void) fprintf(fp, " margin=0.5;\n label=\"AndInv\";\n"); (void) fprintf(fp, " size=\"10,7.5\";\n ratio=\"fill\";\n"); for (i=AigFirstNodeIndex ; inodesArraySize ; i+=AigNodeSize){ (void) fprintf(fp,"Node%ld [label=\"%s \"];\n",i,Aig_NodeReadName(bm, i)); } for (i=AigFirstNodeIndex ; i< bm->nodesArraySize ; i+=AigNodeSize){ if (rightChild(i) != Aig_NULL){ if (Aig_IsInverted(rightChild(i))){ (void) fprintf(fp,"Node%ld -> Node%ld [color = red];\n",Aig_NonInvertedEdge(rightChild(i)), i); } else{ (void) fprintf(fp,"Node%ld -> Node%ld;\n",Aig_NonInvertedEdge(rightChild(i)), i); } if (Aig_IsInverted(leftChild(i))){ (void) fprintf(fp,"Node%ld -> Node%ld [color = red];\n",Aig_NonInvertedEdge(leftChild(i)), i); } else{ (void) fprintf(fp,"Node%ld -> Node%ld;\n",Aig_NonInvertedEdge(leftChild(i)), i); } }/* if */ }/*for */ (void) fprintf(fp, "}\n"); return 1; } /**Function******************************************************************** Synopsis [Print dot file for AIG nodes] SideEffects [] ******************************************************************************/ int Aig_PrintAIG(Aig_Manager_t *bm, AigEdge_t object, char *fileName) { FILE *fp; long nInput, nAnd; long i; char *str; str = util_strcat3(fileName, ".aag", ""); fp = fopen(str, "w"); free(str); /* count # of inputs & # of and gates */ for (i=AigFirstNodeIndex, nInput=0, nAnd=0; inodesArraySize ; i+=AigNodeSize){ if (leftChild(i)==Aig_NULL && rightChild(i)==Aig_NULL) nInput++; else nAnd++; } /* * Write out the header for the output file: * # of nodes, # of inputs, # of latches, # of outputs, # of AND gates */ (void) fprintf(fp, "aag %ld %ld 0 1 %ld\n", nInput+nAnd, nInput, nAnd); /* Input */ for (i=AigFirstNodeIndex ; inodesArraySize ; i+=AigNodeSize){ if (leftChild(i)==Aig_NULL && rightChild(i)==Aig_NULL) fprintf(fp,"%ld\n",i/4); } /* Output */ if (Aig_IsInverted(object)) fprintf(fp, "%ld\n", (Aig_NonInvertedEdge(object)/4)+1); else fprintf(fp, "%ld\n", (Aig_NonInvertedEdge(object)/4)); /* AND gates */ for (i=AigFirstNodeIndex ; i< bm->nodesArraySize ; i+=AigNodeSize){ if (leftChild(i)!=Aig_NULL || rightChild(i)!=Aig_NULL) { fprintf(fp, "%ld ", i/4); if (rightChild(i) != Aig_NULL) { if (Aig_IsInverted(rightChild(i))) fprintf(fp,"%ld ", (Aig_NonInvertedEdge(rightChild(i))/4)+1); else fprintf(fp,"%ld ", Aig_NonInvertedEdge(rightChild(i))/4); } if (leftChild(i) != Aig_NULL) { if (Aig_IsInverted(leftChild(i))) fprintf(fp,"%ld", (Aig_NonInvertedEdge(leftChild(i))/4)+1); else fprintf(fp,"%ld", Aig_NonInvertedEdge(leftChild(i))/4); } fprintf(fp, "\n"); } } fclose(fp); return 1; } /**Function******************************************************************** Synopsis [Set pass flag for node] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AigSetPassFlag( Aig_Manager_t *bm, AigEdge_t node) { flags(node) |= CanonicalBitMask; } /**Function******************************************************************** Synopsis [Reset pass flag for node] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void AigResetPassFlag( Aig_Manager_t *bm, AigEdge_t node) { flags(node) &= ResetCanonicalBitMask; } /**Function******************************************************************** Synopsis [Get pass flag for node] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ int AigGetPassFlag( Aig_Manager_t *bm, AigEdge_t node) { return((flags(node) & CanonicalBitMask) != 0); } /**Function******************************************************************** Synopsis [Create AND node and assign name to it ] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t AigCreateAndNode( Aig_Manager_t *bm, AigEdge_t node1, AigEdge_t node2) { AigEdge_t varIndex; char *name = NIL(char); char *node1Str = util_inttostr(node1); char *node2Str = util_inttostr(node2); name = util_strcat4("Nd", node1Str,"_", node2Str); while (st_lookup(bm->SymbolTable, name, &varIndex)){ printf("Find redundant node at %ld %ld\n", node1, node2); name = util_strcat3(name, node1Str, node2Str); } FREE(node1Str); FREE(node2Str); varIndex = Aig_CreateNode(bm, node1, node2); if (varIndex == Aig_NULL){ FREE(name); return (varIndex); } /* Insert the varaible in the Symbol Table */ st_insert(bm->SymbolTable, name, (char*) (long) varIndex); bm->nameList[AigNodeID(varIndex)] = name; return(varIndex); } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Connect fanin fanout of two AIG nodes] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ static void connectOutput( Aig_Manager_t *bm, AigEdge_t from, AigEdge_t to, int inputIndex) { AigEdge_t *pfan; int nfan; to = Aig_NonInvertedEdge(to); pfan = (AigEdge_t *)fanout(from); nfan = nFanout(from); if(nfan == 0) pfan = ALLOC(AigEdge_t, 2); else pfan = REALLOC(AigEdge_t, pfan, nfan+2); to += Aig_IsInverted(from); to = to << 1; to += inputIndex; pfan[nfan++] = to; pfan[nfan] = 0; fanout(from) = (long)pfan; nFanout(from) = nfan; } /**Function******************************************************************** Synopsis [disconnect fanin fanout of two AIG nodes] Description [] SideEffects [] SeeAlso [] static void unconnectOutput( Aig_Manager_t *bm, AigEdge_t from, AigEdge_t to) { AigEdge_t cur, *pfan, *newfan; int i, nfan; from = Aig_NonInvertedEdge(from); to = Aig_NonInvertedEdge(to); pfan = (AigEdge_t *)fanout(from); nfan = nFanout(from); newfan = (AigEdge_t *)malloc(sizeof(AigEdge_t)*(nfan)); for(i=0; i> 1; cur = Aig_NonInvertedEdge(cur); if(cur == to) { memcpy(newfan, pfan, sizeof(AigEdge_t)*i); memcpy(&(newfan[i]), &(pfan[i+1]), sizeof(AigEdge_t)*(nfan-i-1)); newfan[nfan-1] = 0; fanout(from) = (int)newfan; free(pfan); nFanout(from) = nfan-1; break; } } } ******************************************************************************/ /**Function******************************************************************** Synopsis [Look for the node in the Hash Table.] Description [.] SideEffects [] SeeAlso [] ******************************************************************************/ static AigEdge_t HashTableLookup( Aig_Manager_t *bm, AigEdge_t node1, AigEdge_t node2) { AigEdge_t key = HashTableFunction(node1, node2); AigEdge_t node; node = bm->HashTable[key]; if (node == Aig_NULL) { return Aig_NULL; } else{ while ( (rightChild(Aig_NonInvertedEdge(node)) != node2) || (leftChild(Aig_NonInvertedEdge(node)) != node1)) { if (aig_next(Aig_NonInvertedEdge(node)) == Aig_NULL){ return(Aig_NULL); } node = aig_next(Aig_NonInvertedEdge(node)); /* Get the next Node */ } /* While loop */ return(node); } /* If Then Else */ } /* End of HashTableLookup() */ /**Function******************************************************************** Synopsis [Add a node in the Hash Table.] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ static int HashTableAdd( Aig_Manager_t *bm, AigEdge_t nodeIndexParent, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2) { AigEdge_t key = HashTableFunction(nodeIndex1, nodeIndex2); AigEdge_t nodeIndex; AigEdge_t node; nodeIndex = bm->HashTable[key]; if (nodeIndex == Aig_NULL) { bm->HashTable[key] = nodeIndexParent; return TRUE; } else{ node = nodeIndex; nodeIndex = aig_next(Aig_NonInvertedEdge(nodeIndex)); /* Get the Node */ while (nodeIndex != Aig_NULL) { node = nodeIndex; nodeIndex = aig_next(Aig_NonInvertedEdge(nodeIndex)); } aig_next(Aig_NonInvertedEdge(node)) = nodeIndexParent; return TRUE; } } /* End of HashTableAdd() */ /**Function******************************************************************** Synopsis [Hash table delete] Description [Hash table delete] SideEffects [] SeeAlso [] ******************************************************************************/ #if 0 static int HashTableDelete( Aig_Manager_t *bm, AigEdge_t node) { AigEdge_t key = HashTableFunction(leftChild(node), rightChild(node)); AigEdge_t nodeIndex; nodeIndex = bm->HashTable[key]; if (nodeIndex == node) { bm->HashTable[key] = aig_next(node); return TRUE; } else{ while(nodeIndex && aig_next(Aig_NonInvertedEdge(nodeIndex)) != node) nodeIndex = aig_next(Aig_NonInvertedEdge(nodeIndex)); aig_next(Aig_NonInvertedEdge(nodeIndex)) = aig_next(Aig_NonInvertedEdge(aig_next(Aig_NonInvertedEdge(nodeIndex)))); return TRUE; } } /* End of HashTableAdd() */ #endif /**Function******************************************************************** Synopsis [Structural hasing for and4] Description [Structural hasing for and4] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_And4( Aig_Manager_t *bm, AigEdge_t l, AigEdge_t r) { int caseIndex, caseSig; AigEdge_t ll, lr, rl, rr; AigEdge_t t1, t2; ll = leftChild(l); lr = rightChild(l); rl = leftChild(r); rr = rightChild(r); if(AigCompareNode(l, rl) || AigCompareNode(l, rr)) { return(Aig_And3(bm, l, r)); } else if(AigCompareNode(r, ll) || AigCompareNode(r, lr)) { return(Aig_And3(bm, r, l)); } if(ll > lr+1) AigSwap(ll, lr); if(rl > rr+1) AigSwap(rl, rr); caseIndex = 0; /* (a b)(c d) */ if(AigCompareNode(ll, rl)) { if(AigCompareNode(lr, rr)) { caseIndex = 4; /* (a b) (a b) */ } else { caseIndex = 1; /* (a b) (a c) */ if(lr > rr+1) { AigSwap(ll, rl); AigSwap(lr, rr); AigSwap(l, r); } } } else if(AigCompareNode(lr, rl)) { caseIndex = 2; /* (b a)(a c) */ } else if(AigCompareNode(lr, rr)) { caseIndex = 3; /* (b a)(c a) */ if(ll > rl+1) { AigSwap(ll, rl); AigSwap(lr, rr); AigSwap(l, r); } } else if(AigCompareNode(ll, rr)) { /* (a b)(c a) */ AigSwap(ll, rl); AigSwap(lr, rr); AigSwap(l, r); caseIndex = 2; /* (c a )(a b) because of c < b */ } caseSig = 0; if(Aig_IsInverted(ll)) caseSig += 32; if(Aig_IsInverted(lr)) caseSig += 16; if(Aig_IsInverted(l)) caseSig += 8; if(Aig_IsInverted(rl)) caseSig += 4; if(Aig_IsInverted(rr)) caseSig += 2; if(Aig_IsInverted(r)) caseSig += 1; /** fprintf(stdout, "Index: %d Sig: %2d (%5d%c %5d%c)%c (%5d%c %5d%c)%c (%5d, %5d)\n", caseIndex, caseSig, Aig_NonInvertedEdge(ll), Aig_IsInverted(ll) ? '\'' : ' ', Aig_NonInvertedEdge(lr), Aig_IsInverted(lr) ? '\'' : ' ', Aig_IsInverted(l) ? '\'' : ' ', Aig_NonInvertedEdge(rl), Aig_IsInverted(rl) ? '\'' : ' ', Aig_NonInvertedEdge(rr), Aig_IsInverted(rr) ? '\'' : ' ', Aig_IsInverted(r) ? '\'' : ' ', Aig_NonInvertedEdge(l), Aig_NonInvertedEdge(r) ); **/ if(caseIndex == 0) { return(Aig_And2(bm, l, r)); } else if(caseIndex == 1) { switch(caseSig) { case 19 : case 17 : case 3 : case 1 : case 55 : case 53 : case 39 : case 37 : t1 = Aig_And(bm, lr, Aig_Not(rr)); t2 = Aig_And(bm, ll, t1); return(t2); case 18 : case 16 : case 2 : case 0 : case 54 : case 52 : case 38 : case 36 : t1 = Aig_And(bm, lr, rr); t2 = Aig_And(bm, ll, t1); return(t2); case 26 : case 24 : case 10 : case 8 : case 62 : case 60 : case 46 : case 44 : t1 = Aig_And(bm, Aig_Not(lr), rr); t2 = Aig_And(bm, ll, t1); return(t2); case 61 : case 27 : case 25 : case 11 : case 63 : case 47 : case 9 : case 45 : t1 = Aig_And(bm, Aig_Not(lr), Aig_Not(rr)); t2 = Aig_Or(bm, Aig_Not(ll), t1); return(t2); case 23 : case 21 : case 7 : case 5 : case 51 : case 49 : case 35 : case 33 : return(l); case 30 : case 28 : case 14 : case 12 : case 58 : case 56 : case 42 : case 40 : return(r); case 22 : case 20 : case 6 : case 4 : case 50 : case 48 : case 34 : case 32 : return(Aig_Zero); case 31 : case 29 : case 15 : case 13 : case 59 : case 57 : case 43 : case 41 : t1 = Aig_And2(bm, l, r); return(t1); } } else if(caseIndex == 2) { switch(caseSig) { case 35 : case 33 : case 3 : case 1 : case 55 : case 53 : case 23 : case 21 : t1 = Aig_And(bm, lr, Aig_Not(rr)); t2 = Aig_And(bm, ll, t1); return(t2); case 34 : case 32 : case 2 : case 0 : case 54 : case 52 : case 22 : case 20 : t1 = Aig_And(bm, lr, rr); t2 = Aig_And(bm, ll, t1); return(t2); case 42 : case 40 : case 10 : case 8 : case 62 : case 60 : case 30 : case 28 : t1 = Aig_And(bm, lr, rr); t2 = Aig_And(bm, Aig_Not(ll), t1); return(t2); case 43 : case 41 : case 11 : case 9 : case 63 : case 61 : case 31 : case 29 : t1 = Aig_And(bm, Aig_Not(ll), Aig_Not(rr)); t2 = Aig_Or(bm, Aig_Not(lr), t1); return(t2); case 39 : case 37 : case 7 : case 5 : case 51 : case 49 : case 19 : case 17 : return(l); case 46 : case 44 : case 14 : case 12 : case 58 : case 56 : case 26 : case 24 : return(r); case 38 : case 36 : case 6 : case 4 : case 50 : case 48 : case 18 : case 16 : return(Aig_Zero); case 45 : case 15 : case 13 : case 59 : case 57 : case 47 : case 27 : case 25 : t1 = Aig_And2(bm, l, r); return(t1); } } else if(caseIndex == 3) { switch(caseSig) { case 37 : case 33 : case 5 : case 1 : case 55 : case 51 : case 23 : case 19 : t1 = Aig_And(bm, Aig_Not(rl), lr); t2 = Aig_And(bm, ll, t1); return(t2); case 36 : case 32 : case 4 : case 0 : case 54 : case 50 : case 22 : case 18 : t1 = Aig_And(bm, rl, lr); t2 = Aig_And(bm, ll, t1); return(t2); case 44 : case 40 : case 12 : case 8 : case 62 : case 58 : case 30 : case 26 : t1 = Aig_And(bm, rl, lr); t2 = Aig_And(bm, Aig_Not(ll), t1); return(t2); case 45 : case 41 : case 13 : case 9 : case 63 : case 59 : case 31 : case 27 : t1 = Aig_And(bm, Aig_Not(ll), Aig_Not(rl)); t2 = Aig_Or(bm, Aig_Not(lr), t1); return(t2); case 39 : case 35 : case 7 : case 3 : case 53 : case 49 : case 21 : case 17 : return(l); case 46 : case 42 : case 14 : case 10 : case 60 : case 56 : case 28 : case 24 : return(r); case 38 : case 34 : case 6 : case 2 : case 52 : case 48 : case 20 : case 16 : return(Aig_Zero); case 47 : case 43 : case 15 : case 11 : case 61 : case 57 : case 29 : case 25 : t1 = Aig_And2(bm, l, r); return(t1); } } else if(caseIndex == 4) { switch(caseSig) { case 22 : case 20 : case 6 : case 4 : case 50 : case 48 : case 34 : case 32 : case 2 : case 16 : case 52 : case 1 : case 8 : case 19 : case 26 : case 37 : case 44 : case 38 : case 55 : case 62 : return(Aig_Zero); case 0 : case 18 : case 36 : case 54 : case 9 : case 27 : case 45 : case 63 : case 5 : case 23 : case 33 : case 51 : case 3 : case 17 : case 49 : case 7 : case 35 : case 21 : case 39 : case 53 : return(l); case 40 : case 58 : case 12 : case 30 : case 24 : case 10 : case 14 : case 56 : case 28 : case 42 : case 60 : case 46 : return(r); case 11 : case 47 : case 25 : case 61 : return(Aig_Not(ll)); case 41 : case 59 : case 13 : case 31 : return(Aig_Not(lr)); case 15 : t1 = Aig_And(bm, ll, Aig_Not(lr)); t2 = Aig_And(bm, Aig_Not(ll), lr); return(Aig_Not(Aig_And2(bm, Aig_Not(t1), Aig_Not(t2)))); case 57 : t1 = Aig_And(bm, rl, Aig_Not(rr)); t2 = Aig_And(bm, Aig_Not(rl), rr); return(Aig_Not(Aig_And2(bm, Aig_Not(t1), Aig_Not(t2)))); case 29 : t1 = Aig_And(bm, ll, lr); t2 = Aig_And(bm, Aig_Not(ll), Aig_Not(lr)); return((Aig_And2(bm, Aig_Not(t1), Aig_Not(t2)))); case 43 : t1 = Aig_And(bm, rl, rr); t2 = Aig_And(bm, Aig_Not(rl), Aig_Not(rr)); return((Aig_And2(bm, Aig_Not(t1), Aig_Not(t2)))); } } return(0); } /**Function******************************************************************** Synopsis [Structural hasing for and3] Description [Structural hasing for and3] SideEffects [] SeeAlso [] ******************************************************************************/ AigEdge_t Aig_And3( Aig_Manager_t *bm, AigEdge_t l, AigEdge_t r) { int caseIndex, caseSig; AigEdge_t rl, rr; rl = leftChild(r); rr = rightChild(r); caseIndex = 0; /* (a)(b c) */ if(AigCompareNode(l, rl)) { caseIndex = 1; /* (a)(a b) */ } else if(AigCompareNode(l, rr)) { caseIndex = 2; /* (a)(b a) */ } caseSig = 0; if(Aig_IsInverted(l)) caseSig += 8; if(Aig_IsInverted(rl)) caseSig += 4; if(Aig_IsInverted(rr)) caseSig += 2; if(Aig_IsInverted(r)) caseSig += 1; if(caseIndex == 0) { return(Aig_And2(bm, l, r)); } else if(caseIndex == 1) { switch(caseSig) { case 2 : case 0 : case 14 : case 12 : return(r); case 10 : case 8 : case 6 : case 4 : return(Aig_Zero); case 3 : case 1 : case 15 : case 13 : return(Aig_And(bm, rl, Aig_Not(rr))); case 11 : case 9 : case 7 : case 5 : return(l); } } else if(caseIndex == 2) { switch(caseSig) { case 4 : case 0 : case 14 : case 10 : return(r); case 12 : case 8 : case 6 : case 2 : return(Aig_Zero); case 5 : case 1 : case 15 : case 11 : return(Aig_And(bm, Aig_Not(rl), rr)); case 13 : case 9 : case 7 : case 3 : return(l); } } return(0); } /**Function******************************************************************** Synopsis [Set mask for transitive fanin nodes] Description [Set mask for transitive fanin nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void Aig_SetMaskTransitiveFanin( Aig_Manager_t *bm, int v, unsigned int mask) { if(v == 2) return; if(flags(v) & mask) return; flags(v) |= mask; Aig_SetMaskTransitiveFanin(bm, leftChild(v), mask); Aig_SetMaskTransitiveFanin(bm, rightChild(v), mask); } /**Function******************************************************************** Synopsis [Reset mask for transitive fanin nodes] Description [Reset mask for transitive fanin nodes] SideEffects [] SeeAlso [] ******************************************************************************/ void Aig_ResetMaskTransitiveFanin( Aig_Manager_t *bm, int v, unsigned int mask, unsigned int resetMask) { if(v == 2) return; if(!(flags(v) & mask)) return; flags(v) &= resetMask; Aig_ResetMaskTransitiveFanin(bm, leftChild(v), mask, resetMask); Aig_ResetMaskTransitiveFanin(bm, rightChild(v), mask, resetMask); } /**Function******************************************************************** Synopsis [Get value of aig node.] Description [The default falue is 2, which is same as UNKNOWN. This calue can be assigned from SAT solver.] SideEffects [] SeeAlso [] ******************************************************************************/ int Aig_GetValueOfNode(Aig_Manager_t *bm, AigEdge_t v) { unsigned int value, lvalue, rvalue; AigEdge_t left, right; /* if(!(flags(v) & CoiMask)) return(2); **/ if(v == 2) return(2); value = aig_value(v); if(value == 3) return(2); if(value == 2) { left = Aig_GetCanonical(bm, leftChild(v)); lvalue = Aig_GetValueOfNode(bm, left); if(lvalue == 0) { value = 0; } else { right = Aig_GetCanonical(bm, rightChild(v)); rvalue = Aig_GetValueOfNode(bm, right); if(rvalue == 0) { value = 0; } else if(rvalue == 1 && lvalue == 1) { value = 1; } else { value = 2; } } } if(value == 2) { aig_value(v) = 3; return(value); } else { aig_value(v) = value; return(value ^ Aig_IsInverted(v)); } }