summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/rwr/rwr.h131
-rw-r--r--src/opt/rwr/rwrCut.c256
-rw-r--r--src/opt/rwr/rwrEva.c129
-rw-r--r--src/opt/rwr/rwrExp.c179
-rw-r--r--src/opt/rwr/rwrLib.c670
-rw-r--r--src/opt/rwr/rwrMan.c311
-rw-r--r--src/opt/rwr/rwrUtil.c102
7 files changed, 1778 insertions, 0 deletions
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
new file mode 100644
index 00000000..19fc34c4
--- /dev/null
+++ b/src/opt/rwr/rwr.h
@@ -0,0 +1,131 @@
+/**CFile****************************************************************
+
+ FileName [rwr.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting package.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rwr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __RWR_H__
+#define __RWR_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+#define RWR_LIMIT 1048576/4 // ((1 << 20)
+
+typedef struct Rwr_Node_t_ Rwr_Node_t;
+struct Rwr_Node_t_ // 24 bytes
+{
+ int Id; // ID
+ int TravId; // traversal ID
+ unsigned uTruth : 16; // truth table
+ unsigned Volume : 8; // volume
+ unsigned Level : 5; // level
+ unsigned fMark : 1; // mark
+ unsigned fUsed : 1; // mark
+ unsigned fExor : 1; // mark
+ Rwr_Node_t * p0; // first child
+ Rwr_Node_t * p1; // second child
+ Rwr_Node_t * pNext; // next in the table
+};
+
+typedef struct Rwr_Cut_t_ Rwr_Cut_t;
+struct Rwr_Cut_t_ // 24 bytes
+{
+ unsigned nLeaves : 3; // the number of leaves
+ unsigned fTime : 1; // set to 1 if meets the required times
+ unsigned fGain : 1; // set to 1 if does not increase nodes
+ unsigned Volume : 11; // the gain in the number of nodes
+ unsigned uTruth : 16; // the truth table
+ Abc_Obj_t * ppLeaves[4]; // the leaves
+ Rwr_Cut_t * pNext; // the next cut in the list
+};
+
+struct Abc_ManRwr_t_
+{
+ // internal lookups
+ int nFuncs; // the number of four var functions
+ unsigned short * puCanons; // canonical forms
+ char * puPhases; // canonical phases
+ char * pPractical; // practical classes
+ unsigned short puPerms[256][16]; // permutations for three var functions
+ // node space
+ Vec_Ptr_t * vForest; // all the nodes
+ Rwr_Node_t ** pTable; // the hash table of nodes by their canonical form
+ Extra_MmFixed_t * pMmNode; // memory for nodes and cuts
+ int nTravIds; // the counter of traversal IDs
+ int nConsidered; // the number of nodes considered
+ int nAdded; // the number of nodes added to lists
+ int nClasses; // the number of NN classes
+ // intermediate data
+ Vec_Int_t * vFanNums; // the number of fanouts of each node (used to free cuts)
+ Vec_Int_t * vReqTimes; // the required times for each node (used for delay-driven evalution)
+ // the result of resynthesis
+ Vec_Int_t * vForm; // the decomposition tree (temporary)
+ Vec_Ptr_t * vFanins; // the fanins array (temporary)
+ Vec_Ptr_t * vTfo; // the TFO node array (temporary)
+ Vec_Vec_t * vLevels; // the levelized structure (temporary)
+ int nGainMax;
+ // runtime statistics
+ int time1;
+ int time2;
+ int time3;
+ int time4;
+};
+
+// manipulation of complemented attributes
+static inline bool Rwr_IsComplement( Rwr_Node_t * p ) { return (bool)(((unsigned)p) & 01); }
+static inline Rwr_Node_t * Rwr_Regular( Rwr_Node_t * p ) { return (Rwr_Node_t *)((unsigned)(p) & ~01); }
+static inline Rwr_Node_t * Rwr_Not( Rwr_Node_t * p ) { return (Rwr_Node_t *)((unsigned)(p) ^ 01); }
+static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c ) { return (Rwr_Node_t *)((unsigned)(p) ^ (c)); }
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== rwrLib.c ==========================================================*/
+extern void Rwr_ManPrecompute( Abc_ManRwr_t * p );
+extern void Rwr_ManWriteToFile( Abc_ManRwr_t * p, char * pFileName );
+extern void Rwr_ManLoadFromFile( Abc_ManRwr_t * p, char * pFileName );
+extern void Rwr_ManPrint( Abc_ManRwr_t * p );
+extern Rwr_Node_t * Rwr_ManAddVar( Abc_ManRwr_t * p, unsigned uTruth );
+/*=== rwrMan.c ==========================================================*/
+extern unsigned short Rwr_FunctionPhase( unsigned uTruth, unsigned uPhase );
+/*=== rwrUtil.c ==========================================================*/
+extern Vec_Int_t * Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk );
+extern Vec_Int_t * Rwt_NtkRequiredLevels( Abc_Ntk_t * pNtk );
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/opt/rwr/rwrCut.c b/src/opt/rwr/rwrCut.c
new file mode 100644
index 00000000..88ea3cdb
--- /dev/null
+++ b/src/opt/rwr/rwrCut.c
@@ -0,0 +1,256 @@
+/**CFile****************************************************************
+
+ FileName [rwrCut.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting package.]
+
+ Synopsis [Cut computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rwrCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static Rwr_Cut_t * Rwr_CutAlloc( Abc_ManRwr_t * p );
+static Rwr_Cut_t * Rwr_CutCreateTriv( Abc_ManRwr_t * p, Abc_Obj_t * pNode );
+static Rwr_Cut_t * Rwr_CutsMerge( Abc_ManRwr_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t * pCut1, int fCompl0, int fCompl1 );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Assigns elementary cuts to the PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkManRwrStartCuts( Abc_ManRwr_t * p, Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNode;
+ int i;
+ // set the trivial cuts
+ Abc_NtkCleanCopy( pNtk );
+ Abc_NtkForEachCi( pNtk, pNode, i )
+ pNode->pCopy = (Abc_Obj_t *)Rwr_CutCreateTriv( p, pNode );
+ // precompute the required times for all internal nodes
+ p->vFanNums = Rwt_NtkFanoutCounters( pNtk );
+ // save the fanout counters for all internal nodes
+ p->vReqTimes = Rwt_NtkRequiredLevels( pNtk );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes cuts for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeRwrComputeCuts( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
+{
+ Rwr_Cut_t * pCuts0, * pCuts1, * pTemp0, * pTemp1, * pCut;
+ Rwr_Cut_t * pList = NULL, ** ppPlace = &pList; // linked list of cuts
+ assert( Abc_ObjIsNode(pNode) );
+ if ( Abc_NodeIsConst(pNode) )
+ return;
+ // create the elementary cut
+ pCut = Rwr_CutCreateTriv( p, pNode );
+ // add it to the linked list
+ *ppPlace = pCut; ppPlace = &pCut->pNext;
+ // create cuts by merging pairwise
+ pCuts0 = (Rwr_Cut_t *)Abc_ObjFanin0(pNode)->pCopy;
+ pCuts1 = (Rwr_Cut_t *)Abc_ObjFanin1(pNode)->pCopy;
+ assert( pCuts0 && pCuts1 );
+ for ( pTemp0 = pCuts0; pTemp0; pTemp0 = pTemp0->pNext )
+ for ( pTemp1 = pCuts1; pTemp1; pTemp1 = pTemp1->pNext )
+ {
+ pCut = Rwr_CutsMerge( p, pTemp0, pTemp1, Abc_ObjFaninC0(pNode), Abc_ObjFaninC1(pNode) );
+ if ( pCut == NULL )
+ continue;
+ // add it to the linked list
+ *ppPlace = pCut; ppPlace = &pCut->pNext;
+ }
+ // set the linked list
+ pNode->pCopy = (Abc_Obj_t *)pList;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Start the cut computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Rwr_Cut_t * Rwr_CutsMerge( Abc_ManRwr_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+ Abc_Obj_t * ppNodes[4], * pNodeTemp;
+ Rwr_Cut_t * pCut;
+ unsigned uPhase, uTruth0, uTruth1;
+ int i, k, min, nTotal;
+
+ // solve the most typical case: both cuts are four input
+ if ( pCut0->nLeaves == 4 && pCut1->nLeaves == 4 )
+ {
+ for ( i = 0; i < 4; i++ )
+ if ( pCut0->ppLeaves[i] != pCut1->ppLeaves[i] )
+ return NULL;
+ // create the cut
+ pCut = Rwr_CutAlloc( p );
+ pCut->nLeaves = 4;
+ for ( i = 0; i < 4; i++ )
+ pCut->ppLeaves[i] = pCut0->ppLeaves[i];
+ pCut->uTruth = (fCompl0? ~pCut0->uTruth : pCut0->uTruth) & (fCompl1? ~pCut1->uTruth : pCut1->uTruth) & 0xFFFF;
+ return pCut;
+ }
+
+ // create the set of new nodes
+ // count the number of unique entries in pCut1
+ nTotal = pCut0->nLeaves;
+ for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+ {
+ // try to find this entry among the leaves of pCut0
+ for ( k = 0; k < (int)pCut0->nLeaves; k++ )
+ if ( pCut1->ppLeaves[i] == pCut0->ppLeaves[k] )
+ break;
+ if ( k < (int)pCut0->nLeaves ) // found
+ continue;
+ // we found a new entry to add
+ if ( nTotal == 4 )
+ return NULL;
+ ppNodes[nTotal++] = pCut1->ppLeaves[i];
+ }
+ // we know that the feasible cut exists
+
+ // add the starting entries
+ for ( k = 0; k < (int)pCut0->nLeaves; k++ )
+ ppNodes[k] = pCut0->ppLeaves[k];
+
+ // selection-sort the entries
+ for ( i = 0; i < nTotal - 1; i++ )
+ {
+ min = i;
+ for ( k = i+1; k < nTotal; k++ )
+ if ( ppNodes[k]->Id < ppNodes[min]->Id )
+ min = k;
+ pNodeTemp = ppNodes[i];
+ ppNodes[i] = ppNodes[min];
+ ppNodes[min] = pNodeTemp;
+ }
+
+ // find the mapping from the old nodes to the new
+ if ( pCut0->nLeaves == 4 )
+ uTruth0 = pCut0->uTruth;
+ else
+ {
+ uPhase = 0;
+ for ( i = 0; i < (int)pCut0->nLeaves; i++ )
+ {
+ for ( k = 0; k < nTotal; k++ )
+ if ( pCut0->ppLeaves[i] == ppNodes[k] )
+ break;
+ uPhase |= (1 << k);
+ }
+ assert( uPhase < 16 );
+ assert( pCut0->uTruth < 256 );
+ uTruth0 = p->puPerms[pCut0->uTruth][uPhase];
+ }
+
+ // find the mapping from the old nodes to the new
+ if ( pCut1->nLeaves == 4 )
+ uTruth1 = pCut1->uTruth;
+ else
+ {
+ uPhase = 0;
+ for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+ {
+ for ( k = 0; k < nTotal; k++ )
+ if ( pCut1->ppLeaves[i] == ppNodes[k] )
+ break;
+ uPhase |= (1 << k);
+ }
+ assert( uPhase < 16 );
+ assert( pCut1->uTruth < 256 );
+ uTruth1 = p->puPerms[pCut1->uTruth][uPhase];
+ }
+
+ // create the cut
+ pCut = Rwr_CutAlloc( p );
+ pCut->nLeaves = nTotal;
+ for ( i = 0; i < nTotal; i++ )
+ pCut->ppLeaves[i] = ppNodes[i];
+ pCut->uTruth = (fCompl0? ~uTruth0 : uTruth0) & (fCompl1? ~uTruth1 : uTruth1) & 0xFFFF;
+ return pCut;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Start the cut computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Rwr_Cut_t * Rwr_CutAlloc( Abc_ManRwr_t * p )
+{
+ Rwr_Cut_t * pCut;
+ pCut = (Rwr_Cut_t *)Extra_MmFixedEntryFetch( p->pMmNode );
+ memset( pCut, 0, sizeof(Rwr_Cut_t) );
+ return pCut;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Start the cut computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Rwr_Cut_t * Rwr_CutCreateTriv( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
+{
+ Rwr_Cut_t * pCut;
+ pCut = Rwr_CutAlloc( p );
+ pCut->nLeaves = 1;
+ pCut->ppLeaves[0] = pNode;
+ pCut->uTruth = 0xAAAA;
+ return pCut;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
new file mode 100644
index 00000000..ecf03f4f
--- /dev/null
+++ b/src/opt/rwr/rwrEva.c
@@ -0,0 +1,129 @@
+/**CFile****************************************************************
+
+ FileName [rwrDec.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting package.]
+
+ Synopsis [Evaluation and decomposition procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rwrDec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Rwr_CutEvaluate( Abc_ManRwr_t * p, Rwr_Cut_t * pCut );
+static void Rwr_CutDecompose( Abc_ManRwr_t * p, Rwr_Cut_t * pCut, Vec_Int_t * vForm );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs rewriting for one node.]
+
+ Description [This procedure considers all the cuts computed for the node
+ and tries to rewrite each of them using the "forest" of different AIG
+ structures precomputed and stored in the RWR manager.
+ Determines the best rewriting and computes the gain in the number of AIG
+ nodes in the final network. In the end, p->vFanins contains information
+ about the best cut that can be used for rewriting, while p->vForm gives
+ the decomposition tree (represented using factored form data structure).
+ Returns gain in the number of nodes or -1 if node cannot be rewritten.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NodeRwrRewrite( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
+{
+ Vec_Ptr_t Vector = {0,0,0}, * vFanins = &Vector;
+ Rwr_Cut_t * pCut, * pCutBest;
+ int BestGain = -1;
+ int i, Required = Vec_IntEntry( p->vReqTimes, pNode->Id );
+
+ // go through the cuts
+ for ( pCut = (Rwr_Cut_t *)pNode->pCopy, pCut = pCut->pNext; pCut; pCut = pCut->pNext )
+ {
+ // collect the TFO
+ vFanins->nSize = pCut->nLeaves;
+ vFanins->pArray = pCut->ppLeaves;
+ Abc_NodeCollectTfoCands( pNode->pNtk, pNode, vFanins, Required, p->vLevels, p->vTfo );
+ // evaluate the cut
+ Rwr_CutEvaluate( p, pCut );
+ // check if the cut is the best
+ if ( pCut->fTime && pCut->fGain )
+ {
+ pCutBest = pCut;
+ BestGain = pCut->Volume;
+ }
+ }
+ if ( BestGain == -1 )
+ return -1;
+ // we found a good cut
+
+ // prepare the fanins
+ Vec_PtrClear( p->vFanins );
+ for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
+ Vec_PtrPush( p->vFanins, pCutBest->ppLeaves[i] );
+ // collect the TFO again
+ Abc_NodeCollectTfoCands( pNode->pNtk, pNode, p->vFanins, Required, p->vLevels, p->vTfo );
+ // perform the decomposition
+ Rwr_CutDecompose( p, pCutBest, p->vForm );
+ // the best fanins are in p->vFanins, the result of decomposition is in p->vForm
+ return BestGain;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Evaluates one cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_CutEvaluate( Abc_ManRwr_t * p, Rwr_Cut_t * pCut )
+{
+}
+
+/**Function*************************************************************
+
+ Synopsis [Evaluates one cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_CutDecompose( Abc_ManRwr_t * p, Rwr_Cut_t * pCut, Vec_Int_t * vForm )
+{
+}
+
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/rwr/rwrExp.c b/src/opt/rwr/rwrExp.c
new file mode 100644
index 00000000..37eabf5b
--- /dev/null
+++ b/src/opt/rwr/rwrExp.c
@@ -0,0 +1,179 @@
+/**CFile****************************************************************
+
+ FileName [rwrExp.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting package.]
+
+ Synopsis [Computation of practically used NN-classes of 4-input cuts.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rwrExp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Abc_ManRwrExp_t_ Abc_ManRwrExp_t;
+struct Abc_ManRwrExp_t_
+{
+ // internal lookups
+ int nFuncs; // the number of four-var functions
+ unsigned short * puCanons; // canonical forms
+ int * pnCounts; // the counters of functions in each class
+ int nConsidered; // the number of nodes considered
+ int nClasses; // the number of NN classes
+};
+
+static Abc_ManRwrExp_t * s_pManRwrExp = NULL;
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+ Synopsis [Collects stats about 4-var functions appearing in netlists.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwt_ManExploreStart()
+{
+ Abc_ManRwrExp_t * p;
+ unsigned uTruth;
+ int i, k, nClasses;
+ int clk = clock();
+
+ p = ALLOC( Abc_ManRwrExp_t, 1 );
+ memset( p, 0, sizeof(Abc_ManRwrExp_t) );
+ // canonical forms
+ p->nFuncs = (1<<16);
+ p->puCanons = ALLOC( unsigned short, p->nFuncs );
+ memset( p->puCanons, 0, sizeof(unsigned short) * p->nFuncs );
+ // counters
+ p->pnCounts = ALLOC( int, p->nFuncs );
+ memset( p->pnCounts, 0, sizeof(int) * p->nFuncs );
+
+ // initialize the canonical forms
+ nClasses = 1;
+ for ( i = 1; i < p->nFuncs-1; i++ )
+ {
+ if ( p->puCanons[i] )
+ continue;
+ nClasses++;
+ for ( k = 0; k < 32; k++ )
+ {
+ uTruth = Rwr_FunctionPhase( (unsigned)i, (unsigned)k );
+ if ( p->puCanons[uTruth] == 0 )
+ p->puCanons[uTruth] = (unsigned short)i;
+ else
+ assert( p->puCanons[uTruth] == (unsigned short)i );
+ }
+ }
+ // set info for constant 1
+ p->puCanons[p->nFuncs-1] = 0;
+ printf( "The number of NN-canonical forms = %d.\n", nClasses );
+ s_pManRwrExp = p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects stats about 4-var functions appearing in netlists.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwt_ManExploreCount( unsigned uTruth )
+{
+ assert( uTruth < (1<<16) );
+ s_pManRwrExp->pnCounts[ s_pManRwrExp->puCanons[uTruth] ]++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects stats about 4-var functions appearing in netlists.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwt_ManExplorePrint()
+{
+ FILE * pFile;
+ int i, CountMax, CountWrite, nCuts, nClasses;
+ int * pDistrib;
+ int * pReprs;
+ // find the max number of occurences
+ nCuts = nClasses = 0;
+ CountMax = 0;
+ for ( i = 0; i < s_pManRwrExp->nFuncs; i++ )
+ {
+ if ( CountMax < s_pManRwrExp->pnCounts[i] )
+ CountMax = s_pManRwrExp->pnCounts[i];
+ nCuts += s_pManRwrExp->pnCounts[i];
+ if ( s_pManRwrExp->pnCounts[i] > 0 )
+ nClasses++;
+ }
+ printf( "Number of cuts considered = %8d.\n", nCuts );
+ printf( "Classes occurring at least once = %8d.\n", nClasses );
+ // print the distribution of classes
+ pDistrib = ALLOC( int, CountMax + 1 );
+ pReprs = ALLOC( int, CountMax + 1 );
+ memset( pDistrib, 0, sizeof(int)*(CountMax + 1) );
+ for ( i = 0; i < s_pManRwrExp->nFuncs; i++ )
+ {
+ pDistrib[ s_pManRwrExp->pnCounts[i] ]++;
+ pReprs[ s_pManRwrExp->pnCounts[i] ] = i;
+ }
+
+ printf( "Occurence = %6d. Num classes = %4d. \n", 0, 2288-nClasses );
+ for ( i = 1; i <= CountMax; i++ )
+ if ( pDistrib[i] )
+ {
+ printf( "Occurence = %6d. Num classes = %4d. Repr = ", i, pDistrib[i] );
+ Extra_PrintBinary( stdout, (unsigned*)&(pReprs[i]), 16 );
+ printf( "\n" );
+ }
+ free( pDistrib );
+ free( pReprs );
+ // write into a file all classes above limit (5)
+ CountWrite = 0;
+ pFile = fopen( "nnclass_stats.txt", "w" );
+ for ( i = 0; i < s_pManRwrExp->nFuncs; i++ )
+ if ( s_pManRwrExp->pnCounts[i] > 5 )
+ {
+ fprintf( pFile, "%d ", i );
+ CountWrite++;
+ }
+ fclose( pFile );
+ printf( "%d classes written into file \"%s\".\n", CountWrite, "nnclass_stats.txt" );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/rwr/rwrLib.c b/src/opt/rwr/rwrLib.c
new file mode 100644
index 00000000..91604244
--- /dev/null
+++ b/src/opt/rwr/rwrLib.c
@@ -0,0 +1,670 @@
+/**CFile****************************************************************
+
+ FileName [rwrLib.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rwrLib.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static Rwr_Node_t * Rwr_ManTryNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
+static Rwr_Node_t * Rwr_ManAddNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
+static int Rwr_ManNodeVolume( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 );
+
+static void Rwr_ManIncTravId_int( Abc_ManRwr_t * p );
+static inline void Rwr_ManIncTravId( Abc_ManRwr_t * p ) { if ( p->nTravIds++ == 0x8FFFFFFF ) Rwr_ManIncTravId_int( p ); }
+
+static void Rwr_MarkUsed_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Precomputes the forest in the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_ManPrecompute( Abc_ManRwr_t * p )
+{
+ Rwr_Node_t * p0, * p1;
+ int i, k, Level, Volume;
+ int LevelOld = -1;
+ int nNodes;
+
+ Vec_PtrForEachEntryStart( p->vForest, p0, i, 1 )
+ Vec_PtrForEachEntryStart( p->vForest, p1, k, 1 )
+ {
+ if ( LevelOld < (int)p0->Level )
+ {
+ LevelOld = p0->Level;
+ printf( "Starting level %d (at %d nodes).\n", LevelOld+1, i );
+ printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n",
+ p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
+ }
+
+ if ( k == i )
+ break;
+// if ( p0->Level + p1->Level > 6 ) // hard
+// break;
+
+ if ( p0->Level + p1->Level > 5 ) // easy
+ break;
+
+// if ( p0->Level + p1->Level > 6 || (p0->Level == 3 && p1->Level == 3) )
+// break;
+
+ // compute the level and volume of the new nodes
+ Level = 1 + ABC_MAX( p0->Level, p1->Level );
+ Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
+ // try four different nodes
+ Rwr_ManTryNode( p, p0 , p1 , 0, Level, Volume );
+ Rwr_ManTryNode( p, Rwr_Not(p0), p1 , 0, Level, Volume );
+ Rwr_ManTryNode( p, p0 , Rwr_Not(p1), 0, Level, Volume );
+ Rwr_ManTryNode( p, Rwr_Not(p0), Rwr_Not(p1), 0, Level, Volume );
+ // try EXOR
+ Rwr_ManTryNode( p, p0 , p1 , 1, Level, Volume + 1 );
+ // report the progress
+ if ( p->nConsidered % 50000000 == 0 )
+ printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n",
+ p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
+ // quit after some time
+ if ( p->vForest->nSize == RWR_LIMIT + 5 )
+ {
+ printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n",
+ p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
+ goto save;
+ }
+ }
+save :
+
+ // mark the relevant ones
+ Rwr_ManIncTravId( p );
+ k = 5;
+ nNodes = 0;
+ Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 )
+ if ( p0->uTruth == p->puCanons[p0->uTruth] )
+ {
+ Rwr_MarkUsed_rec( p, p0 );
+ nNodes++;
+ }
+
+ // compact the array by throwing away non-canonical
+ k = 5;
+ Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 )
+ if ( p0->fUsed )
+ {
+ p->vForest->pArray[k] = p0;
+ p0->Id = k;
+ k++;
+ }
+ p->vForest->nSize = k;
+ printf( "Total canonical = %4d. Total used = %5d.\n", nNodes, p->vForest->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes to file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_ManWriteToFile( Abc_ManRwr_t * p, char * pFileName )
+{
+ FILE * pFile;
+ Rwr_Node_t * pNode;
+ unsigned * pBuffer;
+ int i, nEntries, clk = clock();
+ // prepare the buffer
+ nEntries = p->vForest->nSize - 5;
+ pBuffer = ALLOC( unsigned, nEntries * 2 );
+ for ( i = 0; i < nEntries; i++ )
+ {
+ pNode = p->vForest->pArray[i+5];
+ pBuffer[2*i + 0] = (Rwr_Regular(pNode->p0)->Id << 1) | Rwr_IsComplement(pNode->p0);
+ pBuffer[2*i + 1] = (Rwr_Regular(pNode->p1)->Id << 1) | Rwr_IsComplement(pNode->p1);
+ // save EXOR flag
+ pBuffer[2*i + 0] = (pBuffer[2*i + 0] << 1) | pNode->fExor;
+
+ }
+ pFile = fopen( pFileName, "wb" );
+ fwrite( &nEntries, sizeof(int), 1, pFile );
+ fwrite( pBuffer, sizeof(unsigned), nEntries * 2, pFile );
+ free( pBuffer );
+ fclose( pFile );
+ printf( "The number of nodes saved = %d. ", nEntries ); PRT( "Saving", clock() - clk );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Loads data from file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_ManLoadFromFile( Abc_ManRwr_t * p, char * pFileName )
+{
+ FILE * pFile;
+ Rwr_Node_t * p0, * p1;
+ unsigned * pBuffer;
+ int Level, Volume, nEntries, fExor;
+ int i, clk = clock();
+
+ // load the data
+ pFile = fopen( pFileName, "rb" );
+ if ( pFile == NULL )
+ {
+ printf( "Rwr_ManLoadFromFile: Cannot open file \"%s\".\n", pFileName );
+ return;
+ }
+ fread( &nEntries, sizeof(int), 1, pFile );
+ pBuffer = ALLOC( unsigned, nEntries * 2 );
+ fread( pBuffer, sizeof(unsigned), nEntries * 2, pFile );
+ fclose( pFile );
+ // reconstruct the forest
+ for ( i = 0; i < nEntries; i++ )
+ {
+ // get EXOR flag
+ fExor = (pBuffer[2*i + 0] & 1);
+ pBuffer[2*i + 0] = (pBuffer[2*i + 0] >> 1);
+ // get the nodes
+ p0 = p->vForest->pArray[pBuffer[2*i + 0] >> 1];
+ p1 = p->vForest->pArray[pBuffer[2*i + 1] >> 1];
+ // compute the level and volume of the new nodes
+ Level = 1 + ABC_MAX( p0->Level, p1->Level );
+ Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
+ // set the complemented attributes
+ p0 = Rwr_NotCond( p0, (pBuffer[2*i + 0] & 1) );
+ p1 = Rwr_NotCond( p1, (pBuffer[2*i + 1] & 1) );
+ // add the node
+// Rwr_ManTryNode( p, p0, p1, Level, Volume );
+ Rwr_ManAddNode( p, p0, p1, fExor, Level, Volume + fExor );
+ }
+ free( pBuffer );
+ printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
+ printf( "The number of nodes loaded = %d. ", nEntries ); PRT( "Loading", clock() - clk );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_ManIncTravId_int( Abc_ManRwr_t * p )
+{
+ Rwr_Node_t * pNode;
+ int i;
+ Vec_PtrForEachEntry( p->vForest, pNode, i )
+ pNode->TravId = 0;
+ p->nTravIds = 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_MarkUsed_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode )
+{
+ if ( pNode->fUsed || pNode->TravId == p->nTravIds )
+ return;
+ pNode->TravId = p->nTravIds;
+ pNode->fUsed = 1;
+ Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p0) );
+ Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p1) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_Trav_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode, int * pVolume )
+{
+ if ( pNode->fMark || pNode->TravId == p->nTravIds )
+ return;
+ pNode->TravId = p->nTravIds;
+ (*pVolume)++;
+ if ( pNode->fExor )
+ (*pVolume)++;
+ Rwr_Trav_rec( p, Rwr_Regular(pNode->p0), pVolume );
+ Rwr_Trav_rec( p, Rwr_Regular(pNode->p1), pVolume );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_Trav2_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode, int * pVolume )
+{
+ if ( pNode->fMark || pNode->TravId == p->nTravIds )
+ return;
+ pNode->TravId = p->nTravIds;
+ (*pVolume)++;
+ Rwr_Trav2_rec( p, Rwr_Regular(pNode->p0), pVolume );
+ Rwr_Trav2_rec( p, Rwr_Regular(pNode->p1), pVolume );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rwr_ManNodeVolume( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 )
+{
+ int Volume = 0;
+ Rwr_ManIncTravId( p );
+ Rwr_Trav_rec( p, p0, &Volume );
+ Rwr_Trav_rec( p, p1, &Volume );
+ return Volume;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Rwr_Node_t * Rwr_ManTryNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
+{
+ Rwr_Node_t * pOld, * pNew, ** ppPlace;
+ unsigned uTruth, uCanon;
+ // compute truth table, level, volume
+ p->nConsidered++;
+ if ( fExor )
+ {
+// printf( "Considering EXOR of %d and %d.\n", p0->Id, p1->Id );
+ uTruth = (p0->uTruth ^ p1->uTruth);
+ }
+ else
+ uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) &
+ (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
+ uCanon = p->puCanons[uTruth];
+ // skip non-practical classes
+ if ( Level > 2 && p->pPractical[uCanon] == 0 )
+ return NULL;
+ // enumerate through the nodes with the same canonical form
+ ppPlace = p->pTable + uCanon;
+ for ( pOld = *ppPlace; pOld; ppPlace = &pOld->pNext, pOld = pOld->pNext )
+ {
+ if ( pOld->Level < (unsigned)Level && pOld->Volume < (unsigned)Volume )
+ return NULL;
+ if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
+ return NULL;
+// if ( pOld->Level < (unsigned)Level && pOld->Volume == (unsigned)Volume )
+// return NULL;
+ }
+// if ( fExor )
+// printf( "Adding EXOR of %d and %d.\n", p0->Id, p1->Id );
+ // create the new node
+ pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
+ pNew->Id = p->vForest->nSize;
+ pNew->TravId = 0;
+ pNew->uTruth = uTruth;
+ pNew->Level = Level;
+ pNew->Volume = Volume;
+ pNew->fMark = 0;
+ pNew->fUsed = 0;
+ pNew->fExor = fExor;
+ pNew->p0 = p0;
+ pNew->p1 = p1;
+ pNew->pNext = NULL;
+ Vec_PtrPush( p->vForest, pNew );
+ *ppPlace = pNew;
+ if ( p->pTable[uCanon] == pNew )
+ p->nClasses++;
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Rwr_Node_t * Rwr_ManAddNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
+{
+ Rwr_Node_t * pOld, * pNew;
+ unsigned uTruth, uCanon;
+ // compute truth table, leve, volume
+ p->nConsidered++;
+ if ( fExor )
+ uTruth = (p0->uTruth ^ p1->uTruth);
+ else
+ uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) &
+ (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
+ uCanon = p->puCanons[uTruth];
+ // skip non-practical classes
+// if ( p->pPractical[uCanon] == 0 )
+// return NULL;
+ // create the new node
+ pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
+ pNew->Id = p->vForest->nSize;
+ pNew->TravId = 0;
+ pNew->uTruth = uTruth;
+ pNew->Level = Level;
+ pNew->Volume = Volume;
+ pNew->fMark = 0;
+ pNew->fUsed = 0;
+ pNew->fExor = fExor;
+ pNew->p0 = p0;
+ pNew->p1 = p1;
+ pNew->pNext = NULL;
+ Vec_PtrPush( p->vForest, pNew );
+ // do not add if the node is not essential
+ if ( uTruth != uCanon )
+ return pNew;
+
+ // add to the list
+ p->nAdded++;
+ pOld = p->pTable[uCanon];
+ if ( pOld == NULL )
+ p->nClasses++;
+ pNew->pNext = pOld;
+ p->pTable[uCanon] = pNew;
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Rwr_Node_t * Rwr_ManAddVar( Abc_ManRwr_t * p, unsigned uTruth )
+{
+ Rwr_Node_t * pNew;
+ pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
+ pNew->Id = p->vForest->nSize;
+ pNew->TravId = 0;
+ pNew->uTruth = uTruth;
+ pNew->Level = 0;
+ pNew->Volume = 0;
+ pNew->fMark = 1;
+ pNew->fUsed = 1;
+ pNew->fExor = 0;
+ pNew->p0 = NULL;
+ pNew->p1 = NULL; pNew->pNext = NULL;
+ Vec_PtrPush( p->vForest, pNew );
+ assert( p->pTable[p->puCanons[uTruth]] == NULL );
+ p->pTable[p->puCanons[uTruth]] = pNew;
+ return pNew;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Prints one rwr node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_NodePrint_rec( FILE * pFile, Rwr_Node_t * pNode )
+{
+ assert( !Rwr_IsComplement(pNode) );
+
+ if ( pNode->Id == 0 )
+ {
+ fprintf( pFile, "Const1" );
+ return;
+ }
+
+ if ( pNode->Id < 5 )
+ {
+ fprintf( pFile, "%c", 'a' + pNode->Id - 1 );
+ return;
+ }
+
+ if ( Rwr_IsComplement(pNode->p0) )
+ {
+ if ( Rwr_Regular(pNode->p0)->Id < 5 )
+ {
+ Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p0) );
+ fprintf( pFile, "\'" );
+ }
+ else
+ {
+ fprintf( pFile, "(" );
+ Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p0) );
+ fprintf( pFile, ")\'" );
+ }
+ }
+ else
+ {
+ if ( Rwr_Regular(pNode->p0)->Id < 5 )
+ {
+ Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p0) );
+ }
+ else
+ {
+ fprintf( pFile, "(" );
+ Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p0) );
+ fprintf( pFile, ")" );
+ }
+ }
+
+ if ( pNode->fExor )
+ fprintf( pFile, "+" );
+
+ if ( Rwr_IsComplement(pNode->p1) )
+ {
+ if ( Rwr_Regular(pNode->p1)->Id < 5 )
+ {
+ Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p1) );
+ fprintf( pFile, "\'" );
+ }
+ else
+ {
+ fprintf( pFile, "(" );
+ Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p1) );
+ fprintf( pFile, ")\'" );
+ }
+ }
+ else
+ {
+ if ( Rwr_Regular(pNode->p1)->Id < 5 )
+ {
+ Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p1) );
+ }
+ else
+ {
+ fprintf( pFile, "(" );
+ Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p1) );
+ fprintf( pFile, ")" );
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints one rwr node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_NodePrint( FILE * pFile, Abc_ManRwr_t * p, Rwr_Node_t * pNode )
+{
+ unsigned uTruth;
+ fprintf( pFile, "%5d :", pNode->Id );
+ fprintf( pFile, " tt=", pNode->Id );
+ uTruth = pNode->uTruth;
+ Extra_PrintBinary( pFile, &uTruth, 16 );
+ fprintf( pFile, " cn=", pNode->Id );
+ uTruth = p->puCanons[pNode->uTruth];
+ Extra_PrintBinary( pFile, &uTruth, 16 );
+ fprintf( pFile, " lev=%d", pNode->Level );
+ fprintf( pFile, " vol=%d", pNode->Volume );
+ fprintf( pFile, " " );
+ Rwr_NodePrint_rec( pFile, pNode );
+ fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints one rwr node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_ManPrint( Abc_ManRwr_t * p )
+{
+/*
+ Rwr_Node_t * pNode;
+ unsigned uTruth;
+ int Limit = 4;
+ int i;
+
+ for ( i = 0; i < p->nFuncs; i++ )
+ {
+ if ( p->pTable[i] == NULL )
+ continue;
+ if ( Limit-- == 0 )
+ break;
+ printf( "\nClass " );
+ uTruth = i;
+ Extra_PrintBinary( stdout, &uTruth, 16 );
+ printf( "\n" );
+ for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
+ if ( pNode->uTruth == p->puCanons[pNode->uTruth] )
+ Rwr_NodePrint( p, pNode );
+ }
+*/
+ FILE * pFile;
+ Rwr_Node_t * pNode;
+ unsigned uTruth;
+ int Limit = 4;
+ int Counter;
+ int i;
+
+ pFile = fopen( "graph_lib.txt", "w" );
+
+ Counter = 0;
+ for ( i = 0; i < p->nFuncs; i++ )
+ {
+ if ( p->pTable[i] == NULL )
+ continue;
+// if ( Limit-- == 0 )
+// break;
+ fprintf( pFile, "\nClass %3d ", Counter++ );
+
+ // count the volume of the bush
+ {
+ int Volume = 0;
+ int nFuncs = 0;
+ Rwr_ManIncTravId( p );
+ for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
+ if ( pNode->uTruth == p->puCanons[pNode->uTruth] )
+ {
+ nFuncs++;
+ Rwr_Trav2_rec( p, pNode, &Volume );
+ }
+ fprintf( pFile, "Functions = %2d. Volume = %2d. ", nFuncs, Volume );
+ }
+
+ uTruth = i;
+ Extra_PrintBinary( pFile, &uTruth, 16 );
+ fprintf( pFile, "\n" );
+
+ for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
+ if ( pNode->uTruth == p->puCanons[pNode->uTruth] )
+ Rwr_NodePrint( pFile, p, pNode );
+ }
+
+ fclose( pFile );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
new file mode 100644
index 00000000..46752696
--- /dev/null
+++ b/src/opt/rwr/rwrMan.c
@@ -0,0 +1,311 @@
+/**CFile****************************************************************
+
+ FileName [rwrMan.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rwrMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// the following information was derived by computing all 4-input cuts of IWLS, MCNC, and ISCAS benchmarks
+#define RWR_NUM_CLASSES 775
+static int s_PracticalClasses[RWR_NUM_CLASSES] = {
+ 0, 1, 3, 5, 6, 7, 15, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 51, 53, 54, 55, 60, 61, 63, 85, 86,
+ 87, 90, 91, 95, 102, 103, 105, 107, 111, 119, 123, 125, 126, 127, 255, 257, 258, 259, 260, 261, 262, 263, 264, 265,
+ 266, 267, 268, 269, 270, 271, 272, 273, 274, 275, 276, 277, 278, 281, 282, 284, 286, 287, 288, 289, 290, 291, 293, 297,
+ 298, 299, 300, 302, 303, 304, 305, 306, 307, 308, 310, 311, 312, 313, 315, 316, 317, 319, 320, 321, 323, 324, 325, 329,
+ 332, 334, 335, 336, 337, 338, 340, 341, 342, 343, 345, 347, 349, 351, 352, 357, 358, 359, 361, 367, 368, 369, 371,
+ 373, 375, 379, 381, 383, 384, 385, 386, 388, 389, 392, 393, 395, 397, 399, 400, 404, 408, 409, 416, 417, 419, 420,
+ 421, 424, 425, 426, 427, 431, 433, 443, 448, 449, 451, 453, 456, 457, 459, 460, 461, 462, 463, 465, 476, 477, 480,
+ 481, 483, 489, 492, 493, 494, 495, 496, 497, 499, 500, 501, 506, 507, 508, 509, 510, 771, 773, 774, 775, 780, 781,
+ 783, 785, 786, 787, 788, 790, 791, 792, 796, 797, 799, 816, 817, 819, 820, 821, 834, 835, 836, 837, 838, 839, 840,
+ 844, 847, 848, 849, 850, 851, 852, 853, 854, 855, 856, 859, 860, 861, 863, 864, 867, 870, 871, 876, 878, 880, 883,
+ 884, 885, 887, 967, 973, 975, 979, 984, 988, 989, 990, 1009, 1011, 1012, 1013, 1020, 1285, 1286, 1287, 1290, 1291,
+ 1295, 1297, 1298, 1300, 1301, 1303, 1307, 1308, 1309, 1311, 1314, 1316, 1317, 1318, 1319, 1322, 1325, 1327, 1329,
+ 1330, 1331, 1332, 1333, 1334, 1335, 1336, 1338, 1340, 1341, 1360, 1361, 1363, 1365, 1367, 1380, 1381, 1382, 1383,
+ 1390, 1392, 1395, 1397, 1399, 1440, 1445, 1447, 1450, 1451, 1455, 1458, 1461, 1463, 1467, 1525, 1530, 1542, 1543,
+ 1545, 1547, 1551, 1553, 1554, 1558, 1559, 1561, 1567, 1569, 1570, 1572, 1574, 1576, 1587, 1588, 1590, 1591, 1596,
+ 1618, 1620, 1621, 1623, 1624, 1632, 1638, 1641, 1647, 1654, 1655, 1680, 1686, 1687, 1689, 1695, 1718, 1776, 1782,
+ 1785, 1799, 1803, 1805, 1806, 1807, 1811, 1813, 1815, 1823, 1826, 1831, 1843, 1844, 1847, 1859, 1860, 1863, 1875,
+ 1877, 1879, 1895, 1902, 1904, 1911, 1912, 1927, 1928, 1933, 1935, 1945, 1956, 1957, 1959, 1962, 1964, 1965, 1975,
+ 1979, 1987, 1991, 1995, 1996, 2000, 2002, 2007, 2013, 2023, 2032, 2040, 3855, 3857, 3859, 3861, 3864, 3866, 3867,
+ 3868, 3869, 3870, 3891, 3892, 3893, 3900, 3921, 3925, 3942, 3945, 3956, 3960, 4080, 4369, 4370, 4371, 4372, 4373,
+ 4374, 4375, 4376, 4377, 4378, 4379, 4380, 4381, 4382, 4386, 4387, 4388, 4389, 4391, 4392, 4394, 4396, 4403, 4405,
+ 4408, 4409, 4411, 4420, 4421, 4422, 4423, 4424, 4426, 4428, 4437, 4439, 4445, 4488, 4494, 4505, 4507, 4509, 4522,
+ 4524, 4525, 4526, 4539, 4540, 4542, 4556, 4557, 4573, 4574, 4590, 4626, 4627, 4629, 4630, 4631, 4632, 4634, 4638,
+ 4641, 4643, 4648, 4659, 4680, 4695, 4698, 4702, 4713, 4731, 4740, 4758, 4766, 4773, 4791, 4812, 4830, 4845, 4883,
+ 4885, 4887, 4888, 4891, 4892, 4899, 4903, 4913, 4914, 4915, 4934, 4940, 4945, 4947, 4949, 4951, 4972, 5005, 5011,
+ 5017, 5019, 5029, 5043, 5049, 5058, 5059, 5060, 5068, 5075, 5079, 5083, 5084, 5100, 5140, 5141, 5142, 5143, 5148,
+ 5160, 5171, 5174, 5180, 5182, 5185, 5186, 5187, 5189, 5205, 5207, 5214, 5238, 5245, 5246, 5250, 5270, 5278, 5290,
+ 5310, 5315, 5335, 5355, 5397, 5399, 5401, 5402, 5405, 5413, 5414, 5415, 5418, 5427, 5429, 5445, 5457, 5460, 5461,
+ 5463, 5469, 5482, 5522, 5525, 5533, 5540, 5546, 5557, 5565, 5571, 5580, 5589, 5593, 5605, 5610, 5654, 5673, 5692,
+ 5698, 5729, 5734, 5782, 5790, 5796, 5814, 5826, 5846, 5911, 5931, 5965, 6001, 6066, 6120, 6168, 6174, 6180, 6206,
+ 6210, 6229, 6234, 6270, 6273, 6279, 6363, 6375, 6425, 6427, 6438, 6446, 6451, 6457, 6478, 6482, 6485, 6489, 6502,
+ 6545, 6553, 6564, 6570, 6594, 6617, 6630, 6682, 6683, 6685, 6686, 6693, 6709, 6741, 6746, 6817, 6821, 6826, 6833,
+ 6849, 6885, 6939, 6940, 6951, 6963, 6969, 6990, 6997, 7065, 7077, 7089, 7140, 7196, 7212, 7219, 7220, 7228, 7230,
+ 7251, 7324, 7356, 7361, 7363, 7372, 7377, 7395, 7453, 7470, 7475, 7495, 7509, 7513, 7526, 7619, 7633, 7650, 7710,
+ 7725, 7731, 7740, 7755, 7770, 7800, 7815, 7830, 7845, 7860, 7890, 7905, 13107, 13109, 13110, 13116, 13141, 13146,
+ 13161, 13164, 13621, 13622, 13626, 13651, 13653, 13658, 13669, 13670, 13763, 13765, 13770, 13878, 13881, 13884,
+ 13910, 13923, 13926, 13932, 13971, 13974, 13980, 14022, 14025, 15420, 15445, 15450, 15462, 15465, 15555, 21845,
+ 21846, 21850, 21865, 21866, 21930, 22102, 22105, 22106, 22117, 22118, 22122, 22165, 22166, 22169, 22170, 22181,
+ 22182, 22185, 23130, 23142, 23145, 23205, 26214, 26217, 26985, 27030
+};
+
+static unsigned short Rwr_FunctionPerm( unsigned uTruth, int Phase );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Starts the resynthesis manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_ManRwr_t * Abc_NtkManRwrStart( char * pFileName )
+{
+ Abc_ManRwr_t * p;
+ unsigned uTruth;
+ int i, k, nClasses;
+ int clk = clock();
+
+ p = ALLOC( Abc_ManRwr_t, 1 );
+ memset( p, 0, sizeof(Abc_ManRwr_t) );
+ // canonical forms
+ p->nFuncs = (1<<16);
+ p->puCanons = ALLOC( unsigned short, p->nFuncs );
+ memset( p->puCanons, 0, sizeof(unsigned short) * p->nFuncs );
+ // permutations
+ p->puPhases = ALLOC( char, p->nFuncs );
+ memset( p->puPhases, 0, sizeof(char) * p->nFuncs );
+ // hash table
+ p->pTable = ALLOC( Rwr_Node_t *, p->nFuncs );
+ memset( p->pTable, 0, sizeof(Rwr_Node_t *) * p->nFuncs );
+ // practical classes
+ p->pPractical = ALLOC( char, p->nFuncs );
+ memset( p->pPractical, 0, sizeof(char) * p->nFuncs );
+ // other stuff
+ p->vForest = Vec_PtrAlloc( 100 );
+ p->vForm = Vec_IntAlloc( 50 );
+ p->vFanins = Vec_PtrAlloc( 50 );
+ p->vTfo = Vec_PtrAlloc( 50 );
+ p->vLevels = Vec_VecAlloc( 50 );
+ p->pMmNode = Extra_MmFixedStart( sizeof(Rwr_Node_t) );
+ p->nTravIds = 1;
+ assert( sizeof(Rwr_Node_t) == sizeof(Rwr_Cut_t) );
+
+ // initialize the canonical forms
+ nClasses = 1;
+ for ( i = 1; i < p->nFuncs-1; i++ )
+ {
+ if ( p->puCanons[i] )
+ continue;
+ nClasses++;
+ for ( k = 0; k < 32; k++ )
+ {
+ uTruth = Rwr_FunctionPhase( (unsigned)i, (unsigned)k );
+ if ( p->puCanons[uTruth] == 0 )
+ {
+ p->puCanons[uTruth] = (unsigned short)i;
+ p->puPhases[uTruth] = (char)k;
+ }
+ else
+ assert( p->puCanons[uTruth] == (unsigned short)i );
+ }
+ }
+ // set info for constant 1
+ p->puCanons[p->nFuncs-1] = 0;
+ p->puPhases[p->nFuncs-1] = 16;
+ printf( "The number of NN-canonical forms = %d.\n", nClasses );
+
+ // initialize permutations
+ for ( i = 0; i < 256; i++ )
+ for ( k = 0; k < 16; k++ )
+ p->puPerms[i][k] = Rwr_FunctionPerm( i, k );
+
+ // initialize practical classes
+ for ( i = 0; i < RWR_NUM_CLASSES; i++ )
+ p->pPractical[ s_PracticalClasses[i] ] = 1;
+
+ // initialize forest
+ Rwr_ManAddVar( p, 0xFFFF ); // constant 1
+ Rwr_ManAddVar( p, 0xAAAA ); // var A
+ Rwr_ManAddVar( p, 0xCCCC ); // var B
+ Rwr_ManAddVar( p, 0xF0F0 ); // var C
+ Rwr_ManAddVar( p, 0xFF00 ); // var D
+ p->nClasses = 5;
+PRT( "Manager startup time", clock() - clk );
+
+ // create the nodes
+ if ( pFileName == NULL )
+ { // precompute
+ Rwr_ManPrecompute( p );
+ Rwr_ManWriteToFile( p, "data.aaa" );
+ }
+ else
+ { // load previously saved nodes
+ Rwr_ManLoadFromFile( p, pFileName );
+ }
+ Rwr_ManPrint( p );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the resynthesis manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkManRwrStop( Abc_ManRwr_t * p )
+{
+ if ( p->vFanNums ) Vec_IntFree( p->vFanNums );
+ if ( p->vReqTimes ) Vec_IntFree( p->vReqTimes );
+ Vec_IntFree( p->vForm );
+ Vec_PtrFree( p->vFanins );
+ Vec_PtrFree( p->vTfo );
+ Vec_VecFree( p->vLevels );
+ Vec_PtrFree( p->vForest );
+ Extra_MmFixedStop( p->pMmNode, 0 );
+ free( p->pPractical );
+ free( p->puCanons );
+ free( p->puPhases );
+ free( p->pTable );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the resynthesis manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkManRwrDecs( Abc_ManRwr_t * p )
+{
+ return p->vForm;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the resynthesis manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkManRwrFanins( Abc_ManRwr_t * p )
+{
+ return p->vFanins;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes a phase of the 4-var function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned short Rwr_FunctionPhase( unsigned uTruth, unsigned uPhase )
+{
+ static unsigned uMasks0[4] = { 0x5555, 0x3333, 0x0F0F, 0x00FF };
+ static unsigned uMasks1[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
+ int v, Shift;
+ for ( v = 0, Shift = 1; v < 4; v++, Shift <<= 1 )
+ if ( uPhase & Shift )
+ uTruth = (((uTruth & uMasks0[v]) << Shift) | ((uTruth & uMasks1[v]) >> Shift));
+ if ( uPhase & 16 )
+ uTruth = ~uTruth & 0xFFFF;
+ return uTruth;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes a phase of the 3-var function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned short Rwr_FunctionPerm( unsigned uTruth, int Phase )
+{
+ static int Perm[16][4] = {
+ { 0, 1, 2, 3 }, // 0000 - skip
+ { 0, 1, 2, 3 }, // 0001 - skip
+ { 1, 0, 2, 3 }, // 0010
+ { 0, 1, 2, 3 }, // 0011 - skip
+ { 2, 1, 0, 3 }, // 0100
+ { 0, 2, 1, 3 }, // 0101
+ { 2, 0, 1, 3 }, // 0110
+ { 0, 1, 2, 3 }, // 0111 - skip
+ { 3, 1, 2, 0 }, // 1000
+ { 0, 3, 2, 1 }, // 1001
+ { 3, 0, 2, 1 }, // 1010
+ { 0, 1, 3, 2 }, // 1011
+ { 2, 3, 0, 1 }, // 1100
+ { 0, 3, 1, 2 }, // 1101
+ { 3, 0, 1, 2 }, // 1110
+ { 0, 1, 2, 3 } // 1111 - skip
+ };
+ int i, k, iRes;
+ unsigned uTruthRes;
+ assert( Phase < 16 );
+ uTruthRes = 0;
+ for ( i = 0; i < 16; i++ )
+ if ( uTruth & (1 << i) )
+ {
+ for ( iRes = 0, k = 0; k < 4; k++ )
+ if ( i & (1 << k) )
+ iRes |= (1 << Perm[Phase][k]);
+ uTruthRes |= (1 << iRes);
+ }
+ return uTruthRes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/rwr/rwrUtil.c b/src/opt/rwr/rwrUtil.c
new file mode 100644
index 00000000..ae8665ef
--- /dev/null
+++ b/src/opt/rwr/rwrUtil.c
@@ -0,0 +1,102 @@
+/**CFile****************************************************************
+
+ FileName [rwrUtil.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting package.]
+
+ Synopsis [Various utilities.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rwrUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Creates the array of fanout counters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk )
+{
+ Vec_Int_t * vFanNums;
+ Abc_Obj_t * pObj;
+ int i;
+ vFanNums = Vec_IntAlloc( 0 );
+ Vec_IntFill( vFanNums, Abc_NtkObjNumMax(pNtk), -1 );
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if ( Abc_ObjIsNode( pObj ) )
+ Vec_IntWriteEntry( vFanNums, i, Abc_ObjFanoutNum(pObj) );
+ return vFanNums;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the array of required times.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Rwt_NtkRequiredLevels( Abc_Ntk_t * pNtk )
+{
+ Vec_Int_t * vReqTimes;
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pObj, * pFanout;
+ int i, k, nLevelsMax, nLevelsCur;
+ // start the required times
+ vReqTimes = Vec_IntAlloc( 0 );
+ Vec_IntFill( vReqTimes, Abc_NtkObjNumMax(pNtk), ABC_INFINITY );
+ // compute levels in reverse topological order
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Vec_IntWriteEntry( vReqTimes, pObj->Id, 0 );
+ vNodes = Abc_NtkDfsReverse( pNtk );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ nLevelsCur = 0;
+ Abc_ObjForEachFanout( pObj, pFanout, k )
+ if ( nLevelsCur < Vec_IntEntry(vReqTimes, pFanout->Id) )
+ nLevelsCur = Vec_IntEntry(vReqTimes, pFanout->Id);
+ Vec_IntWriteEntry( vReqTimes, pObj->Id, nLevelsCur + 1 );
+ }
+ Vec_PtrFree( vNodes );
+ // convert levels into required times: RetTime = NumLevels + 1 - Level
+ nLevelsMax = Abc_AigGetLevelNum(pNtk) + 1;
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ Vec_IntWriteEntry( vReqTimes, pObj->Id, nLevelsMax - Vec_IntEntry(vReqTimes, pObj->Id) );
+// Abc_NtkForEachNode( pNtk, pObj, i )
+// printf( "(%d,%d)", pObj->Level, Vec_IntEntry(vReqTimes, pObj->Id) );
+// printf( "\n" );
+ return vReqTimes;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+