ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
darCore.c File Reference
#include "darInt.h"
Include dependency graph for darCore.c:

Go to the source code of this file.

Macros

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

Functions

void Dar_ManDefaultRwrParams (Dar_RwrPar_t *pPars)
 FUNCTION DEFINITIONS ///.
 
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

◆ Aig_ManForEachNodeInOrder

#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] )
Cube * p
Definition exorList.c:222
#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.

31#define Aig_ManForEachNodeInOrder( p, pObj ) \
32 for ( assert(p->pOrderData), p->iPrev = 0, p->iNext = p->pOrderData[1]; \
33 p->iNext && (((pObj) = Aig_ManObj(p, p->iNext)), 1); \
34 p->iNext = p->pOrderData[2*p->iPrev+1] )

◆ MAX_VAL

#define MAX_VAL   10

Definition at line 66 of file darCore.c.

Function Documentation

◆ Dar_ManComputeCuts()

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 291 of file darCore.c.

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

◆ Dar_ManCutCount()

int Dar_ManCutCount ( Aig_Man_t * pAig,
int * pnCutsK )

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

Synopsis [Computes the total number of cuts.]

Description []

SideEffects []

SeeAlso []

Definition at line 263 of file darCore.c.

264{
265 Dar_Cut_t * pCut;
266 Aig_Obj_t * pObj;
267 int i, k, nCuts = 0, nCutsK = 0;
268 Aig_ManForEachNode( pAig, pObj, i )
269 Dar_ObjForEachCut( pObj, pCut, k )
270 {
271 nCuts++;
272 if ( pCut->nLeaves == 4 )
273 nCutsK++;
274 }
275 if ( pnCutsK )
276 *pnCutsK = nCutsK;
277 return nCuts;
278}
#define Dar_ObjForEachCut(pObj, pCut, i)
Definition darInt.h:121
unsigned nLeaves
Definition darInt.h:62
Here is the caller graph for this function:

◆ Dar_ManDefaultRwrParams()

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->nMinSaved = 1;
57 pPars->fFanout = 1;
58 pPars->fUpdateLevel = 0;
59 pPars->fUseZeros = 0;
60 pPars->fPower = 0;
61 pPars->fRecycle = 1;
62 pPars->fVerbose = 0;
63 pPars->fVeryVerbose = 0;
64}
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_ManRewrite()

int Dar_ManRewrite ( Aig_Man_t * pAig,
Dar_RwrPar_t * pPars )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file darCore.c.

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