diff options
Diffstat (limited to 'src/aig/fra/fraMan.c')
| -rw-r--r-- | src/aig/fra/fraMan.c | 304 |
1 files changed, 304 insertions, 0 deletions
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c new file mode 100644 index 00000000..f505b0c2 --- /dev/null +++ b/src/aig/fra/fraMan.c @@ -0,0 +1,304 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + + |