1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
|
/**CFile****************************************************************
FileName [dar.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware AIG rewriting.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: dar.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __DAR_H__
#define __DAR_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "vec.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Dar_Par_t_ Dar_Par_t;
typedef struct Dar_Man_t_ Dar_Man_t;
typedef struct Dar_Obj_t_ Dar_Obj_t;
typedef struct Dar_Cut_t_ Dar_Cut_t;
typedef struct Dar_Cnf_t_ Dar_Cnf_t;
typedef struct Dar_MmFixed_t_ Dar_MmFixed_t;
typedef struct Dar_MmFlex_t_ Dar_MmFlex_t;
typedef struct Dar_MmStep_t_ Dar_MmStep_t;
// the maximum number of cuts stored at a node
#define DAR_CUT_BASE 64
// object types
typedef enum {
DAR_AIG_NONE, // 0: non-existent object
DAR_AIG_CONST1, // 1: constant 1
DAR_AIG_PI, // 2: primary input
DAR_AIG_PO, // 3: primary output
DAR_AIG_BUF, // 4: buffer node
DAR_AIG_AND, // 5: AND node
DAR_AIG_EXOR, // 6: EXOR node
DAR_AIG_LATCH, // 7: latch
DAR_AIG_VOID // 8: unused object
} Dar_Type_t;
// the parameters
struct Dar_Par_t_
{
int fUpdateLevel;
int fUseZeros;
int fVerbose;
int fVeryVerbose;
};
// the AIG 4-cut
struct Dar_Cut_t_ // 8 words
{
unsigned uSign;
unsigned uTruth : 16; // the truth table of the cut function
unsigned Cost : 6; // the cost of the cut in terms of CNF clauses
unsigned FanRefs : 4; // the average number of fanin references
unsigned NoRefs : 3; // the average number of fanin references
unsigned nLeaves : 3; // the number of leaves
int pLeaves[4]; // the array of leaves
// unsigned char pIndices[4];
float Area; // the area flow or exact area of the cut
};
// the AIG node
struct Dar_Obj_t_ // 8 words
{
void * pData; // misc (cuts, copy, etc)
Dar_Obj_t * pNext; // strashing table
Dar_Obj_t * pFanin0; // fanin
Dar_Obj_t * pFanin1; // fanin
unsigned long Type : 3; // object type
unsigned long fPhase : 1; // value under 000...0 pattern
unsigned long fMarkA : 1; // multipurpose mask
unsigned long fMarkB : 1; // multipurpose mask
unsigned long nRefs : 26; // reference count
unsigned Level : 24; // the level of this node
unsigned nCuts : 8; // the number of cuts
int TravId; // unique ID of last traversal involving the node
int Id; // unique ID of the node
};
// the AIG manager
struct Dar_Man_t_
{
// parameters governing rewriting
Dar_Par_t * pPars;
// AIG nodes
Vec_Ptr_t * vPis; // the array of PIs
Vec_Ptr_t * vPos; // the array of POs
Vec_Ptr_t * vObjs; // the array of all nodes (optional)
Dar_Obj_t * pConst1; // the constant 1 node
Dar_Obj_t Ghost; // the ghost node
// AIG node counters
int nObjs[DAR_AIG_VOID];// the number of objects by type
int nCreated; // the number of created objects
int nDeleted; // the number of deleted objects
// structural hash table
Dar_Obj_t ** pTable; // structural hash table
int nTableSize; // structural hash table size
// 4-input cuts of the nodes
Dar_Cut_t * pBaseCuts[DAR_CUT_BASE];
Dar_Cut_t BaseCuts[DAR_CUT_BASE];
int nBaseCuts;
int nCutsUsed;
int nCutsFiltered;
// current rewriting step
int nNodesInit; // the original number of nodes
Vec_Ptr_t * vLeavesBest; // the best set of leaves
int OutBest; // the best output (in the library)
int GainBest; // the best gain
int LevelBest; // the level of node with the best gain
int ClassBest; // the equivalence class of the best replacement
int nTotalSubgs; // the total number of subgraphs tried
int ClassTimes[222];// the runtimes for each class
int ClassGains[222];// the gains for each class
int ClassSubgs[222];// the graphs for each class
// various data members
Dar_MmFixed_t * pMemObjs; // memory manager for objects
Dar_MmFlex_t * pMemCuts; // memory manager for cuts
Vec_Int_t * vRequired; // the required times
int nLevelMax; // maximum number of levels
void * pData; // the temporary data
int nTravIds; // the current traversal ID
int fCatchExor; // enables EXOR nodes
// CNF mapping
char * pSopSizes; // sizes of SOPs for 4-variable functions
char ** pSops; // the SOPs for 4-variable functions
int aArea; // the area of the mapping
// rewriting statistics
int nCutsBad;
int nCutsGood;
// timing statistics
int timeCuts;
int timeEval;
int timeOther;
int timeTotal;
int time1;
int time2;
};
// the CNF asserting outputs of AIG to be 1
struct Dar_Cnf_t_
{
Dar_Man_t * pMan; // the AIG manager, for which CNF is computed
int nLiterals; // the number of CNF literals
int nClauses; // the number of CNF clauses
int ** pClauses; // the CNF clauses
int * pVarNums; // the number of CNF variable for each node ID (-1 if unused)
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define DAR_MIN(a,b) (((a) < (b))? (a) : (b))
#define DAR_MAX(a,b) (((a) > (b))? (a) : (b))
#define DAR_INFINITY (100000000)
#ifndef PRT
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif
static inline int Dar_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
static inline int Dar_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline int Dar_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
static inline void Dar_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Dar_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
static inline Dar_Obj_t * Dar_Regular( Dar_Obj_t * p ) { return (Dar_Obj_t *)((unsigned long)(p) & ~01); }
static inline Dar_Obj_t * Dar_Not( Dar_Obj_t * p ) { return (Dar_Obj_t *)((unsigned long)(p) ^ 01); }
static inline Dar_Obj_t * Dar_NotCond( Dar_Obj_t * p, int c ) { return (Dar_Obj_t *)((unsigned long)(p) ^ (c)); }
static inline int Dar_IsComplement( Dar_Obj_t * p ) { return (int )(((unsigned long)p) & 01); }
static inline Dar_Obj_t * Dar_ManConst0( Dar_Man_t * p ) { return Dar_Not(p->pConst1); }
static inline Dar_Obj_t * Dar_ManConst1( Dar_Man_t * p ) { return p->pConst1; }
static inline Dar_Obj_t * Dar_ManGhost( Dar_Man_t * p ) { return &p->Ghost; }
static inline Dar_Obj_t * Dar_ManPi( Dar_Man_t * p, int i ) { return (Dar_Obj_t *)Vec_PtrEntry(p->vPis, i); }
static inline Dar_Obj_t * Dar_ManPo( Dar_Man_t * p, int i ) { return (Dar_Obj_t *)Vec_PtrEntry(p->vPos, i); }
static inline Dar_Obj_t * Dar_ManObj( Dar_Man_t * p, int i ) { return p->vObjs ? (Dar_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; }
static inline int Dar_ManPiNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_PI]; }
static inline int Dar_ManPoNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_PO]; }
static inline int Dar_ManBufNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_BUF]; }
static inline int Dar_ManAndNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]; }
static inline int Dar_ManExorNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_EXOR]; }
static inline int Dar_ManLatchNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_LATCH]; }
static inline int Dar_ManNodeNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+p->nObjs[DAR_AIG_EXOR]; }
static inline int Dar_ManGetCost( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+3*p->nObjs[DAR_AIG_EXOR]; }
static inline int Dar_ManObjNum( Dar_Man_t * p ) { return p->nCreated - p->nDeleted; }
static inline int Dar_ManObjIdMax( Dar_Man_t * p ) { return Vec_PtrSize(p->vObjs); }
static inline Dar_Type_t Dar_ObjType( Dar_Obj_t * pObj ) { return (Dar_Type_t)pObj->Type; }
static inline int Dar_ObjIsNone( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_NONE; }
static inline int Dar_ObjIsConst1( Dar_Obj_t * pObj ) { assert(!Dar_IsComplement(pObj)); return pObj->Type == DAR_AIG_CONST1; }
static inline int Dar_ObjIsPi( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_PI; }
static inline int Dar_ObjIsPo( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_PO; }
static inline int Dar_ObjIsBuf( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_BUF; }
static inline int Dar_ObjIsAnd( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND; }
static inline int Dar_ObjIsExor( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_EXOR; }
static inline int Dar_ObjIsLatch( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_LATCH; }
static inline int Dar_ObjIsNode( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR; }
static inline int Dar_ObjIsTerm( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_PI || pObj->Type == DAR_AIG_PO || pObj->Type == DAR_AIG_CONST1; }
static inline int Dar_ObjIsHash( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR || pObj->Type == DAR_AIG_LATCH; }
static inline int Dar_ObjIsMarkA( Dar_Obj_t * pObj ) { return pObj->fMarkA; }
static inline void Dar_ObjSetMarkA( Dar_Obj_t * pObj ) { pObj->fMarkA = 1; }
static inline void Dar_ObjClearMarkA( Dar_Obj_t * pObj ) { pObj->fMarkA = 0; }
static inline void Dar_ObjSetTravId( Dar_Obj_t * pObj, int TravId ) { pObj->TravId = TravId; }
static inline void Dar_ObjSetTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->TravId = p->nTravIds; }
static inline void Dar_ObjSetTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->TravId = p->nTravIds - 1; }
static inline int Dar_ObjIsTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int)(pObj->TravId == p->nTravIds); }
static inline int Dar_ObjIsTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int)(pObj->TravId == p->nTravIds - 1); }
static inline int Dar_ObjTravId( Dar_Obj_t * pObj ) { return (int)pObj->pData; }
static inline int Dar_ObjPhase( Dar_Obj_t * pObj ) { return pObj->fPhase; }
static inline int Dar_ObjRefs( Dar_Obj_t * pObj ) { return pObj->nRefs; }
static inline void Dar_ObjRef( Dar_Obj_t * pObj ) { pObj->nRefs++; }
static inline void Dar_ObjDeref( Dar_Obj_t * pObj ) { assert( pObj->nRefs > 0 ); pObj->nRefs--; }
static inline void Dar_ObjClearRef( Dar_Obj_t * pObj ) { pObj->nRefs = 0; }
static inline int Dar_ObjFaninC0( Dar_Obj_t * pObj ) { return Dar_IsComplement(pObj->pFanin0); }
static inline int Dar_ObjFaninC1( Dar_Obj_t * pObj ) { return Dar_IsComplement(pObj->pFanin1); }
static inline Dar_Obj_t * Dar_ObjFanin0( Dar_Obj_t * pObj ) { return Dar_Regular(pObj->pFanin0); }
static inline Dar_Obj_t * Dar_ObjFanin1( Dar_Obj_t * pObj ) { return Dar_Regular(pObj->pFanin1); }
static inline Dar_Obj_t * Dar_ObjChild0( Dar_Obj_t * pObj ) { return pObj->pFanin0; }
static inline Dar_Obj_t * Dar_ObjChild1( Dar_Obj_t * pObj ) { return pObj->pFanin1; }
static inline Dar_Obj_t * Dar_ObjChild0Copy( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond((Dar_Obj_t *)Dar_ObjFanin0(pObj)->pData, Dar_ObjFaninC0(pObj)) : NULL; }
static inline Dar_Obj_t * Dar_ObjChild1Copy( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond((Dar_Obj_t *)Dar_ObjFanin1(pObj)->pData, Dar_ObjFaninC1(pObj)) : NULL; }
static inline int Dar_ObjLevel( Dar_Obj_t * pObj ) { return pObj->nRefs; }
static inline int Dar_ObjLevelNew( Dar_Obj_t * pObj ) { return 1 + Dar_ObjIsExor(pObj) + DAR_MAX(Dar_ObjFanin0(pObj)->Level, Dar_ObjFanin1(pObj)->Level); }
static inline int Dar_ObjFaninPhase( Dar_Obj_t * pObj ) { return Dar_Regular(pObj)->fPhase ^ Dar_IsComplement(pObj); }
static inline void Dar_ObjClean( Dar_Obj_t * pObj ) { memset( pObj, 0, sizeof(Dar_Obj_t) ); }
static inline int Dar_ObjWhatFanin( Dar_Obj_t * pObj, Dar_Obj_t * pFanin )
{
if ( Dar_ObjFanin0(pObj) == pFanin ) return 0;
if ( Dar_ObjFanin1(pObj) == pFanin ) return 1;
assert(0); return -1;
}
static inline int Dar_ObjFanoutC( Dar_Obj_t * pObj, Dar_Obj_t * pFanout )
{
if ( Dar_ObjFanin0(pFanout) == pObj ) return Dar_ObjFaninC0(pObj);
if ( Dar_ObjFanin1(pFanout) == pObj ) return Dar_ObjFaninC1(pObj);
assert(0); return -1;
}
static inline Dar_Cut_t * Dar_ObjBestCut( Dar_Obj_t * pObj ) { return (Dar_Cut_t *)pObj->pNext; }
static inline void Dar_ObjSetBestCut( Dar_Obj_t * pObj, Dar_Cut_t * pCut ) { pObj->pNext = (Dar_Obj_t *)pCut; }
// create the ghost of the new node
static inline Dar_Obj_t * Dar_ObjCreateGhost( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t Type )
{
Dar_Obj_t * pGhost;
assert( Type != DAR_AIG_AND || !Dar_ObjIsConst1(Dar_Regular(p0)) );
assert( p1 == NULL || !Dar_ObjIsConst1(Dar_Regular(p1)) );
assert( Type == DAR_AIG_PI || Dar_Regular(p0) != Dar_Regular(p1) );
pGhost = Dar_ManGhost(p);
pGhost->Type = Type;
if ( p1 == NULL || Dar_Regular(p0)->Id < Dar_Regular(p1)->Id )
{
pGhost->pFanin0 = p0;
pGhost->pFanin1 = p1;
}
else
{
pGhost->pFanin0 = p1;
pGhost->pFanin1 = p0;
}
return pGhost;
}
// internal memory manager
static inline Dar_Obj_t * Dar_ManFetchMemory( Dar_Man_t * p )
{
extern char * Dar_MmFixedEntryFetch( Dar_MmFixed_t * p );
Dar_Obj_t * pTemp;
pTemp = (Dar_Obj_t *)Dar_MmFixedEntryFetch( p->pMemObjs );
memset( pTemp, 0, sizeof(Dar_Obj_t) );
Vec_PtrPush( p->vObjs, pTemp );
pTemp->Id = p->nCreated++;
return pTemp;
}
static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry )
{
extern void Dar_MmFixedEntryRecycle( Dar_MmFixed_t * p, char * pEntry );
assert( pEntry->nRefs == 0 );
pEntry->Type = DAR_AIG_NONE; // distinquishes a dead node from a live node
Dar_MmFixedEntryRecycle( p->pMemObjs, (char *)pEntry );
p->nDeleted++;
}
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
// iterator over the primary inputs
#define Dar_ManForEachPi( p, pObj, i ) \
Vec_PtrForEachEntry( p->vPis, pObj, i )
// iterator over the primary outputs
#define Dar_ManForEachPo( p, pObj, i ) \
Vec_PtrForEachEntry( p->vPos, pObj, i )
// iterator over all objects, including those currently not used
#define Dar_ManForEachObj( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
// iterator over all cuts of the node
#define Dar_ObjForEachCut( pObj, pCut, i ) \
for ( pCut = pObj->pData, i = 0; i < (int)pObj->nCuts; i++, pCut++ ) if ( i==0 ) {} else
// iterator over leaves of the cut
#define Dar_CutForEachLeaf( p, pCut, pLeaf, i ) \
for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = Dar_ManObj(p, (pCut)->pLeaves[i])); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== darBalance.c ========================================================*/
extern Dar_Man_t * Dar_ManBalance( Dar_Man_t * p, int fUpdateLevel );
extern Dar_Obj_t * Dar_NodeBalanceBuildSuper( Dar_Man_t * p, Vec_Ptr_t * vSuper, Dar_Type_t Type, int fUpdateLevel );
/*=== darCheck.c ========================================================*/
extern int Dar_ManCheck( Dar_Man_t * p );
/*=== darCnf.c ========================================================*/
extern Dar_Cnf_t * Dar_ManDeriveCnf( Dar_Man_t * p );
extern Dar_Cut_t * Dar_ObjFindBestCut( Dar_Obj_t * pObj );
extern void Dar_CutAssignAreaFlow( Dar_Man_t * p, Dar_Cut_t * pCut );
extern void Dar_CutAssignArea( Dar_Man_t * p, Dar_Cut_t * pCut );
extern void Dar_CnfFree( Dar_Cnf_t * pCnf );
/*=== darCore.c ========================================================*/
extern int Dar_ManRewrite( Dar_Man_t * p );
extern int Dar_ManComputeCuts( Dar_Man_t * p );
/*=== darCut.c ========================================================*/
extern void Dar_ManSetupPis( Dar_Man_t * p );
extern Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Dar_Obj_t * pObj );
extern Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Dar_Obj_t * pObj );
extern void Dar_ManCutsFree( Dar_Man_t * p );
/*=== darData.c ========================================================*/
extern Vec_Int_t * Dar_LibReadNodes();
extern Vec_Int_t * Dar_LibReadOuts();
/*=== darData2.c ========================================================*/
extern void Dar_LibReadMsops( char ** ppSopSizes, char *** ppSops );
/*=== darDfs.c ==========================================================*/
extern Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p );
extern int Dar_ManCountLevels( Dar_Man_t * p );
extern void Dar_ManCreateRefs( Dar_Man_t * p );
extern int Dar_DagSize( Dar_Obj_t * pObj );
extern void Dar_ConeUnmark_rec( Dar_Obj_t * pObj );
extern Dar_Obj_t * Dar_Transfer( Dar_Man_t * pSour, Dar_Man_t * pDest, Dar_Obj_t * pObj, int nVars );
extern Dar_Obj_t * Dar_Compose( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Obj_t * pFunc, int iVar );
/*=== darLib.c ==========================================================*/
extern void Dar_LibStart();
extern void Dar_LibStop();
extern void Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
extern Dar_Obj_t * Dar_LibBuildBest( Dar_Man_t * p );
/*=== darMan.c ==========================================================*/
extern Dar_Man_t * Dar_ManStart();
extern Dar_Man_t * Dar_ManDup( Dar_Man_t * p );
extern void Dar_ManStop( Dar_Man_t * p );
extern int Dar_ManCleanup( Dar_Man_t * p );
extern void Dar_ManPrintStats( Dar_Man_t * p );
extern void Dar_ManPrintRuntime( Dar_Man_t * p );
/*=== darMem.c ==========================================================*/
extern void Dar_ManStartMemory( Dar_Man_t * p );
extern void Dar_ManStopMemory( Dar_Man_t * p );
/*=== darObj.c ==========================================================*/
extern Dar_Obj_t * Dar_ObjCreatePi( Dar_Man_t * p );
extern Dar_Obj_t * Dar_ObjCreatePo( Dar_Man_t * p, Dar_Obj_t * pDriver );
extern Dar_Obj_t * Dar_ObjCreate( Dar_Man_t * p, Dar_Obj_t * pGhost );
extern void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFan0, Dar_Obj_t * pFan1 );
extern void Dar_ObjDisconnect( Dar_Man_t * p, Dar_Obj_t * pObj );
extern void Dar_ObjDelete( Dar_Man_t * p, Dar_Obj_t * pObj );
extern void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop );
extern void Dar_ObjPatchFanin0( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFaninNew );
extern void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew, int fNodesOnly );
/*=== darOper.c =========================================================*/
extern Dar_Obj_t * Dar_IthVar( Dar_Man_t * p, int i );
extern Dar_Obj_t * Dar_Oper( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t Type );
extern Dar_Obj_t * Dar_And( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 );
extern Dar_Obj_t * Dar_Latch( Dar_Man_t * p, Dar_Obj_t * pObj, int fInitOne );
extern Dar_Obj_t * Dar_Or( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 );
extern Dar_Obj_t * Dar_Exor( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 );
extern Dar_Obj_t * Dar_Mux( Dar_Man_t * p, Dar_Obj_t * pC, Dar_Obj_t * p1, Dar_Obj_t * p0 );
extern Dar_Obj_t * Dar_Maj( Dar_Man_t * p, Dar_Obj_t * pA, Dar_Obj_t * pB, Dar_Obj_t * pC );
extern Dar_Obj_t * Dar_Miter( Dar_Man_t * p, Vec_Ptr_t * vPairs );
extern Dar_Obj_t * Dar_CreateAnd( Dar_Man_t * p, int nVars );
extern Dar_Obj_t * Dar_CreateOr( Dar_Man_t * p, int nVars );
extern Dar_Obj_t * Dar_CreateExor( Dar_Man_t * p, int nVars );
/*=== darSeq.c ========================================================*/
extern int Dar_ManSeqStrash( Dar_Man_t * p, int nLatches, int * pInits );
/*=== darTable.c ========================================================*/
extern Dar_Obj_t * Dar_TableLookup( Dar_Man_t * p, Dar_Obj_t * pGhost );
extern void Dar_TableInsert( Dar_Man_t * p, Dar_Obj_t * pObj );
extern void Dar_TableDelete( Dar_Man_t * p, Dar_Obj_t * pObj );
extern int Dar_TableCountEntries( Dar_Man_t * p );
extern void Dar_TableProfile( Dar_Man_t * p );
/*=== darUtil.c =========================================================*/
extern Dar_Par_t * Dar_ManDefaultParams();
extern void Dar_ManIncrementTravId( Dar_Man_t * p );
extern int Dar_ManLevels( Dar_Man_t * p );
extern void Dar_ManCleanData( Dar_Man_t * p );
extern void Dar_ObjCleanData_rec( Dar_Obj_t * pObj );
extern void Dar_ObjCollectMulti( Dar_Obj_t * pFunc, Vec_Ptr_t * vSuper );
extern int Dar_ObjIsMuxType( Dar_Obj_t * pObj );
extern int Dar_ObjRecognizeExor( Dar_Obj_t * pObj, Dar_Obj_t ** ppFan0, Dar_Obj_t ** ppFan1 );
extern Dar_Obj_t * Dar_ObjRecognizeMux( Dar_Obj_t * pObj, Dar_Obj_t ** ppObjT, Dar_Obj_t ** ppObjE );
extern Dar_Obj_t * Dar_ObjReal_rec( Dar_Obj_t * pObj );
extern void Dar_ObjPrintEqn( FILE * pFile, Dar_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
extern void Dar_ObjPrintVerilog( FILE * pFile, Dar_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
extern void Dar_ObjPrintVerbose( Dar_Obj_t * pObj, int fHaig );
extern void Dar_ManPrintVerbose( Dar_Man_t * p, int fHaig );
extern void Dar_ManDumpBlif( Dar_Man_t * p, char * pFileName );
/*=== darMem.c ===========================================================*/
// fixed-size-block memory manager
extern Dar_MmFixed_t * Dar_MmFixedStart( int nEntrySize, int nEntriesMax );
extern void Dar_MmFixedStop( Dar_MmFixed_t * p, int fVerbose );
extern char * Dar_MmFixedEntryFetch( Dar_MmFixed_t * p );
extern void Dar_MmFixedEntryRecycle( Dar_MmFixed_t * p, char * pEntry );
extern void Dar_MmFixedRestart( Dar_MmFixed_t * p );
extern int Dar_MmFixedReadMemUsage( Dar_MmFixed_t * p );
extern int Dar_MmFixedReadMaxEntriesUsed( Dar_MmFixed_t * p );
// flexible-size-block memory manager
extern Dar_MmFlex_t * Dar_MmFlexStart();
extern void Dar_MmFlexStop( Dar_MmFlex_t * p, int fVerbose );
extern char * Dar_MmFlexEntryFetch( Dar_MmFlex_t * p, int nBytes );
extern void Dar_MmFlexRestart( Dar_MmFlex_t * p );
extern int Dar_MmFlexReadMemUsage( Dar_MmFlex_t * p );
// hierarchical memory manager
extern Dar_MmStep_t * Dar_MmStepStart( int nSteps );
extern void Dar_MmStepStop( Dar_MmStep_t * p, int fVerbose );
extern char * Dar_MmStepEntryFetch( Dar_MmStep_t * p, int nBytes );
extern void Dar_MmStepEntryRecycle( Dar_MmStep_t * p, char * pEntry, int nBytes );
extern int Dar_MmStepReadMemUsage( Dar_MmStep_t * p );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|