1 /**CFile****************************************************************
2
3 FileName [saigDup.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Sequential AIG package.]
8
9 Synopsis [Various duplication procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: saigDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "saig.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Duplicates while ORing the POs of sequential circuit.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Saig_ManDupOrpos(Aig_Man_t * pAig)45 Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * pAig )
46 {
47 Aig_Man_t * pAigNew;
48 Aig_Obj_t * pObj, * pMiter;
49 int i;
50 if ( pAig->nConstrs > 0 )
51 {
52 printf( "The AIG manager should have no constraints.\n" );
53 return NULL;
54 }
55 // start the new manager
56 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
57 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
58 pAigNew->nConstrs = pAig->nConstrs;
59 // map the constant node
60 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
61 // create variables for PIs
62 Aig_ManForEachCi( pAig, pObj, i )
63 pObj->pData = Aig_ObjCreateCi( pAigNew );
64 // add internal nodes of this frame
65 Aig_ManForEachNode( pAig, pObj, i )
66 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
67 // create PO of the circuit
68 pMiter = Aig_ManConst0( pAigNew );
69 Saig_ManForEachPo( pAig, pObj, i )
70 pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) );
71 Aig_ObjCreateCo( pAigNew, pMiter );
72 // transfer to register outputs
73 Saig_ManForEachLi( pAig, pObj, i )
74 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
75 Aig_ManCleanup( pAigNew );
76 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
77 return pAigNew;
78 }
79
80 /**Function*************************************************************
81
82 Synopsis [Duplicates while ORing the POs of sequential circuit.]
83
84 Description []
85
86 SideEffects []
87
88 SeeAlso []
89
90 ***********************************************************************/
Saig_ManCreateEquivMiter(Aig_Man_t * pAig,Vec_Int_t * vPairs,int fAddOuts)91 Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs, int fAddOuts )
92 {
93 Aig_Man_t * pAigNew;
94 Aig_Obj_t * pObj, * pObj2, * pMiter;
95 int i;
96 if ( pAig->nConstrs > 0 )
97 {
98 printf( "The AIG manager should have no constraints.\n" );
99 return NULL;
100 }
101 // start the new manager
102 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
103 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
104 pAigNew->nConstrs = pAig->nConstrs;
105 // map the constant node
106 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
107 // create variables for PIs
108 Aig_ManForEachCi( pAig, pObj, i )
109 pObj->pData = Aig_ObjCreateCi( pAigNew );
110 // add internal nodes of this frame
111 Aig_ManForEachNode( pAig, pObj, i )
112 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
113 // create POs
114 assert( Vec_IntSize(vPairs) % 2 == 0 );
115 Aig_ManForEachObjVec( vPairs, pAig, pObj, i )
116 {
117 pObj2 = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) );
118 pMiter = Aig_Exor( pAigNew, (Aig_Obj_t *)pObj->pData, (Aig_Obj_t *)pObj2->pData );
119 pMiter = Aig_NotCond( pMiter, pObj->fPhase ^ pObj2->fPhase );
120 Aig_ObjCreateCo( pAigNew, pMiter );
121 }
122 // transfer to register outputs
123 if ( fAddOuts )
124 Saig_ManForEachLi( pAig, pObj, i )
125 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
126 Aig_ManCleanup( pAigNew );
127 if ( fAddOuts )
128 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
129 return pAigNew;
130 }
131
132 /**Function*************************************************************
133
134 Synopsis [Trims the model by removing PIs without fanout.]
135
136 Description []
137
138 SideEffects []
139
140 SeeAlso []
141
142 ***********************************************************************/
Saig_ManTrimPis(Aig_Man_t * p)143 Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p )
144 {
145 Aig_Man_t * pNew;
146 Aig_Obj_t * pObj;
147 int i, fAllPisHaveNoRefs;
148 // check the refs of PIs
149 fAllPisHaveNoRefs = 1;
150 Saig_ManForEachPi( p, pObj, i )
151 if ( pObj->nRefs )
152 fAllPisHaveNoRefs = 0;
153 // start the new manager
154 pNew = Aig_ManStart( Aig_ManObjNum(p) );
155 pNew->pName = Abc_UtilStrsav( p->pName );
156 pNew->nConstrs = p->nConstrs;
157 // start mapping of the CI numbers
158 pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) );
159 // map const and primary inputs
160 Aig_ManCleanData( p );
161 Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
162 Aig_ManForEachCi( p, pObj, i )
163 if ( fAllPisHaveNoRefs || pObj->nRefs || Saig_ObjIsLo(p, pObj) )
164 {
165 pObj->pData = Aig_ObjCreateCi( pNew );
166 Vec_IntPush( pNew->vCiNumsOrig, Vec_IntEntry(p->vCiNumsOrig, i) );
167 }
168 Aig_ManForEachNode( p, pObj, i )
169 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
170 Aig_ManForEachCo( p, pObj, i )
171 pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
172 Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
173 return pNew;
174 }
175
176 /**Function*************************************************************
177
178 Synopsis [Duplicates the AIG manager recursively.]
179
180 Description []
181
182 SideEffects []
183
184 SeeAlso []
185
186 ***********************************************************************/
Saig_ManAbstractionDfs_rec(Aig_Man_t * pNew,Aig_Obj_t * pObj)187 Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
188 {
189 if ( pObj->pData )
190 return (Aig_Obj_t *)pObj->pData;
191 Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
192 Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) );
193 return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
194 }
195
196 /**Function*************************************************************
197
198 Synopsis [Performs abstraction of the AIG to preserve the included flops.]
199
200 Description []
201
202 SideEffects []
203
204 SeeAlso []
205
206 ***********************************************************************/
Saig_ManDupAbstraction(Aig_Man_t * p,Vec_Int_t * vFlops)207 Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops )
208 {
209 Aig_Man_t * pNew;//, * pTemp;
210 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
211 int i, Entry;
212 Aig_ManCleanData( p );
213 // start the new manager
214 pNew = Aig_ManStart( 5000 );
215 pNew->pName = Abc_UtilStrsav( p->pName );
216 // map the constant node
217 Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
218 // label included flops
219 Vec_IntForEachEntry( vFlops, Entry, i )
220 {
221 pObjLi = Saig_ManLi( p, Entry );
222 assert( pObjLi->fMarkA == 0 );
223 pObjLi->fMarkA = 1;
224 pObjLo = Saig_ManLo( p, Entry );
225 assert( pObjLo->fMarkA == 0 );
226 pObjLo->fMarkA = 1;
227 }
228 // create variables for PIs
229 assert( p->vCiNumsOrig == NULL );
230 pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) );
231 Aig_ManForEachCi( p, pObj, i )
232 if ( !pObj->fMarkA )
233 {
234 pObj->pData = Aig_ObjCreateCi( pNew );
235 Vec_IntPush( pNew->vCiNumsOrig, i );
236 }
237 // create variables for LOs
238 Aig_ManForEachCi( p, pObj, i )
239 if ( pObj->fMarkA )
240 {
241 pObj->fMarkA = 0;
242 pObj->pData = Aig_ObjCreateCi( pNew );
243 Vec_IntPush( pNew->vCiNumsOrig, i );
244 }
245 // add internal nodes
246 // Aig_ManForEachNode( p, pObj, i )
247 // pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
248 // create POs
249 Saig_ManForEachPo( p, pObj, i )
250 {
251 Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
252 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
253 }
254 // create LIs
255 Aig_ManForEachCo( p, pObj, i )
256 if ( pObj->fMarkA )
257 {
258 pObj->fMarkA = 0;
259 Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
260 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
261 }
262 Aig_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
263 Aig_ManSeqCleanup( pNew );
264 // remove PIs without fanout
265 // pNew = Saig_ManTrimPis( pTemp = pNew );
266 // Aig_ManStop( pTemp );
267 return pNew;
268 }
269
270 /**Function*************************************************************
271
272 Synopsis [Resimulates the counter-example.]
273
274 Description []
275
276 SideEffects []
277
278 SeeAlso []
279
280 ***********************************************************************/
Saig_ManVerifyCex(Aig_Man_t * pAig,Abc_Cex_t * p)281 int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
282 {
283 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
284 int RetValue, i, k, iBit = 0;
285 Aig_ManCleanMarkB(pAig);
286 Aig_ManConst1(pAig)->fMarkB = 1;
287 Saig_ManForEachLo( pAig, pObj, i )
288 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
289 for ( i = 0; i <= p->iFrame; i++ )
290 {
291 Saig_ManForEachPi( pAig, pObj, k )
292 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
293 Aig_ManForEachNode( pAig, pObj, k )
294 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
295 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
296 Aig_ManForEachCo( pAig, pObj, k )
297 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
298 if ( i == p->iFrame )
299 break;
300 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
301 pObjRo->fMarkB = pObjRi->fMarkB;
302 }
303 assert( iBit == p->nBits );
304 RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
305 Aig_ManCleanMarkB(pAig);
306 return RetValue;
307 }
308
309 /**Function*************************************************************
310
311 Synopsis [Resimulates the counter-example.]
312
313 Description []
314
315 SideEffects []
316
317 SeeAlso []
318
319 ***********************************************************************/
Saig_ManVerifyCexNoClear(Aig_Man_t * pAig,Abc_Cex_t * p)320 int Saig_ManVerifyCexNoClear( Aig_Man_t * pAig, Abc_Cex_t * p )
321 {
322 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
323 int RetValue, i, k, iBit = 0;
324 Aig_ManCleanMarkB(pAig);
325 Aig_ManConst1(pAig)->fMarkB = 1;
326 Saig_ManForEachLo( pAig, pObj, i )
327 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
328 for ( i = 0; i <= p->iFrame; i++ )
329 {
330 Saig_ManForEachPi( pAig, pObj, k )
331 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
332 Aig_ManForEachNode( pAig, pObj, k )
333 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
334 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
335 Aig_ManForEachCo( pAig, pObj, k )
336 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
337 if ( i == p->iFrame )
338 break;
339 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
340 pObjRo->fMarkB = pObjRi->fMarkB;
341 }
342 assert( iBit == p->nBits );
343 RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
344 //Aig_ManCleanMarkB(pAig);
345 return RetValue;
346 }
Saig_ManReturnFailingState(Aig_Man_t * pAig,Abc_Cex_t * p,int fNextOne)347 Vec_Int_t * Saig_ManReturnFailingState( Aig_Man_t * pAig, Abc_Cex_t * p, int fNextOne )
348 {
349 Aig_Obj_t * pObj;
350 Vec_Int_t * vState;
351 int i, RetValue = Saig_ManVerifyCexNoClear( pAig, p );
352 if ( RetValue == 0 )
353 {
354 Aig_ManCleanMarkB(pAig);
355 printf( "CEX does fail the given sequential miter.\n" );
356 return NULL;
357 }
358 vState = Vec_IntAlloc( Aig_ManRegNum(pAig) );
359 if ( fNextOne )
360 {
361 Saig_ManForEachLi( pAig, pObj, i )
362 Vec_IntPush( vState, pObj->fMarkB );
363 }
364 else
365 {
366 Saig_ManForEachLo( pAig, pObj, i )
367 Vec_IntPush( vState, pObj->fMarkB );
368 }
369 Aig_ManCleanMarkB(pAig);
370 return vState;
371 }
372
373 /**Function*************************************************************
374
375 Synopsis [Resimulates the counter-example.]
376
377 Description []
378
379 SideEffects []
380
381 SeeAlso []
382
383 ***********************************************************************/
Saig_ManExtendCex(Aig_Man_t * pAig,Abc_Cex_t * p)384 Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p )
385 {
386 Abc_Cex_t * pNew;
387 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
388 int RetValue, i, k, iBit = 0;
389 // create new counter-example
390 pNew = Abc_CexAlloc( 0, Aig_ManCiNum(pAig), p->iFrame + 1 );
391 pNew->iPo = p->iPo;
392 pNew->iFrame = p->iFrame;
393 // simulate the AIG
394 Aig_ManCleanMarkB(pAig);
395 Aig_ManConst1(pAig)->fMarkB = 1;
396 Saig_ManForEachLo( pAig, pObj, i )
397 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
398 for ( i = 0; i <= p->iFrame; i++ )
399 {
400 Saig_ManForEachPi( pAig, pObj, k )
401 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
402 ///////// write PI+LO values ////////////
403 Aig_ManForEachCi( pAig, pObj, k )
404 if ( pObj->fMarkB )
405 Abc_InfoSetBit(pNew->pData, Aig_ManCiNum(pAig)*i + k);
406 /////////////////////////////////////////
407 Aig_ManForEachNode( pAig, pObj, k )
408 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
409 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
410 Aig_ManForEachCo( pAig, pObj, k )
411 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
412 if ( i == p->iFrame )
413 break;
414 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
415 pObjRo->fMarkB = pObjRi->fMarkB;
416 }
417 assert( iBit == p->nBits );
418 RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
419 Aig_ManCleanMarkB(pAig);
420 if ( RetValue == 0 )
421 printf( "Saig_ManExtendCex(): The counter-example is invalid!!!\n" );
422 return pNew;
423 }
424
425 /**Function*************************************************************
426
427 Synopsis [Resimulates the counter-example.]
428
429 Description []
430
431 SideEffects []
432
433 SeeAlso []
434
435 ***********************************************************************/
Saig_ManFindFailedPoCex(Aig_Man_t * pAig,Abc_Cex_t * p)436 int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p )
437 {
438 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
439 int RetValue, i, k, iBit = 0;
440 Aig_ManCleanMarkB(pAig);
441 Aig_ManConst1(pAig)->fMarkB = 1;
442 Saig_ManForEachLo( pAig, pObj, i )
443 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
444 for ( i = 0; i <= p->iFrame; i++ )
445 {
446 Saig_ManForEachPi( pAig, pObj, k )
447 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
448 Aig_ManForEachNode( pAig, pObj, k )
449 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
450 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
451 Aig_ManForEachCo( pAig, pObj, k )
452 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
453 if ( i == p->iFrame )
454 break;
455 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
456 pObjRo->fMarkB = pObjRi->fMarkB;
457 }
458 assert( iBit == p->nBits );
459 // remember the number of failed output
460 RetValue = -1;
461 Saig_ManForEachPo( pAig, pObj, i )
462 if ( pObj->fMarkB )
463 {
464 RetValue = i;
465 break;
466 }
467 Aig_ManCleanMarkB(pAig);
468 return RetValue;
469 }
470
471 /**Function*************************************************************
472
473 Synopsis [Duplicates while ORing the POs of sequential circuit.]
474
475 Description []
476
477 SideEffects []
478
479 SeeAlso []
480
481 ***********************************************************************/
Saig_ManDupWithPhase(Aig_Man_t * pAig,Vec_Int_t * vInit)482 Aig_Man_t * Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit )
483 {
484 Aig_Man_t * pAigNew;
485 Aig_Obj_t * pObj;
486 int i;
487 assert( Aig_ManRegNum(pAig) <= Vec_IntSize(vInit) );
488 // start the new manager
489 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
490 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
491 pAigNew->nConstrs = pAig->nConstrs;
492 // map the constant node
493 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
494 // create variables for PIs
495 Aig_ManForEachCi( pAig, pObj, i )
496 pObj->pData = Aig_ObjCreateCi( pAigNew );
497 // update the flop variables
498 Saig_ManForEachLo( pAig, pObj, i )
499 pObj->pData = Aig_NotCond( (Aig_Obj_t *)pObj->pData, Vec_IntEntry(vInit, i) );
500 // add internal nodes of this frame
501 Aig_ManForEachNode( pAig, pObj, i )
502 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
503 // transfer to register outputs
504 Saig_ManForEachPo( pAig, pObj, i )
505 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
506 // update the flop variables
507 Saig_ManForEachLi( pAig, pObj, i )
508 Aig_ObjCreateCo( pAigNew, Aig_NotCond(Aig_ObjChild0Copy(pObj), Vec_IntEntry(vInit, i)) );
509 // finalize
510 Aig_ManCleanup( pAigNew );
511 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
512 return pAigNew;
513 }
514
515 /**Function*************************************************************
516
517 Synopsis [Copy an AIG structure related to the selected POs.]
518
519 Description []
520
521 SideEffects []
522
523 SeeAlso []
524
525 ***********************************************************************/
Saig_ManDupCones_rec(Aig_Man_t * p,Aig_Obj_t * pObj,Vec_Ptr_t * vLeaves,Vec_Ptr_t * vNodes,Vec_Ptr_t * vRoots)526 void Saig_ManDupCones_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vRoots )
527 {
528 if ( Aig_ObjIsTravIdCurrent(p, pObj) )
529 return;
530 Aig_ObjSetTravIdCurrent(p, pObj);
531 if ( Aig_ObjIsNode(pObj) )
532 {
533 Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
534 Saig_ManDupCones_rec( p, Aig_ObjFanin1(pObj), vLeaves, vNodes, vRoots );
535 Vec_PtrPush( vNodes, pObj );
536 }
537 else if ( Aig_ObjIsCo(pObj) )
538 Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
539 else if ( Saig_ObjIsLo(p, pObj) )
540 Vec_PtrPush( vRoots, Saig_ObjLoToLi(p, pObj) );
541 else if ( Saig_ObjIsPi(p, pObj) )
542 Vec_PtrPush( vLeaves, pObj );
543 else assert( 0 );
544 }
Saig_ManDupCones(Aig_Man_t * pAig,int * pPos,int nPos)545 Aig_Man_t * Saig_ManDupCones( Aig_Man_t * pAig, int * pPos, int nPos )
546 {
547 Aig_Man_t * pAigNew;
548 Vec_Ptr_t * vLeaves, * vNodes, * vRoots;
549 Aig_Obj_t * pObj;
550 int i;
551
552 // collect initial POs
553 vLeaves = Vec_PtrAlloc( 100 );
554 vNodes = Vec_PtrAlloc( 100 );
555 vRoots = Vec_PtrAlloc( 100 );
556 for ( i = 0; i < nPos; i++ )
557 Vec_PtrPush( vRoots, Aig_ManCo(pAig, pPos[i]) );
558
559 // mark internal nodes
560 Aig_ManIncrementTravId( pAig );
561 Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
562 Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
563 Saig_ManDupCones_rec( pAig, pObj, vLeaves, vNodes, vRoots );
564
565 // start the new manager
566 pAigNew = Aig_ManStart( Vec_PtrSize(vNodes) );
567 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
568 // map the constant node
569 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
570 // create PIs
571 Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
572 pObj->pData = Aig_ObjCreateCi( pAigNew );
573 // create LOs
574 Vec_PtrForEachEntryStart( Aig_Obj_t *, vRoots, pObj, i, nPos )
575 Saig_ObjLiToLo(pAig, pObj)->pData = Aig_ObjCreateCi( pAigNew );
576 // create internal nodes
577 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
578 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
579 // create COs
580 Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
581 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
582 // finalize
583 Aig_ManSetRegNum( pAigNew, Vec_PtrSize(vRoots)-nPos );
584 Vec_PtrFree( vLeaves );
585 Vec_PtrFree( vNodes );
586 Vec_PtrFree( vRoots );
587 return pAigNew;
588
589 }
590
591 #ifndef ABC_USE_CUDD
Aig_ManVerifyUsingBdds(Aig_Man_t * pInit,Saig_ParBbr_t * pPars)592 int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars ) { return 0; }
Bbr_ManSetDefaultParams(Saig_ParBbr_t * p)593 void Bbr_ManSetDefaultParams( Saig_ParBbr_t * p ) {}
594 #endif
595
596 ////////////////////////////////////////////////////////////////////////
597 /// END OF FILE ///
598 ////////////////////////////////////////////////////////////////////////
599
600
601 ABC_NAMESPACE_IMPL_END
602
603