1 /**CFile****************************************************************
2
3 FileName [giaShrink6.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Implementation of DAG-aware unmapping for 6-input cuts.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: giaShrink6.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22 #include "bool/bdc/bdc.h"
23 #include "bool/rsb/rsb.h"
24 //#include "misc/util/utilTruth.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31
32 static word Truth[8] = {
33 ABC_CONST(0xAAAAAAAAAAAAAAAA),
34 ABC_CONST(0xCCCCCCCCCCCCCCCC),
35 ABC_CONST(0xF0F0F0F0F0F0F0F0),
36 ABC_CONST(0xFF00FF00FF00FF00),
37 ABC_CONST(0xFFFF0000FFFF0000),
38 ABC_CONST(0xFFFFFFFF00000000),
39 ABC_CONST(0x0000000000000000),
40 ABC_CONST(0xFFFFFFFFFFFFFFFF)
41 };
42
43 // fanout structure
44 typedef struct Shr_Fan_t_ Shr_Fan_t;
45 struct Shr_Fan_t_
46 {
47 int iFan; // fanout ID
48 int Next; // next structure
49 };
50
51 // operation manager
52 typedef struct Shr_Man_t_ Shr_Man_t;
53 struct Shr_Man_t_
54 {
55 Gia_Man_t * pGia; // user's AIG
56 Gia_Man_t * pNew; // constructed AIG
57 int nDivMax; // max number of divisors
58 int nNewSize; // max growth size
59 // dynamic fanout (can only grow)
60 Vec_Wrd_t * vFanMem; // fanout memory
61 Vec_Int_t * vObj2Fan; // fanout
62 Shr_Fan_t * pFanTemp; // temporary fanout
63 // divisors
64 Vec_Int_t * vDivs; // divisors
65 Vec_Int_t * vPrio; // priority queue
66 Vec_Int_t * vDivResub; // resubstitution
67 Vec_Int_t * vLeaves; // cut leaves
68 // truth tables
69 Vec_Wrd_t * vTruths; // truth tables
70 Vec_Wrd_t * vDivTruths; // truth tables
71 // bidecomposition
72 Rsb_Man_t * pManRsb;
73 Bdc_Man_t * pManDec;
74 Bdc_Par_t Pars;
75 // statistics
76 };
77
78 #define Shr_ObjForEachFanout( p, iNode, iFan ) \
79 for ( iFan = Shr_ManFanIterStart(p, iNode); iFan; iFan = Shr_ManFanIterNext(p) )
80
81 ////////////////////////////////////////////////////////////////////////
82 /// FUNCTION DEFINITIONS ///
83 ////////////////////////////////////////////////////////////////////////
84
85 /**Function*************************************************************
86
87 Synopsis []
88
89 Description []
90
91 SideEffects []
92
93 SeeAlso []
94
95 ***********************************************************************/
Shr_ManAlloc(Gia_Man_t * pGia)96 Shr_Man_t * Shr_ManAlloc( Gia_Man_t * pGia )
97 {
98 Shr_Man_t * p;
99 p = ABC_CALLOC( Shr_Man_t, 1 );
100 p->nDivMax = 64;
101 p->nNewSize = 2 * Gia_ManObjNum(pGia);
102 p->pGia = pGia;
103 p->vFanMem = Vec_WrdAlloc( 1000 ); Vec_WrdPush(p->vFanMem, -1);
104 p->vObj2Fan = Vec_IntStart( p->nNewSize );
105 p->vDivs = Vec_IntAlloc( 1000 );
106 p->vPrio = Vec_IntAlloc( 1000 );
107 p->vTruths = Vec_WrdStart( p->nNewSize );
108 p->vDivTruths = Vec_WrdAlloc( 100 );
109 p->vDivResub = Vec_IntAlloc( 6 );
110 p->vLeaves = Vec_IntAlloc( 6 );
111 // start new manager
112 p->pNew = Gia_ManStart( p->nNewSize );
113 p->pNew->pName = Abc_UtilStrsav( pGia->pName );
114 p->pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
115 Gia_ManHashAlloc( p->pNew );
116 Gia_ManCleanLevels( p->pNew, p->nNewSize );
117 // allocate traversal IDs
118 p->pNew->nObjs = p->nNewSize;
119 Gia_ManIncrementTravId( p->pNew );
120 p->pNew->nObjs = 1;
121 // start decompostion
122 p->Pars.nVarsMax = 6;
123 p->Pars.fVerbose = 0;
124 p->pManDec = Bdc_ManAlloc( &p->Pars );
125 p->pManRsb = Rsb_ManAlloc( 6, p->nDivMax, 4, 1 );
126 return p;
127 }
Shr_ManFree(Shr_Man_t * p)128 Gia_Man_t * Shr_ManFree( Shr_Man_t * p )
129 {
130 // prepare the manager
131 Gia_Man_t * pTemp;
132 Gia_ManHashStop( p->pNew );
133 Vec_IntFreeP( &p->pNew->vLevels );
134 if ( Gia_ManHasDangling(p->pNew) )
135 {
136 p->pNew = Gia_ManCleanup( pTemp = p->pNew );
137 if ( Gia_ManAndNum(p->pNew) != Gia_ManAndNum(pTemp) )
138 printf( "Node reduction after sweep %6d -> %6d.\n", Gia_ManAndNum(pTemp), Gia_ManAndNum(p->pNew) );
139 Gia_ManStop( pTemp );
140 }
141 Gia_ManSetRegNum( p->pNew, Gia_ManRegNum(p->pGia) );
142 pTemp = p->pNew; p->pNew = NULL;
143 // free data structures
144 Rsb_ManFree( p->pManRsb );
145 Bdc_ManFree( p->pManDec );
146 Gia_ManStopP( &p->pNew );
147 Vec_WrdFree( p->vFanMem );
148 Vec_IntFree( p->vObj2Fan );
149 Vec_IntFree( p->vDivs );
150 Vec_IntFree( p->vPrio );
151 Vec_WrdFree( p->vTruths );
152 Vec_WrdFree( p->vDivTruths );
153 Vec_IntFree( p->vDivResub );
154 Vec_IntFree( p->vLeaves );
155 ABC_FREE( p );
156 return pTemp;
157 }
158
159
160 /**Function*************************************************************
161
162 Synopsis [Fanout manipulation.]
163
164 Description []
165
166 SideEffects []
167
168 SeeAlso []
169
170 ***********************************************************************/
Shr_ManAddFanout(Shr_Man_t * p,int iFanin,int iFanout)171 static inline void Shr_ManAddFanout( Shr_Man_t * p, int iFanin, int iFanout )
172 {
173 union {
174 Shr_Fan_t sFan;
175 word sWord;
176 } FanStr;
177 FanStr.sFan.iFan = iFanout;
178 FanStr.sFan.Next = Vec_IntEntry(p->vObj2Fan, iFanin);
179 Vec_IntWriteEntry( p->vObj2Fan, iFanin, Vec_WrdSize(p->vFanMem) );
180 Vec_WrdPush(p->vFanMem, FanStr.sWord );
181 }
Shr_ManFanIterStart(Shr_Man_t * p,int iNode)182 static inline int Shr_ManFanIterStart( Shr_Man_t * p, int iNode )
183 {
184 if ( Vec_IntEntry(p->vObj2Fan, iNode) == 0 )
185 return 0;
186 p->pFanTemp = (Shr_Fan_t *)Vec_WrdEntryP( p->vFanMem, Vec_IntEntry(p->vObj2Fan, iNode) );
187 return p->pFanTemp->iFan;
188 }
Shr_ManFanIterNext(Shr_Man_t * p)189 static inline int Shr_ManFanIterNext( Shr_Man_t * p )
190 {
191 if ( p->pFanTemp->Next == 0 )
192 return 0;
193 p->pFanTemp = (Shr_Fan_t *)Vec_WrdEntryP( p->vFanMem, p->pFanTemp->Next );
194 return p->pFanTemp->iFan;
195 }
196
197 /**Function*************************************************************
198
199 Synopsis [Collect divisors.]
200
201 Description []
202
203 SideEffects []
204
205 SeeAlso []
206
207 ***********************************************************************/
Shr_ManDivPushOrderByLevel(Shr_Man_t * p,int iDiv)208 static inline int Shr_ManDivPushOrderByLevel( Shr_Man_t * p, int iDiv )
209 {
210 int iPlace, * pArray;
211 Vec_IntPush( p->vPrio, iDiv );
212 if ( Vec_IntSize(p->vPrio) == 1 )
213 return 0;
214 pArray = Vec_IntArray(p->vPrio);
215 for ( iPlace = Vec_IntSize(p->vPrio) - 1; iPlace > 0; iPlace-- )
216 if ( Gia_ObjLevel(p->pNew, Gia_ManObj(p->pNew, pArray[iPlace-1])) >
217 Gia_ObjLevel(p->pNew, Gia_ManObj(p->pNew, pArray[iPlace])) )
218 ABC_SWAP( int, pArray[iPlace-1], pArray[iPlace] )
219 else
220 break;
221 return iPlace; // the place of the new divisor
222 }
Shr_ManCollectDivisors(Shr_Man_t * p,Vec_Int_t * vLeaves,int Limit,int nFanoutMax)223 static inline int Shr_ManCollectDivisors( Shr_Man_t * p, Vec_Int_t * vLeaves, int Limit, int nFanoutMax )
224 {
225 Gia_Obj_t * pFan;
226 int i, c, iDiv, iFan, iPlace;
227 assert( Limit > 6 );
228 Vec_IntClear( p->vDivs );
229 Vec_IntClear( p->vPrio );
230 Gia_ManIncrementTravId( p->pNew );
231 Vec_IntForEachEntry( vLeaves, iDiv, i )
232 {
233 Vec_IntPush( p->vDivs, iDiv );
234 Shr_ManDivPushOrderByLevel( p, iDiv );
235 Gia_ObjSetTravIdCurrentId( p->pNew, iDiv );
236 }
237 Vec_IntForEachEntry( p->vPrio, iDiv, i )
238 {
239 c = 0;
240 assert( Gia_ObjIsTravIdCurrentId(p->pNew, iDiv) );
241 Shr_ObjForEachFanout( p, iDiv, iFan )
242 {
243 if ( c++ == nFanoutMax )
244 break;
245 if ( Gia_ObjIsTravIdCurrentId(p->pNew, iFan) )
246 continue;
247 pFan = Gia_ManObj( p->pNew, iFan );
248 assert( Gia_ObjIsAnd(pFan) );
249 assert( Gia_ObjLevel(p->pNew, Gia_ManObj(p->pNew, iDiv)) < Gia_ObjLevel(p->pNew, pFan) );
250 if ( !Gia_ObjIsTravIdCurrentId(p->pNew, Gia_ObjFaninId0(pFan, iFan)) ||
251 !Gia_ObjIsTravIdCurrentId(p->pNew, Gia_ObjFaninId1(pFan, iFan)) )
252 continue;
253 Vec_IntPush( p->vDivs, iFan );
254 Gia_ObjSetTravIdCurrentId( p->pNew, iFan );
255 iPlace = Shr_ManDivPushOrderByLevel( p, iFan );
256 assert( i < iPlace );
257 if ( Vec_IntSize(p->vDivs) == Limit )
258 return Vec_IntSize(p->vDivs);
259 }
260 }
261 return Vec_IntSize(p->vDivs);
262 }
263
264 /**Function*************************************************************
265
266 Synopsis [Resynthesizes nodes using bi-decomposition.]
267
268 Description []
269
270 SideEffects []
271
272 SeeAlso []
273
274 ***********************************************************************/
Shr_ObjPerformBidec(Shr_Man_t * p,Bdc_Man_t * pManDec,Gia_Man_t * pNew,Vec_Int_t * vLeafLits,word uTruth1,word uTruthC)275 int Shr_ObjPerformBidec( Shr_Man_t * p, Bdc_Man_t * pManDec, Gia_Man_t * pNew, Vec_Int_t * vLeafLits, word uTruth1, word uTruthC )
276 {
277 Bdc_Fun_t * pFunc;
278 Gia_Obj_t * pObj;
279 int i, iVar, iLit, nNodes, iLast;
280 int nVars = Vec_IntSize(vLeafLits);
281 assert( uTruth1 != 0 && uTruthC != 0 );
282 Bdc_ManDecompose( pManDec, (unsigned *)&uTruth1, (unsigned *)&uTruthC, nVars, NULL, 1000 );
283 Bdc_FuncSetCopyInt( Bdc_ManFunc(pManDec, 0), 1 );
284 Vec_IntForEachEntry( vLeafLits, iVar, i )
285 Bdc_FuncSetCopyInt( Bdc_ManFunc(pManDec, i+1), Abc_Var2Lit(iVar, 0) );
286 nNodes = Bdc_ManNodeNum( pManDec );
287 for ( i = nVars + 1; i < nNodes; i++ )
288 {
289 pFunc = Bdc_ManFunc( pManDec, i );
290 iLast = Gia_ManObjNum(pNew);
291 iLit = Gia_ManHashAnd( pNew, Bdc_FunFanin0Copy(pFunc), Bdc_FunFanin1Copy(pFunc) );
292 Bdc_FuncSetCopyInt( pFunc, iLit );
293 if ( iLast == Gia_ManObjNum(pNew) )
294 continue;
295 assert( iLast + 1 == Gia_ManObjNum(pNew) );
296 pObj = Gia_ManObj(pNew, Abc_Lit2Var(iLit));
297 Gia_ObjSetAndLevel( pNew, pObj );
298 Shr_ManAddFanout( p, Gia_ObjFaninId0p(pNew, pObj), Gia_ObjId(pNew, pObj) );
299 Shr_ManAddFanout( p, Gia_ObjFaninId1p(pNew, pObj), Gia_ObjId(pNew, pObj) );
300 assert( Gia_ManObjNum(pNew) < p->nNewSize );
301 }
302 return Bdc_FunObjCopy( Bdc_ManRoot(pManDec) );
303 }
304
305
306 /**Function*************************************************************
307
308 Synopsis [Compute truth table.]
309
310 Description []
311
312 SideEffects []
313
314 SeeAlso []
315
316 ***********************************************************************/
Shr_ManComputeTruth6_rec(Gia_Man_t * p,int iNode,Vec_Wrd_t * vTruths)317 word Shr_ManComputeTruth6_rec( Gia_Man_t * p, int iNode, Vec_Wrd_t * vTruths )
318 {
319 Gia_Obj_t * pObj;
320 word Truth0, Truth1;
321 if ( Gia_ObjIsTravIdCurrentId(p, iNode) )
322 return Vec_WrdEntry(vTruths, iNode);
323 Gia_ObjSetTravIdCurrentId(p, iNode);
324 pObj = Gia_ManObj( p, iNode );
325 assert( Gia_ObjIsAnd(pObj) );
326 Truth0 = Shr_ManComputeTruth6_rec( p, Gia_ObjFaninId0p(p, pObj), vTruths );
327 Truth1 = Shr_ManComputeTruth6_rec( p, Gia_ObjFaninId1p(p, pObj), vTruths );
328 if ( Gia_ObjFaninC0(pObj) )
329 Truth0 = ~Truth0;
330 if ( Gia_ObjFaninC1(pObj) )
331 Truth1 = ~Truth1;
332 Vec_WrdWriteEntry( vTruths, iNode, Truth0 & Truth1 );
333 return Truth0 & Truth1;
334 }
Shr_ManComputeTruth6(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vLeaves,Vec_Wrd_t * vTruths)335 word Shr_ManComputeTruth6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves, Vec_Wrd_t * vTruths )
336 {
337 int i, iLeaf;
338 assert( Gia_ObjIsAnd(pObj) );
339 Gia_ManIncrementTravId( p );
340 Vec_IntForEachEntry( vLeaves, iLeaf, i )
341 {
342 Gia_ObjSetTravIdCurrentId( p, iLeaf );
343 Vec_WrdWriteEntry( vTruths, iLeaf, Truth[i] );
344 }
345 return Shr_ManComputeTruth6_rec( p, Gia_ObjId(p, pObj), vTruths );
346 }
347
348 /**Function*************************************************************
349
350 Synopsis [Compute truth table.]
351
352 Description []
353
354 SideEffects []
355
356 SeeAlso []
357
358 ***********************************************************************/
Shr_ManComputeTruths(Gia_Man_t * p,int nVars,Vec_Int_t * vDivs,Vec_Wrd_t * vDivTruths,Vec_Wrd_t * vTruths)359 void Shr_ManComputeTruths( Gia_Man_t * p, int nVars, Vec_Int_t * vDivs, Vec_Wrd_t * vDivTruths, Vec_Wrd_t * vTruths )
360 {
361 Gia_Obj_t * pObj;
362 word Truth0, Truth1;//, Truthh;
363 int i, iDiv;
364 Vec_WrdClear( vDivTruths );
365 Vec_IntForEachEntryStop( vDivs, iDiv, i, nVars )
366 {
367 Vec_WrdWriteEntry( vTruths, iDiv, Truth[i] );
368 Vec_WrdPush( vDivTruths, Truth[i] );
369 }
370 Vec_IntForEachEntryStart( vDivs, iDiv, i, nVars )
371 {
372 pObj = Gia_ManObj( p, iDiv );
373 Truth0 = Vec_WrdEntry( vTruths, Gia_ObjFaninId0(pObj, iDiv) );
374 Truth1 = Vec_WrdEntry( vTruths, Gia_ObjFaninId1(pObj, iDiv) );
375 if ( Gia_ObjFaninC0(pObj) )
376 Truth0 = ~Truth0;
377 if ( Gia_ObjFaninC1(pObj) )
378 Truth1 = ~Truth1;
379 Vec_WrdWriteEntry( vTruths, iDiv, Truth0 & Truth1 );
380 Vec_WrdPush( vDivTruths, Truth0 & Truth1 );
381
382 // Truthh = Truth0 & Truth1;
383 // Abc_TtPrintBinary( &Truthh, nVars ); //printf( "\n" );
384 // Kit_DsdPrintFromTruth( &Truthh, nVars ); printf( "\n" );
385 }
386 // printf( "\n" );
387 }
388
389
390 /**Function*************************************************************
391
392 Synopsis []
393
394 Description []
395
396 SideEffects []
397
398 SeeAlso []
399
400 ***********************************************************************/
Gia_ManMapShrink6(Gia_Man_t * p,int nFanoutMax,int fKeepLevel,int fVerbose)401 Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int nFanoutMax, int fKeepLevel, int fVerbose )
402 {
403 Shr_Man_t * pMan;
404 Gia_Obj_t * pObj, * pFanin;
405 word uTruth, uTruth0, uTruth1;
406 int i, k, nDivs, iNode;
407 int RetValue, Counter1 = 0, Counter2 = 0;
408 abctime clk2, clk = Abc_Clock();
409 abctime timeFanout = 0;
410 assert( Gia_ManHasMapping(p) );
411 pMan = Shr_ManAlloc( p );
412 Gia_ManFillValue( p );
413 Gia_ManConst0(p)->Value = 0;
414 Gia_ManForEachObj1( p, pObj, i )
415 {
416 if ( Gia_ObjIsCi(pObj) )
417 {
418 pObj->Value = Gia_ManAppendCi( pMan->pNew );
419 if ( p->vLevels )
420 Gia_ObjSetLevel( pMan->pNew, Gia_ObjFromLit(pMan->pNew, Gia_ObjValue(pObj)), Gia_ObjLevel(p, pObj) );
421 }
422 else if ( Gia_ObjIsCo(pObj) )
423 {
424 pObj->Value = Gia_ManAppendCo( pMan->pNew, Gia_ObjFanin0Copy(pObj) );
425 }
426 else if ( Gia_ObjIsLut(p, i) )
427 {
428 // collect leaves of this gate
429 Vec_IntClear( pMan->vLeaves );
430 Gia_LutForEachFanin( p, i, iNode, k )
431 Vec_IntPush( pMan->vLeaves, iNode );
432 assert( Vec_IntSize(pMan->vLeaves) <= 6 );
433 // compute truth table
434 uTruth = Shr_ManComputeTruth6( pMan->pGia, pObj, pMan->vLeaves, pMan->vTruths );
435 assert( pObj->Value == ~0 );
436 if ( uTruth == 0 || ~uTruth == 0 )
437 pObj->Value = Abc_LitNotCond( 0, ~uTruth == 0 );
438 else
439 Gia_ManForEachObjVec( pMan->vLeaves, p, pFanin, k )
440 if ( uTruth == Truth[k] || ~uTruth == Truth[k] )
441 pObj->Value = Abc_LitNotCond( pFanin->Value, ~uTruth == Truth[k] );
442 if ( pObj->Value != ~0 )
443 continue;
444 // translate into new nodes
445 Gia_ManForEachObjVec( pMan->vLeaves, p, pFanin, k )
446 {
447 if ( Abc_LitIsCompl(pFanin->Value) )
448 uTruth = ((uTruth & Truth[k]) >> (1 << k)) | ((uTruth & ~Truth[k]) << (1 << k));
449 Vec_IntWriteEntry( pMan->vLeaves, k, Abc_Lit2Var(pFanin->Value) );
450 }
451 // compute divisors
452 clk2 = Abc_Clock();
453 nDivs = Shr_ManCollectDivisors( pMan, pMan->vLeaves, pMan->nDivMax, nFanoutMax );
454 assert( nDivs <= pMan->nDivMax );
455 timeFanout += Abc_Clock() - clk2;
456 // compute truth tables
457 Shr_ManComputeTruths( pMan->pNew, Vec_IntSize(pMan->vLeaves), pMan->vDivs, pMan->vDivTruths, pMan->vTruths );
458 // perform resubstitution
459 RetValue = Rsb_ManPerformResub6( pMan->pManRsb, Vec_IntSize(pMan->vLeaves), uTruth, pMan->vDivTruths, &uTruth0, &uTruth1, 0 );
460 if ( RetValue ) // resub exists
461 {
462 Vec_Int_t * vResult = Rsb_ManGetFanins(pMan->pManRsb);
463 Vec_IntClear( pMan->vDivResub );
464 Vec_IntForEachEntry( vResult, iNode, k )
465 Vec_IntPush( pMan->vDivResub, Vec_IntEntry(pMan->vDivs, iNode) );
466 pObj->Value = Shr_ObjPerformBidec( pMan, pMan->pManDec, pMan->pNew, pMan->vDivResub, uTruth1, uTruth0 | uTruth1 );
467 Counter1++;
468 }
469 else
470 {
471 pObj->Value = Shr_ObjPerformBidec( pMan, pMan->pManDec, pMan->pNew, pMan->vLeaves, uTruth, ~(word)0 );
472 Counter2++;
473 }
474 }
475 }
476 if ( fVerbose )
477 {
478 printf( "Performed %d resubs and %d decomps. ", Counter1, Counter2 );
479 printf( "Gain in AIG nodes = %d. ", Gia_ManObjNum(p)-Gia_ManObjNum(pMan->pNew) );
480 ABC_PRT( "Runtime", Abc_Clock() - clk );
481 // ABC_PRT( "Divisors", timeFanout );
482 }
483 return Shr_ManFree( pMan );
484 }
485
486 ////////////////////////////////////////////////////////////////////////
487 /// END OF FILE ///
488 ////////////////////////////////////////////////////////////////////////
489
490
491 ABC_NAMESPACE_IMPL_END
492
493