abc70930: src/base/abci/abcMiter.c Source File

00001 
00021 #include "abc.h"
00022 
00026 
00027 static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize );
00028 static void        Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize );
00029 static void        Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter );
00030 static void        Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize );
00031 static void        Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame );
00032 
00033 // to be exported 
00034 typedef void (*AddFrameMapping)( Abc_Obj_t*, Abc_Obj_t*, int, void*);
00035 extern Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg );
00036 static void        Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg );
00037 
00041 
00053 Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize )
00054 {
00055     Abc_Ntk_t * pTemp = NULL;
00056     int fRemove1, fRemove2;
00057     assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) );
00058     assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) );
00059     // check that the networks have the same PIs/POs/latches
00060     if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 0, fComb ) )
00061         return NULL;
00062     // make sure the circuits are strashed 
00063     fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0));
00064     fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0));
00065     if ( pNtk1 && pNtk2 )
00066         pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb, nPartSize );
00067     if ( fRemove1 )  Abc_NtkDelete( pNtk1 );
00068     if ( fRemove2 )  Abc_NtkDelete( pNtk2 );
00069     return pTemp;
00070 }
00071 
00083 Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize )
00084 {
00085     char Buffer[1000];
00086     Abc_Ntk_t * pNtkMiter;
00087 
00088     assert( Abc_NtkIsStrash(pNtk1) );
00089     assert( Abc_NtkIsStrash(pNtk2) );
00090 
00091     // start the new network
00092     pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
00093     sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
00094     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
00095 
00096     // perform strashing
00097     Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
00098     Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
00099     Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
00100     Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
00101     Abc_AigCleanup(pNtkMiter->pManFunc);
00102 
00103     // make sure that everything is okay
00104     if ( !Abc_NtkCheck( pNtkMiter ) )
00105     {
00106         printf( "Abc_NtkMiter: The network check has failed.\n" );
00107         Abc_NtkDelete( pNtkMiter );
00108         return NULL;
00109     }
00110     return pNtkMiter;
00111 }
00112 
00124 void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize )
00125 {
00126     Abc_Obj_t * pObj, * pObjNew;
00127     int i;
00128     // clean the copy field in all objects
00129 //    Abc_NtkCleanCopy( pNtk1 );
00130 //    Abc_NtkCleanCopy( pNtk2 );
00131     Abc_AigConst1(pNtk1)->pCopy = Abc_AigConst1(pNtkMiter);
00132     Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtkMiter);
00133 
00134     if ( fComb )
00135     {
00136         // create new PIs and remember them in the old PIs
00137         Abc_NtkForEachCi( pNtk1, pObj, i )
00138         {
00139             pObjNew = Abc_NtkCreatePi( pNtkMiter );
00140             // remember this PI in the old PIs
00141             pObj->pCopy = pObjNew;
00142             pObj = Abc_NtkCi(pNtk2, i);  
00143             pObj->pCopy = pObjNew;
00144             // add name
00145             Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
00146         }
00147         if ( nPartSize <= 0 )
00148         {
00149             // create the only PO
00150             pObjNew = Abc_NtkCreatePo( pNtkMiter );
00151             // add the PO name
00152             Abc_ObjAssignName( pObjNew, "miter", NULL );
00153         }
00154     }
00155     else
00156     {
00157         // create new PIs and remember them in the old PIs
00158         Abc_NtkForEachPi( pNtk1, pObj, i )
00159         {
00160             pObjNew = Abc_NtkCreatePi( pNtkMiter );
00161             // remember this PI in the old PIs
00162             pObj->pCopy = pObjNew;
00163             pObj = Abc_NtkPi(pNtk2, i);  
00164             pObj->pCopy = pObjNew;
00165             // add name
00166             Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
00167         }
00168         if ( nPartSize <= 0 )
00169         {
00170             // create the only PO
00171             pObjNew = Abc_NtkCreatePo( pNtkMiter );
00172             // add the PO name
00173             Abc_ObjAssignName( pObjNew, "miter", NULL );
00174         }
00175         // create the latches
00176         Abc_NtkForEachLatch( pNtk1, pObj, i )
00177         {
00178             pObjNew = Abc_NtkDupBox( pNtkMiter, pObj, 0 );
00179             // add names
00180             Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), "_1" );
00181             Abc_ObjAssignName( Abc_ObjFanin0(pObjNew),  Abc_ObjName(Abc_ObjFanin0(pObj)), "_1" );
00182             Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pObj)), "_1" );
00183         }
00184         Abc_NtkForEachLatch( pNtk2, pObj, i )
00185         {
00186             pObjNew = Abc_NtkDupBox( pNtkMiter, pObj, 0 );
00187             // add name
00188             Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), "_2" );
00189             Abc_ObjAssignName( Abc_ObjFanin0(pObjNew),  Abc_ObjName(Abc_ObjFanin0(pObj)), "_2" );
00190             Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pObj)), "_2" );
00191         }
00192     }
00193 }
00194 
00206 void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter )
00207 {
00208     Abc_Obj_t * pNode;
00209     int i;
00210     assert( Abc_NtkIsDfsOrdered(pNtk) );
00211     Abc_AigForEachAnd( pNtk, pNode, i )
00212         pNode->pCopy = Abc_AigAnd( pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
00213 }
00214 
00226 void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pRoot )
00227 {
00228     Vec_Ptr_t * vNodes;
00229     Abc_Obj_t * pNode;
00230     int i;
00231     // map the constant nodes
00232     Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkMiter);
00233     // perform strashing
00234     vNodes = Abc_NtkDfsNodes( pNtk, &pRoot, 1 );
00235     Vec_PtrForEachEntry( vNodes, pNode, i )
00236         if ( Abc_AigNodeIsAnd(pNode) )
00237             pNode->pCopy = Abc_AigAnd( pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
00238     Vec_PtrFree( vNodes );
00239 }
00240 
00241 
00253 void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize )
00254 {
00255     Vec_Ptr_t * vPairs;
00256     Abc_Obj_t * pMiter, * pNode;
00257     int i;
00258     // collect the PO pairs from both networks
00259     vPairs = Vec_PtrAlloc( 100 );
00260     if ( fComb )
00261     {
00262         // collect the CO nodes for the miter
00263         Abc_NtkForEachCo( pNtk1, pNode, i )
00264         {
00265             Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
00266             pNode = Abc_NtkCo( pNtk2, i );
00267             Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
00268         }
00269     }
00270     else
00271     {
00272         // collect the PO nodes for the miter
00273         Abc_NtkForEachPo( pNtk1, pNode, i )
00274         {
00275             Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
00276             pNode = Abc_NtkPo( pNtk2, i );
00277             Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
00278         }
00279         // connect new latches
00280         Abc_NtkForEachLatch( pNtk1, pNode, i )
00281             Abc_ObjAddFanin( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjChild0Copy(Abc_ObjFanin0(pNode)) );
00282         Abc_NtkForEachLatch( pNtk2, pNode, i )
00283             Abc_ObjAddFanin( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjChild0Copy(Abc_ObjFanin0(pNode)) );
00284     }
00285     // add the miter
00286     if ( nPartSize <= 0 )
00287     {
00288         pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs );
00289         Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
00290         Vec_PtrFree( vPairs );
00291     }
00292     else
00293     {
00294         char Buffer[1024];
00295         Vec_Ptr_t * vPairsPart;
00296         int nParts, i, k, iCur;
00297         assert( Vec_PtrSize(vPairs) == 2 * Abc_NtkCoNum(pNtk1) );
00298         // create partitions
00299         nParts = Abc_NtkCoNum(pNtk1) / nPartSize + (int)((Abc_NtkCoNum(pNtk1) % nPartSize) > 0);
00300         vPairsPart = Vec_PtrAlloc( nPartSize );
00301         for ( i = 0; i < nParts; i++ )
00302         {
00303             Vec_PtrClear( vPairsPart );
00304             for ( k = 0; k < nPartSize; k++ )
00305             {
00306                 iCur = i * nPartSize + k;
00307                 if ( iCur >= Abc_NtkCoNum(pNtk1) )
00308                     break;
00309                 Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur  ) );
00310                 Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur+1) );
00311             }
00312             pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairsPart );
00313             pNode = Abc_NtkCreatePo( pNtkMiter );
00314             Abc_ObjAddFanin( pNode, pMiter );
00315             // assign the name to the node
00316             if ( nPartSize == 1 )
00317                 sprintf( Buffer, "%s", Abc_ObjName(Abc_NtkCo(pNtk1,i)) );
00318             else
00319                 sprintf( Buffer, "%d", i );
00320             Abc_ObjAssignName( pNode, "miter_", Buffer );
00321         }
00322         Vec_PtrFree( vPairsPart );
00323         Vec_PtrFree( vPairs );
00324     }
00325 }
00326 
00327 
00328 
00340 Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 )
00341 {
00342     char Buffer[1000];
00343     Abc_Ntk_t * pNtkMiter;
00344     Abc_Obj_t * pOutput1, * pOutput2;
00345     Abc_Obj_t * pRoot1, * pRoot2, * pMiter;
00346 
00347     assert( Abc_NtkIsStrash(pNtk1) );
00348     assert( Abc_NtkIsStrash(pNtk2) );
00349     assert( 1 == Abc_NtkCoNum(pNtk1) );
00350     assert( 1 == Abc_NtkCoNum(pNtk2) );
00351     assert( 0 == Abc_NtkLatchNum(pNtk1) );
00352     assert( 0 == Abc_NtkLatchNum(pNtk2) );
00353     assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
00354     assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) );
00355     assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) );
00356 
00357     // start the new network
00358     pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
00359 //    sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
00360     sprintf( Buffer, "product" );
00361     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
00362 
00363     // perform strashing
00364     Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, 1, -1 );
00365     Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
00366     Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
00367 //    Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, 1 );
00368     pRoot1 = Abc_NtkPo(pNtk1,0);
00369     pRoot2 = Abc_NtkPo(pNtk2,0);
00370     pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot1)->pCopy, Abc_ObjFaninC0(pRoot1) );
00371     pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot2)->pCopy, Abc_ObjFaninC0(pRoot2) ^ fCompl2 );
00372     
00373     // create the miter of the two outputs
00374     if ( fOr )
00375         pMiter = Abc_AigOr( pNtkMiter->pManFunc, pOutput1, pOutput2 );
00376     else
00377         pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 );
00378     Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
00379 
00380     // make sure that everything is okay
00381     if ( !Abc_NtkCheck( pNtkMiter ) )
00382     {
00383         printf( "Abc_NtkMiterAnd: The network check has failed.\n" );
00384         Abc_NtkDelete( pNtkMiter );
00385         return NULL;
00386     }
00387     return pNtkMiter;
00388 }
00389 
00390 
00403 Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
00404 {
00405     char Buffer[1000];
00406     Abc_Ntk_t * pNtkMiter;
00407     Abc_Obj_t * pRoot, * pOutput1;
00408     int Value, i;
00409 
00410     assert( Abc_NtkIsStrash(pNtk) );
00411     assert( 1 == Abc_NtkCoNum(pNtk) );
00412     assert( Abc_NtkHasOnlyLatchBoxes(pNtk) );
00413 
00414     // start the new network
00415     pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
00416     sprintf( Buffer, "%s_miter", pNtk->pName );
00417     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
00418 
00419     // get the root output
00420     pRoot = Abc_NtkCo( pNtk, 0 );
00421 
00422     // perform strashing
00423     Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1, -1 );
00424     // set the first cofactor
00425     Vec_IntForEachEntry( vPiValues, Value, i )
00426     {
00427         if ( Value == -1 )
00428             continue;
00429         if ( Value == 0 )
00430         {
00431             Abc_NtkCi(pNtk, i)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) );
00432             continue;
00433         }
00434         if ( Value == 1 )
00435         {
00436             Abc_NtkCi(pNtk, i)->pCopy = Abc_AigConst1(pNtkMiter);
00437             continue;
00438         }
00439         assert( 0 );
00440     }
00441     // add the first cofactor
00442     Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
00443 
00444     // save the output
00445     pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) );
00446 
00447     // create the miter of the two outputs
00448     Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pOutput1 );
00449 
00450     // make sure that everything is okay
00451     if ( !Abc_NtkCheck( pNtkMiter ) )
00452     {
00453         printf( "Abc_NtkMiterCofactor: The network check has failed.\n" );
00454         Abc_NtkDelete( pNtkMiter );
00455         return NULL;
00456     }
00457     return pNtkMiter;
00458 }
00470 Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
00471 {
00472     char Buffer[1000];
00473     Abc_Ntk_t * pNtkMiter;
00474     Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
00475 
00476     assert( Abc_NtkIsStrash(pNtk) );
00477     assert( Out < Abc_NtkCoNum(pNtk) );
00478     assert( In1 < Abc_NtkCiNum(pNtk) );
00479     assert( In2 < Abc_NtkCiNum(pNtk) );
00480     assert( Abc_NtkHasOnlyLatchBoxes(pNtk) );
00481 
00482     // start the new network
00483     pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
00484     sprintf( Buffer, "%s_miter", Abc_ObjName(Abc_NtkCo(pNtk, Out)) );
00485     pNtkMiter->pName = Extra_UtilStrsav(Buffer);
00486 
00487     // get the root output
00488     pRoot = Abc_NtkCo( pNtk, Out );
00489 
00490     // perform strashing
00491     Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1, -1 );
00492     // set the first cofactor
00493     Abc_NtkCi(pNtk, In1)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) );
00494     if ( In2 >= 0 )
00495     Abc_NtkCi(pNtk, In2)->pCopy = Abc_AigConst1(pNtkMiter);
00496     // add the first cofactor
00497     Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
00498 
00499     // save the output
00500     pOutput1 = Abc_ObjFanin0(pRoot)->pCopy;
00501 
00502     // set the second cofactor
00503     Abc_NtkCi(pNtk, In1)->pCopy = Abc_AigConst1(pNtkMiter);
00504     if ( In2 >= 0 )
00505     Abc_NtkCi(pNtk, In2)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) );
00506     // add the second cofactor
00507     Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
00508 
00509     // save the output
00510     pOutput2 = Abc_ObjFanin0(pRoot)->pCopy;
00511 
00512     // create the miter of the two outputs
00513     pMiter = Abc_AigXor( pNtkMiter->pManFunc, pOutput1, pOutput2 );
00514     Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
00515 
00516     // make sure that everything is okay
00517     if ( !Abc_NtkCheck( pNtkMiter ) )
00518     {
00519         printf( "Abc_NtkMiter: The network check has failed.\n" );
00520         Abc_NtkDelete( pNtkMiter );
00521         return NULL;
00522     }
00523     return pNtkMiter;
00524 }
00525 
00526 
00538 Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
00539 {
00540     Abc_Ntk_t * pNtkMiter;
00541     Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
00542 
00543     assert( Abc_NtkIsStrash(pNtk) );
00544     assert( 1 == Abc_NtkCoNum(pNtk) );
00545     assert( In < Abc_NtkCiNum(pNtk) );
00546     assert( Abc_NtkHasOnlyLatchBoxes(pNtk) );
00547 
00548     // start the new network
00549     pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
00550     pNtkMiter->pName = Extra_UtilStrsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) );
00551 
00552     // get the root output
00553     pRoot = Abc_NtkCo( pNtk, 0 );
00554 
00555     // perform strashing
00556     Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1, -1 );
00557     // set the first cofactor
00558     Abc_NtkCi(pNtk, In)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) );
00559     // add the first cofactor
00560     Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
00561     // save the output
00562 //    pOutput1 = Abc_ObjFanin0(pRoot)->pCopy;
00563     pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) );
00564 
00565     // set the second cofactor
00566     Abc_NtkCi(pNtk, In)->pCopy = Abc_AigConst1(pNtkMiter);
00567     // add the second cofactor
00568     Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
00569     // save the output
00570 //    pOutput2 = Abc_ObjFanin0(pRoot)->pCopy;
00571     pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) );
00572 
00573     // create the miter of the two outputs
00574     if ( fExist ) 
00575         pMiter = Abc_AigOr( pNtkMiter->pManFunc, pOutput1, pOutput2 );
00576     else
00577         pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 );
00578     Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
00579 
00580     // make sure that everything is okay
00581     if ( !Abc_NtkCheck( pNtkMiter ) )
00582     {
00583         printf( "Abc_NtkMiter: The network check has failed.\n" );
00584         Abc_NtkDelete( pNtkMiter );
00585         return NULL;
00586     }
00587     return pNtkMiter;
00588 }
00589 
00601 Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk )
00602 {
00603     Abc_Ntk_t * pNtkTemp;
00604     Abc_Obj_t * pObj;
00605     int i;
00606     assert( Abc_NtkHasOnlyLatchBoxes(pNtk) );
00607 
00608     Abc_NtkForEachPi( pNtk, pObj, i )
00609     {
00610         if ( Abc_ObjFanoutNum(pObj) == 0 )
00611             continue;
00612         pNtk = Abc_NtkMiterQuantify( pNtkTemp = pNtk, i, 1 );
00613         Abc_NtkDelete( pNtkTemp );
00614     }
00615 
00616     return pNtk;
00617 }
00618 
00619 
00620 
00621 
00635 int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter )
00636 {
00637     Abc_Obj_t * pNodePo, * pChild;
00638     int i;
00639     assert( Abc_NtkIsStrash(pMiter) );
00640     Abc_NtkForEachPo( pMiter, pNodePo, i )
00641     {
00642         pChild = Abc_ObjChild0( pNodePo );
00643         if ( Abc_AigNodeIsConst(pChild) )
00644         {
00645             assert( Abc_ObjRegular(pChild) == Abc_AigConst1(pMiter) );
00646             if ( !Abc_ObjIsComplement(pChild) )
00647             {
00648                 // if the miter is constant 1, return immediately
00649 //                printf( "MITER IS CONSTANT 1!\n" );
00650                 return 0;
00651             }
00652         }
00653         // if the miter is undecided (or satisfiable), return immediately
00654         else 
00655             return -1;
00656     }
00657     // return 1, meaning all outputs are constant zero
00658     return 1;
00659 }
00660 
00672 void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
00673 {
00674     Abc_Obj_t * pChild, * pNode;
00675     int i;
00676     if ( Abc_NtkPoNum(pMiter) == 1 )
00677     {
00678         pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,0) );
00679         if ( Abc_AigNodeIsConst(pChild) )
00680         {
00681             if ( Abc_ObjIsComplement(pChild) )
00682                 printf( "Unsatisfiable.\n" );
00683             else
00684                 printf( "Satisfiable. (Constant 1).\n" );
00685         }
00686         else
00687             printf( "Satisfiable.\n" );
00688     }
00689     else
00690     {
00691         Abc_NtkForEachPo( pMiter, pNode, i )
00692         {
00693             pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,i) );
00694             printf( "Output #%2d : ", i );
00695             if ( Abc_AigNodeIsConst(pChild) )
00696             {
00697                 if ( Abc_ObjIsComplement(pChild) )
00698                     printf( "Unsatisfiable.\n" );
00699                 else
00700                     printf( "Satisfiable. (Constant 1).\n" );
00701             }
00702             else
00703                 printf( "Satisfiable.\n" );
00704         }
00705     }
00706 }
00707 
00708 
00720 Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
00721 {
00722     char Buffer[1000];
00723     ProgressBar * pProgress;
00724     Abc_Ntk_t * pNtkFrames;
00725     Abc_Obj_t * pLatch, * pLatchOut;
00726     int i, Counter;
00727     assert( nFrames > 0 );
00728     assert( Abc_NtkIsStrash(pNtk) );
00729     assert( Abc_NtkIsDfsOrdered(pNtk) );
00730     assert( Abc_NtkHasOnlyLatchBoxes(pNtk) );
00731     // start the new network
00732     pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
00733     sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
00734     pNtkFrames->pName = Extra_UtilStrsav(Buffer);
00735     // map the constant nodes
00736     Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames);
00737     // create new latches (or their initial values) and remember them in the new latches
00738     if ( !fInitial )
00739     {
00740         Abc_NtkForEachLatch( pNtk, pLatch, i )
00741             Abc_NtkDupBox( pNtkFrames, pLatch, 1 );
00742     }
00743     else
00744     {
00745         Counter = 0;
00746         Abc_NtkForEachLatch( pNtk, pLatch, i )
00747         {
00748             pLatchOut = Abc_ObjFanout0(pLatch);
00749             if ( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI
00750             {
00751                 pLatchOut->pCopy = Abc_NtkCreatePi(pNtkFrames);
00752                 Abc_ObjAssignName( pLatchOut->pCopy, Abc_ObjName(pLatchOut), NULL );
00753                 Counter++;
00754             }
00755             else
00756                 pLatchOut->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) );
00757         }
00758         if ( Counter )
00759             printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter );
00760     }
00761     
00762     // create the timeframes
00763     pProgress = Extra_ProgressBarStart( stdout, nFrames );
00764     for ( i = 0; i < nFrames; i++ )
00765     {
00766         Extra_ProgressBarUpdate( pProgress, i, NULL );
00767         Abc_NtkAddFrame( pNtkFrames, pNtk, i );
00768     }
00769     Extra_ProgressBarStop( pProgress );
00770     
00771     // connect the new latches to the outputs of the last frame
00772     if ( !fInitial )
00773     {
00774         // we cannot use pLatch->pCopy here because pLatch->pCopy is used for temporary storage of strashed values
00775         Abc_NtkForEachLatch( pNtk, pLatch, i )
00776             Abc_ObjAddFanin( Abc_ObjFanin0(pLatch)->pCopy, Abc_ObjFanout0(pLatch)->pCopy );
00777     }
00778 
00779     // remove dangling nodes
00780     Abc_AigCleanup( pNtkFrames->pManFunc );
00781     // reorder the latches
00782     Abc_NtkOrderCisCos( pNtkFrames );
00783     // make sure that everything is okay
00784     if ( !Abc_NtkCheck( pNtkFrames ) )
00785     {
00786         printf( "Abc_NtkFrames: The network check has failed.\n" );
00787         Abc_NtkDelete( pNtkFrames );
00788         return NULL;
00789     }
00790     return pNtkFrames;
00791 }
00792 
00807 void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame )
00808 {
00809     char Buffer[10];
00810     Abc_Obj_t * pNode, * pLatch;
00811     int i;
00812     // create the prefix to be added to the node names
00813     sprintf( Buffer, "_%02d", iFrame );
00814     // add the new PI nodes
00815     Abc_NtkForEachPi( pNtk, pNode, i )
00816         Abc_ObjAssignName( Abc_NtkDupObj(pNtkFrames, pNode, 0), Abc_ObjName(pNode), Buffer );
00817     // add the internal nodes
00818     Abc_AigForEachAnd( pNtk, pNode, i )
00819         pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
00820     // add the new POs
00821     Abc_NtkForEachPo( pNtk, pNode, i )
00822     {
00823         Abc_ObjAssignName( Abc_NtkDupObj(pNtkFrames, pNode, 0), Abc_ObjName(pNode), Buffer );
00824         Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) );
00825     }
00826     // add the new asserts
00827     Abc_NtkForEachAssert( pNtk, pNode, i )
00828     {
00829         Abc_ObjAssignName( Abc_NtkDupObj(pNtkFrames, pNode, 0), Abc_ObjName(pNode), Buffer );
00830         Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) );
00831     }
00832     // transfer the implementation of the latch inputs to the latch outputs
00833     Abc_NtkForEachLatch( pNtk, pLatch, i )
00834         pLatch->pCopy = Abc_ObjChild0Copy(Abc_ObjFanin0(pLatch));
00835     Abc_NtkForEachLatch( pNtk, pLatch, i )
00836         Abc_ObjFanout0(pLatch)->pCopy = pLatch->pCopy;
00837 }
00838 
00839 
00840 
00852 Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg )
00853 {
00854 /*
00855     char Buffer[1000];
00856     ProgressBar * pProgress;
00857     Abc_Ntk_t * pNtkFrames;
00858     Vec_Ptr_t * vNodes;
00859     Abc_Obj_t * pLatch, * pLatchNew;
00860     int i, Counter;
00861     assert( nFrames > 0 );
00862     assert( Abc_NtkIsStrash(pNtk) );   
00863     // start the new network
00864     pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
00865     sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
00866     pNtkFrames->pName = Extra_UtilStrsav(Buffer);
00867     // create new latches (or their initial values) and remember them in the new latches
00868     if ( !fInitial )
00869     {
00870         Abc_NtkForEachLatch( pNtk, pLatch, i ) {
00871             Abc_NtkDupObj( pNtkFrames, pLatch );
00872             if (addFrameMapping) addFrameMapping(pLatch->pCopy, pLatch, 0, arg);
00873         }
00874     }
00875     else
00876     {
00877         Counter = 0;
00878         Abc_NtkForEachLatch( pNtk, pLatch, i )
00879         {
00880             if ( Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI
00881             {
00882                 pLatch->pCopy = Abc_NtkCreatePi(pNtkFrames);
00883                 Abc_ObjAssignName( pLatch->pCopy, Abc_ObjName(pLatch), NULL );
00884                 Counter++;
00885             }
00886             else {
00887                 pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) );
00888             }
00889  
00890             if (addFrameMapping) addFrameMapping(pLatch->pCopy, pLatch, 0, arg);
00891         }
00892         if ( Counter )
00893             printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter );
00894     }
00895     
00896     // create the timeframes
00897     vNodes = Abc_NtkDfs( pNtk, 0 );
00898     pProgress = Extra_ProgressBarStart( stdout, nFrames );
00899     for ( i = 0; i < nFrames; i++ )
00900     {
00901         Extra_ProgressBarUpdate( pProgress, i, NULL );
00902         Abc_NtkAddFrame2( pNtkFrames, pNtk, i, vNodes, addFrameMapping, arg );
00903     }
00904     Extra_ProgressBarStop( pProgress );
00905     Vec_PtrFree( vNodes );
00906     
00907     // connect the new latches to the outputs of the last frame
00908     if ( !fInitial )
00909     {
00910         Abc_NtkForEachLatch( pNtk, pLatch, i )
00911         {
00912             pLatchNew = Abc_NtkBox(pNtkFrames, i);
00913             Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
00914             Abc_ObjAssignName( pLatchNew, Abc_ObjName(pLatch), NULL );
00915         }
00916     }
00917     Abc_NtkForEachLatch( pNtk, pLatch, i )
00918         pLatch->pNext = NULL;
00919 
00920     // remove dangling nodes
00921     Abc_AigCleanup( pNtkFrames->pManFunc );
00922 
00923     // reorder the latches
00924     Abc_NtkOrderCisCos( pNtkFrames );
00925     
00926     // make sure that everything is okay
00927     if ( !Abc_NtkCheck( pNtkFrames ) )
00928     {
00929         printf( "Abc_NtkFrames: The network check has failed.\n" );
00930         Abc_NtkDelete( pNtkFrames );
00931         return NULL;
00932     }
00933     return pNtkFrames;
00934 */
00935     return NULL;
00936 }
00937 
00952 void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg )
00953 {
00954 /*
00955     char Buffer[10];
00956     Abc_Obj_t * pNode, * pNodeNew, * pLatch;
00957     Abc_Obj_t * pConst1, * pConst1New;
00958     int i;
00959     // get the constant nodes
00960     pConst1    = Abc_AigConst1(pNtk);
00961     pConst1New = Abc_AigConst1(pNtkFrames);
00962     // create the prefix to be added to the node names
00963     sprintf( Buffer, "_%02d", iFrame );
00964     // add the new PI nodes
00965     Abc_NtkForEachPi( pNtk, pNode, i )
00966     {
00967         pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode );       
00968         Abc_ObjAssignName( pNodeNew, Abc_ObjName(pNode), Buffer );
00969         if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg);
00970     }
00971     // add the internal nodes
00972     Vec_PtrForEachEntry( vNodes, pNode, i )
00973     {
00974         if ( pNode == pConst1 )
00975             pNodeNew = pConst1New;
00976         else
00977             pNodeNew = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
00978         pNode->pCopy = pNodeNew;
00979         if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg);
00980     }
00981     // add the new POs
00982     Abc_NtkForEachPo( pNtk, pNode, i )
00983     {
00984         pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode );       
00985         Abc_ObjAddFanin( pNodeNew, Abc_ObjChild0Copy(pNode) );
00986         Abc_ObjAssignName( pNodeNew, Abc_ObjName(pNode), Buffer );
00987         if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg);
00988     }
00989     // transfer the implementation of the latch drivers to the latches
00990 
00991     // it is important that these two steps are performed it two loops
00992     // and not in the same loop
00993     Abc_NtkForEachLatch( pNtk, pLatch, i ) 
00994         pLatch->pNext = Abc_ObjChild0Copy(pLatch);
00995     Abc_NtkForEachLatch( pNtk, pLatch, i ) 
00996         pLatch->pCopy = pLatch->pNext;
00997 
00998     Abc_NtkForEachLatch( pNtk, pLatch, i ) 
00999     {
01000         if (addFrameMapping) {
01001             // don't give Mike complemented pointers because he doesn't like it
01002             if (Abc_ObjIsComplement(pLatch->pCopy)) {            
01003                 pNodeNew = Abc_NtkCreateNode( pNtkFrames );
01004                 Abc_ObjAddFanin( pNodeNew, pLatch->pCopy );
01005                 assert(Abc_ObjFaninNum(pNodeNew) == 1);
01006                 pNodeNew->Level = 1 + Abc_ObjRegular(pLatch->pCopy)->Level;
01007 
01008                 pLatch->pNext = pNodeNew;
01009                 pLatch->pCopy = pNodeNew;
01010             }
01011             addFrameMapping(pLatch->pCopy, pLatch, iFrame+1, arg);
01012         }
01013     }
01014 */
01015 }
01016 
01017 
01018 
01030 int Abc_NtkDemiter( Abc_Ntk_t * pNtk )
01031 {
01032     Abc_Obj_t * pNodeC, * pNodeA, * pNodeB, * pNode;
01033     Abc_Obj_t * pPoNew;
01034     Vec_Ptr_t * vNodes1, * vNodes2;
01035     int nCommon, i;
01036 
01037     assert( Abc_NtkIsStrash(pNtk) );
01038     assert( Abc_NtkPoNum(pNtk) == 1 );
01039     if ( !Abc_NodeIsExorType(Abc_ObjFanin0(Abc_NtkPo(pNtk,0))) )
01040     {
01041         printf( "The root of the miter is not an EXOR gate.\n" );
01042         return 0;
01043     }
01044     pNodeC = Abc_NodeRecognizeMux( Abc_ObjFanin0(Abc_NtkPo(pNtk,0)), &pNodeA, &pNodeB );
01045     assert( Abc_ObjRegular(pNodeA) == Abc_ObjRegular(pNodeB) );
01046     if ( Abc_ObjFaninC0(Abc_NtkPo(pNtk,0)) )
01047     {
01048         pNodeA = Abc_ObjNot(pNodeA);
01049         pNodeB = Abc_ObjNot(pNodeB);
01050     }
01051 
01052     // add the PO corresponding to control input
01053     pPoNew = Abc_NtkCreatePo( pNtk );
01054     Abc_ObjAddFanin( pPoNew, pNodeC );
01055     Abc_ObjAssignName( pPoNew, "addOut1", NULL );
01056 
01057     // add the PO corresponding to other input
01058     pPoNew = Abc_NtkCreatePo( pNtk );
01059     Abc_ObjAddFanin( pPoNew, pNodeB );
01060     Abc_ObjAssignName( pPoNew, "addOut2", NULL );
01061 
01062     // mark the nodes in the first cone
01063     pNodeB = Abc_ObjRegular(pNodeB);
01064     vNodes1 = Abc_NtkDfsNodes( pNtk, &pNodeC, 1 );
01065     vNodes2 = Abc_NtkDfsNodes( pNtk, &pNodeB, 1 );
01066 
01067     Vec_PtrForEachEntry( vNodes1, pNode, i )
01068         pNode->fMarkA = 1;
01069     nCommon = 0;
01070     Vec_PtrForEachEntry( vNodes2, pNode, i )
01071         nCommon += pNode->fMarkA;
01072     Vec_PtrForEachEntry( vNodes1, pNode, i )
01073         pNode->fMarkA = 0;
01074 
01075     printf( "First cone = %6d.  Second cone = %6d.  Common = %6d.\n", vNodes1->nSize, vNodes2->nSize, nCommon );
01076     Vec_PtrFree( vNodes1 );
01077     Vec_PtrFree( vNodes2 );
01078 
01079     // reorder the latches
01080     Abc_NtkOrderCisCos( pNtk );
01081     // make sure that everything is okay
01082     if ( !Abc_NtkCheck( pNtk ) )
01083         printf( "Abc_NtkDemiter: The network check has failed.\n" );
01084     return 1;
01085 }
01086 
01098 int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd )
01099 {
01100     Abc_Obj_t * pNode, * pMiter;
01101     int i;
01102     assert( Abc_NtkIsStrash(pNtk) );
01103 //    assert( Abc_NtkLatchNum(pNtk) == 0 );
01104     if ( Abc_NtkPoNum(pNtk) == 1 )
01105         return 1;
01106     // start the result
01107     if ( fAnd )
01108         pMiter = Abc_AigConst1(pNtk);
01109     else
01110         pMiter = Abc_ObjNot( Abc_AigConst1(pNtk) );
01111     // perform operations on the POs
01112     Abc_NtkForEachPo( pNtk, pNode, i )
01113         if ( fAnd )
01114             pMiter = Abc_AigAnd( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
01115         else
01116             pMiter = Abc_AigOr( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
01117     // remove the POs and their names
01118     for ( i = Abc_NtkPoNum(pNtk) - 1; i >= 0; i-- )
01119         Abc_NtkDeleteObj( Abc_NtkPo(pNtk, i) );
01120     assert( Abc_NtkPoNum(pNtk) == 0 );
01121     // create the new PO
01122     pNode = Abc_NtkCreatePo( pNtk );
01123     Abc_ObjAddFanin( pNode, pMiter );
01124     Abc_ObjAssignName( pNode, "miter", NULL );
01125     // make sure that everything is okay
01126     if ( !Abc_NtkCheck( pNtk ) )
01127     {
01128         printf( "Abc_NtkOrPos: The network check has failed.\n" );
01129         return 0;
01130     }
01131     return 1;
01132 }
01133 
01137 
01138