abc70930: src/aig/aig/aigUtil.c Source File

00001 
00021 #include "aig.h"
00022 
00026 
00030 
00042 unsigned int Aig_PrimeCudd( unsigned int p )
00043 {
00044     int i,pn;
00045 
00046     p--;
00047     do {
00048         p++;
00049         if (p&1) {
00050             pn = 1;
00051             i = 3;
00052             while ((unsigned) (i * i) <= p) {
00053                 if (p % i == 0) {
00054                     pn = 0;
00055                     break;
00056                 }
00057                 i += 2;
00058             }
00059         } else {
00060             pn = 0;
00061         }
00062     } while (!pn);
00063     return(p);
00064 
00065 } /* end of Cudd_Prime */
00066 
00078 void Aig_ManIncrementTravId( Aig_Man_t * p )
00079 {
00080     if ( p->nTravIds >= (1<<30)-1 )
00081         Aig_ManCleanData( p );
00082     p->nTravIds++;
00083 }
00084 
00096 int Aig_ManLevels( Aig_Man_t * p )
00097 {
00098     Aig_Obj_t * pObj;
00099     int i, LevelMax = 0;
00100     Aig_ManForEachPo( p, pObj, i )
00101         LevelMax = AIG_MAX( LevelMax, (int)Aig_ObjFanin0(pObj)->Level );
00102     return LevelMax;
00103 }
00104 
00116 void Aig_ManResetRefs( Aig_Man_t * p )
00117 {
00118     Aig_Obj_t * pObj;
00119     int i;
00120     Aig_ManForEachObj( p, pObj, i )
00121         pObj->nRefs = 0;
00122     Aig_ManForEachObj( p, pObj, i )
00123     {
00124         if ( Aig_ObjFanin0(pObj) )
00125             Aig_ObjFanin0(pObj)->nRefs++;
00126         if ( Aig_ObjFanin1(pObj) )
00127             Aig_ObjFanin1(pObj)->nRefs++;
00128     }
00129 }
00130 
00142 void Aig_ManCleanMarkA( Aig_Man_t * p )
00143 {
00144     Aig_Obj_t * pObj;
00145     int i;
00146     Aig_ManForEachObj( p, pObj, i )
00147         pObj->fMarkA = 0;
00148 }
00149 
00161 void Aig_ManCleanMarkB( Aig_Man_t * p )
00162 {
00163     Aig_Obj_t * pObj;
00164     int i;
00165     Aig_ManForEachObj( p, pObj, i )
00166         pObj->fMarkB = 0;
00167 }
00168 
00180 void Aig_ManCleanData( Aig_Man_t * p )
00181 {
00182     Aig_Obj_t * pObj;
00183     int i;
00184     Aig_ManForEachObj( p, pObj, i )
00185         pObj->pData = NULL;
00186 }
00187 
00199 void Aig_ObjCleanData_rec( Aig_Obj_t * pObj )
00200 {
00201     assert( !Aig_IsComplement(pObj) );
00202     assert( !Aig_ObjIsPo(pObj) );
00203     if ( Aig_ObjIsAnd(pObj) )
00204     {
00205         Aig_ObjCleanData_rec( Aig_ObjFanin0(pObj) );
00206         Aig_ObjCleanData_rec( Aig_ObjFanin1(pObj) );
00207     }
00208     pObj->pData = NULL;
00209 }
00210 
00211 
00223 void Aig_ObjCollectMulti_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
00224 {
00225     if ( pRoot != pObj && (Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || Aig_ObjType(pRoot) != Aig_ObjType(pObj)) )
00226     {
00227         Vec_PtrPushUnique(vSuper, pObj);
00228         return;
00229     }
00230     Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild0(pObj), vSuper );
00231     Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild1(pObj), vSuper );
00232 }
00233 
00245 void Aig_ObjCollectMulti( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper )
00246 {
00247     assert( !Aig_IsComplement(pRoot) );
00248     Vec_PtrClear( vSuper );
00249     Aig_ObjCollectMulti_rec( pRoot, pRoot, vSuper );
00250 }
00251 
00263 int Aig_ObjIsMuxType( Aig_Obj_t * pNode )
00264 {
00265     Aig_Obj_t * pNode0, * pNode1;
00266     // check that the node is regular
00267     assert( !Aig_IsComplement(pNode) );
00268     // if the node is not AND, this is not MUX
00269     if ( !Aig_ObjIsAnd(pNode) )
00270         return 0;
00271     // if the children are not complemented, this is not MUX
00272     if ( !Aig_ObjFaninC0(pNode) || !Aig_ObjFaninC1(pNode) )
00273         return 0;
00274     // get children
00275     pNode0 = Aig_ObjFanin0(pNode);
00276     pNode1 = Aig_ObjFanin1(pNode);
00277     // if the children are not ANDs, this is not MUX
00278     if ( !Aig_ObjIsAnd(pNode0) || !Aig_ObjIsAnd(pNode1) )
00279         return 0;
00280     // otherwise the node is MUX iff it has a pair of equal grandchildren
00281     return (Aig_ObjFanin0(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC0(pNode1))) || 
00282            (Aig_ObjFanin0(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC1(pNode1))) ||
00283            (Aig_ObjFanin1(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC0(pNode1))) ||
00284            (Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)));
00285 }
00286 
00287 
00299 int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 )
00300 {
00301     Aig_Obj_t * p0, * p1;
00302     assert( !Aig_IsComplement(pObj) );
00303     if ( !Aig_ObjIsNode(pObj) )
00304         return 0;
00305     if ( Aig_ObjIsExor(pObj) )
00306     {
00307         *ppFan0 = Aig_ObjChild0(pObj);
00308         *ppFan1 = Aig_ObjChild1(pObj);
00309         return 1;
00310     }
00311     assert( Aig_ObjIsAnd(pObj) );
00312     p0 = Aig_ObjChild0(pObj);
00313     p1 = Aig_ObjChild1(pObj);
00314     if ( !Aig_IsComplement(p0) || !Aig_IsComplement(p1) )
00315         return 0;
00316     p0 = Aig_Regular(p0);
00317     p1 = Aig_Regular(p1);
00318     if ( !Aig_ObjIsAnd(p0) || !Aig_ObjIsAnd(p1) )
00319         return 0;
00320     if ( Aig_ObjFanin0(p0) != Aig_ObjFanin0(p1) || Aig_ObjFanin1(p0) != Aig_ObjFanin1(p1) )
00321         return 0;
00322     if ( Aig_ObjFaninC0(p0) == Aig_ObjFaninC0(p1) || Aig_ObjFaninC1(p0) == Aig_ObjFaninC1(p1) )
00323         return 0;
00324     *ppFan0 = Aig_ObjChild0(p0);
00325     *ppFan1 = Aig_ObjChild1(p0);
00326     return 1;
00327 }
00328 
00343 Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pNode, Aig_Obj_t ** ppNodeT, Aig_Obj_t ** ppNodeE )
00344 {
00345     Aig_Obj_t * pNode0, * pNode1;
00346     assert( !Aig_IsComplement(pNode) );
00347     assert( Aig_ObjIsMuxType(pNode) );
00348     // get children
00349     pNode0 = Aig_ObjFanin0(pNode);
00350     pNode1 = Aig_ObjFanin1(pNode);
00351 
00352     // find the control variable
00353     if ( Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)) )
00354     {
00355 //        if ( Fraig_IsComplement(pNode1->p2) )
00356         if ( Aig_ObjFaninC1(pNode0) )
00357         { // pNode2->p2 is positive phase of C
00358             *ppNodeT = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
00359             *ppNodeE = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
00360             return Aig_ObjChild1(pNode1);//pNode2->p2;
00361         }
00362         else
00363         { // pNode1->p2 is positive phase of C
00364             *ppNodeT = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
00365             *ppNodeE = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
00366             return Aig_ObjChild1(pNode0);//pNode1->p2;
00367         }
00368     }
00369     else if ( Aig_ObjFanin0(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC0(pNode1)) )
00370     {
00371 //        if ( Fraig_IsComplement(pNode1->p1) )
00372         if ( Aig_ObjFaninC0(pNode0) )
00373         { // pNode2->p1 is positive phase of C
00374             *ppNodeT = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
00375             *ppNodeE = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
00376             return Aig_ObjChild0(pNode1);//pNode2->p1;
00377         }
00378         else
00379         { // pNode1->p1 is positive phase of C
00380             *ppNodeT = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
00381             *ppNodeE = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
00382             return Aig_ObjChild0(pNode0);//pNode1->p1;
00383         }
00384     }
00385     else if ( Aig_ObjFanin0(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC1(pNode1)) )
00386     {
00387 //        if ( Fraig_IsComplement(pNode1->p1) )
00388         if ( Aig_ObjFaninC0(pNode0) )
00389         { // pNode2->p2 is positive phase of C
00390             *ppNodeT = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
00391             *ppNodeE = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
00392             return Aig_ObjChild1(pNode1);//pNode2->p2;
00393         }
00394         else
00395         { // pNode1->p1 is positive phase of C
00396             *ppNodeT = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
00397             *ppNodeE = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
00398             return Aig_ObjChild0(pNode0);//pNode1->p1;
00399         }
00400     }
00401     else if ( Aig_ObjFanin1(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC0(pNode1)) )
00402     {
00403 //        if ( Fraig_IsComplement(pNode1->p2) )
00404         if ( Aig_ObjFaninC1(pNode0) )
00405         { // pNode2->p1 is positive phase of C
00406             *ppNodeT = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
00407             *ppNodeE = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
00408             return Aig_ObjChild0(pNode1);//pNode2->p1;
00409         }
00410         else
00411         { // pNode1->p2 is positive phase of C
00412             *ppNodeT = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
00413             *ppNodeE = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
00414             return Aig_ObjChild1(pNode0);//pNode1->p2;
00415         }
00416     }
00417     assert( 0 ); // this is not MUX
00418     return NULL;
00419 }
00420 
00432 Aig_Obj_t * Aig_ObjReal_rec( Aig_Obj_t * pObj )
00433 {
00434     Aig_Obj_t * pObjNew, * pObjR = Aig_Regular(pObj);
00435     if ( !Aig_ObjIsBuf(pObjR) )
00436         return pObj;
00437     pObjNew = Aig_ObjReal_rec( Aig_ObjChild0(pObjR) );
00438     return Aig_NotCond( pObjNew, Aig_IsComplement(pObj) );
00439 }
00440 
00441 
00454 void Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
00455 {
00456     Vec_Ptr_t * vSuper;
00457     Aig_Obj_t * pFanin;
00458     int fCompl, i;
00459     // store the complemented attribute
00460     fCompl = Aig_IsComplement(pObj);
00461     pObj = Aig_Regular(pObj);
00462     // constant case
00463     if ( Aig_ObjIsConst1(pObj) )
00464     {
00465         fprintf( pFile, "%d", !fCompl );
00466         return;
00467     }
00468     // PI case
00469     if ( Aig_ObjIsPi(pObj) )
00470     {
00471         fprintf( pFile, "%s%s", fCompl? "!" : "", (char*)pObj->pData );
00472         return;
00473     }
00474     // AND case
00475     Vec_VecExpand( vLevels, Level );
00476     vSuper = Vec_VecEntry(vLevels, Level);
00477     Aig_ObjCollectMulti( pObj, vSuper );
00478     fprintf( pFile, "%s", (Level==0? "" : "(") );
00479     Vec_PtrForEachEntry( vSuper, pFanin, i )
00480     {
00481         Aig_ObjPrintEqn( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 );
00482         if ( i < Vec_PtrSize(vSuper) - 1 )
00483             fprintf( pFile, " %s ", fCompl? "+" : "*" );
00484     }
00485     fprintf( pFile, "%s", (Level==0? "" : ")") );
00486     return;
00487 }
00488 
00501 void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
00502 {
00503     Vec_Ptr_t * vSuper;
00504     Aig_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC;
00505     int fCompl, i;
00506     // store the complemented attribute
00507     fCompl = Aig_IsComplement(pObj);
00508     pObj = Aig_Regular(pObj);
00509     // constant case
00510     if ( Aig_ObjIsConst1(pObj) )
00511     {
00512         fprintf( pFile, "1\'b%d", !fCompl );
00513         return;
00514     }
00515     // PI case
00516     if ( Aig_ObjIsPi(pObj) )
00517     {
00518         fprintf( pFile, "%s%s", fCompl? "~" : "", (char*)pObj->pData );
00519         return;
00520     }
00521     // EXOR case
00522     if ( Aig_ObjIsExor(pObj) )
00523     {
00524         Vec_VecExpand( vLevels, Level );
00525         vSuper = Vec_VecEntry( vLevels, Level );
00526         Aig_ObjCollectMulti( pObj, vSuper );
00527         fprintf( pFile, "%s", (Level==0? "" : "(") );
00528         Vec_PtrForEachEntry( vSuper, pFanin, i )
00529         {
00530             Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 );
00531             if ( i < Vec_PtrSize(vSuper) - 1 )
00532                 fprintf( pFile, " ^ " );
00533         }
00534         fprintf( pFile, "%s", (Level==0? "" : ")") );
00535         return;
00536     }
00537     // MUX case
00538     if ( Aig_ObjIsMuxType(pObj) )
00539     {
00540         if ( Aig_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) )
00541         {
00542             fprintf( pFile, "%s", (Level==0? "" : "(") );
00543             Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
00544             fprintf( pFile, " ^ " );
00545             Aig_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 );
00546             fprintf( pFile, "%s", (Level==0? "" : ")") );
00547         }
00548         else 
00549         {
00550             pFaninC = Aig_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 );
00551             fprintf( pFile, "%s", (Level==0? "" : "(") );
00552             Aig_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 );
00553             fprintf( pFile, " ? " );
00554             Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin1, fCompl), vLevels, Level+1 );
00555             fprintf( pFile, " : " );
00556             Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
00557             fprintf( pFile, "%s", (Level==0? "" : ")") );
00558         }
00559         return;
00560     }
00561     // AND case
00562     Vec_VecExpand( vLevels, Level );
00563     vSuper = Vec_VecEntry(vLevels, Level);
00564     Aig_ObjCollectMulti( pObj, vSuper );
00565     fprintf( pFile, "%s", (Level==0? "" : "(") );
00566     Vec_PtrForEachEntry( vSuper, pFanin, i )
00567     {
00568         Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 );
00569         if ( i < Vec_PtrSize(vSuper) - 1 )
00570             fprintf( pFile, " %s ", fCompl? "|" : "&" );
00571     }
00572     fprintf( pFile, "%s", (Level==0? "" : ")") );
00573     return;
00574 }
00575 
00576 
00588 void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig )
00589 {
00590     assert( !Aig_IsComplement(pObj) );
00591     printf( "Node %p : ", pObj );
00592     if ( Aig_ObjIsConst1(pObj) )
00593         printf( "constant 1" );
00594     else if ( Aig_ObjIsPi(pObj) )
00595         printf( "PI" );
00596     else
00597         printf( "AND( %p%s, %p%s )", 
00598             Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " "), 
00599             Aig_ObjFanin1(pObj), (Aig_ObjFaninC1(pObj)? "\'" : " ") );
00600     printf( " (refs = %3d)", Aig_ObjRefs(pObj) );
00601 }
00602 
00614 void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig )
00615 {
00616     Vec_Ptr_t * vNodes;
00617     Aig_Obj_t * pObj;
00618     int i;
00619     printf( "PIs: " );
00620     Aig_ManForEachPi( p, pObj, i )
00621         printf( " %p", pObj );
00622     printf( "\n" );
00623     vNodes = Aig_ManDfs( p );
00624     Vec_PtrForEachEntry( vNodes, pObj, i )
00625         Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
00626     printf( "\n" );
00627 }
00628 
00640 void Aig_ManDump( Aig_Man_t * p )
00641 { 
00642     static int Counter = 0;
00643     char FileName[20];
00644     // dump the logic into a file
00645     sprintf( FileName, "aigbug\\%03d.blif", ++Counter );
00646     Aig_ManDumpBlif( p, FileName );
00647     printf( "Intermediate AIG with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(p), FileName );
00648 }
00649 
00661 void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
00662 {
00663     FILE * pFile;
00664     Vec_Ptr_t * vNodes;
00665     Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
00666     int i, nDigits, Counter = 0;
00667     if ( Aig_ManPoNum(p) == 0 )
00668     {
00669         printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
00670         return;
00671     }
00672     // collect nodes in the DFS order
00673     vNodes = Aig_ManDfs( p );
00674     // assign IDs to objects
00675     Aig_ManConst1(p)->iData = Counter++;
00676     Aig_ManForEachPi( p, pObj, i )
00677         pObj->iData = Counter++;
00678     Aig_ManForEachPo( p, pObj, i )
00679         pObj->iData = Counter++;
00680     Vec_PtrForEachEntry( vNodes, pObj, i )
00681         pObj->iData = Counter++;
00682     nDigits = Aig_Base10Log( Counter );
00683     // write the file
00684     pFile = fopen( pFileName, "w" );
00685     fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" );
00686 //    fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
00687     fprintf( pFile, ".model test\n" );
00688     // write PIs
00689     fprintf( pFile, ".inputs" );
00690     Aig_ManForEachPiSeq( p, pObj, i )
00691         fprintf( pFile, " n%0*d", nDigits, pObj->iData );
00692     fprintf( pFile, "\n" );
00693     // write POs
00694     fprintf( pFile, ".outputs" );
00695     Aig_ManForEachPoSeq( p, pObj, i )
00696         fprintf( pFile, " n%0*d", nDigits, pObj->iData );
00697     fprintf( pFile, "\n" );
00698     // write latches
00699     if ( Aig_ManRegNum(p) )
00700     {
00701     fprintf( pFile, "\n" );
00702     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
00703         fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, pObjLi->iData, nDigits, pObjLo->iData );
00704     fprintf( pFile, "\n" );
00705     }
00706     // write nodes
00707     Vec_PtrForEachEntry( vNodes, pObj, i )
00708     {
00709         fprintf( pFile, ".names n%0*d n%0*d n%0*d\n", 
00710             nDigits, Aig_ObjFanin0(pObj)->iData, 
00711             nDigits, Aig_ObjFanin1(pObj)->iData, 
00712             nDigits, pObj->iData );
00713         fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
00714     }
00715     // write POs
00716     Aig_ManForEachPo( p, pObj, i )
00717     {
00718         fprintf( pFile, ".names n%0*d n%0*d\n", 
00719             nDigits, Aig_ObjFanin0(pObj)->iData, 
00720             nDigits, pObj->iData );
00721         fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
00722         if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
00723             pConst1 = Aig_ManConst1(p);
00724     }
00725     if ( pConst1 )
00726         fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData );
00727     fprintf( pFile, ".end\n\n" );
00728     fclose( pFile );
00729     Vec_PtrFree( vNodes );
00730 }
00731 
00743 void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
00744 {
00745     FILE * pFile;
00746     Vec_Ptr_t * vNodes;
00747     Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
00748     int i, nDigits, Counter = 0;
00749     if ( Aig_ManPoNum(p) == 0 )
00750     {
00751         printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
00752         return;
00753     }
00754     // collect nodes in the DFS order
00755     vNodes = Aig_ManDfs( p );
00756     // assign IDs to objects
00757     Aig_ManConst1(p)->iData = Counter++;
00758     Aig_ManForEachPi( p, pObj, i )
00759         pObj->iData = Counter++;
00760     Aig_ManForEachPo( p, pObj, i )
00761         pObj->iData = Counter++;
00762     Vec_PtrForEachEntry( vNodes, pObj, i )
00763         pObj->iData = Counter++;
00764     nDigits = Aig_Base10Log( Counter );
00765     // write the file
00766     pFile = fopen( pFileName, "w" );
00767     fprintf( pFile, "// Verilog file written by procedure Aig_ManDumpVerilog()\n" );
00768 //    fprintf( pFile, "// http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
00769     if ( Aig_ManRegNum(p) )
00770         fprintf( pFile, "module %s ( clock", p->pName? p->pName: "test" );
00771     else
00772         fprintf( pFile, "module %s (", p->pName? p->pName: "test" );
00773     Aig_ManForEachPiSeq( p, pObj, i )
00774         fprintf( pFile, "%s n%0*d", ((Aig_ManRegNum(p) || i)? ",":""), nDigits, pObj->iData );
00775     Aig_ManForEachPoSeq( p, pObj, i )
00776         fprintf( pFile, ", n%0*d", nDigits, pObj->iData );
00777     fprintf( pFile, " );\n" );
00778 
00779     // write PIs
00780     if ( Aig_ManRegNum(p) )
00781         fprintf( pFile, "input clock;\n" );
00782     Aig_ManForEachPiSeq( p, pObj, i )
00783         fprintf( pFile, "input n%0*d;\n", nDigits, pObj->iData );
00784     // write POs
00785     Aig_ManForEachPoSeq( p, pObj, i )
00786         fprintf( pFile, "output n%0*d;\n", nDigits, pObj->iData );
00787     // write latches
00788     if ( Aig_ManRegNum(p) )
00789     {
00790     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
00791         fprintf( pFile, "reg n%0*d;\n", nDigits, pObjLo->iData );
00792     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
00793         fprintf( pFile, "wire n%0*d;\n", nDigits, pObjLi->iData );
00794     }
00795     // write nodes
00796     Vec_PtrForEachEntry( vNodes, pObj, i )
00797         fprintf( pFile, "wire n%0*d;\n", nDigits, pObj->iData );
00798     // write nodes
00799     Vec_PtrForEachEntry( vNodes, pObj, i )
00800     {
00801         fprintf( pFile, "assign n%0*d = %sn%0*d & %sn%0*d;\n", 
00802             nDigits, pObj->iData,
00803             !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData, 
00804             !Aig_ObjFaninC1(pObj) ? " " : "~", nDigits, Aig_ObjFanin1(pObj)->iData
00805             );
00806     }
00807     // write POs
00808     Aig_ManForEachPoSeq( p, pObj, i )
00809     {
00810         fprintf( pFile, "assign n%0*d = %sn%0*d;\n", 
00811             nDigits, pObj->iData,
00812             !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData );
00813         if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
00814             pConst1 = Aig_ManConst1(p);
00815     }
00816     if ( Aig_ManRegNum(p) )
00817     {
00818         Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
00819         {
00820             fprintf( pFile, "assign n%0*d = %sn%0*d;\n", 
00821                 nDigits, pObjLi->iData,
00822                 !Aig_ObjFaninC0(pObjLi) ? " " : "~", nDigits, Aig_ObjFanin0(pObjLi)->iData );
00823             if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObjLi)) )
00824                 pConst1 = Aig_ManConst1(p);
00825         }
00826     }
00827     if ( pConst1 )
00828         fprintf( pFile, "assign n%0*d = 1\'b1;\n", nDigits, pConst1->iData );
00829 
00830     // write initial state
00831     if ( Aig_ManRegNum(p) )
00832     {
00833         Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
00834             fprintf( pFile, "always @ (posedge clock) begin n%0*d <= n%0*d; end\n", 
00835                  nDigits, pObjLo->iData,
00836                  nDigits, pObjLi->iData );
00837         Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
00838             fprintf( pFile, "initial begin n%0*d <= 1\'b0; end\n", 
00839                  nDigits, pObjLo->iData );
00840     }
00841 
00842     fprintf( pFile, "endmodule\n\n" );
00843     fclose( pFile );
00844     Vec_PtrFree( vNodes );
00845 }
00846 
00850 
00851