summaryrefslogtreecommitdiffstats
path: root/src/aig/dar
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/dar')
-rw-r--r--src/aig/dar/darBalance.c18
-rw-r--r--src/aig/dar/darCore.c47
-rw-r--r--src/aig/dar/darCut.c50
-rw-r--r--src/aig/dar/darInt.h16
-rw-r--r--src/aig/dar/darLib.c268
-rw-r--r--src/aig/dar/darMan.c21
-rw-r--r--src/aig/dar/darRefact.c48
-rw-r--r--src/aig/dar/darResub.c48
-rw-r--r--src/aig/dar/darScript.c48
-rw-r--r--src/aig/dar/dar_.c2
-rw-r--r--src/aig/dar/module.make3
11 files changed, 469 insertions, 100 deletions
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index a1502382..969e5253 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -49,7 +49,7 @@ static Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig
Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
{
Aig_Man_t * pNew;
- Aig_Obj_t * pObj, * pObjNew;
+ Aig_Obj_t * pObj, * pDriver, * pObjNew;
Vec_Vec_t * vStore;
int i;
// create the new manager
@@ -63,14 +63,15 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
vStore = Vec_VecAlloc( 50 );
Aig_ManForEachPo( p, pObj, i )
{
- pObjNew = Dar_Balance_rec( pNew, Aig_ObjFanin0(pObj), vStore, 0, fUpdateLevel );
- Aig_ObjCreatePo( pNew, Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) ) );
+ pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+ pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+ pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+ Aig_ObjCreatePo( pNew, pObjNew );
}
Vec_VecFree( vStore );
// remove dangling nodes
-// Aig_ManCreateRefs( pNew );
-// if ( i = Aig_ManCleanup( pNew ) )
-// printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
+ if ( i = Aig_ManCleanup( pNew ) )
+ printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
// check the resulting AIG
if ( !Aig_ManCheck(pNew) )
printf( "Dar_ManBalance(): The check has failed.\n" );
@@ -94,6 +95,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
Vec_Ptr_t * vSuper;
int i;
assert( !Aig_IsComplement(pObjOld) );
+ assert( !Aig_ObjIsBuf(pObjOld) );
// return if the result is known
if ( pObjOld->pData )
return pObjOld->pData;
@@ -157,8 +159,8 @@ int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper
assert( !Aig_IsComplement(pObj) );
assert( Aig_ObjIsNode(pObj) );
// go through the branches
- RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjChild0(pObj), vSuper );
- RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjChild1(pObj), vSuper );
+ RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
+ RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
if ( RetValue1 == -1 || RetValue2 == -1 )
return -1;
// return 1 if at least one branch has a duplicate
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index a617f5d6..e7186e83 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -43,7 +43,7 @@ void Dar_ManDefaultParams( Dar_Par_t * pPars )
{
memset( pPars, 0, sizeof(Dar_Par_t) );
pPars->nCutsMax = 8;
- pPars->nSubgMax = 4;
+ pPars->nSubgMax = 5; // 5 is a "magic number"
pPars->fUpdateLevel = 0;
pPars->fUseZeros = 0;
pPars->fVerbose = 0;
@@ -69,18 +69,18 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars )
Aig_Obj_t * pObj, * pObjNew;
int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
int clk = 0, clkStart;
+ // prepare the library
+ Dar_LibPrepare( pPars->nSubgMax );
// create rewriting manager
p = Dar_ManStart( pAig, pPars );
// remove dangling nodes
Aig_ManCleanup( pAig );
+ // if updating levels is requested, start fanout and timing
+ Aig_ManCreateFanout( pAig );
+ if ( p->pPars->fUpdateLevel )
+ Aig_ManStartReverseLevels( pAig, 0 );
// set elementary cuts for the PIs
-// Dar_ManSetupPis( p );
- Aig_ManCleanData( pAig );
- Dar_ObjPrepareCuts( p, Aig_ManConst1(pAig) );
- Aig_ManForEachPi( pAig, pObj, i )
- Dar_ObjPrepareCuts( p, pObj );
-// if ( p->pPars->fUpdateLevel )
-// Aig_NtkStartReverseLevels( p );
+ Dar_ManCutsStart( p );
// resynthesize each node once
clkStart = clock();
p->nNodesInit = Aig_ManNodeNum(pAig);
@@ -93,6 +93,10 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars )
continue;
if ( i > nNodesOld )
break;
+ // consider freeing the cuts
+// if ( (i & 0xFFF) == 0 && Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) > 100 )
+// Dar_ManCutsStart( p );
+
// compute cuts for the node
clk = clock();
Dar_ObjComputeCuts_rec( p, pObj );
@@ -100,7 +104,7 @@ p->timeCuts += clock() - clk;
// check if there is a trivial cut
Dar_ObjForEachCut( pObj, pCut, k )
- if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id) )
+ if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id && Aig_ManObj(p->pAig, pCut->pLeaves[0])) )
break;
if ( k < (int)pObj->nCuts )
{
@@ -115,10 +119,10 @@ p->timeCuts += clock() - clk;
assert( pCut->uTruth == 0xAAAA || pCut->uTruth == 0x5555 );
pObjNew = Aig_NotCond( Aig_ManObj(p->pAig, pCut->pLeaves[0]), pCut->uTruth==0x5555 );
}
- // replace the node
- Aig_ObjReplace( pAig, pObj, pObjNew, 1 );
// remove the old cuts
Dar_ObjSetCuts( pObj, NULL );
+ // replace the node
+ Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
continue;
}
@@ -128,17 +132,17 @@ p->timeCuts += clock() - clk;
Dar_ObjForEachCut( pObj, pCut, k )
Dar_LibEval( p, pObj, pCut, Required );
// check the best gain
- if ( !(p->GainBest > 0 || p->GainBest == 0 && p->pPars->fUseZeros) )
+ if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
continue;
+ // remove the old cuts
+ Dar_ObjSetCuts( pObj, NULL );
// if we end up here, a rewriting step is accepted
nNodeBefore = Aig_ManNodeNum( pAig );
pObjNew = Dar_LibBuildBest( p );
pObjNew = Aig_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase );
assert( (int)Aig_Regular(pObjNew)->Level <= Required );
// replace the node
- Aig_ObjReplace( pAig, pObj, pObjNew, 1 );
- // remove the old cuts
- Dar_ObjSetCuts( pObj, NULL );
+ Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
// compare the gains
nNodeAfter = Aig_ManNodeNum( pAig );
assert( p->GainBest <= nNodeBefore - nNodeAfter );
@@ -151,13 +155,14 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
Extra_ProgressBarStop( pProgress );
p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20);
Dar_ManCutsFree( p );
- // stop the rewriting manager
- Dar_ManStop( p );
// put the nodes into the DFS order and reassign their IDs
// Aig_NtkReassignIds( p );
// fix the levels
-// if ( p->pPars->fUpdateLevel )
-// Aig_NtkStopReverseLevels( p );
+ Aig_ManDeleteFanout( pAig );
+ if ( p->pPars->fUpdateLevel )
+ Aig_ManStopReverseLevels( pAig );
+ // stop the rewriting manager
+ Dar_ManStop( p );
// check
if ( !Aig_ManCheck( pAig ) )
{
@@ -190,9 +195,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig )
// remove dangling nodes
Aig_ManCleanup( pAig );
// set elementary cuts for the PIs
-// Dar_ManSetupPis( p );
- Aig_ManForEachPi( pAig, pObj, i )
- Dar_ObjPrepareCuts( p, pObj );
+ Dar_ManCutsStart( p );
// compute cuts for each nodes in the topological order
Aig_ManForEachObj( pAig, pObj, i )
{
diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c
index af9d1227..08bd77a9 100644
--- a/src/aig/dar/darCut.c
+++ b/src/aig/dar/darCut.c
@@ -62,20 +62,25 @@ static inline int Dar_WordCountOnes( unsigned uWord )
static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Aig_Obj_t * pLeaf;
- int i, Value;
+ int i, Value, nOnes;
assert( pCut->fUsed );
- if ( pCut->nLeaves < 2 )
- return 1001;
Value = 0;
+ nOnes = 0;
Dar_CutForEachLeaf( p->pAig, pCut, pLeaf, i )
{
if ( pLeaf == NULL )
return 0;
assert( pLeaf != NULL );
Value += pLeaf->nRefs;
+ nOnes += (pLeaf->nRefs == 1);
}
+ if ( pCut->nLeaves < 2 )
+ return 1001;
+// Value = Value * 100 / pCut->nLeaves;
if ( Value > 1000 )
Value = 1000;
+ if ( nOnes > 3 )
+ Value = 5 - nOnes;
return Value;
}
@@ -83,7 +88,7 @@ static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut )
Synopsis [Returns the next free cut to use.]
- Description []
+ Description [Uses the cut with the smallest value.]
SideEffects []
@@ -114,6 +119,14 @@ static inline Dar_Cut_t * Dar_CutFindFree( Dar_Man_t * p, Aig_Obj_t * pObj )
pCutMax = pCut;
}
}
+ if ( pCutMax == NULL )
+ {
+ Dar_ObjForEachCutAll( pObj, pCut, i )
+ {
+ if ( pCutMax == NULL || pCutMax->Value > pCut->Value )
+ pCutMax = pCut;
+ }
+ }
assert( pCutMax != NULL );
pCutMax->fUsed = 0;
return pCutMax;
@@ -466,7 +479,6 @@ static inline int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
unsigned uPhase = 0, uTruth = 0xFFFF & pCut->uTruth;
int i, k, nLeaves;
assert( pCut->fUsed );
- assert( pCut->nLeaves > 0 );
// compute the truth support of the cut's function
nLeaves = pCut->nLeaves;
for ( i = 0; i < (int)pCut->nLeaves; i++ )
@@ -566,6 +578,28 @@ Dar_Cut_t * Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
+void Dar_ManCutsStart( Dar_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Aig_ManCleanData( p->pAig );
+ Aig_MmFixedRestart( p->pMemCuts );
+ Dar_ObjPrepareCuts( p, Aig_ManConst1(p->pAig) );
+ Aig_ManForEachPi( p->pAig, pObj, i )
+ Dar_ObjPrepareCuts( p, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
@@ -612,10 +646,6 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
// minimize support of the cut
if ( Dar_CutSuppMinimize( pCut ) )
{
- // if a simple cut is found return immediately
- if ( pCut->nLeaves < 2 )
- return pCutSet;
- // otherwise, filter the cuts again
RetValue = Dar_CutFilter( pObj, pCut );
assert( !RetValue );
}
@@ -628,6 +658,8 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
p->nCutsSkipped++;
pCut->fUsed = 0;
}
+ else if ( pCut->nLeaves < 2 )
+ return pCutSet;
}
// count the number of nontrivial cuts cuts
Dar_ObjForEachCut( pObj, pCut, i )
diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h
index 0eb8f9fe..f496a73f 100644
--- a/src/aig/dar/darInt.h
+++ b/src/aig/dar/darInt.h
@@ -101,7 +101,7 @@ struct Dar_Man_t_
};
static inline Dar_Cut_t * Dar_ObjCuts( Aig_Obj_t * pObj ) { return pObj->pData; }
-static inline void Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts ) { pObj->pData = pCuts; }
+static inline void Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts ) { assert( !Aig_ObjIsNone(pObj) ); pObj->pData = pCuts; }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
@@ -126,22 +126,24 @@ static inline void Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts )
/*=== darBalance.c ========================================================*/
extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
-/*=== darCore.c ========================================================*/
-/*=== darCut.c ========================================================*/
-extern Dar_Cut_t * Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
+/*=== darCore.c ===========================================================*/
+/*=== darCut.c ============================================================*/
+extern void Dar_ManCutsStart( Dar_Man_t * p );
extern void Dar_ManCutsFree( Dar_Man_t * p );
extern Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj );
extern Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
-/*=== darData.c ========================================================*/
+/*=== darData.c ===========================================================*/
extern Vec_Int_t * Dar_LibReadNodes();
extern Vec_Int_t * Dar_LibReadOuts();
extern Vec_Int_t * Dar_LibReadPrios();
-/*=== darLib.c ==========================================================*/
+/*=== darLib.c ============================================================*/
extern void Dar_LibStart();
extern void Dar_LibStop();
+extern void Dar_LibPrepare( int nSubgraphs );
+extern void Dar_LibReturnCanonicals( unsigned * pCanons );
extern void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
extern Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p );
-/*=== darMan.c ==========================================================*/
+/*=== darMan.c ============================================================*/
extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars );
extern void Dar_ManStop( Dar_Man_t * p );
extern void Dar_ManPrintStats( Dar_Man_t * p );
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index fce6155b..c3d57b52 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -44,7 +44,7 @@ struct Dar_LibDat_t_ // library object data
Aig_Obj_t * pFunc; // the corresponding AIG node if it exists
int Level; // level of this node after it is constructured
int TravId; // traversal ID of the library object data
- unsigned char Area; // area of the node
+ unsigned char fMffc; // set to one if node is part of MFFC
unsigned char nLats[3]; // the number of latches on the input/output stem
};
@@ -54,9 +54,6 @@ struct Dar_Lib_t_ // library
Dar_LibObj_t * pObjs; // the set of library objects
int nObjs; // the number of objects used
int iObj; // the current object
- // object data
- Dar_LibDat_t * pDatas;
- int nDatas;
// structures by class
int nSubgr[222]; // the number of subgraphs by class
int * pSubgr[222]; // the subgraphs for each class
@@ -75,8 +72,24 @@ struct Dar_Lib_t_ // library
int nNodes[222]; // the number of nodes by class
int * pNodes[222]; // the nodes for each class
int * pNodesMem; // memory for nodes pointers
- int pNodesTotal; // the total number of nodes
- // information by NPN classes
+ int nNodesTotal; // the total number of nodes
+ // prepared library
+ int nSubgraphs;
+ int nNodes0Max;
+ // nodes by class
+ int nNodes0[222]; // the number of nodes by class
+ int * pNodes0[222]; // the nodes for each class
+ int * pNodes0Mem; // memory for nodes pointers
+ int nNodes0Total; // the total number of nodes
+ // structures by class
+ int nSubgr0[222]; // the number of subgraphs by class
+ int * pSubgr0[222]; // the subgraphs for each class
+ int * pSubgr0Mem; // memory for subgraph pointers
+ int nSubgr0Total; // the total number of subgraph
+ // object data
+ Dar_LibDat_t * pDatas;
+ int nDatas;
+ // information about NPN classes
char ** pPerms4;
unsigned short * puCanons;
char * pPhases;
@@ -104,7 +117,7 @@ static inline int Dar_LibObjTruth( Dar_LibObj_t * pObj ) { return pOb
SeeAlso []
***********************************************************************/
-Dar_Lib_t * Dar_LibAlloc( int nObjs, int nDatas )
+Dar_Lib_t * Dar_LibAlloc( int nObjs )
{
unsigned uTruths[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
Dar_Lib_t * p;
@@ -115,10 +128,6 @@ Dar_Lib_t * Dar_LibAlloc( int nObjs, int nDatas )
p->nObjs = nObjs;
p->pObjs = ALLOC( Dar_LibObj_t, nObjs );
memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs );
- // allocate datas
- p->nDatas = nDatas;
- p->pDatas = ALLOC( Dar_LibDat_t, nDatas );
- memset( p->pObjs, 0, sizeof(Dar_LibDat_t) * nDatas );
// allocate canonical data
p->pPerms4 = Extra_Permutations( 4 );
Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
@@ -149,7 +158,9 @@ void Dar_LibFree( Dar_Lib_t * p )
free( p->pObjs );
free( p->pDatas );
free( p->pNodesMem );
+ free( p->pNodes0Mem );
free( p->pSubgrMem );
+ free( p->pSubgr0Mem );
free( p->pPriosMem );
FREE( p->pPlaceMem );
FREE( p->pScoreMem );
@@ -163,6 +174,31 @@ void Dar_LibFree( Dar_Lib_t * p )
/**Function*************************************************************
+ Synopsis [Returns canonical truth tables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_LibReturnCanonicals( unsigned * pCanons )
+{
+ int Visits[222] = {0};
+ int i, k;
+ // find canonical truth tables
+ for ( i = k = 0; i < (1<<16); i++ )
+ if ( !Visits[s_DarLib->pMap[i]] )
+ {
+ Visits[s_DarLib->pMap[i]] = 1;
+ pCanons[k++] = ((i<<16) | i);
+ }
+ assert( k == 222 );
+}
+
+/**Function*************************************************************
+
Synopsis [Adds one AND to the library.]
Description []
@@ -196,14 +232,14 @@ void Dar_LibAddNode( Dar_Lib_t * p, int Id0, int Id1, int fCompl0, int fCompl1 )
SeeAlso []
***********************************************************************/
-void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class )
+void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect )
{
if ( pObj->fTerm || (int)pObj->Num == Class )
return;
pObj->Num = Class;
- Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class );
- Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class );
- if ( p->pNodesMem )
+ Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect );
+ Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect );
+ if ( fCollect )
p->pNodes[Class][ p->nNodes[Class]++ ] = pObj-p->pObjs;
else
p->nNodes[Class]++;
@@ -239,10 +275,12 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
}
// allocate memory for the roots of each class
p->pSubgrMem = ALLOC( int, Vec_IntSize(vOuts) );
+ p->pSubgr0Mem = ALLOC( int, Vec_IntSize(vOuts) );
p->nSubgrTotal = 0;
for ( i = 0; i < 222; i++ )
{
p->pSubgr[i] = p->pSubgrMem + p->nSubgrTotal;
+ p->pSubgr0[i] = p->pSubgr0Mem + p->nSubgrTotal;
p->nSubgrTotal += p->nSubgr[i];
p->nSubgr[i] = 0;
}
@@ -321,18 +359,20 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
// count nodes in each class
for ( i = 0; i < 222; i++ )
for ( k = 0; k < p->nSubgr[i]; k++ )
- Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i );
+ Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 0 );
// count the total number of nodes
- p->pNodesTotal = 0;
+ p->nNodesTotal = 0;
for ( i = 0; i < 222; i++ )
- p->pNodesTotal += p->nNodes[i];
+ p->nNodesTotal += p->nNodes[i];
// allocate memory for the nodes of each class
- p->pNodesMem = ALLOC( int, p->pNodesTotal );
- p->pNodesTotal = 0;
+ p->pNodesMem = ALLOC( int, p->nNodesTotal );
+ p->pNodes0Mem = ALLOC( int, p->nNodesTotal );
+ p->nNodesTotal = 0;
for ( i = 0; i < 222; i++ )
{
- p->pNodes[i] = p->pNodesMem + p->pNodesTotal;
- p->pNodesTotal += p->nNodes[i];
+ p->pNodes[i] = p->pNodesMem + p->nNodesTotal;
+ p->pNodes0[i] = p->pNodes0Mem + p->nNodesTotal;
+ p->nNodesTotal += p->nNodes[i];
p->nNodes[i] = 0;
}
// create traversal IDs
@@ -343,11 +383,11 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
for ( i = 0; i < 222; i++ )
{
for ( k = 0; k < p->nSubgr[i]; k++ )
- Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i );
+ Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 1 );
nNodesTotal += p->nNodes[i];
//printf( "Class %3d : Subgraphs = %4d. Nodes = %5d.\n", i, p->nSubgr[i], p->nNodes[i] );
}
- assert( nNodesTotal == p->pNodesTotal );
+ assert( nNodesTotal == p->nNodesTotal );
// prepare the number of the PI nodes
for ( i = 0; i < 4; i++ )
Dar_LibObj(p, i)->Num = i;
@@ -355,6 +395,133 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
/**Function*************************************************************
+ Synopsis [Starts the library.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_LibCreateData( Dar_Lib_t * p, int nDatas )
+{
+ if ( p->nDatas == nDatas )
+ return;
+ FREE( p->pDatas );
+ // allocate datas
+ p->nDatas = nDatas;
+ p->pDatas = ALLOC( Dar_LibDat_t, nDatas );
+ memset( p->pDatas, 0, sizeof(Dar_LibDat_t) * nDatas );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one AND to the library.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_LibSetup0_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect )
+{
+ if ( pObj->fTerm || (int)pObj->Num == Class )
+ return;
+ pObj->Num = Class;
+ Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect );
+ Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect );
+ if ( fCollect )
+ p->pNodes0[Class][ p->nNodes0[Class]++ ] = pObj-p->pObjs;
+ else
+ p->nNodes0[Class]++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the library.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_LibPrepare( int nSubgraphs )
+{
+ Dar_Lib_t * p = s_DarLib;
+ int i, k, nNodes0Total;
+ if ( p->nSubgraphs == nSubgraphs )
+ return;
+
+ // favor special classes:
+ // 1 : F = (!d*!c*!b*!a)
+ // 4 : F = (!d*!c*!(b*a))
+ // 12 : F = (!d*!(c*!(!b*!a)))
+ // 20 : F = (!d*!(c*b*a))
+
+ // set the subgraph counters
+ p->nSubgr0Total = 0;
+ for ( i = 0; i < 222; i++ )
+ {
+// if ( i == 1 || i == 4 || i == 12 || i == 20 ) // special classes
+ if ( i == 1 ) // special classes
+ p->nSubgr0[i] = p->nSubgr[i];
+ else
+ p->nSubgr0[i] = AIG_MIN( p->nSubgr[i], nSubgraphs );
+ p->nSubgr0Total += p->nSubgr0[i];
+ for ( k = 0; k < p->nSubgr0[i]; k++ )
+ p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ];
+ }
+
+ // count the number of nodes
+ // clean node counters
+ for ( i = 0; i < 222; i++ )
+ p->nNodes0[i] = 0;
+ // create traversal IDs
+ for ( i = 0; i < p->iObj; i++ )
+ Dar_LibObj(p, i)->Num = 0xff;
+ // count nodes in each class
+ // count the total number of nodes and the largest class
+ p->nNodes0Total = 0;
+ p->nNodes0Max = 0;
+ for ( i = 0; i < 222; i++ )
+ {
+ for ( k = 0; k < p->nSubgr0[i]; k++ )
+ Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 );
+ p->nNodes0Total += p->nNodes0[i];
+ p->nNodes0Max = AIG_MAX( p->nNodes0Max, p->nNodes0[i] );
+ }
+
+ // clean node counters
+ for ( i = 0; i < 222; i++ )
+ p->nNodes0[i] = 0;
+ // create traversal IDs
+ for ( i = 0; i < p->iObj; i++ )
+ Dar_LibObj(p, i)->Num = 0xff;
+ // add the nodes to storage
+ nNodes0Total = 0;
+ for ( i = 0; i < 222; i++ )
+ {
+ for ( k = 0; k < p->nSubgr0[i]; k++ )
+ Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 1 );
+ nNodes0Total += p->nNodes0[i];
+ }
+ assert( nNodes0Total == p->nNodes0Total );
+ // prepare the number of the PI nodes
+ for ( i = 0; i < 4; i++ )
+ Dar_LibObj(p, i)->Num = i;
+
+ // realloc the datas
+ Dar_LibCreateData( p, p->nNodes0Max + 32 );
+ // allocated more because Dar_LibBuildBest() sometimes requires more entries
+}
+
+/**Function*************************************************************
+
Synopsis [Reads library from array.]
Description []
@@ -374,7 +541,7 @@ Dar_Lib_t * Dar_LibRead()
vOuts = Dar_LibReadOuts();
vPrios = Dar_LibReadPrios();
// create library
- p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4, 6000 );
+ p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4 );
// create nodes
for ( i = 0; i < vObjs->nSize; i += 2 )
Dar_LibAddNode( p, vObjs->pArray[i] >> 1, vObjs->pArray[i+1] >> 1,
@@ -383,6 +550,7 @@ Dar_Lib_t * Dar_LibRead()
Dar_LibSetup( p, vOuts, vPrios );
Vec_IntFree( vObjs );
Vec_IntFree( vOuts );
+ Vec_IntFree( vPrios );
return p;
}
@@ -670,15 +838,20 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
Dar_LibDat_t * pData, * pData0, * pData1;
Aig_Obj_t * pGhost, * pFanin0, * pFanin1;
int i;
- for ( i = 0; i < s_DarLib->nNodes[Class]; i++ )
+ for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ )
{
// get one class node, assign its temporary number and set its data
- pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes[Class][i]);
+ pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes0[Class][i]);
pObj->Num = 4 + i;
+ assert( (int)pObj->Num < s_DarLib->nNodes0Max + 4 );
pData = s_DarLib->pDatas + pObj->Num;
+ pData->fMffc = 0;
pData->pFunc = NULL;
pData->TravId = 0xFFFF;
+
// explore the fanins
+ assert( (int)Dar_LibObj(s_DarLib, pObj->Fan0)->Num < s_DarLib->nNodes0Max + 4 );
+ assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 );
pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num;
pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num;
pData->Level = 1 + AIG_MAX(pData0->Level, pData1->Level);
@@ -704,9 +877,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
// clear the node if it is part of MFFC
if ( pData->pFunc != NULL && Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc) )
- pData->pFunc = NULL;
-//if ( Class == 7 )
-//printf( "Evaling node %d at data %d\n", pData->pFunc? pData->pFunc->Id : -1, pObj->Num );
+ pData->fMffc = 1;
}
}
@@ -729,20 +900,22 @@ int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required
return 0;
assert( pObj->Num > 3 );
pData = s_DarLib->pDatas + pObj->Num;
- if ( pData->pFunc )
+ if ( pData->pFunc && !pData->fMffc )
return 0;
if ( pData->Level > Required )
return 0xff;
if ( pData->TravId == Out )
- return pData->Area;
+ return 0;
pData->TravId = Out;
- Area = 1 + Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required );
+ // this is a new node - get a bound on the area of its branches
+ nNodesSaved--;
+ Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1 );
if ( Area > nNodesSaved )
- return pData->Area = 0xff;
- Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required );
+ return 0xff;
+ Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required+1 );
if ( Area > nNodesSaved )
- return pData->Area = 0xff;
- return pData->Area = Area;
+ return 0xff;
+ return Area + 1;
}
/**Function*************************************************************
@@ -773,25 +946,27 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
Class = s_DarLib->pMap[pCut->uTruth];
Dar_LibEvalAssignNums( p, Class );
// profile outputs by their savings
- p->nTotalSubgs += s_DarLib->nSubgr[Class];
- p->ClassSubgs[Class] += s_DarLib->nSubgr[Class];
- for ( Out = 0; Out < s_DarLib->nSubgr[Class]; Out++ )
+ p->nTotalSubgs += s_DarLib->nSubgr0[Class];
+ p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class];
+ for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ )
{
- pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr[Class][Out]);
- nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved, Required );
+ pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]);
+ if ( Aig_Regular(s_DarLib->pDatas[pObj->Num].pFunc) == pRoot )
+ continue;
+ nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required );
nNodesGained = nNodesSaved - nNodesAdded;
if ( fTraining && nNodesGained >= 0 )
Dar_LibIncrementScore( Class, Out, nNodesGained + 1 );
- if ( nNodesGained <= 0 )
+ if ( nNodesGained < 0 || (nNodesGained == 0 && !p->pPars->fUseZeros) )
continue;
- if ( nNodesGained < p->GainBest ||
- (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->GainBest) )
+ if ( nNodesGained < p->GainBest ||
+ (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->LevelBest) )
continue;
// remember this possibility
Vec_PtrClear( p->vLeavesBest );
for ( k = 0; k < (int)pCut->nLeaves; k++ )
Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc );
- p->OutBest = s_DarLib->pSubgr[Class][Out];
+ p->OutBest = s_DarLib->pSubgr0[Class][Out];
p->OutNumBest = Out;
p->LevelBest = s_DarLib->pDatas[pObj->Num].Level;
p->GainBest = nNodesGained;
@@ -845,7 +1020,6 @@ Aig_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj )
pFanin0 = Aig_NotCond( pFanin0, pObj->fCompl0 );
pFanin1 = Aig_NotCond( pFanin1, pObj->fCompl1 );
pData->pFunc = Aig_And( p->pAig, pFanin0, pFanin1 );
-//printf( "Adding node %d for data %d\n", pData->pFunc->Id, pObj->Num );
return pData->pFunc;
}
diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c
index a209503a..8b7c5afb 100644
--- a/src/aig/dar/darMan.c
+++ b/src/aig/dar/darMan.c
@@ -48,7 +48,7 @@ Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars )
p->pPars = pPars;
p->pAig = pAig;
// prepare the internal memory manager
- p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 512 );
+ p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 1024 );
// other data
p->vLeavesBest = Vec_PtrAlloc( 4 );
return p;
@@ -89,18 +89,27 @@ void Dar_ManStop( Dar_Man_t * p )
***********************************************************************/
void Dar_ManPrintStats( Dar_Man_t * p )
{
- int i, Gain;
+ unsigned pCanons[222];
+ int Gain, i;
+ extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
+
Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%). Cut mem = %d Mb\n",
p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit, p->nCutMemUsed );
printf( "Cuts = %8d. Tried = %8d. Used = %8d. Bad = %5d. Skipped = %5d. Ave = %.2f.\n",
p->nCutsAll, p->nCutsTried, p->nCutsUsed, p->nCutsBad, p->nCutsSkipped,
(float)p->nCutsUsed/Aig_ManNodeNum(p->pAig) );
+
+ printf( "Bufs = %5d. BufMax = %5d. BufReplace = %6d. BufFix = %6d.\n",
+ Aig_ManBufNum(p->pAig), p->pAig->nBufMax, p->pAig->nBufReplaces, p->pAig->nBufFixes );
PRT( "Cuts ", p->timeCuts );
PRT( "Eval ", p->timeEval );
PRT( "Other ", p->timeOther );
PRT( "TOTAL ", p->timeTotal );
-/*
+
+ if ( !p->pPars->fVeryVerbose )
+ return;
+ Dar_LibReturnCanonicals( pCanons );
for ( i = 0; i < 222; i++ )
{
if ( p->ClassGains[i] == 0 && p->ClassTimes[i] == 0 )
@@ -108,10 +117,10 @@ void Dar_ManPrintStats( Dar_Man_t * p )
printf( "%3d : ", i );
printf( "G = %6d (%5.2f %%) ", p->ClassGains[i], Gain? 100.0*p->ClassGains[i]/Gain : 0.0 );
printf( "S = %8d (%5.2f %%) ", p->ClassSubgs[i], p->nTotalSubgs? 100.0*p->ClassSubgs[i]/p->nTotalSubgs : 0.0 );
- printf( "R = %7d ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 );
- PRTP( "T", p->ClassTimes[i], p->timeEval );
+ printf( "R = %7d ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 );
+ Kit_DsdPrintFromTruth( pCanons + i, 4 );
+// PRTP( "T", p->ClassTimes[i], p->timeEval );
}
-*/
}
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
new file mode 100644
index 00000000..1bcc0466
--- /dev/null
+++ b/src/aig/dar/darRefact.c
@@ -0,0 +1,48 @@
+/**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 $]
+
+***********************************************************************/
+
+#include "darInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/darResub.c b/src/aig/dar/darResub.c
new file mode 100644
index 00000000..f819934e
--- /dev/null
+++ b/src/aig/dar/darResub.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+ FileName [darResub.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: darResub.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "darInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
new file mode 100644
index 00000000..c98a263e
--- /dev/null
+++ b/src/aig/dar/darScript.c
@@ -0,0 +1,48 @@
+/**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 $]
+
+***********************************************************************/
+
+#include "darInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/dar_.c b/src/aig/dar/dar_.c
index 08bd8c3e..12fd7d17 100644
--- a/src/aig/dar/dar_.c
+++ b/src/aig/dar/dar_.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "dar.h"
+#include "darInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/aig/dar/module.make b/src/aig/dar/module.make
index bcf9a2e6..09b45171 100644
--- a/src/aig/dar/module.make
+++ b/src/aig/dar/module.make
@@ -4,4 +4,7 @@ SRC += src/aig/dar/darBalance.c \
src/aig/dar/darData.c \
src/aig/dar/darLib.c \
src/aig/dar/darMan.c \
+ src/aig/dar/darRefact.c \
+ src/aig/dar/darResub.c \
+ src/aig/dar/darScript.c \
src/aig/dar/darTruth.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 09:21:49 +0000