ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
ivyCutTrav.c
Go to the documentation of this file.
1
20
21#include "ivy.h"
22
24
25
29
30static unsigned * Ivy_NodeCutElementary( Vec_Int_t * vStore, int nWords, int NodeId );
31static void Ivy_NodeComputeVolume( Ivy_Obj_t * pObj, int nNodeLimit, Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront );
32static void Ivy_NodeFindCutsMerge( Vec_Ptr_t * vCuts0, Vec_Ptr_t * vCuts1, Vec_Ptr_t * vCuts, int nLeaves, int nWords, Vec_Int_t * vStore );
33
37
49Ivy_Store_t * Ivy_NodeFindCutsTravAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves, int nNodeLimit,
50 Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront, Vec_Int_t * vStore, Vec_Vec_t * vBitCuts )
51{
52 static Ivy_Store_t CutStore, * pCutStore = &CutStore;
53 Vec_Ptr_t * vCuts, * vCuts0, * vCuts1;
54 unsigned * pBitCut;
55 Ivy_Obj_t * pLeaf;
56 Ivy_Cut_t * pCut;
57 int i, k, nWords, nNodes;
58
59 assert( nLeaves <= IVY_CUT_INPUT );
60
61 // find the given number of nodes in the TFI
62 Ivy_NodeComputeVolume( pObj, nNodeLimit - 1, vNodes, vFront );
63 nNodes = Vec_PtrSize(vNodes);
64// assert( nNodes <= nNodeLimit );
65
66 // make sure vBitCuts has enough room
67 Vec_VecExpand( vBitCuts, nNodes-1 );
68 Vec_VecClear( vBitCuts );
69
70 // prepare the memory manager
71 Vec_IntClear( vStore );
72 Vec_IntGrow( vStore, 64000 );
73
74 // set elementary cuts for the leaves
75 nWords = Extra_BitWordNum( nNodes );
76 Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pLeaf, i )
77 {
78 assert( Ivy_ObjTravId(pLeaf) < nNodes );
79 // get the new bitcut
80 pBitCut = Ivy_NodeCutElementary( vStore, nWords, Ivy_ObjTravId(pLeaf) );
81 // set it as the cut of this leaf
82 Vec_VecPush( vBitCuts, Ivy_ObjTravId(pLeaf), pBitCut );
83 }
84
85 // compute the cuts for each node
86 Vec_PtrForEachEntry( Ivy_Obj_t *, vNodes, pLeaf, i )
87 {
88 // skip the leaves
89 vCuts = Vec_VecEntry( vBitCuts, Ivy_ObjTravId(pLeaf) );
90 if ( Vec_PtrSize(vCuts) > 0 )
91 continue;
92 // add elementary cut
93 pBitCut = Ivy_NodeCutElementary( vStore, nWords, Ivy_ObjTravId(pLeaf) );
94 // set it as the cut of this leaf
95 Vec_VecPush( vBitCuts, Ivy_ObjTravId(pLeaf), pBitCut );
96 // get the fanin cuts
97 vCuts0 = Vec_VecEntry( vBitCuts, Ivy_ObjTravId( Ivy_ObjFanin0(pLeaf) ) );
98 vCuts1 = Vec_VecEntry( vBitCuts, Ivy_ObjTravId( Ivy_ObjFanin1(pLeaf) ) );
99 assert( Vec_PtrSize(vCuts0) > 0 );
100 assert( Vec_PtrSize(vCuts1) > 0 );
101 // merge the cuts
102 Ivy_NodeFindCutsMerge( vCuts0, vCuts1, vCuts, nLeaves, nWords, vStore );
103 }
104
105 // start the structure
106 pCutStore->nCuts = 0;
107 pCutStore->nCutsMax = IVY_CUT_LIMIT;
108 // collect the cuts of the root node
109 vCuts = Vec_VecEntry( vBitCuts, Ivy_ObjTravId(pObj) );
110 Vec_PtrForEachEntry( unsigned *, vCuts, pBitCut, i )
111 {
112 pCut = pCutStore->pCuts + pCutStore->nCuts++;
113 pCut->nSize = 0;
114 pCut->nSizeMax = nLeaves;
115 pCut->uHash = 0;
116 for ( k = 0; k < nNodes; k++ )
117 if ( Extra_TruthHasBit(pBitCut, k) )
118 pCut->pArray[ pCut->nSize++ ] = Ivy_ObjId( (Ivy_Obj_t *)Vec_PtrEntry(vNodes, k) );
119 assert( pCut->nSize <= nLeaves );
120 if ( pCutStore->nCuts == pCutStore->nCutsMax )
121 break;
122 }
123
124 // clean the travIds
125 Vec_PtrForEachEntry( Ivy_Obj_t *, vNodes, pLeaf, i )
126 pLeaf->TravId = 0;
127 return pCutStore;
128}
129
141unsigned * Ivy_NodeCutElementary( Vec_Int_t * vStore, int nWords, int NodeId )
142{
143 unsigned * pBitCut;
144 pBitCut = Vec_IntFetch( vStore, nWords );
145 memset( pBitCut, 0, (size_t)(4 * nWords) );
146 Extra_TruthSetBit( pBitCut, NodeId );
147 return pBitCut;
148}
149
161int Ivy_CompareNodesByLevel( Ivy_Obj_t ** ppObj1, Ivy_Obj_t ** ppObj2 )
162{
163 Ivy_Obj_t * pObj1 = *ppObj1;
164 Ivy_Obj_t * pObj2 = *ppObj2;
165 if ( pObj1->Level < pObj2->Level )
166 return -1;
167 if ( pObj1->Level > pObj2->Level )
168 return 1;
169 return 0;
170}
171
184{
185 if ( Ivy_ObjIsCi(pObj) || Depth == 0 )
186 return;
187 Ivy_NodeComputeVolumeTrav1_rec( Ivy_ObjFanin0(pObj), Depth - 1 );
188 Ivy_NodeComputeVolumeTrav1_rec( Ivy_ObjFanin1(pObj), Depth - 1 );
189 pObj->fMarkA = 1;
190}
191
204{
205 if ( !pObj->fMarkA )
206 return;
207 Ivy_NodeComputeVolumeTrav2_rec( Ivy_ObjFanin0(pObj), vNodes );
208 Ivy_NodeComputeVolumeTrav2_rec( Ivy_ObjFanin1(pObj), vNodes );
209 Vec_PtrPush( vNodes, pObj );
210}
211
223void Ivy_NodeComputeVolume( Ivy_Obj_t * pObj, int nNodeLimit, Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront )
224{
225 Ivy_Obj_t * pTemp, * pFanin;
226 int i, nNodes;
227 // mark nodes up to the given depth
229 // collect the marked nodes
230 Vec_PtrClear( vFront );
231 Ivy_NodeComputeVolumeTrav2_rec( pObj, vFront );
232 // find the fanins that are not marked
233 Vec_PtrClear( vNodes );
234 Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pTemp, i )
235 {
236 pFanin = Ivy_ObjFanin0(pTemp);
237 if ( !pFanin->fMarkA )
238 {
239 pFanin->fMarkA = 1;
240 Vec_PtrPush( vNodes, pFanin );
241 }
242 pFanin = Ivy_ObjFanin1(pTemp);
243 if ( !pFanin->fMarkA )
244 {
245 pFanin->fMarkA = 1;
246 Vec_PtrPush( vNodes, pFanin );
247 }
248 }
249 // remember the number of nodes in the frontier
250 nNodes = Vec_PtrSize( vNodes );
251 // add the remaining nodes
252 Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pTemp, i )
253 Vec_PtrPush( vNodes, pTemp );
254 // unmark the nodes
255 Vec_PtrForEachEntry( Ivy_Obj_t *, vNodes, pTemp, i )
256 {
257 pTemp->fMarkA = 0;
258 pTemp->TravId = i;
259 }
260 // collect the frontier nodes
261 Vec_PtrClear( vFront );
262 Vec_PtrForEachEntryStop( Ivy_Obj_t *, vNodes, pTemp, i, nNodes )
263 Vec_PtrPush( vFront, pTemp );
264// printf( "%d ", Vec_PtrSize(vNodes) );
265}
266
278void Ivy_NodeComputeVolume2( Ivy_Obj_t * pObj, int nNodeLimit, Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront )
279{
280 Ivy_Obj_t * pLeaf, * pPivot, * pFanin;
281 int LevelMax, i;
282 assert( Ivy_ObjIsNode(pObj) );
283 // clear arrays
284 Vec_PtrClear( vNodes );
285 Vec_PtrClear( vFront );
286 // add the root
287 pObj->fMarkA = 1;
288 Vec_PtrPush( vNodes, pObj );
289 Vec_PtrPush( vFront, pObj );
290 // expand node with maximum level
291 LevelMax = pObj->Level;
292 do {
293 // get the node to expand
294 pPivot = NULL;
295 Vec_PtrForEachEntryReverse( Ivy_Obj_t *, vFront, pLeaf, i )
296 {
297 if ( (int)pLeaf->Level == LevelMax )
298 {
299 pPivot = pLeaf;
300 break;
301 }
302 }
303 // decrease level if we did not find the node
304 if ( pPivot == NULL )
305 {
306 if ( --LevelMax == 0 )
307 break;
308 continue;
309 }
310 // the node to expand is found
311 // remove it from frontier
312 Vec_PtrRemove( vFront, pPivot );
313 // add fanins
314 pFanin = Ivy_ObjFanin0(pPivot);
315 if ( !pFanin->fMarkA )
316 {
317 pFanin->fMarkA = 1;
318 Vec_PtrPush( vNodes, pFanin );
319 Vec_PtrPush( vFront, pFanin );
320 }
321 pFanin = Ivy_ObjFanin1(pPivot);
322 if ( pFanin && !pFanin->fMarkA )
323 {
324 pFanin->fMarkA = 1;
325 Vec_PtrPush( vNodes, pFanin );
326 Vec_PtrPush( vFront, pFanin );
327 }
328 // quit if we collected enough nodes
329 } while ( Vec_PtrSize(vNodes) < nNodeLimit );
330
331 // sort nodes by level
332 Vec_PtrSort( vNodes, (int (*)(const void *, const void *))Ivy_CompareNodesByLevel );
333 // make sure the nodes are ordered in the increasing number of levels
334 pFanin = (Ivy_Obj_t *)Vec_PtrEntry( vNodes, 0 );
335 pPivot = (Ivy_Obj_t *)Vec_PtrEntryLast( vNodes );
336 assert( pFanin->Level <= pPivot->Level );
337
338 // clean the marks and remember node numbers in the TravId
339 Vec_PtrForEachEntry( Ivy_Obj_t *, vNodes, pFanin, i )
340 {
341 pFanin->fMarkA = 0;
342 pFanin->TravId = i;
343 }
344}
345
357static inline void Extra_TruthOrWords( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nWords )
358{
359 int w;
360 for ( w = nWords-1; w >= 0; w-- )
361 pOut[w] = pIn0[w] | pIn1[w];
362}
363static inline int Extra_TruthIsImplyWords( unsigned * pIn1, unsigned * pIn2, int nWords )
364{
365 int w;
366 for ( w = nWords-1; w >= 0; w-- )
367 if ( pIn1[w] & ~pIn2[w] )
368 return 0;
369 return 1;
370}
371
383void Ivy_NodeFindCutsMerge( Vec_Ptr_t * vCuts0, Vec_Ptr_t * vCuts1, Vec_Ptr_t * vCuts,
384 int nLeaves, int nWords, Vec_Int_t * vStore )
385{
386 unsigned * pBitCut, * pBitCut0, * pBitCut1, * pBitCutTest;
387 int i, k, c, w, Counter;
388 // iterate through the cut pairs
389 Vec_PtrForEachEntry( unsigned *, vCuts0, pBitCut0, i )
390 Vec_PtrForEachEntry( unsigned *, vCuts1, pBitCut1, k )
391 {
392 // skip infeasible cuts
393 Counter = 0;
394 for ( w = 0; w < nWords; w++ )
395 {
396 Counter += Extra_WordCountOnes( pBitCut0[w] | pBitCut1[w] );
397 if ( Counter > nLeaves )
398 break;
399 }
400 if ( Counter > nLeaves )
401 continue;
402 // the new cut is feasible - create it
403 pBitCutTest = Vec_IntFetch( vStore, nWords );
404 Extra_TruthOrWords( pBitCutTest, pBitCut0, pBitCut1, nWords );
405 // filter contained cuts; try to find containing cut
406 w = 0;
407 Vec_PtrForEachEntry( unsigned *, vCuts, pBitCut, c )
408 {
409 if ( Extra_TruthIsImplyWords( pBitCut, pBitCutTest, nWords ) )
410 break;
411 if ( Extra_TruthIsImplyWords( pBitCutTest, pBitCut, nWords ) )
412 continue;
413 Vec_PtrWriteEntry( vCuts, w++, pBitCut );
414 }
415 if ( c != Vec_PtrSize(vCuts) )
416 continue;
417 Vec_PtrShrink( vCuts, w );
418 // add the cut
419 Vec_PtrPush( vCuts, pBitCutTest );
420 }
421}
422
435{
436 Ivy_Store_t * pStore;
437 Ivy_Obj_t * pObj;
438 Vec_Ptr_t * vNodes, * vFront;
439 Vec_Int_t * vStore;
440 Vec_Vec_t * vBitCuts;
441 int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
442 abctime clk = Abc_Clock();
443
444 vNodes = Vec_PtrAlloc( 100 );
445 vFront = Vec_PtrAlloc( 100 );
446 vStore = Vec_IntAlloc( 100 );
447 vBitCuts = Vec_VecAlloc( 100 );
448
449 nNodeTotal = nNodeOver = 0;
450 nCutsTotal = -Ivy_ManNodeNum(p);
451 Ivy_ManForEachObj( p, pObj, i )
452 {
453 if ( !Ivy_ObjIsNode(pObj) )
454 continue;
455 pStore = Ivy_NodeFindCutsTravAll( p, pObj, 4, 60, vNodes, vFront, vStore, vBitCuts );
456 nCutsCut = pStore->nCuts;
457 nCutsTotal += nCutsCut;
458 nNodeOver += (nCutsCut == IVY_CUT_LIMIT);
459 nNodeTotal++;
460 }
461 printf( "Total cuts = %6d. Trivial = %6d. Nodes = %6d. Satur = %6d. ",
462 nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
463 ABC_PRT( "Time", Abc_Clock() - clk );
464
465 Vec_PtrFree( vNodes );
466 Vec_PtrFree( vFront );
467 Vec_IntFree( vStore );
468 Vec_VecFree( vBitCuts );
469
470}
471
475
476
478
int nWords
Definition abcNpn.c:127
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_PRT(a, t)
Definition abc_global.h:255
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
void Ivy_NodeComputeVolume2(Ivy_Obj_t *pObj, int nNodeLimit, Vec_Ptr_t *vNodes, Vec_Ptr_t *vFront)
Definition ivyCutTrav.c:278
void Ivy_NodeComputeVolumeTrav2_rec(Ivy_Obj_t *pObj, Vec_Ptr_t *vNodes)
Definition ivyCutTrav.c:203
Ivy_Store_t * Ivy_NodeFindCutsTravAll(Ivy_Man_t *p, Ivy_Obj_t *pObj, int nLeaves, int nNodeLimit, Vec_Ptr_t *vNodes, Vec_Ptr_t *vFront, Vec_Int_t *vStore, Vec_Vec_t *vBitCuts)
FUNCTION DEFINITIONS ///.
Definition ivyCutTrav.c:49
void Ivy_ManTestCutsTravAll(Ivy_Man_t *p)
Definition ivyCutTrav.c:434
void Ivy_NodeComputeVolumeTrav1_rec(Ivy_Obj_t *pObj, int Depth)
Definition ivyCutTrav.c:183
int Ivy_CompareNodesByLevel(Ivy_Obj_t **ppObj1, Ivy_Obj_t **ppObj2)
Definition ivyCutTrav.c:161
struct Ivy_Cut_t_ Ivy_Cut_t
Definition ivy.h:155
#define IVY_CUT_INPUT
Definition ivy.h:153
typedefABC_NAMESPACE_HEADER_START struct Ivy_Man_t_ Ivy_Man_t
INCLUDES ///.
Definition ivy.h:46
#define Ivy_ManForEachObj(p, pObj, i)
Definition ivy.h:393
struct Ivy_Store_t_ Ivy_Store_t
Definition ivy.h:165
struct Ivy_Obj_t_ Ivy_Obj_t
Definition ivy.h:47
#define IVY_CUT_LIMIT
Definition ivy.h:152
unsigned uHash
Definition ivy.h:162
short nSize
Definition ivy.h:159
short nSizeMax
Definition ivy.h:160
int pArray[IVY_CUT_INPUT]
Definition ivy.h:161
int TravId
Definition ivy.h:76
unsigned Level
Definition ivy.h:84
unsigned fMarkA
Definition ivy.h:78
Ivy_Cut_t pCuts[IVY_CUT_LIMIT]
Definition ivy.h:172
int nCutsMax
Definition ivy.h:170
int nCuts
Definition ivy.h:168
#define assert(ex)
Definition util_old.h:213
char * memset()
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition vecPtr.h:63
#define Vec_PtrForEachEntryStop(Type, vVec, pEntry, i, Stop)
Definition vecPtr.h:59
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42