diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 08:01:00 -0800 |
commit | 4d30a1e4f1edecff86d5066ce4653a370e59e5e1 (patch) | |
tree | 366355938a4af0a92f848841ac65374f338d691b /src/aig/fra/fraMan.c | |
parent | 6537f941887b06e588d3acfc97b5fdf48875cc4e (diff) | |
download | abc-4d30a1e4f1edecff86d5066ce4653a370e59e5e1.tar.gz abc-4d30a1e4f1edecff86d5066ce4653a370e59e5e1.tar.bz2 abc-4d30a1e4f1edecff86d5066ce4653a370e59e5e1.zip |
Version abc80130
Diffstat (limited to 'src/aig/fra/fraMan.c')
-rw-r--r-- | src/aig/fra/fraMan.c | 304 |
1 files changed, 0 insertions, 304 deletions
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c deleted file mode 100644 index f505b0c2..00000000 --- a/src/aig/fra/fraMan.c +++ /dev/null @@ -1,304 +0,0 @@ -/**CFile**************************************************************** - - FileName [fraMan.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [New FRAIG package.] - - Synopsis [Starts the FRAIG manager.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 30, 2007.] - - Revision [$Id: fraMan.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "fra.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Sets the default solving parameters.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_ParamsDefault( Fra_Par_t * pPars ) -{ - memset( pPars, 0, sizeof(Fra_Par_t) ); - pPars->nSimWords = 32; // the number of words in the simulation info - pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached - pPars->fPatScores = 0; // enables simulation pattern scoring - pPars->MaxScore = 25; // max score after which resimulation is used - pPars->fDoSparse = 1; // skips sparse functions -// pPars->dActConeRatio = 0.05; // the ratio of cone to be bumped -// pPars->dActConeBumpMax = 5.0; // the largest bump of activity - pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped - pPars->dActConeBumpMax = 10.0; // the largest bump of activity - pPars->nBTLimitNode = 100; // conflict limit at a node - pPars->nBTLimitMiter = 500000; // conflict limit at an output - pPars->nFramesK = 0; // the number of timeframes to unroll - pPars->fConeBias = 1; - pPars->fRewrite = 0; -} - -/**Function************************************************************* - - Synopsis [Sets the default solving parameters.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) -{ - memset( pPars, 0, sizeof(Fra_Par_t) ); - pPars->nSimWords = 1; // the number of words in the simulation info - pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached - pPars->fPatScores = 0; // enables simulation pattern scoring - pPars->MaxScore = 25; // max score after which resimulation is used - pPars->fDoSparse = 1; // skips sparse functions - pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped - pPars->dActConeBumpMax = 10.0; // the largest bump of activity - pPars->nBTLimitNode = 10000000; // conflict limit at a node - pPars->nBTLimitMiter = 500000; // conflict limit at an output - pPars->nFramesK = 1; // the number of timeframes to unroll - pPars->fConeBias = 0; - pPars->fRewrite = 0; - pPars->fLatchCorr = 0; -} - -/**Function************************************************************* - - Synopsis [Starts the fraiging manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) -{ - Fra_Man_t * p; - Aig_Obj_t * pObj; - int i; - // allocate the fraiging manager - p = ALLOC( Fra_Man_t, 1 ); - memset( p, 0, sizeof(Fra_Man_t) ); - p->pPars = pPars; - p->pManAig = pManAig; - p->nSizeAlloc = Aig_ManObjNumMax( pManAig ); - p->nFramesAll = pPars->nFramesK + 1; - // allocate storage for sim pattern - p->nPatWords = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) ); - p->pPatWords = ALLOC( unsigned, p->nPatWords ); - p->vPiVars = Vec_PtrAlloc( 100 ); - // equivalence classes - p->pCla = Fra_ClassesStart( pManAig ); - // allocate other members - p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll ); - memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); - // set random number generator - srand( 0xABCABC ); - // set the pointer to the manager - Aig_ManForEachObj( p->pManAig, pObj, i ) - pObj->pData = p; - return p; -} - -/**Function************************************************************* - - Synopsis [Starts the fraiging manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_ManClean( Fra_Man_t * p, int nNodesMax ) -{ - int i; - // remove old arrays - for ( i = 0; i < p->nMemAlloc; i++ ) - if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 ) - Vec_PtrFree( p->pMemFanins[i] ); - // realloc for the new size - if ( p->nMemAlloc < nNodesMax ) - { - int nMemAllocNew = nNodesMax + 5000; - p->pMemFanins = REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew ); - p->pMemSatNums = REALLOC( int, p->pMemSatNums, nMemAllocNew ); - p->nMemAlloc = nMemAllocNew; - } - // prepare for the new run - memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc ); - memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc ); -} - -/**Function************************************************************* - - Synopsis [Prepares the new manager to begin fraiging.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ) -{ - Aig_Man_t * pManFraig; - Aig_Obj_t * pObj; - int i; - assert( p->pManFraig == NULL ); - // start the fraig package - pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) ); - pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName ); - pManFraig->nRegs = p->pManAig->nRegs; - pManFraig->nAsserts = p->pManAig->nAsserts; - // set the pointers to the available fraig nodes - Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) ); - Aig_ManForEachPi( p->pManAig, pObj, i ) - Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) ); - // set the pointers to the manager - Aig_ManForEachObj( pManFraig, pObj, i ) - pObj->pData = p; - // allocate memory for mapping FRAIG nodes into SAT numbers and fanins - p->nMemAlloc = p->nSizeAlloc; - p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nMemAlloc ); - memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc ); - p->pMemSatNums = ALLOC( int, p->nMemAlloc ); - memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc ); - // make sure the satisfying assignment is node assigned - assert( pManFraig->pData == NULL ); - return pManFraig; -} - -/**Function************************************************************* - - Synopsis [Finalizes the combinational miter after fraiging.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_ManFinalizeComb( Fra_Man_t * p ) -{ - Aig_Obj_t * pObj; - int i; - // add the POs - Aig_ManForEachPo( p->pManAig, pObj, i ) - Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj,0) ); - // postprocess - Aig_ManCleanMarkB( p->pManFraig ); -} - - -/**Function************************************************************* - - Synopsis [Stops the fraiging manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_ManStop( Fra_Man_t * p ) -{ - if ( p->pPars->fVerbose ) - Fra_ManPrint( p ); - // save mapping from original nodes into FRAIG nodes - if ( p->pManAig ) - { - if ( p->pManAig->pObjCopies ) - free( p->pManAig->pObjCopies ); - p->pManAig->pObjCopies = p->pMemFraig; - p->pMemFraig = NULL; - } - Fra_ManClean( p, 0 ); - if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts ); - if ( p->vPiVars ) Vec_PtrFree( p->vPiVars ); - if ( p->pSat ) sat_solver_delete( p->pSat ); - if ( p->pCla ) Fra_ClassesStop( p->pCla ); - if ( p->pSml ) Fra_SmlStop( p->pSml ); - if ( p->vCex ) Vec_IntFree( p->vCex ); - FREE( p->pMemFraig ); - FREE( p->pMemFanins ); - FREE( p->pMemSatNums ); - FREE( p->pPatWords ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Prints stats for the fraiging manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_ManPrint( Fra_Man_t * p ) -{ - double nMemory = 1.0*Aig_ManObjNumMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20); - printf( "SimWord = %d. Round = %d. Mem = %0.2f Mb. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n", - p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) ); - printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n", - p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) ); - printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", - p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), - p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) ); - if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat ); - PRT( "AIG simulation ", p->pSml->timeSim ); - PRT( "AIG traversal ", p->timeTrav ); - if ( p->timeRwr ) - { - PRT( "AIG rewriting ", p->timeRwr ); - } - PRT( "SAT solving ", p->timeSat ); - PRT( " Unsat ", p->timeSatUnsat ); - PRT( " Sat ", p->timeSatSat ); - PRT( " Fail ", p->timeSatFail ); - PRT( "Class refining ", p->timeRef ); - PRT( "TOTAL RUNTIME ", p->timeTotal ); - if ( p->time1 ) { PRT( "time1 ", p->time1 ); } - if ( p->nSpeculs ) - printf( "Speculations = %d.\n", p->nSpeculs ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |