abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
aigUtil.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [aigUtil.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [AIG package.]
8 
9  Synopsis [Various procedures.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - April 28, 2007.]
16 
17  Revision [$Id: aigUtil.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "aig.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 ////////////////////////////////////////////////////////////////////////
26 /// DECLARATIONS ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// FUNCTION DEFINITIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 /**Function*************************************************************
34 
35  Synopsis [Increments the current traversal ID of the network.]
36 
37  Description []
38 
39  SideEffects []
40 
41  SeeAlso []
42 
43 ***********************************************************************/
44 void Aig_ManIncrementTravId( Aig_Man_t * p )
45 {
46  if ( p->nTravIds >= (1<<30)-1 )
47  Aig_ManCleanData( p );
48  p->nTravIds++;
49 }
50 
51 /**Function*************************************************************
52 
53  Synopsis [Returns the time stamp.]
54 
55  Description [The file should be closed.]
56 
57  SideEffects []
58 
59  SeeAlso []
60 
61 ***********************************************************************/
62 char * Aig_TimeStamp()
63 {
64  static char Buffer[100];
65  char * TimeStamp;
66  time_t ltime;
67  // get the current time
68  time( &ltime );
69  TimeStamp = asctime( localtime( &ltime ) );
70  TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
71  strcpy( Buffer, TimeStamp );
72  return Buffer;
73 }
74 
75 /**Function*************************************************************
76 
77  Synopsis [Make sure AIG has not gaps in the numeric order.]
78 
79  Description []
80 
81  SideEffects []
82 
83  SeeAlso []
84 
85 ***********************************************************************/
86 int Aig_ManHasNoGaps( Aig_Man_t * p )
87 {
88  return (int)(Aig_ManObjNum(p) == Aig_ManCiNum(p) + Aig_ManCoNum(p) + Aig_ManNodeNum(p) + 1);
89 }
90 
91 /**Function*************************************************************
92 
93  Synopsis [Collect the latches.]
94 
95  Description []
96 
97  SideEffects []
98 
99  SeeAlso []
100 
101 ***********************************************************************/
102 int Aig_ManLevels( Aig_Man_t * p )
103 {
104  Aig_Obj_t * pObj;
105  int i, LevelMax = 0;
106  Aig_ManForEachCo( p, pObj, i )
107  LevelMax = Abc_MaxInt( LevelMax, (int)Aig_ObjFanin0(pObj)->Level );
108  return LevelMax;
109 }
110 
111 /**Function*************************************************************
112 
113  Synopsis [Reset reference counters.]
114 
115  Description []
116 
117  SideEffects []
118 
119  SeeAlso []
120 
121 ***********************************************************************/
122 void Aig_ManResetRefs( Aig_Man_t * p )
123 {
124  Aig_Obj_t * pObj;
125  int i;
126  Aig_ManForEachObj( p, pObj, i )
127  pObj->nRefs = 0;
128  Aig_ManForEachObj( p, pObj, i )
129  {
130  if ( Aig_ObjFanin0(pObj) )
131  Aig_ObjFanin0(pObj)->nRefs++;
132  if ( Aig_ObjFanin1(pObj) )
133  Aig_ObjFanin1(pObj)->nRefs++;
134  }
135 }
136 
137 /**Function*************************************************************
138 
139  Synopsis [Cleans fMarkA.]
140 
141  Description []
142 
143  SideEffects []
144 
145  SeeAlso []
146 
147 ***********************************************************************/
148 void Aig_ManCleanMarkA( Aig_Man_t * p )
149 {
150  Aig_Obj_t * pObj;
151  int i;
152  Aig_ManForEachObj( p, pObj, i )
153  pObj->fMarkA = 0;
154 }
155 
156 /**Function*************************************************************
157 
158  Synopsis [Cleans fMarkB.]
159 
160  Description []
161 
162  SideEffects []
163 
164  SeeAlso []
165 
166 ***********************************************************************/
167 void Aig_ManCleanMarkB( Aig_Man_t * p )
168 {
169  Aig_Obj_t * pObj;
170  int i;
171  Aig_ManForEachObj( p, pObj, i )
172  pObj->fMarkB = 0;
173 }
174 
175 /**Function*************************************************************
176 
177  Synopsis [Cleans fMarkB.]
178 
179  Description []
180 
181  SideEffects []
182 
183  SeeAlso []
184 
185 ***********************************************************************/
186 void Aig_ManCleanMarkAB( Aig_Man_t * p )
187 {
188  Aig_Obj_t * pObj;
189  int i;
190  Aig_ManForEachObj( p, pObj, i )
191  pObj->fMarkA = pObj->fMarkB = 0;
192 }
193 
194 /**Function*************************************************************
195 
196  Synopsis [Cleans the data pointers for the nodes.]
197 
198  Description []
199 
200  SideEffects []
201 
202  SeeAlso []
203 
204 ***********************************************************************/
205 void Aig_ManCleanData( Aig_Man_t * p )
206 {
207  Aig_Obj_t * pObj;
208  int i;
209  Aig_ManForEachObj( p, pObj, i )
210  pObj->pData = NULL;
211 }
212 
213 /**Function*************************************************************
214 
215  Synopsis [Cleans the data pointers for the nodes.]
216 
217  Description []
218 
219  SideEffects []
220 
221  SeeAlso []
222 
223 ***********************************************************************/
224 void Aig_ManCleanNext( Aig_Man_t * p )
225 {
226  Aig_Obj_t * pObj;
227  int i;
228  Aig_ManForEachObj( p, pObj, i )
229  pObj->pNext = NULL;
230 }
231 
232 /**Function*************************************************************
233 
234  Synopsis [Recursively cleans the data pointers in the cone of the node.]
235 
236  Description [Applicable to small AIGs only because no caching is performed.]
237 
238  SideEffects []
239 
240  SeeAlso []
241 
242 ***********************************************************************/
243 void Aig_ObjCleanData_rec( Aig_Obj_t * pObj )
244 {
245  assert( !Aig_IsComplement(pObj) );
246  assert( !Aig_ObjIsCo(pObj) );
247  if ( Aig_ObjIsAnd(pObj) )
248  {
249  Aig_ObjCleanData_rec( Aig_ObjFanin0(pObj) );
250  Aig_ObjCleanData_rec( Aig_ObjFanin1(pObj) );
251  }
252  pObj->pData = NULL;
253 }
254 
255 
256 /**Function*************************************************************
257 
258  Synopsis [Detects multi-input gate rooted at this node.]
259 
260  Description []
261 
262  SideEffects []
263 
264  SeeAlso []
265 
266 ***********************************************************************/
267 void Aig_ObjCollectMulti_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
268 {
269  if ( pRoot != pObj && (Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || Aig_ObjType(pRoot) != Aig_ObjType(pObj)) )
270  {
271  Vec_PtrPushUnique(vSuper, pObj);
272  return;
273  }
274  Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild0(pObj), vSuper );
275  Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild1(pObj), vSuper );
276 }
277 
278 /**Function*************************************************************
279 
280  Synopsis [Detects multi-input gate rooted at this node.]
281 
282  Description []
283 
284  SideEffects []
285 
286  SeeAlso []
287 
288 ***********************************************************************/
289 void Aig_ObjCollectMulti( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper )
290 {
291  assert( !Aig_IsComplement(pRoot) );
292  Vec_PtrClear( vSuper );
293  Aig_ObjCollectMulti_rec( pRoot, pRoot, vSuper );
294 }
295 
296 /**Function*************************************************************
297 
298  Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
299 
300  Description []
301 
302  SideEffects []
303 
304  SeeAlso []
305 
306 ***********************************************************************/
307 int Aig_ObjIsMuxType( Aig_Obj_t * pNode )
308 {
309  Aig_Obj_t * pNode0, * pNode1;
310  // check that the node is regular
311  assert( !Aig_IsComplement(pNode) );
312  // if the node is not AND, this is not MUX
313  if ( !Aig_ObjIsAnd(pNode) )
314  return 0;
315  // if the children are not complemented, this is not MUX
316  if ( !Aig_ObjFaninC0(pNode) || !Aig_ObjFaninC1(pNode) )
317  return 0;
318  // get children
319  pNode0 = Aig_ObjFanin0(pNode);
320  pNode1 = Aig_ObjFanin1(pNode);
321  // if the children are not ANDs, this is not MUX
322  if ( !Aig_ObjIsAnd(pNode0) || !Aig_ObjIsAnd(pNode1) )
323  return 0;
324  // otherwise the node is MUX iff it has a pair of equal grandchildren
325  return (Aig_ObjFanin0(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC0(pNode1))) ||
326  (Aig_ObjFanin0(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC1(pNode1))) ||
327  (Aig_ObjFanin1(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC0(pNode1))) ||
328  (Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)));
329 }
330 
331 
332 /**Function*************************************************************
333 
334  Synopsis [Recognizes what nodes are inputs of the EXOR.]
335 
336  Description []
337 
338  SideEffects []
339 
340  SeeAlso []
341 
342 ***********************************************************************/
343 int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 )
344 {
345  Aig_Obj_t * p0, * p1;
346  assert( !Aig_IsComplement(pObj) );
347  if ( !Aig_ObjIsNode(pObj) )
348  return 0;
349  if ( Aig_ObjIsExor(pObj) )
350  {
351  *ppFan0 = Aig_ObjChild0(pObj);
352  *ppFan1 = Aig_ObjChild1(pObj);
353  return 1;
354  }
355  assert( Aig_ObjIsAnd(pObj) );
356  p0 = Aig_ObjChild0(pObj);
357  p1 = Aig_ObjChild1(pObj);
358  if ( !Aig_IsComplement(p0) || !Aig_IsComplement(p1) )
359  return 0;
360  p0 = Aig_Regular(p0);
361  p1 = Aig_Regular(p1);
362  if ( !Aig_ObjIsAnd(p0) || !Aig_ObjIsAnd(p1) )
363  return 0;
364  if ( Aig_ObjFanin0(p0) != Aig_ObjFanin0(p1) || Aig_ObjFanin1(p0) != Aig_ObjFanin1(p1) )
365  return 0;
366  if ( Aig_ObjFaninC0(p0) == Aig_ObjFaninC0(p1) || Aig_ObjFaninC1(p0) == Aig_ObjFaninC1(p1) )
367  return 0;
368  *ppFan0 = Aig_ObjChild0(p0);
369  *ppFan1 = Aig_ObjChild1(p0);
370  return 1;
371 }
372 
373 /**Function*************************************************************
374 
375  Synopsis [Recognizes what nodes are control and data inputs of a MUX.]
376 
377  Description [If the node is a MUX, returns the control variable C.
378  Assigns nodes T and E to be the then and else variables of the MUX.
379  Node C is never complemented. Nodes T and E can be complemented.
380  This function also recognizes EXOR/NEXOR gates as MUXes.]
381 
382  SideEffects []
383 
384  SeeAlso []
385 
386 ***********************************************************************/
387 Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pNode, Aig_Obj_t ** ppNodeT, Aig_Obj_t ** ppNodeE )
388 {
389  Aig_Obj_t * pNode0, * pNode1;
390  assert( !Aig_IsComplement(pNode) );
391  assert( Aig_ObjIsMuxType(pNode) );
392  // get children
393  pNode0 = Aig_ObjFanin0(pNode);
394  pNode1 = Aig_ObjFanin1(pNode);
395 
396  // find the control variable
397  if ( Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)) )
398  {
399 // if ( Fraig_IsComplement(pNode1->p2) )
400  if ( Aig_ObjFaninC1(pNode0) )
401  { // pNode2->p2 is positive phase of C
402  *ppNodeT = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
403  *ppNodeE = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
404  return Aig_ObjChild1(pNode1);//pNode2->p2;
405  }
406  else
407  { // pNode1->p2 is positive phase of C
408  *ppNodeT = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
409  *ppNodeE = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
410  return Aig_ObjChild1(pNode0);//pNode1->p2;
411  }
412  }
413  else if ( Aig_ObjFanin0(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC0(pNode1)) )
414  {
415 // if ( Fraig_IsComplement(pNode1->p1) )
416  if ( Aig_ObjFaninC0(pNode0) )
417  { // pNode2->p1 is positive phase of C
418  *ppNodeT = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
419  *ppNodeE = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
420  return Aig_ObjChild0(pNode1);//pNode2->p1;
421  }
422  else
423  { // pNode1->p1 is positive phase of C
424  *ppNodeT = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
425  *ppNodeE = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
426  return Aig_ObjChild0(pNode0);//pNode1->p1;
427  }
428  }
429  else if ( Aig_ObjFanin0(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC1(pNode1)) )
430  {
431 // if ( Fraig_IsComplement(pNode1->p1) )
432  if ( Aig_ObjFaninC0(pNode0) )
433  { // pNode2->p2 is positive phase of C
434  *ppNodeT = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
435  *ppNodeE = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
436  return Aig_ObjChild1(pNode1);//pNode2->p2;
437  }
438  else
439  { // pNode1->p1 is positive phase of C
440  *ppNodeT = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
441  *ppNodeE = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
442  return Aig_ObjChild0(pNode0);//pNode1->p1;
443  }
444  }
445  else if ( Aig_ObjFanin1(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC0(pNode1)) )
446  {
447 // if ( Fraig_IsComplement(pNode1->p2) )
448  if ( Aig_ObjFaninC1(pNode0) )
449  { // pNode2->p1 is positive phase of C
450  *ppNodeT = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
451  *ppNodeE = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
452  return Aig_ObjChild0(pNode1);//pNode2->p1;
453  }
454  else
455  { // pNode1->p2 is positive phase of C
456  *ppNodeT = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
457  *ppNodeE = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
458  return Aig_ObjChild1(pNode0);//pNode1->p2;
459  }
460  }
461  assert( 0 ); // this is not MUX
462  return NULL;
463 }
464 
465 /**Function*************************************************************
466 
467  Synopsis []
468 
469  Description []
470 
471  SideEffects []
472 
473  SeeAlso []
474 
475 ***********************************************************************/
476 Aig_Obj_t * Aig_ObjReal_rec( Aig_Obj_t * pObj )
477 {
478  Aig_Obj_t * pObjNew, * pObjR = Aig_Regular(pObj);
479  if ( !Aig_ObjIsBuf(pObjR) )
480  return pObj;
481  pObjNew = Aig_ObjReal_rec( Aig_ObjChild0(pObjR) );
482  return Aig_NotCond( pObjNew, Aig_IsComplement(pObj) );
483 }
484 
485 /**Function*************************************************************
486 
487  Synopsis [Procedure used for sorting the nodes in increasing order of IDs.]
488 
489  Description []
490 
491  SideEffects []
492 
493  SeeAlso []
494 
495 ***********************************************************************/
496 int Aig_ObjCompareIdIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
497 {
498  int Diff = Aig_ObjId(*pp1) - Aig_ObjId(*pp2);
499  if ( Diff < 0 )
500  return -1;
501  if ( Diff > 0 )
502  return 1;
503  return 0;
504 }
505 
506 
507 /**Function*************************************************************
508 
509  Synopsis [Prints Eqn formula for the AIG rooted at this node.]
510 
511  Description [The formula is in terms of PIs, which should have
512  their names assigned in pObj->pData fields.]
513 
514  SideEffects []
515 
516  SeeAlso []
517 
518 ***********************************************************************/
519 void Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
520 {
521  Vec_Ptr_t * vSuper;
522  Aig_Obj_t * pFanin;
523  int fCompl, i;
524  // store the complemented attribute
525  fCompl = Aig_IsComplement(pObj);
526  pObj = Aig_Regular(pObj);
527  // constant case
528  if ( Aig_ObjIsConst1(pObj) )
529  {
530  fprintf( pFile, "%d", !fCompl );
531  return;
532  }
533  // PI case
534  if ( Aig_ObjIsCi(pObj) )
535  {
536  fprintf( pFile, "%s%s", fCompl? "!" : "", (char*)pObj->pData );
537  return;
538  }
539  // AND case
540  Vec_VecExpand( vLevels, Level );
541  vSuper = Vec_VecEntry(vLevels, Level);
542  Aig_ObjCollectMulti( pObj, vSuper );
543  fprintf( pFile, "%s", (Level==0? "" : "(") );
544  Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
545  {
546  Aig_ObjPrintEqn( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 );
547  if ( i < Vec_PtrSize(vSuper) - 1 )
548  fprintf( pFile, " %s ", fCompl? "+" : "*" );
549  }
550  fprintf( pFile, "%s", (Level==0? "" : ")") );
551  return;
552 }
553 
554 /**Function*************************************************************
555 
556  Synopsis [Prints Verilog formula for the AIG rooted at this node.]
557 
558  Description [The formula is in terms of PIs, which should have
559  their names assigned in pObj->pData fields.]
560 
561  SideEffects []
562 
563  SeeAlso []
564 
565 ***********************************************************************/
566 void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
567 {
568  Vec_Ptr_t * vSuper;
569  Aig_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC;
570  int fCompl, i;
571  // store the complemented attribute
572  fCompl = Aig_IsComplement(pObj);
573  pObj = Aig_Regular(pObj);
574  // constant case
575  if ( Aig_ObjIsConst1(pObj) )
576  {
577  fprintf( pFile, "1\'b%d", !fCompl );
578  return;
579  }
580  // PI case
581  if ( Aig_ObjIsCi(pObj) )
582  {
583  fprintf( pFile, "%s%s", fCompl? "~" : "", (char*)pObj->pData );
584  return;
585  }
586  // EXOR case
587  if ( Aig_ObjIsExor(pObj) )
588  {
589  Vec_VecExpand( vLevels, Level );
590  vSuper = Vec_VecEntry( vLevels, Level );
591  Aig_ObjCollectMulti( pObj, vSuper );
592  fprintf( pFile, "%s", (Level==0? "" : "(") );
593  Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
594  {
595  Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 );
596  if ( i < Vec_PtrSize(vSuper) - 1 )
597  fprintf( pFile, " ^ " );
598  }
599  fprintf( pFile, "%s", (Level==0? "" : ")") );
600  return;
601  }
602  // MUX case
603  if ( Aig_ObjIsMuxType(pObj) )
604  {
605  if ( Aig_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) )
606  {
607  fprintf( pFile, "%s", (Level==0? "" : "(") );
608  Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
609  fprintf( pFile, " ^ " );
610  Aig_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 );
611  fprintf( pFile, "%s", (Level==0? "" : ")") );
612  }
613  else
614  {
615  pFaninC = Aig_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 );
616  fprintf( pFile, "%s", (Level==0? "" : "(") );
617  Aig_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 );
618  fprintf( pFile, " ? " );
619  Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin1, fCompl), vLevels, Level+1 );
620  fprintf( pFile, " : " );
621  Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
622  fprintf( pFile, "%s", (Level==0? "" : ")") );
623  }
624  return;
625  }
626  // AND case
627  Vec_VecExpand( vLevels, Level );
628  vSuper = Vec_VecEntry(vLevels, Level);
629  Aig_ObjCollectMulti( pObj, vSuper );
630  fprintf( pFile, "%s", (Level==0? "" : "(") );
631  Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
632  {
633  Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 );
634  if ( i < Vec_PtrSize(vSuper) - 1 )
635  fprintf( pFile, " %s ", fCompl? "|" : "&" );
636  }
637  fprintf( pFile, "%s", (Level==0? "" : ")") );
638  return;
639 }
640 
641 
642 /**Function*************************************************************
643 
644  Synopsis [Prints node in HAIG.]
645 
646  Description []
647 
648  SideEffects []
649 
650  SeeAlso []
651 
652 ***********************************************************************/
653 void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig )
654 {
655  assert( !Aig_IsComplement(pObj) );
656  printf( "Node %p : ", pObj );
657  if ( Aig_ObjIsConst1(pObj) )
658  printf( "constant 1" );
659  else if ( Aig_ObjIsCi(pObj) )
660  printf( "PI" );
661  else if ( Aig_ObjIsCo(pObj) )
662  {
663  printf( "PO" );
664  printf( "%p%s",
665  Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " ") );
666  }
667  else
668  printf( "AND( %p%s, %p%s )",
669  Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " "),
670  Aig_ObjFanin1(pObj), (Aig_ObjFaninC1(pObj)? "\'" : " ") );
671  printf( " (refs = %3d)", Aig_ObjRefs(pObj) );
672 }
673 
674 /**Function*************************************************************
675 
676  Synopsis [Prints node in HAIG.]
677 
678  Description []
679 
680  SideEffects []
681 
682  SeeAlso []
683 
684 ***********************************************************************/
685 void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig )
686 {
687  Vec_Ptr_t * vNodes;
688  Aig_Obj_t * pObj;
689  int i;
690  printf( "PIs: " );
691  Aig_ManForEachCi( p, pObj, i )
692  printf( " %p", pObj );
693  printf( "\n" );
694  vNodes = Aig_ManDfs( p, 0 );
695  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
696  Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
697  printf( "\n" );
698  Vec_PtrFree( vNodes );
699 }
700 
701 /**Function*************************************************************
702 
703  Synopsis [Write speculative miter for one node.]
704 
705  Description []
706 
707  SideEffects []
708 
709  SeeAlso []
710 
711 ***********************************************************************/
712 void Aig_ManDump( Aig_Man_t * p )
713 {
714  static int Counter = 0;
715  char FileName[20];
716  // dump the logic into a file
717  sprintf( FileName, "aigbug\\%03d.blif", ++Counter );
718  Aig_ManDumpBlif( p, FileName, NULL, NULL );
719  printf( "Intermediate AIG with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(p), FileName );
720 }
721 
722 /**Function*************************************************************
723 
724  Synopsis [Writes the AIG into a BLIF file.]
725 
726  Description []
727 
728  SideEffects []
729 
730  SeeAlso []
731 
732 ***********************************************************************/
733 void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames )
734 {
735  FILE * pFile;
736  Vec_Ptr_t * vNodes;
737  Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
738  int i, nDigits, Counter = 0;
739  if ( Aig_ManCoNum(p) == 0 )
740  {
741  printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
742  return;
743  }
744  // check if constant is used
745  Aig_ManForEachCo( p, pObj, i )
746  if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
747  pConst1 = Aig_ManConst1(p);
748  // collect nodes in the DFS order
749  vNodes = Aig_ManDfs( p, 1 );
750  // assign IDs to objects
751  Aig_ManConst1(p)->iData = Counter++;
752  Aig_ManForEachCi( p, pObj, i )
753  pObj->iData = Counter++;
754  Aig_ManForEachCo( p, pObj, i )
755  pObj->iData = Counter++;
756  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
757  pObj->iData = Counter++;
758  nDigits = Abc_Base10Log( Counter );
759  // write the file
760  pFile = fopen( pFileName, "w" );
761  fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" );
762 // fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
763  fprintf( pFile, ".model %s\n", p->pName );
764  // write PIs
765  fprintf( pFile, ".inputs" );
766  Aig_ManForEachPiSeq( p, pObj, i )
767  if ( vPiNames )
768  fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, i) );
769  else
770  fprintf( pFile, " n%0*d", nDigits, pObj->iData );
771  fprintf( pFile, "\n" );
772  // write POs
773  fprintf( pFile, ".outputs" );
774  Aig_ManForEachPoSeq( p, pObj, i )
775  if ( vPoNames )
776  fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, i) );
777  else
778  fprintf( pFile, " n%0*d", nDigits, pObj->iData );
779  fprintf( pFile, "\n" );
780  // write latches
781  if ( Aig_ManRegNum(p) )
782  {
783  fprintf( pFile, "\n" );
784  Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
785  {
786  fprintf( pFile, ".latch" );
787  if ( vPoNames )
788  fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, Aig_ManCoNum(p)-Aig_ManRegNum(p)+i) );
789  else
790  fprintf( pFile, " n%0*d", nDigits, pObjLi->iData );
791  if ( vPiNames )
792  fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ManCiNum(p)-Aig_ManRegNum(p)+i) );
793  else
794  fprintf( pFile, " n%0*d", nDigits, pObjLo->iData );
795  fprintf( pFile, " 0\n" );
796  }
797  fprintf( pFile, "\n" );
798  }
799  // write nodes
800  if ( pConst1 )
801  fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData );
802  Aig_ManSetCioIds( p );
803  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
804  {
805  fprintf( pFile, ".names" );
806  if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) )
807  fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) );
808  else
809  fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
810  if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin1(pObj)) )
811  fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin1(pObj))) );
812  else
813  fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin1(pObj)->iData );
814  fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
815  fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
816  }
817  // write POs
818  Aig_ManForEachCo( p, pObj, i )
819  {
820  fprintf( pFile, ".names" );
821  if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) )
822  fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) );
823  else
824  fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
825  if ( vPoNames )
826  fprintf( pFile, " %s\n", (char*)Vec_PtrEntry(vPoNames, Aig_ObjCioId(pObj)) );
827  else
828  fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
829  fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
830  }
831  Aig_ManCleanCioIds( p );
832  fprintf( pFile, ".end\n\n" );
833  fclose( pFile );
834  Vec_PtrFree( vNodes );
835 }
836 
837 /**Function*************************************************************
838 
839  Synopsis [Writes the AIG into a Verilog file.]
840 
841  Description []
842 
843  SideEffects []
844 
845  SeeAlso []
846 
847 ***********************************************************************/
848 void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
849 {
850  FILE * pFile;
851  Vec_Ptr_t * vNodes;
852  Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
853  int i, nDigits, Counter = 0;
854  if ( Aig_ManCoNum(p) == 0 )
855  {
856  printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
857  return;
858  }
859  // check if constant is used
860  Aig_ManForEachCo( p, pObj, i )
861  if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
862  pConst1 = Aig_ManConst1(p);
863  // collect nodes in the DFS order
864  vNodes = Aig_ManDfs( p, 1 );
865  // assign IDs to objects
866  Aig_ManConst1(p)->iData = Counter++;
867  Aig_ManForEachCi( p, pObj, i )
868  pObj->iData = Counter++;
869  Aig_ManForEachCo( p, pObj, i )
870  pObj->iData = Counter++;
871  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
872  pObj->iData = Counter++;
873  nDigits = Abc_Base10Log( Counter );
874  // write the file
875  pFile = fopen( pFileName, "w" );
876  fprintf( pFile, "// Verilog file written by procedure Aig_ManDumpVerilog()\n" );
877 // fprintf( pFile, "// http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
878  if ( Aig_ManRegNum(p) )
879  fprintf( pFile, "module %s ( clock", p->pName? p->pName: "test" );
880  else
881  fprintf( pFile, "module %s (", p->pName? p->pName: "test" );
882  Aig_ManForEachPiSeq( p, pObj, i )
883  fprintf( pFile, "%s n%0*d", ((Aig_ManRegNum(p) || i)? ",":""), nDigits, pObj->iData );
884  Aig_ManForEachPoSeq( p, pObj, i )
885  fprintf( pFile, ", n%0*d", nDigits, pObj->iData );
886  fprintf( pFile, " );\n" );
887 
888  // write PIs
889  if ( Aig_ManRegNum(p) )
890  fprintf( pFile, "input clock;\n" );
891  Aig_ManForEachPiSeq( p, pObj, i )
892  fprintf( pFile, "input n%0*d;\n", nDigits, pObj->iData );
893  // write POs
894  Aig_ManForEachPoSeq( p, pObj, i )
895  fprintf( pFile, "output n%0*d;\n", nDigits, pObj->iData );
896  // write latches
897  if ( Aig_ManRegNum(p) )
898  {
899  Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
900  fprintf( pFile, "reg n%0*d;\n", nDigits, pObjLo->iData );
901  Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
902  fprintf( pFile, "wire n%0*d;\n", nDigits, pObjLi->iData );
903  }
904  // write nodes
905  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
906  fprintf( pFile, "wire n%0*d;\n", nDigits, pObj->iData );
907  if ( pConst1 )
908  fprintf( pFile, "wire n%0*d;\n", nDigits, pConst1->iData );
909  // write nodes
910  if ( pConst1 )
911  fprintf( pFile, "assign n%0*d = 1\'b1;\n", nDigits, pConst1->iData );
912  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
913  {
914  fprintf( pFile, "assign n%0*d = %sn%0*d & %sn%0*d;\n",
915  nDigits, pObj->iData,
916  !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData,
917  !Aig_ObjFaninC1(pObj) ? " " : "~", nDigits, Aig_ObjFanin1(pObj)->iData
918  );
919  }
920  // write POs
921  Aig_ManForEachPoSeq( p, pObj, i )
922  {
923  fprintf( pFile, "assign n%0*d = %sn%0*d;\n",
924  nDigits, pObj->iData,
925  !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData );
926  }
927  if ( Aig_ManRegNum(p) )
928  {
929  Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
930  {
931  fprintf( pFile, "assign n%0*d = %sn%0*d;\n",
932  nDigits, pObjLi->iData,
933  !Aig_ObjFaninC0(pObjLi) ? " " : "~", nDigits, Aig_ObjFanin0(pObjLi)->iData );
934  }
935  }
936 
937  // write initial state
938  if ( Aig_ManRegNum(p) )
939  {
940  Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
941  fprintf( pFile, "always @ (posedge clock) begin n%0*d <= n%0*d; end\n",
942  nDigits, pObjLo->iData,
943  nDigits, pObjLi->iData );
944  Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
945  fprintf( pFile, "initial begin n%0*d <= 1\'b0; end\n",
946  nDigits, pObjLo->iData );
947  }
948 
949  fprintf( pFile, "endmodule\n\n" );
950  fclose( pFile );
951  Vec_PtrFree( vNodes );
952 }
953 
954 /**Function*************************************************************
955 
956  Synopsis [Sets the PI/PO numbers.]
957 
958  Description []
959 
960  SideEffects []
961 
962  SeeAlso []
963 
964 ***********************************************************************/
965 void Aig_ManSetCioIds( Aig_Man_t * p )
966 {
967  Aig_Obj_t * pObj;
968  int i;
969  Aig_ManForEachCi( p, pObj, i )
970  pObj->CioId = i;
971  Aig_ManForEachCo( p, pObj, i )
972  pObj->CioId = i;
973 }
974 
975 /**Function*************************************************************
976 
977  Synopsis [Sets the PI/PO numbers.]
978 
979  Description []
980 
981  SideEffects []
982 
983  SeeAlso []
984 
985 ***********************************************************************/
986 void Aig_ManCleanCioIds( Aig_Man_t * p )
987 {
988  Aig_Obj_t * pObj;
989  int i;
990  Aig_ManForEachCi( p, pObj, i )
991  pObj->pNext = NULL;
992  Aig_ManForEachCo( p, pObj, i )
993  pObj->pNext = NULL;
994 }
995 
996 /**Function*************************************************************
997 
998  Synopsis [Sets the PI/PO numbers.]
999 
1000  Description []
1001 
1002  SideEffects []
1003 
1004  SeeAlso []
1005 
1006 ***********************************************************************/
1007 int Aig_ManChoiceNum( Aig_Man_t * p )
1008 {
1009  Aig_Obj_t * pObj;
1010  int i, Counter = 0;
1011  Aig_ManForEachNode( p, pObj, i )
1012  Counter += Aig_ObjIsChoice( p, pObj );
1013  return Counter;
1014 }
1015 
1016 /**Function*************************************************************
1017 
1018  Synopsis [Prints the fanouts of the control register.]
1019 
1020  Description [Useful only for Intel MC benchmarks.]
1021 
1022  SideEffects []
1023 
1024  SeeAlso []
1025 
1026 ***********************************************************************/
1027 void Aig_ManPrintControlFanouts( Aig_Man_t * p )
1028 {
1029  Aig_Obj_t * pObj, * pFanin0, * pFanin1, * pCtrl;
1030  int i;
1031 
1032  pCtrl = Aig_ManCi( p, Aig_ManCiNum(p) - 1 );
1033 
1034  printf( "Control signal:\n" );
1035  Aig_ObjPrint( p, pCtrl ); printf( "\n\n" );
1036 
1037  Aig_ManForEachObj( p, pObj, i )
1038  {
1039  if ( !Aig_ObjIsNode(pObj) )
1040  continue;
1041  assert( pObj != pCtrl );
1042  pFanin0 = Aig_ObjFanin0(pObj);
1043  pFanin1 = Aig_ObjFanin1(pObj);
1044  if ( pFanin0 == pCtrl && Aig_ObjIsCi(pFanin1) )
1045  {
1046  Aig_ObjPrint( p, pObj ); printf( "\n" );
1047  Aig_ObjPrint( p, pFanin1 ); printf( "\n" );
1048  printf( "\n" );
1049  }
1050  if ( pFanin1 == pCtrl && Aig_ObjIsCi(pFanin0) )
1051  {
1052  Aig_ObjPrint( p, pObj ); printf( "\n" );
1053  Aig_ObjPrint( p, pFanin0 ); printf( "\n" );
1054  printf( "\n" );
1055  }
1056  }
1057 }
1058 
1059 /**Function*************************************************************
1060 
1061  Synopsis [Returns the composite name of the file.]
1062 
1063  Description []
1064 
1065  SideEffects []
1066 
1067  SeeAlso []
1068 
1069 ***********************************************************************/
1070 char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix )
1071 {
1072  static char Buffer[1000];
1073  char * pDot;
1074  strcpy( Buffer, pBase );
1075  if ( (pDot = strrchr( Buffer, '.' )) )
1076  *pDot = 0;
1077  strcat( Buffer, pSuffix );
1078  if ( (pDot = strrchr( Buffer, '\\' )) || (pDot = strrchr( Buffer, '/' )) )
1079  return pDot+1;
1080  return Buffer;
1081 }
1082 
1083 /**Function*************************************************************
1084 
1085  Synopsis [Creates a sequence of random numbers.]
1086 
1087  Description []
1088 
1089  SideEffects []
1090 
1091  SeeAlso [http://en.wikipedia.org/wiki/LFSR]
1092 
1093 ***********************************************************************/
1094 void Aig_ManRandomTest2()
1095 {
1096  FILE * pFile;
1097  unsigned int lfsr = 1;
1098  unsigned int period = 0;
1099  pFile = fopen( "rand.txt", "w" );
1100  do {
1101 // lfsr = (lfsr >> 1) ^ (-(lfsr & 1u) & 0xd0000001u); // taps 32 31 29 1
1102  lfsr = 1; // to prevent the warning
1103  ++period;
1104  fprintf( pFile, "%10d : %10d ", period, lfsr );
1105 // Extra_PrintBinary( pFile, &lfsr, 32 );
1106  fprintf( pFile, "\n" );
1107  if ( period == 20000 )
1108  break;
1109  } while(lfsr != 1u);
1110  fclose( pFile );
1111 }
1112 
1113 /**Function*************************************************************
1114 
1115  Synopsis [Creates a sequence of random numbers.]
1116 
1117  Description []
1118 
1119  SideEffects []
1120 
1121  SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]
1122 
1123 ***********************************************************************/
1124 void Aig_ManRandomTest1()
1125 {
1126  FILE * pFile;
1127  unsigned int lfsr;
1128  unsigned int period = 0;
1129  pFile = fopen( "rand.txt", "w" );
1130  do {
1131  lfsr = Aig_ManRandom( 0 );
1132  ++period;
1133  fprintf( pFile, "%10d : %10d ", period, lfsr );
1134 // Extra_PrintBinary( pFile, &lfsr, 32 );
1135  fprintf( pFile, "\n" );
1136  if ( period == 20000 )
1137  break;
1138  } while(lfsr != 1u);
1139  fclose( pFile );
1140 }
1141 
1142 
1143 #define NUMBER1 3716960521u
1144 #define NUMBER2 2174103536u
1145 
1146 /**Function*************************************************************
1147 
1148  Synopsis [Creates a sequence of random numbers.]
1149 
1150  Description []
1151 
1152  SideEffects []
1153 
1154  SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]
1155 
1156 ***********************************************************************/
1157 unsigned Aig_ManRandom( int fReset )
1158 {
1159  static unsigned int m_z = NUMBER1;
1160  static unsigned int m_w = NUMBER2;
1161  if ( fReset )
1162  {
1163  m_z = NUMBER1;
1164  m_w = NUMBER2;
1165  }
1166  m_z = 36969 * (m_z & 65535) + (m_z >> 16);
1167  m_w = 18000 * (m_w & 65535) + (m_w >> 16);
1168  return (m_z << 16) + m_w;
1169 }
1170 
1171 /**Function*************************************************************
1172 
1173  Synopsis [Creates a sequence of random numbers.]
1174 
1175  Description []
1176 
1177  SideEffects []
1178 
1179  SeeAlso []
1180 
1181 ***********************************************************************/
1182 word Aig_ManRandom64( int fReset )
1183 {
1184  word Res = (word)Aig_ManRandom(fReset);
1185  return Res | ((word)Aig_ManRandom(0) << 32);
1186 }
1187 
1188 
1189 /**Function*************************************************************
1190 
1191  Synopsis [Creates random info for the primary inputs.]
1192 
1193  Description []
1194 
1195  SideEffects []
1196 
1197  SeeAlso []
1198 
1199 ***********************************************************************/
1200 void Aig_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop )
1201 {
1202  unsigned * pInfo;
1203  int i, w;
1204  Vec_PtrForEachEntryStart( unsigned *, vInfo, pInfo, i, iInputStart )
1205  for ( w = iWordStart; w < iWordStop; w++ )
1206  pInfo[w] = Aig_ManRandom(0);
1207 }
1208 
1209 /**Function*************************************************************
1210 
1211  Synopsis [Returns the result of merging the two vectors.]
1212 
1213  Description [Assumes that the vectors are sorted in the increasing order.]
1214 
1215  SideEffects []
1216 
1217  SeeAlso []
1218 
1219 ***********************************************************************/
1220 void Aig_NodeUnionLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
1221 {
1222  Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
1223  Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
1224  Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
1225  Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
1226  Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
1227  Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) );
1228  pBeg = (Aig_Obj_t **)vArr->pArray;
1229  while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
1230  {
1231  if ( (*pBeg1)->Id == (*pBeg2)->Id )
1232  *pBeg++ = *pBeg1++, pBeg2++;
1233  else if ( (*pBeg1)->Id < (*pBeg2)->Id )
1234  *pBeg++ = *pBeg1++;
1235  else
1236  *pBeg++ = *pBeg2++;
1237  }
1238  while ( pBeg1 < pEnd1 )
1239  *pBeg++ = *pBeg1++;
1240  while ( pBeg2 < pEnd2 )
1241  *pBeg++ = *pBeg2++;
1242  vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
1243  assert( vArr->nSize <= vArr->nCap );
1244  assert( vArr->nSize >= vArr1->nSize );
1245  assert( vArr->nSize >= vArr2->nSize );
1246 }
1247 
1248 /**Function*************************************************************
1249 
1250  Synopsis [Returns the result of intersecting the two vectors.]
1251 
1252  Description [Assumes that the vectors are sorted in the increasing order.]
1253 
1254  SideEffects []
1255 
1256  SeeAlso []
1257 
1258 ***********************************************************************/
1259 void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
1260 {
1261  Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
1262  Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
1263  Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
1264  Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
1265  Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
1266  Vec_PtrGrow( vArr, Abc_MaxInt( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
1267  pBeg = (Aig_Obj_t **)vArr->pArray;
1268  while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
1269  {
1270  if ( (*pBeg1)->Id == (*pBeg2)->Id )
1271  *pBeg++ = *pBeg1++, pBeg2++;
1272  else if ( (*pBeg1)->Id < (*pBeg2)->Id )
1273 // *pBeg++ = *pBeg1++;
1274  pBeg1++;
1275  else
1276 // *pBeg++ = *pBeg2++;
1277  pBeg2++;
1278  }
1279 // while ( pBeg1 < pEnd1 )
1280 // *pBeg++ = *pBeg1++;
1281 // while ( pBeg2 < pEnd2 )
1282 // *pBeg++ = *pBeg2++;
1283  vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
1284  assert( vArr->nSize <= vArr->nCap );
1285  assert( vArr->nSize <= vArr1->nSize );
1286  assert( vArr->nSize <= vArr2->nSize );
1287 }
1288 
1289 ABC_NAMESPACE_IMPL_END
1290 
1291 #include "proof/fra/fra.h"
1292 #include "aig/saig/saig.h"
1293 
1294 ABC_NAMESPACE_IMPL_START
1295 
1296 
1297 extern void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex );
1298 extern void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig );
1299 extern int Aig_ManCounterExampleValueLookup( Aig_Man_t * pAig, int Id, int iFrame );
1300 
1301 /**Function*************************************************************
1302 
1303  Synopsis [Starts the process of retuning values for internal nodes.]
1304 
1305  Description [Should be called when pCex is available, before probing
1306  any object for its value using Aig_ManCounterExampleValueLookup().]
1307 
1308  SideEffects []
1309 
1310  SeeAlso []
1311 
1312 ***********************************************************************/
1313 void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex )
1314 {
1315  Aig_Obj_t * pObj, * pObjRi, * pObjRo;
1316  int Val0, Val1, nObjs, i, k, iBit = 0;
1317  assert( Aig_ManRegNum(pAig) > 0 ); // makes sense only for sequential AIGs
1318  assert( pAig->pData2 == NULL ); // if this fail, there may be a memory leak
1319  // allocate memory to store simulation bits for internal nodes
1320  pAig->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNumMax(pAig) ) );
1321  // the register values in the counter-example should be zero
1322  Saig_ManForEachLo( pAig, pObj, k )
1323  assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 );
1324  // iterate through the timeframes
1325  nObjs = Aig_ManObjNumMax(pAig);
1326  for ( i = 0; i <= pCex->iFrame; i++ )
1327  {
1328  // set constant 1 node
1329  Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + 0 );
1330  // set primary inputs according to the counter-example
1331  Saig_ManForEachPi( pAig, pObj, k )
1332  if ( Abc_InfoHasBit(pCex->pData, iBit++) )
1333  Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
1334  // compute values for each node
1335  Aig_ManForEachNode( pAig, pObj, k )
1336  {
1337  Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
1338  Val1 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) );
1339  if ( (Val0 ^ Aig_ObjFaninC0(pObj)) & (Val1 ^ Aig_ObjFaninC1(pObj)) )
1340  Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
1341  }
1342  // derive values for combinational outputs
1343  Aig_ManForEachCo( pAig, pObj, k )
1344  {
1345  Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
1346  if ( Val0 ^ Aig_ObjFaninC0(pObj) )
1347  Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
1348  }
1349  if ( i == pCex->iFrame )
1350  continue;
1351  // transfer values to the register output of the next frame
1352  Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
1353  if ( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) )
1354  Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) );
1355  }
1356  assert( iBit == pCex->nBits );
1357  // check that the counter-example is correct, that is, the corresponding output is asserted
1358  assert( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManCo(pAig, pCex->iPo)) ) );
1359 }
1360 
1361 /**Function*************************************************************
1362 
1363  Synopsis [Stops the process of retuning values for internal nodes.]
1364 
1365  Description [Should be called when probing is no longer needed]
1366 
1367  SideEffects []
1368 
1369  SeeAlso []
1370 
1371 ***********************************************************************/
1372 void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig )
1373 {
1374  assert( pAig->pData2 != NULL ); // if this fail, we try to call this procedure more than once
1375  free( pAig->pData2 );
1376  pAig->pData2 = NULL;
1377 }
1378 
1379 /**Function*************************************************************
1380 
1381  Synopsis [Returns the value of the given object in the given timeframe.]
1382 
1383  Description [Should be called to probe the value of an object with
1384  the given ID (iFrame is a 0-based number of a time frame - should not
1385  exceed the number of timeframes in the original counter-example).]
1386 
1387  SideEffects []
1388 
1389  SeeAlso []
1390 
1391 ***********************************************************************/
1392 int Aig_ManCounterExampleValueLookup( Aig_Man_t * pAig, int Id, int iFrame )
1393 {
1394  assert( Id >= 0 && Id < Aig_ManObjNumMax(pAig) );
1395  return Abc_InfoHasBit( (unsigned *)pAig->pData2, Aig_ManObjNumMax(pAig) * iFrame + Id );
1396 }
1397 
1398 /**Function*************************************************************
1399 
1400  Synopsis [Procedure to test the above code.]
1401 
1402  Description []
1403 
1404  SideEffects []
1405 
1406  SeeAlso []
1407 
1408 ***********************************************************************/
1409 void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Abc_Cex_t * pCex )
1410 {
1411  Aig_Obj_t * pObj = Aig_ManObj( pAig, Aig_ManObjNumMax(pAig)/2 );
1412  int iFrame = Abc_MaxInt( 0, pCex->iFrame - 1 );
1413  printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame );
1414  Aig_ManCounterExampleValueStart( pAig, pCex );
1415  printf( "Value of object %d in frame %d is %d.\n", Aig_ObjId(pObj), iFrame,
1416  Aig_ManCounterExampleValueLookup(pAig, Aig_ObjId(pObj), iFrame) );
1417  Aig_ManCounterExampleValueStop( pAig );
1418 }
1419 
1420 /**Function*************************************************************
1421 
1422  Synopsis [Handle the counter-example.]
1423 
1424  Description []
1425 
1426  SideEffects []
1427 
1428  SeeAlso []
1429 
1430 ***********************************************************************/
1431 void Aig_ManSetPhase( Aig_Man_t * pAig )
1432 {
1433  Aig_Obj_t * pObj;
1434  int i;
1435  // set the PI simulation information
1436  Aig_ManConst1( pAig )->fPhase = 1;
1437  Aig_ManForEachCi( pAig, pObj, i )
1438  pObj->fPhase = 0;
1439  // simulate internal nodes
1440  Aig_ManForEachNode( pAig, pObj, i )
1441  pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) )
1442  & ( Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj) );
1443  // simulate PO nodes
1444  Aig_ManForEachCo( pAig, pObj, i )
1445  pObj->fPhase = Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj);
1446 }
1447 
1448 
1449 /**Function*************************************************************
1450 
1451  Synopsis [Collects muxes.]
1452 
1453  Description []
1454 
1455  SideEffects []
1456 
1457  SeeAlso []
1458 
1459 ***********************************************************************/
1460 Vec_Ptr_t * Aig_ManMuxesCollect( Aig_Man_t * pAig )
1461 {
1462  Vec_Ptr_t * vMuxes;
1463  Aig_Obj_t * pObj;
1464  int i;
1465  vMuxes = Vec_PtrAlloc( 100 );
1466  Aig_ManForEachNode( pAig, pObj, i )
1467  if ( Aig_ObjIsMuxType(pObj) )
1468  Vec_PtrPush( vMuxes, pObj );
1469  return vMuxes;
1470 }
1471 
1472 /**Function*************************************************************
1473 
1474  Synopsis [Dereferences muxes.]
1475 
1476  Description []
1477 
1478  SideEffects []
1479 
1480  SeeAlso []
1481 
1482 ***********************************************************************/
1483 void Aig_ManMuxesDeref( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes )
1484 {
1485  Aig_Obj_t * pObj, * pNodeT, * pNodeE, * pNodeC;
1486  int i;
1487  Vec_PtrForEachEntry( Aig_Obj_t *, vMuxes, pObj, i )
1488  {
1489  if ( Aig_ObjRecognizeExor( pObj, &pNodeT, &pNodeE ) )
1490  {
1491  pNodeT->nRefs--;
1492  pNodeE->nRefs--;
1493  }
1494  else
1495  {
1496  pNodeC = Aig_ObjRecognizeMux( pObj, &pNodeT, &pNodeE );
1497  pNodeC->nRefs--;
1498  }
1499  }
1500 }
1501 
1502 /**Function*************************************************************
1503 
1504  Synopsis [References muxes.]
1505 
1506  Description []
1507 
1508  SideEffects []
1509 
1510  SeeAlso []
1511 
1512 ***********************************************************************/
1513 void Aig_ManMuxesRef( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes )
1514 {
1515  Aig_Obj_t * pObj, * pNodeT, * pNodeE, * pNodeC;
1516  int i;
1517  Vec_PtrForEachEntry( Aig_Obj_t *, vMuxes, pObj, i )
1518  {
1519  if ( Aig_ObjRecognizeExor( pObj, &pNodeT, &pNodeE ) )
1520  {
1521  pNodeT->nRefs++;
1522  pNodeE->nRefs++;
1523  }
1524  else
1525  {
1526  pNodeC = Aig_ObjRecognizeMux( pObj, &pNodeT, &pNodeE );
1527  pNodeC->nRefs++;
1528  }
1529  }
1530 }
1531 
1532 /**Function*************************************************************
1533 
1534  Synopsis [Complements the constraint outputs.]
1535 
1536  Description []
1537 
1538  SideEffects []
1539 
1540  SeeAlso []
1541 
1542 ***********************************************************************/
1543 void Aig_ManInvertConstraints( Aig_Man_t * pAig )
1544 {
1545  Aig_Obj_t * pObj;
1546  int i;
1547  if ( Aig_ManConstrNum(pAig) == 0 )
1548  return;
1549  Saig_ManForEachPo( pAig, pObj, i )
1550  {
1551  if ( i >= Saig_ManPoNum(pAig) - Aig_ManConstrNum(pAig) )
1552  Aig_ObjChild0Flip( pObj );
1553  }
1554 }
1555 
1556 ////////////////////////////////////////////////////////////////////////
1557 /// END OF FILE ///
1558 ////////////////////////////////////////////////////////////////////////
1559 
1560 
1561 ABC_NAMESPACE_IMPL_END
1562 
Aig_ManCounterExampleValueStart
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START void Aig_ManCounterExampleValueStart(Aig_Man_t *pAig, Abc_Cex_t *pCex)
Definition: aigUtil.c:1313
Aig_Obj_t_::CioId
int CioId
Definition: aig.h:73
Aig_ManCounterExampleValueTest
void Aig_ManCounterExampleValueTest(Aig_Man_t *pAig, Abc_Cex_t *pCex)
Definition: aigUtil.c:1409
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_ManCleanMarkB
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition: aigUtil.c:167
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition: aigUtil.c:148
free
VOID_HACK free()
Aig_ObjType
static Aig_Type_t Aig_ObjType(Aig_Obj_t *pObj)
Definition: aig.h:272
Aig_ObjFaninId0
static int Aig_ObjFaninId0(Aig_Obj_t *pObj)
Definition: aig.h:304
Aig_FileNameGenericAppend
char * Aig_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition: aigUtil.c:1070
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
Aig_ManConstrNum
static int Aig_ManConstrNum(Aig_Man_t *p)
Definition: aig.h:261
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_ManResetRefs
void Aig_ManResetRefs(Aig_Man_t *p)
Definition: aigUtil.c:122
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Aig_ManDumpBlif
void Aig_ManDumpBlif(Aig_Man_t *p, char *pFileName, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vPoNames)
Definition: aigUtil.c:733
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
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
Vec_PtrGrow
static void Vec_PtrGrow(Vec_Ptr_t *p, int nCapMin)
Definition: vecPtr.h:430
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition: aig.h:80
Aig_ObjRecognizeExor
int Aig_ObjRecognizeExor(Aig_Obj_t *pObj, Aig_Obj_t **ppFan0, Aig_Obj_t **ppFan1)
Definition: aigUtil.c:343
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Aig_ManSetCioIds
void Aig_ManSetCioIds(Aig_Man_t *p)
Definition: aigUtil.c:965
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_ManPrintVerbose
void Aig_ManPrintVerbose(Aig_Man_t *p, int fHaig)
Definition: aigUtil.c:685
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
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_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
Aig_Not
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
Aig_ManChoiceNum
int Aig_ManChoiceNum(Aig_Man_t *p)
Definition: aigUtil.c:1007
Aig_ObjFaninId1
static int Aig_ObjFaninId1(Aig_Obj_t *pObj)
Definition: aig.h:305
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Aig_ManMuxesCollect
Vec_Ptr_t * Aig_ManMuxesCollect(Aig_Man_t *pAig)
Definition: aigUtil.c:1460
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_NodeUnionLists
void Aig_NodeUnionLists(Vec_Ptr_t *vArr1, Vec_Ptr_t *vArr2, Vec_Ptr_t *vArr)
Definition: aigUtil.c:1220
Aig_ObjCleanData_rec
void Aig_ObjCleanData_rec(Aig_Obj_t *pObj)
Definition: aigUtil.c:243
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Aig_ObjPrint
void Aig_ObjPrint(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aigObj.c:316
Aig_ManPrintControlFanouts
void Aig_ManPrintControlFanouts(Aig_Man_t *p)
Definition: aigUtil.c:1027
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_ManHasNoGaps
int Aig_ManHasNoGaps(Aig_Man_t *p)
Definition: aigUtil.c:86
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Aig_ManRandomTest1
void Aig_ManRandomTest1()
Definition: aigUtil.c:1124
Aig_ObjIsBuf
static int Aig_ObjIsBuf(Aig_Obj_t *pObj)
Definition: aig.h:277
Aig_ObjPrintVerbose
void Aig_ObjPrintVerbose(Aig_Obj_t *pObj, int fHaig)
Definition: aigUtil.c:653
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
NUMBER1
#define NUMBER1
Definition: aigUtil.c:1143
Aig_ManRandom64
word Aig_ManRandom64(int fReset)
Definition: aigUtil.c:1182
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
Aig_ManForEachLiLoSeq
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition: aig.h:450
Aig_ManSetPhase
void Aig_ManSetPhase(Aig_Man_t *pAig)
Definition: aigUtil.c:1431
Aig_ObjCompareIdIncrease
int Aig_ObjCompareIdIncrease(Aig_Obj_t **pp1, Aig_Obj_t **pp2)
Definition: aigUtil.c:496
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Abc_Base10Log
static int Abc_Base10Log(unsigned n)
Definition: abc_global.h:252
Aig_ManCounterExampleValueStop
void Aig_ManCounterExampleValueStop(Aig_Man_t *pAig)
Definition: aigUtil.c:1372
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
NUMBER2
#define NUMBER2
Definition: aigUtil.c:1144
Aig_ObjChild1
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Aig_ObjReal_rec
Aig_Obj_t * Aig_ObjReal_rec(Aig_Obj_t *pObj)
Definition: aigUtil.c:476
Aig_ManDumpVerilog
void Aig_ManDumpVerilog(Aig_Man_t *p, char *pFileName)
Definition: aigUtil.c:848
Aig_ManDfs
Vec_Ptr_t * Aig_ManDfs(Aig_Man_t *p, int fNodesOnly)
Definition: aigDfs.c:145
Aig_Obj_t_
Definition: aig.h:69
Aig_Obj_t_::pNext
Aig_Obj_t * pNext
Definition: aig.h:72
sprintf
char * sprintf()
Counter
static int Counter
Definition: extraBddMisc.c:1877
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Aig_ManRandomTest2
void Aig_ManRandomTest2()
Definition: aigUtil.c:1094
Aig_ManCleanNext
void Aig_ManCleanNext(Aig_Man_t *p)
Definition: aigUtil.c:224
Aig_ObjChild0Flip
static void Aig_ObjChild0Flip(Aig_Obj_t *pObj)
Definition: aig.h:316
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pNode)
Definition: aigUtil.c:307
strcpy
char * strcpy()
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManMuxesRef
void Aig_ManMuxesRef(Aig_Man_t *pAig, Vec_Ptr_t *vMuxes)
Definition: aigUtil.c:1513
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Aig_ObjIsExor
static int Aig_ObjIsExor(Aig_Obj_t *pObj)
Definition: aig.h:279
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Aig_ManRandomInfo
void Aig_ManRandomInfo(Vec_Ptr_t *vInfo, int iInputStart, int iWordStart, int iWordStop)
Definition: aigUtil.c:1200
Aig_ObjCollectMulti_rec
void Aig_ObjCollectMulti_rec(Aig_Obj_t *pRoot, Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
Definition: aigUtil.c:267
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
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_ObjRecognizeMux
Aig_Obj_t * Aig_ObjRecognizeMux(Aig_Obj_t *pNode, Aig_Obj_t **ppNodeT, Aig_Obj_t **ppNodeE)
Definition: aigUtil.c:387
Aig_ManLevels
int Aig_ManLevels(Aig_Man_t *p)
Definition: aigUtil.c:102
Aig_Obj_t_::iData
int iData
Definition: aig.h:88
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Aig_ManMuxesDeref
void Aig_ManMuxesDeref(Aig_Man_t *pAig, Vec_Ptr_t *vMuxes)
Definition: aigUtil.c:1483
Vec_VecExpand
static void Vec_VecExpand(Vec_Vec_t *p, int Level)
Definition: vecVec.h:190
Aig_ManDump
void Aig_ManDump(Aig_Man_t *p)
Definition: aigUtil.c:712
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
GLOBAL VARIABLES ///.
Definition: aigUtil.c:1157
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
strcat
char * strcat()
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
strlen
int strlen()
Aig_ManIncrementTravId
ABC_NAMESPACE_IMPL_START void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_TimeStamp
char * Aig_TimeStamp()
Definition: aigUtil.c:62
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Aig_ManCleanMarkAB
void Aig_ManCleanMarkAB(Aig_Man_t *p)
Definition: aigUtil.c:186
Vec_VecEntry
static Vec_Ptr_t * Vec_VecEntry(Vec_Vec_t *p, int i)
Definition: vecVec.h:271
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Aig_ObjCollectMulti
void Aig_ObjCollectMulti(Aig_Obj_t *pRoot, Vec_Ptr_t *vSuper)
Definition: aigUtil.c:289
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
Aig_ManForEachPoSeq
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition: aig.h:444
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
strrchr
char * strrchr()
Aig_ManInvertConstraints
void Aig_ManInvertConstraints(Aig_Man_t *pAig)
Definition: aigUtil.c:1543
Aig_NodeIntersectLists
void Aig_NodeIntersectLists(Vec_Ptr_t *vArr1, Vec_Ptr_t *vArr2, Vec_Ptr_t *vArr)
Definition: aigUtil.c:1259
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
Aig_ObjIsChoice
static int Aig_ObjIsChoice(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:283
Aig_ObjPrintEqn
void Aig_ObjPrintEqn(FILE *pFile, Aig_Obj_t *pObj, Vec_Vec_t *vLevels, int Level)
Definition: aigUtil.c:519
Aig_ManForEachPiSeq
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition: aig.h:438
Aig_ObjPrintVerilog
void Aig_ObjPrintVerilog(FILE *pFile, Aig_Obj_t *pObj, Vec_Vec_t *vLevels, int Level)
Definition: aigUtil.c:566
Aig_ObjIsAnd
static int Aig_ObjIsAnd(Aig_Obj_t *pObj)
Definition: aig.h:278
Aig_ManCleanCioIds
void Aig_ManCleanCioIds(Aig_Man_t *p)
Definition: aigUtil.c:986
Aig_ObjCioId
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285
Aig_ManCounterExampleValueLookup
int Aig_ManCounterExampleValueLookup(Aig_Man_t *pAig, int Id, int iFrame)
Definition: aigUtil.c:1392
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