src/aig/dar/dar.h File Reference

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  Dar_RwrPar_t_
struct  Dar_RefPar_t_

Typedefs

typedef struct Dar_RwrPar_t_ Dar_RwrPar_t
typedef struct Dar_RefPar_t_ Dar_RefPar_t

Functions

void Dar_LibStart ()
void Dar_LibStop ()
Aig_Man_t * Dar_ManBalance (Aig_Man_t *p, int fUpdateLevel)
void Dar_ManDefaultRwrParams (Dar_RwrPar_t *pPars)
int Dar_ManRewrite (Aig_Man_t *pAig, Dar_RwrPar_t *pPars)
Aig_MmFixed_t * Dar_ManComputeCuts (Aig_Man_t *pAig, int nCutsMax)
void Dar_ManDefaultRefParams (Dar_RefPar_t *pPars)
int Dar_ManRefactor (Aig_Man_t *pAig, Dar_RefPar_t *pPars)
Aig_Man_t * Dar_ManRewriteDefault (Aig_Man_t *pAig)
Aig_Man_t * Dar_ManRwsat (Aig_Man_t *pAig, int fBalance, int fVerbose)
Aig_Man_t * Dar_ManCompress (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fVerbose)
Aig_Man_t * Dar_ManCompress2 (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fVerbose)
Aig_Man_t * Dar_ManChoice (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fVerbose)

Typedef Documentation

typedef struct Dar_RefPar_t_ Dar_RefPar_t

Definition at line 41 of file dar.h.

typedef struct Dar_RwrPar_t_ Dar_RwrPar_t

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

