1 /**CFile****************************************************************
2
3 FileName [giaTruth.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Truth table computation.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: giaTruth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22 #include "misc/vec/vecMem.h"
23 #include "misc/vec/vecWec.h"
24 #include "misc/util/utilTruth.h"
25 #include "opt/dau/dau.h"
26
27 ABC_NAMESPACE_IMPL_START
28
29
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 static word s_Truth6[6] = {
35 ABC_CONST(0xAAAAAAAAAAAAAAAA),
36 ABC_CONST(0xCCCCCCCCCCCCCCCC),
37 ABC_CONST(0xF0F0F0F0F0F0F0F0),
38 ABC_CONST(0xFF00FF00FF00FF00),
39 ABC_CONST(0xFFFF0000FFFF0000),
40 ABC_CONST(0xFFFFFFFF00000000)
41 };
42
Gla_ObjTruthElem(Gia_Man_t * p,int i)43 static inline word * Gla_ObjTruthElem( Gia_Man_t * p, int i ) { return (word *)Vec_PtrEntry( p->vTtInputs, i ); }
Gla_ObjTruthNodeId(Gia_Man_t * p,int Id)44 static inline word * Gla_ObjTruthNodeId( Gia_Man_t * p, int Id ) { return Vec_WrdArray(p->vTtMemory) + p->nTtWords * Id; }
Gla_ObjTruthNode(Gia_Man_t * p,Gia_Obj_t * pObj)45 static inline word * Gla_ObjTruthNode( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_WrdArray(p->vTtMemory) + p->nTtWords * Gia_ObjNum(p, pObj); }
Gla_ObjTruthFree1(Gia_Man_t * p)46 static inline word * Gla_ObjTruthFree1( Gia_Man_t * p ) { return Vec_WrdArray(p->vTtMemory) + Vec_WrdSize(p->vTtMemory) - p->nTtWords * 1; }
Gla_ObjTruthFree2(Gia_Man_t * p)47 static inline word * Gla_ObjTruthFree2( Gia_Man_t * p ) { return Vec_WrdArray(p->vTtMemory) + Vec_WrdSize(p->vTtMemory) - p->nTtWords * 2; }
Gla_ObjTruthConst0(Gia_Man_t * p,word * pDst)48 static inline word * Gla_ObjTruthConst0( Gia_Man_t * p, word * pDst ) { int w; for ( w = 0; w < p->nTtWords; w++ ) pDst[w] = 0; return pDst; }
Gla_ObjTruthDup(Gia_Man_t * p,word * pDst,word * pSrc,int c)49 static inline word * Gla_ObjTruthDup( Gia_Man_t * p, word * pDst, word * pSrc, int c ) { int w; for ( w = 0; w < p->nTtWords; w++ ) pDst[w] = c ? ~pSrc[w] : pSrc[w]; return pDst; }
50
51 ////////////////////////////////////////////////////////////////////////
52 /// FUNCTION DEFINITIONS ///
53 ////////////////////////////////////////////////////////////////////////
54
55 /**Function*************************************************************
56
57 Synopsis [Compute truth table.]
58
59 Description []
60
61 SideEffects []
62
63 SeeAlso []
64
65 ***********************************************************************/
Gia_LutComputeTruth6Simple_rec(Gia_Man_t * p,int iObj)66 word Gia_LutComputeTruth6Simple_rec( Gia_Man_t * p, int iObj )
67 {
68 word Truth0, Truth1, Truth;
69 Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
70 if ( Gia_ObjIsConst0(pObj) )
71 return 0;
72 if ( Gia_ObjIsCi(pObj) )
73 return s_Truths6[Gia_ObjCioId(pObj)];
74 Truth0 = Gia_LutComputeTruth6Simple_rec( p, Gia_ObjFaninId0(pObj, iObj) );
75 Truth1 = Gia_LutComputeTruth6Simple_rec( p, Gia_ObjFaninId1(pObj, iObj) );
76 Truth0 = Gia_ObjFaninC0(pObj) ? ~Truth0 : Truth0;
77 Truth1 = Gia_ObjFaninC1(pObj) ? ~Truth1 : Truth1;
78 Truth = Gia_ObjIsXor(pObj) ? Truth0 ^ Truth1 : Truth0 & Truth1;
79 return Truth;
80 }
Gia_LutComputeTruth6Simple(Gia_Man_t * p,int iPo)81 word Gia_LutComputeTruth6Simple( Gia_Man_t * p, int iPo )
82 {
83 Gia_Obj_t * pObj = Gia_ManPo( p, iPo );
84 word Truth = Gia_LutComputeTruth6Simple_rec( p, Gia_ObjFaninId0p(p, pObj) );
85 return Gia_ObjFaninC0(pObj) ? ~Truth : Truth;
86
87 }
88
89 /**Function*************************************************************
90
91 Synopsis [Compute truth table.]
92
93 Description []
94
95 SideEffects []
96
97 SeeAlso []
98
99 ***********************************************************************/
Gia_LutComputeTruth6_rec(Gia_Man_t * p,int iNode,Vec_Wrd_t * vTruths)100 word Gia_LutComputeTruth6_rec( Gia_Man_t * p, int iNode, Vec_Wrd_t * vTruths )
101 {
102 Gia_Obj_t * pObj;
103 word Truth0, Truth1;
104 if ( Gia_ObjIsTravIdCurrentId(p, iNode) )
105 return Vec_WrdEntry(vTruths, iNode);
106 Gia_ObjSetTravIdCurrentId(p, iNode);
107 pObj = Gia_ManObj( p, iNode );
108 assert( Gia_ObjIsAnd(pObj) );
109 Truth0 = Gia_LutComputeTruth6_rec( p, Gia_ObjFaninId0p(p, pObj), vTruths );
110 Truth1 = Gia_LutComputeTruth6_rec( p, Gia_ObjFaninId1p(p, pObj), vTruths );
111 if ( Gia_ObjFaninC0(pObj) )
112 Truth0 = ~Truth0;
113 if ( Gia_ObjFaninC1(pObj) )
114 Truth1 = ~Truth1;
115 Vec_WrdWriteEntry( vTruths, iNode, Truth0 & Truth1 );
116 return Truth0 & Truth1;
117 }
Gia_LutComputeTruth6(Gia_Man_t * p,int iObj,Vec_Wrd_t * vTruths)118 word Gia_LutComputeTruth6( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTruths )
119 {
120 int k, iFan;
121 assert( Gia_ObjIsLut(p, iObj) );
122 Gia_ManIncrementTravId( p );
123 Gia_LutForEachFanin( p, iObj, iFan, k )
124 {
125 Vec_WrdWriteEntry( vTruths, iFan, s_Truths6[k] );
126 Gia_ObjSetTravIdCurrentId( p, iFan );
127 }
128 return Gia_LutComputeTruth6_rec( p, iObj, vTruths );
129 }
130
131 /**Function*************************************************************
132
133 Synopsis [Computes truth table of a 6-LUT.]
134
135 Description []
136
137 SideEffects []
138
139 SeeAlso []
140
141 ***********************************************************************/
Gia_ObjComputeTruthTable6Lut_rec(Gia_Man_t * p,int iObj,Vec_Wrd_t * vTemp)142 void Gia_ObjComputeTruthTable6Lut_rec( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp )
143 {
144 word uTruth0, uTruth1;
145 Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
146 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
147 return;
148 Gia_ObjSetTravIdCurrentId(p, iObj);
149 assert( Gia_ObjIsAnd(pObj) );
150 Gia_ObjComputeTruthTable6Lut_rec( p, Gia_ObjFaninId0p(p, pObj), vTemp );
151 Gia_ObjComputeTruthTable6Lut_rec( p, Gia_ObjFaninId1p(p, pObj), vTemp );
152 uTruth0 = Vec_WrdEntry( vTemp, Gia_ObjFaninId0p(p, pObj) );
153 uTruth0 = Gia_ObjFaninC0(pObj) ? ~uTruth0 : uTruth0;
154 uTruth1 = Vec_WrdEntry( vTemp, Gia_ObjFaninId1p(p, pObj) );
155 uTruth1 = Gia_ObjFaninC1(pObj) ? ~uTruth1 : uTruth1;
156 Vec_WrdWriteEntry( vTemp, iObj, uTruth0 & uTruth1 );
157 }
Gia_ObjComputeTruthTable6Lut(Gia_Man_t * p,int iObj,Vec_Wrd_t * vTemp)158 word Gia_ObjComputeTruthTable6Lut( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp )
159 {
160 int i, Fanin;
161 assert( Vec_WrdSize(vTemp) == Gia_ManObjNum(p) );
162 assert( Gia_ObjIsLut(p, iObj) );
163 Gia_ManIncrementTravId( p );
164 Gia_LutForEachFanin( p, iObj, Fanin, i )
165 {
166 Gia_ObjSetTravIdCurrentId( p, Fanin );
167 Vec_WrdWriteEntry( vTemp, Fanin, s_Truth6[i] );
168 }
169 assert( i <= 6 );
170 Gia_ObjComputeTruthTable6Lut_rec( p, iObj, vTemp );
171 return Vec_WrdEntry( vTemp, iObj );
172 }
173
174 /**Function*************************************************************
175
176 Synopsis [Computes truth table up to 6 inputs in terms of CIs.]
177
178 Description []
179
180 SideEffects []
181
182 SeeAlso []
183
184 ***********************************************************************/
Gia_ObjComputeTruth6(Gia_Man_t * p,int iObj,Vec_Int_t * vSupp,Vec_Wrd_t * vTemp)185 word Gia_ObjComputeTruth6( Gia_Man_t * p, int iObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTemp )
186 {
187 int i, Fanin;
188 assert( Vec_WrdSize(vTemp) == Gia_ManObjNum(p) );
189 assert( Vec_IntSize(vSupp) <= 6 );
190 Gia_ManIncrementTravId( p );
191 Vec_IntForEachEntry( vSupp, Fanin, i )
192 {
193 Gia_ObjSetTravIdCurrentId( p, Fanin );
194 Vec_WrdWriteEntry( vTemp, Fanin, s_Truth6[i] );
195 }
196 Gia_ObjComputeTruthTable6Lut_rec( p, iObj, vTemp );
197 return Vec_WrdEntry( vTemp, iObj );
198 }
Gia_ObjComputeTruth6CisSupport_rec(Gia_Man_t * p,int iObj,Vec_Int_t * vSupp)199 void Gia_ObjComputeTruth6CisSupport_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vSupp )
200 {
201 Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
202 if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
203 return;
204 Gia_ObjSetTravIdCurrentId(p, iObj);
205 if ( Gia_ObjIsCi(pObj) )
206 {
207 Vec_IntPushOrder( vSupp, iObj );
208 return;
209 }
210 assert( Gia_ObjIsAnd(pObj) );
211 Gia_ObjComputeTruth6CisSupport_rec( p, Gia_ObjFaninId0p(p, pObj), vSupp );
212 Gia_ObjComputeTruth6CisSupport_rec( p, Gia_ObjFaninId1p(p, pObj), vSupp );
213 }
Gia_ObjComputeTruth6Cis(Gia_Man_t * p,int iLit,Vec_Int_t * vSupp,Vec_Wrd_t * vTemp)214 word Gia_ObjComputeTruth6Cis( Gia_Man_t * p, int iLit, Vec_Int_t * vSupp, Vec_Wrd_t * vTemp )
215 {
216 int iObj = Abc_Lit2Var(iLit);
217 Vec_IntClear( vSupp );
218 if ( !iObj ) return Abc_LitIsCompl(iLit) ? ~(word)0 : (word)0;
219 Gia_ManIncrementTravId( p );
220 Gia_ObjComputeTruth6CisSupport_rec( p, iObj, vSupp );
221 if ( Vec_IntSize(vSupp) > 6 )
222 return 0;
223 Gia_ObjComputeTruth6( p, iObj, vSupp, vTemp );
224 return Abc_LitIsCompl(iLit) ? ~Vec_WrdEntry(vTemp, iObj) : Vec_WrdEntry(vTemp, iObj);
225 }
226
227 /**Function*************************************************************
228
229 Synopsis [Computes truth table up to 6 inputs.]
230
231 Description []
232
233 SideEffects []
234
235 SeeAlso []
236
237 ***********************************************************************/
Gia_ObjComputeTruthTable6_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Wrd_t * vTruths)238 void Gia_ObjComputeTruthTable6_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Wrd_t * vTruths )
239 {
240 word uTruth0, uTruth1;
241 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
242 return;
243 Gia_ObjSetTravIdCurrent(p, pObj);
244 assert( !pObj->fMark0 );
245 assert( Gia_ObjIsAnd(pObj) );
246 Gia_ObjComputeTruthTable6_rec( p, Gia_ObjFanin0(pObj), vTruths );
247 Gia_ObjComputeTruthTable6_rec( p, Gia_ObjFanin1(pObj), vTruths );
248 uTruth0 = Vec_WrdEntry( vTruths, Gia_ObjFanin0(pObj)->Value );
249 uTruth0 = Gia_ObjFaninC0(pObj) ? ~uTruth0 : uTruth0;
250 uTruth1 = Vec_WrdEntry( vTruths, Gia_ObjFanin1(pObj)->Value );
251 uTruth1 = Gia_ObjFaninC1(pObj) ? ~uTruth1 : uTruth1;
252 pObj->Value = Vec_WrdSize(vTruths);
253 Vec_WrdPush( vTruths, uTruth0 & uTruth1 );
254 }
Gia_ObjComputeTruthTable6(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vSupp,Vec_Wrd_t * vTruths)255 word Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths )
256 {
257 Gia_Obj_t * pLeaf;
258 int i;
259 assert( Vec_IntSize(vSupp) <= 6 );
260 assert( Gia_ObjIsAnd(pObj) );
261 assert( !pObj->fMark0 );
262 Vec_WrdClear( vTruths );
263 Gia_ManIncrementTravId( p );
264 Gia_ManForEachObjVec( vSupp, p, pLeaf, i )
265 {
266 assert( pLeaf->fMark0 || Gia_ObjIsRo(p, pLeaf) );
267 pLeaf->Value = Vec_WrdSize(vTruths);
268 Vec_WrdPush( vTruths, s_Truth6[i] );
269 Gia_ObjSetTravIdCurrent(p, pLeaf);
270 }
271 Gia_ObjComputeTruthTable6_rec( p, pObj, vTruths );
272 return Vec_WrdEntryLast( vTruths );
273 }
274
275 /**Function*************************************************************
276
277 Synopsis [Collects internal nodes reachable from the given node.]
278
279 Description []
280
281 SideEffects []
282
283 SeeAlso []
284
285 ***********************************************************************/
Gia_ObjCollectInternal_rec(Gia_Man_t * p,Gia_Obj_t * pObj)286 void Gia_ObjCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
287 {
288 if ( !Gia_ObjIsAnd(pObj) )
289 return;
290 if ( pObj->fMark0 )
291 return;
292 pObj->fMark0 = 1;
293 Gia_ObjCollectInternal_rec( p, Gia_ObjFanin0(pObj) );
294 Gia_ObjCollectInternal_rec( p, Gia_ObjFanin1(pObj) );
295 Gia_ObjSetNum( p, pObj, Vec_IntSize(p->vTtNodes) );
296 Vec_IntPush( p->vTtNodes, Gia_ObjId(p, pObj) );
297 }
Gia_ObjCollectInternal(Gia_Man_t * p,Gia_Obj_t * pObj)298 void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj )
299 {
300 Vec_IntClear( p->vTtNodes );
301 Gia_ObjCollectInternal_rec( p, pObj );
302 }
303
304 /**Function*************************************************************
305
306 Synopsis [Computing the truth table for GIA object.]
307
308 Description [The truth table should be used by the calling application
309 (or saved into the user's storage) before this procedure is called again.]
310
311 SideEffects []
312
313 SeeAlso []
314
315 ***********************************************************************/
Gia_ObjComputeTruthTable(Gia_Man_t * p,Gia_Obj_t * pObj)316 word * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj )
317 {
318 Gia_Obj_t * pTemp, * pRoot;
319 word * pTruth, * pTruthL, * pTruth0, * pTruth1;
320 int i;
321 if ( p->vTtMemory == NULL )
322 {
323 p->nTtVars = Gia_ManPiNum( p );
324 p->nTtWords = Abc_Truth6WordNum( p->nTtVars );
325 p->vTtNums = Vec_IntStart( Gia_ManObjNum(p) + 1000 );
326 p->vTtNodes = Vec_IntAlloc( 256 );
327 p->vTtInputs = Vec_PtrAllocTruthTables( Abc_MaxInt(6, p->nTtVars) );
328 p->vTtMemory = Vec_WrdStart( p->nTtWords * 256 );
329 }
330 else
331 {
332 // make sure the number of primary inputs did not change
333 // since the truth table computation storage was prepared
334 assert( p->nTtVars == Gia_ManPiNum(p) );
335 }
336 // extend ID numbers
337 if ( Vec_IntSize(p->vTtNums) < Gia_ManObjNum(p) )
338 Vec_IntFillExtra( p->vTtNums, Gia_ManObjNum(p), 0 );
339 // collect internal nodes
340 pRoot = Gia_ObjIsCo(pObj) ? Gia_ObjFanin0(pObj) : pObj;
341 Gia_ObjCollectInternal( p, pRoot );
342 // extend TT storage
343 if ( Vec_WrdSize(p->vTtMemory) < p->nTtWords * (Vec_IntSize(p->vTtNodes) + 2) )
344 Vec_WrdFillExtra( p->vTtMemory, p->nTtWords * (Vec_IntSize(p->vTtNodes) + 2), 0 );
345 // compute the truth table for internal nodes
346 Gia_ManForEachObjVec( p->vTtNodes, p, pTemp, i )
347 {
348 pTemp->fMark0 = 0; // unmark nodes marked by Gia_ObjCollectInternal()
349 pTruth = Gla_ObjTruthNode(p, pTemp);
350 pTruthL = pTruth + p->nTtWords;
351 pTruth0 = Gia_ObjIsAnd(Gia_ObjFanin0(pTemp)) ? Gla_ObjTruthNode(p, Gia_ObjFanin0(pTemp)) : Gla_ObjTruthElem(p, Gia_ObjCioId(Gia_ObjFanin0(pTemp)) );
352 pTruth1 = Gia_ObjIsAnd(Gia_ObjFanin1(pTemp)) ? Gla_ObjTruthNode(p, Gia_ObjFanin1(pTemp)) : Gla_ObjTruthElem(p, Gia_ObjCioId(Gia_ObjFanin1(pTemp)) );
353 if ( Gia_ObjFaninC0(pTemp) )
354 {
355 if ( Gia_ObjFaninC1(pTemp) )
356 while ( pTruth < pTruthL )
357 *pTruth++ = ~*pTruth0++ & ~*pTruth1++;
358 else
359 while ( pTruth < pTruthL )
360 *pTruth++ = ~*pTruth0++ & *pTruth1++;
361 }
362 else
363 {
364 if ( Gia_ObjFaninC1(pTemp) )
365 while ( pTruth < pTruthL )
366 *pTruth++ = *pTruth0++ & ~*pTruth1++;
367 else
368 while ( pTruth < pTruthL )
369 *pTruth++ = *pTruth0++ & *pTruth1++;
370 }
371 }
372 // compute the final table
373 if ( Gia_ObjIsConst0(pRoot) )
374 pTruth = Gla_ObjTruthConst0( p, Gla_ObjTruthFree1(p) );
375 else if ( Gia_ObjIsPi(p, pRoot) )
376 pTruth = Gla_ObjTruthElem( p, Gia_ObjCioId(pRoot) );
377 else if ( Gia_ObjIsAnd(pRoot) )
378 pTruth = Gla_ObjTruthNode( p, pRoot );
379 else
380 pTruth = NULL;
381 return Gla_ObjTruthDup( p, Gla_ObjTruthFree2(p), pTruth, Gia_ObjIsCo(pObj) && Gia_ObjFaninC0(pObj) );
382 }
383
384 /**Function*************************************************************
385
386 Synopsis [Testing truth table computation.]
387
388 Description []
389
390 SideEffects []
391
392 SeeAlso []
393
394 ***********************************************************************/
Gia_ObjComputeTruthTableTest(Gia_Man_t * p)395 void Gia_ObjComputeTruthTableTest( Gia_Man_t * p )
396 {
397 Gia_Obj_t * pObj;
398 unsigned * pTruth;
399 abctime clk = Abc_Clock();
400 int i;
401 Gia_ManForEachPo( p, pObj, i )
402 {
403 pTruth = (unsigned *)Gia_ObjComputeTruthTable( p, pObj );
404 // Extra_PrintHex( stdout, pTruth, Gia_ManPiNum(p) ); printf( "\n" );
405 }
406 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
407 }
408
409
410 /**Function*************************************************************
411
412 Synopsis []
413
414 Description []
415
416 SideEffects []
417
418 SeeAlso []
419
420 ***********************************************************************/
Gia_ObjComputeTruthTableStart(Gia_Man_t * p,int nVarsMax)421 void Gia_ObjComputeTruthTableStart( Gia_Man_t * p, int nVarsMax )
422 {
423 assert( p->vTtMemory == NULL );
424 p->nTtVars = nVarsMax;
425 p->nTtWords = Abc_Truth6WordNum( p->nTtVars );
426 p->vTtNodes = Vec_IntAlloc( 256 );
427 p->vTtInputs = Vec_PtrAllocTruthTables( Abc_MaxInt(6, p->nTtVars) );
428 p->vTtMemory = Vec_WrdStart( p->nTtWords * 64 );
429 p->vTtNums = Vec_IntAlloc( Gia_ManObjNum(p) + 1000 );
430 Vec_IntFill( p->vTtNums, Vec_IntCap(p->vTtNums), -ABC_INFINITY );
431 }
Gia_ObjComputeTruthTableStop(Gia_Man_t * p)432 void Gia_ObjComputeTruthTableStop( Gia_Man_t * p )
433 {
434 p->nTtVars = 0;
435 p->nTtWords = 0;
436 Vec_IntFreeP( &p->vTtNums );
437 Vec_IntFreeP( &p->vTtNodes );
438 Vec_PtrFreeP( &p->vTtInputs );
439 Vec_WrdFreeP( &p->vTtMemory );
440 }
441
442 /**Function*************************************************************
443
444 Synopsis [Collects internal nodes reachable from the given node.]
445
446 Description []
447
448 SideEffects []
449
450 SeeAlso []
451
452 ***********************************************************************/
Gia_ObjCollectInternalCut_rec(Gia_Man_t * p,int iObj)453 void Gia_ObjCollectInternalCut_rec( Gia_Man_t * p, int iObj )
454 {
455 if ( Gia_ObjHasNumId(p, iObj) )
456 return;
457 assert( Gia_ObjIsAnd(Gia_ManObj(p, iObj)) );
458 Gia_ObjCollectInternalCut_rec( p, Gia_ObjFaninId0(Gia_ManObj(p, iObj), iObj) );
459 Gia_ObjCollectInternalCut_rec( p, Gia_ObjFaninId1(Gia_ManObj(p, iObj), iObj) );
460 Gia_ObjSetNumId( p, iObj, Vec_IntSize(p->vTtNodes) );
461 Vec_IntPush( p->vTtNodes, iObj );
462 }
Gia_ObjCollectInternalCut(Gia_Man_t * p,int iRoot,Vec_Int_t * vLeaves)463 void Gia_ObjCollectInternalCut( Gia_Man_t * p, int iRoot, Vec_Int_t * vLeaves )
464 {
465 int i, iObj;
466 assert( !Gia_ObjHasNumId(p, iRoot) );
467 assert( Gia_ObjIsAnd(Gia_ManObj(p, iRoot)) );
468 Vec_IntForEachEntry( vLeaves, iObj, i )
469 {
470 if ( Gia_ObjHasNumId(p, iObj) ) // if cuts have repeated variables, skip
471 continue;
472 assert( !Gia_ObjHasNumId(p, iObj) );
473 Gia_ObjSetNumId( p, iObj, -i );
474 }
475 assert( !Gia_ObjHasNumId(p, iRoot) ); // the root cannot be one of the leaves
476 Vec_IntClear( p->vTtNodes );
477 Vec_IntPush( p->vTtNodes, -1 );
478 Gia_ObjCollectInternalCut_rec( p, iRoot );
479 }
480
481 /**Function*************************************************************
482
483 Synopsis [Computes the truth table of pRoot in terms of leaves.]
484
485 Description [The root cannot be one of the leaves.]
486
487 SideEffects []
488
489 SeeAlso []
490
491 ***********************************************************************/
Gia_ObjComputeTruthTableCut(Gia_Man_t * p,Gia_Obj_t * pRoot,Vec_Int_t * vLeaves)492 word * Gia_ObjComputeTruthTableCut( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves )
493 {
494 Gia_Obj_t * pTemp;
495 word * pTruth, * pTruthL, * pTruth0, * pTruth1;
496 int i, iObj, Id0, Id1;
497 assert( p->vTtMemory != NULL );
498 assert( Vec_IntSize(vLeaves) <= p->nTtVars );
499 // extend ID numbers
500 if ( Vec_IntSize(p->vTtNums) < Gia_ManObjNum(p) )
501 Vec_IntFillExtra( p->vTtNums, Gia_ManObjNum(p), -ABC_INFINITY );
502 // collect internal nodes
503 Gia_ObjCollectInternalCut( p, Gia_ObjId(p, pRoot), vLeaves );
504 // extend TT storage
505 if ( Vec_WrdSize(p->vTtMemory) < p->nTtWords * (Vec_IntSize(p->vTtNodes) + 2) )
506 Vec_WrdFillExtra( p->vTtMemory, p->nTtWords * (Vec_IntSize(p->vTtNodes) + 2), 0 );
507 // compute the truth table for internal nodes
508 Vec_IntForEachEntryStart( p->vTtNodes, iObj, i, 1 )
509 {
510 assert( i == Gia_ObjNumId(p, iObj) );
511 pTemp = Gia_ManObj( p, iObj );
512 pTruth = Gla_ObjTruthNodeId( p, i );
513 pTruthL = pTruth + p->nTtWords;
514 Id0 = Gia_ObjNumId( p, Gia_ObjFaninId0(pTemp, iObj) );
515 Id1 = Gia_ObjNumId( p, Gia_ObjFaninId1(pTemp, iObj) );
516 pTruth0 = (Id0 > 0) ? Gla_ObjTruthNodeId(p, Id0) : Gla_ObjTruthElem(p, -Id0);
517 pTruth1 = (Id1 > 0) ? Gla_ObjTruthNodeId(p, Id1) : Gla_ObjTruthElem(p, -Id1);
518 if ( Gia_ObjFaninC0(pTemp) )
519 {
520 if ( Gia_ObjFaninC1(pTemp) )
521 while ( pTruth < pTruthL )
522 *pTruth++ = ~*pTruth0++ & ~*pTruth1++;
523 else
524 while ( pTruth < pTruthL )
525 *pTruth++ = ~*pTruth0++ & *pTruth1++;
526 }
527 else
528 {
529 if ( Gia_ObjFaninC1(pTemp) )
530 while ( pTruth < pTruthL )
531 *pTruth++ = *pTruth0++ & ~*pTruth1++;
532 else
533 while ( pTruth < pTruthL )
534 *pTruth++ = *pTruth0++ & *pTruth1++;
535 }
536 }
537 pTruth = Gla_ObjTruthNode( p, pRoot );
538 // unmark leaves marked by Gia_ObjCollectInternal()
539 Vec_IntForEachEntry( vLeaves, iObj, i )
540 Gia_ObjResetNumId( p, iObj );
541 Vec_IntForEachEntryStart( p->vTtNodes, iObj, i, 1 )
542 Gia_ObjResetNumId( p, iObj );
543 return pTruth;
544 }
545
546 /**Function*************************************************************
547
548 Synopsis [Reduces GIA to contain isomorphic POs.]
549
550 Description [The root cannot be one of the leaves.]
551
552 SideEffects []
553
554 SeeAlso []
555
556 ***********************************************************************/
Gia_ManIsoNpnReduce(Gia_Man_t * p,Vec_Ptr_t ** pvPosEquivs,int fVerbose)557 Gia_Man_t * Gia_ManIsoNpnReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
558 {
559 char pCanonPerm[16];
560 int i, iObj, uCanonPhase, nVars, lastId, truthId;
561 int IndexCon = -1, IndexVar = -1;
562 Vec_Wec_t * vPosEquivs = Vec_WecAlloc( 100 );
563 word * pTruth;
564 Gia_Obj_t * pObj;
565 Vec_Mem_t * vTtMem[17]; // truth table memory and hash table
566 Gia_Man_t * pNew = NULL;
567 Vec_Int_t * vLeaves = Vec_IntAlloc( 16 );
568 Vec_Int_t * vFirsts;
569 Vec_Int_t * vTt2Class[17];
570 for ( i = 0; i < 17; i++ )
571 {
572 vTtMem[i] = Vec_MemAlloc( Abc_TtWordNum(i), 10 );
573 Vec_MemHashAlloc( vTtMem[i], 1000 );
574 vTt2Class[i] = Vec_IntStartFull( Gia_ManCoNum(p)+1 );
575 }
576 Gia_ObjComputeTruthTableStart( p, 16 );
577 Gia_ManForEachPo( p, pObj, i )
578 {
579 iObj = Gia_ObjId(p, pObj);
580 Gia_ManCollectCis( p, &iObj, 1, vLeaves );
581 if ( Vec_IntSize(vLeaves) > 16 )
582 {
583 Vec_IntPush( Vec_WecPushLevel(vPosEquivs), i );
584 continue;
585 }
586 pObj = Gia_ObjFanin0(pObj);
587 if ( Gia_ObjIsConst0(pObj) )
588 {
589 if ( IndexCon == -1 )
590 {
591 IndexCon = Vec_WecSize(vPosEquivs);
592 Vec_WecPushLevel(vPosEquivs);
593 }
594 Vec_WecPush( vPosEquivs, IndexCon, i );
595 continue;
596 }
597 if ( Gia_ObjIsCi(pObj) )
598 {
599 if ( IndexVar == -1 )
600 {
601 IndexVar = Vec_WecSize(vPosEquivs);
602 Vec_WecPushLevel(vPosEquivs);
603 }
604 Vec_WecPush( vPosEquivs, IndexVar, i );
605 continue;
606 }
607 assert( Gia_ObjIsAnd(pObj) );
608 pTruth = Gia_ObjComputeTruthTableCut( p, pObj, vLeaves );
609 Abc_TtMinimumBase( pTruth, NULL, Vec_IntSize(vLeaves), &nVars );
610 if ( nVars == 0 )
611 {
612 if ( IndexCon == -1 )
613 {
614 IndexCon = Vec_WecSize(vPosEquivs);
615 Vec_WecPushLevel(vPosEquivs);
616 }
617 Vec_WecPush( vPosEquivs, IndexCon, i );
618 continue;
619 }
620 if ( nVars == 1 )
621 {
622 if ( IndexVar == -1 )
623 {
624 IndexVar = Vec_WecSize(vPosEquivs);
625 Vec_WecPushLevel(vPosEquivs);
626 }
627 Vec_WecPush( vPosEquivs, IndexVar, i );
628 continue;
629 }
630 uCanonPhase = Abc_TtCanonicize( pTruth, nVars, pCanonPerm );
631 lastId = Vec_MemEntryNum( vTtMem[nVars] );
632 truthId = Vec_MemHashInsert( vTtMem[nVars], pTruth );
633 if ( lastId != Vec_MemEntryNum( vTtMem[nVars] ) ) // new one
634 {
635 assert( Vec_IntEntry(vTt2Class[nVars], truthId) == -1 );
636 Vec_IntWriteEntry( vTt2Class[nVars], truthId, Vec_WecSize(vPosEquivs) );
637 Vec_WecPushLevel(vPosEquivs);
638 }
639 assert( Vec_IntEntry(vTt2Class[nVars], truthId) >= 0 );
640 Vec_WecPush( vPosEquivs, Vec_IntEntry(vTt2Class[nVars], truthId), i );
641 }
642 Gia_ObjComputeTruthTableStop( p );
643 Vec_IntFree( vLeaves );
644 for ( i = 0; i < 17; i++ )
645 {
646 Vec_MemHashFree( vTtMem[i] );
647 Vec_MemFree( vTtMem[i] );
648 Vec_IntFree( vTt2Class[i] );
649 }
650
651 // find the first outputs and derive GIA
652 vFirsts = Vec_WecCollectFirsts( vPosEquivs );
653 pNew = Gia_ManDupCones( p, Vec_IntArray(vFirsts), Vec_IntSize(vFirsts), 0 );
654 Vec_IntFree( vFirsts );
655 // report and return
656 if ( fVerbose )
657 {
658 printf( "Nontrivial classes:\n" );
659 Vec_WecPrint( vPosEquivs, 1 );
660 }
661 if ( pvPosEquivs )
662 *pvPosEquivs = Vec_WecConvertToVecPtr( vPosEquivs );
663 Vec_WecFree( vPosEquivs );
664 return pNew;
665 }
666
667 ////////////////////////////////////////////////////////////////////////
668 /// END OF FILE ///
669 ////////////////////////////////////////////////////////////////////////
670
671
672 ABC_NAMESPACE_IMPL_END
673
674