src/aig/dar/darRefact.c File Reference

#include "darInt.h"
#include "kit.h"
Include dependency graph for darRefact.c:

Go to the source code of this file.

Data Structures

struct  Ref_Man_t_

Typedefs

typedef struct Ref_Man_t_ Ref_Man_t

Functions

void Dar_ManDefaultRefParams (Dar_RefPar_t *pPars)
Ref_Man_t * Dar_ManRefStart (Aig_Man_t *pAig, Dar_RefPar_t *pPars)
void Dar_ManRefPrintStats (Ref_Man_t *p)
void Dar_ManRefStop (Ref_Man_t *p)
void Ref_ObjComputeCuts (Aig_Man_t *pAig, Aig_Obj_t *pRoot, Vec_Vec_t *vCuts)
void Ref_ObjPrint (Aig_Obj_t *pObj)
int Dar_RefactTryGraph (Aig_Man_t *pAig, Aig_Obj_t *pRoot, Vec_Ptr_t *vCut, Kit_Graph_t *pGraph, int NodeMax, int LevelMax)
Aig_Obj_t * Dar_RefactBuildGraph (Aig_Man_t *pAig, Vec_Ptr_t *vCut, Kit_Graph_t *pGraph)
int Dar_ManRefactorTryCuts (Ref_Man_t *p, Aig_Obj_t *pObj, int nNodesSaved, int Required)
int Dar_ObjCutLevelAchieved (Vec_Ptr_t *vCut, int nLevelMin)
int Dar_ManRefactor (Aig_Man_t *pAig, Dar_RefPar_t *pPars)

Typedef Documentation

typedef struct Ref_Man_t_ Ref_Man_t

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

FileName [darRefact.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [Refactoring.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

] DECLARATIONS ///

Definition at line 29 of file darRefact.c.

Function Documentation

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 }

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_ManRefactorTryCuts ( Ref_Man_t *  p,
Aig_Obj_t *  pObj,
int  nNodesSaved,
int  Required 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 343 of file darRefact.c.

00344 {
00345     Vec_Ptr_t * vCut;
00346     Kit_Graph_t * pGraphCur;
00347     int k, RetValue, GainCur, nNodesAdded;
00348     unsigned * pTruth;
00349 
00350     p->GainBest = -1;
00351     p->pGraphBest = NULL;
00352     Vec_VecForEachLevel( p->vCuts, vCut, k )
00353     {
00354         if ( Vec_PtrSize(vCut) == 0 )
00355             continue;
00356 //        if ( Vec_PtrSize(vCut) != 0 && Vec_PtrSize(Vec_VecEntry(p->vCuts, k+1)) != 0 )
00357 //            continue;
00358 
00359         p->nCutsTried++;
00360         // get the cut nodes
00361         Aig_ObjCollectCut( pObj, vCut, p->vCutNodes );
00362         // get the truth table
00363         pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore );
00364         if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) )
00365         {
00366             p->GainBest = Vec_PtrSize(p->vCutNodes);
00367             p->pGraphBest = Kit_GraphCreateConst0();
00368             Vec_PtrCopy( p->vLeavesBest, vCut );
00369             return p->GainBest;
00370         }
00371         if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) )
00372         {
00373             p->GainBest = Vec_PtrSize(p->vCutNodes);
00374             p->pGraphBest = Kit_GraphCreateConst1();
00375             Vec_PtrCopy( p->vLeavesBest, vCut );
00376             return p->GainBest;
00377         }
00378 
00379         // try the positive phase
00380         RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
00381         if ( RetValue > -1 )
00382         {
00383             pGraphCur = Kit_SopFactor( p->vMemory, 0, Vec_PtrSize(vCut), p->vMemory );
00384             nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
00385             if ( nNodesAdded > -1 )
00386             {
00387                 GainCur = nNodesSaved - nNodesAdded;
00388                 if ( p->GainBest < GainCur || (p->GainBest == GainCur && 
00389                     (Kit_GraphIsConst(pGraphCur) || Kit_GraphRootLevel(pGraphCur) < Kit_GraphRootLevel(p->pGraphBest))) )
00390                 {
00391                     p->GainBest = GainCur;
00392                     if ( p->pGraphBest )
00393                         Kit_GraphFree( p->pGraphBest );
00394                     p->pGraphBest = pGraphCur;
00395                     Vec_PtrCopy( p->vLeavesBest, vCut );
00396                 }
00397                 else
00398                     Kit_GraphFree( pGraphCur );
00399             }
00400             else
00401                 Kit_GraphFree( pGraphCur );
00402         }
00403         // try negative phase
00404         Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
00405         RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
00406         if ( RetValue > -1 )
00407         {
00408             pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory );
00409             nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
00410             if ( nNodesAdded > -1 )
00411             {
00412                 GainCur = nNodesSaved - nNodesAdded;
00413                 if ( p->GainBest < GainCur || (p->GainBest == GainCur && 
00414                     (Kit_GraphIsConst(pGraphCur) || Kit_GraphRootLevel(pGraphCur) < Kit_GraphRootLevel(p->pGraphBest))) )
00415                 {
00416                     p->GainBest = GainCur;
00417                     if ( p->pGraphBest )
00418                         Kit_GraphFree( p->pGraphBest );
00419                     p->pGraphBest = pGraphCur;
00420                     Vec_PtrCopy( p->vLeavesBest, vCut );
00421                 }
00422                 else
00423                     Kit_GraphFree( pGraphCur );
00424             }
00425             else
00426                 Kit_GraphFree( pGraphCur );
00427         }
00428     }
00429     return p->GainBest;
00430 }

