diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abc/abc.c | 37 | ||||
-rw-r--r-- | src/base/abc/abc.h | 26 | ||||
-rw-r--r-- | src/base/abc/abcAig.c | 1 | ||||
-rw-r--r-- | src/base/abc/abcReconv.c | 26 | ||||
-rw-r--r-- | src/base/abc/abcRefactor.c | 209 | ||||
-rw-r--r-- | src/base/abc/abcRefs.c | 26 | ||||
-rw-r--r-- | src/base/abc/abcResRef.c | 192 | ||||
-rw-r--r-- | src/base/abc/abcRewrite.c (renamed from src/base/abc/abcRes.c) | 67 | ||||
-rw-r--r-- | src/base/abc/abcStrash.c | 67 | ||||
-rw-r--r-- | src/base/abc/abcTiming.c | 43 | ||||
-rw-r--r-- | src/base/abc/module.make | 3 |
11 files changed, 394 insertions, 303 deletions
diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c index ca18265d..be813996 100644 --- a/src/base/abc/abc.c +++ b/src/base/abc/abc.c @@ -148,7 +148,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); Ft_FactorStartMan(); -// Rwt_ManExploreStart(); +// Rwt_Man4ExploreStart(); } /**Function************************************************************* @@ -166,7 +166,7 @@ void Abc_End() { Ft_FactorStopMan(); Abc_NtkFraigStoreClean(); -// Rwt_ManExplorePrint(); +// Rwt_Man4ExplorePrint(); } /**Function************************************************************* @@ -1323,20 +1323,23 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; bool fVerbose; + // external functions + extern void * Abc_NtkManRwrStart( char * pFileName ); + extern void Abc_NtkManRwrStop( void * p ); + extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk ); +/* { - Abc_ManRwr_t * p; + void * p; int fFlag = 0; - if ( fFlag ) p = Abc_NtkManRwrStart( NULL ); else p = Abc_NtkManRwrStart( "data.aaa" ); - Abc_NtkManRwrStop( p ); return 0; } - +*/ pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1406,22 +1409,23 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; - Abc_ManRef_t * p; - bool fVerbose; int nNodeSizeMax; int nConeSizeMax; + bool fUseDcs; + bool fVerbose; + extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUseDcs, bool fVerbose ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - p = Abc_NtkManRefStart(); - fVerbose = 0; nNodeSizeMax = 10; nConeSizeMax = 10; + fUseDcs = 0; + fVerbose = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ncvh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "ncdvh" ) ) != EOF ) { switch ( c ) { @@ -1447,6 +1451,9 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nConeSizeMax < 0 ) goto usage; break; + case 'd': + fUseDcs ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -1460,24 +1467,21 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); - Abc_NtkManRefStop( p ); return 1; } if ( !Abc_NtkIsAig(pNtk) ) { fprintf( pErr, "This command can only be applied to an AIG.\n" ); - Abc_NtkManRefStop( p ); return 1; } if ( Abc_NtkCountChoiceNodes(pNtk) ) { fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" ); - Abc_NtkManRefStop( p ); return 1; } // modify the current network - if ( !Abc_NtkRefactor( pNtk, p ) ) + if ( !Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose ) ) { fprintf( pErr, "Refactoring has failed.\n" ); return 1; @@ -1485,10 +1489,11 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: refactor [-n num] [-c num] [-vh]\n" ); + fprintf( pErr, "usage: refactor [-n num] [-c num] [-dvh]\n" ); fprintf( pErr, "\t performs technology-independent refactoring of the AIG\n" ); fprintf( pErr, "\t-n num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax ); fprintf( pErr, "\t-c num : the max support of the containing cone [default = %d]\n", nConeSizeMax ); + fprintf( pErr, "\t-d : toggle use of don't-cares [default = %s]\n", fUseDcs? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index b6d15951..18923f26 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -89,8 +89,6 @@ typedef struct Abc_Ntk_t_ Abc_Ntk_t; typedef struct Abc_Aig_t_ Abc_Aig_t; typedef struct Abc_ManTime_t_ Abc_ManTime_t; typedef struct Abc_ManCut_t_ Abc_ManCut_t; -typedef struct Abc_ManRef_t_ Abc_ManRef_t; -typedef struct Abc_ManRwr_t_ Abc_ManRwr_t; typedef struct Abc_Time_t_ Abc_Time_t; struct Abc_Time_t_ @@ -375,6 +373,7 @@ extern int Abc_AigGetLevelNum( Abc_Ntk_t * pNtk ); extern Abc_Obj_t * Abc_AigConst1( Abc_Aig_t * pMan ); extern Abc_Obj_t * Abc_AigReset( Abc_Aig_t * pMan ); extern Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); +extern Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); extern Abc_Obj_t * Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); extern Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); extern Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs ); @@ -494,33 +493,18 @@ extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode ) extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile ); extern void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode ); /*=== abcReconv.c ==========================================================*/ -extern Abc_ManCut_t * Abc_NtkManCutStart(); +extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax ); extern void Abc_NtkManCutStop( Abc_ManCut_t * p ); -extern void Abc_NodeFindCut( Abc_ManCut_t * p ); +extern Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot ); extern DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited ); extern void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult ); /*=== abcRefs.c ==========================================================*/ extern int Abc_NodeMffcSize( Abc_Obj_t * pNode ); extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode ); +extern void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain ); /*=== abcRenode.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple ); extern DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld ); -/*=== abcRes.c ==========================================================*/ -extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk ); -extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, Abc_ManRef_t * p ); -/*=== abcResRef.c ==========================================================*/ -extern Abc_ManRef_t * Abc_NtkManRefStart(); -extern void Abc_NtkManRefStop( Abc_ManRef_t * p ); -extern bool Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode ); -extern Vec_Int_t * Abc_NtkManRefResult( Abc_ManRef_t * p ); -/*=== abcResRwr.c ==========================================================*/ -extern Abc_ManRwr_t * Abc_NtkManRwrStart( char * pFileName ); -extern void Abc_NtkManRwrStop( Abc_ManRwr_t * p ); -extern void Abc_NtkManRwrStartCuts( Abc_ManRwr_t * p, Abc_Ntk_t * pNtk ); -extern void Abc_NodeRwrComputeCuts( Abc_ManRwr_t * p, Abc_Obj_t * pNode ); -extern int Abc_NodeRwrRewrite( Abc_ManRwr_t * p, Abc_Obj_t * pNode ); -extern Vec_Int_t * Abc_NtkManRwrDecs( Abc_ManRwr_t * p ); -extern Vec_Ptr_t * Abc_NtkManRwrFanins( Abc_ManRwr_t * p ); /*=== abcSat.c ==========================================================*/ extern bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose ); extern solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ); @@ -561,6 +545,7 @@ extern void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, /*=== abcStrash.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes ); extern Abc_Obj_t * Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm ); +extern int Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, Vec_Int_t * vLevels, int NodeMax, int LevelMax ); extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ); /*=== abcSweep.c ==========================================================*/ @@ -582,6 +567,7 @@ extern void Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk ); extern float * Abc_NtkGetCiArrivalFloats( Abc_Ntk_t * pNtk ); extern Abc_Time_t * Abc_NtkGetCiArrivalTimes( Abc_Ntk_t * pNtk ); extern float Abc_NtkDelayTrace( Abc_Ntk_t * pNtk ); +extern Vec_Int_t * Abc_NtkGetRequiredLevels( Abc_Ntk_t * pNtk ); /*=== abcTravId.c ==========================================================*/ extern void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk ); extern void Abc_NodeSetTravId( Abc_Obj_t * pObj, int TravId ); diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 2f123dd3..25237868 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -78,7 +78,6 @@ static inline unsigned Abc_HashKey2( Abc_Obj_t * p0, Abc_Obj_t * p1, int TableSi // structural hash table procedures static Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); static Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, Abc_Obj_t * pAnd ); -static Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); static void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis ); static void Abc_AigResize( Abc_Aig_t * pMan ); // incremental AIG procedures diff --git a/src/base/abc/abcReconv.c b/src/base/abc/abcReconv.c index 7f4588a2..82adc92c 100644 --- a/src/base/abc/abcReconv.c +++ b/src/base/abc/abcReconv.c @@ -31,7 +31,6 @@ struct Abc_ManCut_t_ int nNodeSizeMax; // the limit on the size of the supernode int nConeSizeMax; // the limit on the size of the containing cone // internal parameters - Abc_Obj_t * pNode; // the node currently considered Vec_Ptr_t * vFaninsNode; // fanins of the supernode Vec_Ptr_t * vInsideNode; // inside of the supernode Vec_Ptr_t * vFaninsCone; // fanins of the containing cone @@ -60,20 +59,20 @@ static void Abc_NodeConeUnmark( Vec_Ptr_t * vVisited ); SeeAlso [] ***********************************************************************/ -void Abc_NodeFindCut( Abc_ManCut_t * p ) +Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot ) { - Abc_Obj_t * pNode = p->pNode; + Abc_Obj_t * pNode; int i; // mark TFI using fMarkA Vec_PtrClear( p->vVisited ); - Abc_NodeConeMarkCollect_rec( pNode, p->vVisited ); + Abc_NodeConeMarkCollect_rec( pRoot, p->vVisited ); // start the reconvergence-driven node Vec_PtrClear( p->vInsideNode ); Vec_PtrClear( p->vFaninsNode ); - Vec_PtrPush( p->vFaninsNode, pNode ); - pNode->fMarkB = 1; + Vec_PtrPush( p->vFaninsNode, pRoot ); + pRoot->fMarkB = 1; // compute reconvergence-driven node while ( Abc_NodeFindCut_int( p->vInsideNode, p->vFaninsNode, p->nNodeSizeMax ) ); @@ -107,6 +106,7 @@ void Abc_NodeFindCut( Abc_ManCut_t * p ) // unmark TFI using fMarkA Abc_NodeConeUnmark( p->vVisited ); + return p->vFaninsNode; } /**Function************************************************************* @@ -311,16 +311,18 @@ DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, V SeeAlso [] ***********************************************************************/ -Abc_ManCut_t * Abc_NtkManCutStart() +Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax ) { Abc_ManCut_t * p; p = ALLOC( Abc_ManCut_t, 1 ); memset( p, 0, sizeof(Abc_ManCut_t) ); - p->vFaninsNode = Vec_PtrAlloc( 100 ); - p->vInsideNode = Vec_PtrAlloc( 100 ); - p->vFaninsCone = Vec_PtrAlloc( 100 ); - p->vInsideCone = Vec_PtrAlloc( 100 ); - p->vVisited = Vec_PtrAlloc( 100 ); + p->vFaninsNode = Vec_PtrAlloc( 100 ); + p->vInsideNode = Vec_PtrAlloc( 100 ); + p->vFaninsCone = Vec_PtrAlloc( 100 ); + p->vInsideCone = Vec_PtrAlloc( 100 ); + p->vVisited = Vec_PtrAlloc( 100 ); + p->nNodeSizeMax = nNodeSizeMax; + p->nConeSizeMax = nConeSizeMax; return p; } diff --git a/src/base/abc/abcRefactor.c b/src/base/abc/abcRefactor.c new file mode 100644 index 00000000..b60b0969 --- /dev/null +++ b/src/base/abc/abcRefactor.c @@ -0,0 +1,209 @@ +/**CFile**************************************************************** + + FileName [abcResRef.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Resynthesis based on refactoring.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcResRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "ft.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Abc_ManRef_t_ Abc_ManRef_t; +struct Abc_ManRef_t_ +{ + // user specified parameters + int nNodeSizeMax; // the limit on the size of the supernode + int nConeSizeMax; // the limit on the size of the containing cone + int fVerbose; // the verbosity flag + // internal parameters + DdManager * dd; // the BDD manager + Vec_Int_t * vReqTimes; // required times for each node + Vec_Str_t * vCube; // temporary + Vec_Int_t * vForm; // temporary + Vec_Int_t * vLevNums; // temporary + Vec_Ptr_t * vVisited; // temporary + // runtime statistics + int time1; + int time2; + int time3; +}; + +static Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, int fVerbose ); +static void Abc_NtkManRefStop( Abc_ManRef_t * p ); +static Vec_Int_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs incremental resynthesis of the AIG.] + + Description [Starting from each node, computes a reconvergence-driven cut, + derives BDD of the cut function, constructs ISOP, factors the cover, + and replaces the current implementation of the MFFC of the cut by the + new factored form if the number of AIG nodes is reduced. Returns the + number of AIG nodes saved.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUseDcs, bool fVerbose ) +{ + int fCheck = 1; + ProgressBar * pProgress; + Abc_ManRef_t * pManRef; + Abc_ManCut_t * pManCut; + Vec_Ptr_t * vFanins; + Vec_Int_t * vForm; + Abc_Obj_t * pNode; + int i, nNodes; + + assert( Abc_NtkIsAig(pNtk) ); + // start the managers + pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax ); + pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fVerbose ); + pManRef->vReqTimes = Abc_NtkGetRequiredLevels( pNtk ); + + // resynthesize each node once + nNodes = Abc_NtkObjNumMax(pNtk); + pProgress = Extra_ProgressBarStart( stdout, nNodes ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, nNodes, NULL ); + // compute a reconvergence-driven cut + vFanins = Abc_NodeFindCut( pManCut, pNode ); + // evaluate this cut + vForm = Abc_NodeRefactor( pManRef, pNode, vFanins ); + // if acceptable replacement found, update the graph + if ( vForm ) + Abc_NodeUpdate( pNode, vFanins, vForm, 0 ); + // check the improvement + if ( i == nNodes ) + break; + } + Extra_ProgressBarStop( pProgress ); + + // delete the managers + Abc_NtkManCutStop( pManCut ); + Abc_NtkManRefStop( pManRef ); + // check + if ( fCheck && !Abc_NtkCheck( pNtk ) ) + { + printf( "Abc_NtkRewrite: The network check has failed.\n" ); + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Resynthesizes the node using refactoring.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins ) +{ + Vec_Int_t * vForm; + DdNode * bFuncNode; + int nNodesSaved, RetValue; + char * pSop; + + // get the cover + bFuncNode = Abc_NodeConeBdd( p->dd, p->dd->vars, pNode, vFanins, p->vVisited ); Cudd_Ref( bFuncNode ); + pSop = Abc_ConvertBddToSop( NULL, p->dd, bFuncNode, bFuncNode, vFanins->nSize, p->vCube, -1 ); + Cudd_RecursiveDeref( p->dd, bFuncNode ); + // derive the factored form + vForm = Ft_Factor( pSop ); + free( pSop ); + + // label MFFC with current ID + nNodesSaved = Abc_NodeMffcLabel( pNode ); + // detect how many unlabeled nodes will be reused + RetValue = Abc_NodeStrashDecCount( pNode->pNtk->pManFunc, vFanins, vForm, + p->vLevNums, nNodesSaved, Vec_IntEntry( p->vReqTimes, pNode->Id ) ); + if ( RetValue >= 0 ) + return vForm; + Vec_IntFree( vForm ); + return vForm; +} + +/**Function************************************************************* + + Synopsis [Starts the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, int fVerbose ) +{ + Abc_ManRef_t * p; + p = ALLOC( Abc_ManRef_t, 1 ); + memset( p, 0, sizeof(Abc_ManRef_t) ); + p->vCube = Vec_StrAlloc( 100 ); + p->vLevNums = Vec_IntAlloc( 100 ); + p->vVisited = Vec_PtrAlloc( 100 ); + p->nNodeSizeMax = nNodeSizeMax; + p->nConeSizeMax = nConeSizeMax; + p->fVerbose = fVerbose; + // start the BDD manager + p->dd = Cudd_Init( p->nNodeSizeMax + p->nConeSizeMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Cudd_zddVarsFromBddVars( p->dd, 2 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkManRefStop( Abc_ManRef_t * p ) +{ + Extra_StopManager( p->dd ); + Vec_IntFree( p->vReqTimes ); + Vec_PtrFree( p->vVisited ); + Vec_IntFree( p->vLevNums ); + Vec_StrFree( p->vCube ); + free( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c index 96e8a3b2..764dc165 100644 --- a/src/base/abc/abcRefs.c +++ b/src/base/abc/abcRefs.c @@ -117,6 +117,32 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel ) return Counter; } +/**Function************************************************************* + + Synopsis [Replaces MFFC of the node by the new factored.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain ) +{ + Abc_Obj_t * pNodeNew; + int nNodesNew, nNodesOld; + nNodesOld = Abc_NtkNodeNum(pNode->pNtk); + // create the new structure of nodes + assert( Vec_PtrSize(vFanins) < Vec_IntSize(vForm) ); + pNodeNew = Abc_NodeStrashDec( pNode->pNtk->pManFunc, vFanins, vForm ); + // remove the old nodes + Abc_AigReplace( pNode->pNtk->pManFunc, pNode, pNodeNew ); + // compare the gains + nNodesNew = Abc_NtkNodeNum(pNode->pNtk); + assert( nGain <= nNodesOld - nNodesNew ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcResRef.c b/src/base/abc/abcResRef.c deleted file mode 100644 index fb806ad8..00000000 --- a/src/base/abc/abcResRef.c +++ /dev/null @@ -1,192 +0,0 @@ -/**CFile**************************************************************** - - FileName [abcResRef.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [Resynthesis based on refactoring.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: abcResRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -struct Abc_ManRef_t_ -{ - // user specified parameters - int nNodeSizeMax; // the limit on the size of the supernode - int nConeSizeMax; // the limit on the size of the containing cone - int fVerbose; // the verbosity flag - // the node currently processed - Abc_Obj_t * pNode; // the node currently considered - // internal parameters - DdManager * dd; // the BDD manager - DdNode * bCubeX; // the cube of PI variables - Vec_Str_t * vCube; // temporary cube for generating covers - Vec_Int_t * vForm; // the factored form (temporary) - // runtime statistics - int time1; - int time2; - int time3; - int time4; -}; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Resynthesizes the node using refactoring.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -bool Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode ) -{ - return 0; -} - -/**Function************************************************************* - - Synopsis [Derives the factored form of the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -/* -Vec_Int_t * Abc_NodeRefactor( Abc_ManRef_t * p ) -{ - Vec_Int_t * vForm; - DdManager * dd = p->dd; - DdNode * bFuncNode, * bFuncCone, * bCare, * bFuncOn, * bFuncOnDc; - char * pSop; - int nFanins; - - assert( p->vFaninsNode->nSize < p->nNodeSizeMax ); - assert( p->vFaninsCone->nSize < p->nConeSizeMax ); - - // get the function of the node - bFuncNode = Abc_NodeConeBdd( dd, p->dd->vars, p->pNode, p->vFaninsNode, p->vVisited ); - Cudd_Ref( bFuncNode ); - nFanins = p->vFaninsNode->nSize; - if ( p->nConeSizeMax > p->nNodeSizeMax ) - { - // get the function of the cone - bFuncCone = Abc_NodeConeBdd( dd, p->dd->vars + p->nNodeSizeMax, p->pNode, p->vFaninsCone, p->vVisited ); - Cudd_Ref( bFuncCone ); - // get the care set - bCare = Cudd_bddXorExistAbstract( p->dd, Cudd_Not(bFuncNode), bFuncCone, p->bCubeX ); Cudd_Ref( bCare ); - Cudd_RecursiveDeref( dd, bFuncCone ); - // compute the on-set and off-set of the function of the node - bFuncOn = Cudd_bddAnd( dd, bFuncNode, bCare ); Cudd_Ref( bFuncOn ); - bFuncOnDc = Cudd_bddAnd( dd, Cudd_Not(bFuncNode), bCare ); Cudd_Ref( bFuncOnDc ); - bFuncOnDc = Cudd_Not( bFuncOnDc ); - Cudd_RecursiveDeref( dd, bCare ); - // get the cover - pSop = Abc_ConvertBddToSop( NULL, dd, bFuncOn, bFuncOnDc, nFanins, p->vCube, -1 ); - Cudd_RecursiveDeref( dd, bFuncOn ); - Cudd_RecursiveDeref( dd, bFuncOnDc ); - } - else - { - // get the cover - pSop = Abc_ConvertBddToSop( NULL, dd, bFuncNode, bFuncNode, nFanins, p->vCube, -1 ); - } - Cudd_RecursiveDeref( dd, bFuncNode ); - // derive the factored form - vForm = Ft_Factor( pSop ); - free( pSop ); - return vForm; -} -*/ - - -/**Function************************************************************* - - Synopsis [Starts the resynthesis manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_ManRef_t * Abc_NtkManRefStart() -{ - Abc_ManRef_t * p; - p = ALLOC( Abc_ManRef_t, 1 ); - memset( p, 0, sizeof(Abc_ManRef_t) ); - p->vCube = Vec_StrAlloc( 100 ); - - - // start the BDD manager - p->dd = Cudd_Init( p->nNodeSizeMax + p->nConeSizeMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - Cudd_zddVarsFromBddVars( p->dd, 2 ); - p->bCubeX = Extra_bddComputeRangeCube( p->dd, p->nNodeSizeMax, p->dd->size ); Cudd_Ref( p->bCubeX ); - - return p; -} - -/**Function************************************************************* - - Synopsis [Stops the resynthesis manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkManRefStop( Abc_ManRef_t * p ) -{ - if ( p->bCubeX ) Cudd_RecursiveDeref( p->dd, p->bCubeX ); - if ( p->dd ) Extra_StopManager( p->dd ); - Vec_StrFree( p->vCube ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Stops the resynthesis manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Abc_NtkManRefResult( Abc_ManRef_t * p ) -{ - return p->vForm; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/abc/abcRes.c b/src/base/abc/abcRewrite.c index 7ab60376..437448de 100644 --- a/src/base/abc/abcRes.c +++ b/src/base/abc/abcRewrite.c @@ -19,14 +19,12 @@ ***********************************************************************/ #include "abc.h" -#include "ft.h" +#include "rwr.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// @@ -46,14 +44,14 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk ) { int fCheck = 1; ProgressBar * pProgress; - Abc_ManRwr_t * p; + Rwr_Man_t * p; Abc_Obj_t * pNode; int i, nNodes, nGain; assert( Abc_NtkIsAig(pNtk) ); // start the rewriting manager - p = Abc_NtkManRwrStart( "data.aaa" ); - Abc_NtkManRwrStartCuts( p, pNtk ); + p = Rwr_ManStart( "data.aaa" ); + Rwr_ManPrepareNetwork( p, pNtk ); // resynthesize each node once nNodes = Abc_NtkObjNumMax(pNtk); @@ -61,19 +59,16 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk ) Abc_NtkForEachNode( pNtk, pNode, i ) { Extra_ProgressBarUpdate( pProgress, nNodes, NULL ); - // compute the cuts of the node - Abc_NodeRwrComputeCuts( p, pNode ); // for each cut, try to resynthesize it - if ( (nGain = Abc_NodeRwrRewrite( p, pNode )) >= 0 ) - Abc_NodeUpdate( pNode, Abc_NtkManRwrFanins(p), Abc_NtkManRwrDecs(p), nGain ); + if ( (nGain = Rwr_NodeRewrite( p, pNode )) >= 0 ) + Abc_NodeUpdate( pNode, Rwr_ManReadFanins(p), Rwr_ManReadDecs(p), nGain ); // check the improvement if ( i == nNodes ) break; } Extra_ProgressBarStop( pProgress ); - // delete the manager - Abc_NtkManRwrStop( p ); + Rwr_ManStop( p ); // check if ( fCheck && !Abc_NtkCheck( pNtk ) ) { @@ -84,54 +79,6 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk ) } -/**Function************************************************************* - - Synopsis [Performs incremental resynthesis of the AIG.] - - Description [Starting from each node, computes a reconvergence-driven cut, - derives BDD of the cut function, constructs ISOP, factors the cover, - and replaces the current implementation of the MFFC of the cut by the - new factored form if the number of AIG nodes is reduced. Returns the - number of AIG nodes saved.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkRefactor( Abc_Ntk_t * pNtk, Abc_ManRef_t * p ) -{ - int fCheck = 1; - return 1; -} - -/**Function************************************************************* - - Synopsis [Replaces MFFC of the node by the new factored.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain ) -{ - Abc_Obj_t * pNodeNew; - int nNodesNew, nNodesOld; - nNodesOld = Abc_NtkNodeNum(pNode->pNtk); - // create the new structure of nodes - assert( Vec_PtrSize(vFanins) < Vec_IntSize(vForm) ); - pNodeNew = Abc_NodeStrashDec( pNode->pNtk->pManFunc, vFanins, vForm ); - // remove the old nodes - Abc_AigReplace( pNode->pNtk->pManFunc, pNode, pNodeNew ); - // compare the gains - nNodesNew = Abc_NtkNodeNum(pNode->pNtk); - assert( nGain <= nNodesOld - nNodesNew ); -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c index e9fed474..403b5be3 100644 --- a/src/base/abc/abcStrash.c +++ b/src/base/abc/abcStrash.c @@ -320,7 +320,7 @@ Abc_Obj_t * Abc_NodeStrashFactor2( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * p /**Function************************************************************* - Synopsis [Strashes one logic node using its SOP.] + Synopsis [Strashes the factored form into the AIG.] Description [] @@ -365,6 +365,71 @@ Abc_Obj_t * Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t /**Function************************************************************* + Synopsis [Counts the number of new nodes added when using this factored form,] + + Description [Returns -1 if the number of nodes and levels exceeded the given limit.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, Vec_Int_t * vLevels, int NodeMax, int LevelMax ) +{ + Abc_Obj_t * pAnd, * pAnd0, * pAnd1; + Ft_Node_t * pFtNode; + int i, nVars, Counter, LevelNew; + + // sanity checks + nVars = Ft_FactorGetNumVars( vForm ); + assert( nVars >= 0 ); + assert( vForm->nSize > nVars ); + assert( nVars == vFanins->nSize ); + + // check for constant function + pFtNode = Ft_NodeRead( vForm, 0 ); + if ( pFtNode->fConst ) + return 0; + + // set the levels + Vec_IntClear( vLevels ); + Vec_PtrForEachEntry( vFanins, pAnd, i ) + Vec_IntPush( vLevels, pAnd->Level ); + + // compute the function of other nodes + Counter = 0; + for ( i = nVars; i < vForm->nSize; i++ ) + { + pFtNode = Ft_NodeRead( vForm, i ); + pAnd0 = Abc_ObjNotCond( Vec_PtrEntry(vFanins, pFtNode->iFanin0), pFtNode->fCompl0 ); + if ( pAnd0 ) + { + pAnd1 = Abc_ObjNotCond( Vec_PtrEntry(vFanins, pFtNode->iFanin1), pFtNode->fCompl1 ); + pAnd = pAnd1? Abc_AigAndLookup( pMan, pAnd0, pAnd1 ) : NULL; + } + else + pAnd = NULL; + // count the number of added nodes + if ( pAnd == NULL || Abc_NodeIsTravIdCurrent(pAnd) ) + { + Counter++; + if ( Counter > NodeMax ) + return -1; + } + // count the number of new levels + LevelNew = 1 + ABC_MAX( Vec_IntEntry(vLevels, pFtNode->iFanin0), Vec_IntEntry(vLevels, pFtNode->iFanin1) ); + assert( pAnd == NULL || LevelNew == (int)Abc_ObjRegular(pAnd)->Level ); + if ( LevelNew > LevelMax ) + return -1; + Vec_PtrPush( vFanins, pAnd ); + Vec_IntPush( vLevels, LevelNew ); + } + assert( vForm->nSize = vFanins->nSize ); + return Counter; +} + +/**Function************************************************************* + Synopsis [Appends the second network to the first.] Description [Modifies the first network by adding the logic of the second. diff --git a/src/base/abc/abcTiming.c b/src/base/abc/abcTiming.c index d91a4443..10f8ae98 100644 --- a/src/base/abc/abcTiming.c +++ b/src/base/abc/abcTiming.c @@ -626,6 +626,49 @@ void Abc_NodeDelayTraceArrival( Abc_Obj_t * pNode ) pTimeOut->Worst = ABC_MAX( pTimeOut->Rise, pTimeOut->Fall ); } +/**Function************************************************************* + + Synopsis [Creates the array of required times.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkGetRequiredLevels( 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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/module.make b/src/base/abc/module.make index ee494926..b05cf03b 100644 --- a/src/base/abc/module.make +++ b/src/base/abc/module.make @@ -20,7 +20,8 @@ SRC += src/base/abc/abc.c \ src/base/abc/abcPrint.c \ src/base/abc/abcRefs.c \ src/base/abc/abcRenode.c \ - src/base/abc/abcRes.c \ + src/base/abc/abcRefactor.c \ + src/base/abc/abcRewrite.c \ src/base/abc/abcSat.c \ src/base/abc/abcSeq.c \ src/base/abc/abcSeqRetime.c \ |