src/opt/rwr/rwr.h File Reference

#include "abc.h"
#include "cut.h"
Include dependency graph for rwr.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  Rwr_Man_t_
struct  Rwr_Node_t_

Defines

#define RWR_LIMIT   1048576/4

Typedefs

typedef struct Rwr_Man_t_ Rwr_Man_t
typedef struct Rwr_Node_t_ Rwr_Node_t

Functions

static bool Rwr_IsComplement (Rwr_Node_t *p)
static Rwr_Node_tRwr_Regular (Rwr_Node_t *p)
static Rwr_Node_tRwr_Not (Rwr_Node_t *p)
static Rwr_Node_tRwr_NotCond (Rwr_Node_t *p, int c)
void Rwr_ManPreprocess (Rwr_Man_t *p)
int Rwr_NodeRewrite (Rwr_Man_t *p, Cut_Man_t *pManCut, Abc_Obj_t *pNode, int fUpdateLevel, int fUseZeros, int fPlaceEnable)
void Rwr_ScoresClean (Rwr_Man_t *p)
void Rwr_ScoresReport (Rwr_Man_t *p)
void Rwr_ManPrecompute (Rwr_Man_t *p)
Rwr_Node_tRwr_ManAddVar (Rwr_Man_t *p, unsigned uTruth, int fPrecompute)
Rwr_Node_tRwr_ManAddNode (Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1, int fExor, int Level, int Volume)
int Rwr_ManNodeVolume (Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1)
void Rwr_ManIncTravId (Rwr_Man_t *p)
Rwr_Man_tRwr_ManStart (bool fPrecompute)
void Rwr_ManStop (Rwr_Man_t *p)
void Rwr_ManPrintStats (Rwr_Man_t *p)
void Rwr_ManPrintStatsFile (Rwr_Man_t *p)
void * Rwr_ManReadDecs (Rwr_Man_t *p)
Vec_Ptr_tRwr_ManReadLeaves (Rwr_Man_t *p)
int Rwr_ManReadCompl (Rwr_Man_t *p)
void Rwr_ManAddTimeCuts (Rwr_Man_t *p, int Time)
void Rwr_ManAddTimeUpdate (Rwr_Man_t *p, int Time)
void Rwr_ManAddTimeTotal (Rwr_Man_t *p, int Time)
void Rwr_ManPrint (Rwr_Man_t *p)
void Rwr_ManWriteToArray (Rwr_Man_t *p)
void Rwr_ManLoadFromArray (Rwr_Man_t *p, int fVerbose)
void Rwr_ManWriteToFile (Rwr_Man_t *p, char *pFileName)
void Rwr_ManLoadFromFile (Rwr_Man_t *p, char *pFileName)
void Rwr_ListAddToTail (Rwr_Node_t **ppList, Rwr_Node_t *pNode)
char * Rwr_ManGetPractical (Rwr_Man_t *p)

Define Documentation

#define RWR_LIMIT   1048576/4

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

] INCLUDES /// PARAMETERS /// BASIC TYPES ///

Definition at line 43 of file rwr.h.


Typedef Documentation

typedef struct Rwr_Man_t_ Rwr_Man_t

Definition at line 45 of file rwr.h.

typedef struct Rwr_Node_t_ Rwr_Node_t

Definition at line 46 of file rwr.h.


Function Documentation

static bool Rwr_IsComplement ( Rwr_Node_t p  )  [inline, static]

Definition at line 114 of file rwr.h.

00114 { return (bool)(((unsigned long)p) & 01);           }

void Rwr_ListAddToTail ( Rwr_Node_t **  ppList,
Rwr_Node_t pNode 
)

Function*************************************************************

Synopsis [Adds the node to the end of the list.]

Description []

SideEffects []

SeeAlso []

Definition at line 238 of file rwrUtil.c.

00239 {
00240     Rwr_Node_t * pTemp;
00241     // find the last one
00242     for ( pTemp = *ppList; pTemp; pTemp = pTemp->pNext )
00243         ppList = &pTemp->pNext;
00244     // attach at the end
00245     *ppList = pNode;
00246 }

Rwr_Node_t* Rwr_ManAddNode ( Rwr_Man_t p,
Rwr_Node_t p0,
Rwr_Node_t p1,
int  fExor,
int  Level,
int  Volume 
)

Function*************************************************************

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 203 of file rwrLib.c.

