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

00001 
00021 #include "abc.h"
00022 
00026 
00030 
00042 void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort )
00043 {
00044     Abc_Ntk_t * pNtk, * pNtkTemp;
00045 
00046     pNtk = *ppNtk;
00047 
00048     Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00049     Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
00050     pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
00051     Abc_NtkDelete( pNtkTemp );
00052 
00053     if ( fMoreEffort )
00054     {
00055         Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00056         Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
00057         pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
00058         Abc_NtkDelete( pNtkTemp );
00059     }
00060 
00061     *ppNtk = pNtk;
00062 }
00063 
00075 int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int fUniv, int iVar, int fVerbose )
00076 {
00077     Vec_Ptr_t * vNodes;
00078     Abc_Obj_t * pObj, * pNext, * pFanin;
00079     int i;
00080     assert( Abc_NtkIsStrash(pNtk) );
00081     assert( iVar < Abc_NtkCiNum(pNtk) );
00082 
00083     // collect the internal nodes
00084     pObj = Abc_NtkCi( pNtk, iVar );
00085     vNodes = Abc_NtkDfsReverseNodes( pNtk, &pObj, 1 );
00086 
00087     // assign the cofactors of the CI node to be constants
00088     pObj->pCopy = Abc_ObjNot( Abc_AigConst1(pNtk) ); 
00089     pObj->pData = Abc_AigConst1(pNtk); 
00090 
00091     // quantify the nodes
00092     Vec_PtrForEachEntry( vNodes, pObj, i )
00093     {
00094         for ( pNext = pObj? pObj->pCopy : pObj; pObj; pObj = pNext, pNext = pObj? pObj->pCopy : pObj )
00095         {
00096             pFanin = Abc_ObjFanin0(pObj);
00097             if ( !Abc_NodeIsTravIdCurrent(pFanin) )
00098                 pFanin->pCopy = pFanin->pData = pFanin;
00099             pFanin = Abc_ObjFanin1(pObj);
00100             if ( !Abc_NodeIsTravIdCurrent(pFanin) )
00101                 pFanin->pCopy = pFanin->pData = pFanin;
00102             pObj->pCopy = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
00103             pObj->pData = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Data(pObj), Abc_ObjChild1Data(pObj) );
00104         }
00105     }
00106     Vec_PtrFree( vNodes );
00107 
00108     // update the affected COs
00109     Abc_NtkForEachCo( pNtk, pObj, i )
00110     {
00111         if ( !Abc_NodeIsTravIdCurrent(pObj) )
00112             continue;
00113         pFanin = Abc_ObjFanin0(pObj);
00114         // get the result of quantification
00115         if ( fUniv )
00116             pNext = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
00117         else
00118             pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
00119         pNext = Abc_ObjNotCond( pNext, Abc_ObjFaninC0(pObj) );
00120         if ( Abc_ObjRegular(pNext) == pFanin )
00121             continue;
00122         // update the fanins of the CO
00123         Abc_ObjPatchFanin( pObj, pFanin, pNext );
00124 //        if ( Abc_ObjFanoutNum(pFanin) == 0 )
00125 //            Abc_AigDeleteNode( pNtk->pManFunc, pFanin );
00126     }
00127 
00128     // make sure the node has no fanouts
00129 //    pObj = Abc_NtkCi( pNtk, iVar );
00130 //    assert( Abc_ObjFanoutNum(pObj) == 0 );
00131     return 1;
00132 }
00133 
00145 Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
00146 {
00147     char Buffer[1000];
00148     Vec_Ptr_t * vPairs;
00149     Abc_Ntk_t * pNtkNew;
00150     Abc_Obj_t * pObj, * pMiter;
00151     int i, nLatches;
00152     int fSynthesis = 1;
00153 
00154     assert( Abc_NtkIsStrash(pNtk) );
00155     assert( Abc_NtkLatchNum(pNtk) );
00156     nLatches = Abc_NtkLatchNum(pNtk);
00157     // start the network
00158     pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
00159     // duplicate the name and the spec
00160     sprintf( Buffer, "%s_TR", pNtk->pName );
00161     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
00162 //    pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
00163     Abc_NtkCleanCopy( pNtk );
00164     // create current state variables
00165     Abc_NtkForEachLatchOutput( pNtk, pObj, i )
00166     {
00167         pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
00168         Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
00169     }
00170     // create next state variables
00171     Abc_NtkForEachLatchInput( pNtk, pObj, i )
00172         Abc_ObjAssignName( Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj), NULL );
00173     // create PI variables
00174     Abc_NtkForEachPi( pNtk, pObj, i )
00175         Abc_NtkDupObj( pNtkNew, pObj, 1 );
00176     // create the PO
00177     Abc_NtkCreatePo( pNtkNew );
00178     // restrash the nodes (assuming a topological order of the old network)
00179     Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
00180     Abc_NtkForEachNode( pNtk, pObj, i )
00181         pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
00182     // create the function of the primary output
00183     assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
00184     vPairs = Vec_PtrAlloc( 2*nLatches );
00185     Abc_NtkForEachLatchInput( pNtk, pObj, i )
00186     {
00187         Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pObj) );
00188         Vec_PtrPush( vPairs, Abc_NtkPi(pNtkNew, i+nLatches) );
00189     }
00190     pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs );
00191     Vec_PtrFree( vPairs );
00192     // add the primary output
00193     Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), Abc_ObjNot(pMiter) );
00194     Abc_ObjAssignName( Abc_NtkPo(pNtkNew,0), "rel", NULL );
00195 
00196     // quantify inputs
00197     if ( fInputs )
00198     {
00199         assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) + 2*nLatches );
00200         for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
00201 //        for ( i = 2*nLatches; i < Abc_NtkPiNum(pNtkNew); i++ )
00202         {
00203             Abc_NtkQuantify( pNtkNew, 0, i, fVerbose );
00204 //            if ( fSynthesis && (i % 3 == 2) )
00205             if ( fSynthesis  )
00206             {
00207                 Abc_NtkCleanData( pNtkNew );
00208                 Abc_AigCleanup( pNtkNew->pManFunc );
00209                 Abc_NtkSynthesize( &pNtkNew, 1 );
00210             }
00211 //            printf( "Var = %3d. Nodes = %6d. ", Abc_NtkPiNum(pNtkNew) - 1 - i, Abc_NtkNodeNum(pNtkNew) );
00212 //            printf( "Var = %3d. Nodes = %6d. ", i - 2*nLatches, Abc_NtkNodeNum(pNtkNew) );
00213         }
00214 //        printf( "\n" );
00215         Abc_NtkCleanData( pNtkNew );
00216         Abc_AigCleanup( pNtkNew->pManFunc );
00217         for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
00218         {
00219             pObj = Abc_NtkPi( pNtkNew, i );
00220             assert( Abc_ObjFanoutNum(pObj) == 0 );
00221             Abc_NtkDeleteObj( pObj );
00222         }
00223     }
00224 
00225     // check consistency of the network
00226     if ( !Abc_NtkCheck( pNtkNew ) )
00227     {
00228         printf( "Abc_NtkTransRel: The network check has failed.\n" );
00229         Abc_NtkDelete( pNtkNew );
00230         return NULL;
00231     }
00232     return pNtkNew;
00233 }
00234 
00235 
00247 Abc_Ntk_t * Abc_NtkInitialState( Abc_Ntk_t * pNtk )
00248 {
00249     Abc_Ntk_t * pNtkNew;
00250     Abc_Obj_t * pMiter;
00251     int i, nVars = Abc_NtkPiNum(pNtk)/2;
00252     assert( Abc_NtkIsStrash(pNtk) );
00253     // start the new network 
00254     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
00255     // compute the all-zero state in terms of the CS variables
00256     pMiter = Abc_AigConst1(pNtkNew);
00257     for ( i = 0; i < nVars; i++ )
00258         pMiter = Abc_AigAnd( pNtkNew->pManFunc, pMiter, Abc_ObjNot( Abc_NtkPi(pNtkNew, i) ) );
00259     // add the PO
00260     Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter );
00261     return pNtkNew;
00262 }
00263 
00275 Abc_Ntk_t * Abc_NtkSwapVariables( Abc_Ntk_t * pNtk )
00276 {
00277     Abc_Ntk_t * pNtkNew;
00278     Abc_Obj_t * pMiter, * pObj, * pObj0, * pObj1;
00279     int i, nVars = Abc_NtkPiNum(pNtk)/2;
00280     assert( Abc_NtkIsStrash(pNtk) );
00281     // start the new network 
00282     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
00283     // update the PIs
00284     for ( i = 0; i < nVars; i++ )
00285     {
00286         pObj0 = Abc_NtkPi( pNtk, i );
00287         pObj1 = Abc_NtkPi( pNtk, i+nVars );
00288         pMiter = pObj0->pCopy;
00289         pObj0->pCopy = pObj1->pCopy;
00290         pObj1->pCopy = pMiter;
00291     }
00292     // restrash
00293     Abc_NtkForEachNode( pNtk, pObj, i )
00294         pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
00295     // add the PO
00296     pMiter = Abc_ObjChild0Copy( Abc_NtkPo(pNtk,0) );
00297     Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter );
00298     return pNtkNew;
00299 }
00300 
00312 Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
00313 {
00314     Abc_Obj_t * pObj;
00315     Abc_Ntk_t * pNtkFront, * pNtkReached, * pNtkNext, * pNtkTemp;
00316     int clk, i, v, nVars, nNodesOld, nNodesNew, nNodesPrev;
00317     int fFixedPoint = 0;
00318     int fSynthesis  = 1;
00319     int fMoreEffort = 1;
00320 
00321     assert( Abc_NtkIsStrash(pNtkRel) );
00322     assert( Abc_NtkLatchNum(pNtkRel) == 0 );
00323     assert( Abc_NtkPiNum(pNtkRel) % 2 == 0 );
00324 
00325     // compute the network composed of the initial states
00326     pNtkFront = Abc_NtkInitialState( pNtkRel );
00327     pNtkReached = Abc_NtkDup( pNtkFront );
00328 //Abc_NtkShow( pNtkReached, 0, 0, 0 );
00329 
00330 //    if ( fVerbose )
00331 //        printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) );
00332 
00333     // perform iterations of reachability analysis
00334     nNodesPrev = Abc_NtkNodeNum(pNtkFront);
00335     nVars = Abc_NtkPiNum(pNtkRel)/2;
00336     for ( i = 0; i < nIters; i++ )
00337     {
00338         clk = clock();
00339         // get the set of next states
00340         pNtkNext = Abc_NtkMiterAnd( pNtkRel, pNtkFront, 0, 0 );
00341         Abc_NtkDelete( pNtkFront );
00342         // quantify the current state variables
00343         for ( v = 0; v < nVars; v++ )
00344         {
00345             Abc_NtkQuantify( pNtkNext, 0, v, fVerbose );
00346             if ( fSynthesis && (v % 3 == 2) )
00347             {
00348                 Abc_NtkCleanData( pNtkNext );
00349                 Abc_AigCleanup( pNtkNext->pManFunc );
00350                 Abc_NtkSynthesize( &pNtkNext, fMoreEffort );
00351             }
00352         }
00353         Abc_NtkCleanData( pNtkNext );
00354         Abc_AigCleanup( pNtkNext->pManFunc );
00355         if ( fSynthesis )
00356             Abc_NtkSynthesize( &pNtkNext, 1 );
00357         // map the next states into the current states
00358         pNtkNext = Abc_NtkSwapVariables( pNtkTemp = pNtkNext );
00359         Abc_NtkDelete( pNtkTemp );
00360         // check the termination condition
00361         if ( Abc_ObjFanin0(Abc_NtkPo(pNtkNext,0)) == Abc_AigConst1(pNtkNext) )
00362         {
00363             fFixedPoint = 1;
00364             printf( "Fixed point is reached!\n" );
00365             Abc_NtkDelete( pNtkNext );
00366             break;
00367         }
00368         // compute new front
00369         pNtkFront = Abc_NtkMiterAnd( pNtkNext, pNtkReached, 0, 1 );
00370         Abc_NtkDelete( pNtkNext );
00371         // add the reached states
00372         pNtkReached = Abc_NtkMiterAnd( pNtkTemp = pNtkReached, pNtkFront, 1, 0 );
00373         Abc_NtkDelete( pNtkTemp );
00374         // compress the size of Front
00375         nNodesOld = Abc_NtkNodeNum(pNtkFront);
00376         if ( fSynthesis )
00377         {
00378             Abc_NtkSynthesize( &pNtkFront, fMoreEffort );
00379             Abc_NtkSynthesize( &pNtkReached, fMoreEffort );
00380         }
00381         nNodesNew = Abc_NtkNodeNum(pNtkFront);
00382         // print statistics
00383         if ( fVerbose )
00384         {
00385             printf( "I = %3d : Reach = %6d  Fr = %6d  FrM = %6d  %7.2f %%   ", 
00386                 i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesPrev );
00387             PRT( "T", clock() - clk );
00388         }
00389         nNodesPrev = Abc_NtkNodeNum(pNtkFront);
00390     }
00391     if ( !fFixedPoint )
00392         fprintf( stdout, "Reachability analysis stopped after %d iterations.\n", nIters );
00393 
00394     // complement the output to represent the set of unreachable states
00395     Abc_ObjXorFaninC( Abc_NtkPo(pNtkReached,0), 0 );
00396 
00397     // remove next state variables
00398     for ( i = 2*nVars - 1; i >= nVars; i-- )
00399     {
00400         pObj = Abc_NtkPi( pNtkReached, i );
00401         assert( Abc_ObjFanoutNum(pObj) == 0 );
00402         Abc_NtkDeleteObj( pObj );
00403     }
00404 
00405     // check consistency of the network
00406     if ( !Abc_NtkCheck( pNtkReached ) )
00407     {
00408         printf( "Abc_NtkReachability: The network check has failed.\n" );
00409         Abc_NtkDelete( pNtkReached );
00410         return NULL;
00411     }
00412     return pNtkReached;
00413 }
00414 
00418 
00419