1 /**CFile****************************************************************
2
3 FileName [giaEquiv.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Manipulation of equivalence classes.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: giaEquiv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22 #include "proof/cec/cec.h"
23 #include "sat/bmc/bmc.h"
24
25 ABC_NAMESPACE_IMPL_START
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 /**Function*************************************************************
36
37 Synopsis [Manipulating original IDs.]
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Gia_ManOrigIdsInit(Gia_Man_t * p)46 void Gia_ManOrigIdsInit( Gia_Man_t * p )
47 {
48 Vec_IntFreeP( &p->vIdsOrig );
49 p->vIdsOrig = Vec_IntStartNatural( Gia_ManObjNum(p) );
50 }
Gia_ManOrigIdsStart(Gia_Man_t * p)51 void Gia_ManOrigIdsStart( Gia_Man_t * p )
52 {
53 Vec_IntFreeP( &p->vIdsOrig );
54 p->vIdsOrig = Vec_IntStartFull( Gia_ManObjNum(p) );
55 }
Gia_ManOrigIdsRemap(Gia_Man_t * p,Gia_Man_t * pNew)56 void Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew )
57 {
58 Gia_Obj_t * pObj; int i;
59 if ( p->vIdsOrig == NULL )
60 return;
61 Gia_ManOrigIdsStart( pNew );
62 Vec_IntWriteEntry( pNew->vIdsOrig, 0, 0 );
63 Gia_ManForEachObj1( p, pObj, i )
64 if ( ~pObj->Value && Abc_Lit2Var(pObj->Value) && Vec_IntEntry(p->vIdsOrig, i) != -1 && Vec_IntEntry(pNew->vIdsOrig, Abc_Lit2Var(pObj->Value)) == -1 )
65 Vec_IntWriteEntry( pNew->vIdsOrig, Abc_Lit2Var(pObj->Value), Vec_IntEntry(p->vIdsOrig, i) );
66 Gia_ManForEachObj( pNew, pObj, i )
67 assert( Vec_IntEntry(pNew->vIdsOrig, i) >= 0 );
68 }
69 // input is a set of equivalent node pairs in any order
70 // output is the mapping of each node into the equiv node with the smallest ID
Gia_ManOrigIdsRemapPairsInsert(Vec_Int_t * vMap,int One,int Two)71 void Gia_ManOrigIdsRemapPairsInsert( Vec_Int_t * vMap, int One, int Two )
72 {
73 int Smo = One < Two ? One : Two;
74 int Big = One < Two ? Two : One;
75 assert( Smo != Big );
76 if ( Vec_IntEntry(vMap, Big) == -1 )
77 Vec_IntWriteEntry( vMap, Big, Smo );
78 else
79 Gia_ManOrigIdsRemapPairsInsert( vMap, Smo, Vec_IntEntry(vMap, Big) );
80 }
Gia_ManOrigIdsRemapPairsExtract(Vec_Int_t * vMap,int One)81 int Gia_ManOrigIdsRemapPairsExtract( Vec_Int_t * vMap, int One )
82 {
83 if ( Vec_IntEntry(vMap, One) == -1 )
84 return One;
85 return Gia_ManOrigIdsRemapPairsExtract( vMap, Vec_IntEntry(vMap, One) );
86 }
Gia_ManOrigIdsRemapPairs(Vec_Int_t * vEquivPairs,int nObjs)87 Vec_Int_t * Gia_ManOrigIdsRemapPairs( Vec_Int_t * vEquivPairs, int nObjs )
88 {
89 Vec_Int_t * vMapResult;
90 Vec_Int_t * vMap2Smaller;
91 int i, One, Two;
92 // map bigger into smaller one
93 vMap2Smaller = Vec_IntStartFull( nObjs );
94 Vec_IntForEachEntryDouble( vEquivPairs, One, Two, i )
95 Gia_ManOrigIdsRemapPairsInsert( vMap2Smaller, One, Two );
96 // collect results in the topo order
97 vMapResult = Vec_IntStartFull( nObjs );
98 Vec_IntForEachEntry( vMap2Smaller, One, i )
99 if ( One >= 0 )
100 Vec_IntWriteEntry( vMapResult, i, Gia_ManOrigIdsRemapPairsExtract(vMap2Smaller, One) );
101 Vec_IntFree( vMap2Smaller );
102 return vMapResult;
103 }
104 // remap the AIG using the equivalent pairs proved
105 // returns the reduced AIG and the equivalence classes of the original AIG
Gia_ManOrigIdsReduce(Gia_Man_t * p,Vec_Int_t * vPairs)106 Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs )
107 {
108 Gia_Man_t * pNew = NULL;
109 Gia_Obj_t * pObj, * pRepr; int i;
110 Vec_Int_t * vMap = Gia_ManOrigIdsRemapPairs( vPairs, Gia_ManObjNum(p) );
111 Gia_ManSetPhase( p );
112 pNew = Gia_ManStart( Gia_ManObjNum(p) );
113 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
114 pNew->pName = Abc_UtilStrsav( p->pName );
115 Gia_ManFillValue(p);
116 Gia_ManConst0(p)->Value = 0;
117 Gia_ManForEachCi( p, pObj, i )
118 pObj->Value = Gia_ManAppendCi(pNew);
119 Gia_ManHashAlloc( pNew );
120 Gia_ManForEachAnd( p, pObj, i )
121 {
122 if ( Vec_IntEntry(vMap, i) == -1 )
123 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
124 else
125 {
126 pRepr = Gia_ManObj( p, Vec_IntEntry(vMap, i) );
127 pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
128 }
129 }
130 Gia_ManHashStop( pNew );
131 Gia_ManForEachCo( p, pObj, i )
132 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
133 Vec_IntFree( vMap );
134 // compute equivalences
135 assert( !p->pReprs && !p->pNexts );
136 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
137 for ( i = 0; i < Gia_ManObjNum(p); i++ )
138 Gia_ObjSetRepr( p, i, GIA_VOID );
139 Gia_ManFillValue(pNew);
140 Gia_ManForEachAnd( p, pObj, i )
141 {
142 int iRepr = Abc_Lit2Var(pObj->Value);
143 if ( iRepr == 0 )
144 {
145 Gia_ObjSetRepr( p, i, 0 );
146 continue;
147 }
148 pRepr = Gia_ManObj( pNew, iRepr );
149 if ( !~pRepr->Value ) // first time
150 {
151 pRepr->Value = i;
152 continue;
153 }
154 // add equivalence
155 Gia_ObjSetRepr( p, i, pRepr->Value );
156 }
157 p->pNexts = Gia_ManDeriveNexts( p );
158 return pNew;
159 }
Gia_ManOrigIdsReduceTest(Gia_Man_t * p,Vec_Int_t * vPairs)160 Gia_Man_t * Gia_ManOrigIdsReduceTest( Gia_Man_t * p, Vec_Int_t * vPairs )
161 {
162 Gia_Man_t * pTemp, * pNew = Gia_ManOrigIdsReduce( p, vPairs );
163 Gia_ManPrintStats( p, NULL );
164 Gia_ManPrintStats( pNew, NULL );
165 //Gia_ManStop( pNew );
166 // cleanup the resulting one
167 pNew = Gia_ManCleanup( pTemp = pNew );
168 Gia_ManStop( pTemp );
169 return pNew;
170 }
171
172 /**Function*************************************************************
173
174 Synopsis [Compute equivalence classes of nodes.]
175
176 Description []
177
178 SideEffects []
179
180 SeeAlso []
181
182 ***********************************************************************/
Gia_ManComputeGiaEquivs(Gia_Man_t * pGia,int nConfs,int fVerbose)183 Gia_Man_t * Gia_ManComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose )
184 {
185 Gia_Man_t * pTemp;
186 Cec_ParFra_t ParsFra, * pPars = &ParsFra;
187 Cec_ManFraSetDefaultParams( pPars );
188 pPars->fUseOrigIds = 1;
189 pPars->fSatSweeping = 1;
190 pPars->nBTLimit = nConfs;
191 pPars->fVerbose = fVerbose;
192 pTemp = Cec_ManSatSweeping( pGia, pPars, 0 );
193 Gia_ManStop( pTemp );
194 return Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv );
195 }
196
197 /**Function*************************************************************
198
199 Synopsis [Returns 1 if AIG is not in the required topo order.]
200
201 Description []
202
203 SideEffects []
204
205 SeeAlso []
206
207 ***********************************************************************/
Gia_ManCheckTopoOrder_rec(Gia_Man_t * p,Gia_Obj_t * pObj)208 int Gia_ManCheckTopoOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
209 {
210 Gia_Obj_t * pRepr;
211 if ( pObj->Value == 0 )
212 return 1;
213 pObj->Value = 0;
214 assert( Gia_ObjIsAnd(pObj) );
215 if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin0(pObj) ) )
216 return 0;
217 if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin1(pObj) ) )
218 return 0;
219 pRepr = p->pReprs ? Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ) : NULL;
220 return pRepr == NULL || pRepr->Value == 0;
221 }
222
223 /**Function*************************************************************
224
225 Synopsis [Returns 0 if AIG is not in the required topo order.]
226
227 Description [AIG should be in such an order that the representative
228 is always traversed before the node.]
229
230 SideEffects []
231
232 SeeAlso []
233
234 ***********************************************************************/
Gia_ManCheckTopoOrder(Gia_Man_t * p)235 int Gia_ManCheckTopoOrder( Gia_Man_t * p )
236 {
237 Gia_Obj_t * pObj;
238 int i, RetValue = 1;
239 Gia_ManFillValue( p );
240 Gia_ManConst0(p)->Value = 0;
241 Gia_ManForEachCi( p, pObj, i )
242 pObj->Value = 0;
243 Gia_ManForEachCo( p, pObj, i )
244 RetValue &= Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin0(pObj) );
245 return RetValue;
246 }
247
248 /**Function*************************************************************
249
250 Synopsis [Given representatives, derives pointers to the next objects.]
251
252 Description []
253
254 SideEffects []
255
256 SeeAlso []
257
258 ***********************************************************************/
Gia_ManDeriveNexts(Gia_Man_t * p)259 int * Gia_ManDeriveNexts( Gia_Man_t * p )
260 {
261 unsigned * pNexts, * pTails;
262 int i;
263 assert( p->pReprs != NULL );
264 assert( p->pNexts == NULL );
265 pNexts = ABC_CALLOC( unsigned, Gia_ManObjNum(p) );
266 pTails = ABC_ALLOC( unsigned, Gia_ManObjNum(p) );
267 for ( i = 0; i < Gia_ManObjNum(p); i++ )
268 pTails[i] = i;
269 for ( i = 0; i < Gia_ManObjNum(p); i++ )
270 {
271 if ( !p->pReprs[i].iRepr || p->pReprs[i].iRepr == GIA_VOID )
272 continue;
273 pNexts[ pTails[p->pReprs[i].iRepr] ] = i;
274 pTails[p->pReprs[i].iRepr] = i;
275 }
276 ABC_FREE( pTails );
277 return (int *)pNexts;
278 }
279
280 /**Function*************************************************************
281
282 Synopsis [Given points to the next objects, derives representatives.]
283
284 Description []
285
286 SideEffects []
287
288 SeeAlso []
289
290 ***********************************************************************/
Gia_ManDeriveReprs(Gia_Man_t * p)291 void Gia_ManDeriveReprs( Gia_Man_t * p )
292 {
293 int i, iObj;
294 assert( p->pReprs == NULL );
295 assert( p->pNexts != NULL );
296 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
297 for ( i = 0; i < Gia_ManObjNum(p); i++ )
298 Gia_ObjSetRepr( p, i, GIA_VOID );
299 for ( i = 0; i < Gia_ManObjNum(p); i++ )
300 {
301 if ( p->pNexts[i] == 0 )
302 continue;
303 if ( p->pReprs[i].iRepr != GIA_VOID )
304 continue;
305 // next is set, repr is not set
306 for ( iObj = p->pNexts[i]; iObj; iObj = p->pNexts[iObj] )
307 p->pReprs[iObj].iRepr = i;
308 }
309 }
310
311 /**Function*************************************************************
312
313 Synopsis []
314
315 Description []
316
317 SideEffects []
318
319 SeeAlso []
320
321 ***********************************************************************/
Gia_ManEquivCountLitsAll(Gia_Man_t * p)322 int Gia_ManEquivCountLitsAll( Gia_Man_t * p )
323 {
324 int i, nLits = 0;
325 for ( i = 0; i < Gia_ManObjNum(p); i++ )
326 nLits += (Gia_ObjRepr(p, i) != GIA_VOID);
327 return nLits;
328 }
329
330 /**Function*************************************************************
331
332 Synopsis []
333
334 Description []
335
336 SideEffects []
337
338 SeeAlso []
339
340 ***********************************************************************/
Gia_ManEquivCountClasses(Gia_Man_t * p)341 int Gia_ManEquivCountClasses( Gia_Man_t * p )
342 {
343 int i, Counter = 0;
344 if ( p->pReprs == NULL )
345 return 0;
346 for ( i = 1; i < Gia_ManObjNum(p); i++ )
347 Counter += Gia_ObjIsHead(p, i);
348 return Counter;
349 }
350
351 /**Function*************************************************************
352
353 Synopsis []
354
355 Description []
356
357 SideEffects []
358
359 SeeAlso []
360
361 ***********************************************************************/
Gia_ManEquivCheckLits(Gia_Man_t * p,int nLits)362 int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
363 {
364 int nLitsReal = Gia_ManEquivCountLitsAll( p );
365 if ( nLitsReal != nLits )
366 Abc_Print( 1, "Detected a mismatch in counting equivalence classes (%d).\n", nLitsReal - nLits );
367 return 1;
368 }
369
370 /**Function*************************************************************
371
372 Synopsis []
373
374 Description []
375
376 SideEffects []
377
378 SeeAlso []
379
380 ***********************************************************************/
Gia_ManPrintStatsClasses(Gia_Man_t * p)381 void Gia_ManPrintStatsClasses( Gia_Man_t * p )
382 {
383 int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
384 for ( i = 1; i < Gia_ManObjNum(p); i++ )
385 {
386 if ( Gia_ObjIsHead(p, i) )
387 Counter++;
388 else if ( Gia_ObjIsConst(p, i) )
389 Counter0++;
390 else if ( Gia_ObjIsNone(p, i) )
391 CounterX++;
392 if ( Gia_ObjProved(p, i) )
393 Proved++;
394 }
395 CounterX -= Gia_ManCoNum(p);
396 nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
397
398 // Abc_Print( 1, "i/o/ff =%5d/%5d/%5d ", Gia_ManPiNum(p), Gia_ManPoNum(p), Gia_ManRegNum(p) );
399 // Abc_Print( 1, "and =%5d ", Gia_ManAndNum(p) );
400 // Abc_Print( 1, "lev =%3d ", Gia_ManLevelNum(p) );
401 Abc_Print( 1, "cst =%3d cls =%6d lit =%8d\n", Counter0, Counter, nLits );
402 }
403
404 /**Function*************************************************************
405
406 Synopsis []
407
408 Description []
409
410 SideEffects []
411
412 SeeAlso []
413
414 ***********************************************************************/
Gia_ManEquivCountLits(Gia_Man_t * p)415 int Gia_ManEquivCountLits( Gia_Man_t * p )
416 {
417 int i, Counter = 0, Counter0 = 0, CounterX = 0;
418 if ( p->pReprs == NULL || p->pNexts == NULL )
419 return 0;
420 for ( i = 1; i < Gia_ManObjNum(p); i++ )
421 {
422 if ( Gia_ObjIsHead(p, i) )
423 Counter++;
424 else if ( Gia_ObjIsConst(p, i) )
425 Counter0++;
426 else if ( Gia_ObjIsNone(p, i) )
427 CounterX++;
428 }
429 CounterX -= Gia_ManCoNum(p);
430 return Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
431 }
432
433 /**Function*************************************************************
434
435 Synopsis []
436
437 Description []
438
439 SideEffects []
440
441 SeeAlso []
442
443 ***********************************************************************/
Gia_ManEquivCountOne(Gia_Man_t * p,int i)444 int Gia_ManEquivCountOne( Gia_Man_t * p, int i )
445 {
446 int Ent, nLits = 1;
447 Gia_ClassForEachObj1( p, i, Ent )
448 {
449 assert( Gia_ObjRepr(p, Ent) == i );
450 nLits++;
451 }
452 return nLits;
453 }
Gia_ManEquivPrintOne(Gia_Man_t * p,int i,int Counter)454 void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter )
455 {
456 int Ent;
457 Abc_Print( 1, "Class %4d : Num = %2d {", Counter, Gia_ManEquivCountOne(p, i) );
458 Gia_ClassForEachObj( p, i, Ent )
459 {
460 Abc_Print( 1," %d", Ent );
461 if ( p->pReprs[Ent].fColorA || p->pReprs[Ent].fColorB )
462 Abc_Print( 1," <%d%d>", p->pReprs[Ent].fColorA, p->pReprs[Ent].fColorB );
463 }
464 Abc_Print( 1, " }\n" );
465 }
Gia_ManEquivPrintClasses(Gia_Man_t * p,int fVerbose,float Mem)466 void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
467 {
468 int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
469 for ( i = 1; i < Gia_ManObjNum(p); i++ )
470 {
471 if ( Gia_ObjIsHead(p, i) )
472 Counter++;
473 else if ( Gia_ObjIsConst(p, i) )
474 Counter0++;
475 else if ( Gia_ObjIsNone(p, i) )
476 CounterX++;
477 if ( Gia_ObjProved(p, i) )
478 Proved++;
479 }
480 CounterX -= Gia_ManCoNum(p);
481 nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
482 Abc_Print( 1, "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f MB\n",
483 Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
484 assert( Gia_ManEquivCheckLits( p, nLits ) );
485 if ( fVerbose )
486 {
487 // int Ent;
488 Abc_Print( 1, "Const0 (%d) = ", Counter0 );
489 Gia_ManForEachConst( p, i )
490 Abc_Print( 1, "%d ", i );
491 Abc_Print( 1, "\n" );
492 Counter = 0;
493 Gia_ManForEachClass( p, i )
494 Gia_ManEquivPrintOne( p, i, ++Counter );
495 /*
496 Gia_ManLevelNum( p );
497 Gia_ManForEachClass( p, i )
498 if ( i % 100 == 0 )
499 {
500 // Abc_Print( 1, "%d ", Gia_ManEquivCountOne(p, i) );
501 Gia_ClassForEachObj( p, i, Ent )
502 {
503 Abc_Print( 1, "%d ", Gia_ObjLevel( p, Gia_ManObj(p, Ent) ) );
504 }
505 Abc_Print( 1, "\n" );
506 }
507 */
508 }
509 }
510
511
512 /**Function*************************************************************
513
514 Synopsis [Map representatives into class members with minimum level.]
515
516 Description []
517
518 SideEffects []
519
520 SeeAlso []
521
522 ***********************************************************************/
Gia_ManChoiceMinLevel_rec(Gia_Man_t * p,int iPivot,int fDiveIn,Vec_Int_t * vMap)523 int Gia_ManChoiceMinLevel_rec( Gia_Man_t * p, int iPivot, int fDiveIn, Vec_Int_t * vMap )
524 {
525 int Level0, Level1, LevelMax;
526 Gia_Obj_t * pPivot = Gia_ManObj( p, iPivot );
527 if ( Gia_ObjIsCi(pPivot) )
528 return 0;
529 if ( Gia_ObjLevel(p, pPivot) )
530 return Gia_ObjLevel(p, pPivot);
531 if ( fDiveIn && Gia_ObjIsClass(p, iPivot) )
532 {
533 int iObj, ObjMin = -1, iRepr = Gia_ObjRepr(p, iPivot), LevMin = ABC_INFINITY;
534 Gia_ClassForEachObj( p, iRepr, iObj )
535 {
536 int LevCur = Gia_ManChoiceMinLevel_rec( p, iObj, 0, vMap );
537 if ( LevMin > LevCur )
538 {
539 LevMin = LevCur;
540 ObjMin = iObj;
541 }
542 }
543 assert( LevMin > 0 );
544 Vec_IntWriteEntry( vMap, iRepr, ObjMin );
545 Gia_ClassForEachObj( p, iRepr, iObj )
546 Gia_ObjSetLevelId( p, iObj, LevMin );
547 return LevMin;
548 }
549 assert( Gia_ObjIsAnd(pPivot) );
550 Level0 = Gia_ManChoiceMinLevel_rec( p, Gia_ObjFaninId0(pPivot, iPivot), 1, vMap );
551 Level1 = Gia_ManChoiceMinLevel_rec( p, Gia_ObjFaninId1(pPivot, iPivot), 1, vMap );
552 LevelMax = 1 + Abc_MaxInt(Level0, Level1);
553 Gia_ObjSetLevel( p, pPivot, LevelMax );
554 return LevelMax;
555 }
Gia_ManChoiceMinLevel(Gia_Man_t * p)556 Vec_Int_t * Gia_ManChoiceMinLevel( Gia_Man_t * p )
557 {
558 Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
559 Gia_Obj_t * pObj;
560 int i, LevelCur, LevelMax = 0;
561 // assert( Gia_ManRegNum(p) == 0 );
562 Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
563 Gia_ManForEachCo( p, pObj, i )
564 {
565 LevelCur = Gia_ManChoiceMinLevel_rec( p, Gia_ObjFaninId0p(p, pObj), 1, vMap );
566 LevelMax = Abc_MaxInt(LevelMax, LevelCur);
567 }
568 //printf( "Max level %d\n", LevelMax );
569 return vMap;
570 }
571
572 /**Function*************************************************************
573
574 Synopsis [Returns representative node.]
575
576 Description []
577
578 SideEffects []
579
580 SeeAlso []
581
582 ***********************************************************************/
Gia_ManEquivRepr(Gia_Man_t * p,Gia_Obj_t * pObj,int fUseAll,int fDualOut)583 static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut )
584 {
585 if ( fUseAll )
586 {
587 if ( Gia_ObjRepr(p, Gia_ObjId(p,pObj)) == GIA_VOID )
588 return NULL;
589 }
590 else
591 {
592 if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
593 return NULL;
594 }
595 // if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ) )
596 if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ) )
597 return NULL;
598 return Gia_ManObj( p, Gia_ObjRepr(p, Gia_ObjId(p,pObj)) );
599 }
600
601 /**Function*************************************************************
602
603 Synopsis [Duplicates the AIG in the DFS order.]
604
605 Description []
606
607 SideEffects []
608
609 SeeAlso []
610
611 ***********************************************************************/
Gia_ManEquivReduce_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj,int fUseAll,int fDualOut)612 void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut )
613 {
614 Gia_Obj_t * pRepr;
615 if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
616 {
617 Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut );
618 pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
619 return;
620 }
621 if ( ~pObj->Value )
622 return;
623 assert( Gia_ObjIsAnd(pObj) );
624 Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
625 Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll, fDualOut );
626 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
627 }
628
629 /**Function*************************************************************
630
631 Synopsis [Reduces AIG using equivalence classes.]
632
633 Description []
634
635 SideEffects []
636
637 SeeAlso []
638
639 ***********************************************************************/
Gia_ManEquivReduce(Gia_Man_t * p,int fUseAll,int fDualOut,int fSkipPhase,int fVerbose)640 Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose )
641 {
642 Gia_Man_t * pNew;
643 Gia_Obj_t * pObj;
644 int i;
645 if ( !p->pReprs && p->pSibls )
646 {
647 int * pMap = ABC_FALLOC( int, Gia_ManObjNum(p) );
648 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
649 for ( i = 0; i < Gia_ManObjNum(p); i++ )
650 Gia_ObjSetRepr( p, i, GIA_VOID );
651 for ( i = 0; i < Gia_ManObjNum(p); i++ )
652 if ( p->pSibls[i] > 0 )
653 {
654 if ( pMap[p->pSibls[i]] == -1 )
655 pMap[p->pSibls[i]] = p->pSibls[i];
656 pMap[i] = pMap[p->pSibls[i]];
657 }
658 for ( i = 0; i < Gia_ManObjNum(p); i++ )
659 if ( p->pSibls[i] > 0 )
660 Gia_ObjSetRepr( p, i, pMap[i] );
661 //printf( "Created equivalence classes.\n" );
662 ABC_FREE( p->pNexts );
663 p->pNexts = Gia_ManDeriveNexts( p );
664 ABC_FREE( pMap );
665 }
666 if ( !p->pReprs )
667 {
668 Abc_Print( 1, "Gia_ManEquivReduce(): Equivalence classes are not available.\n" );
669 return NULL;
670 }
671 if ( fDualOut && (Gia_ManPoNum(p) & 1) )
672 {
673 Abc_Print( 1, "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" );
674 return NULL;
675 }
676 // check if there are any equivalences defined
677 Gia_ManForEachObj( p, pObj, i )
678 if ( Gia_ObjReprObj(p, i) != NULL )
679 break;
680 if ( i == Gia_ManObjNum(p) )
681 {
682 // Abc_Print( 1, "Gia_ManEquivReduce(): There are no equivalences to reduce.\n" );
683 // return NULL;
684 return Gia_ManDup( p );
685 }
686 /*
687 if ( !Gia_ManCheckTopoOrder( p ) )
688 {
689 Abc_Print( 1, "Gia_ManEquivReduce(): AIG is not in a correct topological order.\n" );
690 return NULL;
691 }
692 */
693 if ( !fSkipPhase )
694 Gia_ManSetPhase( p );
695 if ( fDualOut )
696 Gia_ManEquivSetColors( p, fVerbose );
697 pNew = Gia_ManStart( Gia_ManObjNum(p) );
698 pNew->pName = Abc_UtilStrsav( p->pName );
699 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
700 Gia_ManFillValue( p );
701 Gia_ManConst0(p)->Value = 0;
702 Gia_ManForEachCi( p, pObj, i )
703 pObj->Value = Gia_ManAppendCi(pNew);
704 Gia_ManHashAlloc( pNew );
705 Gia_ManForEachCo( p, pObj, i )
706 Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
707 Gia_ManForEachCo( p, pObj, i )
708 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
709 Gia_ManHashStop( pNew );
710 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
711 return pNew;
712 }
713
714 /**Function*************************************************************
715
716 Synopsis [Duplicates the AIG in the DFS order.]
717
718 Description []
719
720 SideEffects []
721
722 SeeAlso []
723
724 ***********************************************************************/
Gia_ManEquivReduce2_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vMap,int fDiveIn)725 void Gia_ManEquivReduce2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vMap, int fDiveIn )
726 {
727 Gia_Obj_t * pRepr;
728 if ( ~pObj->Value )
729 return;
730 assert( Gia_ObjIsAnd(pObj) );
731 if ( fDiveIn && (pRepr = Gia_ManEquivRepr(p, pObj, 1, 0)) )
732 {
733 int iTemp, iRepr = Gia_ObjId(p, pRepr);
734 Gia_Obj_t * pRepr2 = Gia_ManObj( p, Vec_IntEntry(vMap, iRepr) );
735 Gia_ManEquivReduce2_rec( pNew, p, pRepr2, vMap, 0 );
736 Gia_ClassForEachObj( p, iRepr, iTemp )
737 {
738 Gia_Obj_t * pTemp = Gia_ManObj(p, iTemp);
739 pTemp->Value = Abc_LitNotCond( pRepr2->Value, Gia_ObjPhaseReal(pRepr2) ^ Gia_ObjPhaseReal(pTemp) );
740 }
741 assert( ~pObj->Value );
742 assert( ~pRepr->Value );
743 assert( ~pRepr2->Value );
744 return;
745 }
746 Gia_ManEquivReduce2_rec( pNew, p, Gia_ObjFanin0(pObj), vMap, 1 );
747 Gia_ManEquivReduce2_rec( pNew, p, Gia_ObjFanin1(pObj), vMap, 1 );
748 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
749 }
Gia_ManEquivReduce2(Gia_Man_t * p)750 Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p )
751 {
752 Vec_Int_t * vMap;
753 Gia_Man_t * pNew;
754 Gia_Obj_t * pObj;
755 int i;
756 if ( !p->pReprs && p->pSibls )
757 {
758 int * pMap = ABC_FALLOC( int, Gia_ManObjNum(p) );
759 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
760 for ( i = 0; i < Gia_ManObjNum(p); i++ )
761 Gia_ObjSetRepr( p, i, GIA_VOID );
762 for ( i = 0; i < Gia_ManObjNum(p); i++ )
763 if ( p->pSibls[i] > 0 )
764 {
765 if ( pMap[p->pSibls[i]] == -1 )
766 pMap[p->pSibls[i]] = p->pSibls[i];
767 pMap[i] = pMap[p->pSibls[i]];
768 }
769 for ( i = 0; i < Gia_ManObjNum(p); i++ )
770 if ( p->pSibls[i] > 0 )
771 Gia_ObjSetRepr( p, i, pMap[i] );
772 //printf( "Created equivalence classes.\n" );
773 ABC_FREE( p->pNexts );
774 p->pNexts = Gia_ManDeriveNexts( p );
775 ABC_FREE( pMap );
776 }
777 if ( !p->pReprs )
778 {
779 Abc_Print( 1, "Gia_ManEquivReduce(): Equivalence classes are not available.\n" );
780 return NULL;
781 }
782 // check if there are any equivalences defined
783 Gia_ManForEachObj( p, pObj, i )
784 if ( Gia_ObjReprObj(p, i) != NULL )
785 break;
786 if ( i == Gia_ManObjNum(p) )
787 return Gia_ManDup( p );
788 vMap = Gia_ManChoiceMinLevel( p );
789 Gia_ManSetPhase( p );
790 pNew = Gia_ManStart( Gia_ManObjNum(p) );
791 pNew->pName = Abc_UtilStrsav( p->pName );
792 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
793 Gia_ManFillValue( p );
794 Gia_ManConst0(p)->Value = 0;
795 Gia_ManForEachCi( p, pObj, i )
796 pObj->Value = Gia_ManAppendCi(pNew);
797 Gia_ManHashAlloc( pNew );
798 Gia_ManForEachCo( p, pObj, i )
799 Gia_ManEquivReduce2_rec( pNew, p, Gia_ObjFanin0(pObj), vMap, 1 );
800 Gia_ManForEachCo( p, pObj, i )
801 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
802 Gia_ManHashStop( pNew );
803 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
804 Vec_IntFree( vMap );
805 return pNew;
806 }
807
808
809 /**Function*************************************************************
810
811 Synopsis [Reduces AIG using equivalence classes.]
812
813 Description []
814
815 SideEffects []
816
817 SeeAlso []
818
819 ***********************************************************************/
Gia_ManEquivFixOutputPairs(Gia_Man_t * p)820 void Gia_ManEquivFixOutputPairs( Gia_Man_t * p )
821 {
822 Gia_Obj_t * pObj0, * pObj1;
823 int i;
824 assert( (Gia_ManPoNum(p) & 1) == 0 );
825 Gia_ManForEachPo( p, pObj0, i )
826 {
827 pObj1 = Gia_ManPo( p, ++i );
828 if ( Gia_ObjChild0(pObj0) != Gia_ObjChild0(pObj1) )
829 continue;
830 pObj0->iDiff0 = Gia_ObjId(p, pObj0);
831 pObj0->fCompl0 = 0;
832 pObj1->iDiff0 = Gia_ObjId(p, pObj1);
833 pObj1->fCompl0 = 0;
834 }
835 }
836
837 /**Function*************************************************************
838
839 Synopsis [Removes pointers to the unmarked nodes..]
840
841 Description []
842
843 SideEffects []
844
845 SeeAlso []
846
847 ***********************************************************************/
Gia_ManEquivUpdatePointers(Gia_Man_t * p,Gia_Man_t * pNew)848 void Gia_ManEquivUpdatePointers( Gia_Man_t * p, Gia_Man_t * pNew )
849 {
850 Gia_Obj_t * pObj, * pObjNew;
851 int i;
852 Gia_ManForEachObj( p, pObj, i )
853 {
854 if ( !~pObj->Value )
855 continue;
856 pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
857 if ( pObjNew->fMark0 )
858 pObj->Value = ~0;
859 }
860 }
861
862 /**Function*************************************************************
863
864 Synopsis [Removes pointers to the unmarked nodes..]
865
866 Description []
867
868 SideEffects []
869
870 SeeAlso []
871
872 ***********************************************************************/
Gia_ManEquivDeriveReprs(Gia_Man_t * p,Gia_Man_t * pNew,Gia_Man_t * pFinal)873 void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFinal )
874 {
875 Vec_Int_t * vClass;
876 Gia_Obj_t * pObj, * pObjNew;
877 int i, k, iNode, iRepr, iPrev;
878 // start representatives
879 pFinal->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pFinal) );
880 for ( i = 0; i < Gia_ManObjNum(pFinal); i++ )
881 Gia_ObjSetRepr( pFinal, i, GIA_VOID );
882 // iterate over constant candidates
883 Gia_ManForEachConst( p, i )
884 {
885 pObj = Gia_ManObj( p, i );
886 if ( !~pObj->Value )
887 continue;
888 pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
889 if ( Abc_Lit2Var(pObjNew->Value) == 0 )
890 continue;
891 Gia_ObjSetRepr( pFinal, Abc_Lit2Var(pObjNew->Value), 0 );
892 }
893 // iterate over class candidates
894 vClass = Vec_IntAlloc( 100 );
895 Gia_ManForEachClass( p, i )
896 {
897 Vec_IntClear( vClass );
898 Gia_ClassForEachObj( p, i, k )
899 {
900 pObj = Gia_ManObj( p, k );
901 if ( !~pObj->Value )
902 continue;
903 pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
904 Vec_IntPushUnique( vClass, Abc_Lit2Var(pObjNew->Value) );
905 }
906 if ( Vec_IntSize( vClass ) < 2 )
907 continue;
908 Vec_IntSort( vClass, 0 );
909 iRepr = iPrev = Vec_IntEntry( vClass, 0 );
910 Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
911 {
912 Gia_ObjSetRepr( pFinal, iNode, iRepr );
913 assert( iPrev < iNode );
914 iPrev = iNode;
915 }
916 }
917 Vec_IntFree( vClass );
918 pFinal->pNexts = Gia_ManDeriveNexts( pFinal );
919 }
920
921 /**Function*************************************************************
922
923 Synopsis [Removes pointers to the unmarked nodes..]
924
925 Description []
926
927 SideEffects []
928
929 SeeAlso []
930
931 ***********************************************************************/
Gia_ManEquivRemapDfs(Gia_Man_t * p)932 Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p )
933 {
934 Gia_Man_t * pNew;
935 Vec_Int_t * vClass;
936 int i, k, iNode, iRepr, iPrev;
937 pNew = Gia_ManDupDfs( p );
938 // start representatives
939 pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
940 for ( i = 0; i < Gia_ManObjNum(pNew); i++ )
941 Gia_ObjSetRepr( pNew, i, GIA_VOID );
942 // iterate over constant candidates
943 Gia_ManForEachConst( p, i )
944 Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
945 // iterate over class candidates
946 vClass = Vec_IntAlloc( 100 );
947 Gia_ManForEachClass( p, i )
948 {
949 Vec_IntClear( vClass );
950 Gia_ClassForEachObj( p, i, k )
951 Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
952 assert( Vec_IntSize( vClass ) > 1 );
953 Vec_IntSort( vClass, 0 );
954 iRepr = iPrev = Vec_IntEntry( vClass, 0 );
955 Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
956 {
957 Gia_ObjSetRepr( pNew, iNode, iRepr );
958 assert( iPrev < iNode );
959 iPrev = iNode;
960 }
961 }
962 Vec_IntFree( vClass );
963 pNew->pNexts = Gia_ManDeriveNexts( pNew );
964 return pNew;
965 }
966
967 /**Function*************************************************************
968
969 Synopsis [Reduces AIG while remapping equivalence classes.]
970
971 Description [Drops the pairs of outputs if they are proved equivalent.]
972
973 SideEffects []
974
975 SeeAlso []
976
977 ***********************************************************************/
Gia_ManEquivReduceAndRemap(Gia_Man_t * p,int fSeq,int fMiterPairs)978 Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs )
979 {
980 Gia_Man_t * pNew, * pFinal;
981 pNew = Gia_ManEquivReduce( p, 0, 0, 0, 0 );
982 if ( pNew == NULL )
983 return NULL;
984 Gia_ManOrigIdsRemap( p, pNew );
985 if ( fMiterPairs )
986 Gia_ManEquivFixOutputPairs( pNew );
987 if ( fSeq )
988 Gia_ManSeqMarkUsed( pNew );
989 else
990 Gia_ManCombMarkUsed( pNew );
991 Gia_ManEquivUpdatePointers( p, pNew );
992 pFinal = Gia_ManDupMarked( pNew );
993 Gia_ManOrigIdsRemap( pNew, pFinal );
994 Gia_ManEquivDeriveReprs( p, pNew, pFinal );
995 Gia_ManStop( pNew );
996 pFinal = Gia_ManEquivRemapDfs( pNew = pFinal );
997 Gia_ManOrigIdsRemap( pNew, pFinal );
998 Gia_ManStop( pNew );
999 return pFinal;
1000 }
1001
1002 /**Function*************************************************************
1003
1004 Synopsis [Marks CIs/COs/ANDs unreachable from POs.]
1005
1006 Description []
1007
1008 SideEffects []
1009
1010 SeeAlso []
1011
1012 ***********************************************************************/
Gia_ManEquivSetColor_rec(Gia_Man_t * p,Gia_Obj_t * pObj,int fOdds)1013 int Gia_ManEquivSetColor_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fOdds )
1014 {
1015 if ( Gia_ObjVisitColor( p, Gia_ObjId(p,pObj), fOdds ) )
1016 return 0;
1017 if ( Gia_ObjIsRo(p, pObj) )
1018 return 1 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p, pObj)), fOdds );
1019 assert( Gia_ObjIsAnd(pObj) );
1020 return 1 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), fOdds )
1021 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin1(pObj), fOdds );
1022 }
1023
1024 /**Function*************************************************************
1025
1026 Synopsis [Marks CIs/COs/ANDs unreachable from POs.]
1027
1028 Description []
1029
1030 SideEffects []
1031
1032 SeeAlso []
1033
1034 ***********************************************************************/
Gia_ManEquivSetColors(Gia_Man_t * p,int fVerbose)1035 int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
1036 {
1037 Gia_Obj_t * pObj;
1038 int i, nNodes[2], nDiffs[2];
1039 assert( (Gia_ManPoNum(p) & 1) == 0 );
1040 Gia_ObjSetColors( p, 0 );
1041 Gia_ManForEachPi( p, pObj, i )
1042 Gia_ObjSetColors( p, Gia_ObjId(p,pObj) );
1043 nNodes[0] = nNodes[1] = Gia_ManPiNum(p);
1044 Gia_ManForEachPo( p, pObj, i )
1045 nNodes[i&1] += Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), i&1 );
1046 // Gia_ManForEachObj( p, pObj, i )
1047 // if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) )
1048 // assert( Gia_ObjColors(p, i) );
1049 nDiffs[0] = Gia_ManCandNum(p) - nNodes[0];
1050 nDiffs[1] = Gia_ManCandNum(p) - nNodes[1];
1051 if ( fVerbose )
1052 {
1053 Abc_Print( 1, "CI+AND = %7d A = %7d B = %7d Ad = %7d Bd = %7d AB = %7d.\n",
1054 Gia_ManCandNum(p), nNodes[0], nNodes[1], nDiffs[0], nDiffs[1],
1055 Gia_ManCandNum(p) - nDiffs[0] - nDiffs[1] );
1056 }
1057 return (nDiffs[0] + nDiffs[1]) / 2;
1058 }
1059
1060 /**Function*************************************************************
1061
1062 Synopsis [Duplicates the AIG in the DFS order.]
1063
1064 Description []
1065
1066 SideEffects []
1067
1068 SeeAlso []
1069
1070 ***********************************************************************/
Gia_ManSpecBuild(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vXorLits,int fDualOut,int fSpeculate,Vec_Int_t * vTrace,Vec_Int_t * vGuide,Vec_Int_t * vMap)1071 static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide, Vec_Int_t * vMap )
1072 {
1073 Gia_Obj_t * pRepr;
1074 unsigned iLitNew;
1075 pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
1076 if ( pRepr == NULL )
1077 return;
1078 // if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
1079 if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
1080 return;
1081 iLitNew = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1082 if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
1083 {
1084 if ( vTrace )
1085 Vec_IntPush( vTrace, 1 );
1086 if ( vGuide == NULL || Vec_IntEntry( vGuide, Vec_IntSize(vTrace)-1 ) )
1087 {
1088 if ( vMap )
1089 Vec_IntPush( vMap, Gia_ObjId(p, pObj) );
1090 Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
1091 }
1092 }
1093 else
1094 {
1095 if ( vTrace )
1096 Vec_IntPush( vTrace, 0 );
1097 }
1098 if ( fSpeculate )
1099 pObj->Value = iLitNew;
1100 }
1101
1102 /**Function*************************************************************
1103
1104 Synopsis [Duplicates the AIG in the DFS order.]
1105
1106 Description []
1107
1108 SideEffects []
1109
1110 SeeAlso []
1111
1112 ***********************************************************************/
Gia_ManSpecReduce_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vXorLits,int fDualOut,int fSpeculate,Vec_Int_t * vTrace,Vec_Int_t * vGuide,Vec_Int_t * vMap)1113 void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide, Vec_Int_t * vMap )
1114 {
1115 if ( ~pObj->Value )
1116 return;
1117 assert( Gia_ObjIsAnd(pObj) );
1118 Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap );
1119 Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap );
1120 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1121 Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap );
1122 }
1123
1124 /**Function*************************************************************
1125
1126 Synopsis [Reduces AIG using equivalence classes.]
1127
1128 Description []
1129
1130 SideEffects []
1131
1132 SeeAlso []
1133
1134 ***********************************************************************/
Gia_ManSpecReduceTrace(Gia_Man_t * p,Vec_Int_t * vTrace,Vec_Int_t * vMap)1135 Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace, Vec_Int_t * vMap )
1136 {
1137 Vec_Int_t * vXorLits;
1138 Gia_Man_t * pNew, * pTemp;
1139 Gia_Obj_t * pObj;
1140 int i, iLitNew;
1141 if ( !p->pReprs )
1142 {
1143 Abc_Print( 1, "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
1144 return NULL;
1145 }
1146 Vec_IntClear( vTrace );
1147 vXorLits = Vec_IntAlloc( 1000 );
1148 Gia_ManSetPhase( p );
1149 Gia_ManFillValue( p );
1150 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1151 pNew->pName = Abc_UtilStrsav( p->pName );
1152 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1153 Gia_ManHashAlloc( pNew );
1154 Gia_ManConst0(p)->Value = 0;
1155 Gia_ManForEachCi( p, pObj, i )
1156 pObj->Value = Gia_ManAppendCi(pNew);
1157 Gia_ManForEachRo( p, pObj, i )
1158 Gia_ManSpecBuild( pNew, p, pObj, vXorLits, 0, 1, vTrace, NULL, vMap );
1159 Gia_ManForEachCo( p, pObj, i )
1160 Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, 0, 1, vTrace, NULL, vMap );
1161 Gia_ManForEachPo( p, pObj, i )
1162 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1163 Vec_IntForEachEntry( vXorLits, iLitNew, i )
1164 Gia_ManAppendCo( pNew, iLitNew );
1165 if ( Vec_IntSize(vXorLits) == 0 )
1166 {
1167 Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
1168 Gia_ManAppendCo( pNew, 0 );
1169 }
1170 Gia_ManForEachRi( p, pObj, i )
1171 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1172 Gia_ManHashStop( pNew );
1173 Vec_IntFree( vXorLits );
1174 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1175 pNew = Gia_ManCleanup( pTemp = pNew );
1176 Gia_ManStop( pTemp );
1177 return pNew;
1178 }
1179
1180 /**Function*************************************************************
1181
1182 Synopsis [Reduces AIG using equivalence classes.]
1183
1184 Description []
1185
1186 SideEffects []
1187
1188 SeeAlso []
1189
1190 ***********************************************************************/
Gia_ManSpecReduce(Gia_Man_t * p,int fDualOut,int fSynthesis,int fSpeculate,int fSkipSome,int fVerbose)1191 Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fSpeculate, int fSkipSome, int fVerbose )
1192 {
1193 Gia_Man_t * pNew, * pTemp;
1194 Gia_Obj_t * pObj;
1195 Vec_Int_t * vXorLits;
1196 int i, iLitNew;
1197 Vec_Int_t * vTrace = NULL, * vGuide = NULL;
1198 if ( !p->pReprs )
1199 {
1200 Abc_Print( 1, "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
1201 return NULL;
1202 }
1203 if ( fDualOut && (Gia_ManPoNum(p) & 1) )
1204 {
1205 Abc_Print( 1, "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
1206 return NULL;
1207 }
1208 if ( fSkipSome )
1209 {
1210 vGuide = Vec_IntAlloc( 100 );
1211 pTemp = Gia_ManSpecReduceTrace( p, vGuide, NULL );
1212 Gia_ManStop( pTemp );
1213 assert( Vec_IntSize(vGuide) == Gia_ManEquivCountLitsAll(p) );
1214 vTrace = Vec_IntAlloc( 100 );
1215 }
1216 vXorLits = Vec_IntAlloc( 1000 );
1217 Gia_ManSetPhase( p );
1218 Gia_ManFillValue( p );
1219 if ( fDualOut )
1220 Gia_ManEquivSetColors( p, fVerbose );
1221 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1222 pNew->pName = Abc_UtilStrsav( p->pName );
1223 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1224 Gia_ManHashAlloc( pNew );
1225 Gia_ManConst0(p)->Value = 0;
1226 Gia_ManForEachCi( p, pObj, i )
1227 pObj->Value = Gia_ManAppendCi(pNew);
1228 Gia_ManForEachRo( p, pObj, i )
1229 Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide, NULL );
1230 Gia_ManForEachCo( p, pObj, i )
1231 Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, NULL );
1232 if ( !fSynthesis )
1233 {
1234 Gia_ManForEachPo( p, pObj, i )
1235 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1236 }
1237 Vec_IntForEachEntry( vXorLits, iLitNew, i )
1238 Gia_ManAppendCo( pNew, iLitNew );
1239 if ( Vec_IntSize(vXorLits) == 0 )
1240 {
1241 Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
1242 Gia_ManAppendCo( pNew, 0 );
1243 }
1244 Gia_ManForEachRi( p, pObj, i )
1245 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
1246 Gia_ManHashStop( pNew );
1247 Vec_IntFree( vXorLits );
1248 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
1249 pNew = Gia_ManCleanup( pTemp = pNew );
1250 Gia_ManStop( pTemp );
1251
1252 // update using trace
1253 if ( fSkipSome )
1254 {
1255 // count the number of non-zero entries
1256 int iLit, nAddPos = 0;
1257 Vec_IntForEachEntry( vGuide, iLit, i )
1258 if ( iLit )
1259 nAddPos++;
1260 if ( nAddPos )
1261 assert( Gia_ManPoNum(pNew) == Gia_ManPoNum(p) + nAddPos );
1262 }
1263 Vec_IntFreeP( &vTrace );
1264 Vec_IntFreeP( &vGuide );
1265 return pNew;
1266 }
1267
1268 /**Function*************************************************************
1269
1270 Synopsis [Duplicates the AIG in the DFS order.]
1271
1272 Description []
1273
1274 SideEffects []
1275
1276 SeeAlso []
1277
1278 ***********************************************************************/
Gia_ManSpecBuildInit(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vXorLits,int f,int fDualOut)1279 void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f, int fDualOut )
1280 {
1281 Gia_Obj_t * pRepr;
1282 int iLitNew;
1283 pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
1284 if ( pRepr == NULL )
1285 return;
1286 // if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
1287 if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
1288 return;
1289 iLitNew = Abc_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1290 if ( Gia_ObjCopyF(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
1291 Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjCopyF(p, f, pObj), iLitNew) );
1292 Gia_ObjSetCopyF( p, f, pObj, iLitNew );
1293 }
1294
1295 /**Function*************************************************************
1296
1297 Synopsis [Duplicates the AIG in the DFS order.]
1298
1299 Description []
1300
1301 SideEffects []
1302
1303 SeeAlso []
1304
1305 ***********************************************************************/
Gia_ManSpecReduceInit_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vXorLits,int f,int fDualOut)1306 void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f, int fDualOut )
1307 {
1308 if ( ~Gia_ObjCopyF(p, f, pObj) )
1309 return;
1310 assert( Gia_ObjIsAnd(pObj) );
1311 Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut );
1312 Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f, fDualOut );
1313 Gia_ObjSetCopyF( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj)) );
1314 Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut );
1315 }
1316
1317 /**Function*************************************************************
1318
1319 Synopsis [Creates initialized SRM with the given number of frames.]
1320
1321 Description []
1322
1323 SideEffects []
1324
1325 SeeAlso []
1326
1327 ***********************************************************************/
Gia_ManSpecReduceInit(Gia_Man_t * p,Abc_Cex_t * pInit,int nFrames,int fDualOut)1328 Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames, int fDualOut )
1329 {
1330 Gia_Man_t * pNew, * pTemp;
1331 Gia_Obj_t * pObj, * pObjRi, * pObjRo;
1332 Vec_Int_t * vXorLits;
1333 int f, i, iLitNew;
1334 if ( !p->pReprs )
1335 {
1336 Abc_Print( 1, "Gia_ManSpecReduceInit(): Equivalence classes are not available.\n" );
1337 return NULL;
1338 }
1339 if ( Gia_ManRegNum(p) == 0 )
1340 {
1341 Abc_Print( 1, "Gia_ManSpecReduceInit(): Circuit is not sequential.\n" );
1342 return NULL;
1343 }
1344 if ( Gia_ManRegNum(p) != pInit->nRegs )
1345 {
1346 Abc_Print( 1, "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" );
1347 return NULL;
1348 }
1349 if ( fDualOut && (Gia_ManPoNum(p) & 1) )
1350 {
1351 Abc_Print( 1, "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" );
1352 return NULL;
1353 }
1354
1355 /*
1356 if ( !Gia_ManCheckTopoOrder( p ) )
1357 {
1358 Abc_Print( 1, "Gia_ManSpecReduceInit(): AIG is not in a correct topological order.\n" );
1359 return NULL;
1360 }
1361 */
1362 assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 );
1363 Vec_IntFill( &p->vCopies, nFrames * Gia_ManObjNum(p), -1 );
1364 vXorLits = Vec_IntAlloc( 1000 );
1365 Gia_ManSetPhase( p );
1366 if ( fDualOut )
1367 Gia_ManEquivSetColors( p, 0 );
1368 pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
1369 pNew->pName = Abc_UtilStrsav( p->pName );
1370 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1371 Gia_ManHashAlloc( pNew );
1372 Gia_ManForEachRo( p, pObj, i )
1373 Gia_ObjSetCopyF( p, 0, pObj, Abc_InfoHasBit(pInit->pData, i) );
1374 for ( f = 0; f < nFrames; f++ )
1375 {
1376 Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
1377 Gia_ManForEachPi( p, pObj, i )
1378 Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
1379 Gia_ManForEachRo( p, pObj, i )
1380 Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut );
1381 Gia_ManForEachCo( p, pObj, i )
1382 {
1383 Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut );
1384 Gia_ObjSetCopyF( p, f, pObj, Gia_ObjFanin0CopyF(p, f, pObj) );
1385 }
1386 if ( f == nFrames - 1 )
1387 break;
1388 Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
1389 Gia_ObjSetCopyF( p, f+1, pObjRo, Gia_ObjCopyF(p, f, pObjRi) );
1390 }
1391 Vec_IntForEachEntry( vXorLits, iLitNew, i )
1392 Gia_ManAppendCo( pNew, iLitNew );
1393 if ( Vec_IntSize(vXorLits) == 0 )
1394 {
1395 // Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
1396 Gia_ManAppendCo( pNew, 0 );
1397 }
1398 Vec_IntErase( &p->vCopies );
1399 Vec_IntFree( vXorLits );
1400 Gia_ManHashStop( pNew );
1401 pNew = Gia_ManCleanup( pTemp = pNew );
1402 Gia_ManStop( pTemp );
1403 return pNew;
1404 }
1405
1406 /**Function*************************************************************
1407
1408 Synopsis [Creates initialized SRM with the given number of frames.]
1409
1410 Description [Uses as many frames as needed to create the number of
1411 output not less than the number of equivalence literals.]
1412
1413 SideEffects []
1414
1415 SeeAlso []
1416
1417 ***********************************************************************/
Gia_ManSpecReduceInitFrames(Gia_Man_t * p,Abc_Cex_t * pInit,int nFramesMax,int * pnFrames,int fDualOut,int nMinOutputs)1418 Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs )
1419 {
1420 Gia_Man_t * pFrames;
1421 int f, nLits;
1422 nLits = Gia_ManEquivCountLits( p );
1423 for ( f = 1; ; f++ )
1424 {
1425 pFrames = Gia_ManSpecReduceInit( p, pInit, f, fDualOut );
1426 if ( (nMinOutputs == 0 && Gia_ManPoNum(pFrames) >= nLits/2+1) ||
1427 (nMinOutputs != 0 && Gia_ManPoNum(pFrames) >= nMinOutputs) )
1428 break;
1429 if ( f == nFramesMax )
1430 break;
1431 if ( Gia_ManAndNum(pFrames) > 500000 )
1432 {
1433 Gia_ManStop( pFrames );
1434 return NULL;
1435 }
1436 Gia_ManStop( pFrames );
1437 pFrames = NULL;
1438 }
1439 if ( f == nFramesMax )
1440 Abc_Print( 1, "Stopped unrolling after %d frames.\n", nFramesMax );
1441 if ( pnFrames )
1442 *pnFrames = f;
1443 return pFrames;
1444 }
1445
1446 /**Function*************************************************************
1447
1448 Synopsis [Transforms equiv classes by removing the AB nodes.]
1449
1450 Description []
1451
1452 SideEffects []
1453
1454 SeeAlso []
1455
1456 ***********************************************************************/
Gia_ManEquivTransform(Gia_Man_t * p,int fVerbose)1457 void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose )
1458 {
1459 extern void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass );
1460 Vec_Int_t * vClass, * vClassNew;
1461 int iRepr, iNode, Ent, k;
1462 int nRemovedLits = 0, nRemovedClas = 0;
1463 int nTotalLits = 0, nTotalClas = 0;
1464 Gia_Obj_t * pObj;
1465 int i;
1466 assert( p->pReprs && p->pNexts );
1467 vClass = Vec_IntAlloc( 100 );
1468 vClassNew = Vec_IntAlloc( 100 );
1469 Gia_ManForEachObj( p, pObj, i )
1470 if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) )
1471 assert( Gia_ObjColors(p, i) );
1472 Gia_ManForEachClassReverse( p, iRepr )
1473 {
1474 nTotalClas++;
1475 Vec_IntClear( vClass );
1476 Vec_IntClear( vClassNew );
1477 Gia_ClassForEachObj( p, iRepr, iNode )
1478 {
1479 nTotalLits++;
1480 Vec_IntPush( vClass, iNode );
1481 assert( Gia_ObjColors(p, iNode) );
1482 if ( Gia_ObjColors(p, iNode) != 3 )
1483 Vec_IntPush( vClassNew, iNode );
1484 else
1485 nRemovedLits++;
1486 }
1487 Vec_IntForEachEntry( vClass, Ent, k )
1488 {
1489 p->pReprs[Ent].fFailed = p->pReprs[Ent].fProved = 0;
1490 p->pReprs[Ent].iRepr = GIA_VOID;
1491 p->pNexts[Ent] = 0;
1492 }
1493 if ( Vec_IntSize(vClassNew) < 2 )
1494 {
1495 nRemovedClas++;
1496 continue;
1497 }
1498 Cec_ManSimClassCreate( p, vClassNew );
1499 }
1500 Vec_IntFree( vClass );
1501 Vec_IntFree( vClassNew );
1502 if ( fVerbose )
1503 Abc_Print( 1, "Removed classes = %6d (out of %6d). Removed literals = %6d (out of %6d).\n",
1504 nRemovedClas, nTotalClas, nRemovedLits, nTotalLits );
1505 }
1506
1507 /**Function*************************************************************
1508
1509 Synopsis [Marks proved equivalences.]
1510
1511 Description []
1512
1513 SideEffects []
1514
1515 SeeAlso []
1516
1517 ***********************************************************************/
Gia_ManEquivMark(Gia_Man_t * p,char * pFileName,int fSkipSome,int fVerbose)1518 void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerbose )
1519 {
1520 Gia_Man_t * pMiter, * pTemp;
1521 Gia_Obj_t * pObj;
1522 int i, iLit, nAddPos, nLits = 0;
1523 int nLitsAll, Counter = 0;
1524 nLitsAll = Gia_ManEquivCountLitsAll( p );
1525 if ( nLitsAll == 0 )
1526 {
1527 Abc_Print( 1, "Gia_ManEquivMark(): Current AIG does not have equivalences.\n" );
1528 return;
1529 }
1530 // read AIGER file
1531 pMiter = Gia_AigerRead( pFileName, 0, 0, 0 );
1532 if ( pMiter == NULL )
1533 {
1534 Abc_Print( 1, "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
1535 return;
1536 }
1537 if ( fSkipSome )
1538 {
1539 Vec_Int_t * vTrace = Vec_IntAlloc( 100 );
1540 pTemp = Gia_ManSpecReduceTrace( p, vTrace, NULL );
1541 Gia_ManStop( pTemp );
1542 assert( Vec_IntSize(vTrace) == nLitsAll );
1543 // count the number of non-zero entries
1544 nAddPos = 0;
1545 Vec_IntForEachEntry( vTrace, iLit, i )
1546 if ( iLit )
1547 nAddPos++;
1548 // check the number
1549 if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nAddPos )
1550 {
1551 Abc_Print( 1, "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGFilteredEquivNum(%d).\n",
1552 Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nAddPos );
1553 Gia_ManStop( pMiter );
1554 Vec_IntFreeP( &vTrace );
1555 return;
1556 }
1557 // mark corresponding POs as solved
1558 nLits = iLit = Counter = 0;
1559 for ( i = 0; i < Gia_ManObjNum(p); i++ )
1560 {
1561 if ( Gia_ObjRepr(p, i) == GIA_VOID )
1562 continue;
1563 if ( Vec_IntEntry( vTrace, nLits++ ) == 0 )
1564 continue;
1565 pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + iLit++ );
1566 if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven
1567 {
1568 Gia_ObjSetProved(p, i);
1569 Counter++;
1570 }
1571 }
1572 assert( nLits == nLitsAll );
1573 assert( iLit == nAddPos );
1574 Vec_IntFreeP( &vTrace );
1575 }
1576 else
1577 {
1578 if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nLitsAll )
1579 {
1580 Abc_Print( 1, "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGEquivNum(%d).\n",
1581 Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nLitsAll );
1582 Gia_ManStop( pMiter );
1583 return;
1584 }
1585 // mark corresponding POs as solved
1586 nLits = 0;
1587 for ( i = 0; i < Gia_ManObjNum(p); i++ )
1588 {
1589 if ( Gia_ObjRepr(p, i) == GIA_VOID )
1590 continue;
1591 pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + nLits++ );
1592 if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven
1593 {
1594 Gia_ObjSetProved(p, i);
1595 Counter++;
1596 }
1597 }
1598 assert( nLits == nLitsAll );
1599 }
1600 if ( fVerbose )
1601 Abc_Print( 1, "Set %d equivalences as proved.\n", Counter );
1602 Gia_ManStop( pMiter );
1603 }
1604
1605 /**Function*************************************************************
1606
1607 Synopsis [Transforms equiv classes by filtering those that correspond to disproved outputs.]
1608
1609 Description []
1610
1611 SideEffects []
1612
1613 SeeAlso []
1614
1615 ***********************************************************************/
Gia_ManEquivFilter(Gia_Man_t * p,Vec_Int_t * vPoIds,int fVerbose)1616 void Gia_ManEquivFilter( Gia_Man_t * p, Vec_Int_t * vPoIds, int fVerbose )
1617 {
1618 Gia_Man_t * pSrm;
1619 Vec_Int_t * vTrace, * vMap;
1620 int i, iObjId, Entry, Prev = -1;
1621 // check if there are equivalences
1622 if ( p->pReprs == NULL || p->pNexts == NULL )
1623 {
1624 Abc_Print( 1, "Gia_ManEquivFilter(): Equivalence classes are not defined.\n" );
1625 return;
1626 }
1627 // check if PO indexes are available
1628 if ( vPoIds == NULL )
1629 {
1630 Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs is not available.\n" );
1631 return;
1632 }
1633 if ( Vec_IntSize(vPoIds) == 0 )
1634 return;
1635 // create SRM with mapping into POs
1636 vMap = Vec_IntAlloc( 1000 );
1637 vTrace = Vec_IntAlloc( 1000 );
1638 pSrm = Gia_ManSpecReduceTrace( p, vTrace, vMap );
1639 Vec_IntFree( vTrace );
1640 // the resulting array (vMap) maps PO indexes of the SRM into object IDs
1641 assert( Gia_ManPoNum(pSrm) == Gia_ManPoNum(p) + Vec_IntSize(vMap) );
1642 Gia_ManStop( pSrm );
1643 if ( fVerbose )
1644 printf( "Design POs = %d. SRM POs = %d. Spec POs = %d. Disproved POs = %d.\n",
1645 Gia_ManPoNum(p), Gia_ManPoNum(p) + Vec_IntSize(vMap), Vec_IntSize(vMap), Vec_IntSize(vPoIds) );
1646 // check if disproved POs satisfy the range
1647 Vec_IntSort( vPoIds, 0 );
1648 Vec_IntForEachEntry( vPoIds, Entry, i )
1649 {
1650 if ( Entry < 0 || Entry >= Gia_ManPoNum(p) + Vec_IntSize(vMap) )
1651 {
1652 Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs contains PO index (%d),\n", Entry );
1653 Abc_Print( 1, "which does not fit into the range of available PO indexes of the SRM: [%d; %d].\n", 0, Gia_ManPoNum(p) + Vec_IntSize(vMap)-1 );
1654 Vec_IntFree( vMap );
1655 return;
1656 }
1657 if ( Entry < Gia_ManPoNum(p) )
1658 Abc_Print( 0, "Gia_ManEquivFilter(): One of the original POs (%d) have failed.\n", Entry );
1659 if ( Prev == Entry )
1660 {
1661 Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs contains at least one duplicate entry (%d),\n", Entry );
1662 Vec_IntFree( vMap );
1663 return;
1664 }
1665 Prev = Entry;
1666 }
1667 // perform the reduction of the equivalence classes
1668 Vec_IntForEachEntry( vPoIds, Entry, i )
1669 {
1670 if ( Entry < Gia_ManPoNum(p) )
1671 continue;
1672 iObjId = Vec_IntEntry( vMap, Entry - Gia_ManPoNum(p) );
1673 Gia_ObjUnsetRepr( p, iObjId );
1674 // Gia_ObjSetNext( p, iObjId, 0 );
1675 }
1676 Vec_IntFree( vMap );
1677 ABC_FREE( p->pNexts );
1678 p->pNexts = Gia_ManDeriveNexts( p );
1679 }
1680
1681 /**Function*************************************************************
1682
1683 Synopsis [Transforms equiv classes by filtering those that correspond to disproved outputs.]
1684
1685 Description []
1686
1687 SideEffects []
1688
1689 SeeAlso []
1690
1691 ***********************************************************************/
Gia_ManEquivFilterTest(Gia_Man_t * p)1692 void Gia_ManEquivFilterTest( Gia_Man_t * p )
1693 {
1694 Vec_Int_t * vPoIds;
1695 int i;
1696 vPoIds = Vec_IntAlloc( 1000 );
1697 for ( i = 0; i < 10; i++ )
1698 {
1699 Vec_IntPush( vPoIds, Gia_ManPoNum(p) + 2 * i + 2 );
1700 printf( "%d ", Gia_ManPoNum(p) + 2*i + 2 );
1701 }
1702 printf( "\n" );
1703 Gia_ManEquivFilter( p, vPoIds, 1 );
1704 Vec_IntFree( vPoIds );
1705 }
1706
1707 /**Function*************************************************************
1708
1709 Synopsis [Transforms equiv classes by setting a good representative.]
1710
1711 Description []
1712
1713 SideEffects []
1714
1715 SeeAlso []
1716
1717 ***********************************************************************/
Gia_ManEquivImprove(Gia_Man_t * p)1718 void Gia_ManEquivImprove( Gia_Man_t * p )
1719 {
1720 Vec_Int_t * vClass;
1721 int i, k, iNode, iRepr;
1722 int iReprBest, iLevelBest, iLevelCur, iMffcBest, iMffcCur;
1723 assert( p->pReprs != NULL && p->pNexts != NULL );
1724 Gia_ManLevelNum( p );
1725 Gia_ManCreateRefs( p );
1726 // iterate over class candidates
1727 vClass = Vec_IntAlloc( 100 );
1728 Gia_ManForEachClass( p, i )
1729 {
1730 Vec_IntClear( vClass );
1731 iReprBest = -1;
1732 iLevelBest = iMffcBest = ABC_INFINITY;
1733 Gia_ClassForEachObj( p, i, k )
1734 {
1735 iLevelCur = Gia_ObjLevel( p,Gia_ManObj(p, k) );
1736 iMffcCur = Gia_NodeMffcSize( p, Gia_ManObj(p, k) );
1737 if ( iLevelBest > iLevelCur || (iLevelBest == iLevelCur && iMffcBest > iMffcCur) )
1738 {
1739 iReprBest = k;
1740 iLevelBest = iLevelCur;
1741 iMffcBest = iMffcCur;
1742 }
1743 Vec_IntPush( vClass, k );
1744 }
1745 assert( Vec_IntSize( vClass ) > 1 );
1746 assert( iReprBest > 0 );
1747 if ( i == iReprBest )
1748 continue;
1749 /*
1750 Abc_Print( 1, "Repr/Best = %6d/%6d. Lev = %3d/%3d. Mffc = %3d/%3d.\n",
1751 i, iReprBest, Gia_ObjLevel( p,Gia_ManObj(p, i) ), Gia_ObjLevel( p,Gia_ManObj(p, iReprBest) ),
1752 Gia_NodeMffcSize( p, Gia_ManObj(p, i) ), Gia_NodeMffcSize( p, Gia_ManObj(p, iReprBest) ) );
1753 */
1754 iRepr = iReprBest;
1755 Gia_ObjSetRepr( p, iRepr, GIA_VOID );
1756 Gia_ObjSetProved( p, i );
1757 Gia_ObjUnsetProved( p, iRepr );
1758 Vec_IntForEachEntry( vClass, iNode, k )
1759 if ( iNode != iRepr )
1760 Gia_ObjSetRepr( p, iNode, iRepr );
1761 }
1762 Vec_IntFree( vClass );
1763 ABC_FREE( p->pNexts );
1764 // p->pNexts = Gia_ManDeriveNexts( p );
1765 }
1766
1767
1768 /**Function*************************************************************
1769
1770 Synopsis [Returns 1 if pOld is in the TFI of pNode.]
1771
1772 Description []
1773
1774 SideEffects []
1775
1776 SeeAlso []
1777
1778 ***********************************************************************/
Gia_ObjCheckTfi_rec(Gia_Man_t * p,Gia_Obj_t * pOld,Gia_Obj_t * pNode,Vec_Ptr_t * vVisited)1779 int Gia_ObjCheckTfi_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode, Vec_Ptr_t * vVisited )
1780 {
1781 // check the trivial cases
1782 if ( pNode == NULL )
1783 return 0;
1784 if ( Gia_ObjIsCi(pNode) )
1785 return 0;
1786 // if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
1787 // return 0;
1788 if ( pNode == pOld )
1789 return 1;
1790 // skip the visited node
1791 if ( pNode->fMark0 )
1792 return 0;
1793 pNode->fMark0 = 1;
1794 Vec_PtrPush( vVisited, pNode );
1795 // check the children
1796 if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin0(pNode), vVisited ) )
1797 return 1;
1798 if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin1(pNode), vVisited ) )
1799 return 1;
1800 // check equivalent nodes
1801 return Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjNextObj(p, Gia_ObjId(p, pNode)), vVisited );
1802 }
1803
1804 /**Function*************************************************************
1805
1806 Synopsis [Returns 1 if pOld is in the TFI of pNode.]
1807
1808 Description []
1809
1810 SideEffects []
1811
1812 SeeAlso []
1813
1814 ***********************************************************************/
Gia_ObjCheckTfi(Gia_Man_t * p,Gia_Obj_t * pOld,Gia_Obj_t * pNode)1815 int Gia_ObjCheckTfi( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
1816 {
1817 Vec_Ptr_t * vVisited;
1818 Gia_Obj_t * pObj;
1819 int RetValue, i;
1820 assert( !Gia_IsComplement(pOld) );
1821 assert( !Gia_IsComplement(pNode) );
1822 vVisited = Vec_PtrAlloc( 100 );
1823 RetValue = Gia_ObjCheckTfi_rec( p, pOld, pNode, vVisited );
1824 Vec_PtrForEachEntry( Gia_Obj_t *, vVisited, pObj, i )
1825 pObj->fMark0 = 0;
1826 Vec_PtrFree( vVisited );
1827 return RetValue;
1828 }
1829
1830
1831 /**Function*************************************************************
1832
1833 Synopsis [Adds the next entry while making choices.]
1834
1835 Description []
1836
1837 SideEffects []
1838
1839 SeeAlso []
1840
1841 ***********************************************************************/
Gia_ManAddNextEntry_rec(Gia_Man_t * p,Gia_Obj_t * pOld,Gia_Obj_t * pNode)1842 void Gia_ManAddNextEntry_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
1843 {
1844 if ( Gia_ObjNext(p, Gia_ObjId(p, pOld)) == 0 )
1845 {
1846 Gia_ObjSetNext( p, Gia_ObjId(p, pOld), Gia_ObjId(p, pNode) );
1847 return;
1848 }
1849 Gia_ManAddNextEntry_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pOld)), pNode );
1850 }
1851
1852 /**Function*************************************************************
1853
1854 Synopsis [Duplicates the AIG in the DFS order.]
1855
1856 Description []
1857
1858 SideEffects []
1859
1860 SeeAlso []
1861
1862 ***********************************************************************/
Gia_ManEquivToChoices_rec(Gia_Man_t * pNew,Gia_Man_t * p,Gia_Obj_t * pObj)1863 void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
1864 {
1865 Gia_Obj_t * pRepr, * pReprNew, * pObjNew;
1866 if ( ~pObj->Value )
1867 return;
1868 if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
1869 {
1870 if ( Gia_ObjIsConst0(pRepr) )
1871 {
1872 pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1873 return;
1874 }
1875 Gia_ManEquivToChoices_rec( pNew, p, pRepr );
1876 assert( Gia_ObjIsAnd(pObj) );
1877 Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
1878 Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
1879 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1880 if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) )
1881 {
1882 assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
1883 return;
1884 }
1885 if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
1886 return;
1887 assert( pRepr->Value < pObj->Value );
1888 pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) );
1889 pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
1890 if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
1891 {
1892 // assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
1893 if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) != pReprNew )
1894 return;
1895 pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1896 return;
1897 }
1898 if ( !Gia_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
1899 {
1900 assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 );
1901 Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
1902 Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew );
1903 }
1904 pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
1905 return;
1906 }
1907 assert( Gia_ObjIsAnd(pObj) );
1908 Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
1909 Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
1910 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1911 }
1912
1913 /**Function*************************************************************
1914
1915 Synopsis [Removes choices, which contain fanouts.]
1916
1917 Description []
1918
1919 SideEffects []
1920
1921 SeeAlso []
1922
1923 ***********************************************************************/
Gia_ManRemoveBadChoices(Gia_Man_t * p)1924 void Gia_ManRemoveBadChoices( Gia_Man_t * p )
1925 {
1926 Gia_Obj_t * pObj;
1927 int i, iObj, iPrev, Counter = 0;
1928 // mark nodes with fanout
1929 Gia_ManForEachObj( p, pObj, i )
1930 {
1931 pObj->fMark0 = 0;
1932 if ( Gia_ObjIsAnd(pObj) )
1933 {
1934 Gia_ObjFanin0(pObj)->fMark0 = 1;
1935 Gia_ObjFanin1(pObj)->fMark0 = 1;
1936 }
1937 else if ( Gia_ObjIsCo(pObj) )
1938 Gia_ObjFanin0(pObj)->fMark0 = 1;
1939 }
1940 // go through the classes and remove
1941 Gia_ManForEachClass( p, i )
1942 {
1943 for ( iPrev = i, iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iPrev) )
1944 {
1945 if ( !Gia_ManObj(p, iObj)->fMark0 )
1946 {
1947 iPrev = iObj;
1948 continue;
1949 }
1950 Gia_ObjSetRepr( p, iObj, GIA_VOID );
1951 Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
1952 Gia_ObjSetNext( p, iObj, 0 );
1953 Counter++;
1954 }
1955 }
1956 // remove the marks
1957 Gia_ManCleanMark0( p );
1958 // Abc_Print( 1, "Removed %d bad choices.\n", Counter );
1959 }
1960
1961 /**Function*************************************************************
1962
1963 Synopsis [Reduces AIG using equivalence classes.]
1964
1965 Description []
1966
1967 SideEffects []
1968
1969 SeeAlso []
1970
1971 ***********************************************************************/
Gia_ManEquivToChoices(Gia_Man_t * p,int nSnapshots)1972 Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
1973 {
1974 Vec_Int_t * vNodes;
1975 Gia_Man_t * pNew, * pTemp;
1976 Gia_Obj_t * pObj, * pRepr;
1977 int i;
1978 //Gia_ManEquivPrintClasses( p, 0, 0 );
1979 assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
1980 Gia_ManSetPhase( p );
1981 pNew = Gia_ManStart( Gia_ManObjNum(p) );
1982 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1983 pNew->pName = Abc_UtilStrsav( p->pName );
1984 pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
1985 pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
1986 for ( i = 0; i < Gia_ManObjNum(p); i++ )
1987 Gia_ObjSetRepr( pNew, i, GIA_VOID );
1988 Gia_ManFillValue( p );
1989 Gia_ManConst0(p)->Value = 0;
1990 Gia_ManForEachCi( p, pObj, i )
1991 pObj->Value = Gia_ManAppendCi(pNew);
1992 Gia_ManForEachRo( p, pObj, i )
1993 if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
1994 {
1995 assert( Gia_ObjIsConst0(pRepr) || Gia_ObjIsRo(p, pRepr) );
1996 pObj->Value = pRepr->Value;
1997 }
1998 Gia_ManHashAlloc( pNew );
1999 Gia_ManForEachCo( p, pObj, i )
2000 Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
2001 vNodes = Gia_ManGetDangling( p );
2002 Gia_ManForEachObjVec( vNodes, p, pObj, i )
2003 Gia_ManEquivToChoices_rec( pNew, p, pObj );
2004 Vec_IntFree( vNodes );
2005 Gia_ManForEachCo( p, pObj, i )
2006 if ( i % nSnapshots == 0 )
2007 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2008 Gia_ManHashStop( pNew );
2009 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2010 Gia_ManRemoveBadChoices( pNew );
2011 //Gia_ManEquivPrintClasses( pNew, 0, 0 );
2012 pNew = Gia_ManCleanup( pTemp = pNew );
2013 Gia_ManStop( pTemp );
2014 //Gia_ManEquivPrintClasses( pNew, 0, 0 );
2015 return pNew;
2016 }
2017
2018 /**Function*************************************************************
2019
2020 Synopsis [Counts the number of choice nodes]
2021
2022 Description []
2023
2024 SideEffects []
2025
2026 SeeAlso []
2027
2028 ***********************************************************************/
Gia_ManCountChoiceNodes(Gia_Man_t * p)2029 int Gia_ManCountChoiceNodes( Gia_Man_t * p )
2030 {
2031 Gia_Obj_t * pObj;
2032 int i, Counter = 0;
2033 if ( p->pReprs == NULL || p->pNexts == NULL )
2034 return 0;
2035 Gia_ManForEachObj( p, pObj, i )
2036 Counter += Gia_ObjIsHead( p, i );
2037 return Counter;
2038 }
2039
2040 /**Function*************************************************************
2041
2042 Synopsis [Counts the number of choices]
2043
2044 Description []
2045
2046 SideEffects []
2047
2048 SeeAlso []
2049
2050 ***********************************************************************/
Gia_ManCountChoices(Gia_Man_t * p)2051 int Gia_ManCountChoices( Gia_Man_t * p )
2052 {
2053 Gia_Obj_t * pObj;
2054 int i, Counter = 0;
2055 if ( p->pReprs == NULL || p->pNexts == NULL )
2056 return 0;
2057 Gia_ManForEachObj( p, pObj, i )
2058 Counter += (int)(Gia_ObjNext( p, i ) > 0);
2059 return Counter;
2060 }
2061
2062 ABC_NAMESPACE_IMPL_END
2063
2064 #include "aig/aig/aig.h"
2065 #include "aig/saig/saig.h"
2066 #include "proof/cec/cec.h"
2067 #include "giaAig.h"
2068
2069 ABC_NAMESPACE_IMPL_START
2070
2071
2072 /**Function*************************************************************
2073
2074 Synopsis [Returns 1 if AIG has dangling nodes.]
2075
2076 Description []
2077
2078 SideEffects []
2079
2080 SeeAlso []
2081
2082 ***********************************************************************/
Gia_ManHasNoEquivs(Gia_Man_t * p)2083 int Gia_ManHasNoEquivs( Gia_Man_t * p )
2084 {
2085 Gia_Obj_t * pObj;
2086 int i;
2087 if ( p->pReprs == NULL )
2088 return 1;
2089 Gia_ManForEachObj( p, pObj, i )
2090 if ( Gia_ObjReprObj(p, i) != NULL )
2091 break;
2092 return i == Gia_ManObjNum(p);
2093 }
2094
2095 /**Function*************************************************************
2096
2097 Synopsis [Implements iteration during speculation.]
2098
2099 Description []
2100
2101 SideEffects []
2102
2103 SeeAlso []
2104
2105 ***********************************************************************/
Gia_CommandSpecI(Gia_Man_t * pGia,int nFramesInit,int nBTLimitInit,int fStart,int fCheckMiter,int fVerbose)2106 int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int fStart, int fCheckMiter, int fVerbose )
2107 {
2108 // extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
2109 Aig_Man_t * pTemp;
2110 Gia_Man_t * pSrm, * pReduce, * pAux;
2111 int nIter, nStart = 0;
2112 if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
2113 {
2114 Abc_Print( 1, "Gia_CommandSpecI(): Equivalence classes are not defined.\n" );
2115 return 0;
2116 }
2117 // (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim
2118 Gia_ManCleanMark0( pGia );
2119 Gia_ManPrintStats( pGia, NULL );
2120 for ( nIter = 0; ; nIter++ )
2121 {
2122 if ( Gia_ManHasNoEquivs(pGia) )
2123 {
2124 Abc_Print( 1, "Gia_CommandSpecI: No equivalences left.\n" );
2125 break;
2126 }
2127 Abc_Print( 1, "ITER %3d : ", nIter );
2128 // if ( fVerbose )
2129 // Abc_Print( 1, "Starting BMC from frame %d.\n", nStart );
2130 // if ( fVerbose )
2131 // Gia_ManPrintStats( pGia, 0 );
2132 Gia_ManPrintStatsClasses( pGia );
2133 // perform speculative reduction
2134 // if ( Gia_ManPoNum(pSrm) <= Gia_ManPoNum(pGia) )
2135 if ( !Cec_ManCheckNonTrivialCands(pGia) )
2136 {
2137 Abc_Print( 1, "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
2138 break;
2139 }
2140 pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
2141 // bmc2 -F 100 -C 25000
2142 {
2143 Abc_Cex_t * pCex;
2144 int nFrames = nFramesInit; // different from default
2145 int nNodeDelta = 2000;
2146 int nBTLimit = nBTLimitInit; // different from default
2147 int nBTLimitAll = 2000000;
2148 pTemp = Gia_ManToAig( pSrm, 0 );
2149 // Aig_ManPrintStats( pTemp );
2150 Gia_ManStop( pSrm );
2151 Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVerbose, 0, NULL, 0, 0 );
2152 pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
2153 Aig_ManStop( pTemp );
2154 if ( pCex == NULL )
2155 {
2156 Abc_Print( 1, "Gia_CommandSpecI(): Internal BMC could not find a counter-example.\n" );
2157 break;
2158 }
2159 if ( fStart )
2160 nStart = pCex->iFrame;
2161 // perform simulation
2162 {
2163 Cec_ParSim_t Pars, * pPars = &Pars;
2164 Cec_ManSimSetDefaultParams( pPars );
2165 pPars->fCheckMiter = fCheckMiter;
2166 if ( Cec_ManSeqResimulateCounter( pGia, pPars, pCex ) )
2167 {
2168 ABC_FREE( pCex );
2169 break;
2170 }
2171 ABC_FREE( pCex );
2172 }
2173 }
2174 // write equivalence classes
2175 Gia_AigerWrite( pGia, "gore.aig", 0, 0, 0 );
2176 // reduce the model
2177 pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
2178 if ( pReduce )
2179 {
2180 pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
2181 Gia_ManStop( pAux );
2182 Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0, 0 );
2183 // Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
2184 // Gia_ManPrintStatsShort( pReduce );
2185 Gia_ManStop( pReduce );
2186 }
2187 }
2188 return 1;
2189 }
2190
2191
2192
2193
2194 /**Function*************************************************************
2195
2196 Synopsis [Reduces AIG using equivalence classes.]
2197
2198 Description []
2199
2200 SideEffects []
2201
2202 SeeAlso []
2203
2204 ***********************************************************************/
Gia_ManFilterEquivsForSpeculation(Gia_Man_t * pGia,char * pName1,char * pName2,int fLatchA,int fLatchB)2205 int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * pName2, int fLatchA, int fLatchB )
2206 {
2207 Gia_Man_t * pGia1, * pGia2, * pMiter;
2208 Gia_Obj_t * pObj1, * pObj2, * pObjM, * pObj;
2209 int i, iObj, iNext, Counter = 0;
2210 if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
2211 {
2212 Abc_Print( 1, "Equivalences are not defined.\n" );
2213 return 0;
2214 }
2215 pGia1 = Gia_AigerRead( pName1, 0, 0, 0 );
2216 if ( pGia1 == NULL )
2217 {
2218 Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
2219 return 0;
2220 }
2221 pGia2 = Gia_AigerRead( pName2, 0, 0, 0 );
2222 if ( pGia2 == NULL )
2223 {
2224 Gia_ManStop( pGia2 );
2225 Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
2226 return 0;
2227 }
2228 pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 );
2229 if ( pMiter == NULL )
2230 {
2231 Gia_ManStop( pGia1 );
2232 Gia_ManStop( pGia2 );
2233 Abc_Print( 1, "Cannot create sequential miter.\n" );
2234 return 0;
2235 }
2236 // make sure the miter is isomorphic
2237 if ( Gia_ManObjNum(pGia) != Gia_ManObjNum(pMiter) )
2238 {
2239 Gia_ManStop( pGia1 );
2240 Gia_ManStop( pGia2 );
2241 Gia_ManStop( pMiter );
2242 Abc_Print( 1, "The number of objects in different.\n" );
2243 return 0;
2244 }
2245 if ( memcmp( pGia->pObjs, pMiter->pObjs, sizeof(Gia_Obj_t) * Gia_ManObjNum(pGia) ) )
2246 {
2247 Gia_ManStop( pGia1 );
2248 Gia_ManStop( pGia2 );
2249 Gia_ManStop( pMiter );
2250 Abc_Print( 1, "The AIG structure of the miter does not match.\n" );
2251 return 0;
2252 }
2253 // transfer copies
2254 Gia_ManCleanMark0( pGia );
2255 Gia_ManForEachObj( pGia1, pObj1, i )
2256 {
2257 if ( pObj1->Value == ~0 )
2258 continue;
2259 pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) );
2260 pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
2261 pObj->fMark0 = 1;
2262 }
2263 Gia_ManCleanMark1( pGia );
2264 Gia_ManForEachObj( pGia2, pObj2, i )
2265 {
2266 if ( pObj2->Value == ~0 )
2267 continue;
2268 pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) );
2269 pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
2270 pObj->fMark1 = 1;
2271 }
2272
2273 // filter equivalences
2274 Gia_ManForEachConst( pGia, i )
2275 {
2276 Gia_ObjUnsetRepr( pGia, i );
2277 assert( pGia->pNexts[i] == 0 );
2278 }
2279 Gia_ManForEachClass( pGia, i )
2280 {
2281 // find the first colorA and colorB
2282 int ClassA = -1, ClassB = -1;
2283 Gia_ClassForEachObj( pGia, i, iObj )
2284 {
2285 pObj = Gia_ManObj( pGia, iObj );
2286 if ( ClassA == -1 && pObj->fMark0 && !pObj->fMark1 )
2287 {
2288 if ( fLatchA && !Gia_ObjIsRo(pGia, pObj) )
2289 continue;
2290 ClassA = iObj;
2291 }
2292 if ( ClassB == -1 && pObj->fMark1 && !pObj->fMark0 )
2293 {
2294 if ( fLatchB && !Gia_ObjIsRo(pGia, pObj) )
2295 continue;
2296 ClassB = iObj;
2297 }
2298 }
2299 // undo equivalence classes
2300 for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
2301 iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
2302 {
2303 Gia_ObjUnsetRepr( pGia, iObj );
2304 Gia_ObjSetNext( pGia, iObj, 0 );
2305 }
2306 assert( !Gia_ObjIsHead(pGia, i) );
2307 if ( ClassA > 0 && ClassB > 0 )
2308 {
2309 if ( ClassA > ClassB )
2310 {
2311 ClassA ^= ClassB;
2312 ClassB ^= ClassA;
2313 ClassA ^= ClassB;
2314 }
2315 assert( ClassA < ClassB );
2316 Gia_ObjSetNext( pGia, ClassA, ClassB );
2317 Gia_ObjSetRepr( pGia, ClassB, ClassA );
2318 Counter++;
2319 assert( Gia_ObjIsHead(pGia, ClassA) );
2320 }
2321 }
2322 Abc_Print( 1, "The number of two-node classes after filtering = %d.\n", Counter );
2323 //Gia_ManEquivPrintClasses( pGia, 1, 0 );
2324
2325 Gia_ManCleanMark0( pGia );
2326 Gia_ManCleanMark1( pGia );
2327 return 1;
2328 }
2329
2330
2331 /**Function*************************************************************
2332
2333 Synopsis [Reduces AIG using equivalence classes.]
2334
2335 Description []
2336
2337 SideEffects []
2338
2339 SeeAlso []
2340
2341 ***********************************************************************/
Gia_ManFilterEquivsUsingParts(Gia_Man_t * pGia,char * pName1,char * pName2)2342 int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName2 )
2343 {
2344 Vec_Int_t * vNodes;
2345 Gia_Man_t * pGia1, * pGia2, * pMiter;
2346 Gia_Obj_t * pObj1, * pObj2, * pObjM, * pObj = NULL;
2347 int i, k, iObj, iNext, iPrev, iRepr;
2348 int iLitsOld, iLitsNew;
2349 if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
2350 {
2351 Abc_Print( 1, "Equivalences are not defined.\n" );
2352 return 0;
2353 }
2354 pGia1 = Gia_AigerRead( pName1, 0, 0, 0 );
2355 if ( pGia1 == NULL )
2356 {
2357 Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
2358 return 0;
2359 }
2360 pGia2 = Gia_AigerRead( pName2, 0, 0, 0 );
2361 if ( pGia2 == NULL )
2362 {
2363 Gia_ManStop( pGia2 );
2364 Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
2365 return 0;
2366 }
2367 pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 );
2368 if ( pMiter == NULL )
2369 {
2370 Gia_ManStop( pGia1 );
2371 Gia_ManStop( pGia2 );
2372 Abc_Print( 1, "Cannot create sequential miter.\n" );
2373 return 0;
2374 }
2375 // make sure the miter is isomorphic
2376 if ( Gia_ManObjNum(pGia) != Gia_ManObjNum(pMiter) )
2377 {
2378 Gia_ManStop( pGia1 );
2379 Gia_ManStop( pGia2 );
2380 Gia_ManStop( pMiter );
2381 Abc_Print( 1, "The number of objects in different.\n" );
2382 return 0;
2383 }
2384 if ( memcmp( pGia->pObjs, pMiter->pObjs, sizeof(Gia_Obj_t) * Gia_ManObjNum(pGia) ) )
2385 {
2386 Gia_ManStop( pGia1 );
2387 Gia_ManStop( pGia2 );
2388 Gia_ManStop( pMiter );
2389 Abc_Print( 1, "The AIG structure of the miter does not match.\n" );
2390 return 0;
2391 }
2392 // transfer copies
2393 Gia_ManCleanMark0( pGia );
2394 Gia_ManForEachObj( pGia1, pObj1, i )
2395 {
2396 if ( pObj1->Value == ~0 )
2397 continue;
2398 pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) );
2399 pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
2400 pObj->fMark0 = 1;
2401 }
2402 Gia_ManCleanMark1( pGia );
2403 Gia_ManForEachObj( pGia2, pObj2, i )
2404 {
2405 if ( pObj2->Value == ~0 )
2406 continue;
2407 pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) );
2408 pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
2409 pObj->fMark1 = 1;
2410 }
2411
2412 // filter equivalences
2413 iLitsOld = iLitsNew = 0;
2414 Gia_ManForEachConst( pGia, i )
2415 {
2416 iLitsOld++;
2417 pObj = Gia_ManObj( pGia, i );
2418 assert( pGia->pNexts[i] == 0 );
2419 assert( pObj->fMark0 || pObj->fMark1 );
2420 if ( pObj->fMark0 && pObj->fMark1 ) // belongs to both A and B
2421 Gia_ObjUnsetRepr( pGia, i );
2422 else
2423 iLitsNew++;
2424 }
2425 // filter equivalences
2426 vNodes = Vec_IntAlloc( 100 );
2427 Gia_ManForEachClass( pGia, i )
2428 {
2429 int fSeenA = 0, fSeenB = 0;
2430 assert( pObj->fMark0 || pObj->fMark1 );
2431 Vec_IntClear( vNodes );
2432 Gia_ClassForEachObj( pGia, i, iObj )
2433 {
2434 pObj = Gia_ManObj( pGia, iObj );
2435 if ( pObj->fMark0 && !pObj->fMark1 )
2436 {
2437 fSeenA = 1;
2438 Vec_IntPush( vNodes, iObj );
2439 }
2440 if ( !pObj->fMark0 && pObj->fMark1 )
2441 {
2442 fSeenB = 1;
2443 Vec_IntPush( vNodes, iObj );
2444 }
2445 iLitsOld++;
2446 }
2447 iLitsOld--;
2448 // undo equivalence classes
2449 for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
2450 iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
2451 {
2452 Gia_ObjUnsetRepr( pGia, iObj );
2453 Gia_ObjSetNext( pGia, iObj, 0 );
2454 }
2455 assert( !Gia_ObjIsHead(pGia, i) );
2456 if ( fSeenA && fSeenB && Vec_IntSize(vNodes) > 1 )
2457 {
2458 // create new class
2459 iPrev = iRepr = Vec_IntEntry( vNodes, 0 );
2460 Vec_IntForEachEntryStart( vNodes, iObj, k, 1 )
2461 {
2462 Gia_ObjSetRepr( pGia, iObj, iRepr );
2463 Gia_ObjSetNext( pGia, iPrev, iObj );
2464 iPrev = iObj;
2465 iLitsNew++;
2466 }
2467 assert( Gia_ObjNext(pGia, iPrev) == 0 );
2468 }
2469 }
2470 Vec_IntFree( vNodes );
2471 Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew );
2472 //Gia_ManEquivPrintClasses( pGia, 1, 0 );
2473
2474 Gia_ManCleanMark0( pGia );
2475 Gia_ManCleanMark1( pGia );
2476 return 1;
2477 }
2478
2479 /**Function*************************************************************
2480
2481 Synopsis []
2482
2483 Description []
2484
2485 SideEffects []
2486
2487 SeeAlso []
2488
2489 ***********************************************************************/
Gia_ManFilterEquivsUsingLatches(Gia_Man_t * pGia,int fFlopsOnly,int fFlopsWith,int fUseRiDrivers)2490 void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlopsWith, int fUseRiDrivers )
2491 {
2492 Gia_Obj_t * pObjR;
2493 Vec_Int_t * vNodes, * vFfIds;
2494 int i, k, iObj, iNext, iPrev, iRepr;
2495 int iLitsOld = 0, iLitsNew = 0;
2496 assert( fFlopsOnly ^ fFlopsWith );
2497 vNodes = Vec_IntAlloc( 100 );
2498 // select nodes "flop" node IDs
2499 vFfIds = Vec_IntStart( Gia_ManObjNum(pGia) );
2500 if ( fUseRiDrivers )
2501 {
2502 Gia_ManForEachRi( pGia, pObjR, i )
2503 Vec_IntWriteEntry( vFfIds, Gia_ObjFaninId0p(pGia, pObjR), 1 );
2504 }
2505 else
2506 {
2507 Gia_ManForEachRo( pGia, pObjR, i )
2508 Vec_IntWriteEntry( vFfIds, Gia_ObjId(pGia, pObjR), 1 );
2509 }
2510 // remove all non-flop constants
2511 Gia_ManForEachConst( pGia, i )
2512 {
2513 iLitsOld++;
2514 assert( pGia->pNexts[i] == 0 );
2515 if ( !Vec_IntEntry(vFfIds, i) )
2516 Gia_ObjUnsetRepr( pGia, i );
2517 else
2518 iLitsNew++;
2519 }
2520 // clear the classes
2521 if ( fFlopsOnly )
2522 {
2523 Gia_ManForEachClass( pGia, i )
2524 {
2525 Vec_IntClear( vNodes );
2526 Gia_ClassForEachObj( pGia, i, iObj )
2527 {
2528 if ( Vec_IntEntry(vFfIds, iObj) )
2529 Vec_IntPush( vNodes, iObj );
2530 iLitsOld++;
2531 }
2532 iLitsOld--;
2533 // undo equivalence classes
2534 for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
2535 iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
2536 {
2537 Gia_ObjUnsetRepr( pGia, iObj );
2538 Gia_ObjSetNext( pGia, iObj, 0 );
2539 }
2540 assert( !Gia_ObjIsHead(pGia, i) );
2541 if ( Vec_IntSize(vNodes) > 1 )
2542 {
2543 // create new class
2544 iPrev = iRepr = Vec_IntEntry( vNodes, 0 );
2545 Vec_IntForEachEntryStart( vNodes, iObj, k, 1 )
2546 {
2547 Gia_ObjSetRepr( pGia, iObj, iRepr );
2548 Gia_ObjSetNext( pGia, iPrev, iObj );
2549 iPrev = iObj;
2550 iLitsNew++;
2551 }
2552 assert( Gia_ObjNext(pGia, iPrev) == 0 );
2553 }
2554 }
2555 }
2556 else
2557 {
2558 Gia_ManForEachClass( pGia, i )
2559 {
2560 int fSeenFlop = 0;
2561 Gia_ClassForEachObj( pGia, i, iObj )
2562 {
2563 if ( Vec_IntEntry(vFfIds, iObj) )
2564 fSeenFlop = 1;
2565 iLitsOld++;
2566 iLitsNew++;
2567 }
2568 iLitsOld--;
2569 iLitsNew--;
2570 if ( fSeenFlop )
2571 continue;
2572 // undo equivalence classes
2573 for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj;
2574 iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) )
2575 {
2576 Gia_ObjUnsetRepr( pGia, iObj );
2577 Gia_ObjSetNext( pGia, iObj, 0 );
2578 iLitsNew--;
2579 }
2580 iLitsNew++;
2581 assert( !Gia_ObjIsHead(pGia, i) );
2582 }
2583 }
2584 Vec_IntFree( vNodes );
2585 Vec_IntFree( vFfIds );
2586 Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew );
2587 }
2588
2589 ////////////////////////////////////////////////////////////////////////
2590 /// END OF FILE ///
2591 ////////////////////////////////////////////////////////////////////////
2592
2593
2594 ABC_NAMESPACE_IMPL_END
2595