abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
darCore.c File Reference
#include "darInt.h"

Go to the source code of this file.

Macros

#define Aig_ManForEachNodeInOrder(p, pObj)
 DECLARATIONS ///. More...
 
#define MAX_VAL   10
 

Functions

void Dar_ManDefaultRwrParams (Dar_RwrPar_t *pPars)
 FUNCTION DEFINITIONS ///. More...
 
int Dar_ManRewrite (Aig_Man_t *pAig, Dar_RwrPar_t *pPars)
 
int Dar_ManCutCount (Aig_Man_t *pAig, int *pnCutsK)
 
Aig_MmFixed_tDar_ManComputeCuts (Aig_Man_t *pAig, int nCutsMax, int fSkipTtMin, int fVerbose)
 

Macro Definition Documentation

#define Aig_ManForEachNodeInOrder (   p,
  pObj 
)
Value:
for ( assert(p->pOrderData), p->iPrev = 0, p->iNext = p->pOrderData[1]; \
p->iNext && (((pObj) = Aig_ManObj(p, p->iNext)), 1); \
p->iNext = p->pOrderData[2*p->iPrev+1] )
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
#define assert(ex)
Definition: util_old.h:213

DECLARATIONS ///.

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

FileName [darCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [Core of the rewriting package.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 31 of file darCore.c.

#define MAX_VAL   10

Definition at line 65 of file darCore.c.

Function Documentation

Aig_MmFixed_t* Dar_ManComputeCuts ( Aig_Man_t pAig,
int  nCutsMax,
int  fSkipTtMin,
int  fVerbose 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 287 of file darCore.c.

288 {
289  Dar_Man_t * p;
290  Dar_RwrPar_t Pars, * pPars = &Pars;
291  Aig_Obj_t * pObj;
292  Aig_MmFixed_t * pMemCuts;
293  int i, nNodes;
294  abctime clk = Abc_Clock();
295  // remove dangling nodes
296  if ( (nNodes = Aig_ManCleanup( pAig )) )
297  {
298 // printf( "Removing %d nodes.\n", nNodes );
299  }
300  // create default parameters
301  Dar_ManDefaultRwrParams( pPars );
302  pPars->nCutsMax = nCutsMax;
303  // create rewriting manager
304  p = Dar_ManStart( pAig, pPars );
305  // set elementary cuts for the PIs
306 // Dar_ManCutsStart( p );
307  Aig_MmFixedRestart( p->pMemCuts );
308  Dar_ObjPrepareCuts( p, Aig_ManConst1(p->pAig) );
309  Aig_ManForEachCi( pAig, pObj, i )
310  Dar_ObjPrepareCuts( p, pObj );
311  // compute cuts for each nodes in the topological order
312  Aig_ManForEachNode( pAig, pObj, i )
313  Dar_ObjComputeCuts( p, pObj, fSkipTtMin );
314  // print verbose stats
315  if ( fVerbose )
316  {
317 // Aig_Obj_t * pObj;
318  int nCuts, nCutsK;//, i;
319  nCuts = Dar_ManCutCount( pAig, &nCutsK );
320  printf( "Nodes = %6d. Total cuts = %6d. 4-input cuts = %6d.\n",
321  Aig_ManObjNum(pAig), nCuts, nCutsK );
322  printf( "Cut size = %2d. Truth size = %2d. Total mem = %5.2f MB ",
323  (int)sizeof(Dar_Cut_t), (int)4, 1.0*Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) );
324  ABC_PRT( "Runtime", Abc_Clock() - clk );
325 /*
326  Aig_ManForEachNode( pAig, pObj, i )
327  if ( i % 300 == 0 )
328  Dar_ObjCutPrint( pAig, pObj );
329 */
330  }
331  // free the cuts
332  pMemCuts = p->pMemCuts;
333  p->pMemCuts = NULL;
334 // Dar_ManCutsFree( p );
335  // stop the rewriting manager
336  Dar_ManStop( p );
337  return pMemCuts;
338 }
void Dar_ManStop(Dar_Man_t *p)
Definition: darMan.c:69
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Aig_ManObjNum(Aig_Man_t *p)
Definition: aig.h:258
Dar_Cut_t * Dar_ObjComputeCuts(Dar_Man_t *p, Aig_Obj_t *pObj, int fSkipTtMin)
Definition: darCut.c:738
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
int Dar_ManCutCount(Aig_Man_t *pAig, int *pnCutsK)
Definition: darCore.c:259
static abctime Abc_Clock()
Definition: abc_global.h:279
DECLARATIONS ///.
Definition: aigMem.c:30
typedefABC_NAMESPACE_HEADER_START struct Dar_Man_t_ Dar_Man_t
INCLUDES ///.
Definition: darInt.h:51
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Dar_Man_t * Dar_ManStart(Aig_Man_t *pAig, Dar_RwrPar_t *pPars)
DECLARATIONS ///.
Definition: darMan.c:44
int Aig_MmFixedReadMemUsage(Aig_MmFixed_t *p)
Definition: aigMem.c:271
#define ABC_PRT(a, t)
Definition: abc_global.h:220
typedefABC_NAMESPACE_HEADER_START struct Dar_RwrPar_t_ Dar_RwrPar_t
INCLUDES ///.
Definition: dar.h:42
void Aig_MmFixedRestart(Aig_MmFixed_t *p)
Definition: aigMem.c:232
void Dar_ManDefaultRwrParams(Dar_RwrPar_t *pPars)
FUNCTION DEFINITIONS ///.
Definition: darCore.c:51
Dar_Cut_t * Dar_ObjPrepareCuts(Dar_Man_t *p, Aig_Obj_t *pObj)
Definition: darCut.c:668
ABC_INT64_T abctime
Definition: abc_global.h:278
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
int Dar_ManCutCount ( Aig_Man_t pAig,
int *  pnCutsK 
)

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

Synopsis [Computes the total number of cuts.]

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file darCore.c.

260 {
261  Dar_Cut_t * pCut;
262  Aig_Obj_t * pObj;
263  int i, k, nCuts = 0, nCutsK = 0;
264  Aig_ManForEachNode( pAig, pObj, i )
265  Dar_ObjForEachCut( pObj, pCut, k )
266  {
267  nCuts++;
268  if ( pCut->nLeaves == 4 )
269  nCutsK++;
270  }
271  if ( pnCutsK )
272  *pnCutsK = nCutsK;
273  return nCuts;
274 }
#define Dar_ObjForEachCut(pObj, pCut, i)
Definition: darInt.h:121
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Definition: aig.h:69
void Dar_ManDefaultRwrParams ( Dar_RwrPar_t pPars)

FUNCTION DEFINITIONS ///.

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file darCore.c.

52 {
53  memset( pPars, 0, sizeof(Dar_RwrPar_t) );
54  pPars->nCutsMax = 8; // 8
55  pPars->nSubgMax = 5; // 5 is a "magic number"
56  pPars->fFanout = 1;
57  pPars->fUpdateLevel = 0;
58  pPars->fUseZeros = 0;
59  pPars->fPower = 0;
60  pPars->fRecycle = 1;
61  pPars->fVerbose = 0;
62  pPars->fVeryVerbose = 0;
63 }
char * memset()
typedefABC_NAMESPACE_HEADER_START struct Dar_RwrPar_t_ Dar_RwrPar_t
INCLUDES ///.
Definition: dar.h:42
int Dar_ManRewrite ( Aig_Man_t pAig,
Dar_RwrPar_t pPars 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file darCore.c.

79 {
80  extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
81  Dar_Man_t * p;
82 // Bar_Progress_t * pProgress;
83  Dar_Cut_t * pCut;
84  Aig_Obj_t * pObj, * pObjNew;
85  int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
86  abctime clk = 0, clkStart;
87  int Counter = 0;
88  int nMffcSize;//, nMffcGains[MAX_VAL+1][MAX_VAL+1] = {{0}};
89  // prepare the library
90  Dar_LibPrepare( pPars->nSubgMax );
91  // create rewriting manager
92  p = Dar_ManStart( pAig, pPars );
93  if ( pPars->fPower )
94  pAig->vProbs = Saig_ManComputeSwitchProbs( pAig, 48, 16, 1 );
95  // remove dangling nodes
96  Aig_ManCleanup( pAig );
97  // if updating levels is requested, start fanout and timing
98  if ( p->pPars->fFanout )
99  Aig_ManFanoutStart( pAig );
100  if ( p->pPars->fUpdateLevel )
101  Aig_ManStartReverseLevels( pAig, 0 );
102  // set elementary cuts for the PIs
103 // Dar_ManCutsStart( p );
104  // resynthesize each node once
105  clkStart = Abc_Clock();
106  p->nNodesInit = Aig_ManNodeNum(pAig);
107  nNodesOld = Vec_PtrSize( pAig->vObjs );
108 
109 // pProgress = Bar_ProgressStart( stdout, nNodesOld );
110  Aig_ManForEachObj( pAig, pObj, i )
111 // pProgress = Bar_ProgressStart( stdout, 100 );
112 // Aig_ManOrderStart( pAig );
113 // Aig_ManForEachNodeInOrder( pAig, pObj )
114  {
115  if ( pAig->Time2Quit && !(i & 256) && Abc_Clock() > pAig->Time2Quit )
116  break;
117 // Bar_ProgressUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL );
118 // Bar_ProgressUpdate( pProgress, i, NULL );
119  if ( !Aig_ObjIsNode(pObj) )
120  continue;
121  if ( i > nNodesOld )
122 // if ( p->pPars->fUseZeros && i > nNodesOld )
123  break;
124  if ( pPars->fRecycle && ++Counter % 50000 == 0 && Aig_DagSize(pObj) < Vec_PtrSize(p->vCutNodes)/100 )
125  {
126 // printf( "Counter = %7d. Node = %7d. Dag = %5d. Vec = %5d.\n",
127 // Counter, i, Aig_DagSize(pObj), Vec_PtrSize(p->vCutNodes) );
128 // fflush( stdout );
129  Dar_ManCutsRestart( p, pObj );
130  }
131 
132  // consider freeing the cuts
133 // if ( (i & 0xFFF) == 0 && Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) > 100 )
134 // Dar_ManCutsStart( p );
135 
136  // compute cuts for the node
137  p->nNodesTried++;
138 clk = Abc_Clock();
139  Dar_ObjSetCuts( pObj, NULL );
140  Dar_ObjComputeCuts_rec( p, pObj );
141 p->timeCuts += Abc_Clock() - clk;
142 
143  // check if there is a trivial cut
144  Dar_ObjForEachCut( pObj, pCut, k )
145  if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id && Aig_ManObj(p->pAig, pCut->pLeaves[0])) )
146  break;
147  if ( k < (int)pObj->nCuts )
148  {
149  assert( pCut->nLeaves < 2 );
150  if ( pCut->nLeaves == 0 ) // replace by constant
151  {
152  assert( pCut->uTruth == 0 || pCut->uTruth == 0xFFFF );
153  pObjNew = Aig_NotCond( Aig_ManConst1(p->pAig), pCut->uTruth==0 );
154  }
155  else
156  {
157  assert( pCut->uTruth == 0xAAAA || pCut->uTruth == 0x5555 );
158  pObjNew = Aig_NotCond( Aig_ManObj(p->pAig, pCut->pLeaves[0]), pCut->uTruth==0x5555 );
159  }
160  // remove the old cuts
161  Dar_ObjSetCuts( pObj, NULL );
162  // replace the node
163  Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
164  continue;
165  }
166 
167  // evaluate the cuts
168  p->GainBest = -1;
169  nMffcSize = -1;
170  Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY;
171  Dar_ObjForEachCut( pObj, pCut, k )
172  {
173  int nLeavesOld = pCut->nLeaves;
174  if ( pCut->nLeaves == 3 )
175  pCut->pLeaves[pCut->nLeaves++] = 0;
176  Dar_LibEval( p, pObj, pCut, Required, &nMffcSize );
177  pCut->nLeaves = nLeavesOld;
178  }
179  // check the best gain
180  if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
181  {
182 // Aig_ObjOrderAdvance( pAig );
183  continue;
184  }
185 // nMffcGains[p->GainBest < MAX_VAL ? p->GainBest : MAX_VAL][nMffcSize < MAX_VAL ? nMffcSize : MAX_VAL]++;
186  // remove the old cuts
187  Dar_ObjSetCuts( pObj, NULL );
188  // if we end up here, a rewriting step is accepted
189  nNodeBefore = Aig_ManNodeNum( pAig );
190  pObjNew = Dar_LibBuildBest( p ); // pObjNew can be complemented!
191  pObjNew = Aig_NotCond( pObjNew, Aig_ObjPhaseReal(pObjNew) ^ pObj->fPhase );
192  assert( (int)Aig_Regular(pObjNew)->Level <= Required );
193  // replace the node
194  Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
195  // compare the gains
196  nNodeAfter = Aig_ManNodeNum( pAig );
197  assert( p->GainBest <= nNodeBefore - nNodeAfter );
198  // count gains of this class
199  p->ClassGains[p->ClassBest] += nNodeBefore - nNodeAfter;
200  }
201 // Aig_ManOrderStop( pAig );
202 /*
203  printf( "Distribution of gain (row) by MFFC size (column) %s 0-costs:\n", p->pPars->fUseZeros? "with":"without" );
204  for ( k = 0; k <= MAX_VAL; k++ )
205  printf( "<%4d> ", k );
206  printf( "\n" );
207  for ( i = 0; i <= MAX_VAL; i++ )
208  {
209  for ( k = 0; k <= MAX_VAL; k++ )
210  printf( "%6d ", nMffcGains[i][k] );
211  printf( "\n" );
212  }
213 */
214 
215 p->timeTotal = Abc_Clock() - clkStart;
216 p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
217 
218 // Bar_ProgressStop( pProgress );
219  Dar_ManCutsFree( p );
220  // put the nodes into the DFS order and reassign their IDs
221 // Aig_NtkReassignIds( p );
222  // fix the levels
223 // Aig_ManVerifyLevel( pAig );
224  if ( p->pPars->fFanout )
225  Aig_ManFanoutStop( pAig );
226  if ( p->pPars->fUpdateLevel )
227  {
228 // Aig_ManVerifyReverseLevel( pAig );
229  Aig_ManStopReverseLevels( pAig );
230  }
231  if ( pAig->vProbs )
232  {
233  Vec_IntFree( pAig->vProbs );
234  pAig->vProbs = NULL;
235  }
236  // stop the rewriting manager
237  Dar_ManStop( p );
238  Aig_ManCheckPhase( pAig );
239  // check
240  if ( !Aig_ManCheck( pAig ) )
241  {
242  printf( "Aig_ManRewrite: The network check has failed.\n" );
243  return 0;
244  }
245  return 1;
246 }
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition: aigCheck.c:45
void Dar_ManStop(Dar_Man_t *p)
Definition: darMan.c:69
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Aig_ManCheckPhase(Aig_Man_t *p)
Definition: aigCheck.c:151
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
unsigned uTruth
Definition: darInt.h:58
static void Dar_ObjSetCuts(Aig_Obj_t *pObj, Dar_Cut_t *pCuts)
Definition: darInt.h:108
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
int Aig_ObjRequiredLevel(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aigTiming.c:100
static abctime Abc_Clock()
Definition: abc_global.h:279
void Dar_ManCutsRestart(Dar_Man_t *p, Aig_Obj_t *pRoot)
FUNCTION DECLARATIONS ///.
Definition: darCut.c:714
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
void Aig_ManFanoutStart(Aig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: aigFanout.c:56
void Aig_ManStartReverseLevels(Aig_Man_t *p, int nMaxLevelIncrease)
Definition: aigTiming.c:142
void Aig_ManFanoutStop(Aig_Man_t *p)
Definition: aigFanout.c:89
Dar_Cut_t * Dar_ObjComputeCuts_rec(Dar_Man_t *p, Aig_Obj_t *pObj)
Definition: darCut.c:818
#define Dar_ObjForEachCut(pObj, pCut, i)
Definition: darInt.h:121
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
void Aig_ManStopReverseLevels(Aig_Man_t *p)
Definition: aigTiming.c:175
typedefABC_NAMESPACE_HEADER_START struct Dar_Man_t_ Dar_Man_t
INCLUDES ///.
Definition: darInt.h:51
int pLeaves[4]
Definition: darInt.h:63
Vec_Int_t * Saig_ManComputeSwitchProbs(Aig_Man_t *pAig, int nFrames, int nPref, int fProbOne)
Definition: giaSwitch.c:684
void Aig_ObjReplace(Aig_Man_t *p, Aig_Obj_t *pObjOld, Aig_Obj_t *pObjNew, int fUpdateLevel)
Definition: aigObj.c:467
void Dar_LibEval(Dar_Man_t *p, Aig_Obj_t *pRoot, Dar_Cut_t *pCut, int Required, int *pnMffcSize)
Definition: darLib.c:920
if(last==0)
Definition: sparse_int.h:34
static int Aig_ObjPhaseReal(Aig_Obj_t *pObj)
Definition: aig.h:299
Definition: aig.h:69
static int Counter
void Dar_ManCutsFree(Dar_Man_t *p)
Definition: darCut.c:648
unsigned nLeaves
Definition: darInt.h:62
void Dar_LibPrepare(int nSubgraphs)
Definition: darLib.c:478
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
int Aig_DagSize(Aig_Obj_t *pObj)
Definition: aigDfs.c:712
unsigned int fPhase
Definition: aig.h:78
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Dar_Man_t * Dar_ManStart(Aig_Man_t *pAig, Dar_RwrPar_t *pPars)
DECLARATIONS ///.
Definition: darMan.c:44
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
ABC_INT64_T abctime
Definition: abc_global.h:278
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Aig_Obj_t * Dar_LibBuildBest(Dar_Man_t *p)
Definition: darLib.c:1031