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

00001 
00021 #include "abc.h"
00022 #include "fraig.h"
00023 #include "math.h"
00024 
00028 
00029 extern int  Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
00030 extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
00031 
00032 static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, sint64 nInspLimit, int * pRetValue, int * pNumFails, sint64 * pNumConfs, sint64 * pNumInspects );
00033 static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose );
00034 
00035 
00039   
00054 int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
00055 {
00056     Prove_Params_t * pParams = pPars;
00057     Abc_Ntk_t * pNtk, * pNtkTemp;
00058     int RetValue, nIter, nSatFails, Counter, clk, timeStart = clock();
00059     sint64 nSatConfs, nSatInspects, nInspectLimit;
00060 
00061     // get the starting network
00062     pNtk = *ppNtk;
00063     assert( Abc_NtkIsStrash(pNtk) );
00064     assert( Abc_NtkPoNum(pNtk) == 1 );
00065  
00066     if ( pParams->fVerbose )
00067     {
00068         printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
00069             pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
00070         printf( "Mitering = %d (%3.1f).  Rewriting = %d (%3.1f).  Fraiging = %d (%3.1f).\n", 
00071             pParams->nMiteringLimitStart,  pParams->nMiteringLimitMulti, 
00072             pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
00073             pParams->nFraigingLimitStart,  pParams->nFraigingLimitMulti );
00074         printf( "Mitering last = %d.\n", 
00075             pParams->nMiteringLimitLast );
00076     }
00077 
00078     // if SAT only, solve without iteration
00079     if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
00080     {
00081         clk = clock();
00082         RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, NULL, NULL );
00083         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
00084         *ppNtk = pNtk;
00085         return RetValue;
00086     }
00087 
00088     // check the current resource limits
00089     for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
00090     {
00091         if ( pParams->fVerbose )
00092         {
00093             printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, 
00094                  (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 
00095                  (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
00096             fflush( stdout );
00097         }
00098 
00099         // try brute-force SAT
00100         clk = clock();
00101         nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
00102         RetValue = Abc_NtkMiterSat( pNtk, (sint64)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (sint64)nInspectLimit, 0, &nSatConfs, &nSatInspects );
00103         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
00104         if ( RetValue >= 0 )
00105             break;
00106 
00107         // add to the number of backtracks and inspects
00108         pParams->nTotalBacktracksMade += nSatConfs;
00109         pParams->nTotalInspectsMade   += nSatInspects;
00110         // check if global resource limit is reached
00111         if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
00112              (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
00113         {
00114             printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
00115             *ppNtk = pNtk;
00116             return -1;
00117         }
00118 
00119         // try rewriting
00120         if ( pParams->fUseRewriting )
00121         {
00122             clk = clock();
00123             Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
00124 //            Counter = 1;
00125             while ( 1 )
00126             {
00127 /*
00128                 extern Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose );
00129                 pNtk = Abc_NtkIvyResyn( pNtkTemp = pNtk, 0, 0 );  Abc_NtkDelete( pNtkTemp );
00130                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
00131                     break;
00132                 if ( --Counter == 0 )
00133                     break;
00134 */
00135 /*
00136                 Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00137                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
00138                     break;
00139                 if ( --Counter == 0 )
00140                     break;
00141 */
00142                 Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00143                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
00144                     break;
00145                 if ( --Counter == 0 )
00146                     break;
00147                 Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
00148                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
00149                     break;
00150                 if ( --Counter == 0 )
00151                     break;
00152                 pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );  Abc_NtkDelete( pNtkTemp );
00153                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
00154                     break;
00155                 if ( --Counter == 0 )
00156                     break;
00157             }
00158             Abc_NtkMiterPrint( pNtk, "Rewriting  ", clk, pParams->fVerbose );
00159         }
00160  
00161         if ( pParams->fUseFraiging )
00162         {
00163             // try FRAIGing
00164             clk = clock();
00165             nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
00166             pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), nInspectLimit, &RetValue, &nSatFails, &nSatConfs, &nSatInspects );  Abc_NtkDelete( pNtkTemp );
00167             Abc_NtkMiterPrint( pNtk, "FRAIGing   ", clk, pParams->fVerbose );
00168 //            printf( "NumFails = %d\n", nSatFails );
00169             if ( RetValue >= 0 )
00170                 break;
00171 
00172             // add to the number of backtracks and inspects
00173             pParams->nTotalBacktracksMade += nSatConfs;
00174             pParams->nTotalInspectsMade += nSatInspects;
00175             // check if global resource limit is reached
00176             if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
00177                  (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
00178             {
00179                 printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
00180                 *ppNtk = pNtk;
00181                 return -1;
00182             }
00183         }
00184 
00185     }    
00186 
00187     // try to prove it using brute force SAT
00188     if ( RetValue < 0 && pParams->fUseBdds )
00189     {
00190         if ( pParams->fVerbose )
00191         {
00192             printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
00193             fflush( stdout );
00194         }
00195         clk = clock();
00196         pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
00197         if ( pNtk )   
00198         {
00199             Abc_NtkDelete( pNtkTemp );
00200             RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) );
00201         }
00202         else 
00203             pNtk = pNtkTemp;
00204         Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose );
00205     }
00206 
00207     if ( RetValue < 0 )
00208     {
00209         if ( pParams->fVerbose )
00210         {
00211             printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
00212             fflush( stdout );
00213         }
00214         clk = clock();
00215         nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
00216         RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)nInspectLimit, 0, NULL, NULL );
00217         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
00218     }
00219 
00220     // assign the model if it was proved by rewriting (const 1 miter)
00221     if ( RetValue == 0 && pNtk->pModel == NULL )
00222     {
00223         pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) );
00224         memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) );
00225     }
00226     *ppNtk = pNtk;
00227     return RetValue;
00228 }
00229 
00241 Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, sint64 nInspLimit, int * pRetValue, int * pNumFails, sint64 * pNumConfs, sint64 * pNumInspects )
00242 {
00243     Abc_Ntk_t * pNtkNew;
00244     Fraig_Params_t Params, * pParams = &Params;
00245     Fraig_Man_t * pMan;
00246     int nWords1, nWords2, nWordsMin, RetValue;
00247     int * pModel;
00248 
00249     // to determine the number of simulation patterns
00250     // use the following strategy
00251     // at least 64 words (32 words random and 32 words dynamic)
00252     // no more than 256M for one circuit (128M + 128M)
00253     nWords1 = 32;
00254     nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk));
00255     nWordsMin = ABC_MIN( nWords1, nWords2 );
00256 
00257     // set the FRAIGing parameters
00258     Fraig_ParamsSetDefault( pParams );
00259     pParams->nPatsRand  = nWordsMin * 32; // the number of words of random simulation info
00260     pParams->nPatsDyna  = nWordsMin * 32; // the number of words of dynamic simulation info
00261     pParams->nBTLimit   = nBTLimit;       // the max number of backtracks
00262     pParams->nSeconds   = -1;             // the runtime limit
00263     pParams->fTryProve  = 0;              // do not try to prove the final miter
00264     pParams->fDoSparse  = 1;              // try proving sparse functions
00265     pParams->fVerbose   = 0;
00266     pParams->nInspLimit = nInspLimit;
00267 
00268     // transform the target into a fraig
00269     pMan = Abc_NtkToFraig( pNtk, pParams, 0, 0 ); 
00270     Fraig_ManProveMiter( pMan );
00271     RetValue = Fraig_ManCheckMiter( pMan );
00272 
00273     // create the network 
00274     pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
00275 
00276     // save model
00277     if ( RetValue == 0 )
00278     {
00279         pModel = Fraig_ManReadModel( pMan );
00280         FREE( pNtkNew->pModel );
00281         pNtkNew->pModel = ALLOC( int, Abc_NtkCiNum(pNtkNew) );
00282         memcpy( pNtkNew->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtkNew) );
00283     }
00284 
00285     // save the return values
00286     *pRetValue = RetValue;
00287     *pNumFails = Fraig_ManReadSatFails( pMan );
00288     *pNumConfs = Fraig_ManReadConflicts( pMan );
00289     *pNumInspects = Fraig_ManReadInspects( pMan );
00290 
00291     // delete the fraig manager
00292     Fraig_ManFree( pMan );
00293     return pNtkNew;
00294 }
00295 
00307 void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose )
00308 {
00309     if ( !fVerbose )
00310         return;
00311     printf( "Nodes = %7d.  Levels = %4d.  ", Abc_NtkNodeNum(pNtk), 
00312         Abc_NtkIsStrash(pNtk)? Abc_AigLevel(pNtk) : Abc_NtkLevel(pNtk) );
00313     PRT( pString, clock() - clk );
00314 }
00315 
00316   
00328 Abc_Ntk_t * Abc_NtkMiterRwsat( Abc_Ntk_t * pNtk )
00329 {
00330     Abc_Ntk_t * pNtkTemp;
00331     Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00332     pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );  Abc_NtkDelete( pNtkTemp );
00333     Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00334     Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
00335     return pNtk;
00336 }
00337 
00338 
00342 
00343