00204 {
00205     Rwr_Node_t * pNew;
00206     unsigned uTruth;
00207     // compute truth table, leve, volume
00208     p->nConsidered++;
00209     if ( fExor )
00210         uTruth = (p0->uTruth ^ p1->uTruth);
00211     else
00212         uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 
00213                  (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
00214     // create the new node
00215     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
00216     pNew->Id     = p->vForest->nSize;
00217     pNew->TravId = 0;
00218     pNew->uTruth = uTruth;
00219     pNew->Level  = Level;
00220     pNew->Volume = Volume;
00221     pNew->fUsed  = 0;
00222     pNew->fExor  = fExor;
00223     pNew->p0     = p0;
00224     pNew->p1     = p1;
00225     pNew->pNext  = NULL;
00226     Vec_PtrPush( p->vForest, pNew );
00227     // do not add if the node is not essential
00228     if ( uTruth != p->puCanons[uTruth] )
00229         return pNew;
00230 
00231     // add to the list
00232     p->nAdded++;
00233     if ( p->pTable[uTruth] == NULL )
00234         p->nClasses++;
00235     Rwr_ListAddToTail( p->pTable + uTruth, pNew );
00236     return pNew;
00237 }

void Rwr_ManAddTimeCuts ( Rwr_Man_t p,
int  Time 
)

Function*************************************************************

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 258 of file rwrMan.c.

00259 {
00260     p->timeCut += Time;
00261 }

void Rwr_ManAddTimeTotal ( Rwr_Man_t p,
int  Time 
)

Function*************************************************************

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 290 of file rwrMan.c.

00291 {
00292     p->timeTotal += Time;
00293 }

void Rwr_ManAddTimeUpdate ( Rwr_Man_t p,
int  Time 
)

Function*************************************************************

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 274 of file rwrMan.c.

00275 {
00276     p->timeUpdate += Time;
00277 }

Rwr_Node_t* Rwr_ManAddVar ( Rwr_Man_t p,
unsigned  uTruth,
int  fPrecompute 
)

Function*************************************************************

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 250 of file rwrLib.c.

00251 {
00252     Rwr_Node_t * pNew;
00253     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
00254     pNew->Id     = p->vForest->nSize;
00255     pNew->TravId = 0;
00256     pNew->uTruth = uTruth;
00257     pNew->Level  = 0;
00258     pNew->Volume = 0;
00259     pNew->fUsed  = 1;
00260     pNew->fExor  = 0;
00261     pNew->p0     = NULL;
00262     pNew->p1     = NULL;    
00263     pNew->pNext  = NULL;
00264     Vec_PtrPush( p->vForest, pNew );
00265     if ( fPrecompute )
00266         Rwr_ListAddToTail( p->pTable + uTruth, pNew );
00267     return pNew;
00268 }

char* Rwr_ManGetPractical ( Rwr_Man_t p  ) 

Function*************************************************************

Synopsis [Create practical classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file rwrUtil.c.

00260 {
00261     char * pPractical;
00262     int i;
00263     pPractical = ALLOC( char, p->nFuncs );
00264     memset( pPractical, 0, sizeof(char) * p->nFuncs );
00265     pPractical[0] = 1;
00266     for ( i = 1; ; i++ )
00267     {
00268         if ( s_RwrPracticalClasses[i] == 0 )
00269             break;
00270         pPractical[ s_RwrPracticalClasses[i] ] = 1;
00271     }
00272     return pPractical;
00273 }

void Rwr_ManIncTravId ( Rwr_Man_t p  ) 

Function*************************************************************

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 347 of file rwrLib.c.

00348 {
00349     Rwr_Node_t * pNode;
00350     int i;
00351     if ( p->nTravIds++ < 0x8FFFFFFF )
00352         return;
00353     Vec_PtrForEachEntry( p->vForest, pNode, i )
00354         pNode->TravId = 0;
00355     p->nTravIds = 1;
00356 }

void Rwr_ManLoadFromArray ( Rwr_Man_t p,
int  fVerbose 
)

Function*************************************************************

Synopsis [Loads data.]

Description []

SideEffects []

SeeAlso []

Definition at line 95 of file rwrUtil.c.

00096 {
00097     unsigned short * pArray = s_RwtAigSubgraphs;
00098     Rwr_Node_t * p0, * p1;
00099     unsigned Entry0, Entry1;
00100     int Level, Volume, nEntries, fExor;
00101     int i, clk = clock();
00102 
00103     // reconstruct the forest
00104     for ( i = 0; ; i++ )
00105     {
00106         Entry0 = pArray[2*i + 0];
00107         Entry1 = pArray[2*i + 1];
00108         if ( Entry0 == 0 && Entry1 == 0 )
00109             break;
00110         // get EXOR flag
00111         fExor = (Entry0 & 1);
00112         Entry0 >>= 1;
00113         // get the nodes
00114         p0 = p->vForest->pArray[Entry0 >> 1];
00115         p1 = p->vForest->pArray[Entry1 >> 1];
00116         // compute the level and volume of the new nodes
00117         Level  = 1 + ABC_MAX( p0->Level, p1->Level );
00118         Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
00119         // set the complemented attributes
00120         p0 = Rwr_NotCond( p0, (Entry0 & 1) );
00121         p1 = Rwr_NotCond( p1, (Entry1 & 1) );
00122         // add the node
00123 //        Rwr_ManTryNode( p, p0, p1, Level, Volume );
00124         Rwr_ManAddNode( p, p0, p1, fExor, Level, Volume + fExor );
00125     }
00126     nEntries = i - 1;
00127     if ( fVerbose )
00128     {
00129         printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
00130         printf( "The number of nodes loaded = %d.  ", nEntries );  PRT( "Loading", clock() - clk );
00131     }
00132 }

void Rwr_ManLoadFromFile ( Rwr_Man_t p,
char *  pFileName 
)

Function*************************************************************

Synopsis [Loads data.]

Description []

SideEffects []

SeeAlso []

Definition at line 183 of file rwrUtil.c.

00184 {
00185     FILE * pFile;
00186     Rwr_Node_t * p0, * p1;
00187     unsigned * pBuffer;
00188     int Level, Volume, nEntries, fExor;
00189     int i, clk = clock();
00190 
00191     // load the data
00192     pFile = fopen( pFileName, "rb" );
00193     if ( pFile == NULL )
00194     {
00195         printf( "Rwr_ManLoadFromFile: Cannot open file \"%s\".\n", pFileName );
00196         return;
00197     }
00198     fread( &nEntries, sizeof(int), 1, pFile );
00199     pBuffer = ALLOC( unsigned, nEntries * 2 );
00200     fread( pBuffer, sizeof(unsigned), nEntries * 2, pFile );
00201     fclose( pFile );
00202     // reconstruct the forest
00203     for ( i = 0; i < nEntries; i++ )
00204     {
00205         // get EXOR flag
00206         fExor = (pBuffer[2*i + 0] & 1);
00207         pBuffer[2*i + 0] = (pBuffer[2*i + 0] >> 1);
00208         // get the nodes
00209         p0 = p->vForest->pArray[pBuffer[2*i + 0] >> 1];
00210         p1 = p->vForest->pArray[pBuffer[2*i + 1] >> 1];
00211         // compute the level and volume of the new nodes
00212         Level  = 1 + ABC_MAX( p0->Level, p1->Level );
00213         Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
00214         // set the complemented attributes
00215         p0 = Rwr_NotCond( p0, (pBuffer[2*i + 0] & 1) );
00216         p1 = Rwr_NotCond( p1, (pBuffer[2*i + 1] & 1) );
00217         // add the node
00218 //        Rwr_ManTryNode( p, p0, p1, Level, Volume );
00219         Rwr_ManAddNode( p, p0, p1, fExor, Level, Volume + fExor );
00220     }
00221     free( pBuffer );
00222     printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
00223     printf( "The number of nodes loaded = %d.   ", nEntries );  PRT( "Loading", clock() - clk );
00224 }

int Rwr_ManNodeVolume ( Rwr_Man_t p,
Rwr_Node_t p0,
Rwr_Node_t p1 
)

Function*************************************************************

Synopsis [Adds one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 327 of file rwrLib.c.

00328 {
00329     int Volume = 0;
00330     Rwr_ManIncTravId( p );
00331     Rwr_Trav_rec( p, p0, &Volume );
00332     Rwr_Trav_rec( p, p1, &Volume );
00333     return Volume;
00334 }

void Rwr_ManPrecompute ( Rwr_Man_t p  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Precomputes the forest in the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file rwrLib.c.

00046 {
00047     Rwr_Node_t * p0, * p1;
00048     int i, k, Level, Volume;
00049     int LevelOld = -1;
00050     int nNodes;
00051 
00052     Vec_PtrForEachEntryStart( p->vForest, p0, i, 1 )
00053     Vec_PtrForEachEntryStart( p->vForest, p1, k, 1 )
00054     {
00055         if ( LevelOld < (int)p0->Level )
00056         {
00057             LevelOld = p0->Level;
00058             printf( "Starting level %d  (at %d nodes).\n", LevelOld+1, i );
00059             printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
00060                 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
00061         }
00062 
00063         if ( k == i )
00064             break;
00065 //        if ( p0->Level + p1->Level > 6 ) // hard
00066 //            break;
00067 
00068         if ( p0->Level + p1->Level > 5 ) // easy 
00069             break;
00070 
00071 //        if ( p0->Level + p1->Level > 6 || (p0->Level == 3 && p1->Level == 3) )
00072 //            break;
00073 
00074         // compute the level and volume of the new nodes
00075         Level  = 1 + ABC_MAX( p0->Level, p1->Level );
00076         Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
00077         // try four different AND nodes
00078         Rwr_ManTryNode( p,         p0 ,         p1 , 0, Level, Volume );
00079         Rwr_ManTryNode( p, Rwr_Not(p0),         p1 , 0, Level, Volume );
00080         Rwr_ManTryNode( p,         p0 , Rwr_Not(p1), 0, Level, Volume );
00081         Rwr_ManTryNode( p, Rwr_Not(p0), Rwr_Not(p1), 0, Level, Volume );
00082         // try EXOR
00083         Rwr_ManTryNode( p,         p0 ,         p1 , 1, Level, Volume + 1 );
00084         // report the progress
00085         if ( p->nConsidered % 50000000 == 0 )
00086             printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
00087                 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
00088         // quit after some time
00089         if ( p->vForest->nSize == RWR_LIMIT + 5 )
00090         {
00091             printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
00092                 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
00093             goto save;
00094         }
00095     }
00096 save :
00097 
00098     // mark the relevant ones
00099     Rwr_ManIncTravId( p );
00100     k = 5;
00101     nNodes = 0;
00102     Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 )
00103         if ( p0->uTruth == p->puCanons[p0->uTruth] )
00104         {
00105             Rwr_MarkUsed_rec( p, p0 );
00106             nNodes++;
00107         }
00108 
00109     // compact the array by throwing away non-canonical
00110     k = 5;
00111     Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 )
00112         if ( p0->fUsed )
00113         {
00114             p->vForest->pArray[k] = p0;
00115             p0->Id = k++;
00116         }
00117     p->vForest->nSize = k;
00118     printf( "Total canonical = %4d. Total used = %5d.\n", nNodes, p->vForest->nSize );
00119 }

void Rwr_ManPreprocess ( Rwr_Man_t p  ) 

MACRO DEFINITIONS /// FUNCTION DECLARATIONS ///

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Preprocesses computed library of subgraphs.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file rwrDec.c.

00047 {
00048     Dec_Graph_t * pGraph;
00049     Rwr_Node_t * pNode;
00050     int i, k;
00051     // put the nodes into the structure
00052     p->pMapInv  = ALLOC( unsigned short, 222 );
00053     memset( p->pMapInv, 0, sizeof(unsigned short) * 222 );
00054     p->vClasses = Vec_VecStart( 222 );
00055     for ( i = 0; i < p->nFuncs; i++ )
00056     {
00057         if ( p->pTable[i] == NULL )
00058             continue;
00059         // consider all implementations of this function
00060         for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
00061         {
00062             assert( pNode->uTruth == p->pTable[i]->uTruth );
00063             assert( p->pMap[pNode->uTruth] >= 0 && p->pMap[pNode->uTruth] < 222 );
00064             Vec_VecPush( p->vClasses, p->pMap[pNode->uTruth], pNode );
00065             p->pMapInv[ p->pMap[pNode->uTruth] ] = p->puCanons[pNode->uTruth];
00066         }
00067     }
00068     // compute decomposition forms for each node and verify them
00069     Vec_VecForEachEntry( p->vClasses, pNode, i, k )
00070     {
00071         pGraph = Rwr_NodePreprocess( p, pNode );
00072         pNode->pNext = (Rwr_Node_t *)pGraph;
00073         assert( pNode->uTruth == (Dec_GraphDeriveTruth(pGraph) & 0xFFFF) );
00074     }
00075 }

void Rwr_ManPrint ( Rwr_Man_t p  ) 

Function*************************************************************

Synopsis [Prints one rwr node.]

Description []

SideEffects []

SeeAlso []

Definition at line 234 of file rwrPrint.c.

00235 {
00236     FILE * pFile;
00237     Rwr_Node_t * pNode;
00238     unsigned uTruth;
00239     int Limit, Counter, Volume, nFuncs, i;
00240     pFile = fopen( "graph_lib.txt", "w" );
00241     Counter = 0;
00242     Limit = (1 << 16);
00243     for ( i = 0; i < Limit; i++ )
00244     {
00245         if ( p->pTable[i] == NULL )
00246             continue;
00247         if ( i != p->puCanons[i] )
00248             continue;
00249         fprintf( pFile, "\nClass %3d. Func %6d.  ", p->pMap[i], Counter++ );
00250         Rwr_GetBushVolume( p, i, &Volume, &nFuncs );
00251         fprintf( pFile, "Roots = %3d. Vol = %3d. Sum = %3d.  ", nFuncs, Volume, Rwr_GetBushSumOfVolumes(p, i) );
00252         uTruth = i;
00253         Extra_PrintBinary( pFile, &uTruth, 16 );
00254         fprintf( pFile, "\n" );
00255         for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
00256             if ( pNode->uTruth == p->puCanons[pNode->uTruth] )
00257                 Rwr_NodePrint( pFile, p, pNode );
00258     }
00259     fclose( pFile );
00260 }

void Rwr_ManPrintStats ( Rwr_Man_t p  ) 

Function*************************************************************

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file rwrMan.c.

00141 {
00142     int i, Counter = 0;
00143     for ( i = 0; i < 222; i++ )
00144         Counter += (p->nScores[i] > 0);
00145 
00146     printf( "Rewriting statistics:\n" );
00147     printf( "Total cuts tries  = %8d.\n", p->nCutsGood );
00148     printf( "Bad cuts found    = %8d.\n", p->nCutsBad );
00149     printf( "Total subgraphs   = %8d.\n", p->nSubgraphs );
00150     printf( "Used NPN classes  = %8d.\n", Counter );
00151     printf( "Nodes considered  = %8d.\n", p->nNodesConsidered );
00152     printf( "Nodes rewritten   = %8d.\n", p->nNodesRewritten );
00153     printf( "Gain              = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
00154     PRT( "Start       ", p->timeStart );
00155     PRT( "Cuts        ", p->timeCut );
00156     PRT( "Resynthesis ", p->timeRes );
00157     PRT( "    Mffc    ", p->timeMffc );
00158     PRT( "    Eval    ", p->timeEval );
00159     PRT( "Update      ", p->timeUpdate );
00160     PRT( "TOTAL       ", p->timeTotal );
00161 
00162 /*
00163     printf( "The scores are:\n" );
00164     for ( i = 0; i < 222; i++ )
00165         if ( p->nScores[i] > 0 )
00166         {
00167             extern void Ivy_TruthDsdComputePrint( unsigned uTruth );
00168             printf( "%3d = %8d  canon = %5d  ", i, p->nScores[i], p->pMapInv[i] );
00169             Ivy_TruthDsdComputePrint( (unsigned)p->pMapInv[i] | ((unsigned)p->pMapInv[i] << 16) );
00170         }
00171 */
00172     printf( "\n" );
00173 
00174 }

void Rwr_ManPrintStatsFile ( Rwr_Man_t p  ) 

Function*************************************************************

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 187 of file rwrMan.c.

00188 {
00189     FILE * pTable;
00190     pTable = fopen( "stats.txt", "a+" );
00191     fprintf( pTable, "%d ", p->nCutsGood );
00192     fprintf( pTable, "%d ", p->nSubgraphs );
00193     fprintf( pTable, "%d ", p->nNodesRewritten );
00194     fprintf( pTable, "%d", p->nNodesGained );
00195     fprintf( pTable, "\n" );
00196     fclose( pTable );
00197 }

int Rwr_ManReadCompl ( Rwr_Man_t p  ) 

Function*************************************************************

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 242 of file rwrMan.c.

00243 {
00244     return p->fCompl;
00245 }

void* Rwr_ManReadDecs ( Rwr_Man_t p  ) 

Function*************************************************************

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 210 of file rwrMan.c.

00211 {
00212     return p->pGraph;
00213 }

Vec_Ptr_t* Rwr_ManReadLeaves ( Rwr_Man_t p  ) 

Function*************************************************************

Synopsis [Stops the resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 226 of file rwrMan.c.

00227 {
00228     return p->vFanins;
00229 }

Rwr_Man_t* Rwr_ManStart ( bool  fPrecompute  ) 

CFile****************************************************************

FileName [rwrMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting package.]

Synopsis [Rewriting manager.]

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

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Starts rewriting manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file rwrMan.c.

00045 {
00046     Dec_Man_t * pManDec;
00047     Rwr_Man_t * p;
00048     int clk = clock();
00049 clk = clock();
00050     p = ALLOC( Rwr_Man_t, 1 );
00051     memset( p, 0, sizeof(Rwr_Man_t) );
00052     p->nFuncs = (1<<16);
00053     pManDec   = Abc_FrameReadManDec();
00054     p->puCanons = pManDec->puCanons; 
00055     p->pPhases  = pManDec->pPhases; 
00056     p->pPerms   = pManDec->pPerms; 
00057     p->pMap     = pManDec->pMap; 
00058     // initialize practical NPN classes
00059     p->pPractical  = Rwr_ManGetPractical( p );
00060     // create the table
00061     p->pTable = ALLOC( Rwr_Node_t *, p->nFuncs );
00062     memset( p->pTable, 0, sizeof(Rwr_Node_t *) * p->nFuncs );
00063     // create the elementary nodes
00064     p->pMmNode  = Extra_MmFixedStart( sizeof(Rwr_Node_t) );
00065     p->vForest  = Vec_PtrAlloc( 100 );
00066     Rwr_ManAddVar( p, 0x0000, fPrecompute ); // constant 0
00067     Rwr_ManAddVar( p, 0xAAAA, fPrecompute ); // var A
00068     Rwr_ManAddVar( p, 0xCCCC, fPrecompute ); // var B
00069     Rwr_ManAddVar( p, 0xF0F0, fPrecompute ); // var C
00070     Rwr_ManAddVar( p, 0xFF00, fPrecompute ); // var D
00071     p->nClasses = 5;
00072     // other stuff
00073     p->nTravIds   = 1;
00074     p->pPerms4    = Extra_Permutations( 4 );
00075     p->vLevNums   = Vec_IntAlloc( 50 );
00076     p->vFanins    = Vec_PtrAlloc( 50 );
00077     p->vFaninsCur = Vec_PtrAlloc( 50 );
00078     p->vNodesTemp = Vec_PtrAlloc( 50 );
00079     if ( fPrecompute )
00080     {   // precompute subgraphs
00081         Rwr_ManPrecompute( p );
00082 //        Rwr_ManPrint( p );
00083         Rwr_ManWriteToArray( p );
00084     }
00085     else
00086     {   // load saved subgraphs
00087         Rwr_ManLoadFromArray( p, 0 );
00088 //        Rwr_ManPrint( p );
00089         Rwr_ManPreprocess( p );
00090     }
00091 p->timeStart = clock() - clk;
00092     return p;
00093 }

void Rwr_ManStop ( Rwr_Man_t p  ) 

Function*************************************************************

Synopsis [Stops rewriting manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file rwrMan.c.

00107 {
00108     if ( p->vClasses )
00109     {
00110         Rwr_Node_t * pNode;
00111         int i, k;
00112         Vec_VecForEachEntry( p->vClasses, pNode, i, k )
00113             Dec_GraphFree( (Dec_Graph_t *)pNode->pNext );
00114     }
00115     if ( p->vClasses )  Vec_VecFree( p->vClasses );
00116     Vec_PtrFree( p->vNodesTemp );
00117     Vec_PtrFree( p->vForest );
00118     Vec_IntFree( p->vLevNums );
00119     Vec_PtrFree( p->vFanins );
00120     Vec_PtrFree( p->vFaninsCur );
00121     Extra_MmFixedStop( p->pMmNode );
00122     FREE( p->pMapInv );
00123     free( p->pTable );
00124     free( p->pPractical );
00125     free( p->pPerms4 );
00126     free( p );
00127 }

void Rwr_ManWriteToArray ( Rwr_Man_t p  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Writes data.]

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file rwrUtil.c.

00052 {
00053     FILE * pFile;
00054     Rwr_Node_t * pNode;
00055     unsigned Entry0, Entry1;
00056     int i, nEntries, clk = clock();
00057     // prepare the buffer
00058     nEntries = p->vForest->nSize - 5;
00059     pFile = fopen( "npn4_aig_array.txt", "w" );
00060     fprintf( pFile, "static unsigned short s_RwtAigSubgraphs[] = \n{" );
00061     for ( i = 0; i < nEntries; i++ )
00062     {
00063         if ( i % 5 == 0 )
00064             fprintf( pFile, "\n    " );
00065         pNode = p->vForest->pArray[i+5];
00066         Entry0 = (Rwr_Regular(pNode->p0)->Id << 1) | Rwr_IsComplement(pNode->p0);
00067         Entry1 = (Rwr_Regular(pNode->p1)->Id << 1) | Rwr_IsComplement(pNode->p1);
00068         Entry0 = (Entry0 << 1) | pNode->fExor;
00069         Extra_PrintHex( pFile, Entry0, 4 );
00070         fprintf( pFile, "," );
00071         Extra_PrintHex( pFile, Entry1, 4 );
00072         fprintf( pFile, ", " );
00073     }
00074     if ( i % 5 == 0 )
00075         fprintf( pFile, "\n    " );
00076     Extra_PrintHex( pFile, 0, 4 );
00077     fprintf( pFile, "," );
00078     Extra_PrintHex( pFile, 0, 4 );
00079     fprintf( pFile, " \n};\n" );
00080     fclose( pFile );
00081     printf( "The number of nodes saved = %d.   ", nEntries );  PRT( "Saving", clock() - clk );
00082 }

void Rwr_ManWriteToFile ( Rwr_Man_t p,
char *  pFileName 
)

Function*************************************************************

Synopsis [Writes.]

Description []

SideEffects []

SeeAlso []

Definition at line 146 of file rwrUtil.c.

00147 {
00148     FILE * pFile;
00149     Rwr_Node_t * pNode;
00150     unsigned * pBuffer;
00151     int i, nEntries, clk = clock();
00152     // prepare the buffer
00153     nEntries = p->vForest->nSize - 5;
00154     pBuffer = ALLOC( unsigned, nEntries * 2 );
00155     for ( i = 0; i < nEntries; i++ )
00156     {
00157         pNode = p->vForest->pArray[i+5];
00158         pBuffer[2*i + 0] = (Rwr_Regular(pNode->p0)->Id << 1) | Rwr_IsComplement(pNode->p0);
00159         pBuffer[2*i + 1] = (Rwr_Regular(pNode->p1)->Id << 1) | Rwr_IsComplement(pNode->p1);
00160         // save EXOR flag
00161         pBuffer[2*i + 0] = (pBuffer[2*i + 0] << 1) | pNode->fExor;
00162 
00163     }
00164     pFile = fopen( pFileName, "wb" );
00165     fwrite( &nEntries, sizeof(int), 1, pFile );
00166     fwrite( pBuffer, sizeof(unsigned), nEntries * 2, pFile );
00167     free( pBuffer );
00168     fclose( pFile );
00169     printf( "The number of nodes saved = %d.   ", nEntries );  PRT( "Saving", clock() - clk );
00170 }

int Rwr_NodeRewrite ( Rwr_Man_t p,
Cut_Man_t pManCut,
Abc_Obj_t pNode,
int  fUpdateLevel,
int  fUseZeros,
int  fPlaceEnable 
)

FUNCTION DEFINITIONS ///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->pGraph gives the decomposition dag (represented using decomposition graph data structure). Returns gain in the number of nodes or -1 if node cannot be rewritten.]

SideEffects []

SeeAlso []

Definition at line 55 of file rwrEva.c.

00056 {
00057     int fVeryVerbose = 0;
00058     Dec_Graph_t * pGraph;
00059     Cut_Cut_t * pCut;//, * pTemp;
00060     Abc_Obj_t * pFanin;
00061     unsigned uPhase, uTruthBest, uTruth;
00062     char * pPerm;
00063     int Required, nNodesSaved, nNodesSaveCur;
00064     int i, GainCur, GainBest = -1;
00065     int clk, clk2;//, Counter;
00066 
00067     p->nNodesConsidered++;
00068     // get the required times
00069     Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
00070 
00071     // get the node's cuts
00072 clk = clock();
00073     pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode, 0, 0 );
00074     assert( pCut != NULL );
00075 p->timeCut += clock() - clk;
00076 
00077 //printf( " %d", Rwr_CutCountNumNodes(pNode, pCut) );
00078 /*
00079     Counter = 0;
00080     for ( pTemp = pCut->pNext; pTemp; pTemp = pTemp->pNext )
00081         Counter++;
00082     printf( "%d ", Counter );
00083 */
00084     // go through the cuts
00085 clk = clock();
00086     for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )
00087     {
00088         // consider only 4-input cuts
00089         if ( pCut->nLeaves < 4 )
00090             continue;
00091 //            Cut_CutPrint( pCut, 0 ), printf( "\n" );
00092 
00093         // get the fanin permutation
00094         uTruth = 0xFFFF & *Cut_CutReadTruth(pCut);
00095         pPerm = p->pPerms4[ p->pPerms[uTruth] ];
00096         uPhase = p->pPhases[uTruth];
00097         // collect fanins with the corresponding permutation/phase
00098         Vec_PtrClear( p->vFaninsCur );
00099         Vec_PtrFill( p->vFaninsCur, (int)pCut->nLeaves, 0 );
00100         for ( i = 0; i < (int)pCut->nLeaves; i++ )
00101         {
00102             pFanin = Abc_NtkObj( pNode->pNtk, pCut->pLeaves[pPerm[i]] );
00103             if ( pFanin == NULL )
00104                 break;
00105             pFanin = Abc_ObjNotCond(pFanin, ((uPhase & (1<<i)) > 0) );
00106             Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
00107         }
00108         if ( i != (int)pCut->nLeaves )
00109         {
00110             p->nCutsBad++;
00111             continue;
00112         }
00113         p->nCutsGood++;
00114 
00115         {
00116             int Counter = 0;
00117             Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
00118                 if ( Abc_ObjFanoutNum(Abc_ObjRegular(pFanin)) == 1 )
00119                     Counter++;
00120             if ( Counter > 2 )
00121                 continue;
00122         }
00123 
00124 clk2 = clock();
00125 /*
00126         printf( "Considering: (" );
00127         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
00128             printf( "%d ", Abc_ObjFanoutNum(Abc_ObjRegular(pFanin)) );
00129         printf( ")\n" );
00130 */
00131         // mark the fanin boundary 
00132         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
00133             Abc_ObjRegular(pFanin)->vFanouts.nSize++;
00134 
00135         // label MFFC with current ID
00136         Abc_NtkIncrementTravId( pNode->pNtk );
00137         nNodesSaved = Abc_NodeMffcLabelAig( pNode );
00138         // unmark the fanin boundary
00139         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
00140             Abc_ObjRegular(pFanin)->vFanouts.nSize--;
00141 p->timeMffc += clock() - clk2;
00142 
00143         // evaluate the cut
00144 clk2 = clock();
00145         pGraph = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, fPlaceEnable );
00146 p->timeEval += clock() - clk2;
00147 
00148         // check if the cut is better than the current best one
00149         if ( pGraph != NULL && GainBest < GainCur )
00150         {
00151             // save this form
00152             nNodesSaveCur = nNodesSaved;
00153             GainBest  = GainCur;
00154             p->pGraph  = pGraph;
00155             p->fCompl = ((uPhase & (1<<4)) > 0);
00156             uTruthBest = 0xFFFF & *Cut_CutReadTruth(pCut);
00157             // collect fanins in the
00158             Vec_PtrClear( p->vFanins );
00159             Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
00160                 Vec_PtrPush( p->vFanins, pFanin );
00161         }
00162     }
00163 p->timeRes += clock() - clk;
00164 
00165     if ( GainBest == -1 )
00166         return -1;
00167 /*
00168     if ( GainBest > 0 )
00169     {
00170         printf( "Class %d  ", p->pMap[uTruthBest] );
00171         printf( "Gain = %d. Node %d : ", GainBest, pNode->Id );
00172         Vec_PtrForEachEntry( p->vFanins, pFanin, i )
00173             printf( "%d ", Abc_ObjRegular(pFanin)->Id );
00174         Dec_GraphPrint( stdout, p->pGraph, NULL, NULL );
00175         printf( "\n" );
00176     }
00177 */
00178 
00179 //    printf( "%d", nNodesSaveCur - GainBest );
00180 /*
00181     if ( GainBest > 0 )
00182     {
00183         if ( Rwr_CutIsBoolean( pNode, p->vFanins ) )
00184             printf( "b" );
00185         else
00186         {
00187             printf( "Node %d : ", pNode->Id );
00188             Vec_PtrForEachEntry( p->vFanins, pFanin, i )
00189                 printf( "%d ", Abc_ObjRegular(pFanin)->Id );
00190             printf( "a" );
00191         }
00192     }
00193 */
00194 /*
00195     if ( GainBest > 0 )
00196         if ( p->fCompl )
00197             printf( "c" );
00198         else
00199             printf( "." );
00200 */
00201 
00202     // copy the leaves
00203     Vec_PtrForEachEntry( p->vFanins, pFanin, i )
00204         Dec_GraphNode(p->pGraph, i)->pFunc = pFanin;
00205 /*
00206     printf( "(" );
00207     Vec_PtrForEachEntry( p->vFanins, pFanin, i )
00208         printf( " %d", Abc_ObjRegular(pFanin)->vFanouts.nSize - 1 );
00209     printf( " )  " );
00210 */
00211 //    printf( "%d ", Rwr_NodeGetDepth_rec( pNode, p->vFanins ) );
00212 
00213     p->nScores[p->pMap[uTruthBest]]++;
00214     p->nNodesGained += GainBest;
00215     if ( fUseZeros || GainBest > 0 )
00216     {
00217         p->nNodesRewritten++;
00218     }
00219 
00220     // report the progress
00221     if ( fVeryVerbose && GainBest > 0 )
00222     {
00223         printf( "Node %6s :   ", Abc_ObjName(pNode) );
00224         printf( "Fanins = %d. ", p->vFanins->nSize );
00225         printf( "Save = %d.  ", nNodesSaveCur );
00226         printf( "Add = %d.  ",  nNodesSaveCur-GainBest );
00227         printf( "GAIN = %d.  ", GainBest );
00228         printf( "Cone = %d.  ", p->pGraph? Dec_GraphNodeNum(p->pGraph) : 0 );
00229         printf( "Class = %d.  ", p->pMap[uTruthBest] );
00230         printf( "\n" );
00231     }
00232     return GainBest;
00233 }

static Rwr_Node_t* Rwr_Not ( Rwr_Node_t p  )  [inline, static]

Definition at line 116 of file rwr.h.

00116 { return (Rwr_Node_t *)((unsigned long)(p) ^  01);  }

static Rwr_Node_t* Rwr_NotCond ( Rwr_Node_t p,
int  c 
) [inline, static]

Definition at line 117 of file rwr.h.

00117 { return (Rwr_Node_t *)((unsigned long)(p) ^ (c));  }

static Rwr_Node_t* Rwr_Regular ( Rwr_Node_t p  )  [inline, static]

Definition at line 115 of file rwr.h.

00115 { return (Rwr_Node_t *)((unsigned long)(p) & ~01);  }

void Rwr_ScoresClean ( Rwr_Man_t p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 495 of file rwrEva.c.

00496 {
00497     Vec_Ptr_t * vSubgraphs;
00498     Rwr_Node_t * pNode;
00499     int i, k;
00500     for ( i = 0; i < p->vClasses->nSize; i++ )
00501     {
00502         vSubgraphs = Vec_VecEntry( p->vClasses, i );
00503         Vec_PtrForEachEntry( vSubgraphs, pNode, k )
00504             pNode->nScore = pNode->nGain = pNode->nAdded = 0;
00505     }
00506 }

void Rwr_ScoresReport ( Rwr_Man_t p  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 541 of file rwrEva.c.

00542 {
00543     extern void Ivy_TruthDsdComputePrint( unsigned uTruth );
00544     int Perm[222];
00545     Vec_Ptr_t * vSubgraphs;
00546     Rwr_Node_t * pNode;
00547     int i, iNew, k;
00548     unsigned uTruth;
00549     // collect total gains
00550     assert( p->vClasses->nSize == 222 );
00551     for ( i = 0; i < p->vClasses->nSize; i++ )
00552     {
00553         Perm[i] = i;
00554         Gains[i] = 0;
00555         vSubgraphs = Vec_VecEntry( p->vClasses, i );
00556         Vec_PtrForEachEntry( vSubgraphs, pNode, k )
00557             Gains[i] += pNode->nGain;
00558     }
00559     // sort the gains
00560     qsort( Perm, 222, sizeof(int), (int (*)(const void *, const void *))Rwr_ScoresCompare );
00561 
00562     // print classes
00563     for ( i = 0; i < p->vClasses->nSize; i++ )
00564     {
00565         iNew = Perm[i];
00566         if ( Gains[iNew] == 0 )
00567             break;
00568         vSubgraphs = Vec_VecEntry( p->vClasses, iNew );
00569         printf( "CLASS %3d: Subgr = %3d. Total gain = %6d.  ", iNew, Vec_PtrSize(vSubgraphs), Gains[iNew] );
00570         uTruth = (unsigned)p->pMapInv[iNew];
00571         Extra_PrintBinary( stdout, &uTruth, 16 );
00572         printf( "  " );
00573         Ivy_TruthDsdComputePrint( (unsigned)p->pMapInv[iNew] | ((unsigned)p->pMapInv[iNew] << 16) );
00574         Vec_PtrForEachEntry( vSubgraphs, pNode, k )
00575         {
00576             if ( pNode->nScore == 0 )
00577                 continue;
00578             printf( "    %2d: S=%5d. A=%5d. G=%6d. ", k, pNode->nScore, pNode->nAdded, pNode->nGain );
00579             Dec_GraphPrint( stdout, (Dec_Graph_t *)pNode->pNext, NULL, NULL );
00580         }
00581     }
00582 }


Generated on Tue Jan 5 12:19:33 2010 for abc70930 by  doxygen 1.6.1