abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcFunc.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [abcFunc.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Network and node package.]
8 
9  Synopsis [Transformations between different functionality representations.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: abcFunc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "abc.h"
22 #include "base/main/main.h"
23 #include "map/mio/mio.h"
24 #include "misc/extra/extraBdd.h"
25 
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 #define ABC_MUX_CUBES 100000
34 
35 int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
36 static DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot);
37 static Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop );
38 
39 extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
40 
41 ////////////////////////////////////////////////////////////////////////
42 /// FUNCTION DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44 
45 /**Function*************************************************************
46 
47  Synopsis [Converts the node from SOP to BDD representation.]
48 
49  Description []
50 
51  SideEffects []
52 
53  SeeAlso []
54 
55 ***********************************************************************/
56 DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, DdNode ** pbVars )
57 {
58  DdNode * bSum, * bCube, * bTemp, * bVar;
59  char * pCube;
60  int nVars, Value, v;
61 
62  // start the cover
63  nVars = Abc_SopGetVarNum(pSop);
64  bSum = Cudd_ReadLogicZero(dd); Cudd_Ref( bSum );
65  if ( Abc_SopIsExorType(pSop) )
66  {
67  for ( v = 0; v < nVars; v++ )
68  {
69  bSum = Cudd_bddXor( dd, bTemp = bSum, pbVars? pbVars[v] : Cudd_bddIthVar(dd, v) ); Cudd_Ref( bSum );
70  Cudd_RecursiveDeref( dd, bTemp );
71  }
72  }
73  else
74  {
75  // check the logic function of the node
76  Abc_SopForEachCube( pSop, nVars, pCube )
77  {
78  bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube );
79  Abc_CubeForEachVar( pCube, Value, v )
80  {
81  if ( Value == '0' )
82  bVar = Cudd_Not( pbVars? pbVars[v] : Cudd_bddIthVar( dd, v ) );
83  else if ( Value == '1' )
84  bVar = pbVars? pbVars[v] : Cudd_bddIthVar( dd, v );
85  else
86  continue;
87  bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube );
88  Cudd_RecursiveDeref( dd, bTemp );
89  }
90  bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );
91  Cudd_Ref( bSum );
92  Cudd_RecursiveDeref( dd, bTemp );
93  Cudd_RecursiveDeref( dd, bCube );
94  }
95  }
96  // complement the result if necessary
97  bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) );
98  Cudd_Deref( bSum );
99  return bSum;
100 }
101 
102 /**Function*************************************************************
103 
104  Synopsis [Converts the network from SOP to BDD representation.]
105 
106  Description []
107 
108  SideEffects []
109 
110  SeeAlso []
111 
112 ***********************************************************************/
114 {
115  Abc_Obj_t * pNode;
116  DdManager * dd, * ddTemp = NULL;
117  Vec_Int_t * vFanins = NULL;
118  int nFaninsMax, i, k, iVar;
119 
120  assert( Abc_NtkHasSop(pNtk) );
121 
122  // start the functionality manager
123  nFaninsMax = Abc_NtkGetFaninMax( pNtk );
124  if ( nFaninsMax == 0 )
125  printf( "Warning: The network has only constant nodes.\n" );
126  dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
127 
128  // start temporary manager for reordered local functions
129  if ( nFaninsMax > 10 )
130  {
131  ddTemp = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
133  vFanins = Vec_IntAlloc( nFaninsMax );
134  }
135 
136  // convert each node from SOP to BDD
137  Abc_NtkForEachNode( pNtk, pNode, i )
138  {
139  if ( Abc_ObjIsBarBuf(pNode) )
140  continue;
141  assert( pNode->pData );
142  if ( Abc_ObjFaninNum(pNode) > 10 )
143  {
144  DdNode * pFunc = Abc_ConvertSopToBdd( ddTemp, (char *)pNode->pData, NULL );
145  if ( pFunc == NULL )
146  {
147  printf( "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
148  return 0;
149  }
150  Cudd_Ref( pFunc );
151  // find variable mapping
152  Vec_IntFill( vFanins, Abc_ObjFaninNum(pNode), -1 );
153  for ( k = iVar = 0; k < nFaninsMax; k++ )
154  if ( ddTemp->invperm[k] < Abc_ObjFaninNum(pNode) )
155  Vec_IntWriteEntry( vFanins, ddTemp->invperm[k], iVar++ );
156  assert( iVar == Abc_ObjFaninNum(pNode) );
157  // transfer to the main manager
158  pNode->pData = Extra_TransferPermute( ddTemp, dd, pFunc, Vec_IntArray(vFanins) );
159  Cudd_Ref( (DdNode *)pNode->pData );
160  Cudd_RecursiveDeref( ddTemp, pFunc );
161  // update variable order
162  Vec_IntClear( vFanins );
163  for ( k = 0; k < nFaninsMax; k++ )
164  if ( ddTemp->invperm[k] < Abc_ObjFaninNum(pNode) )
165  Vec_IntPush( vFanins, Vec_IntEntry(&pNode->vFanins, ddTemp->invperm[k]) );
166  for ( k = 0; k < Abc_ObjFaninNum(pNode); k++ )
167  Vec_IntWriteEntry( &pNode->vFanins, k, Vec_IntEntry(vFanins, k) );
168  }
169  else
170  {
171  pNode->pData = Abc_ConvertSopToBdd( dd, (char *)pNode->pData, NULL );
172  if ( pNode->pData == NULL )
173  {
174  printf( "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
175  return 0;
176  }
177  Cudd_Ref( (DdNode *)pNode->pData );
178  }
179  }
180 
181  if ( ddTemp )
182  {
183 // printf( "Reorderings performed = %d.\n", Cudd_ReadReorderings(ddTemp) );
184  Extra_StopManager( ddTemp );
185  }
186  Vec_IntFreeP( &vFanins );
187  Mem_FlexStop( (Mem_Flex_t *)pNtk->pManFunc, 0 );
188  pNtk->pManFunc = dd;
189 
190  // update the network type
191  pNtk->ntkFunc = ABC_FUNC_BDD;
192  return 1;
193 }
194 
195 
196 
197 
198 /**Function*************************************************************
199 
200  Synopsis [Converts the node from BDD to SOP representation.]
201 
202  Description []
203 
204  SideEffects []
205 
206  SeeAlso []
207 
208 ***********************************************************************/
209 char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode )
210 {
211  int fVerify = 0;
212  char * pSop;
213  DdNode * bFuncNew, * bCover, * zCover, * zCover0, * zCover1;
214  int nCubes, nCubes0, nCubes1, fPhase;
215 
216  assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) );
217  if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) )
218  {
219  if ( fMode == -1 ) // if the phase is not known, write constant 1
220  fMode = 1;
221  Vec_StrFill( vCube, nFanins, '-' );
222  Vec_StrPush( vCube, '\0' );
223  if ( pMan )
224  pSop = Mem_FlexEntryFetch( pMan, nFanins + 4 );
225  else
226  pSop = ABC_ALLOC( char, nFanins + 4 );
227  if ( bFuncOn == Cudd_ReadOne(dd) )
228  sprintf( pSop, "%s %d\n", vCube->pArray, fMode );
229  else
230  sprintf( pSop, "%s %d\n", vCube->pArray, !fMode );
231  return pSop;
232  }
233 
234 
235  if ( fMode == -1 )
236  { // try both phases
237  assert( fAllPrimes == 0 );
238 
239  // get the ZDD of the negative polarity
240  bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover0 );
241  Cudd_Ref( zCover0 );
242  Cudd_Ref( bCover );
243  Cudd_RecursiveDeref( dd, bCover );
244  nCubes0 = Abc_CountZddCubes( dd, zCover0 );
245 
246  // get the ZDD of the positive polarity
247  bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover1 );
248  Cudd_Ref( zCover1 );
249  Cudd_Ref( bCover );
250  Cudd_RecursiveDeref( dd, bCover );
251  nCubes1 = Abc_CountZddCubes( dd, zCover1 );
252 
253  // compare the number of cubes
254  if ( nCubes1 <= nCubes0 )
255  { // use positive polarity
256  nCubes = nCubes1;
257  zCover = zCover1;
258  Cudd_RecursiveDerefZdd( dd, zCover0 );
259  fPhase = 1;
260  }
261  else
262  { // use negative polarity
263  nCubes = nCubes0;
264  zCover = zCover0;
265  Cudd_RecursiveDerefZdd( dd, zCover1 );
266  fPhase = 0;
267  }
268  }
269  else if ( fMode == 0 )
270  {
271  // get the ZDD of the negative polarity
272  if ( fAllPrimes )
273  {
274  zCover = Extra_zddPrimes( dd, Cudd_Not(bFuncOnDc) );
275  Cudd_Ref( zCover );
276  }
277  else
278  {
279  bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover );
280  Cudd_Ref( zCover );
281  Cudd_Ref( bCover );
282  Cudd_RecursiveDeref( dd, bCover );
283  }
284  nCubes = Abc_CountZddCubes( dd, zCover );
285  fPhase = 0;
286  }
287  else if ( fMode == 1 )
288  {
289  // get the ZDD of the positive polarity
290  if ( fAllPrimes )
291  {
292  zCover = Extra_zddPrimes( dd, bFuncOnDc );
293  Cudd_Ref( zCover );
294  }
295  else
296  {
297  bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover );
298  Cudd_Ref( zCover );
299  Cudd_Ref( bCover );
300  Cudd_RecursiveDeref( dd, bCover );
301  }
302  nCubes = Abc_CountZddCubes( dd, zCover );
303  fPhase = 1;
304  }
305  else
306  {
307  assert( 0 );
308  }
309 
310  if ( nCubes > ABC_MUX_CUBES )
311  {
312  Cudd_RecursiveDerefZdd( dd, zCover );
313  printf( "The number of cubes exceeded the predefined limit (%d).\n", ABC_MUX_CUBES );
314  return NULL;
315  }
316 
317  // allocate memory for the cover
318  if ( pMan )
319  pSop = Mem_FlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 );
320  else
321  pSop = ABC_ALLOC( char, (nFanins + 3) * nCubes + 1 );
322  pSop[(nFanins + 3) * nCubes] = 0;
323  // create the SOP
324  Vec_StrFill( vCube, nFanins, '-' );
325  Vec_StrPush( vCube, '\0' );
326  Abc_ConvertZddToSop( dd, zCover, pSop, nFanins, vCube, fPhase );
327  Cudd_RecursiveDerefZdd( dd, zCover );
328 
329  // verify
330  if ( fVerify )
331  {
332  bFuncNew = Abc_ConvertSopToBdd( dd, pSop, NULL ); Cudd_Ref( bFuncNew );
333  if ( bFuncOn == bFuncOnDc )
334  {
335  if ( bFuncNew != bFuncOn )
336  printf( "Verification failed.\n" );
337  }
338  else
339  {
340  if ( !Cudd_bddLeq(dd, bFuncOn, bFuncNew) || !Cudd_bddLeq(dd, bFuncNew, bFuncOnDc) )
341  printf( "Verification failed.\n" );
342  }
343  Cudd_RecursiveDeref( dd, bFuncNew );
344  }
345  return pSop;
346 }
347 
348 /**Function*************************************************************
349 
350  Synopsis [Converts the network from BDD to SOP representation.]
351 
352  Description [If the flag is set to 1, forces the direct phase of all covers.]
353 
354  SideEffects []
355 
356  SeeAlso []
357 
358 ***********************************************************************/
359 int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
360 {
361  extern void Abc_NtkSortSops( Abc_Ntk_t * pNtk );
362  Abc_Obj_t * pNode;
363  Mem_Flex_t * pManNew;
364  DdManager * dd = (DdManager *)pNtk->pManFunc;
365  DdNode * bFunc;
366  Vec_Str_t * vCube;
367  int i, fMode;
368 
369  if ( fDirect )
370  fMode = 1;
371  else
372  fMode = -1;
373 
374  assert( Abc_NtkHasBdd(pNtk) );
375  if ( dd->size > 0 )
376  Cudd_zddVarsFromBddVars( dd, 2 );
377  // create the new manager
378  pManNew = Mem_FlexStart();
379 
380  // go through the objects
381  vCube = Vec_StrAlloc( 100 );
382  Abc_NtkForEachNode( pNtk, pNode, i )
383  {
384  if ( Abc_ObjIsBarBuf(pNode) )
385  continue;
386  assert( pNode->pData );
387  bFunc = (DdNode *)pNode->pData;
388  pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, fMode );
389  if ( pNode->pNext == NULL )
390  {
391  Mem_FlexStop( pManNew, 0 );
392  Abc_NtkCleanNext( pNtk );
393 // printf( "Converting from BDDs to SOPs has failed.\n" );
394  Vec_StrFree( vCube );
395  return 0;
396  }
397  }
398  Vec_StrFree( vCube );
399 
400  // update the network type
401  pNtk->ntkFunc = ABC_FUNC_SOP;
402  // set the new manager
403  pNtk->pManFunc = pManNew;
404  // transfer from next to data
405  Abc_NtkForEachNode( pNtk, pNode, i )
406  {
407  if ( Abc_ObjIsBarBuf(pNode) )
408  continue;
409  Cudd_RecursiveDeref( dd, (DdNode *)pNode->pData );
410  pNode->pData = pNode->pNext;
411  pNode->pNext = NULL;
412  }
413 
414  // check for remaining references in the package
415  Extra_StopManager( dd );
416 
417  // reorder fanins and cubes to make SOPs more human-readable
418  Abc_NtkSortSops( pNtk );
419  return 1;
420 }
421 
422 
423 /**Function*************************************************************
424 
425  Synopsis [Derive the SOP from the ZDD representation of the cubes.]
426 
427  Description []
428 
429  SideEffects []
430 
431  SeeAlso []
432 
433 ***********************************************************************/
434 void Abc_ConvertZddToSop_rec( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase, int * pnCubes )
435 {
436  DdNode * zC0, * zC1, * zC2;
437  int Index;
438 
439  if ( zCover == dd->zero )
440  return;
441  if ( zCover == dd->one )
442  {
443  char * pCube;
444  pCube = pSop + (*pnCubes) * (nFanins + 3);
445  sprintf( pCube, "%s %d\n", vCube->pArray, fPhase );
446  (*pnCubes)++;
447  return;
448  }
449  Index = zCover->index/2;
450  assert( Index < nFanins );
451  extraDecomposeCover( dd, zCover, &zC0, &zC1, &zC2 );
452  vCube->pArray[Index] = '0';
453  Abc_ConvertZddToSop_rec( dd, zC0, pSop, nFanins, vCube, fPhase, pnCubes );
454  vCube->pArray[Index] = '1';
455  Abc_ConvertZddToSop_rec( dd, zC1, pSop, nFanins, vCube, fPhase, pnCubes );
456  vCube->pArray[Index] = '-';
457  Abc_ConvertZddToSop_rec( dd, zC2, pSop, nFanins, vCube, fPhase, pnCubes );
458 }
459 
460 /**Function*************************************************************
461 
462  Synopsis [Derive the BDD for the function in the cut.]
463 
464  Description []
465 
466  SideEffects []
467 
468  SeeAlso []
469 
470 ***********************************************************************/
471 int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase )
472 {
473  int nCubes = 0;
474  Abc_ConvertZddToSop_rec( dd, zCover, pSop, nFanins, vCube, fPhase, &nCubes );
475  return nCubes;
476 }
477 
478 
479 /**Function*************************************************************
480 
481  Synopsis [Computes the SOPs of the negative and positive phase of the node.]
482 
483  Description []
484 
485  SideEffects []
486 
487  SeeAlso []
488 
489 ***********************************************************************/
490 void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Mem_Flex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 )
491 {
492  assert( Abc_NtkHasBdd(pNode->pNtk) );
493  *ppSop0 = Abc_ConvertBddToSop( pMmMan, (DdManager *)pNode->pNtk->pManFunc, (DdNode *)pNode->pData, (DdNode *)pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 0 );
494  *ppSop1 = Abc_ConvertBddToSop( pMmMan, (DdManager *)pNode->pNtk->pManFunc, (DdNode *)pNode->pData, (DdNode *)pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 1 );
495 }
496 
497 
498 /**Function*************************************************************
499 
500  Synopsis [Removes complemented SOP covers.]
501 
502  Description []
503 
504  SideEffects []
505 
506  SeeAlso []
507 
508 ***********************************************************************/
510 {
511  DdManager * dd;
512  DdNode * bFunc;
513  Vec_Str_t * vCube;
514  Abc_Obj_t * pNode;
515  int nFaninsMax, fFound, i;
516 
517  assert( Abc_NtkHasSop(pNtk) );
518 
519  // check if there are nodes with complemented SOPs
520  fFound = 0;
521  Abc_NtkForEachNode( pNtk, pNode, i )
522  if ( !Abc_ObjIsBarBuf(pNode) && Abc_SopIsComplement((char *)pNode->pData) )
523  {
524  fFound = 1;
525  break;
526  }
527  if ( !fFound )
528  return;
529 
530  // start the BDD package
531  nFaninsMax = Abc_NtkGetFaninMax( pNtk );
532  if ( nFaninsMax == 0 )
533  printf( "Warning: The network has only constant nodes.\n" );
534  dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
535 
536  // change the cover of negated nodes
537  vCube = Vec_StrAlloc( 100 );
538  Abc_NtkForEachNode( pNtk, pNode, i )
539  if ( !Abc_ObjIsBarBuf(pNode) && Abc_SopIsComplement((char *)pNode->pData) )
540  {
541  bFunc = Abc_ConvertSopToBdd( dd, (char *)pNode->pData, NULL ); Cudd_Ref( bFunc );
542  pNode->pData = Abc_ConvertBddToSop( (Mem_Flex_t *)pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, 1 );
543  Cudd_RecursiveDeref( dd, bFunc );
544  assert( !Abc_SopIsComplement((char *)pNode->pData) );
545  }
546  Vec_StrFree( vCube );
547  Extra_StopManager( dd );
548 }
549 
550 
551 
552 
553 /**Function*************************************************************
554 
555  Synopsis [Count the number of paths in the ZDD.]
556 
557  Description []
558 
559  SideEffects []
560 
561  SeeAlso []
562 
563 ***********************************************************************/
564 void Abc_CountZddCubes_rec( DdManager * dd, DdNode * zCover, int * pnCubes )
565 {
566  DdNode * zC0, * zC1, * zC2;
567  if ( zCover == dd->zero )
568  return;
569  if ( zCover == dd->one )
570  {
571  (*pnCubes)++;
572  return;
573  }
574  if ( (*pnCubes) > ABC_MUX_CUBES )
575  return;
576  extraDecomposeCover( dd, zCover, &zC0, &zC1, &zC2 );
577  Abc_CountZddCubes_rec( dd, zC0, pnCubes );
578  Abc_CountZddCubes_rec( dd, zC1, pnCubes );
579  Abc_CountZddCubes_rec( dd, zC2, pnCubes );
580 }
581 
582 /**Function*************************************************************
583 
584  Synopsis [Count the number of paths in the ZDD.]
585 
586  Description []
587 
588  SideEffects []
589 
590  SeeAlso []
591 
592 ***********************************************************************/
593 int Abc_CountZddCubes( DdManager * dd, DdNode * zCover )
594 {
595  int nCubes = 0;
596  Abc_CountZddCubes_rec( dd, zCover, &nCubes );
597  return nCubes;
598 }
599 
600 
601 /**Function*************************************************************
602 
603  Synopsis [Converts the network from SOP to AIG representation.]
604 
605  Description []
606 
607  SideEffects []
608 
609  SeeAlso []
610 
611 ***********************************************************************/
613 {
614  Abc_Obj_t * pNode;
615  Hop_Man_t * pMan;
616  int i;
617 
618  assert( Abc_NtkHasSop(pNtk) );
619 
620  // make dist1-free and SCC-free
621 // Abc_NtkMakeLegit( pNtk );
622 
623  // start the functionality manager
624  pMan = Hop_ManStart();
625 
626  // convert each node from SOP to BDD
627  Abc_NtkForEachNode( pNtk, pNode, i )
628  {
629  if ( Abc_ObjIsBarBuf(pNode) )
630  continue;
631  assert( pNode->pData );
632  pNode->pData = Abc_ConvertSopToAig( pMan, (char *)pNode->pData );
633  if ( pNode->pData == NULL )
634  {
635  Hop_ManStop( pMan );
636  printf( "Abc_NtkSopToAig: Error while converting SOP into AIG.\n" );
637  return 0;
638  }
639  }
640  Mem_FlexStop( (Mem_Flex_t *)pNtk->pManFunc, 0 );
641  pNtk->pManFunc = pMan;
642 
643  // update the network type
644  pNtk->ntkFunc = ABC_FUNC_AIG;
645  return 1;
646 }
647 
648 
649 /**Function*************************************************************
650 
651  Synopsis [Strashes one logic node using its SOP.]
652 
653  Description []
654 
655  SideEffects []
656 
657  SeeAlso []
658 
659 ***********************************************************************/
661 {
662  Hop_Obj_t * pAnd, * pSum;
663  int i, Value, nFanins;
664  char * pCube;
665  // get the number of variables
666  nFanins = Abc_SopGetVarNum(pSop);
667  if ( Abc_SopIsExorType(pSop) )
668  {
669  pSum = Hop_ManConst0(pMan);
670  for ( i = 0; i < nFanins; i++ )
671  pSum = Hop_Exor( pMan, pSum, Hop_IthVar(pMan,i) );
672  }
673  else
674  {
675  // go through the cubes of the node's SOP
676  pSum = Hop_ManConst0(pMan);
677  Abc_SopForEachCube( pSop, nFanins, pCube )
678  {
679  // create the AND of literals
680  pAnd = Hop_ManConst1(pMan);
681  Abc_CubeForEachVar( pCube, Value, i )
682  {
683  if ( Value == '1' )
684  pAnd = Hop_And( pMan, pAnd, Hop_IthVar(pMan,i) );
685  else if ( Value == '0' )
686  pAnd = Hop_And( pMan, pAnd, Hop_Not(Hop_IthVar(pMan,i)) );
687  }
688  // add to the sum of cubes
689  pSum = Hop_Or( pMan, pSum, pAnd );
690  }
691  }
692  // decide whether to complement the result
693  if ( Abc_SopIsComplement(pSop) )
694  pSum = Hop_Not(pSum);
695  return pSum;
696 }
697 
698 /**Function*************************************************************
699 
700  Synopsis [Converts the network from AIG to BDD representation.]
701 
702  Description []
703 
704  SideEffects []
705 
706  SeeAlso []
707 
708 ***********************************************************************/
709 Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop )
710 {
711  extern Hop_Obj_t * Dec_GraphFactorSop( Hop_Man_t * pMan, char * pSop );
712  int fUseFactor = 1;
713  // consider the constant node
714  if ( Abc_SopGetVarNum(pSop) == 0 )
715  return Hop_NotCond( Hop_ManConst1(pMan), Abc_SopIsConst0(pSop) );
716  // decide when to use factoring
717  if ( fUseFactor && Abc_SopGetVarNum(pSop) > 2 && Abc_SopGetCubeNum(pSop) > 1 && !Abc_SopIsExorType(pSop) )
718  return Dec_GraphFactorSop( pMan, pSop );
719  return Abc_ConvertSopToAigInternal( pMan, pSop );
720 }
721 
722 /**Function*************************************************************
723 
724  Synopsis [Converts the network from AIG to BDD representation.]
725 
726  Description []
727 
728  SideEffects []
729 
730  SeeAlso []
731 
732 ***********************************************************************/
734 {
735  Abc_Obj_t * pNode;
736  Hop_Man_t * pMan;
737  DdNode * pFunc;
738  DdManager * dd, * ddTemp = NULL;
739  Vec_Int_t * vFanins = NULL;
740  int nFaninsMax, i, k, iVar;
741 
742  assert( Abc_NtkHasAig(pNtk) );
743 
744  // start the functionality manager
745  nFaninsMax = Abc_NtkGetFaninMax( pNtk );
746  if ( nFaninsMax == 0 )
747  printf( "Warning: The network has only constant nodes.\n" );
748 
749  dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
750 
751  // start temporary manager for reordered local functions
752  ddTemp = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
754  vFanins = Vec_IntAlloc( nFaninsMax );
755 
756  // set the mapping of elementary AIG nodes into the elementary BDD nodes
757  pMan = (Hop_Man_t *)pNtk->pManFunc;
758  assert( Hop_ManPiNum(pMan) >= nFaninsMax );
759  for ( i = 0; i < nFaninsMax; i++ )
760  Hop_ManPi(pMan, i)->pData = Cudd_bddIthVar(ddTemp, i);
761 
762  // convert each node from SOP to BDD
763  Abc_NtkForEachNode( pNtk, pNode, i )
764  {
765  if ( Abc_ObjIsBarBuf(pNode) )
766  continue;
767  pFunc = Abc_ConvertAigToBdd( ddTemp, (Hop_Obj_t *)pNode->pData );
768  if ( pFunc == NULL )
769  {
770  printf( "Abc_NtkAigToBdd: Error while converting AIG into BDD.\n" );
771  return 0;
772  }
773  Cudd_Ref( pFunc );
774  // find variable mapping
775  Vec_IntFill( vFanins, Abc_ObjFaninNum(pNode), -1 );
776  for ( k = iVar = 0; k < nFaninsMax; k++ )
777  if ( ddTemp->invperm[k] < Abc_ObjFaninNum(pNode) )
778  Vec_IntWriteEntry( vFanins, ddTemp->invperm[k], iVar++ );
779  assert( iVar == Abc_ObjFaninNum(pNode) );
780  // transfer to the main manager
781  pNode->pData = Extra_TransferPermute( ddTemp, dd, pFunc, Vec_IntArray(vFanins) );
782  Cudd_Ref( (DdNode *)pNode->pData );
783  Cudd_RecursiveDeref( ddTemp, pFunc );
784  // update variable order
785  Vec_IntClear( vFanins );
786  for ( k = 0; k < nFaninsMax; k++ )
787  if ( ddTemp->invperm[k] < Abc_ObjFaninNum(pNode) )
788  Vec_IntPush( vFanins, Vec_IntEntry(&pNode->vFanins, ddTemp->invperm[k]) );
789  for ( k = 0; k < Abc_ObjFaninNum(pNode); k++ )
790  Vec_IntWriteEntry( &pNode->vFanins, k, Vec_IntEntry(vFanins, k) );
791  }
792 
793 // printf( "Reorderings performed = %d.\n", Cudd_ReadReorderings(ddTemp) );
794  Extra_StopManager( ddTemp );
795  Vec_IntFreeP( &vFanins );
796  Hop_ManStop( (Hop_Man_t *)pNtk->pManFunc );
797  pNtk->pManFunc = dd;
798 
799  // update the network type
800  pNtk->ntkFunc = ABC_FUNC_BDD;
801  return 1;
802 }
803 
804 /**Function*************************************************************
805 
806  Synopsis [Construct BDDs and mark AIG nodes.]
807 
808  Description []
809 
810  SideEffects []
811 
812  SeeAlso []
813 
814 ***********************************************************************/
816 {
817  assert( !Hop_IsComplement(pObj) );
818  if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
819  return;
822  pObj->pData = Cudd_bddAnd( dd, (DdNode *)Hop_ObjChild0Copy(pObj), (DdNode *)Hop_ObjChild1Copy(pObj) );
823  Cudd_Ref( (DdNode *)pObj->pData );
824  assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
825  Hop_ObjSetMarkA( pObj );
826 }
827 
828 /**Function*************************************************************
829 
830  Synopsis [Dereference BDDs and unmark AIG nodes.]
831 
832  Description []
833 
834  SideEffects []
835 
836  SeeAlso []
837 
838 ***********************************************************************/
840 {
841  assert( !Hop_IsComplement(pObj) );
842  if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
843  return;
846  Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
847  pObj->pData = NULL;
848  assert( Hop_ObjIsMarkA(pObj) ); // loop detection
849  Hop_ObjClearMarkA( pObj );
850 }
851 
852 /**Function*************************************************************
853 
854  Synopsis [Converts the network from AIG to BDD representation.]
855 
856  Description []
857 
858  SideEffects []
859 
860  SeeAlso []
861 
862 ***********************************************************************/
864 {
865  DdNode * bFunc;
866  // check the case of a constant
867  if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
868  return Cudd_NotCond( Cudd_ReadOne(dd), Hop_IsComplement(pRoot) );
869  // construct BDD
871  // hold on to the result
872  bFunc = Cudd_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) ); Cudd_Ref( bFunc );
873  // dereference BDD
875  // return the result
876  Cudd_Deref( bFunc );
877  return bFunc;
878 }
879 
880 
881 
882 /**Function*************************************************************
883 
884  Synopsis [Converts the network from AIG to GIA representation.]
885 
886  Description []
887 
888  SideEffects []
889 
890  SeeAlso []
891 
892 ***********************************************************************/
894 {
895  assert( !Hop_IsComplement(pObj) );
896  if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
897  return;
901  assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
902  Hop_ObjSetMarkA( pObj );
903 }
905 {
906  assert( !Hop_IsComplement(pObj) );
907  if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
908  return;
911  assert( Hop_ObjIsMarkA(pObj) ); // loop detection
912  Hop_ObjClearMarkA( pObj );
913 }
915 {
916  assert( !Hop_IsComplement(pRoot) );
917  if ( Hop_ObjIsConst1( pRoot ) )
918  return 1;
919  Abc_ConvertAigToGia_rec1( p, pRoot );
920  Abc_ConvertAigToGia_rec2( pRoot );
921  return pRoot->iData;
922 }
923 
924 /**Function*************************************************************
925 
926  Synopsis [Converts the network from AIG to BDD representation.]
927 
928  Description []
929 
930  SideEffects []
931 
932  SeeAlso []
933 
934 ***********************************************************************/
936 {
937  Gia_Man_t * pNew;
938  Hop_Man_t * pHopMan;
939  Hop_Obj_t * pHopObj;
940  Vec_Int_t * vMapping;
941  Vec_Ptr_t * vNodes;
942  Abc_Obj_t * pNode, * pFanin;
943  int i, k, nObjs;
945  pHopMan = (Hop_Man_t *)p->pManFunc;
946  // create new manager
947  pNew = Gia_ManStart( 10000 );
948  pNew->pName = Abc_UtilStrsav( Abc_NtkName(p) );
949  pNew->pSpec = Abc_UtilStrsav( Abc_NtkSpec(p) );
950  Abc_NtkCleanCopy( p );
951  Hop_ManConst1(pHopMan)->iData = 1;
952  // create primary inputs
953  Abc_NtkForEachCi( p, pNode, i )
954  pNode->iTemp = Gia_ManAppendCi(pNew);
955  // find the number of objects
956  nObjs = 1 + Abc_NtkCiNum(p) + Abc_NtkCoNum(p);
957  Abc_NtkForEachNode( p, pNode, i )
958  nObjs += Abc_ObjIsBarBuf(pNode) ? 1 : Hop_DagSize( (Hop_Obj_t *)pNode->pData );
959  vMapping = Vec_IntStart( nObjs );
960  // iterate through nodes used in the mapping
961  vNodes = Abc_NtkDfs( p, 0 );
962  Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
963  {
964  if ( Abc_ObjIsBarBuf(pNode) )
965  {
966  assert( !Abc_ObjFaninC0(pNode) );
967  pNode->iTemp = Gia_ManAppendBuf( pNew, Abc_ObjFanin0(pNode)->iTemp );
968  continue;
969  }
970  Abc_ObjForEachFanin( pNode, pFanin, k )
971  Hop_ManPi(pHopMan, k)->iData = pFanin->iTemp;
972  pHopObj = Hop_Regular( (Hop_Obj_t *)pNode->pData );
973  if ( Hop_DagSize(pHopObj) > 0 )
974  {
975  assert( Abc_ObjFaninNum(pNode) <= Hop_ManPiNum(pHopMan) );
976  Abc_ConvertAigToGia( pNew, pHopObj );
977  if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, Abc_Lit2Var(pHopObj->iData))) )
978  continue;
979  if ( Vec_IntEntry(vMapping, Abc_Lit2Var(pHopObj->iData)) )
980  continue;
981  Vec_IntWriteEntry( vMapping, Abc_Lit2Var(pHopObj->iData), Vec_IntSize(vMapping) );
982  Vec_IntPush( vMapping, Abc_ObjFaninNum(pNode) );
983  Abc_ObjForEachFanin( pNode, pFanin, k )
984  Vec_IntPush( vMapping, Abc_Lit2Var(pFanin->iTemp) );
985  Vec_IntPush( vMapping, Abc_Lit2Var(pHopObj->iData) );
986  }
987  pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) );
988  }
989  Vec_PtrFree( vNodes );
990  // create primary outputs
991  Abc_NtkForEachCo( p, pNode, i )
992  Gia_ManAppendCo( pNew, Abc_ObjFanin0(pNode)->iTemp );
993  Gia_ManSetRegNum( pNew, Abc_NtkLatchNum(p) );
994  // finish mapping
995  assert( Gia_ManObjNum(pNew) <= nObjs );
996  assert( pNew->vMapping == NULL );
997  pNew->vMapping = vMapping;
998  return pNew;
999 }
1000 
1001 
1002 /**Function*************************************************************
1003 
1004  Synopsis [Construct BDDs and mark AIG nodes.]
1005 
1006  Description []
1007 
1008  SideEffects []
1009 
1010  SeeAlso []
1011 
1012 ***********************************************************************/
1014 {
1015  assert( !Hop_IsComplement(pObj) );
1016  if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
1017  return;
1018  Abc_ConvertAigToAig_rec( pNtkAig, Hop_ObjFanin0(pObj) );
1019  Abc_ConvertAigToAig_rec( pNtkAig, Hop_ObjFanin1(pObj) );
1020  pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkAig->pManFunc, (Abc_Obj_t *)Hop_ObjChild0Copy(pObj), (Abc_Obj_t *)Hop_ObjChild1Copy(pObj) );
1021  assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
1022  Hop_ObjSetMarkA( pObj );
1023 }
1024 
1025 /**Function*************************************************************
1026 
1027  Synopsis [Converts the network from AIG to BDD representation.]
1028 
1029  Description []
1030 
1031  SideEffects []
1032 
1033  SeeAlso []
1034 
1035 ***********************************************************************/
1037 {
1038  Hop_Man_t * pHopMan;
1039  Hop_Obj_t * pRoot;
1040  Abc_Obj_t * pFanin;
1041  int i;
1042  // get the local AIG
1043  pHopMan = (Hop_Man_t *)pObjOld->pNtk->pManFunc;
1044  pRoot = (Hop_Obj_t *)pObjOld->pData;
1045  // check the case of a constant
1046  if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
1047  return Abc_ObjNotCond( Abc_AigConst1(pNtkAig), Hop_IsComplement(pRoot) );
1048  // assign the fanin nodes
1049  Abc_ObjForEachFanin( pObjOld, pFanin, i )
1050  {
1051  assert( pFanin->pCopy != NULL );
1052  Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
1053  }
1054  // construct the AIG
1055  Abc_ConvertAigToAig_rec( pNtkAig, Hop_Regular(pRoot) );
1056  Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
1057  // return the result
1058  return Abc_ObjNotCond( (Abc_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
1059 }
1060 
1061 
1062 /**Function*************************************************************
1063 
1064  Synopsis [Unmaps the network.]
1065 
1066  Description []
1067 
1068  SideEffects []
1069 
1070  SeeAlso []
1071 
1072 ***********************************************************************/
1074 {
1075  extern void * Abc_FrameReadLibGen();
1076  Abc_Obj_t * pNode;
1077  char * pSop;
1078  int i;
1079 
1080  assert( Abc_NtkHasMapping(pNtk) );
1081  // update the functionality manager
1082  assert( pNtk->pManFunc == Abc_FrameReadLibGen() );
1083  pNtk->pManFunc = Mem_FlexStart();
1084  pNtk->ntkFunc = ABC_FUNC_SOP;
1085  // update the nodes
1086  Abc_NtkForEachNode( pNtk, pNode, i )
1087  {
1088  if ( Abc_ObjIsBarBuf(pNode) )
1089  continue;
1090  pSop = Mio_GateReadSop((Mio_Gate_t *)pNode->pData);
1091  assert( Abc_SopGetVarNum(pSop) == Abc_ObjFaninNum(pNode) );
1092  pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, pSop );
1093  }
1094  return 1;
1095 }
1096 
1097 /**Function*************************************************************
1098 
1099  Synopsis [Converts SOP functions into BLIF-MV functions.]
1100 
1101  Description []
1102 
1103  SideEffects []
1104 
1105  SeeAlso []
1106 
1107 ***********************************************************************/
1109 {
1110  return 1;
1111 }
1112 
1113 /**Function*************************************************************
1114 
1115  Synopsis [Convers logic network to the SOP form.]
1116 
1117  Description []
1118 
1119  SideEffects []
1120 
1121  SeeAlso []
1122 
1123 ***********************************************************************/
1124 int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect )
1125 {
1126  assert( !Abc_NtkIsStrash(pNtk) );
1127  if ( Abc_NtkHasSop(pNtk) )
1128  {
1129  if ( !fDirect )
1130  return 1;
1131  if ( !Abc_NtkSopToBdd(pNtk) )
1132  return 0;
1133  return Abc_NtkBddToSop(pNtk, fDirect);
1134  }
1135  if ( Abc_NtkHasMapping(pNtk) )
1136  return Abc_NtkMapToSop(pNtk);
1137  if ( Abc_NtkHasBdd(pNtk) )
1138  return Abc_NtkBddToSop(pNtk, fDirect);
1139  if ( Abc_NtkHasAig(pNtk) )
1140  {
1141  if ( !Abc_NtkAigToBdd(pNtk) )
1142  return 0;
1143  return Abc_NtkBddToSop(pNtk, fDirect);
1144  }
1145  assert( 0 );
1146  return 0;
1147 }
1148 
1149 /**Function*************************************************************
1150 
1151  Synopsis [Convers logic network to the SOP form.]
1152 
1153  Description []
1154 
1155  SideEffects []
1156 
1157  SeeAlso []
1158 
1159 ***********************************************************************/
1161 {
1162  assert( !Abc_NtkIsStrash(pNtk) );
1163  if ( Abc_NtkHasBdd(pNtk) )
1164  return 1;
1165  if ( Abc_NtkHasMapping(pNtk) )
1166  {
1167  Abc_NtkMapToSop(pNtk);
1168  return Abc_NtkSopToBdd(pNtk);
1169  }
1170  if ( Abc_NtkHasSop(pNtk) )
1171  {
1172  Abc_NtkSopToAig(pNtk);
1173  return Abc_NtkAigToBdd(pNtk);
1174  }
1175  if ( Abc_NtkHasAig(pNtk) )
1176  return Abc_NtkAigToBdd(pNtk);
1177  assert( 0 );
1178  return 0;
1179 }
1180 
1181 /**Function*************************************************************
1182 
1183  Synopsis [Convers logic network to the SOP form.]
1184 
1185  Description []
1186 
1187  SideEffects []
1188 
1189  SeeAlso []
1190 
1191 ***********************************************************************/
1193 {
1194  assert( !Abc_NtkIsStrash(pNtk) );
1195  if ( Abc_NtkHasAig(pNtk) )
1196  return 1;
1197  if ( Abc_NtkHasMapping(pNtk) )
1198  {
1199  Abc_NtkMapToSop(pNtk);
1200  return Abc_NtkSopToAig(pNtk);
1201  }
1202  if ( Abc_NtkHasBdd(pNtk) )
1203  {
1204  if ( !Abc_NtkBddToSop(pNtk,0) )
1205  return 0;
1206  return Abc_NtkSopToAig(pNtk);
1207  }
1208  if ( Abc_NtkHasSop(pNtk) )
1209  return Abc_NtkSopToAig(pNtk);
1210  assert( 0 );
1211  return 0;
1212 }
1213 
1214 
1215 ////////////////////////////////////////////////////////////////////////
1216 /// END OF FILE ///
1217 ////////////////////////////////////////////////////////////////////////
1218 
1219 
1221 
int iTemp
Definition: abc.h:149
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static Hop_Obj_t * Hop_ObjFanin1(Hop_Obj_t *pObj)
Definition: hop.h:183
static int Hop_ObjIsMarkA(Hop_Obj_t *pObj)
Definition: hop.h:164
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
int Abc_CountZddCubes(DdManager *dd, DdNode *zCover)
Definition: abcFunc.c:593
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static void Hop_ObjSetMarkA(Hop_Obj_t *pObj)
Definition: hop.h:165
static int Abc_NtkHasBdd(Abc_Ntk_t *pNtk)
Definition: abc.h:254
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
ABC_DLL void * Abc_FrameReadLibGen()
Definition: mainFrame.c:56
Hop_Obj_t * Hop_Or(Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1)
Definition: hopOper.c:171
static int Abc_NtkHasSop(Abc_Ntk_t *pNtk)
Definition: abc.h:253
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
#define Cudd_Not(node)
Definition: cudd.h:367
void Abc_ConvertAigToBdd_rec2(DdManager *dd, Hop_Obj_t *pObj)
Definition: abcFunc.c:839
static Hop_Obj_t * Hop_ManConst1(Hop_Man_t *p)
Definition: hop.h:132
ABC_DLL Abc_Obj_t * Abc_AigConst1(Abc_Ntk_t *pNtk)
Definition: abcAig.c:683
Hop_Obj_t * Hop_And(Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1)
Definition: hopOper.c:104
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
int Hop_DagSize(Hop_Obj_t *pObj)
Definition: hopDfs.c:279
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
int size
Definition: cuddInt.h:361
#define Abc_SopForEachCube(pSop, nFanins, pCube)
Definition: abc.h:531
static int Hop_ObjIsNode(Hop_Obj_t *pObj)
Definition: hop.h:160
#define Cudd_IsConstant(node)
Definition: cudd.h:352
DdNode * Cudd_ReadLogicZero(DdManager *dd)
Definition: cuddAPI.c:1058
ABC_DLL int Abc_SopGetCubeNum(char *pSop)
Definition: abcSop.c:489
DdNode * zero
Definition: cuddInt.h:346
int iData
Definition: hop.h:69
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
int Abc_NtkBddToSop(Abc_Ntk_t *pNtk, int fDirect)
Definition: abcFunc.c:359
DdNode * Extra_TransferPermute(DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
Definition: extraBddMisc.c:87
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
static int Abc_ObjIsBarBuf(Abc_Obj_t *pObj)
Definition: abc.h:360
static int Abc_NtkHasMapping(Abc_Ntk_t *pNtk)
Definition: abc.h:256
ABC_DLL int Abc_NtkGetFaninMax(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:453
static int Abc_NtkLatchNum(Abc_Ntk_t *pNtk)
Definition: abc.h:294
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
static int Hop_ObjChild0CopyI(Hop_Obj_t *pObj)
Definition: hop.h:188
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
Vec_Int_t vFanins
Definition: abc.h:143
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
Gia_Man_t * Abc_NtkAigToGia(Abc_Ntk_t *p)
Definition: abcFunc.c:935
void Abc_CountZddCubes_rec(DdManager *dd, DdNode *zCover, int *pnCubes)
Definition: abcFunc.c:564
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
int Abc_NtkToAig(Abc_Ntk_t *pNtk)
Definition: abcFunc.c:1192
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
#define Abc_CubeForEachVar(pCube, Value, i)
Definition: abc.h:529
ABC_DLL Vec_Ptr_t * Abc_NtkDfs(Abc_Ntk_t *pNtk, int fCollectAll)
Definition: abcDfs.c:81
ABC_DLL int Abc_SopIsExorType(char *pSop)
Definition: abcSop.c:802
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
static void Vec_StrPush(Vec_Str_t *p, char Entry)
Definition: vecStr.h:535
static int Abc_NtkIsAigLogic(Abc_Ntk_t *pNtk)
Definition: abc.h:266
static Hop_Obj_t * Hop_Not(Hop_Obj_t *p)
Definition: hop.h:127
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Definition: hop.h:65
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
static int Abc_NtkCoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:288
DECLARATIONS ///.
Definition: abcAig.c:52
int Abc_NtkToSop(Abc_Ntk_t *pNtk, int fDirect)
Definition: abcFunc.c:1124
DdNode * Extra_zddPrimes(DdManager *dd, DdNode *F)
Definition: extraBddMisc.c:933
void Hop_ConeUnmark_rec(Hop_Obj_t *pObj)
Definition: hopDfs.c:257
char * Mem_FlexEntryFetch(Mem_Flex_t *p, int nBytes)
Definition: mem.c:372
Hop_Obj_t * Hop_Exor(Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1)
Definition: hopOper.c:138
void Abc_ConvertAigToGia_rec2(Hop_Obj_t *pObj)
Definition: abcFunc.c:904
int Abc_NtkAigToBdd(Abc_Ntk_t *pNtk)
Definition: abcFunc.c:733
void Hop_ManStop(Hop_Man_t *p)
Definition: hopMan.c:84
int Abc_ConvertAigToGia(Gia_Man_t *p, Hop_Obj_t *pRoot)
Definition: abcFunc.c:914
void extraDecomposeCover(DdManager *dd, DdNode *zC, DdNode **zC0, DdNode **zC1, DdNode **zC2)
static Hop_Obj_t * Hop_ManPi(Hop_Man_t *p, int i)
Definition: hop.h:134
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
void * pManFunc
Definition: abc.h:191
Mem_Flex_t * Mem_FlexStart()
Definition: mem.c:311
ABC_DLL Abc_Obj_t * Abc_AigAnd(Abc_Aig_t *pMan, Abc_Obj_t *p0, Abc_Obj_t *p1)
Definition: abcAig.c:700
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
ABC_DLL char * Abc_SopRegister(Mem_Flex_t *pMan, char *pName)
DECLARATIONS ///.
Definition: abcSop.c:56
Hop_Obj_t * Abc_ConvertSopToAigInternal(Hop_Man_t *pMan, char *pSop)
Definition: abcFunc.c:660
Abc_Obj_t * pCopy
Definition: abc.h:148
char * pArray
Definition: bblif.c:51
char * pName
Definition: gia.h:97
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
char * Abc_ConvertBddToSop(Mem_Flex_t *pMan, DdManager *dd, DdNode *bFuncOn, DdNode *bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t *vCube, int fMode)
Definition: abcFunc.c:209
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
static Hop_Obj_t * Hop_ObjChild1Copy(Hop_Obj_t *pObj)
Definition: hop.h:187
Hop_Obj_t * Dec_GraphFactorSop(Hop_Man_t *pMan, char *pSop)
Definition: decAbc.c:301
static int Gia_ManAppendBuf(Gia_Man_t *p, int iLit)
Definition: gia.h:694
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static void Vec_StrFill(Vec_Str_t *p, int nSize, char Fill)
Definition: vecStr.h:423
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
void Abc_NtkLogicMakeDirectSops(Abc_Ntk_t *pNtk)
Definition: abcFunc.c:509
if(last==0)
Definition: sparse_int.h:34
char * pSpec
Definition: gia.h:98
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Hop_Man_t * Hop_ManStart()
DECLARATIONS ///.
Definition: hopMan.c:45
void Abc_ConvertAigToAig_rec(Abc_Ntk_t *pNtkAig, Hop_Obj_t *pObj)
Definition: abcFunc.c:1013
ABC_DLL void Abc_NtkCleanNext(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:636
static int Hop_IsComplement(Hop_Obj_t *p)
Definition: hop.h:129
DdNode * Cudd_zddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Definition: cuddZddIsop.c:136
static Hop_Obj_t * Hop_ObjChild0Copy(Hop_Obj_t *pObj)
Definition: hop.h:186
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
ABC_DLL int Abc_SopIsConst0(char *pSop)
Definition: abcSop.c:676
int Abc_NtkMapToSop(Abc_Ntk_t *pNtk)
Definition: abcFunc.c:1073
char * sprintf()
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
static void Hop_ObjClearMarkA(Hop_Obj_t *pObj)
Definition: hop.h:166
void * pData
Definition: hop.h:68
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
void Abc_ConvertAigToBdd_rec1(DdManager *dd, Hop_Obj_t *pObj)
Definition: abcFunc.c:815
static Hop_Obj_t * Hop_ObjFanin0(Hop_Obj_t *pObj)
Definition: hop.h:182
void Abc_ConvertAigToGia_rec1(Gia_Man_t *p, Hop_Obj_t *pObj)
Definition: abcFunc.c:893
static int Hop_ObjIsConst1(Hop_Obj_t *pObj)
Definition: hop.h:155
void Abc_NtkSortSops(Abc_Ntk_t *pNtk)
Definition: abcFanOrder.c:348
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition: abc.h:461
void Mem_FlexStop(Mem_Flex_t *p, int fVerbose)
Definition: mem.c:343
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static int Gia_ManAppendAnd2(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:627
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
static int Hop_ObjChild1CopyI(Hop_Obj_t *pObj)
Definition: hop.h:189
static Hop_Obj_t * Abc_ConvertSopToAig(Hop_Man_t *pMan, char *pSop)
Definition: abcFunc.c:709
Abc_Ntk_t * pNtk
Definition: abc.h:130
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static char * Abc_NtkName(Abc_Ntk_t *pNtk)
Definition: abc.h:270
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
Abc_NtkFunc_t ntkFunc
Definition: abc.h:157
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition: abc.h:524
int Abc_ConvertZddToSop(DdManager *dd, DdNode *zCover, char *pSop, int nFanins, Vec_Str_t *vCube, int fPhase)
DECLARATIONS ///.
Definition: abcFunc.c:471
static Hop_Obj_t * Hop_NotCond(Hop_Obj_t *p, int c)
Definition: hop.h:128
DdHalfWord index
Definition: cudd.h:279
Definition: gia.h:95
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
DdNode * Cudd_bddXor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:476
int Abc_NtkSopToBdd(Abc_Ntk_t *pNtk)
Definition: abcFunc.c:113
DdNode * one
Definition: cuddInt.h:345
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
void Abc_NodeBddToCnf(Abc_Obj_t *pNode, Mem_Flex_t *pMmMan, Vec_Str_t *vCube, int fAllPrimes, char **ppSop0, char **ppSop1)
Definition: abcFunc.c:490
ABC_DLL int Abc_SopGetVarNum(char *pSop)
Definition: abcSop.c:536
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Abc_Obj_t * pNext
Definition: abc.h:131
ABC_DLL void Abc_NtkCleanCopy(Abc_Ntk_t *pNtk)
Definition: abcUtil.c:507
int Cudd_zddVarsFromBddVars(DdManager *dd, int multiplicity)
Definition: cuddAPI.c:519
static Abc_Obj_t * Abc_ObjNotCond(Abc_Obj_t *p, int c)
Definition: abc.h:325
int Abc_NtkSopToAig(Abc_Ntk_t *pNtk)
Definition: abcFunc.c:612
#define assert(ex)
Definition: util_old.h:213
static int Abc_NtkHasAig(Abc_Ntk_t *pNtk)
Definition: abc.h:255
int * invperm
Definition: cuddInt.h:388
static Hop_Obj_t * Hop_ManConst0(Hop_Man_t *p)
Definition: hop.h:131
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:669
int Abc_NtkSopToBlifMv(Abc_Ntk_t *pNtk)
Definition: abcFunc.c:1108
static char * Abc_NtkSpec(Abc_Ntk_t *pNtk)
Definition: abc.h:271
void * pData
Definition: abc.h:145
#define ABC_MUX_CUBES
DECLARATIONS ///.
Definition: abcFunc.c:33
DdNode * Abc_ConvertSopToBdd(DdManager *dd, char *pSop, DdNode **pbVars)
FUNCTION DEFINITIONS ///.
Definition: abcFunc.c:56
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Vec_Int_t * vMapping
Definition: gia.h:131
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_Obj_t * Abc_ConvertAigToAig(Abc_Ntk_t *pNtkAig, Abc_Obj_t *pObjOld)
DECLARATIONS ///.
Definition: abcFunc.c:1036
static Hop_Obj_t * Hop_Regular(Hop_Obj_t *p)
Definition: hop.h:126
void Abc_ConvertZddToSop_rec(DdManager *dd, DdNode *zCover, char *pSop, int nFanins, Vec_Str_t *vCube, int fPhase, int *pnCubes)
Definition: abcFunc.c:434
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
int Abc_NtkToBdd(Abc_Ntk_t *pNtk)
Definition: abcFunc.c:1160
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
ABC_DLL int Abc_SopIsComplement(char *pSop)
Definition: abcSop.c:655
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition: hop.h:49
char * Mio_GateReadSop(Mio_Gate_t *pGate)
Definition: mioApi.c:153
Hop_Obj_t * Hop_IthVar(Hop_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Definition: hopOper.c:63
ABC_DLL int Abc_SopGetPhase(char *pSop)
Definition: abcSop.c:556
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static DdNode * Abc_ConvertAigToBdd(DdManager *dd, Hop_Obj_t *pRoot)
Definition: abcFunc.c:863
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
static int Hop_ManPiNum(Hop_Man_t *p)
Definition: hop.h:145