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
25 #ifdef ABC_USE_CUDD
26 #include "bdd/extrab/extraBdd.h"
27 #endif
28
29 ABC_NAMESPACE_IMPL_START
30
31
32 ////////////////////////////////////////////////////////////////////////
33 /// DECLARATIONS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 #define ABC_MAX_CUBES 100000
37
38 static Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop );
39
40 #ifdef ABC_USE_CUDD
41
42 int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
43 static DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot);
44 extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
45
46 ////////////////////////////////////////////////////////////////////////
47 /// FUNCTION DEFINITIONS ///
48 ////////////////////////////////////////////////////////////////////////
49
50 /**Function*************************************************************
51
52 Synopsis [Converts the node from SOP to BDD representation.]
53
54 Description []
55
56 SideEffects []
57
58 SeeAlso []
59
60 ***********************************************************************/
Abc_ConvertSopToBdd(DdManager * dd,char * pSop,DdNode ** pbVars)61 DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, DdNode ** pbVars )
62 {
63 DdNode * bSum, * bCube, * bTemp, * bVar;
64 char * pCube;
65 int nVars, Value, v;
66
67 // start the cover
68 nVars = Abc_SopGetVarNum(pSop);
69 bSum = Cudd_ReadLogicZero(dd); Cudd_Ref( bSum );
70 if ( Abc_SopIsExorType(pSop) )
71 {
72 for ( v = 0; v < nVars; v++ )
73 {
74 bSum = Cudd_bddXor( dd, bTemp = bSum, pbVars? pbVars[v] : Cudd_bddIthVar(dd, v) ); Cudd_Ref( bSum );
75 Cudd_RecursiveDeref( dd, bTemp );
76 }
77 }
78 else
79 {
80 // check the logic function of the node
81 Abc_SopForEachCube( pSop, nVars, pCube )
82 {
83 bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube );
84 Abc_CubeForEachVar( pCube, Value, v )
85 {
86 if ( Value == '0' )
87 bVar = Cudd_Not( pbVars? pbVars[v] : Cudd_bddIthVar( dd, v ) );
88 else if ( Value == '1' )
89 bVar = pbVars? pbVars[v] : Cudd_bddIthVar( dd, v );
90 else
91 continue;
92 bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube );
93 Cudd_RecursiveDeref( dd, bTemp );
94 }
95 bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );
96 Cudd_Ref( bSum );
97 Cudd_RecursiveDeref( dd, bTemp );
98 Cudd_RecursiveDeref( dd, bCube );
99 }
100 }
101 // complement the result if necessary
102 bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) );
103 Cudd_Deref( bSum );
104 return bSum;
105 }
106
107 /**Function*************************************************************
108
109 Synopsis [Converts the network from SOP to BDD representation.]
110
111 Description []
112
113 SideEffects []
114
115 SeeAlso []
116
117 ***********************************************************************/
Abc_NtkSopToBdd(Abc_Ntk_t * pNtk)118 int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
119 {
120 Abc_Obj_t * pNode;
121 DdManager * dd, * ddTemp = NULL;
122 Vec_Int_t * vFanins = NULL;
123 int nFaninsMax, i, k, iVar;
124
125 assert( Abc_NtkHasSop(pNtk) );
126
127 // start the functionality manager
128 nFaninsMax = Abc_NtkGetFaninMax( pNtk );
129 if ( nFaninsMax == 0 )
130 printf( "Warning: The network has only constant nodes.\n" );
131 dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
132
133 // start temporary manager for reordered local functions
134 if ( nFaninsMax > 10 )
135 {
136 ddTemp = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
137 Cudd_AutodynEnable( ddTemp, CUDD_REORDER_SYMM_SIFT );
138 vFanins = Vec_IntAlloc( nFaninsMax );
139 }
140
141 // convert each node from SOP to BDD
142 Abc_NtkForEachNode( pNtk, pNode, i )
143 {
144 if ( Abc_ObjIsBarBuf(pNode) )
145 continue;
146 assert( pNode->pData );
147 if ( Abc_ObjFaninNum(pNode) > 10 )
148 {
149 DdNode * pFunc = Abc_ConvertSopToBdd( ddTemp, (char *)pNode->pData, NULL );
150 if ( pFunc == NULL )
151 {
152 printf( "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
153 return 0;
154 }
155 Cudd_Ref( pFunc );
156 // find variable mapping
157 Vec_IntFill( vFanins, Abc_ObjFaninNum(pNode), -1 );
158 for ( k = iVar = 0; k < nFaninsMax; k++ )
159 if ( ddTemp->invperm[k] < Abc_ObjFaninNum(pNode) )
160 Vec_IntWriteEntry( vFanins, ddTemp->invperm[k], iVar++ );
161 assert( iVar == Abc_ObjFaninNum(pNode) );
162 // transfer to the main manager
163 pNode->pData = Extra_TransferPermute( ddTemp, dd, pFunc, Vec_IntArray(vFanins) );
164 Cudd_Ref( (DdNode *)pNode->pData );
165 Cudd_RecursiveDeref( ddTemp, pFunc );
166 // update variable order
167 Vec_IntClear( vFanins );
168 for ( k = 0; k < nFaninsMax; k++ )
169 if ( ddTemp->invperm[k] < Abc_ObjFaninNum(pNode) )
170 Vec_IntPush( vFanins, Vec_IntEntry(&pNode->vFanins, ddTemp->invperm[k]) );
171 for ( k = 0; k < Abc_ObjFaninNum(pNode); k++ )
172 Vec_IntWriteEntry( &pNode->vFanins, k, Vec_IntEntry(vFanins, k) );
173 }
174 else
175 {
176 pNode->pData = Abc_ConvertSopToBdd( dd, (char *)pNode->pData, NULL );
177 if ( pNode->pData == NULL )
178 {
179 printf( "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
180 return 0;
181 }
182 Cudd_Ref( (DdNode *)pNode->pData );
183 }
184 }
185
186 if ( ddTemp )
187 {
188 // printf( "Reorderings performed = %d.\n", Cudd_ReadReorderings(ddTemp) );
189 Extra_StopManager( ddTemp );
190 }
191 Vec_IntFreeP( &vFanins );
192 Mem_FlexStop( (Mem_Flex_t *)pNtk->pManFunc, 0 );
193 pNtk->pManFunc = dd;
194
195 // update the network type
196 pNtk->ntkFunc = ABC_FUNC_BDD;
197 return 1;
198 }
199
200
201
202
203 /**Function*************************************************************
204
205 Synopsis [Converts the node from BDD to SOP representation.]
206
207 Description []
208
209 SideEffects []
210
211 SeeAlso []
212
213 ***********************************************************************/
Abc_ConvertBddToSop(Mem_Flex_t * pMan,DdManager * dd,DdNode * bFuncOn,DdNode * bFuncOnDc,int nFanins,int fAllPrimes,Vec_Str_t * vCube,int fMode)214 char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode )
215 {
216 int fVerify = 0;
217 char * pSop;
218 DdNode * bFuncNew, * bCover, * zCover, * zCover0, * zCover1;
219 int nCubes = 0, nCubes0, nCubes1, fPhase = 0;
220
221 assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) );
222 if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) )
223 {
224 if ( pMan )
225 pSop = Mem_FlexEntryFetch( pMan, nFanins + 4 );
226 else
227 pSop = ABC_ALLOC( char, nFanins + 4 );
228 pSop[0] = ' ';
229 pSop[1] = '0' + (int)(bFuncOn == Cudd_ReadOne(dd));
230 pSop[2] = '\n';
231 pSop[3] = '\0';
232 return pSop;
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_MAX_CUBES )
311 {
312 Cudd_RecursiveDerefZdd( dd, zCover );
313 printf( "The number of cubes exceeded the predefined limit (%d).\n", ABC_MAX_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 ***********************************************************************/
Abc_NtkBddToSop(Abc_Ntk_t * pNtk,int fMode,int nCubeLimit)359 int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit )
360 {
361 Vec_Int_t * vGuide;
362 Vec_Str_t * vCube;
363 Abc_Obj_t * pNode;
364 Mem_Flex_t * pManNew;
365 DdManager * dd = (DdManager *)pNtk->pManFunc;
366 DdNode * bFunc;
367 int i, nCubes;
368
369 // compute SOP size
370 vGuide = Vec_IntAlloc( Abc_NtkObjNumMax(pNtk) );
371 Vec_IntFill( vGuide, Abc_NtkObjNumMax(pNtk), fMode );
372 if ( nCubeLimit < ABC_INFINITY )
373 {
374 // collect all BDDs into one array
375 Vec_Ptr_t * vFuncs = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
376 assert( !Cudd_ReorderingStatus(dd, (Cudd_ReorderingType *)&nCubes) );
377 Abc_NtkForEachNode( pNtk, pNode, i )
378 if ( !Abc_ObjIsBarBuf(pNode) )
379 Vec_PtrWriteEntry( vFuncs, i, pNode->pData );
380 // compute the number of cubes in the ISOPs and detemine polarity
381 nCubes = Extra_bddCountCubes( dd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs), fMode, nCubeLimit, Vec_IntArray(vGuide) );
382 Vec_PtrFree( vFuncs );
383 if ( nCubes == -1 )
384 {
385 Vec_IntFree( vGuide );
386 return 0;
387 }
388 //printf( "The total number of cubes = %d.\n", nCubes );
389 }
390
391 assert( Abc_NtkHasBdd(pNtk) );
392 if ( dd->size > 0 )
393 Cudd_zddVarsFromBddVars( dd, 2 );
394 // create the new manager
395 pManNew = Mem_FlexStart();
396
397 // go through the objects
398 vCube = Vec_StrAlloc( 100 );
399 Abc_NtkForEachNode( pNtk, pNode, i )
400 {
401 if ( Abc_ObjIsBarBuf(pNode) )
402 continue;
403 assert( pNode->pData );
404 bFunc = (DdNode *)pNode->pData;
405 pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, Vec_IntEntry(vGuide, i) );
406 if ( pNode->pNext == NULL )
407 {
408 Mem_FlexStop( pManNew, 0 );
409 Abc_NtkCleanNext( pNtk );
410 // printf( "Converting from BDDs to SOPs has failed.\n" );
411 Vec_IntFree( vGuide );
412 Vec_StrFree( vCube );
413 return 0;
414 }
415 // it may happen that a constant node was created after structural mapping
416 if ( Abc_SopGetVarNum((char *)pNode->pNext) == 0 )
417 pNode->vFanins.nSize = 0;
418 // check the support
419 if ( Abc_ObjFaninNum(pNode) != Abc_SopGetVarNum((char *)pNode->pNext) )
420 {
421 printf( "Node %d with level %d has %d fanins but its SOP has support size %d.\n",
422 pNode->Id, pNode->Level, Abc_ObjFaninNum(pNode), Abc_SopGetVarNum((char *)pNode->pNext) );
423 fflush( stdout );
424 }
425 assert( Abc_ObjFaninNum(pNode) == Abc_SopGetVarNum((char *)pNode->pNext) );
426 }
427 Vec_IntFree( vGuide );
428 Vec_StrFree( vCube );
429
430 // update the network type
431 pNtk->ntkFunc = ABC_FUNC_SOP;
432 // set the new manager
433 pNtk->pManFunc = pManNew;
434 // transfer from next to data
435 Abc_NtkForEachNode( pNtk, pNode, i )
436 {
437 if ( Abc_ObjIsBarBuf(pNode) )
438 continue;
439 Cudd_RecursiveDeref( dd, (DdNode *)pNode->pData );
440 pNode->pData = pNode->pNext;
441 pNode->pNext = NULL;
442 }
443
444 // check for remaining references in the package
445 Extra_StopManager( dd );
446
447 // reorder fanins and cubes to make SOPs more human-readable
448 Abc_NtkSortSops( pNtk );
449 return 1;
450 }
451
452
453 /**Function*************************************************************
454
455 Synopsis [Derive the SOP from the ZDD representation of the cubes.]
456
457 Description []
458
459 SideEffects []
460
461 SeeAlso []
462
463 ***********************************************************************/
Abc_ConvertZddToSop_rec(DdManager * dd,DdNode * zCover,char * pSop,int nFanins,Vec_Str_t * vCube,int fPhase,int * pnCubes)464 void Abc_ConvertZddToSop_rec( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase, int * pnCubes )
465 {
466 DdNode * zC0, * zC1, * zC2;
467 int Index;
468
469 if ( zCover == dd->zero )
470 return;
471 if ( zCover == dd->one )
472 {
473 char * pCube;
474 pCube = pSop + (*pnCubes) * (nFanins + 3);
475 sprintf( pCube, "%s %d\n", vCube->pArray, fPhase );
476 (*pnCubes)++;
477 return;
478 }
479 Index = zCover->index/2;
480 assert( Index < nFanins );
481 extraDecomposeCover( dd, zCover, &zC0, &zC1, &zC2 );
482 vCube->pArray[Index] = '0';
483 Abc_ConvertZddToSop_rec( dd, zC0, pSop, nFanins, vCube, fPhase, pnCubes );
484 vCube->pArray[Index] = '1';
485 Abc_ConvertZddToSop_rec( dd, zC1, pSop, nFanins, vCube, fPhase, pnCubes );
486 vCube->pArray[Index] = '-';
487 Abc_ConvertZddToSop_rec( dd, zC2, pSop, nFanins, vCube, fPhase, pnCubes );
488 }
489
490 /**Function*************************************************************
491
492 Synopsis [Derive the BDD for the function in the cut.]
493
494 Description []
495
496 SideEffects []
497
498 SeeAlso []
499
500 ***********************************************************************/
Abc_ConvertZddToSop(DdManager * dd,DdNode * zCover,char * pSop,int nFanins,Vec_Str_t * vCube,int fPhase)501 int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase )
502 {
503 int nCubes = 0;
504 Abc_ConvertZddToSop_rec( dd, zCover, pSop, nFanins, vCube, fPhase, &nCubes );
505 return nCubes;
506 }
507
508
509 /**Function*************************************************************
510
511 Synopsis [Computes the SOPs of the negative and positive phase of the node.]
512
513 Description []
514
515 SideEffects []
516
517 SeeAlso []
518
519 ***********************************************************************/
Abc_NodeBddToCnf(Abc_Obj_t * pNode,Mem_Flex_t * pMmMan,Vec_Str_t * vCube,int fAllPrimes,char ** ppSop0,char ** ppSop1)520 void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Mem_Flex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 )
521 {
522 assert( Abc_NtkHasBdd(pNode->pNtk) );
523 *ppSop0 = Abc_ConvertBddToSop( pMmMan, (DdManager *)pNode->pNtk->pManFunc, (DdNode *)pNode->pData, (DdNode *)pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 0 );
524 *ppSop1 = Abc_ConvertBddToSop( pMmMan, (DdManager *)pNode->pNtk->pManFunc, (DdNode *)pNode->pData, (DdNode *)pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 1 );
525 }
526
527
528 /**Function*************************************************************
529
530 Synopsis [Removes complemented SOP covers.]
531
532 Description []
533
534 SideEffects []
535
536 SeeAlso []
537
538 ***********************************************************************/
Abc_NtkLogicMakeDirectSops(Abc_Ntk_t * pNtk)539 void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
540 {
541 DdManager * dd;
542 DdNode * bFunc;
543 Vec_Str_t * vCube;
544 Abc_Obj_t * pNode;
545 int nFaninsMax, fFound, i;
546
547 assert( Abc_NtkHasSop(pNtk) );
548
549 // check if there are nodes with complemented SOPs
550 fFound = 0;
551 Abc_NtkForEachNode( pNtk, pNode, i )
552 if ( !Abc_ObjIsBarBuf(pNode) && Abc_SopIsComplement((char *)pNode->pData) )
553 {
554 fFound = 1;
555 break;
556 }
557 if ( !fFound )
558 return;
559
560 // start the BDD package
561 nFaninsMax = Abc_NtkGetFaninMax( pNtk );
562 if ( nFaninsMax == 0 )
563 printf( "Warning: The network has only constant nodes.\n" );
564 dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
565
566 // change the cover of negated nodes
567 vCube = Vec_StrAlloc( 100 );
568 Abc_NtkForEachNode( pNtk, pNode, i )
569 if ( !Abc_ObjIsBarBuf(pNode) && Abc_SopIsComplement((char *)pNode->pData) )
570 {
571 bFunc = Abc_ConvertSopToBdd( dd, (char *)pNode->pData, NULL ); Cudd_Ref( bFunc );
572 pNode->pData = Abc_ConvertBddToSop( (Mem_Flex_t *)pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, 1 );
573 Cudd_RecursiveDeref( dd, bFunc );
574 assert( !Abc_SopIsComplement((char *)pNode->pData) );
575 }
576 Vec_StrFree( vCube );
577 Extra_StopManager( dd );
578 }
579
580
581
582
583 /**Function*************************************************************
584
585 Synopsis [Count the number of paths in the ZDD.]
586
587 Description []
588
589 SideEffects []
590
591 SeeAlso []
592
593 ***********************************************************************/
Abc_CountZddCubes_rec(DdManager * dd,DdNode * zCover,int * pnCubes)594 void Abc_CountZddCubes_rec( DdManager * dd, DdNode * zCover, int * pnCubes )
595 {
596 DdNode * zC0, * zC1, * zC2;
597 if ( zCover == dd->zero )
598 return;
599 if ( zCover == dd->one )
600 {
601 (*pnCubes)++;
602 return;
603 }
604 if ( (*pnCubes) > ABC_MAX_CUBES )
605 return;
606 extraDecomposeCover( dd, zCover, &zC0, &zC1, &zC2 );
607 Abc_CountZddCubes_rec( dd, zC0, pnCubes );
608 Abc_CountZddCubes_rec( dd, zC1, pnCubes );
609 Abc_CountZddCubes_rec( dd, zC2, pnCubes );
610 }
611
612 /**Function*************************************************************
613
614 Synopsis [Count the number of paths in the ZDD.]
615
616 Description []
617
618 SideEffects []
619
620 SeeAlso []
621
622 ***********************************************************************/
Abc_CountZddCubes(DdManager * dd,DdNode * zCover)623 int Abc_CountZddCubes( DdManager * dd, DdNode * zCover )
624 {
625 int nCubes = 0;
626 Abc_CountZddCubes_rec( dd, zCover, &nCubes );
627 return nCubes;
628 }
629
630 /**Function*************************************************************
631
632 Synopsis [Converts the network from AIG to BDD representation.]
633
634 Description []
635
636 SideEffects []
637
638 SeeAlso []
639
640 ***********************************************************************/
Abc_NtkAigToBdd(Abc_Ntk_t * pNtk)641 int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk )
642 {
643 Abc_Obj_t * pNode;
644 Hop_Man_t * pMan;
645 DdNode * pFunc;
646 DdManager * dd, * ddTemp = NULL;
647 Vec_Int_t * vFanins = NULL;
648 int nFaninsMax, i, k, iVar;
649
650 assert( Abc_NtkHasAig(pNtk) );
651
652 // start the functionality manager
653 nFaninsMax = Abc_NtkGetFaninMax( pNtk );
654 if ( nFaninsMax == 0 )
655 printf( "Warning: The network has only constant nodes.\n" );
656
657 dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
658
659 // start temporary manager for reordered local functions
660 ddTemp = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
661 Cudd_AutodynEnable( ddTemp, CUDD_REORDER_SYMM_SIFT );
662 vFanins = Vec_IntAlloc( nFaninsMax );
663
664 // set the mapping of elementary AIG nodes into the elementary BDD nodes
665 pMan = (Hop_Man_t *)pNtk->pManFunc;
666 assert( Hop_ManPiNum(pMan) >= nFaninsMax );
667 for ( i = 0; i < nFaninsMax; i++ )
668 Hop_ManPi(pMan, i)->pData = Cudd_bddIthVar(ddTemp, i);
669
670 // convert each node from SOP to BDD
671 Abc_NtkForEachNode( pNtk, pNode, i )
672 {
673 if ( Abc_ObjIsBarBuf(pNode) )
674 continue;
675 pFunc = Abc_ConvertAigToBdd( ddTemp, (Hop_Obj_t *)pNode->pData );
676 if ( pFunc == NULL )
677 {
678 printf( "Abc_NtkAigToBdd: Error while converting AIG into BDD.\n" );
679 return 0;
680 }
681 Cudd_Ref( pFunc );
682 // find variable mapping
683 Vec_IntFill( vFanins, Abc_ObjFaninNum(pNode), -1 );
684 for ( k = iVar = 0; k < nFaninsMax; k++ )
685 if ( ddTemp->invperm[k] < Abc_ObjFaninNum(pNode) )
686 Vec_IntWriteEntry( vFanins, ddTemp->invperm[k], iVar++ );
687 assert( iVar == Abc_ObjFaninNum(pNode) );
688 // transfer to the main manager
689 pNode->pData = Extra_TransferPermute( ddTemp, dd, pFunc, Vec_IntArray(vFanins) );
690 Cudd_Ref( (DdNode *)pNode->pData );
691 Cudd_RecursiveDeref( ddTemp, pFunc );
692 // update variable order
693 Vec_IntClear( vFanins );
694 for ( k = 0; k < nFaninsMax; k++ )
695 if ( ddTemp->invperm[k] < Abc_ObjFaninNum(pNode) )
696 Vec_IntPush( vFanins, Vec_IntEntry(&pNode->vFanins, ddTemp->invperm[k]) );
697 for ( k = 0; k < Abc_ObjFaninNum(pNode); k++ )
698 Vec_IntWriteEntry( &pNode->vFanins, k, Vec_IntEntry(vFanins, k) );
699 }
700
701 // printf( "Reorderings performed = %d.\n", Cudd_ReadReorderings(ddTemp) );
702 Extra_StopManager( ddTemp );
703 Vec_IntFreeP( &vFanins );
704 Hop_ManStop( (Hop_Man_t *)pNtk->pManFunc );
705 pNtk->pManFunc = dd;
706
707 // update the network type
708 pNtk->ntkFunc = ABC_FUNC_BDD;
709 return 1;
710 }
711
712 /**Function*************************************************************
713
714 Synopsis [Construct BDDs and mark AIG nodes.]
715
716 Description []
717
718 SideEffects []
719
720 SeeAlso []
721
722 ***********************************************************************/
Abc_ConvertAigToBdd_rec1(DdManager * dd,Hop_Obj_t * pObj)723 void Abc_ConvertAigToBdd_rec1( DdManager * dd, Hop_Obj_t * pObj )
724 {
725 assert( !Hop_IsComplement(pObj) );
726 if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
727 return;
728 Abc_ConvertAigToBdd_rec1( dd, Hop_ObjFanin0(pObj) );
729 Abc_ConvertAigToBdd_rec1( dd, Hop_ObjFanin1(pObj) );
730 pObj->pData = Cudd_bddAnd( dd, (DdNode *)Hop_ObjChild0Copy(pObj), (DdNode *)Hop_ObjChild1Copy(pObj) );
731 Cudd_Ref( (DdNode *)pObj->pData );
732 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
733 Hop_ObjSetMarkA( pObj );
734 }
735
736 /**Function*************************************************************
737
738 Synopsis [Dereference BDDs and unmark AIG nodes.]
739
740 Description []
741
742 SideEffects []
743
744 SeeAlso []
745
746 ***********************************************************************/
Abc_ConvertAigToBdd_rec2(DdManager * dd,Hop_Obj_t * pObj)747 void Abc_ConvertAigToBdd_rec2( DdManager * dd, Hop_Obj_t * pObj )
748 {
749 assert( !Hop_IsComplement(pObj) );
750 if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
751 return;
752 Abc_ConvertAigToBdd_rec2( dd, Hop_ObjFanin0(pObj) );
753 Abc_ConvertAigToBdd_rec2( dd, Hop_ObjFanin1(pObj) );
754 Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
755 pObj->pData = NULL;
756 assert( Hop_ObjIsMarkA(pObj) ); // loop detection
757 Hop_ObjClearMarkA( pObj );
758 }
759
760 /**Function*************************************************************
761
762 Synopsis [Converts the network from AIG to BDD representation.]
763
764 Description []
765
766 SideEffects []
767
768 SeeAlso []
769
770 ***********************************************************************/
Abc_ConvertAigToBdd(DdManager * dd,Hop_Obj_t * pRoot)771 DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot )
772 {
773 DdNode * bFunc;
774 // check the case of a constant
775 if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
776 return Cudd_NotCond( Cudd_ReadOne(dd), Hop_IsComplement(pRoot) );
777 // construct BDD
778 Abc_ConvertAigToBdd_rec1( dd, Hop_Regular(pRoot) );
779 // hold on to the result
780 bFunc = Cudd_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) ); Cudd_Ref( bFunc );
781 // dereference BDD
782 Abc_ConvertAigToBdd_rec2( dd, Hop_Regular(pRoot) );
783 // return the result
784 Cudd_Deref( bFunc );
785 return bFunc;
786 }
787
788 #else
789
Abc_NtkSopToBdd(Abc_Ntk_t * pNtk)790 int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk ) { return 1; }
Abc_NtkBddToSop(Abc_Ntk_t * pNtk,int fMode,int nCubeLimit)791 int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit ) { return 1; }
Abc_NodeBddToCnf(Abc_Obj_t * pNode,Mem_Flex_t * pMmMan,Vec_Str_t * vCube,int fAllPrimes,char ** ppSop0,char ** ppSop1)792 void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Mem_Flex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 ) {}
Abc_NtkLogicMakeDirectSops(Abc_Ntk_t * pNtk)793 void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ) {}
Abc_NtkAigToBdd(Abc_Ntk_t * pNtk)794 int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk ) { return 1; }
795
796 #endif
797
798 /**Function*************************************************************
799
800 Synopsis [Converts the network from SOP to AIG representation.]
801
802 Description []
803
804 SideEffects []
805
806 SeeAlso []
807
808 ***********************************************************************/
Abc_NtkSopToAig(Abc_Ntk_t * pNtk)809 int Abc_NtkSopToAig( Abc_Ntk_t * pNtk )
810 {
811 Abc_Obj_t * pNode;
812 Hop_Man_t * pMan;
813 int i, Max;
814
815 assert( Abc_NtkHasSop(pNtk) );
816
817 // make dist1-free and SCC-free
818 // Abc_NtkMakeLegit( pNtk );
819
820 // start the functionality manager
821 pMan = Hop_ManStart();
822 Max = Abc_NtkGetFaninMax(pNtk);
823 if ( Max ) Hop_IthVar( pMan, Max-1 );
824
825 // convert each node from SOP to BDD
826 Abc_NtkForEachNode( pNtk, pNode, i )
827 {
828 if ( Abc_ObjIsBarBuf(pNode) )
829 continue;
830 assert( pNode->pData );
831 pNode->pData = Abc_ConvertSopToAig( pMan, (char *)pNode->pData );
832 if ( pNode->pData == NULL )
833 {
834 Hop_ManStop( pMan );
835 printf( "Abc_NtkSopToAig: Error while converting SOP into AIG.\n" );
836 return 0;
837 }
838 }
839 Mem_FlexStop( (Mem_Flex_t *)pNtk->pManFunc, 0 );
840 pNtk->pManFunc = pMan;
841
842 // update the network type
843 pNtk->ntkFunc = ABC_FUNC_AIG;
844 return 1;
845 }
846
847
848 /**Function*************************************************************
849
850 Synopsis [Strashes one logic node using its SOP.]
851
852 Description []
853
854 SideEffects []
855
856 SeeAlso []
857
858 ***********************************************************************/
Abc_ConvertSopToAigInternal(Hop_Man_t * pMan,char * pSop)859 Hop_Obj_t * Abc_ConvertSopToAigInternal( Hop_Man_t * pMan, char * pSop )
860 {
861 Hop_Obj_t * pAnd, * pSum;
862 int i, Value, nFanins;
863 char * pCube;
864 // get the number of variables
865 nFanins = Abc_SopGetVarNum(pSop);
866 if ( Abc_SopIsExorType(pSop) )
867 {
868 pSum = Hop_ManConst0(pMan);
869 for ( i = 0; i < nFanins; i++ )
870 pSum = Hop_Exor( pMan, pSum, Hop_IthVar(pMan,i) );
871 }
872 else
873 {
874 // go through the cubes of the node's SOP
875 pSum = Hop_ManConst0(pMan);
876 Abc_SopForEachCube( pSop, nFanins, pCube )
877 {
878 // create the AND of literals
879 pAnd = Hop_ManConst1(pMan);
880 Abc_CubeForEachVar( pCube, Value, i )
881 {
882 if ( Value == '1' )
883 pAnd = Hop_And( pMan, pAnd, Hop_IthVar(pMan,i) );
884 else if ( Value == '0' )
885 pAnd = Hop_And( pMan, pAnd, Hop_Not(Hop_IthVar(pMan,i)) );
886 }
887 // add to the sum of cubes
888 pSum = Hop_Or( pMan, pSum, pAnd );
889 }
890 }
891 // decide whether to complement the result
892 if ( Abc_SopIsComplement(pSop) )
893 pSum = Hop_Not(pSum);
894 return pSum;
895 }
896
897 /**Function*************************************************************
898
899 Synopsis [Converts the network from AIG to BDD representation.]
900
901 Description []
902
903 SideEffects []
904
905 SeeAlso []
906
907 ***********************************************************************/
Abc_ConvertSopToAig(Hop_Man_t * pMan,char * pSop)908 Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop )
909 {
910 extern Hop_Obj_t * Dec_GraphFactorSop( Hop_Man_t * pMan, char * pSop );
911 int fUseFactor = 1;
912 // consider the constant node
913 if ( Abc_SopGetVarNum(pSop) == 0 )
914 return Hop_NotCond( Hop_ManConst1(pMan), Abc_SopIsConst0(pSop) );
915 // decide when to use factoring
916 if ( fUseFactor && Abc_SopGetVarNum(pSop) > 2 && Abc_SopGetCubeNum(pSop) > 1 && !Abc_SopIsExorType(pSop) )
917 return Dec_GraphFactorSop( pMan, pSop );
918 return Abc_ConvertSopToAigInternal( pMan, pSop );
919 }
920
921
922 /**Function*************************************************************
923
924 Synopsis [Converts the network from AIG to GIA representation.]
925
926 Description []
927
928 SideEffects []
929
930 SeeAlso []
931
932 ***********************************************************************/
Abc_ConvertAigToGia_rec1(Gia_Man_t * p,Hop_Obj_t * pObj)933 void Abc_ConvertAigToGia_rec1( Gia_Man_t * p, Hop_Obj_t * pObj )
934 {
935 assert( !Hop_IsComplement(pObj) );
936 if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
937 return;
938 Abc_ConvertAigToGia_rec1( p, Hop_ObjFanin0(pObj) );
939 Abc_ConvertAigToGia_rec1( p, Hop_ObjFanin1(pObj) );
940 pObj->iData = Gia_ManAppendAnd2( p, Hop_ObjChild0CopyI(pObj), Hop_ObjChild1CopyI(pObj) );
941 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
942 Hop_ObjSetMarkA( pObj );
943 }
Abc_ConvertAigToGia_rec2(Hop_Obj_t * pObj)944 void Abc_ConvertAigToGia_rec2( Hop_Obj_t * pObj )
945 {
946 assert( !Hop_IsComplement(pObj) );
947 if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
948 return;
949 Abc_ConvertAigToGia_rec2( Hop_ObjFanin0(pObj) );
950 Abc_ConvertAigToGia_rec2( Hop_ObjFanin1(pObj) );
951 assert( Hop_ObjIsMarkA(pObj) ); // loop detection
952 Hop_ObjClearMarkA( pObj );
953 }
Abc_ConvertAigToGia(Gia_Man_t * p,Hop_Obj_t * pRoot)954 int Abc_ConvertAigToGia( Gia_Man_t * p, Hop_Obj_t * pRoot )
955 {
956 assert( !Hop_IsComplement(pRoot) );
957 if ( Hop_ObjIsConst1( pRoot ) )
958 return 1;
959 Abc_ConvertAigToGia_rec1( p, pRoot );
960 Abc_ConvertAigToGia_rec2( pRoot );
961 return pRoot->iData;
962 }
963
964 /**Function*************************************************************
965
966 Synopsis [Converts the network from AIG to BDD representation.]
967
968 Description []
969
970 SideEffects []
971
972 SeeAlso []
973
974 ***********************************************************************/
Abc_NtkAigToGia(Abc_Ntk_t * p,int fGiaSimple)975 Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p, int fGiaSimple )
976 {
977 Gia_Man_t * pNew;
978 Hop_Man_t * pHopMan;
979 Hop_Obj_t * pHopObj;
980 Vec_Int_t * vMapping = NULL;
981 Vec_Ptr_t * vNodes;
982 Abc_Obj_t * pNode, * pFanin;
983 int i, k, nObjs, iGiaObj;
984 assert( Abc_NtkIsAigLogic(p) );
985 pHopMan = (Hop_Man_t *)p->pManFunc;
986 // create new manager
987 pNew = Gia_ManStart( 10000 );
988 pNew->pName = Abc_UtilStrsav( Abc_NtkName(p) );
989 pNew->pSpec = Abc_UtilStrsav( Abc_NtkSpec(p) );
990 pNew->fGiaSimple = fGiaSimple;
991 Abc_NtkCleanCopy( p );
992 Hop_ManConst1(pHopMan)->iData = 1;
993 // create primary inputs
994 Abc_NtkForEachCi( p, pNode, i )
995 pNode->iTemp = Gia_ManAppendCi(pNew);
996 // find the number of objects
997 nObjs = 1 + Abc_NtkCiNum(p) + Abc_NtkCoNum(p);
998 Abc_NtkForEachNode( p, pNode, i )
999 nObjs += Abc_ObjIsBarBuf(pNode) ? 1 : Hop_DagSize( (Hop_Obj_t *)pNode->pData );
1000 if ( !fGiaSimple )
1001 vMapping = Vec_IntStart( nObjs );
1002 // iterate through nodes used in the mapping
1003 vNodes = Abc_NtkDfs( p, 0 );
1004 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
1005 {
1006 if ( Abc_ObjIsBarBuf(pNode) )
1007 {
1008 assert( !Abc_ObjFaninC0(pNode) );
1009 pNode->iTemp = Gia_ManAppendBuf( pNew, Abc_ObjFanin0(pNode)->iTemp );
1010 continue;
1011 }
1012 Abc_ObjForEachFanin( pNode, pFanin, k )
1013 Hop_ManPi(pHopMan, k)->iData = pFanin->iTemp;
1014 pHopObj = Hop_Regular( (Hop_Obj_t *)pNode->pData );
1015 if ( Hop_DagSize(pHopObj) > 0 )
1016 {
1017 assert( Abc_ObjFaninNum(pNode) <= Hop_ManPiNum(pHopMan) );
1018 Abc_ConvertAigToGia( pNew, pHopObj );
1019 iGiaObj = Abc_Lit2Var( pHopObj->iData );
1020 if ( vMapping && Gia_ObjIsAnd(Gia_ManObj(pNew, iGiaObj)) && !Vec_IntEntry(vMapping, iGiaObj) )
1021 {
1022 Vec_IntWriteEntry( vMapping, iGiaObj, Vec_IntSize(vMapping) );
1023 Vec_IntPush( vMapping, Abc_ObjFaninNum(pNode) );
1024 Abc_ObjForEachFanin( pNode, pFanin, k )
1025 Vec_IntPush( vMapping, Abc_Lit2Var(pFanin->iTemp) );
1026 Vec_IntPush( vMapping, iGiaObj );
1027 }
1028 }
1029 pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) );
1030 }
1031 // create primary outputs
1032 Abc_NtkForEachCo( p, pNode, i )
1033 Gia_ManAppendCo( pNew, Abc_ObjFanin0(pNode)->iTemp );
1034 Gia_ManSetRegNum( pNew, Abc_NtkLatchNum(p) );
1035 // copy original IDs
1036 pNew->vIdsOrig = Vec_IntStart( Gia_ManObjNum(pNew) );
1037 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
1038 Vec_IntWriteEntry( pNew->vIdsOrig, Abc_Lit2Var(pNode->iTemp), Abc_ObjId(pNode) );
1039 Vec_PtrFree( vNodes );
1040 // finish mapping
1041 assert( Gia_ManObjNum(pNew) <= nObjs );
1042 assert( pNew->vMapping == NULL );
1043 pNew->vMapping = vMapping;
1044 return pNew;
1045 }
1046
1047
1048 /**Function*************************************************************
1049
1050 Synopsis [Construct BDDs and mark AIG nodes.]
1051
1052 Description []
1053
1054 SideEffects []
1055
1056 SeeAlso []
1057
1058 ***********************************************************************/
Abc_ConvertAigToAig_rec(Abc_Ntk_t * pNtkAig,Hop_Obj_t * pObj)1059 void Abc_ConvertAigToAig_rec( Abc_Ntk_t * pNtkAig, Hop_Obj_t * pObj )
1060 {
1061 assert( !Hop_IsComplement(pObj) );
1062 if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
1063 return;
1064 Abc_ConvertAigToAig_rec( pNtkAig, Hop_ObjFanin0(pObj) );
1065 Abc_ConvertAigToAig_rec( pNtkAig, Hop_ObjFanin1(pObj) );
1066 pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkAig->pManFunc, (Abc_Obj_t *)Hop_ObjChild0Copy(pObj), (Abc_Obj_t *)Hop_ObjChild1Copy(pObj) );
1067 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
1068 Hop_ObjSetMarkA( pObj );
1069 }
1070
1071 /**Function*************************************************************
1072
1073 Synopsis [Converts the network from AIG to BDD representation.]
1074
1075 Description []
1076
1077 SideEffects []
1078
1079 SeeAlso []
1080
1081 ***********************************************************************/
Abc_ConvertAigToAig(Abc_Ntk_t * pNtkAig,Abc_Obj_t * pObjOld)1082 Abc_Obj_t * Abc_ConvertAigToAig( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pObjOld )
1083 {
1084 Hop_Man_t * pHopMan;
1085 Hop_Obj_t * pRoot;
1086 Abc_Obj_t * pFanin;
1087 int i;
1088 // get the local AIG
1089 pHopMan = (Hop_Man_t *)pObjOld->pNtk->pManFunc;
1090 pRoot = (Hop_Obj_t *)pObjOld->pData;
1091 // check the case of a constant
1092 if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
1093 return Abc_ObjNotCond( Abc_AigConst1(pNtkAig), Hop_IsComplement(pRoot) );
1094 // assign the fanin nodes
1095 Abc_ObjForEachFanin( pObjOld, pFanin, i )
1096 {
1097 assert( pFanin->pCopy != NULL );
1098 Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
1099 }
1100 // construct the AIG
1101 Abc_ConvertAigToAig_rec( pNtkAig, Hop_Regular(pRoot) );
1102 Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
1103 // return the result
1104 return Abc_ObjNotCond( (Abc_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
1105 }
1106
1107
1108 /**Function*************************************************************
1109
1110 Synopsis [Unmaps the network.]
1111
1112 Description []
1113
1114 SideEffects []
1115
1116 SeeAlso []
1117
1118 ***********************************************************************/
Abc_NtkMapToSop(Abc_Ntk_t * pNtk)1119 int Abc_NtkMapToSop( Abc_Ntk_t * pNtk )
1120 {
1121 extern void * Abc_FrameReadLibGen();
1122 Abc_Obj_t * pNode;
1123 char * pSop;
1124 int i;
1125
1126 assert( Abc_NtkHasMapping(pNtk) );
1127 // update the functionality manager
1128 assert( pNtk->pManFunc == Abc_FrameReadLibGen() );
1129 pNtk->pManFunc = Mem_FlexStart();
1130 // update the nodes
1131 Abc_NtkForEachNode( pNtk, pNode, i )
1132 {
1133 if ( Abc_ObjIsBarBuf(pNode) )
1134 continue;
1135 pSop = Mio_GateReadSop((Mio_Gate_t *)pNode->pData);
1136 assert( Abc_SopGetVarNum(pSop) == Abc_ObjFaninNum(pNode) );
1137 pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, pSop );
1138 }
1139 pNtk->ntkFunc = ABC_FUNC_SOP;
1140 return 1;
1141 }
1142
1143 /**Function*************************************************************
1144
1145 Synopsis [Converts SOP functions into BLIF-MV functions.]
1146
1147 Description []
1148
1149 SideEffects []
1150
1151 SeeAlso []
1152
1153 ***********************************************************************/
Abc_NtkSopToBlifMv(Abc_Ntk_t * pNtk)1154 int Abc_NtkSopToBlifMv( Abc_Ntk_t * pNtk )
1155 {
1156 return 1;
1157 }
1158
1159 /**Function*************************************************************
1160
1161 Synopsis [Convers logic network to the SOP form.]
1162
1163 Description []
1164
1165 SideEffects []
1166
1167 SeeAlso []
1168
1169 ***********************************************************************/
Abc_NtkToSop(Abc_Ntk_t * pNtk,int fMode,int nCubeLimit)1170 int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit )
1171 {
1172 assert( !Abc_NtkIsStrash(pNtk) );
1173 if ( Abc_NtkHasBlackbox(pNtk) )
1174 return 1;
1175 if ( Abc_NtkHasSop(pNtk) )
1176 {
1177 if ( fMode == -1 )
1178 return 1;
1179 if ( !Abc_NtkSopToBdd(pNtk) )
1180 return 0;
1181 return Abc_NtkBddToSop(pNtk, fMode, nCubeLimit);
1182 }
1183 if ( Abc_NtkHasMapping(pNtk) )
1184 return Abc_NtkMapToSop(pNtk);
1185 if ( Abc_NtkHasBdd(pNtk) )
1186 return Abc_NtkBddToSop(pNtk, fMode, nCubeLimit);
1187 if ( Abc_NtkHasAig(pNtk) )
1188 {
1189 if ( !Abc_NtkAigToBdd(pNtk) )
1190 return 0;
1191 return Abc_NtkBddToSop(pNtk, fMode, nCubeLimit);
1192 }
1193 assert( 0 );
1194 return 0;
1195 }
1196
1197 /**Function*************************************************************
1198
1199 Synopsis [Convers logic network to the SOP form.]
1200
1201 Description []
1202
1203 SideEffects []
1204
1205 SeeAlso []
1206
1207 ***********************************************************************/
Abc_NtkToBdd(Abc_Ntk_t * pNtk)1208 int Abc_NtkToBdd( Abc_Ntk_t * pNtk )
1209 {
1210 assert( !Abc_NtkIsStrash(pNtk) );
1211 if ( Abc_NtkHasBlackbox(pNtk) )
1212 return 1;
1213 if ( Abc_NtkHasBdd(pNtk) )
1214 return 1;
1215 if ( Abc_NtkHasMapping(pNtk) )
1216 {
1217 Abc_NtkMapToSop(pNtk);
1218 return Abc_NtkSopToBdd(pNtk);
1219 }
1220 if ( Abc_NtkHasSop(pNtk) )
1221 {
1222 Abc_NtkSopToAig(pNtk);
1223 return Abc_NtkAigToBdd(pNtk);
1224 }
1225 if ( Abc_NtkHasAig(pNtk) )
1226 return Abc_NtkAigToBdd(pNtk);
1227 assert( 0 );
1228 return 0;
1229 }
1230
1231 /**Function*************************************************************
1232
1233 Synopsis [Convers logic network to the SOP form.]
1234
1235 Description []
1236
1237 SideEffects []
1238
1239 SeeAlso []
1240
1241 ***********************************************************************/
Abc_NtkToAig(Abc_Ntk_t * pNtk)1242 int Abc_NtkToAig( Abc_Ntk_t * pNtk )
1243 {
1244 assert( !Abc_NtkIsStrash(pNtk) );
1245 if ( Abc_NtkHasBlackbox(pNtk) )
1246 return 1;
1247 if ( Abc_NtkHasAig(pNtk) )
1248 return 1;
1249 if ( Abc_NtkHasMapping(pNtk) )
1250 {
1251 Abc_NtkMapToSop(pNtk);
1252 return Abc_NtkSopToAig(pNtk);
1253 }
1254 if ( Abc_NtkHasBdd(pNtk) )
1255 {
1256 if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) )
1257 return 0;
1258 return Abc_NtkSopToAig(pNtk);
1259 }
1260 if ( Abc_NtkHasSop(pNtk) )
1261 return Abc_NtkSopToAig(pNtk);
1262 assert( 0 );
1263 return 0;
1264 }
1265
1266
1267 ////////////////////////////////////////////////////////////////////////
1268 /// END OF FILE ///
1269 ////////////////////////////////////////////////////////////////////////
1270
1271
1272 ABC_NAMESPACE_IMPL_END
1273
1274