1 /**CFile****************************************************************
2
3 FileName [giaHash.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Structural hashing.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: giaHash.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Returns the place where this node is stored (or should be stored).]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Gia_ManHashOne(int iLit0,int iLit1,int iLitC,int TableSize)45 static inline int Gia_ManHashOne( int iLit0, int iLit1, int iLitC, int TableSize )
46 {
47 unsigned Key = iLitC * 2011;
48 Key += Abc_Lit2Var(iLit0) * 7937;
49 Key += Abc_Lit2Var(iLit1) * 2971;
50 Key += Abc_LitIsCompl(iLit0) * 911;
51 Key += Abc_LitIsCompl(iLit1) * 353;
52 return (int)(Key % TableSize);
53 }
Gia_ManHashFind(Gia_Man_t * p,int iLit0,int iLit1,int iLitC)54 static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1, int iLitC )
55 {
56 int iThis, * pPlace = Vec_IntEntryP( &p->vHTable, Gia_ManHashOne( iLit0, iLit1, iLitC, Vec_IntSize(&p->vHTable) ) );
57 assert( Vec_IntSize(&p->vHash) == Gia_ManObjNum(p) );
58 assert( p->pMuxes || iLit0 < iLit1 );
59 assert( iLit0 < iLit1 || (!Abc_LitIsCompl(iLit0) && !Abc_LitIsCompl(iLit1)) );
60 assert( iLitC == -1 || !Abc_LitIsCompl(iLit1) );
61 for ( ; (iThis = *pPlace); pPlace = Vec_IntEntryP(&p->vHash, iThis) )
62 {
63 Gia_Obj_t * pThis = Gia_ManObj( p, iThis );
64 if ( Gia_ObjFaninLit0(pThis, iThis) == iLit0 && Gia_ObjFaninLit1(pThis, iThis) == iLit1 && (p->pMuxes == NULL || Gia_ObjFaninLit2p(p, pThis) == iLitC) )
65 break;
66 }
67 return pPlace;
68 }
69
70 /**Function*************************************************************
71
72 Synopsis []
73
74 Description []
75
76 SideEffects []
77
78 SeeAlso []
79
80 ***********************************************************************/
Gia_ManHashLookupInt(Gia_Man_t * p,int iLit0,int iLit1)81 int Gia_ManHashLookupInt( Gia_Man_t * p, int iLit0, int iLit1 )
82 {
83 if ( iLit0 > iLit1 )
84 iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
85 return Abc_Var2Lit( *Gia_ManHashFind( p, iLit0, iLit1, -1 ), 0 );
86 }
Gia_ManHashLookup(Gia_Man_t * p,Gia_Obj_t * p0,Gia_Obj_t * p1)87 int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 )
88 {
89 int iLit0 = Gia_ObjToLit( p, p0 );
90 int iLit1 = Gia_ObjToLit( p, p1 );
91 return Gia_ManHashLookupInt( p, iLit0, iLit1 );
92 }
93
94 /**Function*************************************************************
95
96 Synopsis [Starts the hash table.]
97
98 Description []
99
100 SideEffects []
101
102 SeeAlso []
103
104 ***********************************************************************/
Gia_ManHashAlloc(Gia_Man_t * p)105 void Gia_ManHashAlloc( Gia_Man_t * p )
106 {
107 assert( Vec_IntSize(&p->vHTable) == 0 );
108 Vec_IntFill( &p->vHTable, Abc_PrimeCudd( Gia_ManAndNum(p) ? Gia_ManAndNum(p) + 1000 : p->nObjsAlloc ), 0 );
109 Vec_IntGrow( &p->vHash, Abc_MaxInt(Vec_IntSize(&p->vHTable), Gia_ManObjNum(p)) );
110 Vec_IntFill( &p->vHash, Gia_ManObjNum(p), 0 );
111 //printf( "Alloced table with %d entries.\n", Vec_IntSize(&p->vHTable) );
112 }
113
114 /**Function*************************************************************
115
116 Synopsis [Starts the hash table.]
117
118 Description []
119
120 SideEffects []
121
122 SeeAlso []
123
124 ***********************************************************************/
Gia_ManHashStart(Gia_Man_t * p)125 void Gia_ManHashStart( Gia_Man_t * p )
126 {
127 Gia_Obj_t * pObj;
128 int * pPlace, i;
129 Gia_ManHashAlloc( p );
130 Gia_ManForEachAnd( p, pObj, i )
131 {
132 pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i), Gia_ObjFaninLit2(p, i) );
133 assert( *pPlace == 0 );
134 *pPlace = i;
135 }
136 }
137
138 /**Function*************************************************************
139
140 Synopsis [Stops the hash table.]
141
142 Description []
143
144 SideEffects []
145
146 SeeAlso []
147
148 ***********************************************************************/
Gia_ManHashStop(Gia_Man_t * p)149 void Gia_ManHashStop( Gia_Man_t * p )
150 {
151 Vec_IntErase( &p->vHTable );
152 Vec_IntErase( &p->vHash );
153 }
154
155 /**Function*************************************************************
156
157 Synopsis [Resizes the hash table.]
158
159 Description []
160
161 SideEffects []
162
163 SeeAlso []
164
165 ***********************************************************************/
Gia_ManHashResize(Gia_Man_t * p)166 void Gia_ManHashResize( Gia_Man_t * p )
167 {
168 int i, iThis, iNext, Counter, Counter2, * pPlace;
169 Vec_Int_t vOld = p->vHTable;
170 assert( Vec_IntSize(&vOld) > 0 );
171 // replace the table
172 Vec_IntZero( &p->vHTable );
173 Vec_IntFill( &p->vHTable, Abc_PrimeCudd( 2 * Gia_ManAndNum(p) ), 0 );
174 // rehash the entries from the old table
175 Counter = 0;
176 Vec_IntForEachEntry( &vOld, iThis, i )
177 for ( iNext = Vec_IntEntry(&p->vHash, iThis);
178 iThis; iThis = iNext,
179 iNext = Vec_IntEntry(&p->vHash, iThis) )
180 {
181 Gia_Obj_t * pThis0 = Gia_ManObj( p, iThis );
182 Vec_IntWriteEntry( &p->vHash, iThis, 0 );
183 pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0(pThis0, iThis), Gia_ObjFaninLit1(pThis0, iThis), Gia_ObjFaninLit2p(p, pThis0) );
184 assert( *pPlace == 0 ); // should not be there
185 *pPlace = iThis;
186 assert( *pPlace != 0 );
187 Counter++;
188 }
189 Counter2 = Gia_ManAndNum(p) - Gia_ManBufNum(p);
190 assert( Counter == Counter2 );
191 // if ( p->fVerbose )
192 // printf( "Resizing GIA hash table: %d -> %d.\n", Vec_IntSize(&vOld), Vec_IntSize(&p->vHTable) );
193 Vec_IntErase( &vOld );
194 }
195
196 /**Function********************************************************************
197
198 Synopsis [Profiles the hash table.]
199
200 Description []
201
202 SideEffects []
203
204 SeeAlso []
205
206 ******************************************************************************/
Gia_ManHashProfile(Gia_Man_t * p)207 void Gia_ManHashProfile( Gia_Man_t * p )
208 {
209 int iEntry;
210 int i, Counter, Limit;
211 printf( "Table size = %d. Entries = %d. ", Vec_IntSize(&p->vHTable), Gia_ManAndNum(p) );
212 printf( "Hits = %d. Misses = %d.\n", (int)p->nHashHit, (int)p->nHashMiss );
213 Limit = Abc_MinInt( 1000, Vec_IntSize(&p->vHTable) );
214 for ( i = 0; i < Limit; i++ )
215 {
216 Counter = 0;
217 for ( iEntry = Vec_IntEntry(&p->vHTable, i);
218 iEntry;
219 iEntry = iEntry? Vec_IntEntry(&p->vHash, iEntry) : 0 )
220 Counter++;
221 if ( Counter )
222 printf( "%d ", Counter );
223 }
224 printf( "\n" );
225 }
226
227 /**Function*************************************************************
228
229 Synopsis [Recognizes what nodes are control and data inputs of a MUX.]
230
231 Description [If the node is a MUX, returns the control variable C.
232 Assigns nodes T and E to be the then and else variables of the MUX.
233 Node C is never complemented. Nodes T and E can be complemented.
234 This function also recognizes EXOR/NEXOR gates as MUXes.]
235
236 SideEffects []
237
238 SeeAlso []
239
240 ***********************************************************************/
Gia_ObjRecognizeMuxTwo(Gia_Obj_t * pNode0,Gia_Obj_t * pNode1,Gia_Obj_t ** ppNodeT,Gia_Obj_t ** ppNodeE)241 static inline Gia_Obj_t * Gia_ObjRecognizeMuxTwo( Gia_Obj_t * pNode0, Gia_Obj_t * pNode1, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE )
242 {
243 assert( !Gia_IsComplement(pNode0) );
244 assert( !Gia_IsComplement(pNode1) );
245 // find the control variable
246 if ( Gia_ObjFanin1(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC1(pNode1)) )
247 {
248 // if ( FrGia_IsComplement(pNode1->p2) )
249 if ( Gia_ObjFaninC1(pNode0) )
250 { // pNode2->p2 is positive phase of C
251 *ppNodeT = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
252 *ppNodeE = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
253 return Gia_ObjChild1(pNode1);//pNode2->p2;
254 }
255 else
256 { // pNode1->p2 is positive phase of C
257 *ppNodeT = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
258 *ppNodeE = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
259 return Gia_ObjChild1(pNode0);//pNode1->p2;
260 }
261 }
262 else if ( Gia_ObjFanin0(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC0(pNode1)) )
263 {
264 // if ( FrGia_IsComplement(pNode1->p1) )
265 if ( Gia_ObjFaninC0(pNode0) )
266 { // pNode2->p1 is positive phase of C
267 *ppNodeT = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
268 *ppNodeE = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
269 return Gia_ObjChild0(pNode1);//pNode2->p1;
270 }
271 else
272 { // pNode1->p1 is positive phase of C
273 *ppNodeT = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
274 *ppNodeE = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
275 return Gia_ObjChild0(pNode0);//pNode1->p1;
276 }
277 }
278 else if ( Gia_ObjFanin0(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC1(pNode1)) )
279 {
280 // if ( FrGia_IsComplement(pNode1->p1) )
281 if ( Gia_ObjFaninC0(pNode0) )
282 { // pNode2->p2 is positive phase of C
283 *ppNodeT = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
284 *ppNodeE = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
285 return Gia_ObjChild1(pNode1);//pNode2->p2;
286 }
287 else
288 { // pNode1->p1 is positive phase of C
289 *ppNodeT = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
290 *ppNodeE = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
291 return Gia_ObjChild0(pNode0);//pNode1->p1;
292 }
293 }
294 else if ( Gia_ObjFanin1(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC0(pNode1)) )
295 {
296 // if ( FrGia_IsComplement(pNode1->p2) )
297 if ( Gia_ObjFaninC1(pNode0) )
298 { // pNode2->p1 is positive phase of C
299 *ppNodeT = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
300 *ppNodeE = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
301 return Gia_ObjChild0(pNode1);//pNode2->p1;
302 }
303 else
304 { // pNode1->p2 is positive phase of C
305 *ppNodeT = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
306 *ppNodeE = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
307 return Gia_ObjChild1(pNode0);//pNode1->p2;
308 }
309 }
310 assert( 0 ); // this is not MUX
311 return NULL;
312 }
313
314
315 /**Function*************************************************************
316
317 Synopsis [Rehashes AIG with mapping.]
318
319 Description []
320
321 SideEffects []
322
323 SeeAlso []
324
325 ***********************************************************************/
Gia_ManHashAndP(Gia_Man_t * p,Gia_Obj_t * p0,Gia_Obj_t * p1)326 static inline Gia_Obj_t * Gia_ManHashAndP( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 )
327 {
328 return Gia_ObjFromLit( p, Gia_ManHashAnd( p, Gia_ObjToLit(p, p0), Gia_ObjToLit(p, p1) ) );
329 }
330
331 /**Function*************************************************************
332
333 Synopsis [Rehashes AIG with mapping.]
334
335 Description [http://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf]
336
337 SideEffects []
338
339 SeeAlso []
340
341 ***********************************************************************/
Gia_ManAddStrash(Gia_Man_t * p,Gia_Obj_t * p0,Gia_Obj_t * p1)342 static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 )
343 {
344 Gia_Obj_t * pNode0, * pNode1, * pFanA, * pFanB, * pFanC, * pFanD;
345 assert( p->fAddStrash );
346 pNode0 = Gia_Regular(p0);
347 pNode1 = Gia_Regular(p1);
348 if ( !Gia_ObjIsAnd(pNode0) && !Gia_ObjIsAnd(pNode1) )
349 return NULL;
350 pFanA = Gia_ObjIsAnd(pNode0) ? Gia_ObjChild0(pNode0) : NULL;
351 pFanB = Gia_ObjIsAnd(pNode0) ? Gia_ObjChild1(pNode0) : NULL;
352 pFanC = Gia_ObjIsAnd(pNode1) ? Gia_ObjChild0(pNode1) : NULL;
353 pFanD = Gia_ObjIsAnd(pNode1) ? Gia_ObjChild1(pNode1) : NULL;
354 if ( Gia_IsComplement(p0) )
355 {
356 if ( pFanA == Gia_Not(p1) || pFanB == Gia_Not(p1) )
357 return p1;
358 if ( pFanB == p1 )
359 return Gia_ManHashAndP( p, Gia_Not(pFanA), pFanB );
360 if ( pFanA == p1 )
361 return Gia_ManHashAndP( p, Gia_Not(pFanB), pFanA );
362 }
363 else
364 {
365 if ( pFanA == Gia_Not(p1) || pFanB == Gia_Not(p1) )
366 return Gia_ManConst0(p);
367 if ( pFanA == p1 || pFanB == p1 )
368 return p0;
369 }
370 if ( Gia_IsComplement(p1) )
371 {
372 if ( pFanC == Gia_Not(p0) || pFanD == Gia_Not(p0) )
373 return p0;
374 if ( pFanD == p0 )
375 return Gia_ManHashAndP( p, Gia_Not(pFanC), pFanD );
376 if ( pFanC == p0 )
377 return Gia_ManHashAndP( p, Gia_Not(pFanD), pFanC );
378 }
379 else
380 {
381 if ( pFanC == Gia_Not(p0) || pFanD == Gia_Not(p0) )
382 return Gia_ManConst0(p);
383 if ( pFanC == p0 || pFanD == p0 )
384 return p1;
385 }
386 if ( !Gia_IsComplement(p0) && !Gia_IsComplement(p1) )
387 {
388 if ( pFanA == Gia_Not(pFanC) || pFanA == Gia_Not(pFanD) || pFanB == Gia_Not(pFanC) || pFanB == Gia_Not(pFanD) )
389 return Gia_ManConst0(p);
390 if ( pFanA == pFanC || pFanB == pFanC )
391 return Gia_ManHashAndP( p, p0, pFanD );
392 if ( pFanB == pFanC || pFanB == pFanD )
393 return Gia_ManHashAndP( p, pFanA, p1 );
394 if ( pFanA == pFanD || pFanB == pFanD )
395 return Gia_ManHashAndP( p, p0, pFanC );
396 if ( pFanA == pFanC || pFanA == pFanD )
397 return Gia_ManHashAndP( p, pFanB, p1 );
398 }
399 else if ( Gia_IsComplement(p0) && !Gia_IsComplement(p1) )
400 {
401 if ( pFanA == Gia_Not(pFanC) || pFanA == Gia_Not(pFanD) || pFanB == Gia_Not(pFanC) || pFanB == Gia_Not(pFanD) )
402 return p1;
403 if ( pFanB == pFanC || pFanB == pFanD )
404 return Gia_ManHashAndP( p, Gia_Not(pFanA), p1 );
405 if ( pFanA == pFanC || pFanA == pFanD )
406 return Gia_ManHashAndP( p, Gia_Not(pFanB), p1 );
407 }
408 else if ( !Gia_IsComplement(p0) && Gia_IsComplement(p1) )
409 {
410 if ( pFanC == Gia_Not(pFanA) || pFanC == Gia_Not(pFanB) || pFanD == Gia_Not(pFanA) || pFanD == Gia_Not(pFanB) )
411 return p0;
412 if ( pFanD == pFanA || pFanD == pFanB )
413 return Gia_ManHashAndP( p, Gia_Not(pFanC), p0 );
414 if ( pFanC == pFanA || pFanC == pFanB )
415 return Gia_ManHashAndP( p, Gia_Not(pFanD), p0 );
416 }
417 else // if ( Gia_IsComplement(p0) && Gia_IsComplement(p1) )
418 {
419 if ( pFanA == pFanD && pFanB == Gia_Not(pFanC) )
420 return Gia_Not(pFanA);
421 if ( pFanB == pFanC && pFanA == Gia_Not(pFanD) )
422 return Gia_Not(pFanB);
423 if ( pFanA == pFanC && pFanB == Gia_Not(pFanD) )
424 return Gia_Not(pFanA);
425 if ( pFanB == pFanD && pFanA == Gia_Not(pFanC) )
426 return Gia_Not(pFanB);
427 }
428 /*
429 if ( !Gia_IsComplement(p0) || !Gia_IsComplement(p1) )
430 return NULL;
431 if ( !Gia_ObjIsAnd(pNode0) || !Gia_ObjIsAnd(pNode1) )
432 return NULL;
433 if ( (Gia_ObjFanin0(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC0(pNode1))) ||
434 (Gia_ObjFanin0(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC1(pNode1))) ||
435 (Gia_ObjFanin1(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC0(pNode1))) ||
436 (Gia_ObjFanin1(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC1(pNode1))) )
437 {
438 Gia_Obj_t * pNodeC, * pNodeT, * pNodeE;
439 int fCompl;
440 pNodeC = Gia_ObjRecognizeMuxTwo( pNode0, pNode1, &pNodeT, &pNodeE );
441 // using non-standard canonical rule for MUX (d0 is not compl; d1 may be compl)
442 if ( (fCompl = Gia_IsComplement(pNodeE)) )
443 {
444 pNodeE = Gia_Not(pNodeE);
445 pNodeT = Gia_Not(pNodeT);
446 }
447 pNode0 = Gia_ManHashAndP( p, Gia_Not(pNodeC), pNodeE );
448 pNode1 = Gia_ManHashAndP( p, pNodeC, pNodeT );
449 p->fAddStrash = 0;
450 pNodeC = Gia_NotCond( Gia_ManHashAndP( p, Gia_Not(pNode0), Gia_Not(pNode1) ), !fCompl );
451 p->fAddStrash = 1;
452 return pNodeC;
453 }
454 */
455 return NULL;
456 }
457
458 /**Function*************************************************************
459
460 Synopsis [Hashes XOR gate.]
461
462 Description []
463
464 SideEffects []
465
466 SeeAlso []
467
468 ***********************************************************************/
Gia_ManHashXorReal(Gia_Man_t * p,int iLit0,int iLit1)469 int Gia_ManHashXorReal( Gia_Man_t * p, int iLit0, int iLit1 )
470 {
471 int fCompl = 0;
472 assert( p->fAddStrash == 0 );
473 if ( iLit0 < 2 )
474 return iLit0 ? Abc_LitNot(iLit1) : iLit1;
475 if ( iLit1 < 2 )
476 return iLit1 ? Abc_LitNot(iLit0) : iLit0;
477 if ( iLit0 == iLit1 )
478 return 0;
479 if ( iLit0 == Abc_LitNot(iLit1) )
480 return 1;
481 if ( (p->nObjs & 0xFF) == 0 && 2 * Vec_IntSize(&p->vHTable) < Gia_ManAndNum(p) )
482 Gia_ManHashResize( p );
483 if ( iLit0 < iLit1 )
484 iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
485 if ( Abc_LitIsCompl(iLit0) )
486 iLit0 = Abc_LitNot(iLit0), fCompl ^= 1;
487 if ( Abc_LitIsCompl(iLit1) )
488 iLit1 = Abc_LitNot(iLit1), fCompl ^= 1;
489 {
490 int *pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
491 if ( *pPlace )
492 {
493 p->nHashHit++;
494 return Abc_Var2Lit( *pPlace, fCompl );
495 }
496 p->nHashMiss++;
497 if ( Vec_IntSize(&p->vHash) < Vec_IntCap(&p->vHash) )
498 *pPlace = Abc_Lit2Var( Gia_ManAppendXorReal( p, iLit0, iLit1 ) );
499 else
500 {
501 int iNode = Gia_ManAppendXorReal( p, iLit0, iLit1 );
502 pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
503 assert( *pPlace == 0 );
504 *pPlace = Abc_Lit2Var( iNode );
505 }
506 return Abc_Var2Lit( *pPlace, fCompl );
507 }
508 }
509
510 /**Function*************************************************************
511
512 Synopsis [Hashes MUX gate.]
513
514 Description []
515
516 SideEffects []
517
518 SeeAlso []
519
520 ***********************************************************************/
Gia_ManHashMuxReal(Gia_Man_t * p,int iLitC,int iLit1,int iLit0)521 int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 )
522 {
523 int fCompl = 0;
524 assert( p->fAddStrash == 0 );
525 if ( iLitC < 2 )
526 return iLitC ? iLit1 : iLit0;
527 if ( iLit0 < 2 )
528 return iLit0 ? Gia_ManHashOr(p, Abc_LitNot(iLitC), iLit1) : Gia_ManHashAnd(p, iLitC, iLit1);
529 if ( iLit1 < 2 )
530 return iLit1 ? Gia_ManHashOr(p, iLitC, iLit0) : Gia_ManHashAnd(p, Abc_LitNot(iLitC), iLit0);
531 assert( iLit0 > 1 && iLit1 > 1 && iLitC > 1 );
532 if ( iLit0 == iLit1 )
533 return iLit0;
534 if ( iLitC == iLit0 || iLitC == Abc_LitNot(iLit1) )
535 return Gia_ManHashAnd(p, iLit0, iLit1);
536 if ( iLitC == iLit1 || iLitC == Abc_LitNot(iLit0) )
537 return Gia_ManHashOr(p, iLit0, iLit1);
538 if ( Abc_Lit2Var(iLit0) == Abc_Lit2Var(iLit1) )
539 return Gia_ManHashXorReal( p, iLitC, iLit0 );
540 if ( iLit0 > iLit1 )
541 iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1, iLitC = Abc_LitNot(iLitC);
542 if ( Abc_LitIsCompl(iLit1) )
543 iLit0 = Abc_LitNot(iLit0), iLit1 = Abc_LitNot(iLit1), fCompl = 1;
544 {
545 int *pPlace = Gia_ManHashFind( p, iLit0, iLit1, iLitC );
546 if ( *pPlace )
547 {
548 p->nHashHit++;
549 return Abc_Var2Lit( *pPlace, fCompl );
550 }
551 p->nHashMiss++;
552 if ( Vec_IntSize(&p->vHash) < Vec_IntCap(&p->vHash) )
553 *pPlace = Abc_Lit2Var( Gia_ManAppendMuxReal( p, iLitC, iLit1, iLit0 ) );
554 else
555 {
556 int iNode = Gia_ManAppendMuxReal( p, iLitC, iLit1, iLit0 );
557 pPlace = Gia_ManHashFind( p, iLit0, iLit1, iLitC );
558 assert( *pPlace == 0 );
559 *pPlace = Abc_Lit2Var( iNode );
560 }
561 return Abc_Var2Lit( *pPlace, fCompl );
562 }
563 }
564
565 /**Function*************************************************************
566
567 Synopsis [Hashes AND gate.]
568
569 Description []
570
571 SideEffects []
572
573 SeeAlso []
574
575 ***********************************************************************/
Gia_ManHashAnd(Gia_Man_t * p,int iLit0,int iLit1)576 int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
577 {
578 if ( iLit0 < 2 )
579 return iLit0 ? iLit1 : 0;
580 if ( iLit1 < 2 )
581 return iLit1 ? iLit0 : 0;
582 if ( iLit0 == iLit1 )
583 return iLit1;
584 if ( iLit0 == Abc_LitNot(iLit1) )
585 return 0;
586 if ( p->fGiaSimple )
587 {
588 assert( Vec_IntSize(&p->vHTable) == 0 );
589 return Gia_ManAppendAnd( p, iLit0, iLit1 );
590 }
591 if ( (p->nObjs & 0xFF) == 0 && 2 * Vec_IntSize(&p->vHTable) < Gia_ManAndNum(p) )
592 Gia_ManHashResize( p );
593 if ( p->fAddStrash )
594 {
595 Gia_Obj_t * pObj = Gia_ManAddStrash( p, Gia_ObjFromLit(p, iLit0), Gia_ObjFromLit(p, iLit1) );
596 if ( pObj != NULL )
597 return Gia_ObjToLit( p, pObj );
598 }
599 if ( iLit0 > iLit1 )
600 iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
601 {
602 int * pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
603 if ( *pPlace )
604 {
605 p->nHashHit++;
606 return Abc_Var2Lit( *pPlace, 0 );
607 }
608 p->nHashMiss++;
609 if ( Vec_IntSize(&p->vHash) < Vec_IntCap(&p->vHash) )
610 *pPlace = Abc_Lit2Var( Gia_ManAppendAnd( p, iLit0, iLit1 ) );
611 else
612 {
613 int iNode = Gia_ManAppendAnd( p, iLit0, iLit1 );
614 pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
615 assert( *pPlace == 0 );
616 *pPlace = Abc_Lit2Var( iNode );
617 }
618 return Abc_Var2Lit( *pPlace, 0 );
619 }
620 }
Gia_ManHashOr(Gia_Man_t * p,int iLit0,int iLit1)621 int Gia_ManHashOr( Gia_Man_t * p, int iLit0, int iLit1 )
622 {
623 return Abc_LitNot(Gia_ManHashAnd( p, Abc_LitNot(iLit0), Abc_LitNot(iLit1) ));
624 }
625
626 /**Function*************************************************************
627
628 Synopsis []
629
630 Description []
631
632 SideEffects []
633
634 SeeAlso []
635
636 ***********************************************************************/
Gia_ManHashAndTry(Gia_Man_t * p,int iLit0,int iLit1)637 int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 )
638 {
639 if ( iLit0 < 2 )
640 return iLit0 ? iLit1 : 0;
641 if ( iLit1 < 2 )
642 return iLit1 ? iLit0 : 0;
643 if ( iLit0 == iLit1 )
644 return iLit1;
645 if ( iLit0 == Abc_LitNot(iLit1) )
646 return 0;
647 if ( iLit0 > iLit1 )
648 iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
649 {
650 int * pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
651 if ( *pPlace )
652 return Abc_Var2Lit( *pPlace, 0 );
653 return -1;
654 }
655 }
656
657 /**Function*************************************************************
658
659 Synopsis []
660
661 Description []
662
663 SideEffects []
664
665 SeeAlso []
666
667 ***********************************************************************/
Gia_ManHashXor(Gia_Man_t * p,int iLit0,int iLit1)668 int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
669 {
670 if ( p->fGiaSimple )
671 return Gia_ManHashOr(p, Gia_ManHashAnd(p, iLit0, Abc_LitNot(iLit1)), Gia_ManHashAnd(p, Abc_LitNot(iLit0), iLit1) );
672 else
673 {
674 int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1);
675 int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) );
676 int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) );
677 return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
678 }
679 }
680
681 /**Function*************************************************************
682
683 Synopsis []
684
685 Description []
686
687 SideEffects []
688
689 SeeAlso []
690
691 ***********************************************************************/
Gia_ManHashMux(Gia_Man_t * p,int iCtrl,int iData1,int iData0)692 int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
693 {
694 if ( p->fGiaSimple )
695 return Gia_ManHashOr(p, Gia_ManHashAnd(p, iCtrl, iData1), Gia_ManHashAnd(p, Abc_LitNot(iCtrl), iData0) );
696 else
697 {
698 int iTemp0, iTemp1, fCompl = 0;
699 if ( iData0 > iData1 )
700 iData0 ^= iData1, iData1 ^= iData0, iData0 ^= iData1, iCtrl = Abc_LitNot(iCtrl);
701 if ( Abc_LitIsCompl(iData1) )
702 iData0 = Abc_LitNot(iData0), iData1 = Abc_LitNot(iData1), fCompl = 1;
703 iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 );
704 iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 );
705 return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
706 }
707 }
708
709 /**Function*************************************************************
710
711 Synopsis []
712
713 Description []
714
715 SideEffects []
716
717 SeeAlso []
718
719 ***********************************************************************/
Gia_ManHashMaj(Gia_Man_t * p,int iData0,int iData1,int iData2)720 int Gia_ManHashMaj( Gia_Man_t * p, int iData0, int iData1, int iData2 )
721 {
722 int iTemp0 = Gia_ManHashOr( p, iData1, iData2 );
723 int iTemp1 = Gia_ManHashAnd( p, iData0, iTemp0 );
724 int iTemp2 = Gia_ManHashAnd( p, iData1, iData2 );
725 return Gia_ManHashOr( p, iTemp1, iTemp2 );
726 }
727
728 /**Function*************************************************************
729
730 Synopsis [Rehashes AIG.]
731
732 Description []
733
734 SideEffects []
735
736 SeeAlso []
737
738 ***********************************************************************/
Gia_ManRehash(Gia_Man_t * p,int fAddStrash)739 Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash )
740 {
741 Gia_Man_t * pNew, * pTemp;
742 Gia_Obj_t * pObj;
743 int i;
744 pNew = Gia_ManStart( Gia_ManObjNum(p) );
745 pNew->pName = Abc_UtilStrsav( p->pName );
746 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
747 pNew->fAddStrash = fAddStrash;
748 Gia_ManHashAlloc( pNew );
749 Gia_ManConst0(p)->Value = 0;
750 Gia_ManForEachObj( p, pObj, i )
751 {
752 //if ( Gia_ObjIsBuf(pObj) )
753 // pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
754 //else
755 if ( Gia_ObjIsAnd(pObj) )
756 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
757 else if ( Gia_ObjIsCi(pObj) )
758 pObj->Value = Gia_ManAppendCi( pNew );
759 else if ( Gia_ObjIsCo(pObj) )
760 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
761 }
762 Gia_ManHashStop( pNew );
763 pNew->fAddStrash = 0;
764 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
765 // printf( "Top gate is %s\n", Gia_ObjFaninC0(Gia_ManCo(pNew, 0))? "OR" : "AND" );
766 pNew = Gia_ManCleanup( pTemp = pNew );
767 Gia_ManStop( pTemp );
768 return pNew;
769 }
770
771
772 /**Function*************************************************************
773
774 Synopsis [Creates well-balanced AND gate.]
775
776 Description []
777
778 SideEffects []
779
780 SeeAlso []
781
782 ***********************************************************************/
Gia_ManHashAndMulti(Gia_Man_t * p,Vec_Int_t * vLits)783 int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits )
784 {
785 if ( Vec_IntSize(vLits) == 0 )
786 return 0;
787 while ( Vec_IntSize(vLits) > 1 )
788 {
789 int i, k = 0, Lit1, Lit2, LitRes;
790 Vec_IntForEachEntryDouble( vLits, Lit1, Lit2, i )
791 {
792 LitRes = Gia_ManHashAnd( p, Lit1, Lit2 );
793 Vec_IntWriteEntry( vLits, k++, LitRes );
794 }
795 if ( Vec_IntSize(vLits) & 1 )
796 Vec_IntWriteEntry( vLits, k++, Vec_IntEntryLast(vLits) );
797 Vec_IntShrink( vLits, k );
798 }
799 assert( Vec_IntSize(vLits) == 1 );
800 return Vec_IntEntry(vLits, 0);
801 }
Gia_ManHashAndMulti2(Gia_Man_t * p,Vec_Int_t * vLits)802 int Gia_ManHashAndMulti2( Gia_Man_t * p, Vec_Int_t * vLits )
803 {
804 int i, iLit, iRes = 1;
805 Vec_IntForEachEntry( vLits, iLit, i )
806 iRes = Gia_ManHashAnd( p, iRes, iLit );
807 return iRes;
808 }
Gia_ManHashDualMiter(Gia_Man_t * p,Vec_Int_t * vOuts)809 int Gia_ManHashDualMiter( Gia_Man_t * p, Vec_Int_t * vOuts )
810 {
811 int i, iLit0, iLit1, iRes = 0;
812 Vec_IntForEachEntryDouble( vOuts, iLit0, iLit1, i )
813 iRes = Gia_ManHashOr( p, iRes, Gia_ManHashXor(p, iLit0, iLit1) );
814 return iRes;
815 }
816
817 ////////////////////////////////////////////////////////////////////////
818 /// END OF FILE ///
819 ////////////////////////////////////////////////////////////////////////
820
821
822 ABC_NAMESPACE_IMPL_END
823
824