FileName [dar.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
dar.h,v 1.00 2007/04/28 00:00:00 alanmi Exp

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

Definition at line 40 of file dar.h.

Function Documentation

void Dar_LibStart (  ) 

MACRO DEFINITIONS /// ITERATORS /// FUNCTION DECLARATIONS ///

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

Synopsis [Starts the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 568 of file darLib.c.

00569 {
00570 //    int clk = clock();
00571     assert( s_DarLib == NULL );
00572     s_DarLib = Dar_LibRead();
00573 //    printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );
00574 //    PRT( "Time", clock() - clk );
00575 }

void Dar_LibStop (  ) 

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

Synopsis [Stops the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 588 of file darLib.c.

00589 {
00590     assert( s_DarLib != NULL );
00591     Dar_LibFree( s_DarLib );
00592     s_DarLib = NULL;
00593 }

Aig_Man_t* Dar_ManBalance ( Aig_Man_t *  p,
int  fUpdateLevel 
)

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

Synopsis [Performs algebraic balancing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file darBalance.c.

00050 {
00051     Aig_Man_t * pNew;
00052     Aig_Obj_t * pObj, * pDriver, * pObjNew;
00053     Vec_Vec_t * vStore;
00054     int i;
00055     // create the new manager 
00056     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
00057     pNew->pName = Aig_UtilStrsav( p->pName );
00058     pNew->nRegs = p->nRegs;
00059     pNew->nAsserts = p->nAsserts;
00060     if ( p->vFlopNums )
00061         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
00062     // map the PI nodes
00063     Aig_ManCleanData( p );
00064     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
00065     Aig_ManForEachPi( p, pObj, i )
00066         pObj->pData = Aig_ObjCreatePi(pNew);
00067     // balance the AIG
00068     vStore = Vec_VecAlloc( 50 );
00069     Aig_ManForEachPo( p, pObj, i )
00070     {
00071         pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
00072         pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
00073         pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
00074         Aig_ObjCreatePo( pNew, pObjNew );
00075     }
00076     Vec_VecFree( vStore );
00077     // remove dangling nodes
00078     if ( (i = Aig_ManCleanup( pNew )) )
00079         printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
00080     // check the resulting AIG
00081     if ( !Aig_ManCheck(pNew) )
00082         printf( "Dar_ManBalance(): The check has failed.\n" );
00083     return pNew;
00084 }

Aig_Man_t* Dar_ManChoice ( Aig_Man_t *  pAig,
int  fBalance,
int  fUpdateLevel,
int  fVerbose 
)

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

Synopsis [Gives the current ABC network to AIG manager for processing.]

Description []

SideEffects []

SeeAlso []Function*************************************************************

Synopsis [Reproduces script "compress2".]

Description []

SideEffects []

SeeAlso []

Definition at line 353 of file darScript.c.

00354 {
00355 /*
00356     Aig_Man_t * pMan, * pTemp;
00357     Vec_Ptr_t * vAigs;
00358     int i, clk;
00359 
00360 clk = clock();
00361 //    vAigs = Dar_ManChoiceSynthesisExt();
00362     vAigs = Dar_ManChoiceSynthesis( pAig, fBalance, fUpdateLevel, fVerbose );
00363 
00364     // swap the first and last network
00365     // this should lead to the primary choice being "better" because of synthesis
00366     pMan = Vec_PtrPop( vAigs );
00367     Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
00368     Vec_PtrWriteEntry( vAigs, 0, pMan );
00369 
00370 if ( fVerbose )
00371 {
00372 PRT( "Synthesis time", clock() - clk );
00373 }
00374 clk = clock();
00375     pMan = Aig_ManChoicePartitioned( vAigs, 300 );
00376     Vec_PtrForEachEntry( vAigs, pTemp, i )
00377         Aig_ManStop( pTemp );
00378     Vec_PtrFree( vAigs );
00379 if ( fVerbose )
00380 {
00381 PRT( "Choicing time ", clock() - clk );
00382 }
00383     return pMan;
00384 */
00385     return NULL;
00386 }

Aig_Man_t* Dar_ManCompress ( Aig_Man_t *  pAig,
int  fBalance,
int  fUpdateLevel,
int  fVerbose 
)

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

Synopsis [Reproduces script "compress".]

Description []

SideEffects []

SeeAlso []

Definition at line 124 of file darScript.c.

00126 {
00127     Aig_Man_t * pTemp;
00128 
00129     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
00130     Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
00131 
00132     Dar_ManDefaultRwrParams( pParsRwr );
00133     Dar_ManDefaultRefParams( pParsRef );
00134 
00135     pParsRwr->fUpdateLevel = fUpdateLevel;
00136     pParsRef->fUpdateLevel = fUpdateLevel;
00137 
00138     pParsRwr->fVerbose = 0;//fVerbose;
00139     pParsRef->fVerbose = 0;//fVerbose;
00140 
00141     pAig = Aig_ManDup( pAig, 0 ); 
00142     if ( fVerbose ) Aig_ManPrintStats( pAig );
00143 
00144     // balance
00145     if ( fBalance )
00146     {
00147 //    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
00148 //    Aig_ManStop( pTemp );
00149 //    if ( fVerbose ) Aig_ManPrintStats( pAig );
00150     }
00151     
00152     // rewrite
00153     Dar_ManRewrite( pAig, pParsRwr );
00154     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00155     Aig_ManStop( pTemp );
00156     if ( fVerbose ) Aig_ManPrintStats( pAig );
00157     
00158     // refactor
00159     Dar_ManRefactor( pAig, pParsRef );
00160     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00161     Aig_ManStop( pTemp );
00162     if ( fVerbose ) Aig_ManPrintStats( pAig );
00163 
00164     // balance
00165     if ( fBalance )
00166     {
00167     pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
00168     Aig_ManStop( pTemp );
00169     if ( fVerbose ) Aig_ManPrintStats( pAig );
00170     }
00171 
00172     pParsRwr->fUseZeros = 1;
00173     pParsRef->fUseZeros = 1;
00174     
00175     // rewrite
00176     Dar_ManRewrite( pAig, pParsRwr );
00177     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00178     Aig_ManStop( pTemp );
00179     if ( fVerbose ) Aig_ManPrintStats( pAig );
00180 
00181     return pAig;
00182 }

Aig_Man_t* Dar_ManCompress2 ( Aig_Man_t *  pAig,
int  fBalance,
int  fUpdateLevel,
int  fVerbose 
)

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

Synopsis [Reproduces script "compress2".]

Description []

SideEffects []

SeeAlso []

Definition at line 195 of file darScript.c.

00197 {
00198     Aig_Man_t * pTemp;
00199 
00200     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
00201     Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
00202 
00203     Dar_ManDefaultRwrParams( pParsRwr );
00204     Dar_ManDefaultRefParams( pParsRef );
00205 
00206     pParsRwr->fUpdateLevel = fUpdateLevel;
00207     pParsRef->fUpdateLevel = fUpdateLevel;
00208 
00209     pParsRwr->fVerbose = 0;//fVerbose;
00210     pParsRef->fVerbose = 0;//fVerbose;
00211 
00212     pAig = Aig_ManDup( pAig, 0 ); 
00213     if ( fVerbose ) Aig_ManPrintStats( pAig );
00214 
00215     // balance
00216     if ( fBalance )
00217     {
00218 //    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
00219 //    Aig_ManStop( pTemp );
00220 //    if ( fVerbose ) Aig_ManPrintStats( pAig );
00221     }
00222     
00223 
00224     // rewrite
00225     Dar_ManRewrite( pAig, pParsRwr );
00226     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00227     Aig_ManStop( pTemp );
00228     if ( fVerbose ) Aig_ManPrintStats( pAig );
00229     
00230     // refactor
00231     Dar_ManRefactor( pAig, pParsRef );
00232     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00233     Aig_ManStop( pTemp );
00234     if ( fVerbose ) Aig_ManPrintStats( pAig );
00235 
00236     // balance
00237 //    if ( fBalance )
00238     {
00239     pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
00240     Aig_ManStop( pTemp );
00241     if ( fVerbose ) Aig_ManPrintStats( pAig );
00242     }
00243     
00244     // rewrite
00245     Dar_ManRewrite( pAig, pParsRwr );
00246     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00247     Aig_ManStop( pTemp );
00248     if ( fVerbose ) Aig_ManPrintStats( pAig );
00249 
00250     pParsRwr->fUseZeros = 1;
00251     pParsRef->fUseZeros = 1;
00252     
00253     // rewrite
00254     Dar_ManRewrite( pAig, pParsRwr );
00255     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00256     Aig_ManStop( pTemp );
00257     if ( fVerbose ) Aig_ManPrintStats( pAig );
00258 
00259     // balance
00260     if ( fBalance )
00261     {
00262     pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
00263     Aig_ManStop( pTemp );
00264     if ( fVerbose ) Aig_ManPrintStats( pAig );
00265     }
00266     
00267     // refactor
00268     Dar_ManRefactor( pAig, pParsRef );
00269     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00270     Aig_ManStop( pTemp );
00271     if ( fVerbose ) Aig_ManPrintStats( pAig );
00272     
00273     // rewrite
00274     Dar_ManRewrite( pAig, pParsRwr );
00275     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00276     Aig_ManStop( pTemp );
00277     if ( fVerbose ) Aig_ManPrintStats( pAig );
00278 
00279     // balance
00280     if ( fBalance )
00281     {
00282     pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
00283     Aig_ManStop( pTemp );
00284     if ( fVerbose ) Aig_ManPrintStats( pAig );
00285     }
00286     return pAig;
00287 }

Aig_MmFixed_t* Dar_ManComputeCuts ( Aig_Man_t *  pAig,
int  nCutsMax 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 207 of file darCore.c.

00208 {
00209     Dar_Man_t * p;
00210     Dar_RwrPar_t Pars, * pPars = &Pars; 
00211     Aig_Obj_t * pObj;
00212     Aig_MmFixed_t * pMemCuts;
00213     int i, nNodes;
00214     // remove dangling nodes
00215     if ( (nNodes = Aig_ManCleanup( pAig )) )
00216     {
00217 //        printf( "Removing %d nodes.\n", nNodes );
00218     }
00219     // create default parameters
00220     Dar_ManDefaultRwrParams( pPars );
00221     pPars->nCutsMax = nCutsMax;
00222     // create rewriting manager
00223     p = Dar_ManStart( pAig, pPars );
00224     // set elementary cuts for the PIs
00225     Dar_ManCutsStart( p );
00226     // compute cuts for each nodes in the topological order
00227     Aig_ManForEachNode( pAig, pObj, i )
00228         Dar_ObjComputeCuts( p, pObj );
00229     // free the cuts
00230     pMemCuts = p->pMemCuts;
00231     p->pMemCuts = NULL;
00232 //    Dar_ManCutsFree( p );
00233     // stop the rewriting manager
00234     Dar_ManStop( p );
00235     return pMemCuts;
00236 }

void Dar_ManDefaultRefParams ( Dar_RefPar_t *  pPars  ) 

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

Synopsis [Returns the structure with default assignment of parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file darRefact.c.

00077 {
00078     memset( pPars, 0, sizeof(Dar_RefPar_t) );
00079     pPars->nMffcMin     =  2;  // the min MFFC size for which refactoring is used
00080     pPars->nLeafMax     = 12;  // the max number of leaves of a cut
00081     pPars->nCutsMax     =  5;  // the max number of cuts to consider  
00082     pPars->fUpdateLevel =  0;
00083     pPars->fUseZeros    =  0;
00084     pPars->fVerbose     =  0;
00085     pPars->fVeryVerbose =  0;
00086 }

void Dar_ManDefaultRwrParams ( Dar_RwrPar_t *  pPars  ) 

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

FileName [darCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [Core of the rewriting package.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
darCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

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

Synopsis [Returns the structure with default assignment of parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file darCore.c.

00043 {
00044     memset( pPars, 0, sizeof(Dar_RwrPar_t) );
00045     pPars->nCutsMax     =  8; // 8
00046     pPars->nSubgMax     =  5; // 5 is a "magic number"
00047     pPars->fFanout      =  1;
00048     pPars->fUpdateLevel =  0;
00049     pPars->fUseZeros    =  0;
00050     pPars->fVerbose     =  0;
00051     pPars->fVeryVerbose =  0;
00052 }

int Dar_ManRefactor ( Aig_Man_t *  pAig,
Dar_RefPar_t *  pPars 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 464 of file darRefact.c.

00465 {
00466 //    Bar_Progress_t * pProgress;
00467     Ref_Man_t * p;
00468     Vec_Ptr_t * vCut, * vCut2;
00469     Aig_Obj_t * pObj, * pObjNew;
00470     int nNodesOld, nNodeBefore, nNodeAfter, nNodesSaved, nNodesSaved2;
00471     int i, Required, nLevelMin, clkStart, clk;
00472 
00473     // start the manager
00474     p = Dar_ManRefStart( pAig, pPars );
00475     // remove dangling nodes
00476     Aig_ManCleanup( pAig );
00477     // if updating levels is requested, start fanout and timing
00478     Aig_ManFanoutStart( pAig );
00479     if ( p->pPars->fUpdateLevel )
00480         Aig_ManStartReverseLevels( pAig, 0 );
00481 
00482     // resynthesize each node once
00483     clkStart = clock();
00484     vCut = Vec_VecEntry( p->vCuts, 0 );
00485     vCut2 = Vec_VecEntry( p->vCuts, 1 );
00486     p->nNodesInit = Aig_ManNodeNum(pAig);
00487     nNodesOld = Vec_PtrSize( pAig->vObjs );
00488 //    pProgress = Bar_ProgressStart( stdout, nNodesOld );
00489     Aig_ManForEachObj( pAig, pObj, i )
00490     {
00491 //        Bar_ProgressUpdate( pProgress, i, NULL );
00492         if ( !Aig_ObjIsNode(pObj) )
00493             continue;
00494         if ( i > nNodesOld )
00495             break;
00496         Vec_VecClear( p->vCuts );
00497 
00498 //printf( "\nConsidering node %d.\n", pObj->Id );
00499         // get the bounded MFFC size
00500 clk = clock();
00501         nLevelMin = AIG_MAX( 0, Aig_ObjLevel(pObj) - 10 );
00502         nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut );
00503         if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider
00504         {
00505 p->timeCuts += clock() - clk;
00506             continue; 
00507         }
00508         p->nNodesTried++;
00509         if ( Vec_PtrSize(vCut) > p->pPars->nLeafMax ) // get one reconv-driven cut
00510         {
00511             Aig_ManFindCut( pObj, vCut, p->vCutNodes, p->pPars->nLeafMax, 50 );
00512             nNodesSaved = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut );
00513         }
00514         else if ( Vec_PtrSize(vCut) < p->pPars->nLeafMax - 2 && p->pPars->fExtend )
00515         {
00516             if ( !Dar_ObjCutLevelAchieved(vCut, nLevelMin) )
00517             {
00518                 if ( Aig_NodeMffsExtendCut( pAig, pObj, vCut, vCut2 ) )
00519                 {
00520                     nNodesSaved2 = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut );
00521                     assert( nNodesSaved2 == nNodesSaved );
00522                 }
00523                 if ( Vec_PtrSize(vCut2) > p->pPars->nLeafMax )
00524                     Vec_PtrClear(vCut2);
00525                 if ( Vec_PtrSize(vCut2) > 0 )
00526                 {
00527                     p->nNodesExten++;
00528 //                    printf( "%d(%d) ", Vec_PtrSize(vCut), Vec_PtrSize(vCut2) );
00529                 }
00530             }
00531             else
00532                 p->nNodesBelow++;
00533         }
00534 p->timeCuts += clock() - clk;
00535 
00536         // try the cuts
00537 clk = clock();
00538         Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY;
00539         Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required );
00540 p->timeEval += clock() - clk;
00541 
00542         // check the best gain
00543         if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
00544         {
00545             if ( p->pGraphBest )
00546                 Kit_GraphFree( p->pGraphBest );
00547             continue;
00548         }
00549 //printf( "\n" );
00550 
00551         // if we end up here, a rewriting step is accepted
00552         nNodeBefore = Aig_ManNodeNum( pAig );
00553         pObjNew = Dar_RefactBuildGraph( pAig, p->vLeavesBest, p->pGraphBest );
00554         assert( (int)Aig_Regular(pObjNew)->Level <= Required );
00555         // replace the node
00556         Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
00557         // compare the gains
00558         nNodeAfter = Aig_ManNodeNum( pAig );
00559         assert( p->GainBest <= nNodeBefore - nNodeAfter );
00560         Kit_GraphFree( p->pGraphBest );
00561         p->nCutsUsed++;
00562 //        break;
00563     }
00564 p->timeTotal = clock() - clkStart;
00565 p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
00566 
00567 //    Bar_ProgressStop( pProgress );
00568     // put the nodes into the DFS order and reassign their IDs
00569 //    Aig_NtkReassignIds( p );
00570     // fix the levels
00571     Aig_ManFanoutStop( pAig );
00572     if ( p->pPars->fUpdateLevel )
00573         Aig_ManStopReverseLevels( pAig );
00574 
00575     // stop the rewriting manager
00576     Dar_ManRefStop( p );
00577     Aig_ManCheckPhase( pAig );
00578     if ( !Aig_ManCheck( pAig ) )
00579     {
00580         printf( "Dar_ManRefactor: The network check has failed.\n" );
00581         return 0;
00582     }
00583     return 1;
00584 
00585 }

int Dar_ManRewrite ( Aig_Man_t *  pAig,
Dar_RwrPar_t *  pPars 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file darCore.c.

00066 {
00067     Dar_Man_t * p;
00068 //    Bar_Progress_t * pProgress;
00069     Dar_Cut_t * pCut;
00070     Aig_Obj_t * pObj, * pObjNew;
00071     int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
00072     int clk = 0, clkStart;
00073     // prepare the library
00074     Dar_LibPrepare( pPars->nSubgMax ); 
00075     // create rewriting manager
00076     p = Dar_ManStart( pAig, pPars );
00077     // remove dangling nodes
00078     Aig_ManCleanup( pAig );
00079     // if updating levels is requested, start fanout and timing
00080     if ( p->pPars->fFanout )
00081         Aig_ManFanoutStart( pAig );
00082     if ( p->pPars->fUpdateLevel )
00083         Aig_ManStartReverseLevels( pAig, 0 );
00084     // set elementary cuts for the PIs
00085     Dar_ManCutsStart( p );
00086     // resynthesize each node once
00087     clkStart = clock();
00088     p->nNodesInit = Aig_ManNodeNum(pAig);
00089     nNodesOld = Vec_PtrSize( pAig->vObjs );
00090 
00091 //    pProgress = Bar_ProgressStart( stdout, nNodesOld );
00092     Aig_ManForEachObj( pAig, pObj, i )
00093 //    pProgress = Bar_ProgressStart( stdout, 100 );
00094 //    Aig_ManOrderStart( pAig );
00095 //    Aig_ManForEachNodeInOrder( pAig, pObj )
00096     {
00097 //        Bar_ProgressUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL );
00098 
00099 //        Bar_ProgressUpdate( pProgress, i, NULL );
00100         if ( !Aig_ObjIsNode(pObj) )
00101             continue;
00102         if ( i > nNodesOld )
00103             break;
00104 
00105         // consider freeing the cuts
00106 //        if ( (i & 0xFFF) == 0 && Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) > 100 )
00107 //            Dar_ManCutsStart( p );
00108 
00109         // compute cuts for the node
00110         p->nNodesTried++;
00111 clk = clock();
00112         Dar_ObjComputeCuts_rec( p, pObj );
00113 p->timeCuts += clock() - clk;
00114 
00115         // check if there is a trivial cut
00116         Dar_ObjForEachCut( pObj, pCut, k )
00117             if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id && Aig_ManObj(p->pAig, pCut->pLeaves[0])) )
00118                 break;
00119         if ( k < (int)pObj->nCuts )
00120         {
00121             assert( pCut->nLeaves < 2 );
00122             if ( pCut->nLeaves == 0 ) // replace by constant
00123             {
00124                 assert( pCut->uTruth == 0 || pCut->uTruth == 0xFFFF );
00125                 pObjNew = Aig_NotCond( Aig_ManConst1(p->pAig), pCut->uTruth==0 );
00126             }
00127             else
00128             {
00129                 assert( pCut->uTruth == 0xAAAA || pCut->uTruth == 0x5555 );
00130                 pObjNew = Aig_NotCond( Aig_ManObj(p->pAig, pCut->pLeaves[0]), pCut->uTruth==0x5555 );
00131             }
00132             // remove the old cuts
00133             Dar_ObjSetCuts( pObj, NULL );
00134             // replace the node
00135             Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
00136             continue;
00137         }
00138 
00139         // evaluate the cuts
00140         p->GainBest = -1;
00141         Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY;
00142         Dar_ObjForEachCut( pObj, pCut, k )
00143             Dar_LibEval( p, pObj, pCut, Required );
00144         // check the best gain
00145         if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
00146         {
00147 //            Aig_ObjOrderAdvance( pAig );
00148             continue;
00149         }
00150         // remove the old cuts
00151         Dar_ObjSetCuts( pObj, NULL );
00152         // if we end up here, a rewriting step is accepted
00153         nNodeBefore = Aig_ManNodeNum( pAig );
00154         pObjNew = Dar_LibBuildBest( p ); // pObjNew can be complemented!
00155         pObjNew = Aig_NotCond( pObjNew, Aig_ObjPhaseReal(pObjNew) ^ pObj->fPhase );
00156         assert( (int)Aig_Regular(pObjNew)->Level <= Required );
00157         // replace the node
00158         Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
00159         // compare the gains
00160         nNodeAfter = Aig_ManNodeNum( pAig );
00161         assert( p->GainBest <= nNodeBefore - nNodeAfter );
00162         // count gains of this class
00163         p->ClassGains[p->ClassBest] += nNodeBefore - nNodeAfter;
00164     }
00165 //    Aig_ManOrderStop( pAig );
00166 
00167 p->timeTotal = clock() - clkStart;
00168 p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
00169 
00170 //    Bar_ProgressStop( pProgress );
00171     p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20);
00172     Dar_ManCutsFree( p );
00173     // put the nodes into the DFS order and reassign their IDs
00174 //    Aig_NtkReassignIds( p );
00175     // fix the levels
00176 //    Aig_ManVerifyLevel( pAig );
00177     if ( p->pPars->fFanout )
00178         Aig_ManFanoutStop( pAig );
00179     if ( p->pPars->fUpdateLevel )
00180     {
00181 //        Aig_ManVerifyReverseLevel( pAig );
00182         Aig_ManStopReverseLevels( pAig );
00183     }
00184     // stop the rewriting manager
00185     Dar_ManStop( p );
00186     Aig_ManCheckPhase( pAig );
00187     // check
00188     if ( !Aig_ManCheck( pAig ) )
00189     {
00190         printf( "Aig_ManRewrite: The network check has failed.\n" );
00191         return 0;
00192     }
00193     return 1;
00194 }

Aig_Man_t* Dar_ManRewriteDefault ( Aig_Man_t *  pAig  ) 

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

FileName [darScript.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [Rewriting scripts.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
darScript.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

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

Synopsis [Performs one iteration of AIG rewriting.]

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file darScript.c.

00044 {
00045     Aig_Man_t * pTemp;
00046     Dar_RwrPar_t Pars, * pPars = &Pars;
00047     Dar_ManDefaultRwrParams( pPars );
00048     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00049     Aig_ManStop( pTemp );
00050     Dar_ManRewrite( pAig, pPars );
00051     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00052     Aig_ManStop( pTemp );
00053     return pAig;
00054 }

Aig_Man_t* Dar_ManRwsat ( Aig_Man_t *  pAig,
int  fBalance,
int  fVerbose 
)

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

Synopsis [Reproduces script "compress2".]

Description []

SideEffects [This procedure does not tighten level during restructuring.]

SeeAlso []

Definition at line 67 of file darScript.c.

00069 {
00070     Aig_Man_t * pTemp;
00071 
00072     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
00073     Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
00074 
00075     Dar_ManDefaultRwrParams( pParsRwr );
00076     Dar_ManDefaultRefParams( pParsRef );
00077 
00078     pParsRwr->fUpdateLevel = 0;
00079     pParsRef->fUpdateLevel = 0;
00080 
00081     pParsRwr->fVerbose = fVerbose;
00082     pParsRef->fVerbose = fVerbose;
00083 
00084     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00085     Aig_ManStop( pTemp );
00086     
00087     // rewrite
00088     Dar_ManRewrite( pAig, pParsRwr );
00089     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00090     Aig_ManStop( pTemp );
00091     
00092     // refactor
00093     Dar_ManRefactor( pAig, pParsRef );
00094     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00095     Aig_ManStop( pTemp );
00096 
00097     // balance
00098     if ( fBalance )
00099     {
00100     pAig = Dar_ManBalance( pTemp = pAig, 0 );
00101     Aig_ManStop( pTemp );
00102     }
00103     
00104     // rewrite
00105     Dar_ManRewrite( pAig, pParsRwr );
00106     pAig = Aig_ManDup( pTemp = pAig, 0 ); 
00107     Aig_ManStop( pTemp );
00108 
00109     return pAig;
00110 }

Generated on Tue Jan 5 12:18:16 2010 for abc70930 by  doxygen 1.6.1