diff options
Diffstat (limited to 'src/opt/dec')
| -rw-r--r-- | src/opt/dec/dec.h | 543 | ||||
| -rw-r--r-- | src/opt/dec/decAbc.c | 170 | ||||
| -rw-r--r-- | src/opt/dec/decFactor.c | 393 | ||||
| -rw-r--r-- | src/opt/dec/decMan.c | 83 | ||||
| -rw-r--r-- | src/opt/dec/decPrint.c | 221 | ||||
| -rw-r--r-- | src/opt/dec/decUtil.c | 134 | ||||
| -rw-r--r-- | src/opt/dec/module.make | 6 |
7 files changed, 1407 insertions, 143 deletions
diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h index 26af6b1c..6ecc9678 100644 --- a/src/opt/dec/dec.h +++ b/src/opt/dec/dec.h @@ -33,83 +33,89 @@ /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// +typedef struct Dec_Edge_t_ Dec_Edge_t; +struct Dec_Edge_t_ +{ + unsigned fCompl : 1; // the complemented bit + unsigned Node : 30; // the decomposition node pointed by the edge +}; + typedef struct Dec_Node_t_ Dec_Node_t; struct Dec_Node_t_ { - // the first child - unsigned fCompl0 : 1; // complemented attribute of the first fanin - unsigned iFanin0 : 11; // the number of the first fanin - // the second child - unsigned fCompl1 : 1; // complemented attribute of the second fanin - unsigned iFanin1 : 11; // the number of the second fanin + Dec_Edge_t eEdge0; // the left child of the node + Dec_Edge_t eEdge1; // the right child of the node // other info - unsigned fIntern : 1; // marks all internal nodes (to distinquish them from elementary vars) - unsigned fConst : 1; // marks the constant 1 function (topmost node only) - unsigned fCompl : 1; // marks the complement of topmost node (topmost node only) - // printing info (factored forms only) - unsigned fNodeOr : 1; // marks the original OR node - unsigned fEdge0 : 1; // marks the original complemented edge - unsigned fEdge1 : 1; // marks the original complemented edge - // some bits are left unused + void * pFunc; // the function of the node (BDD or AIG) + unsigned Level : 16; // the level of this node in the global AIG + // printing info + unsigned fNodeOr : 1; // marks the original OR node + unsigned fCompl0 : 1; // marks the original complemented edge + unsigned fCompl1 : 1; // marks the original complemented edge +}; + +typedef struct Dec_Graph_t_ Dec_Graph_t; +struct Dec_Graph_t_ +{ + int fConst; // marks the constant 1 graph + int nLeaves; // the number of leaves + int nSize; // the number of nodes (including the leaves) + int nCap; // the number of allocated nodes + Dec_Node_t * pNodes; // the array of leaves and internal nodes + Dec_Edge_t eRoot; // the pointer to the topmost node +}; + +typedef struct Dec_Man_t_ Dec_Man_t; +struct Dec_Man_t_ +{ + void * pMvcMem; // memory manager for MVC cover (used for factoring) + Vec_Int_t * vCubes; // storage for cubes + Vec_Int_t * vLits; // storage for literals + // precomputation information about 4-variable functions + unsigned short * puCanons; // canonical forms + char * pPhases; // canonical phases + char * pPerms; // canonical permutations + unsigned char * pMap; // mapping of functions into class numbers }; -/* - The decomposition tree data structure is designed to represent relatively small - (up to 100 nodes) AIGs used for factoring, rewriting, and decomposition. - - For simplicity, the nodes of the decomposition tree are written in DFS order - into an integer vector (Vec_Int_t). The decomposition node (Dec_Node_t) - is typecast into an integer when written into the array. - - This representation can be readily translated into the main AIG represented - in the ABC network. Because of the linear order of the decomposition nodes - in the array, it is easy to put the existing AIG nodes in correspondence with - them. This process begins by first putting leaves of the decomposition tree - in correpondence with the fanins of the cut used to derive the function, - which was decomposed. Next for each internal node of the decomposition tree, - we find or create a corresponding node in the AIG. Finally, the root node of - the tree replaces the original root node of the cut, which was decomposed. - - To achieve the above scenario, we reserve the first n entries for the array - to the fanins of the cut (the number of fanins is n). These entries are left - empty in the array (that is, they are represented by 0 integer). Each entry - after the fanins is an internal node (flag fIntern is set to 1). The internal - nodes can have complemented inputs (denoted by flags fComp0 and fCompl1). - The last node can be complemented (fCompl), which is true if the root node - of the decomposition tree is represented by a complemented AIG node. - - Two cases have to be specially considered: a constant function and a function - equal to an elementary variables (possibly complemented). In these two cases, - the decomposition tree/array has exactly n+1 nodes, where n in the number of - fanins. (A constant function may depend on n variable, in which case these - are redundant variables. Similarly, a function can be a function in n-D space - but in fact depend only on one variable in this space.) - - When the function is a constant, the last node has a flag fConst set to 1. - In this case the complemented flag (fCompl) shows the value of the constant. - (fCompl = 0 means costant 1; fCompl = 1 means constant 0). - When the function if an elementary variable, the last node has both pointers - pointing to the same elementary node, while the complemented flag (fCompl) - shows whether the variable is complemented. For example: x' = Not( AND(x, x) ). - - When manipulating the decomposition tree, it is convenient to return the - intermediate results of decomposition as an integer, which includes the number - of the Dec_Node_t in the array of decomposition nodes and the complemented flag. - Factoring is a special case of decomposition, which demonstrates this kind - of manipulation. -*/ //////////////////////////////////////////////////////////////////////// -/// MACRO DEFITIONS /// +/// ITERATORS /// //////////////////////////////////////////////////////////////////////// +// interator throught the leaves +#define Dec_GraphForEachLeaf( pGraph, pLeaf, i ) \ + for ( i = 0; (i < (pGraph)->nLeaves) && (((pLeaf) = Dec_GraphNode(pGraph, i)), 1); i++ ) +// interator throught the internal nodes +#define Dec_GraphForEachNode( pGraph, pAnd, i ) \ + for ( i = (pGraph)->nLeaves; (i < (pGraph)->nSize) && (((pAnd) = Dec_GraphNode(pGraph, i)), 1); i++ ) + //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== decAbc.c ========================================================*/ +extern Abc_Obj_t * Dec_GraphToNetwork( Abc_Aig_t * pMan, Dec_Graph_t * pGraph ); +extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ); +extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain ); +/*=== decFactor.c ========================================================*/ +extern Dec_Graph_t * Dec_Factor( char * pSop ); +/*=== decMan.c ========================================================*/ +extern Dec_Man_t * Dec_ManStart(); +extern void Dec_ManStop( Dec_Man_t * p ); +/*=== decPrint.c ========================================================*/ +extern void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char * pNameOut ); +/*=== decUtil.c ========================================================*/ +extern DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph ); +extern unsigned Dec_GraphDeriveTruth( Dec_Graph_t * pGraph ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + /**Function************************************************************* - Synopsis [Cleans the decomposition node.] + Synopsis [Creates an edge pointing to the node in the given polarity.] Description [] @@ -117,12 +123,16 @@ struct Dec_Node_t_ SeeAlso [] -***********************************************************************/ -static inline void Dec_NodeClean( Dec_Node_t * pNode ) { *((int *)pNode) = 0; } +***********************************************************************/ +static inline Dec_Edge_t Dec_EdgeCreate( int Node, int fCompl ) +{ + Dec_Edge_t eEdge = { fCompl, Node }; + return eEdge; +} /**Function************************************************************* - Synopsis [Convert between an interger and an decomposition node.] + Synopsis [Converts the edge into unsigned integer.] Description [] @@ -131,12 +141,14 @@ static inline void Dec_NodeClean( Dec_Node_t * pNode ) { *((int * SeeAlso [] ***********************************************************************/ -static inline Dec_Node_t Dec_Int2Node( int Num ) { return *((Dec_Node_t *)&Num); } -static inline int Dec_Node2Int( Dec_Node_t Node ) { return *((int *)&Node); } +static inline unsigned Dec_EdgeToInt( Dec_Edge_t eEdge ) +{ + return (eEdge.Node << 1) | eEdge.fCompl; +} /**Function************************************************************* - Synopsis [Returns the pointer to the i-th decomposition node.] + Synopsis [Converts unsigned integer into the edge.] Description [] @@ -145,11 +157,14 @@ static inline int Dec_Node2Int( Dec_Node_t Node ) { return * SeeAlso [] ***********************************************************************/ -static inline Dec_Node_t * Dec_NodeRead( Vec_Int_t * vDec, int i ) { return (Dec_Node_t *)vDec->pArray + i; } +static inline Dec_Edge_t Dec_IntToEdge( unsigned Edge ) +{ + return Dec_EdgeCreate( Edge >> 1, Edge & 1 ); +} /**Function************************************************************* - Synopsis [Returns the pointer to the last decomposition node.] + Synopsis [Converts the edge into unsigned integer.] Description [] @@ -158,11 +173,14 @@ static inline Dec_Node_t * Dec_NodeRead( Vec_Int_t * vDec, int i ) { return ( SeeAlso [] ***********************************************************************/ -static inline Dec_Node_t * Dec_NodeReadLast( Vec_Int_t * vDec ) { return (Dec_Node_t *)vDec->pArray + vDec->nSize - 1; } +static inline unsigned Dec_EdgeToInt_( Dec_Edge_t eEdge ) +{ + return *(unsigned *)&eEdge; +} /**Function************************************************************* - Synopsis [Returns the pointer to the fanins of the i-th decomposition node.] + Synopsis [Converts unsigned integer into the edge.] Description [] @@ -171,12 +189,14 @@ static inline Dec_Node_t * Dec_NodeReadLast( Vec_Int_t * vDec ) { return ( SeeAlso [] ***********************************************************************/ -static inline Dec_Node_t * Dec_NodeFanin0( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (Dec_Node_t *)vDec->pArray + Dec_NodeRead(vDec,i)->iFanin0; } -static inline Dec_Node_t * Dec_NodeFanin1( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (Dec_Node_t *)vDec->pArray + Dec_NodeRead(vDec,i)->iFanin1; } +static inline Dec_Edge_t Dec_IntToEdge_( unsigned Edge ) +{ + return *(Dec_Edge_t *)&Edge; +} /**Function************************************************************* - Synopsis [Returns the complemented attributes of the i-th decomposition node.] + Synopsis [Creates a graph with the given number of leaves.] Description [] @@ -185,12 +205,22 @@ static inline Dec_Node_t * Dec_NodeFanin1( Vec_Int_t * vDec, int i ) { assert( D SeeAlso [] ***********************************************************************/ -static inline bool Dec_NodeFaninC0( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (bool)Dec_NodeRead(vDec,i)->fCompl0; } -static inline bool Dec_NodeFaninC1( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (bool)Dec_NodeRead(vDec,i)->fCompl1; } +static inline Dec_Graph_t * Dec_GraphCreate( int nLeaves ) +{ + Dec_Graph_t * pGraph; + pGraph = ALLOC( Dec_Graph_t, 1 ); + memset( pGraph, 0, sizeof(Dec_Graph_t) ); + pGraph->nLeaves = nLeaves; + pGraph->nSize = nLeaves; + pGraph->nCap = 2 * nLeaves + 50; + pGraph->pNodes = ALLOC( Dec_Node_t, pGraph->nCap ); + memset( pGraph->pNodes, 0, sizeof(Dec_Node_t) * pGraph->nSize ); + return pGraph; +} /**Function************************************************************* - Synopsis [Returns the number of leaf variables.] + Synopsis [Creates constant 0 graph.] Description [] @@ -199,18 +229,19 @@ static inline bool Dec_NodeFaninC1( Vec_Int_t * vDec, int i ) { assert( SeeAlso [] ***********************************************************************/ -static inline int Dec_TreeNumVars( Vec_Int_t * vDec ) +static inline Dec_Graph_t * Dec_GraphCreateConst0() { - int i; - for ( i = 0; i < vDec->nSize; i++ ) - if ( vDec->pArray[i] ) - break; - return i; + Dec_Graph_t * pGraph; + pGraph = ALLOC( Dec_Graph_t, 1 ); + memset( pGraph, 0, sizeof(Dec_Graph_t) ); + pGraph->fConst = 1; + pGraph->eRoot.fCompl = 1; + return pGraph; } /**Function************************************************************* - Synopsis [Returns the number of AND nodes in the tree.] + Synopsis [Creates constant 1 graph.] Description [] @@ -219,20 +250,56 @@ static inline int Dec_TreeNumVars( Vec_Int_t * vDec ) SeeAlso [] ***********************************************************************/ -static int Dec_TreeNumAnds( Vec_Int_t * vDec ) +static inline Dec_Graph_t * Dec_GraphCreateConst1() { - Dec_Node_t * pNode; - pNode = Dec_NodeReadLast(vDec); - if ( pNode->fConst ) // constant - return 0; - if ( pNode->iFanin0 == pNode->iFanin1 ) // literal - return 0; - return vDec->nSize - Dec_TreeNumVars(vDec); + Dec_Graph_t * pGraph; + pGraph = ALLOC( Dec_Graph_t, 1 ); + memset( pGraph, 0, sizeof(Dec_Graph_t) ); + pGraph->fConst = 1; + return pGraph; +} + +/**Function************************************************************* + + Synopsis [Creates the literal graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Graph_t * Dec_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl ) +{ + Dec_Graph_t * pGraph; + assert( 0 <= iLeaf && iLeaf < nLeaves ); + pGraph = Dec_GraphCreate( nLeaves ); + pGraph->eRoot.Node = iLeaf; + pGraph->eRoot.fCompl = fCompl; + return pGraph; +} + +/**Function************************************************************* + + Synopsis [Creates a graph with the given number of leaves.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dec_GraphFree( Dec_Graph_t * pGraph ) +{ + FREE( pGraph->pNodes ); + free( pGraph ); } /**Function************************************************************* - Synopsis [Returns the number of literals in the factored form.] + Synopsis [Returns 1 if the graph is a constant.] Description [] @@ -241,16 +308,30 @@ static int Dec_TreeNumAnds( Vec_Int_t * vDec ) SeeAlso [] ***********************************************************************/ -static inline int Dec_TreeNumFFLits( Vec_Int_t * vDec ) +static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph ) { - return 1 + Dec_TreeNumAnds( vDec ); + return pGraph->fConst; } +/**Function************************************************************* + Synopsis [Returns 1 if the graph is constant 0.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline bool Dec_GraphIsConst0( Dec_Graph_t * pGraph ) +{ + return pGraph->fConst && pGraph->eRoot.fCompl; +} /**Function************************************************************* - Synopsis [Checks if the output node of the decomposition tree is complemented.] + Synopsis [Returns 1 if the graph is constant 1.] Description [] @@ -259,11 +340,14 @@ static inline int Dec_TreeNumFFLits( Vec_Int_t * vDec ) SeeAlso [] ***********************************************************************/ -static inline bool Dec_TreeIsComplement( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fCompl; } +static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph ) +{ + return pGraph->fConst && !pGraph->eRoot.fCompl; +} /**Function************************************************************* - Synopsis [Complements the output node of the decomposition tree.] + Synopsis [Returns 1 if the graph is complemented.] Description [] @@ -272,12 +356,31 @@ static inline bool Dec_TreeIsComplement( Vec_Int_t * vForm ) { return Dec_NodeR SeeAlso [] ***********************************************************************/ -static inline void Dec_TreeComplement( Vec_Int_t * vForm ) { Dec_NodeReadLast(vForm)->fCompl ^= 1; } +static inline bool Dec_GraphIsComplement( Dec_Graph_t * pGraph ) +{ + return pGraph->eRoot.fCompl; +} + +/**Function************************************************************* + + Synopsis [Checks if the graph is complemented.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dec_GraphComplement( Dec_Graph_t * pGraph ) +{ + pGraph->eRoot.fCompl ^= 1; +} /**Function************************************************************* - Synopsis [Checks if the output node is a constant.] + Synopsis [Returns the number of leaves.] Description [] @@ -286,13 +389,14 @@ static inline void Dec_TreeComplement( Vec_Int_t * vForm ) { Dec_NodeReadLas SeeAlso [] ***********************************************************************/ -static inline bool Dec_TreeIsConst( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fConst; } -static inline bool Dec_TreeIsConst0( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fConst && Dec_NodeReadLast(vForm)->fCompl; } -static inline bool Dec_TreeIsConst1( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fConst && !Dec_NodeReadLast(vForm)->fCompl; } +static inline int Dec_GraphLeaveNum( Dec_Graph_t * pGraph ) +{ + return pGraph->nLeaves; +} /**Function************************************************************* - Synopsis [Creates a constant 0 decomposition tree.] + Synopsis [Returns the number of internal nodes.] Description [] @@ -301,23 +405,14 @@ static inline bool Dec_TreeIsConst1( Vec_Int_t * vForm ) { return D SeeAlso [] ***********************************************************************/ -static inline Vec_Int_t * Dec_TreeCreateConst0() +static inline int Dec_GraphNodeNum( Dec_Graph_t * pGraph ) { - Vec_Int_t * vForm; - Dec_Node_t * pNode; - // create the constant node - vForm = Vec_IntAlloc( 1 ); - Vec_IntPush( vForm, 0 ); - pNode = Dec_NodeReadLast( vForm ); - pNode->fIntern = 1; - pNode->fConst = 1; - pNode->fCompl = 1; - return vForm; + return pGraph->nSize - pGraph->nLeaves; } /**Function************************************************************* - Synopsis [Creates a constant 1 decomposition tree.] + Synopsis [Returns the pointer to the node.] Description [] @@ -326,24 +421,30 @@ static inline Vec_Int_t * Dec_TreeCreateConst0() SeeAlso [] ***********************************************************************/ -static inline Vec_Int_t * Dec_TreeCreateConst1() +static inline Dec_Node_t * Dec_GraphNode( Dec_Graph_t * pGraph, int i ) { - Vec_Int_t * vForm; - Dec_Node_t * pNode; - // create the constant node - vForm = Vec_IntAlloc( 1 ); - Vec_IntPush( vForm, 0 ); - pNode = Dec_NodeReadLast( vForm ); - pNode->fIntern = 1; - pNode->fConst = 1; - pNode->fCompl = 0; - return vForm; + return pGraph->pNodes + i; } +/**Function************************************************************* + + Synopsis [Returns the pointer to the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Node_t * Dec_GraphNodeLast( Dec_Graph_t * pGraph ) +{ + return pGraph->pNodes + pGraph->nSize - 1; +} /**Function************************************************************* - Synopsis [Checks if the decomposition tree is an elementary var.] + Synopsis [Returns the number of the given node.] Description [] @@ -352,14 +453,14 @@ static inline Vec_Int_t * Dec_TreeCreateConst1() SeeAlso [] ***********************************************************************/ -static inline bool Dec_TreeIsVar( Vec_Int_t * vForm ) +static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode ) { - return Dec_NodeReadLast(vForm)->iFanin0 == Dec_NodeReadLast(vForm)->iFanin1; + return pNode - pGraph->pNodes; } /**Function************************************************************* - Synopsis [Creates the decomposition tree to represent an elementary var.] + Synopsis [Check if the graph represents elementary variable.] Description [] @@ -368,19 +469,177 @@ static inline bool Dec_TreeIsVar( Vec_Int_t * vForm ) SeeAlso [] ***********************************************************************/ -static inline Vec_Int_t * Dec_TreeCreateVar( int iVar, int nVars, int fCompl ) +static inline bool Dec_GraphIsVar( Dec_Graph_t * pGraph ) +{ + return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves; +} + +/**Function************************************************************* + + Synopsis [Check if the graph represents elementary variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline bool Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode ) +{ + return Dec_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; +} + +/**Function************************************************************* + + Synopsis [Returns the elementary variable elementary variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Node_t * Dec_GraphVar( Dec_Graph_t * pGraph ) +{ + assert( Dec_GraphIsVar( pGraph ) ); + return Dec_GraphNode( pGraph, pGraph->eRoot.Node ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of the elementary variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Dec_GraphVarInt( Dec_Graph_t * pGraph ) +{ + assert( Dec_GraphIsVar( pGraph ) ); + return Dec_GraphNodeInt( pGraph, Dec_GraphVar(pGraph) ); +} + +/**Function************************************************************* + + Synopsis [Sets the root of the graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dec_GraphSetRoot( Dec_Graph_t * pGraph, Dec_Edge_t eRoot ) +{ + pGraph->eRoot = eRoot; +} + +/**Function************************************************************* + + Synopsis [Appends a new node to the graph.] + + Description [This procedure is meant for internal use.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Node_t * Dec_GraphAppendNode( Dec_Graph_t * pGraph ) +{ + Dec_Node_t * pNode; + if ( pGraph->nSize == pGraph->nCap ) + { + pGraph->pNodes = REALLOC( Dec_Node_t, pGraph->pNodes, 2 * pGraph->nCap ); + pGraph->nCap = 2 * pGraph->nCap; + } + pNode = pGraph->pNodes + pGraph->nSize++; + memset( pNode, 0, sizeof(Dec_Node_t) ); + return pNode; +} + +/**Function************************************************************* + + Synopsis [Creates an AND node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Edge_t Dec_GraphAddNodeAnd( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 ) +{ + Dec_Node_t * pNode; + // get the new node + pNode = Dec_GraphAppendNode( pGraph ); + // set the inputs and other info + pNode->eEdge0 = eEdge0; + pNode->eEdge1 = eEdge1; + pNode->fCompl0 = eEdge0.fCompl; + pNode->fCompl1 = eEdge1.fCompl; + return Dec_EdgeCreate( pGraph->nSize - 1, 0 ); +} + +/**Function************************************************************* + + Synopsis [Creates an OR node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Edge_t Dec_GraphAddNodeOr( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 ) { - Vec_Int_t * vForm; Dec_Node_t * pNode; - // create the elementary variable node - vForm = Vec_IntAlloc( nVars + 1 ); - Vec_IntFill( vForm, nVars + 1, 0 ); - pNode = Dec_NodeReadLast( vForm ); - pNode->iFanin0 = iVar; - pNode->iFanin1 = iVar; - pNode->fIntern = 1; - pNode->fCompl = fCompl; - return vForm; + // get the new node + pNode = Dec_GraphAppendNode( pGraph ); + // set the inputs and other info + pNode->eEdge0 = eEdge0; + pNode->eEdge1 = eEdge1; + pNode->fCompl0 = eEdge0.fCompl; + pNode->fCompl1 = eEdge1.fCompl; + // make adjustments for the OR gate + pNode->fNodeOr = 1; + pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl; + pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl; + return Dec_EdgeCreate( pGraph->nSize - 1, 1 ); +} + +/**Function************************************************************* + + Synopsis [Creates an XOR node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dec_Edge_t Dec_GraphAddNodeXor( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 ) +{ + Dec_Edge_t eNode0, eNode1; + // derive the first AND + eEdge0.fCompl = !eEdge0.fCompl; + eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); + eEdge0.fCompl = !eEdge0.fCompl; + // derive the second AND + eEdge1.fCompl = !eEdge1.fCompl; + eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); + eEdge1.fCompl = !eEdge1.fCompl; + // derive the final OR + return Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c new file mode 100644 index 00000000..9931b136 --- /dev/null +++ b/src/opt/dec/decAbc.c @@ -0,0 +1,170 @@ +/**CFile**************************************************************** + + FileName [decAbc.c] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Interface between the decomposition package and ABC network.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: decAbc.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "dec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Transforms the decomposition graph into the AIG.] + + Description [AIG nodes for the fanins should be assigned to pNode->pFunc + of the leaves of the graph before calling this procedure.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Dec_GraphToNetwork( Abc_Aig_t * pMan, Dec_Graph_t * pGraph ) +{ + Abc_Obj_t * pAnd0, * pAnd1; + Dec_Node_t * pNode; + int i; + // check for constant function + if ( Dec_GraphIsConst(pGraph) ) + return Abc_ObjNotCond( Abc_AigConst1(pMan), Dec_GraphIsComplement(pGraph) ); + // check for a literal + if ( Dec_GraphIsVar(pGraph) ) + return Abc_ObjNotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) ); + // build the AIG nodes corresponding to the AND gates of the graph + Dec_GraphForEachNode( pGraph, pNode, i ) + { + pAnd0 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); + pAnd1 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); + pNode->pFunc = Abc_AigAnd( pMan, pAnd0, pAnd1 ); + } + // complement the result if necessary + return Abc_ObjNotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) ); +} + +/**Function************************************************************* + + Synopsis [Counts the number of new nodes added when using this graph.] + + Description [AIG nodes for the fanins should be assigned to pNode->pFunc + of the leaves of the graph before calling this procedure. + Returns -1 if the number of nodes and levels exceeded the given limit or + the number of levels exceeded the maximum allowed level.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ) +{ + Abc_Aig_t * pMan = pRoot->pNtk->pManFunc; + Dec_Node_t * pNode, * pNode0, * pNode1; + Abc_Obj_t * pAnd, * pAnd0, * pAnd1; + int i, Counter, LevelNew, LevelOld; + // check for constant function or a literal + if ( Dec_GraphIsConst(pGraph) || Dec_GraphIsVar(pGraph) ) + return 0; + // set the levels of the leaves + Dec_GraphForEachLeaf( pGraph, pNode, i ) + pNode->Level = Abc_ObjRegular(pNode->pFunc)->Level; + // compute the AIG size after adding the internal nodes + Counter = 0; + Dec_GraphForEachNode( pGraph, pNode, i ) + { + // get the children of this node + pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node ); + pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node ); + // get the AIG nodes corresponding to the children + pAnd0 = pNode0->pFunc; + pAnd1 = pNode1->pFunc; + if ( pAnd0 && pAnd1 ) + { + // if they are both present, find the resulting node + pAnd0 = Abc_ObjNotCond( pAnd0, pNode->eEdge0.fCompl ); + pAnd1 = Abc_ObjNotCond( pAnd1, pNode->eEdge1.fCompl ); + pAnd = Abc_AigAndLookup( pMan, pAnd0, pAnd1 ); + // return -1 if the node is the same as the original root + if ( Abc_ObjRegular(pAnd) == pRoot ) + return -1; + } + else + pAnd = NULL; + // count the number of added nodes + if ( pAnd == NULL || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pAnd)) ) + { + if ( ++Counter > NodeMax ) + return -1; + } + // count the number of new levels + LevelNew = 1 + ABC_MAX( pNode0->Level, pNode1->Level ); + if ( pAnd ) + { + if ( Abc_ObjRegular(pAnd) == Abc_AigConst1(pMan) ) + LevelNew = 0; + else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd0) ) + LevelNew = (int)Abc_ObjRegular(pAnd0)->Level; + else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd1) ) + LevelNew = (int)Abc_ObjRegular(pAnd1)->Level; + LevelOld = (int)Abc_ObjRegular(pAnd)->Level; + assert( LevelNew == LevelOld ); + } + if ( LevelNew > LevelMax ) + return -1; + pNode->pFunc = pAnd; + pNode->Level = LevelNew; + } + return Counter; +} + + +/**Function************************************************************* + + Synopsis [Replaces MFFC of the node by the new factored form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain ) +{ + Abc_Obj_t * pRootNew; + Abc_Ntk_t * pNtk = pRoot->pNtk; + int nNodesNew, nNodesOld; + nNodesOld = Abc_NtkNodeNum(pNtk); + // create the new structure of nodes + pRootNew = Dec_GraphToNetwork( pNtk->pManFunc, pGraph ); + // remove the old nodes + Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew ); + // compare the gains + nNodesNew = Abc_NtkNodeNum(pNtk); + assert( nGain <= nNodesOld - nNodesNew ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c new file mode 100644 index 00000000..f6654476 --- /dev/null +++ b/src/opt/dec/decFactor.c @@ -0,0 +1,393 @@ +/**CFile**************************************************************** + + FileName [ftFactor.c] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Procedures for algebraic factoring.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: ftFactor.c,v 1.3 2003/09/01 04:56:43 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "main.h" +#include "mvc.h" +#include "dec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Dec_Edge_t Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover ); +static Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple ); +static Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover ); +static Dec_Edge_t Dec_FactorTrivialCube( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits ); +static Dec_Edge_t Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr ); +static int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm ); +static Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Factors the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Dec_Factor( char * pSop ) +{ + Mvc_Cover_t * pCover; + Dec_Graph_t * pFForm; + Dec_Edge_t eRoot; + + // derive the cover from the SOP representation + pCover = Dec_ConvertSopToMvc( pSop ); + + // make sure the cover is CCS free (should be done before CST) + Mvc_CoverContain( pCover ); + // check for trivial functions + if ( Mvc_CoverIsEmpty(pCover) ) + { + Mvc_CoverFree( pCover ); + return Dec_GraphCreateConst0(); + } + if ( Mvc_CoverIsTautology(pCover) ) + { + Mvc_CoverFree( pCover ); + return Dec_GraphCreateConst1(); + } + + // perform CST + Mvc_CoverInverse( pCover ); // CST + // start the factored form + pFForm = Dec_GraphCreate( Abc_SopGetVarNum(pSop) ); + // factor the cover + eRoot = Dec_Factor_rec( pFForm, pCover ); + // finalize the factored form + Dec_GraphSetRoot( pFForm, eRoot ); + // complement the factored form if SOP is complemented + if ( Abc_SopIsComplement(pSop) ) + Dec_GraphComplement( pFForm ); + // verify the factored form +// if ( !Dec_FactorVerify( pSop, pFForm ) ) +// printf( "Verification has failed.\n" ); +// Mvc_CoverInverse( pCover ); // undo CST + Mvc_CoverFree( pCover ); + return pFForm; +} + +/**Function************************************************************* + + Synopsis [Internal recursive factoring procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover ) +{ + Mvc_Cover_t * pDiv, * pQuo, * pRem, * pCom; + Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem; + Dec_Edge_t eNodeAnd, eNode; + + // make sure the cover contains some cubes + assert( Mvc_CoverReadCubeNum(pCover) ); + + // get the divisor + pDiv = Mvc_CoverDivisor( pCover ); + if ( pDiv == NULL ) + return Dec_FactorTrivial( pFForm, pCover ); + + // divide the cover by the divisor + Mvc_CoverDivideInternal( pCover, pDiv, &pQuo, &pRem ); + assert( Mvc_CoverReadCubeNum(pQuo) ); + + Mvc_CoverFree( pDiv ); + Mvc_CoverFree( pRem ); + + // check the trivial case + if ( Mvc_CoverReadCubeNum(pQuo) == 1 ) + { + eNode = Dec_FactorLF_rec( pFForm, pCover, pQuo ); + Mvc_CoverFree( pQuo ); + return eNode; + } + + // make the quotient cube free + Mvc_CoverMakeCubeFree( pQuo ); + + // divide the cover by the quotient + Mvc_CoverDivideInternal( pCover, pQuo, &pDiv, &pRem ); + + // check the trivial case + if ( Mvc_CoverIsCubeFree( pDiv ) ) + { + eNodeDiv = Dec_Factor_rec( pFForm, pDiv ); + eNodeQuo = Dec_Factor_rec( pFForm, pQuo ); + Mvc_CoverFree( pDiv ); + Mvc_CoverFree( pQuo ); + eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo ); + if ( Mvc_CoverReadCubeNum(pRem) == 0 ) + { + Mvc_CoverFree( pRem ); + return eNodeAnd; + } + else + { + eNodeRem = Dec_Factor_rec( pFForm, pRem ); + Mvc_CoverFree( pRem ); + return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem ); + } + } + + // get the common cube + pCom = Mvc_CoverCommonCubeCover( pDiv ); + Mvc_CoverFree( pDiv ); + Mvc_CoverFree( pQuo ); + Mvc_CoverFree( pRem ); + + // solve the simple problem + eNode = Dec_FactorLF_rec( pFForm, pCover, pCom ); + Mvc_CoverFree( pCom ); + return eNode; +} + + +/**Function************************************************************* + + Synopsis [Internal recursive factoring procedure for the leaf case.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple ) +{ + Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame()); + Vec_Int_t * vEdgeLits = pManDec->vLits; + Mvc_Cover_t * pDiv, * pQuo, * pRem; + Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem; + Dec_Edge_t eNodeAnd; + + // get the most often occurring literal + pDiv = Mvc_CoverBestLiteralCover( pCover, pSimple ); + // divide the cover by the literal + Mvc_CoverDivideByLiteral( pCover, pDiv, &pQuo, &pRem ); + // get the node pointer for the literal + eNodeDiv = Dec_FactorTrivialCube( pFForm, pDiv, Mvc_CoverReadCubeHead(pDiv), vEdgeLits ); + Mvc_CoverFree( pDiv ); + // factor the quotient and remainder + eNodeQuo = Dec_Factor_rec( pFForm, pQuo ); + Mvc_CoverFree( pQuo ); + eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo ); + if ( Mvc_CoverReadCubeNum(pRem) == 0 ) + { + Mvc_CoverFree( pRem ); + return eNodeAnd; + } + else + { + eNodeRem = Dec_Factor_rec( pFForm, pRem ); + Mvc_CoverFree( pRem ); + return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem ); + } +} + + + +/**Function************************************************************* + + Synopsis [Factoring the cover, which has no algebraic divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover ) +{ + Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame()); + Vec_Int_t * vEdgeCubes = pManDec->vCubes; + Vec_Int_t * vEdgeLits = pManDec->vLits; + Mvc_Manager_t * pMem = pManDec->pMvcMem; + Dec_Edge_t eNode; + Mvc_Cube_t * pCube; + // create the factored form for each cube + Vec_IntClear( vEdgeCubes ); + Mvc_CoverForEachCube( pCover, pCube ) + { + eNode = Dec_FactorTrivialCube( pFForm, pCover, pCube, vEdgeLits ); + Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) ); + } + // balance the factored forms + return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeCubes->pArray, vEdgeCubes->nSize, 1 ); +} + +/**Function************************************************************* + + Synopsis [Factoring the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_FactorTrivialCube( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits ) +{ +// Dec_Edge_t eNode; + int iBit, Value; + // create the factored form for each literal + Vec_IntClear( vEdgeLits ); + Mvc_CubeForEachBit( pCover, pCube, iBit, Value ) + if ( Value ) + { +// eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST +// Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) ); + Vec_IntPush( vEdgeLits, iBit ); + } + // balance the factored forms + return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 ); +} + +/**Function************************************************************* + + Synopsis [Create the well-balanced tree of nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr ) +{ + Dec_Edge_t eNode1, eNode2; + int nNodes1, nNodes2; + + if ( nNodes == 1 ) + return peNodes[0]; + + // split the nodes into two parts + nNodes1 = nNodes/2; + nNodes2 = nNodes - nNodes1; +// nNodes2 = nNodes/2; +// nNodes1 = nNodes - nNodes2; + + // recursively construct the tree for the parts + eNode1 = Dec_FactorTrivialTree_rec( pFForm, peNodes, nNodes1, fNodeOr ); + eNode2 = Dec_FactorTrivialTree_rec( pFForm, peNodes + nNodes1, nNodes2, fNodeOr ); + + if ( fNodeOr ) + return Dec_GraphAddNodeOr( pFForm, eNode1, eNode2 ); + else + return Dec_GraphAddNodeAnd( pFForm, eNode1, eNode2 ); +} + + + +/**Function************************************************************* + + Synopsis [Converts SOP into MVC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop ) +{ + Dec_Man_t * pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame()); + Mvc_Manager_t * pMem = pManDec->pMvcMem; + Mvc_Cover_t * pMvc; + Mvc_Cube_t * pMvcCube; + char * pCube; + int nVars, Value, v; + + // start the cover + nVars = Abc_SopGetVarNum(pSop); + pMvc = Mvc_CoverAlloc( pMem, nVars * 2 ); + // check the logic function of the node + Abc_SopForEachCube( pSop, nVars, pCube ) + { + // create and add the cube + pMvcCube = Mvc_CubeAlloc( pMvc ); + Mvc_CoverAddCubeTail( pMvc, pMvcCube ); + // fill in the literals + Mvc_CubeBitFill( pMvcCube ); + Abc_CubeForEachVar( pCube, Value, v ) + { + if ( Value == '0' ) + Mvc_CubeBitRemove( pMvcCube, v * 2 + 1 ); + else if ( Value == '1' ) + Mvc_CubeBitRemove( pMvcCube, v * 2 ); + } + } + return pMvc; +} + +/**Function************************************************************* + + Synopsis [Verifies that the factoring is correct.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm ) +{ + DdManager * dd = Abc_FrameReadManDd( Abc_FrameGetGlobalFrame() ); + DdNode * bFunc1, * bFunc2; + int RetValue; + bFunc1 = Abc_ConvertSopToBdd( dd, pSop ); Cudd_Ref( bFunc1 ); + bFunc2 = Dec_GraphDeriveBdd( dd, pFForm ); Cudd_Ref( bFunc2 ); +//Extra_bddPrint( dd, bFunc1 ); printf("\n"); +//Extra_bddPrint( dd, bFunc2 ); printf("\n"); + RetValue = (bFunc1 == bFunc2); + if ( bFunc1 != bFunc2 ) + { + int s; + Extra_bddPrint( dd, bFunc1 ); printf("\n"); + Extra_bddPrint( dd, bFunc2 ); printf("\n"); + s = 0; + } + Cudd_RecursiveDeref( dd, bFunc1 ); + Cudd_RecursiveDeref( dd, bFunc2 ); + return RetValue; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/dec/decMan.c b/src/opt/dec/decMan.c new file mode 100644 index 00000000..1d44d5cb --- /dev/null +++ b/src/opt/dec/decMan.c @@ -0,0 +1,83 @@ +/**CFile**************************************************************** + + FileName [decMan.c] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Decomposition manager.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: decMan.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "mvc.h" +#include "dec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Start the MVC manager used in the factoring package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Man_t * Dec_ManStart() +{ + Dec_Man_t * p; + int clk = clock(); + p = ALLOC( Dec_Man_t, 1 ); + p->pMvcMem = Mvc_ManagerStart(); + p->vCubes = Vec_IntAlloc( 8 ); + p->vLits = Vec_IntAlloc( 8 ); + // canonical forms, phases, perms + Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap ); +//PRT( "NPN classes precomputation time", clock() - clk ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the MVC maanager used in the factoring package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dec_ManStop( Dec_Man_t * p ) +{ + Mvc_ManagerFree( p->pMvcMem ); + Vec_IntFree( p->vCubes ); + Vec_IntFree( p->vLits ); + free( p->puCanons ); + free( p->pPhases ); + free( p->pPerms ); + free( p->pMap ); + free( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/dec/decPrint.c b/src/opt/dec/decPrint.c new file mode 100644 index 00000000..6fb20327 --- /dev/null +++ b/src/opt/dec/decPrint.c @@ -0,0 +1,221 @@ +/**CFile**************************************************************** + + FileName [decPrint.c] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Procedures to print the decomposition graphs (factored forms).] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: decPrint.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "dec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax ); +static int Dec_GraphPrintGetLeafName( FILE * pFile, int iLeaf, int fCompl, char * pNamesIn[] ); +static void Dec_GraphPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax ); +static int Dec_GraphPrintOutputName( FILE * pFile, char * pNameOut, int fCompl ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Prints the decomposition graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char * pNameOut ) +{ + Vec_Ptr_t * vNamesIn = NULL; + int LitSizeMax, LitSizeCur, Pos, i; + + // create the names if not given by the user + if ( pNamesIn == NULL ) + { + vNamesIn = Abc_NodeGetFakeNames( Dec_GraphLeaveNum(pGraph) ); + pNamesIn = (char **)vNamesIn->pArray; + } + if ( pNameOut == NULL ) + pNameOut = "F"; + + // get the size of the longest literal + LitSizeMax = 0; + for ( i = 0; i < Dec_GraphLeaveNum(pGraph); i++ ) + { + LitSizeCur = strlen(pNamesIn[i]); + if ( LitSizeMax < LitSizeCur ) + LitSizeMax = LitSizeCur; + } + if ( LitSizeMax > 50 ) + LitSizeMax = 20; + + // write the decomposition graph (factored form) + if ( Dec_GraphIsConst(pGraph) ) // constant + { + Pos = Dec_GraphPrintOutputName( pFile, pNameOut, 0 ); + fprintf( pFile, "Constant %d", !Dec_GraphIsComplement(pGraph) ); + } + else if ( Dec_GraphIsVar(pGraph) ) // literal + { + Pos = Dec_GraphPrintOutputName( pFile, pNameOut, 0 ); + Dec_GraphPrintGetLeafName( pFile, Dec_GraphVarInt(pGraph), Dec_GraphIsComplement(pGraph), pNamesIn ); + } + else + { + Pos = Dec_GraphPrintOutputName( pFile, pNameOut, Dec_GraphIsComplement(pGraph) ); + Dec_GraphPrint_rec( pFile, pGraph, Dec_GraphNodeLast(pGraph), 0, pNamesIn, &Pos, LitSizeMax ); + } + fprintf( pFile, "\n" ); + + if ( vNamesIn ) + Abc_NodeFreeNames( vNamesIn ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax ) +{ + Dec_Node_t * pNode0, * pNode1; + pNode0 = Dec_GraphNode(pGraph, pNode->eEdge0.Node); + pNode1 = Dec_GraphNode(pGraph, pNode->eEdge1.Node); + if ( Dec_GraphNodeIsVar(pGraph, pNode) ) // FT_NODE_LEAF ) + { + (*pPos) += Dec_GraphPrintGetLeafName( pFile, Dec_GraphNodeInt(pGraph,pNode), fCompl, pNamesIn ); + return; + } + if ( !pNode->fNodeOr ) // FT_NODE_AND ) + { + if ( !pNode0->fNodeOr ) // != FT_NODE_OR ) + Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax ); + else + { + fprintf( pFile, "(" ); + (*pPos)++; + Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax ); + fprintf( pFile, ")" ); + (*pPos)++; + } + fprintf( pFile, " " ); + (*pPos)++; + + Dec_GraphPrintUpdatePos( pFile, pPos, LitSizeMax ); + + if ( !pNode1->fNodeOr ) // != FT_NODE_OR ) + Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax ); + else + { + fprintf( pFile, "(" ); + (*pPos)++; + Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax ); + fprintf( pFile, ")" ); + (*pPos)++; + } + return; + } + if ( pNode->fNodeOr ) // FT_NODE_OR ) + { + Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax ); + fprintf( pFile, " + " ); + (*pPos) += 3; + + Dec_GraphPrintUpdatePos( pFile, pPos, LitSizeMax ); + + Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax ); + return; + } + assert( 0 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dec_GraphPrintGetLeafName( FILE * pFile, int iLeaf, int fCompl, char * pNamesIn[] ) +{ + static char Buffer[100]; + sprintf( Buffer, "%s%s", pNamesIn[iLeaf], fCompl? "\'" : "" ); + fprintf( pFile, "%s", Buffer ); + return strlen( Buffer ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dec_GraphPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax ) +{ + int i; + if ( *pPos + LitSizeMax < 77 ) + return; + fprintf( pFile, "\n" ); + for ( i = 0; i < 10; i++ ) + fprintf( pFile, " " ); + *pPos = 10; +} + +/**Function************************************************************* + + Synopsis [Starts the printout for a decomposition graph.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dec_GraphPrintOutputName( FILE * pFile, char * pNameOut, int fCompl ) +{ + if ( pNameOut == NULL ) + return 0; + fprintf( pFile, "%6s%s = ", pNameOut, fCompl? "\'" : " " ); + return 10; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/dec/decUtil.c b/src/opt/dec/decUtil.c new file mode 100644 index 00000000..02c3346e --- /dev/null +++ b/src/opt/dec/decUtil.c @@ -0,0 +1,134 @@ +/**CFile**************************************************************** + + FileName [decUtil.c] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Decomposition unitilies.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: decUtil.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "dec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Converts graph to BDD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph ) +{ + DdNode * bFunc, * bFunc0, * bFunc1; + Dec_Node_t * pNode; + int i; + + // sanity checks + assert( Dec_GraphLeaveNum(pGraph) >= 0 ); + assert( Dec_GraphLeaveNum(pGraph) <= pGraph->nSize ); + + // check for constant function + if ( Dec_GraphIsConst(pGraph) ) + return Cudd_NotCond( b1, Dec_GraphIsComplement(pGraph) ); + // check for a literal + if ( Dec_GraphIsVar(pGraph) ) + return Cudd_NotCond( Cudd_bddIthVar(dd, Dec_GraphVarInt(pGraph)), Dec_GraphIsComplement(pGraph) ); + + // assign the elementary variables + Dec_GraphForEachLeaf( pGraph, pNode, i ) + pNode->pFunc = Cudd_bddIthVar( dd, i ); + + // compute the function for each internal node + Dec_GraphForEachNode( pGraph, pNode, i ) + { + bFunc0 = Cudd_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); + bFunc1 = Cudd_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); + pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( pNode->pFunc ); + } + + // deref the intermediate results + bFunc = pNode->pFunc; Cudd_Ref( bFunc ); + Dec_GraphForEachNode( pGraph, pNode, i ) + Cudd_RecursiveDeref( dd, pNode->pFunc ); + Cudd_Deref( bFunc ); + + // complement the result if necessary + return Cudd_NotCond( bFunc, Dec_GraphIsComplement(pGraph) ); +} + +/**Function************************************************************* + + Synopsis [Derives the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Dec_GraphDeriveTruth( Dec_Graph_t * pGraph ) +{ + unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + unsigned uTruth, uTruth0, uTruth1; + Dec_Node_t * pNode; + int i; + + // sanity checks + assert( Dec_GraphLeaveNum(pGraph) >= 0 ); + assert( Dec_GraphLeaveNum(pGraph) <= pGraph->nSize ); + assert( Dec_GraphLeaveNum(pGraph) <= 5 ); + + // check for constant function + if ( Dec_GraphIsConst(pGraph) ) + return Dec_GraphIsComplement(pGraph)? 0 : ~((unsigned)0); + // check for a literal + if ( Dec_GraphIsVar(pGraph) ) + return Dec_GraphIsComplement(pGraph)? ~uTruths[Dec_GraphVarInt(pGraph)] : uTruths[Dec_GraphVarInt(pGraph)]; + + // assign the elementary variables + Dec_GraphForEachLeaf( pGraph, pNode, i ) + pNode->pFunc = (void *)uTruths[i]; + + // compute the function for each internal node + Dec_GraphForEachNode( pGraph, pNode, i ) + { + uTruth0 = (unsigned)Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; + uTruth1 = (unsigned)Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; + uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0; + uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1; + uTruth = uTruth0 & uTruth1; + pNode->pFunc = (void *)uTruth; + } + + // complement the result if necessary + return Dec_GraphIsComplement(pGraph)? ~uTruth : uTruth; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/dec/module.make b/src/opt/dec/module.make index d6d908e7..1e0722d5 100644 --- a/src/opt/dec/module.make +++ b/src/opt/dec/module.make @@ -1 +1,5 @@ -SRC += +SRC += src/opt/dec/decAbc.c \ + src/opt/dec/decFactor.c \ + src/opt/dec/decMan.c \ + src/opt/dec/decPrint.c \ + src/opt/dec/decUtil.c |