abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigDup.c
Go to the documentation of this file.
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 ***********************************************************************/
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 ***********************************************************************/
91 Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs )
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  Saig_ManForEachLi( pAig, pObj, i )
124  Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
125  Aig_ManCleanup( pAigNew );
126  Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
127  return pAigNew;
128 }
129 
130 /**Function*************************************************************
131 
132  Synopsis [Trims the model by removing PIs without fanout.]
133 
134  Description []
135 
136  SideEffects []
137 
138  SeeAlso []
139 
140 ***********************************************************************/
141 Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p )
142 {
143  Aig_Man_t * pNew;
144  Aig_Obj_t * pObj;
145  int i, fAllPisHaveNoRefs;
146  // check the refs of PIs
147  fAllPisHaveNoRefs = 1;
148  Saig_ManForEachPi( p, pObj, i )
149  if ( pObj->nRefs )
150  fAllPisHaveNoRefs = 0;
151  // start the new manager
152  pNew = Aig_ManStart( Aig_ManObjNum(p) );
153  pNew->pName = Abc_UtilStrsav( p->pName );
154  pNew->nConstrs = p->nConstrs;
155  // start mapping of the CI numbers
156  pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) );
157  // map const and primary inputs
158  Aig_ManCleanData( p );
159  Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
160  Aig_ManForEachCi( p, pObj, i )
161  if ( fAllPisHaveNoRefs || pObj->nRefs || Saig_ObjIsLo(p, pObj) )
162  {
163  pObj->pData = Aig_ObjCreateCi( pNew );
164  Vec_IntPush( pNew->vCiNumsOrig, Vec_IntEntry(p->vCiNumsOrig, i) );
165  }
166  Aig_ManForEachNode( p, pObj, i )
167  pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
168  Aig_ManForEachCo( p, pObj, i )
169  pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
170  Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
171  return pNew;
172 }
173 
174 /**Function*************************************************************
175 
176  Synopsis [Duplicates the AIG manager recursively.]
177 
178  Description []
179 
180  SideEffects []
181 
182  SeeAlso []
183 
184 ***********************************************************************/
185 Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
186 {
187  if ( pObj->pData )
188  return (Aig_Obj_t *)pObj->pData;
189  Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
190  Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) );
191  return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
192 }
193 
194 /**Function*************************************************************
195 
196  Synopsis [Performs abstraction of the AIG to preserve the included flops.]
197 
198  Description []
199 
200  SideEffects []
201 
202  SeeAlso []
203 
204 ***********************************************************************/
205 Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops )
206 {
207  Aig_Man_t * pNew;//, * pTemp;
208  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
209  int i, Entry;
210  Aig_ManCleanData( p );
211  // start the new manager
212  pNew = Aig_ManStart( 5000 );
213  pNew->pName = Abc_UtilStrsav( p->pName );
214  // map the constant node
215  Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
216  // label included flops
217  Vec_IntForEachEntry( vFlops, Entry, i )
218  {
219  pObjLi = Saig_ManLi( p, Entry );
220  assert( pObjLi->fMarkA == 0 );
221  pObjLi->fMarkA = 1;
222  pObjLo = Saig_ManLo( p, Entry );
223  assert( pObjLo->fMarkA == 0 );
224  pObjLo->fMarkA = 1;
225  }
226  // create variables for PIs
227  assert( p->vCiNumsOrig == NULL );
228  pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) );
229  Aig_ManForEachCi( p, pObj, i )
230  if ( !pObj->fMarkA )
231  {
232  pObj->pData = Aig_ObjCreateCi( pNew );
233  Vec_IntPush( pNew->vCiNumsOrig, i );
234  }
235  // create variables for LOs
236  Aig_ManForEachCi( p, pObj, i )
237  if ( pObj->fMarkA )
238  {
239  pObj->fMarkA = 0;
240  pObj->pData = Aig_ObjCreateCi( pNew );
241  Vec_IntPush( pNew->vCiNumsOrig, i );
242  }
243  // add internal nodes
244 // Aig_ManForEachNode( p, pObj, i )
245 // pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
246  // create POs
247  Saig_ManForEachPo( p, pObj, i )
248  {
249  Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
250  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
251  }
252  // create LIs
253  Aig_ManForEachCo( p, pObj, i )
254  if ( pObj->fMarkA )
255  {
256  pObj->fMarkA = 0;
257  Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
258  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
259  }
260  Aig_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
261  Aig_ManSeqCleanup( pNew );
262  // remove PIs without fanout
263 // pNew = Saig_ManTrimPis( pTemp = pNew );
264 // Aig_ManStop( pTemp );
265  return pNew;
266 }
267 
268 /**Function*************************************************************
269 
270  Synopsis [Resimulates the counter-example.]
271 
272  Description []
273 
274  SideEffects []
275 
276  SeeAlso []
277 
278 ***********************************************************************/
279 int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
280 {
281  Aig_Obj_t * pObj, * pObjRi, * pObjRo;
282  int RetValue, i, k, iBit = 0;
283  Aig_ManCleanMarkB(pAig);
284  Aig_ManConst1(pAig)->fMarkB = 1;
285  Saig_ManForEachLo( pAig, pObj, i )
286  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
287  for ( i = 0; i <= p->iFrame; i++ )
288  {
289  Saig_ManForEachPi( pAig, pObj, k )
290  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
291  Aig_ManForEachNode( pAig, pObj, k )
292  pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
293  (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
294  Aig_ManForEachCo( pAig, pObj, k )
295  pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
296  if ( i == p->iFrame )
297  break;
298  Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
299  pObjRo->fMarkB = pObjRi->fMarkB;
300  }
301  assert( iBit == p->nBits );
302  RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
303  Aig_ManCleanMarkB(pAig);
304  return RetValue;
305 }
306 
307 /**Function*************************************************************
308 
309  Synopsis [Resimulates the counter-example.]
310 
311  Description []
312 
313  SideEffects []
314 
315  SeeAlso []
316 
317 ***********************************************************************/
318 int Saig_ManVerifyCexNoClear( Aig_Man_t * pAig, Abc_Cex_t * p )
319 {
320  Aig_Obj_t * pObj, * pObjRi, * pObjRo;
321  int RetValue, i, k, iBit = 0;
322  Aig_ManCleanMarkB(pAig);
323  Aig_ManConst1(pAig)->fMarkB = 1;
324  Saig_ManForEachLo( pAig, pObj, i )
325  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
326  for ( i = 0; i <= p->iFrame; i++ )
327  {
328  Saig_ManForEachPi( pAig, pObj, k )
329  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
330  Aig_ManForEachNode( pAig, pObj, k )
331  pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
332  (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
333  Aig_ManForEachCo( pAig, pObj, k )
334  pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
335  if ( i == p->iFrame )
336  break;
337  Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
338  pObjRo->fMarkB = pObjRi->fMarkB;
339  }
340  assert( iBit == p->nBits );
341  RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
342  //Aig_ManCleanMarkB(pAig);
343  return RetValue;
344 }
345 Vec_Int_t * Saig_ManReturnFailingState( Aig_Man_t * pAig, Abc_Cex_t * p, int fNextOne )
346 {
347  Aig_Obj_t * pObj;
348  Vec_Int_t * vState;
349  int i, RetValue = Saig_ManVerifyCexNoClear( pAig, p );
350  if ( RetValue == 0 )
351  {
352  Aig_ManCleanMarkB(pAig);
353  printf( "CEX does fail the given sequential miter.\n" );
354  return NULL;
355  }
356  vState = Vec_IntAlloc( Aig_ManRegNum(pAig) );
357  if ( fNextOne )
358  {
359  Saig_ManForEachLi( pAig, pObj, i )
360  Vec_IntPush( vState, pObj->fMarkB );
361  }
362  else
363  {
364  Saig_ManForEachLo( pAig, pObj, i )
365  Vec_IntPush( vState, pObj->fMarkB );
366  }
367  Aig_ManCleanMarkB(pAig);
368  return vState;
369 }
370 
371 /**Function*************************************************************
372 
373  Synopsis [Resimulates the counter-example.]
374 
375  Description []
376 
377  SideEffects []
378 
379  SeeAlso []
380 
381 ***********************************************************************/
382 Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p )
383 {
384  Abc_Cex_t * pNew;
385  Aig_Obj_t * pObj, * pObjRi, * pObjRo;
386  int RetValue, i, k, iBit = 0;
387  // create new counter-example
388  pNew = Abc_CexAlloc( 0, Aig_ManCiNum(pAig), p->iFrame + 1 );
389  pNew->iPo = p->iPo;
390  pNew->iFrame = p->iFrame;
391  // simulate the AIG
392  Aig_ManCleanMarkB(pAig);
393  Aig_ManConst1(pAig)->fMarkB = 1;
394  Saig_ManForEachLo( pAig, pObj, i )
395  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
396  for ( i = 0; i <= p->iFrame; i++ )
397  {
398  Saig_ManForEachPi( pAig, pObj, k )
399  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
400  ///////// write PI+LO values ////////////
401  Aig_ManForEachCi( pAig, pObj, k )
402  if ( pObj->fMarkB )
403  Abc_InfoSetBit(pNew->pData, Aig_ManCiNum(pAig)*i + k);
404  /////////////////////////////////////////
405  Aig_ManForEachNode( pAig, pObj, k )
406  pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
407  (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
408  Aig_ManForEachCo( pAig, pObj, k )
409  pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
410  if ( i == p->iFrame )
411  break;
412  Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
413  pObjRo->fMarkB = pObjRi->fMarkB;
414  }
415  assert( iBit == p->nBits );
416  RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
417  Aig_ManCleanMarkB(pAig);
418  if ( RetValue == 0 )
419  printf( "Saig_ManExtendCex(): The counter-example is invalid!!!\n" );
420  return pNew;
421 }
422 
423 /**Function*************************************************************
424 
425  Synopsis [Resimulates the counter-example.]
426 
427  Description []
428 
429  SideEffects []
430 
431  SeeAlso []
432 
433 ***********************************************************************/
434 int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p )
435 {
436  Aig_Obj_t * pObj, * pObjRi, * pObjRo;
437  int RetValue, i, k, iBit = 0;
438  Aig_ManCleanMarkB(pAig);
439  Aig_ManConst1(pAig)->fMarkB = 1;
440  Saig_ManForEachLo( pAig, pObj, i )
441  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
442  for ( i = 0; i <= p->iFrame; i++ )
443  {
444  Saig_ManForEachPi( pAig, pObj, k )
445  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
446  Aig_ManForEachNode( pAig, pObj, k )
447  pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
448  (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
449  Aig_ManForEachCo( pAig, pObj, k )
450  pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
451  if ( i == p->iFrame )
452  break;
453  Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
454  pObjRo->fMarkB = pObjRi->fMarkB;
455  }
456  assert( iBit == p->nBits );
457  // remember the number of failed output
458  RetValue = -1;
459  Saig_ManForEachPo( pAig, pObj, i )
460  if ( pObj->fMarkB )
461  {
462  RetValue = i;
463  break;
464  }
465  Aig_ManCleanMarkB(pAig);
466  return RetValue;
467 }
468 
469 /**Function*************************************************************
470 
471  Synopsis [Duplicates while ORing the POs of sequential circuit.]
472 
473  Description []
474 
475  SideEffects []
476 
477  SeeAlso []
478 
479 ***********************************************************************/
480 Aig_Man_t * Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit )
481 {
482  Aig_Man_t * pAigNew;
483  Aig_Obj_t * pObj;
484  int i;
485  assert( Aig_ManRegNum(pAig) <= Vec_IntSize(vInit) );
486  // start the new manager
487  pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
488  pAigNew->pName = Abc_UtilStrsav( pAig->pName );
489  pAigNew->nConstrs = pAig->nConstrs;
490  // map the constant node
491  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
492  // create variables for PIs
493  Aig_ManForEachCi( pAig, pObj, i )
494  pObj->pData = Aig_ObjCreateCi( pAigNew );
495  // update the flop variables
496  Saig_ManForEachLo( pAig, pObj, i )
497  pObj->pData = Aig_NotCond( (Aig_Obj_t *)pObj->pData, Vec_IntEntry(vInit, i) );
498  // add internal nodes of this frame
499  Aig_ManForEachNode( pAig, pObj, i )
500  pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
501  // transfer to register outputs
502  Saig_ManForEachPo( pAig, pObj, i )
503  Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
504  // update the flop variables
505  Saig_ManForEachLi( pAig, pObj, i )
506  Aig_ObjCreateCo( pAigNew, Aig_NotCond(Aig_ObjChild0Copy(pObj), Vec_IntEntry(vInit, i)) );
507  // finalize
508  Aig_ManCleanup( pAigNew );
509  Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
510  return pAigNew;
511 }
512 
513 /**Function*************************************************************
514 
515  Synopsis [Copy an AIG structure related to the selected POs.]
516 
517  Description []
518 
519  SideEffects []
520 
521  SeeAlso []
522 
523 ***********************************************************************/
524 void Saig_ManDupCones_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vRoots )
525 {
526  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
527  return;
528  Aig_ObjSetTravIdCurrent(p, pObj);
529  if ( Aig_ObjIsNode(pObj) )
530  {
531  Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
532  Saig_ManDupCones_rec( p, Aig_ObjFanin1(pObj), vLeaves, vNodes, vRoots );
533  Vec_PtrPush( vNodes, pObj );
534  }
535  else if ( Aig_ObjIsCo(pObj) )
536  Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
537  else if ( Saig_ObjIsLo(p, pObj) )
538  Vec_PtrPush( vRoots, Saig_ObjLoToLi(p, pObj) );
539  else if ( Saig_ObjIsPi(p, pObj) )
540  Vec_PtrPush( vLeaves, pObj );
541  else assert( 0 );
542 }
543 Aig_Man_t * Saig_ManDupCones( Aig_Man_t * pAig, int * pPos, int nPos )
544 {
545  Aig_Man_t * pAigNew;
546  Vec_Ptr_t * vLeaves, * vNodes, * vRoots;
547  Aig_Obj_t * pObj;
548  int i;
549 
550  // collect initial POs
551  vLeaves = Vec_PtrAlloc( 100 );
552  vNodes = Vec_PtrAlloc( 100 );
553  vRoots = Vec_PtrAlloc( 100 );
554  for ( i = 0; i < nPos; i++ )
555  Vec_PtrPush( vRoots, Aig_ManCo(pAig, pPos[i]) );
556 
557  // mark internal nodes
558  Aig_ManIncrementTravId( pAig );
559  Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
560  Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
561  Saig_ManDupCones_rec( pAig, pObj, vLeaves, vNodes, vRoots );
562 
563  // start the new manager
564  pAigNew = Aig_ManStart( Vec_PtrSize(vNodes) );
565  pAigNew->pName = Abc_UtilStrsav( pAig->pName );
566  // map the constant node
567  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
568  // create PIs
569  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
570  pObj->pData = Aig_ObjCreateCi( pAigNew );
571  // create LOs
572  Vec_PtrForEachEntryStart( Aig_Obj_t *, vRoots, pObj, i, nPos )
573  Saig_ObjLiToLo(pAig, pObj)->pData = Aig_ObjCreateCi( pAigNew );
574  // create internal nodes
575  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
576  pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
577  // create COs
578  Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
579  Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
580  // finalize
581  Aig_ManSetRegNum( pAigNew, Vec_PtrSize(vRoots)-nPos );
582  Vec_PtrFree( vLeaves );
583  Vec_PtrFree( vNodes );
584  Vec_PtrFree( vRoots );
585  return pAigNew;
586 
587 }
588 
589 ////////////////////////////////////////////////////////////////////////
590 /// END OF FILE ///
591 ////////////////////////////////////////////////////////////////////////
592 
593 
594 ABC_NAMESPACE_IMPL_END
595 
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Saig_ManDupOrpos
ABC_NAMESPACE_IMPL_START Aig_Man_t * Saig_ManDupOrpos(Aig_Man_t *pAig)
DECLARATIONS ///.
Definition: saigDup.c:45
Saig_ManTrimPis
Aig_Man_t * Saig_ManTrimPis(Aig_Man_t *p)
Definition: saigDup.c:141
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Saig_ManCreateEquivMiter
Aig_Man_t * Saig_ManCreateEquivMiter(Aig_Man_t *pAig, Vec_Int_t *vPairs)
Definition: saigDup.c:91
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition: aig.h:408
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Saig_ManDupCones_rec
void Saig_ManDupCones_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes, Vec_Ptr_t *vRoots)
Definition: saigDup.c:524
Saig_ManDupAbstraction
Aig_Man_t * Saig_ManDupAbstraction(Aig_Man_t *p, Vec_Int_t *vFlops)
Definition: saigDup.c:205
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Aig_ManSeqCleanup
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition: aigScl.c:158
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Aig_ManObjNum
static int Aig_ManObjNum(Aig_Man_t *p)
Definition: aig.h:258
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition: aig.h:80
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Saig_ManLo
static Aig_Obj_t * Saig_ManLo(Aig_Man_t *p, int i)
Definition: saig.h:79
Aig_Exor
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:220
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_ManCleanMarkB
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition: aigUtil.c:167
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition: aig.h:79
Aig_ManConst0
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Aig_ManObj
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Saig_ManExtendCex
Abc_Cex_t * Saig_ManExtendCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:382
Saig_ManReturnFailingState
Vec_Int_t * Saig_ManReturnFailingState(Aig_Man_t *pAig, Abc_Cex_t *p, int fNextOne)
Definition: saigDup.c:345
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Saig_ManDupCones
Aig_Man_t * Saig_ManDupCones(Aig_Man_t *pAig, int *pPos, int nPos)
Definition: saigDup.c:543
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Saig_ManVerifyCex
int Saig_ManVerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:279
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Saig_ObjLiToLo
static Aig_Obj_t * Saig_ObjLiToLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:87
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_ObjChild1Copy
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Aig_Or
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Saig_ManLi
static Aig_Obj_t * Saig_ManLi(Aig_Man_t *p, int i)
Definition: saig.h:80
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Aig_ObjChild0Copy
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Saig_ManVerifyCexNoClear
int Saig_ManVerifyCexNoClear(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:318
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Saig_ManFindFailedPoCex
int Saig_ManFindFailedPoCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:434
Saig_ManAbstractionDfs_rec
Aig_Obj_t * Saig_ManAbstractionDfs_rec(Aig_Man_t *pNew, Aig_Obj_t *pObj)
Definition: saigDup.c:185
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Saig_ManDupWithPhase
Aig_Man_t * Saig_ManDupWithPhase(Aig_Man_t *pAig, Vec_Int_t *vInit)
Definition: saigDup.c:480
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Aig_Obj_t_::nRefs
unsigned int nRefs
Definition: aig.h:81
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91