void Dar_ManRefPrintStats ( Ref_Man_t *  p  ) 

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

Synopsis [Prints out the statistics of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file darRefact.c.

00129 {
00130     int Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
00131     printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%).\n", 
00132         p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit );
00133     printf( "Tried = %6d. Below = %5d. Extended = %5d.  Used = %5d.  Levels = %4d.\n", 
00134         p->nNodesTried, p->nNodesBelow, p->nNodesExten, p->nCutsUsed, Aig_ManLevels(p->pAig) );
00135     PRT( "Cuts  ", p->timeCuts );
00136     PRT( "Eval  ", p->timeEval );
00137     PRT( "Other ", p->timeOther );
00138     PRT( "TOTAL ", p->timeTotal );
00139 }

Ref_Man_t* Dar_ManRefStart ( Aig_Man_t *  pAig,
Dar_RefPar_t *  pPars 
)

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

Synopsis [Starts the rewriting manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 99 of file darRefact.c.

00100 {
00101     Ref_Man_t * p;
00102     // start the manager
00103     p = ALLOC( Ref_Man_t, 1 );
00104     memset( p, 0, sizeof(Ref_Man_t) );
00105     p->pAig         = pAig;
00106     p->pPars        = pPars;
00107     // other data
00108     p->vCuts        = Vec_VecStart( pPars->nCutsMax );
00109     p->vTruthElem   = Vec_PtrAllocTruthTables( pPars->nLeafMax );
00110     p->vTruthStore  = Vec_PtrAllocSimInfo( 256, Kit_TruthWordNum(pPars->nLeafMax) );
00111     p->vMemory      = Vec_IntAlloc( 1 << 16 );
00112     p->vCutNodes    = Vec_PtrAlloc( 256 );
00113     p->vLeavesBest  = Vec_PtrAlloc( pPars->nLeafMax );
00114     return p;
00115 }

void Dar_ManRefStop ( Ref_Man_t *  p  ) 

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

Synopsis [Stops the rewriting manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 152 of file darRefact.c.

00153 {
00154     if ( p->pPars->fVerbose )
00155         Dar_ManRefPrintStats( p );
00156     Vec_VecFree( p->vCuts );
00157     Vec_PtrFree( p->vTruthElem );
00158     Vec_PtrFree( p->vTruthStore );
00159     Vec_PtrFree( p->vLeavesBest );
00160     Vec_IntFree( p->vMemory );
00161     Vec_PtrFree( p->vCutNodes );
00162     free( p );
00163 }

int Dar_ObjCutLevelAchieved ( Vec_Ptr_t *  vCut,
int  nLevelMin 
)

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

Synopsis [Returns 1 if a non-PI node has nLevelMin or below.]

Description []

SideEffects []

SeeAlso []

Definition at line 443 of file darRefact.c.

00444 {
00445     Aig_Obj_t * pObj;
00446     int i;
00447     Vec_PtrForEachEntry( vCut, pObj, i )
00448         if ( !Aig_ObjIsPi(pObj) && (int)pObj->Level <= nLevelMin )
00449             return 1;
00450     return 0;
00451 }

Aig_Obj_t* Dar_RefactBuildGraph ( Aig_Man_t *  pAig,
Vec_Ptr_t *  vCut,
Kit_Graph_t *  pGraph 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 297 of file darRefact.c.

00298 {
00299     Aig_Obj_t * pAnd0, * pAnd1;
00300     Kit_Node_t * pNode = NULL;
00301     int i;
00302     // check for constant function
00303     if ( Kit_GraphIsConst(pGraph) )
00304         return Aig_NotCond( Aig_ManConst1(pAig), Kit_GraphIsComplement(pGraph) );
00305     // set the leaves
00306     Kit_GraphForEachLeaf( pGraph, pNode, i )
00307         pNode->pFunc = Vec_PtrEntry(vCut, i);
00308     // check for a literal
00309     if ( Kit_GraphIsVar(pGraph) )
00310         return Aig_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
00311     // build the AIG nodes corresponding to the AND gates of the graph
00312 //printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) );
00313     Kit_GraphForEachNode( pGraph, pNode, i )
00314     {
00315         pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
00316         pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
00317         pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 );
00318 /*
00319 printf( "Checking " );
00320 Ref_ObjPrint( pAnd0 );
00321 printf( " and " );
00322 Ref_ObjPrint( pAnd1 );
00323 printf( "  Result " );
00324 Ref_ObjPrint( pNode->pFunc );
00325 printf( "\n" );
00326 */
00327     }
00328     // complement the result if necessary
00329     return Aig_NotCond( pNode->pFunc, Kit_GraphIsComplement(pGraph) );
00330 }

int Dar_RefactTryGraph ( Aig_Man_t *  pAig,
Aig_Obj_t *  pRoot,
Vec_Ptr_t *  vCut,
Kit_Graph_t *  pGraph,
int  NodeMax,
int  LevelMax 
)

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

Synopsis [Counts the number of new nodes added when using this graph.]

Description [AIG nodes for the fanins should be assigned to pNode->pFunc of the leaves of the graph before calling this procedure. Returns -1 if the number of nodes and levels exceeded the given limit or the number of levels exceeded the maximum allowed level.]

SideEffects []

SeeAlso []

Definition at line 212 of file darRefact.c.

00213 {
00214     Kit_Node_t * pNode, * pNode0, * pNode1;
00215     Aig_Obj_t * pAnd, * pAnd0, * pAnd1;
00216     int i, Counter, LevelNew, LevelOld;
00217     // check for constant function or a literal
00218     if ( Kit_GraphIsConst(pGraph) || Kit_GraphIsVar(pGraph) )
00219         return 0;
00220     // set the levels of the leaves
00221     Kit_GraphForEachLeaf( pGraph, pNode, i )
00222     {
00223         pNode->pFunc = Vec_PtrEntry(vCut, i);
00224         pNode->Level = Aig_Regular(pNode->pFunc)->Level;
00225         assert( Aig_Regular(pNode->pFunc)->Level < (1<<14)-1 );
00226     }
00227 //printf( "Trying:\n" );
00228     // compute the AIG size after adding the internal nodes
00229     Counter = 0;
00230     Kit_GraphForEachNode( pGraph, pNode, i )
00231     {
00232         // get the children of this node
00233         pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.Node );
00234         pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.Node );
00235         // get the AIG nodes corresponding to the children 
00236         pAnd0 = pNode0->pFunc; 
00237         pAnd1 = pNode1->pFunc; 
00238         if ( pAnd0 && pAnd1 )
00239         {
00240             // if they are both present, find the resulting node
00241             pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.fCompl );
00242             pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.fCompl );
00243             pAnd  = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 );
00244             // return -1 if the node is the same as the original root
00245             if ( Aig_Regular(pAnd) == pRoot )
00246                 return -1;
00247         }
00248         else
00249             pAnd = NULL;
00250         // count the number of added nodes
00251         if ( pAnd == NULL || Aig_ObjIsTravIdCurrent(pAig, Aig_Regular(pAnd)) )
00252         {
00253             if ( ++Counter > NodeMax )
00254                 return -1;
00255         }
00256         // count the number of new levels
00257         LevelNew = 1 + AIG_MAX( pNode0->Level, pNode1->Level );
00258         if ( pAnd )
00259         {
00260             if ( Aig_Regular(pAnd) == Aig_ManConst1(pAig) )
00261                 LevelNew = 0;
00262             else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd0) )
00263                 LevelNew = (int)Aig_Regular(pAnd0)->Level;
00264             else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd1) )
00265                 LevelNew = (int)Aig_Regular(pAnd1)->Level;
00266             LevelOld = (int)Aig_Regular(pAnd)->Level;
00267 //            assert( LevelNew == LevelOld );
00268         }
00269         if ( LevelNew > LevelMax )
00270             return -1;
00271         pNode->pFunc = pAnd;
00272         pNode->Level = LevelNew;
00273 /*
00274 printf( "Checking " );
00275 Ref_ObjPrint( pAnd0 );
00276 printf( " and " );
00277 Ref_ObjPrint( pAnd1 );
00278 printf( "  Result " );
00279 Ref_ObjPrint( pNode->pFunc );
00280 printf( "\n" );
00281 */
00282     }
00283     return Counter;
00284 }

void Ref_ObjComputeCuts ( Aig_Man_t *  pAig,
Aig_Obj_t *  pRoot,
Vec_Vec_t *  vCuts 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 176 of file darRefact.c.

00177 {
00178 }

void Ref_ObjPrint ( Aig_Obj_t *  pObj  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 191 of file darRefact.c.

00192 {
00193     printf( "%d", pObj? Aig_Regular(pObj)->Id : -1 );
00194     if ( pObj )
00195         printf( "(%d) ", Aig_IsComplement(pObj) );
00196 }

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