summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.c37
-rw-r--r--src/base/abc/abc.h26
-rw-r--r--src/base/abc/abcAig.c1
-rw-r--r--src/base/abc/abcReconv.c26
-rw-r--r--src/base/abc/abcRefactor.c209
-rw-r--r--src/base/abc/abcRefs.c26
-rw-r--r--src/base/abc/abcResRef.c192
-rw-r--r--src/base/abc/abcRewrite.c (renamed from src/base/abc/abcRes.c)67
-rw-r--r--src/base/abc/abcStrash.c67
-rw-r--r--src/base/abc/abcTiming.c43
-rw-r--r--src/base/abc/module.make3
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 \