diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
commit | 4812c90424dfc40d26725244723887a2d16ddfd9 (patch) | |
tree | b32ace96e7e2d84d586e09ba605463b6f49c3271 /src/base/abci/abcProve.c | |
parent | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (diff) | |
download | abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.gz abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.bz2 abc-4812c90424dfc40d26725244723887a2d16ddfd9.zip |
Version abc71001
Diffstat (limited to 'src/base/abci/abcProve.c')
-rw-r--r-- | src/base/abci/abcProve.c | 341 |
1 files changed, 341 insertions, 0 deletions
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c new file mode 100644 index 00000000..618b6a0f --- /dev/null +++ b/src/base/abci/abcProve.c @@ -0,0 +1,341 @@ +/**CFile**************************************************************** + + FileName [abcProve.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Proves the miter using AIG rewriting, FRAIGing, and SAT solving.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "fraig.h" +#include "math.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose ); +extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); + +static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, sint64 nInspLimit, int * pRetValue, int * pNumFails, sint64 * pNumConfs, sint64 * pNumInspects ); +static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose ); + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Attempts to solve the miter using a number of tricks.] + + Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT. Returns + a simplified version of the original network (or a constant 0 network). + In case the network is not a constant zero and a SAT assignment is found, + pNtk->pModel contains a satisfying assignment.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) +{ + Prove_Params_t * pParams = pPars; + Abc_Ntk_t * pNtk, * pNtkTemp; + int RetValue, nIter, nSatFails, Counter, clk, timeStart = clock(); + sint64 nSatConfs, nSatInspects, nInspectLimit; + + // get the starting network + pNtk = *ppNtk; + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkPoNum(pNtk) == 1 ); + + if ( pParams->fVerbose ) + { + printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n", + pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" ); + printf( "Miter = %d (%3.1f). Rwr = %d (%3.1f). Fraig = %d (%3.1f). Last = %d.\n", + pParams->nMiteringLimitStart, pParams->nMiteringLimitMulti, + pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti, + pParams->nFraigingLimitStart, pParams->nFraigingLimitMulti, pParams->nMiteringLimitLast ); + } + + // if SAT only, solve without iteration + if ( !pParams->fUseRewriting && !pParams->fUseFraiging ) + { + clk = clock(); + RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, NULL, NULL ); + Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose ); + *ppNtk = pNtk; + return RetValue; + } + + // check the current resource limits + for ( nIter = 0; nIter < pParams->nItersMax; nIter++ ) + { + if ( pParams->fVerbose ) + { + printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, + (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), + (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) ); + fflush( stdout ); + } + + // try brute-force SAT + clk = clock(); + nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0; + RetValue = Abc_NtkMiterSat( pNtk, (sint64)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (sint64)nInspectLimit, 0, &nSatConfs, &nSatInspects ); + Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose ); + if ( RetValue >= 0 ) + break; + + // add to the number of backtracks and inspects + pParams->nTotalBacktracksMade += nSatConfs; + pParams->nTotalInspectsMade += nSatInspects; + // check if global resource limit is reached + if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) || + (pParams->nTotalInspectLimit && pParams->nTotalInspectsMade >= pParams->nTotalInspectLimit) ) + { + printf( "Reached global limit on conflicts/inspects. Quitting.\n" ); + *ppNtk = pNtk; + return -1; + } + + // try rewriting + if ( pParams->fUseRewriting ) + { + clk = clock(); + Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter)); +// Counter = 1; + while ( 1 ) + { +/* + extern Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose ); + pNtk = Abc_NtkIvyResyn( pNtkTemp = pNtk, 0, 0 ); Abc_NtkDelete( pNtkTemp ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + if ( --Counter == 0 ) + break; +*/ +/* + Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + if ( --Counter == 0 ) + break; +*/ + Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + if ( --Counter == 0 ) + break; + Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + if ( --Counter == 0 ) + break; + pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + if ( --Counter == 0 ) + break; + } + Abc_NtkMiterPrint( pNtk, "Rewriting ", clk, pParams->fVerbose ); + } + + if ( pParams->fUseFraiging ) + { + // try FRAIGing + clk = clock(); + nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0; + pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), nInspectLimit, &RetValue, &nSatFails, &nSatConfs, &nSatInspects ); Abc_NtkDelete( pNtkTemp ); + Abc_NtkMiterPrint( pNtk, "FRAIGing ", clk, pParams->fVerbose ); +// printf( "NumFails = %d\n", nSatFails ); + if ( RetValue >= 0 ) + break; + + // add to the number of backtracks and inspects + pParams->nTotalBacktracksMade += nSatConfs; + pParams->nTotalInspectsMade += nSatInspects; + // check if global resource limit is reached + if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) || + (pParams->nTotalInspectLimit && pParams->nTotalInspectsMade >= pParams->nTotalInspectLimit) ) + { + printf( "Reached global limit on conflicts/inspects. Quitting.\n" ); + *ppNtk = pNtk; + return -1; + } + } + + } + + // try to prove it using brute force SAT + if ( RetValue < 0 && pParams->fUseBdds ) + { + if ( pParams->fVerbose ) + { + printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit ); + fflush( stdout ); + } + clk = clock(); + pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 ); + if ( pNtk ) + { + Abc_NtkDelete( pNtkTemp ); + RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) ); + } + else + pNtk = pNtkTemp; + Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose ); + } + + if ( RetValue < 0 ) + { + if ( pParams->fVerbose ) + { + printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast ); + fflush( stdout ); + } + clk = clock(); + nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0; + RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)nInspectLimit, 0, NULL, NULL ); + Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose ); + } + + // assign the model if it was proved by rewriting (const 1 miter) + if ( RetValue == 0 && pNtk->pModel == NULL ) + { + pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) ); + memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) ); + } + *ppNtk = pNtk; + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Attempts to solve the miter using a number of tricks.] + + Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, sint64 nInspLimit, int * pRetValue, int * pNumFails, sint64 * pNumConfs, sint64 * pNumInspects ) +{ + Abc_Ntk_t * pNtkNew; + Fraig_Params_t Params, * pParams = &Params; + Fraig_Man_t * pMan; + int nWords1, nWords2, nWordsMin, RetValue; + int * pModel; + + // to determine the number of simulation patterns + // use the following strategy + // at least 64 words (32 words random and 32 words dynamic) + // no more than 256M for one circuit (128M + 128M) + nWords1 = 32; + nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk)); + nWordsMin = ABC_MIN( nWords1, nWords2 ); + + // set the FRAIGing parameters + Fraig_ParamsSetDefault( pParams ); + pParams->nPatsRand = nWordsMin * 32; // the number of words of random simulation info + pParams->nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info + pParams->nBTLimit = nBTLimit; // the max number of backtracks + pParams->nSeconds = -1; // the runtime limit + pParams->fTryProve = 0; // do not try to prove the final miter + pParams->fDoSparse = 1; // try proving sparse functions + pParams->fVerbose = 0; + pParams->nInspLimit = nInspLimit; + + // transform the target into a fraig + pMan = Abc_NtkToFraig( pNtk, pParams, 0, 0 ); + Fraig_ManProveMiter( pMan ); + RetValue = Fraig_ManCheckMiter( pMan ); + + // create the network + pNtkNew = Abc_NtkFromFraig( pMan, pNtk ); + + // save model + if ( RetValue == 0 ) + { + pModel = Fraig_ManReadModel( pMan ); + FREE( pNtkNew->pModel ); + pNtkNew->pModel = ALLOC( int, Abc_NtkCiNum(pNtkNew) ); + memcpy( pNtkNew->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtkNew) ); + } + + // save the return values + *pRetValue = RetValue; + *pNumFails = Fraig_ManReadSatFails( pMan ); + *pNumConfs = Fraig_ManReadConflicts( pMan ); + *pNumInspects = Fraig_ManReadInspects( pMan ); + + // delete the fraig manager + Fraig_ManFree( pMan ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Attempts to solve the miter using a number of tricks.] + + Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose ) +{ + if ( !fVerbose ) + return; + printf( "Nodes = %7d. Levels = %4d. ", Abc_NtkNodeNum(pNtk), + Abc_NtkIsStrash(pNtk)? Abc_AigLevel(pNtk) : Abc_NtkLevel(pNtk) ); + PRT( pString, clock() - clk ); +} + + +/**Function************************************************************* + + Synopsis [Implements resynthesis for CEC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkMiterRwsat( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkTemp; + Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); + pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp ); + Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); + Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); + return pNtk; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |