1 /**CFile****************************************************************
2
3 FileName [abcBlifMv.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [Procedures to process BLIF-MV networks and AIGs.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: abcBlifMv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "abc.h"
22
23 #ifdef ABC_USE_CUDD
24 #include "bdd/extrab/extraBdd.h"
25 #endif
26
27 ABC_NAMESPACE_IMPL_START
28
29
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 ////////////////////////////////////////////////////////////////////////
35 /// FUNCTION DEFINITIONS ///
36 ////////////////////////////////////////////////////////////////////////
37
38 /**Function*************************************************************
39
40 Synopsis [Starts the Mv-Var manager.]
41
42 Description []
43
44 SideEffects []
45
46 SeeAlso []
47
48 ***********************************************************************/
Abc_NtkStartMvVars(Abc_Ntk_t * pNtk)49 void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk )
50 {
51 Vec_Att_t * pAttMan;
52 assert( Abc_NtkMvVar(pNtk) == NULL );
53 pAttMan = Vec_AttAlloc( Abc_NtkObjNumMax(pNtk) + 1, Mem_FlexStart(), (void(*)(void*))Mem_FlexStop, NULL, NULL );
54 Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_MVVAR, pAttMan );
55 //printf( "allocing attr\n" );
56 }
57
58 /**Function*************************************************************
59
60 Synopsis [Stops the Mv-Var manager.]
61
62 Description []
63
64 SideEffects []
65
66 SeeAlso []
67
68 ***********************************************************************/
Abc_NtkFreeMvVars(Abc_Ntk_t * pNtk)69 void Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk )
70 {
71 Mem_Flex_t * pUserMan;
72 pUserMan = (Mem_Flex_t *)Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, 0 );
73 Mem_FlexStop( pUserMan, 0 );
74 }
75
76 /**Function*************************************************************
77
78 Synopsis [Duplicate the MV variable.]
79
80 Description []
81
82 SideEffects []
83
84 SeeAlso []
85
86 ***********************************************************************/
Abc_NtkSetMvVarValues(Abc_Obj_t * pObj,int nValues)87 void Abc_NtkSetMvVarValues( Abc_Obj_t * pObj, int nValues )
88 {
89 Mem_Flex_t * pFlex;
90 struct temp
91 {
92 int nValues;
93 char ** pNames;
94 } * pVarStruct;
95 assert( nValues > 1 );
96 // skip binary signals
97 if ( nValues == 2 )
98 return;
99 // skip already assigned signals
100 if ( Abc_ObjMvVar(pObj) != NULL )
101 return;
102 // create the structure
103 pFlex = (Mem_Flex_t *)Abc_NtkMvVarMan( pObj->pNtk );
104 pVarStruct = (struct temp *)Mem_FlexEntryFetch( pFlex, sizeof(struct temp) );
105 pVarStruct->nValues = nValues;
106 pVarStruct->pNames = NULL;
107 Abc_ObjSetMvVar( pObj, pVarStruct );
108 }
109
110 /**Function*************************************************************
111
112 Synopsis [Strashes the BLIF-MV netlist.]
113
114 Description []
115
116 SideEffects []
117
118 SeeAlso []
119
120 ***********************************************************************/
Abc_StringGetNumber(char ** ppStr)121 static inline int Abc_StringGetNumber( char ** ppStr )
122 {
123 char * pStr = *ppStr;
124 int Number = 0;
125 assert( *pStr >= '0' && *pStr <= '9' );
126 for ( ; *pStr >= '0' && *pStr <= '9'; pStr++ )
127 Number = 10 * Number + *pStr - '0';
128 *ppStr = pStr;
129 return Number;
130 }
131
132 /**Function*************************************************************
133
134 Synopsis [Strashes one node in the BLIF-MV netlist.]
135
136 Description []
137
138 SideEffects []
139
140 SeeAlso []
141
142 ***********************************************************************/
Abc_NodeStrashBlifMv(Abc_Ntk_t * pNtkNew,Abc_Obj_t * pObj)143 int Abc_NodeStrashBlifMv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
144 {
145 int fAddFreeVars = 1;
146 char * pSop;
147 Abc_Obj_t ** pValues, ** pValuesF, ** pValuesF2;
148 Abc_Obj_t * pTemp, * pTemp2, * pFanin, * pFanin2, * pNet;
149 int k, v, Def, DefIndex, Index, nValues, nValuesF, nValuesF2;
150
151 // start the output values
152 assert( Abc_ObjIsNode(pObj) );
153 pNet = Abc_ObjFanout0(pObj);
154 nValues = Abc_ObjMvVarNum(pNet);
155 pValues = ABC_ALLOC( Abc_Obj_t *, nValues );
156 for ( k = 0; k < nValues; k++ )
157 pValues[k] = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
158
159 // get the BLIF-MV formula
160 pSop = (char *)pObj->pData;
161 // skip the value line
162 // while ( *pSop++ != '\n' );
163
164 // handle the constant
165 if ( Abc_ObjFaninNum(pObj) == 0 )
166 {
167 // skip the default if present
168 if ( *pSop == 'd' )
169 while ( *pSop++ != '\n' );
170 // skip space if present
171 if ( *pSop == ' ' )
172 pSop++;
173 // assume don't-care constant to be zero
174 if ( *pSop == '-' )
175 Index = 0;
176 else
177 Index = Abc_StringGetNumber( &pSop );
178 assert( Index < nValues );
179 ////////////////////////////////////////////
180 // adding free variables for binary ND-constants
181 if ( fAddFreeVars && nValues == 2 && *pSop == '-' )
182 {
183 pValues[1] = Abc_NtkCreatePi(pNtkNew);
184 pValues[0] = Abc_ObjNot( pValues[1] );
185 Abc_ObjAssignName( pValues[1], "free_var_", Abc_ObjName(pValues[1]) );
186 }
187 else
188 pValues[Index] = Abc_AigConst1(pNtkNew);
189 ////////////////////////////////////////////
190 // save the values in the fanout net
191 pNet->pCopy = (Abc_Obj_t *)pValues;
192 return 1;
193 }
194
195 // parse the default line
196 Def = DefIndex = -1;
197 if ( *pSop == 'd' )
198 {
199 pSop++;
200 if ( *pSop == '=' )
201 {
202 pSop++;
203 DefIndex = Abc_StringGetNumber( &pSop );
204 assert( DefIndex < Abc_ObjFaninNum(pObj) );
205 }
206 else if ( *pSop == '-' )
207 {
208 pSop++;
209 Def = 0;
210 }
211 else
212 {
213 Def = Abc_StringGetNumber( &pSop );
214 assert( Def < nValues );
215 }
216 assert( *pSop == '\n' );
217 pSop++;
218 }
219
220 // convert the values
221 while ( *pSop )
222 {
223 // extract the values for each cube
224 pTemp = Abc_AigConst1(pNtkNew);
225 Abc_ObjForEachFanin( pObj, pFanin, k )
226 {
227 if ( *pSop == '-' )
228 {
229 pSop += 2;
230 continue;
231 }
232 if ( *pSop == '!' )
233 {
234 ABC_FREE( pValues );
235 printf( "Abc_NodeStrashBlifMv(): Cannot handle complement in the MV function of node %s.\n", Abc_ObjName(Abc_ObjFanout0(pObj)) );
236 return 0;
237 }
238 if ( *pSop == '{' )
239 {
240 ABC_FREE( pValues );
241 printf( "Abc_NodeStrashBlifMv(): Cannot handle braces in the MV function of node %s.\n", Abc_ObjName(Abc_ObjFanout0(pObj)) );
242 return 0;
243 }
244 // get the value set
245 nValuesF = Abc_ObjMvVarNum(pFanin);
246 pValuesF = (Abc_Obj_t **)pFanin->pCopy;
247 if ( *pSop == '(' )
248 {
249 pSop++;
250 pTemp2 = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
251 while ( *pSop != ')' )
252 {
253 Index = Abc_StringGetNumber( &pSop );
254 assert( Index < nValuesF );
255 pTemp2 = Abc_AigOr( (Abc_Aig_t *)pNtkNew->pManFunc, pTemp2, pValuesF[Index] );
256 assert( *pSop == ')' || *pSop == ',' );
257 if ( *pSop == ',' )
258 pSop++;
259 }
260 assert( *pSop == ')' );
261 pSop++;
262 }
263 else if ( *pSop == '=' )
264 {
265 pSop++;
266 // get the fanin index
267 Index = Abc_StringGetNumber( &pSop );
268 assert( Index < Abc_ObjFaninNum(pObj) );
269 assert( Index != k );
270 // get the fanin
271 pFanin2 = Abc_ObjFanin( pObj, Index );
272 nValuesF2 = Abc_ObjMvVarNum(pFanin2);
273 pValuesF2 = (Abc_Obj_t **)pFanin2->pCopy;
274 // create the sum of products of values
275 assert( nValuesF == nValuesF2 );
276 pTemp2 = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
277 for ( v = 0; v < nValues; v++ )
278 pTemp2 = Abc_AigOr( (Abc_Aig_t *)pNtkNew->pManFunc, pTemp2, Abc_AigAnd((Abc_Aig_t *)pNtkNew->pManFunc, pValuesF[v], pValuesF2[v]) );
279 }
280 else
281 {
282 Index = Abc_StringGetNumber( &pSop );
283 assert( Index < nValuesF );
284 pTemp2 = pValuesF[Index];
285 }
286 // compute the compute
287 pTemp = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, pTemp, pTemp2 );
288 // advance the reading point
289 assert( *pSop == ' ' );
290 pSop++;
291 }
292 // check if the output value is an equal construct
293 if ( *pSop == '=' )
294 {
295 pSop++;
296 // get the output value
297 Index = Abc_StringGetNumber( &pSop );
298 assert( Index < Abc_ObjFaninNum(pObj) );
299 // add values of the given fanin with the given cube
300 pFanin = Abc_ObjFanin( pObj, Index );
301 nValuesF = Abc_ObjMvVarNum(pFanin);
302 pValuesF = (Abc_Obj_t **)pFanin->pCopy;
303 assert( nValuesF == nValues ); // should be guaranteed by the parser
304 for ( k = 0; k < nValuesF; k++ )
305 pValues[k] = Abc_AigOr( (Abc_Aig_t *)pNtkNew->pManFunc, pValues[k], Abc_AigAnd((Abc_Aig_t *)pNtkNew->pManFunc, pTemp, pValuesF[k]) );
306 }
307 else
308 {
309 // get the output value
310 Index = Abc_StringGetNumber( &pSop );
311 assert( Index < nValues );
312 pValues[Index] = Abc_AigOr( (Abc_Aig_t *)pNtkNew->pManFunc, pValues[Index], pTemp );
313 }
314 // advance the reading point
315 assert( *pSop == '\n' );
316 pSop++;
317 }
318
319 // compute the default value
320 if ( Def >= 0 || DefIndex >= 0 )
321 {
322 pTemp = Abc_AigConst1(pNtkNew);
323 for ( k = 0; k < nValues; k++ )
324 {
325 if ( k == Def )
326 continue;
327 pTemp = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, pTemp, Abc_ObjNot(pValues[k]) );
328 }
329
330 // assign the default value
331 if ( Def >= 0 )
332 pValues[Def] = pTemp;
333 else
334 {
335 assert( DefIndex >= 0 );
336 // add values of the given fanin with the given cube
337 pFanin = Abc_ObjFanin( pObj, DefIndex );
338 nValuesF = Abc_ObjMvVarNum(pFanin);
339 pValuesF = (Abc_Obj_t **)pFanin->pCopy;
340 assert( nValuesF == nValues ); // should be guaranteed by the parser
341 for ( k = 0; k < nValuesF; k++ )
342 pValues[k] = Abc_AigOr( (Abc_Aig_t *)pNtkNew->pManFunc, pValues[k], Abc_AigAnd((Abc_Aig_t *)pNtkNew->pManFunc, pTemp, pValuesF[k]) );
343 }
344
345 }
346
347 // save the values in the fanout net
348 pNet->pCopy = (Abc_Obj_t *)pValues;
349 return 1;
350 }
351
352 /**Function*************************************************************
353
354 Synopsis [Assigns name with index.]
355
356 Description []
357
358 SideEffects []
359
360 SeeAlso []
361
362 ***********************************************************************/
Abc_NtkConvertAssignName(Abc_Obj_t * pObj,Abc_Obj_t * pNet,int Index)363 static inline void Abc_NtkConvertAssignName( Abc_Obj_t * pObj, Abc_Obj_t * pNet, int Index )
364 {
365 char Suffix[16];
366 assert( Abc_ObjIsTerm(pObj) );
367 assert( Abc_ObjIsNet(pNet) );
368 sprintf( Suffix, "[%d]", Index );
369 Abc_ObjAssignName( pObj, Abc_ObjName(pNet), Suffix );
370 }
371
372 /**Function*************************************************************
373
374 Synopsis [Strashes the BLIF-MV netlist.]
375
376 Description []
377
378 SideEffects []
379
380 SeeAlso []
381
382 ***********************************************************************/
Abc_NtkStrashBlifMv(Abc_Ntk_t * pNtk)383 Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
384 {
385 int fUsePositional = 0;
386 Vec_Ptr_t * vNodes;
387 Abc_Obj_t ** pBits;
388 Abc_Obj_t ** pValues;
389 Abc_Ntk_t * pNtkNew;
390 Abc_Obj_t * pObj, * pTemp, * pBit, * pNet;
391 int i, k, v, nValues, nValuesMax, nBits;
392 int nCount1, nCount2;
393
394 assert( Abc_NtkIsNetlist(pNtk) );
395 assert( Abc_NtkHasBlifMv(pNtk) );
396 assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
397 assert( Abc_NtkBlackboxNum(pNtk) == 0 );
398
399 // get the largest number of values
400 nValuesMax = 2;
401 Abc_NtkForEachNet( pNtk, pObj, i )
402 {
403 nValues = Abc_ObjMvVarNum(pObj);
404 if ( nValuesMax < nValues )
405 nValuesMax = nValues;
406 }
407 nBits = Abc_Base2Log( nValuesMax );
408 pBits = ABC_ALLOC( Abc_Obj_t *, nBits );
409
410 // clean the node copy fields
411 Abc_NtkCleanCopy( pNtk );
412 // collect the nodes
413 vNodes = Abc_NtkDfs( pNtk, 0 );
414
415 // start the network
416 pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
417 // duplicate the name and the spec
418 pNtkNew->pName = Extra_UtilStrsav( pNtk->pName );
419 // pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pName );
420
421 nCount1 = nCount2 = 0;
422 // encode the CI nets
423 Abc_NtkIncrementTravId( pNtk );
424 if ( fUsePositional )
425 {
426 Abc_NtkForEachCi( pNtk, pObj, i )
427 {
428 if ( !Abc_ObjIsPi(pObj) )
429 continue;
430 pNet = Abc_ObjFanout0(pObj);
431 nValues = Abc_ObjMvVarNum(pNet);
432 pValues = ABC_ALLOC( Abc_Obj_t *, nValues );
433 // create PIs for the values
434 for ( v = 0; v < nValues; v++ )
435 {
436 pValues[v] = Abc_NtkCreatePi( pNtkNew );
437 if ( nValuesMax == 2 )
438 Abc_ObjAssignName( pValues[v], Abc_ObjName(pNet), NULL );
439 else
440 Abc_NtkConvertAssignName( pValues[v], pNet, v );
441 }
442 // save the values in the fanout net
443 pNet->pCopy = (Abc_Obj_t *)pValues;
444 // mark the net
445 Abc_NodeSetTravIdCurrent( pNet );
446 }
447 Abc_NtkForEachCi( pNtk, pObj, i )
448 {
449 if ( Abc_ObjIsPi(pObj) )
450 continue;
451 pNet = Abc_ObjFanout0(pObj);
452 nValues = Abc_ObjMvVarNum(pNet);
453 pValues = ABC_ALLOC( Abc_Obj_t *, nValues );
454 // create PIs for the values
455 for ( v = 0; v < nValues; v++ )
456 {
457 pValues[v] = Abc_NtkCreateBo( pNtkNew );
458 if ( nValuesMax == 2 )
459 Abc_ObjAssignName( pValues[v], Abc_ObjName(pNet), NULL );
460 else
461 Abc_NtkConvertAssignName( pValues[v], pNet, v );
462 nCount1++;
463 }
464 // save the values in the fanout net
465 pNet->pCopy = (Abc_Obj_t *)pValues;
466 // mark the net
467 Abc_NodeSetTravIdCurrent( pNet );
468 }
469 }
470 else
471 {
472 Abc_NtkForEachCi( pNtk, pObj, i )
473 {
474 if ( !Abc_ObjIsPi(pObj) )
475 continue;
476 pNet = Abc_ObjFanout0(pObj);
477 nValues = Abc_ObjMvVarNum(pNet);
478 pValues = ABC_ALLOC( Abc_Obj_t *, nValues );
479 // create PIs for the encoding bits
480 nBits = Abc_Base2Log( nValues );
481 for ( k = 0; k < nBits; k++ )
482 {
483 pBits[k] = Abc_NtkCreatePi( pNtkNew );
484 if ( nValuesMax == 2 )
485 Abc_ObjAssignName( pBits[k], Abc_ObjName(pNet), NULL );
486 else
487 Abc_NtkConvertAssignName( pBits[k], pNet, k );
488 }
489 // encode the values
490 for ( v = 0; v < nValues; v++ )
491 {
492 pValues[v] = Abc_AigConst1(pNtkNew);
493 for ( k = 0; k < nBits; k++ )
494 {
495 pBit = Abc_ObjNotCond( pBits[k], (v&(1<<k)) == 0 );
496 pValues[v] = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, pValues[v], pBit );
497 }
498 }
499 // save the values in the fanout net
500 pNet->pCopy = (Abc_Obj_t *)pValues;
501 // mark the net
502 Abc_NodeSetTravIdCurrent( pNet );
503 }
504 Abc_NtkForEachCi( pNtk, pObj, i )
505 {
506 if ( Abc_ObjIsPi(pObj) )
507 continue;
508 pNet = Abc_ObjFanout0(pObj);
509 nValues = Abc_ObjMvVarNum(pNet);
510 pValues = ABC_ALLOC( Abc_Obj_t *, nValues );
511 // create PIs for the encoding bits
512 nBits = Abc_Base2Log( nValues );
513 for ( k = 0; k < nBits; k++ )
514 {
515 pBits[k] = Abc_NtkCreateBo( pNtkNew );
516 if ( nValuesMax == 2 )
517 Abc_ObjAssignName( pBits[k], Abc_ObjName(pNet), NULL );
518 else
519 Abc_NtkConvertAssignName( pBits[k], pNet, k );
520 nCount1++;
521 }
522 // encode the values
523 for ( v = 0; v < nValues; v++ )
524 {
525 pValues[v] = Abc_AigConst1(pNtkNew);
526 for ( k = 0; k < nBits; k++ )
527 {
528 pBit = Abc_ObjNotCond( pBits[k], (v&(1<<k)) == 0 );
529 pValues[v] = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, pValues[v], pBit );
530 }
531 }
532 // save the values in the fanout net
533 pNet->pCopy = (Abc_Obj_t *)pValues;
534 // mark the net
535 Abc_NodeSetTravIdCurrent( pNet );
536 }
537 }
538
539 // process nodes in the topological order
540 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
541 if ( !Abc_NodeStrashBlifMv( pNtkNew, pObj ) )
542 {
543 Abc_NtkDelete( pNtkNew );
544 return NULL;
545 }
546 Vec_PtrFree( vNodes );
547
548 // encode the CO nets
549 if ( fUsePositional )
550 {
551 Abc_NtkForEachCo( pNtk, pObj, i )
552 {
553 if ( !Abc_ObjIsPo(pObj) )
554 continue;
555 pNet = Abc_ObjFanin0(pObj);
556 // skip marked nets
557 // if ( Abc_NodeIsTravIdCurrent(pNet) )
558 // continue;
559 // Abc_NodeSetTravIdCurrent( pNet );
560 nValues = Abc_ObjMvVarNum(pNet);
561 pValues = (Abc_Obj_t **)pNet->pCopy;
562 for ( v = 0; v < nValues; v++ )
563 {
564 pTemp = Abc_NtkCreatePo( pNtkNew );
565 Abc_ObjAddFanin( pTemp, pValues[v] );
566 if ( nValuesMax == 2 )
567 Abc_ObjAssignName( pTemp, Abc_ObjName(pNet), NULL );
568 else
569 Abc_NtkConvertAssignName( pTemp, pNet, v );
570 }
571 }
572 Abc_NtkForEachCo( pNtk, pObj, i )
573 {
574 if ( Abc_ObjIsPo(pObj) )
575 continue;
576 pNet = Abc_ObjFanin0(pObj);
577 // skip marked nets
578 // if ( Abc_NodeIsTravIdCurrent(pNet) )
579 // continue;
580 // Abc_NodeSetTravIdCurrent( pNet );
581 nValues = Abc_ObjMvVarNum(pNet);
582 pValues = (Abc_Obj_t **)pNet->pCopy;
583 for ( v = 0; v < nValues; v++ )
584 {
585 pTemp = Abc_NtkCreateBi( pNtkNew );
586 Abc_ObjAddFanin( pTemp, pValues[v] );
587 if ( nValuesMax == 2 )
588 Abc_ObjAssignName( pTemp, Abc_ObjName(pNet), NULL );
589 else
590 Abc_NtkConvertAssignName( pTemp, pNet, v );
591 nCount2++;
592 }
593 }
594 }
595 else // if ( fPositional == 0 )
596 {
597 Abc_NtkForEachCo( pNtk, pObj, i )
598 {
599 if ( !Abc_ObjIsPo(pObj) )
600 continue;
601 pNet = Abc_ObjFanin0(pObj);
602 // skip marked nets
603 // if ( Abc_NodeIsTravIdCurrent(pNet) )
604 // continue;
605 // Abc_NodeSetTravIdCurrent( pNet );
606 nValues = Abc_ObjMvVarNum(pNet);
607 pValues = (Abc_Obj_t **)pNet->pCopy;
608 nBits = Abc_Base2Log( nValues );
609 for ( k = 0; k < nBits; k++ )
610 {
611 pBit = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
612 for ( v = 0; v < nValues; v++ )
613 if ( v & (1<<k) )
614 pBit = Abc_AigOr( (Abc_Aig_t *)pNtkNew->pManFunc, pBit, pValues[v] );
615 pTemp = Abc_NtkCreatePo( pNtkNew );
616 Abc_ObjAddFanin( pTemp, pBit );
617 if ( nValuesMax == 2 )
618 Abc_ObjAssignName( pTemp, Abc_ObjName(pNet), NULL );
619 else
620 Abc_NtkConvertAssignName( pTemp, pNet, k );
621 }
622 }
623 Abc_NtkForEachCo( pNtk, pObj, i )
624 {
625 if ( Abc_ObjIsPo(pObj) )
626 continue;
627 pNet = Abc_ObjFanin0(pObj);
628 // skip marked nets
629 // if ( Abc_NodeIsTravIdCurrent(pNet) )
630 // continue;
631 // Abc_NodeSetTravIdCurrent( pNet );
632 nValues = Abc_ObjMvVarNum(pNet);
633 pValues = (Abc_Obj_t **)pNet->pCopy;
634 nBits = Abc_Base2Log( nValues );
635 for ( k = 0; k < nBits; k++ )
636 {
637 pBit = Abc_ObjNot( Abc_AigConst1(pNtkNew) );
638 for ( v = 0; v < nValues; v++ )
639 if ( v & (1<<k) )
640 pBit = Abc_AigOr( (Abc_Aig_t *)pNtkNew->pManFunc, pBit, pValues[v] );
641 pTemp = Abc_NtkCreateBi( pNtkNew );
642 Abc_ObjAddFanin( pTemp, pBit );
643 if ( nValuesMax == 2 )
644 Abc_ObjAssignName( pTemp, Abc_ObjName(pNet), NULL );
645 else
646 Abc_NtkConvertAssignName( pTemp, pNet, k );
647 nCount2++;
648 }
649 }
650 }
651
652 if ( Abc_NtkLatchNum(pNtk) )
653 {
654 Vec_Ptr_t * vTemp;
655 Abc_Obj_t * pLatch, * pObjLi, * pObjLo;
656 int i;
657 // move free vars to the front among the PIs
658 vTemp = Vec_PtrAlloc( Vec_PtrSize(pNtkNew->vPis) );
659 Abc_NtkForEachPi( pNtkNew, pObj, i )
660 if ( strncmp( Abc_ObjName(pObj), "free_var_", 9 ) == 0 )
661 Vec_PtrPush( vTemp, pObj );
662 Abc_NtkForEachPi( pNtkNew, pObj, i )
663 if ( strncmp( Abc_ObjName(pObj), "free_var_", 9 ) != 0 )
664 Vec_PtrPush( vTemp, pObj );
665 assert( Vec_PtrSize(vTemp) == Vec_PtrSize(pNtkNew->vPis) );
666 Vec_PtrFree( pNtkNew->vPis );
667 pNtkNew->vPis = vTemp;
668 // move free vars to the front among the CIs
669 vTemp = Vec_PtrAlloc( Vec_PtrSize(pNtkNew->vCis) );
670 Abc_NtkForEachCi( pNtkNew, pObj, i )
671 if ( strncmp( Abc_ObjName(pObj), "free_var_", 9 ) == 0 )
672 Vec_PtrPush( vTemp, pObj );
673 Abc_NtkForEachCi( pNtkNew, pObj, i )
674 if ( strncmp( Abc_ObjName(pObj), "free_var_", 9 ) != 0 )
675 Vec_PtrPush( vTemp, pObj );
676 assert( Vec_PtrSize(vTemp) == Vec_PtrSize(pNtkNew->vCis) );
677 Vec_PtrFree( pNtkNew->vCis );
678 pNtkNew->vCis = vTemp;
679 // create registers
680 assert( nCount1 == nCount2 );
681 for ( i = 0; i < nCount1; i++ )
682 {
683 // create latch
684 pLatch = Abc_NtkCreateLatch( pNtkNew );
685 Abc_LatchSetInit0( pLatch );
686 Abc_ObjAssignName( pLatch, Abc_ObjName(pLatch), NULL );
687 // connect
688 pObjLi = Abc_NtkCo( pNtkNew, Abc_NtkCoNum(pNtkNew)-nCount1+i );
689 pObjLo = Abc_NtkCi( pNtkNew, Abc_NtkCiNum(pNtkNew)-nCount1+i );
690 Abc_ObjAddFanin( pLatch, pObjLi );
691 Abc_ObjAddFanin( pObjLo, pLatch );
692 }
693 }
694
695 // cleanup
696 ABC_FREE( pBits );
697 Abc_NtkForEachObj( pNtk, pObj, i )
698 if ( pObj->pCopy )
699 ABC_FREE( pObj->pCopy );
700
701 // remove dangling nodes
702 i = Abc_AigCleanup((Abc_Aig_t *)pNtkNew->pManFunc);
703 // printf( "Cleanup removed %d nodes.\n", i );
704 // Abc_NtkReassignIds( pNtkNew );
705
706 // check integrity
707 if ( !Abc_NtkCheck( pNtkNew ) )
708 {
709 fprintf( stdout, "Abc_NtkStrashBlifMv(): Network check has failed.\n" );
710 Abc_NtkDelete( pNtkNew );
711 return NULL;
712 }
713 return pNtkNew;
714 }
715
716 /**Function*************************************************************
717
718 Synopsis [Extract the MV-skeleton of the BLIF-MV network.]
719
720 Description []
721
722 SideEffects []
723
724 SeeAlso []
725
726 ***********************************************************************/
Abc_NtkSkeletonBlifMv(Abc_Ntk_t * pNtk)727 Abc_Ntk_t * Abc_NtkSkeletonBlifMv( Abc_Ntk_t * pNtk )
728 {
729 int fUsePositional = 0;
730 Abc_Ntk_t * pNtkNew;
731 Abc_Obj_t * pObj, * pNet, * pNetNew, * pNodeNew, * pTermNew, * pBoxNew;
732 int i, k, v, nValues, nBits;
733
734 assert( Abc_NtkIsNetlist(pNtk) );
735 assert( Abc_NtkHasBlifMv(pNtk) );
736 assert( Abc_NtkWhiteboxNum(pNtk) == 0 );
737 assert( Abc_NtkBlackboxNum(pNtk) == 0 );
738
739 // clean the node copy fields
740 Abc_NtkCleanCopy( pNtk );
741
742 // start the network
743 pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
744 // duplicate the name and the spec
745 pNtkNew->pName = Extra_UtilStrsav( pNtk->pName );
746 pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pName );
747 // create the internal box (it is important to put it first!)
748 pBoxNew = Abc_NtkCreateWhitebox( pNtkNew );
749 // create PIs and their nets
750 Abc_NtkForEachPi( pNtk, pObj, i )
751 {
752 Abc_NtkDupObj( pNtkNew, pObj, 0 );
753 pNet = Abc_ObjFanout0(pObj);
754 Abc_NtkDupObj( pNtkNew, pNet, 1 );
755 Abc_ObjAddFanin( pNet->pCopy, pObj->pCopy );
756 }
757 // create POs and their nets
758 Abc_NtkForEachPo( pNtk, pObj, i )
759 {
760 Abc_NtkDupObj( pNtkNew, pObj, 0 );
761 pNet = Abc_ObjFanin0(pObj);
762 if ( pNet->pCopy == NULL )
763 Abc_NtkDupObj( pNtkNew, pNet, 1 );
764 Abc_ObjAddFanin( pObj->pCopy, pNet->pCopy );
765 }
766 // create latches
767 Abc_NtkForEachLatch( pNtk, pObj, i )
768 {
769 Abc_NtkDupBox( pNtkNew, pObj, 0 );
770 // latch outputs
771 pNet = Abc_ObjFanout0(Abc_ObjFanout0(pObj));
772 assert( pNet->pCopy == NULL );
773 Abc_NtkDupObj( pNtkNew, pNet, 1 );
774 Abc_ObjAddFanin( pNet->pCopy, Abc_ObjFanout0(pObj)->pCopy );
775 // latch inputs
776 pNet = Abc_ObjFanin0(Abc_ObjFanin0(pObj));
777 if ( pNet->pCopy == NULL )
778 Abc_NtkDupObj( pNtkNew, pNet, 1 );
779 Abc_ObjAddFanin( Abc_ObjFanin0(pObj)->pCopy, pNet->pCopy );
780 }
781
782 // encode the CI nets
783 Abc_NtkIncrementTravId( pNtk );
784 if ( fUsePositional )
785 {
786 Abc_NtkForEachCi( pNtk, pObj, i )
787 {
788 pNet = Abc_ObjFanout0(pObj);
789 nValues = Abc_ObjMvVarNum(pNet);
790 for ( v = 0; v < nValues; v++ )
791 {
792 pNodeNew = Abc_NtkCreateNode( pNtkNew );
793 pNodeNew->pData = Abc_SopEncoderPos( (Mem_Flex_t *)pNtkNew->pManFunc, v, nValues );
794 pNetNew = Abc_NtkCreateNet( pNtkNew );
795 pTermNew = Abc_NtkCreateBi( pNtkNew );
796 Abc_ObjAddFanin( pNodeNew, pNet->pCopy );
797 Abc_ObjAddFanin( pNetNew, pNodeNew );
798 Abc_ObjAddFanin( pTermNew, pNetNew );
799 Abc_ObjAddFanin( pBoxNew, pTermNew );
800 }
801 // mark the net
802 Abc_NodeSetTravIdCurrent( pNet );
803 }
804 }
805 else
806 {
807 Abc_NtkForEachCi( pNtk, pObj, i )
808 {
809 pNet = Abc_ObjFanout0(pObj);
810 nValues = Abc_ObjMvVarNum(pNet);
811 nBits = Abc_Base2Log( nValues );
812 for ( k = 0; k < nBits; k++ )
813 {
814 pNodeNew = Abc_NtkCreateNode( pNtkNew );
815 pNodeNew->pData = Abc_SopEncoderLog( (Mem_Flex_t *)pNtkNew->pManFunc, k, nValues );
816 pNetNew = Abc_NtkCreateNet( pNtkNew );
817 pTermNew = Abc_NtkCreateBi( pNtkNew );
818 Abc_ObjAddFanin( pNodeNew, pNet->pCopy );
819 Abc_ObjAddFanin( pNetNew, pNodeNew );
820 Abc_ObjAddFanin( pTermNew, pNetNew );
821 Abc_ObjAddFanin( pBoxNew, pTermNew );
822 }
823 // mark the net
824 Abc_NodeSetTravIdCurrent( pNet );
825 }
826 }
827
828 // encode the CO nets
829 if ( fUsePositional )
830 {
831 Abc_NtkForEachCo( pNtk, pObj, i )
832 {
833 pNet = Abc_ObjFanin0(pObj);
834 // skip marked nets
835 if ( Abc_NodeIsTravIdCurrent(pNet) )
836 continue;
837 Abc_NodeSetTravIdCurrent( pNet );
838 nValues = Abc_ObjMvVarNum(pNet);
839 pNodeNew = Abc_NtkCreateNode( pNtkNew );
840 pNodeNew->pData = Abc_SopDecoderPos( (Mem_Flex_t *)pNtkNew->pManFunc, nValues );
841 for ( v = 0; v < nValues; v++ )
842 {
843 pTermNew = Abc_NtkCreateBo( pNtkNew );
844 pNetNew = Abc_NtkCreateNet( pNtkNew );
845 Abc_ObjAddFanin( pTermNew, pBoxNew );
846 Abc_ObjAddFanin( pNetNew, pTermNew );
847 Abc_ObjAddFanin( pNodeNew, pNetNew );
848 }
849 Abc_ObjAddFanin( pNet->pCopy, pNodeNew );
850 }
851 }
852 else
853 {
854 Abc_NtkForEachCo( pNtk, pObj, i )
855 {
856 pNet = Abc_ObjFanin0(pObj);
857 // skip marked nets
858 if ( Abc_NodeIsTravIdCurrent(pNet) )
859 continue;
860 Abc_NodeSetTravIdCurrent( pNet );
861 nValues = Abc_ObjMvVarNum(pNet);
862 nBits = Abc_Base2Log( nValues );
863 pNodeNew = Abc_NtkCreateNode( pNtkNew );
864 pNodeNew->pData = Abc_SopDecoderLog( (Mem_Flex_t *)pNtkNew->pManFunc, nValues );
865 for ( k = 0; k < nBits; k++ )
866 {
867 pTermNew = Abc_NtkCreateBo( pNtkNew );
868 pNetNew = Abc_NtkCreateNet( pNtkNew );
869 Abc_ObjAddFanin( pTermNew, pBoxNew );
870 Abc_ObjAddFanin( pNetNew, pTermNew );
871 Abc_ObjAddFanin( pNodeNew, pNetNew );
872 }
873 Abc_ObjAddFanin( pNet->pCopy, pNodeNew );
874 }
875 }
876
877 // if it is a BLIF-MV netlist transfer the values of all nets
878 if ( Abc_NtkHasBlifMv(pNtk) && Abc_NtkMvVar(pNtk) )
879 {
880 if ( Abc_NtkMvVar( pNtkNew ) == NULL )
881 Abc_NtkStartMvVars( pNtkNew );
882 Abc_NtkForEachNet( pNtk, pObj, i )
883 if ( pObj->pCopy )
884 Abc_NtkSetMvVarValues( pObj->pCopy, Abc_ObjMvVarNum(pObj) );
885 }
886
887 // check integrity
888 if ( !Abc_NtkCheck( pNtkNew ) )
889 {
890 fprintf( stdout, "Abc_NtkSkeletonBlifMv(): Network check has failed.\n" );
891 Abc_NtkDelete( pNtkNew );
892 return NULL;
893 }
894 return pNtkNew;
895 }
896
897 /**Function*************************************************************
898
899 Synopsis [Inserts processed network into original base MV network.]
900
901 Description [The original network remembers the interface of combinational
902 logic (PIs/POs/latches names and values). The processed network may
903 be binary or multi-valued (currently, multi-value is not supported).
904 The resulting network has the same interface as the original network
905 while the internal logic is the same as that of the processed network.]
906
907 SideEffects []
908
909 SeeAlso []
910
911 ***********************************************************************/
Abc_NtkInsertBlifMv(Abc_Ntk_t * pNtkBase,Abc_Ntk_t * pNtkLogic)912 Abc_Ntk_t * Abc_NtkInsertBlifMv( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtkLogic )
913 {
914 Abc_Ntk_t * pNtkSkel, * pNtkNew;
915 Abc_Obj_t * pBox;
916
917 assert( Abc_NtkIsNetlist(pNtkBase) );
918 assert( Abc_NtkHasBlifMv(pNtkBase) );
919 assert( Abc_NtkWhiteboxNum(pNtkBase) == 0 );
920 assert( Abc_NtkBlackboxNum(pNtkBase) == 0 );
921
922 assert( Abc_NtkIsNetlist(pNtkLogic) );
923 assert( Abc_NtkHasBlifMv(pNtkLogic) );
924 assert( Abc_NtkWhiteboxNum(pNtkLogic) == 0 );
925 assert( Abc_NtkBlackboxNum(pNtkLogic) == 0 );
926
927 // extract the skeleton of the old network
928 pNtkSkel = Abc_NtkSkeletonBlifMv( pNtkBase );
929
930 // set the implementation of the box to be the same as the processed network
931 assert( Abc_NtkWhiteboxNum(pNtkSkel) == 1 );
932 pBox = Abc_NtkBox( pNtkSkel, 0 );
933 assert( Abc_ObjIsWhitebox(pBox) );
934 assert( pBox->pData == NULL );
935 assert( Abc_ObjFaninNum(pBox) == Abc_NtkPiNum(pNtkLogic) );
936 assert( Abc_ObjFanoutNum(pBox) == Abc_NtkPoNum(pNtkLogic) );
937 pBox->pData = pNtkLogic;
938
939 // flatten the hierarchy to insert the processed network
940 pNtkNew = Abc_NtkFlattenLogicHierarchy( pNtkSkel );
941 pBox->pData = NULL;
942 Abc_NtkDelete( pNtkSkel );
943 return pNtkNew;
944 }
945
946 /**Function*************************************************************
947
948 Synopsis [Converts SOP netlist into BLIF-MV netlist.]
949
950 Description []
951
952 SideEffects []
953
954 SeeAlso []
955
956 ***********************************************************************/
Abc_NtkConvertToBlifMv(Abc_Ntk_t * pNtk)957 int Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk )
958 {
959 #ifdef ABC_USE_CUDD
960 Mem_Flex_t * pMmFlex;
961 Abc_Obj_t * pNode;
962 Vec_Str_t * vCube;
963 char * pSop0, * pSop1, * pBlifMv, * pCube, * pCur;
964 int Value, nCubes, nSize, i, k;
965
966 assert( Abc_NtkIsNetlist(pNtk) );
967 if ( !Abc_NtkToBdd(pNtk) )
968 {
969 printf( "Converting logic functions to BDDs has failed.\n" );
970 return 0;
971 }
972
973 pMmFlex = Mem_FlexStart();
974 vCube = Vec_StrAlloc( 100 );
975 Abc_NtkForEachNode( pNtk, pNode, i )
976 {
977 // convert BDD into cubes for on-set and off-set
978 Abc_NodeBddToCnf( pNode, pMmFlex, vCube, 0, &pSop0, &pSop1 );
979 // allocate room for the MV-SOP
980 nCubes = Abc_SopGetCubeNum(pSop0) + Abc_SopGetCubeNum(pSop1);
981 nSize = nCubes*(2*Abc_ObjFaninNum(pNode) + 2)+1;
982 pBlifMv = Mem_FlexEntryFetch( pMmFlex, nSize );
983 // add the cubes
984 pCur = pBlifMv;
985 Abc_SopForEachCube( pSop0, Abc_ObjFaninNum(pNode), pCube )
986 {
987 Abc_CubeForEachVar( pCube, Value, k )
988 {
989 *pCur++ = Value;
990 *pCur++ = ' ';
991 }
992 *pCur++ = '0';
993 *pCur++ = '\n';
994 }
995 Abc_SopForEachCube( pSop1, Abc_ObjFaninNum(pNode), pCube )
996 {
997 Abc_CubeForEachVar( pCube, Value, k )
998 {
999 *pCur++ = Value;
1000 *pCur++ = ' ';
1001 }
1002 *pCur++ = '1';
1003 *pCur++ = '\n';
1004 }
1005 *pCur++ = 0;
1006 assert( pCur - pBlifMv == nSize );
1007 // update the node representation
1008 Cudd_RecursiveDeref( (DdManager *)pNtk->pManFunc, (DdNode *)pNode->pData );
1009 pNode->pData = pBlifMv;
1010 }
1011
1012 // update the functionality type
1013 pNtk->ntkFunc = ABC_FUNC_BLIFMV;
1014 Cudd_Quit( (DdManager *)pNtk->pManFunc );
1015 pNtk->pManFunc = pMmFlex;
1016
1017 Vec_StrFree( vCube );
1018 #endif
1019 return 1;
1020 }
1021
1022 /**Function*************************************************************
1023
1024 Synopsis [Converts SOP into MV-SOP.]
1025
1026 Description []
1027
1028 SideEffects []
1029
1030 SeeAlso []
1031
1032 ***********************************************************************/
Abc_NodeConvertSopToMvSop(int nVars,Vec_Int_t * vSop0,Vec_Int_t * vSop1)1033 char * Abc_NodeConvertSopToMvSop( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 )
1034 {
1035 char * pMvSop, * pCur;
1036 unsigned uCube;
1037 int nCubes, nSize, Value, i, k;
1038 // consider the case of the constant node
1039 if ( Vec_IntSize(vSop0) == 0 || Vec_IntSize(vSop1) == 0 )
1040 {
1041 // (temporary) create a tautology cube
1042 pMvSop = ABC_ALLOC( char, nVars + 3 );
1043 for ( k = 0; k < nVars; k++ )
1044 pMvSop[k] = '-';
1045 pMvSop[nVars] = '0' + (int)(Vec_IntSize(vSop1) > 0);
1046 pMvSop[nVars+1] = '\n';
1047 pMvSop[nVars+2] = 0;
1048 return pMvSop;
1049 }
1050 // find the total number of cubes
1051 nCubes = Vec_IntSize(vSop0) + Vec_IntSize(vSop1);
1052 // find the size of the MVSOP represented as a C-string
1053 // (each cube has nVars variables + one output literal + end-of-line,
1054 // and the string is zero-terminated)
1055 nSize = nCubes * (nVars + 2) + 1;
1056 // allocate memory
1057 pMvSop = pCur = ABC_ALLOC( char, nSize );
1058 // fill in the negative polarity cubes
1059 Vec_IntForEachEntry( vSop0, uCube, i )
1060 {
1061 for ( k = 0; k < nVars; k++ )
1062 {
1063 Value = (uCube >> (2*k)) & 3;
1064 if ( Value == 1 )
1065 *pCur++ = '0';
1066 else if ( Value == 2 )
1067 *pCur++ = '1';
1068 else if ( Value == 0 )
1069 *pCur++ = '-';
1070 else
1071 assert( 0 );
1072 }
1073 *pCur++ = '0';
1074 *pCur++ = '\n';
1075 }
1076 // fill in the positive polarity cubes
1077 Vec_IntForEachEntry( vSop1, uCube, i )
1078 {
1079 for ( k = 0; k < nVars; k++ )
1080 {
1081 Value = (uCube >> (2*k)) & 3;
1082 if ( Value == 1 )
1083 *pCur++ = '0';
1084 else if ( Value == 2 )
1085 *pCur++ = '1';
1086 else if ( Value == 0 )
1087 *pCur++ = '-';
1088 else
1089 assert( 0 );
1090 }
1091 *pCur++ = '1';
1092 *pCur++ = '\n';
1093 }
1094 *pCur++ = 0;
1095 assert( pCur - pMvSop == nSize );
1096 return pMvSop;
1097 }
1098
1099
1100 /**Function*************************************************************
1101
1102 Synopsis [A prototype of internal cost evaluation procedure.]
1103
1104 Description [This procedure takes the number of variables (nVars),
1105 the array of values of the inputs and the output (pVarValues)
1106 (note that this array has nVars+1 entries), and an MV-SOP represented
1107 as a C-string with one charater for each literal, including inputs
1108 and output. Each cube is terminated with the new-line character ('\n').
1109 The string is zero-terminated.]
1110
1111 SideEffects []
1112
1113 SeeAlso []
1114
1115 ***********************************************************************/
Abc_NodeEvalMvCostInternal(int nVars,int * pVarValues,char * pMvSop)1116 int Abc_NodeEvalMvCostInternal( int nVars, int * pVarValues, char * pMvSop )
1117 {
1118 // for now, return the number of cubes in the MV-SOP
1119 int Counter = 0;
1120 while ( *pMvSop ) Counter += (*pMvSop++ == '\n');
1121 return Counter;
1122 }
1123
1124
1125 /**Function*************************************************************
1126
1127 Synopsis [Evaluates the cost of the cut.]
1128
1129 Description [The Boolean function of the cut is specified by two SOPs,
1130 which represent the negative/positive polarities of the cut function.
1131 Converts these two SOPs into a mutually-agreed-upon representation
1132 to be passed to the internal cost-evaluation procedure (see the above
1133 prototype Abc_NodeEvalMvCostInternal).]
1134
1135 SideEffects []
1136
1137 SeeAlso []
1138
1139 ***********************************************************************/
Abc_NodeEvalMvCost(int nVars,Vec_Int_t * vSop0,Vec_Int_t * vSop1)1140 int Abc_NodeEvalMvCost( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 )
1141 {
1142 char * pMvSop;
1143 int * pVarValues;
1144 int i, RetValue;
1145 // collect the input and output values (currently, they are binary)
1146 pVarValues = ABC_ALLOC( int, nVars + 1 );
1147 for ( i = 0; i <= nVars; i++ )
1148 pVarValues[i] = 2;
1149 // prepare MV-SOP for evaluation
1150 pMvSop = Abc_NodeConvertSopToMvSop( nVars, vSop0, vSop1 );
1151 // have a look at the MV-SOP:
1152 // printf( "%s\n", pMvSop );
1153 // get the result of internal cost evaluation
1154 RetValue = Abc_NodeEvalMvCostInternal( nVars, pVarValues, pMvSop );
1155 // cleanup
1156 ABC_FREE( pVarValues );
1157 ABC_FREE( pMvSop );
1158 return RetValue;
1159 }
1160
1161 ////////////////////////////////////////////////////////////////////////
1162 /// END OF FILE ///
1163 ////////////////////////////////////////////////////////////////////////
1164
1165
1166 ABC_NAMESPACE_IMPL_END
1167
1168