diff options
Diffstat (limited to 'src/aig/ssw/sswCore.c')
-rw-r--r-- | src/aig/ssw/sswCore.c | 119 |
1 files changed, 69 insertions, 50 deletions
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index b03a248e..8e3ab01a 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -66,65 +66,24 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) +Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) { Aig_Man_t * pAigNew; - Ssw_Man_t * p; - int RetValue, nIter, clk, clkTotal = clock(); - // reset random numbers - Aig_ManRandom( 1 ); - - // consider the case of empty AIG - if ( Aig_ManNodeNum(pAig) == 0 ) - { - pPars->nIters = 0; - // Ntl_ManFinalize() needs the following to satisfy an assertion - Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) ); - return Aig_ManDupOrdered(pAig); - } - - // check and update parameters - assert( Aig_ManRegNum(pAig) > 0 ); - assert( pPars->nFramesK > 0 ); - if ( pPars->nFramesK > 1 ) - pPars->fSkipCheck = 0; - - // perform partitioning - if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig)) - || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) ) - return Ssw_SignalCorrespondencePart( pAig, pPars ); - - // start the choicing manager - p = Ssw_ManCreate( pAig, pPars ); - // compute candidate equivalence classes -// p->pPars->nConstrs = 1; - if ( p->pPars->nConstrs == 0 ) - { - // perform one round of seq simulation and generate candidate equivalence classes - p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose ); - p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); - Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual ); - } - else - { - // create trivial equivalence classes with all nodes being candidates for constant 1 - p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); - Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex ); - } - + int RetValue, nIter; + int clk, clkTotal = clock(); // get the starting stats p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses ); - p->nNodesBeg = Aig_ManNodeNum(pAig); - p->nRegsBeg = Aig_ManRegNum(pAig); + p->nNodesBeg = Aig_ManNodeNum(p->pAig); + p->nRegsBeg = Aig_ManRegNum(p->pAig); // refine classes using BMC - if ( pPars->fVerbose ) + if ( p->pPars->fVerbose ) { printf( "Before BMC: " ); Ssw_ClassesPrint( p->ppClasses, 0 ); } Ssw_ManSweepBmc( p ); Ssw_ManCleanup( p ); - if ( pPars->fVerbose ) + if ( p->pPars->fVerbose ) { printf( "After BMC: " ); Ssw_ClassesPrint( p->ppClasses, 0 ); @@ -134,7 +93,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) { clk = clock(); RetValue = Ssw_ManSweep( p ); - if ( pPars->fVerbose ) + if ( p->pPars->fVerbose ) { printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), @@ -150,12 +109,72 @@ clk = clock(); } p->pPars->nIters = nIter + 1; p->timeTotal = clock() - clkTotal; - pAigNew = Aig_ManDupRepr( pAig, 0 ); + pAigNew = Aig_ManDupRepr( p->pAig, 0 ); Aig_ManSeqCleanup( pAigNew ); // get the final stats p->nLitsEnd = Ssw_ClassesLitNum( p->ppClasses ); p->nNodesEnd = Aig_ManNodeNum(pAigNew); p->nRegsEnd = Aig_ManRegNum(pAigNew); + return pAigNew; +} + +/**Function************************************************************* + + Synopsis [Performs computation of signal correspondence with constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) +{ + Ssw_Pars_t Pars; + Aig_Man_t * pAigNew; + Ssw_Man_t * p; + // reset random numbers + Aig_ManRandom( 1 ); + // if parameters are not given, create them + if ( pPars == NULL ) + Ssw_ManSetDefaultParams( pPars = &Pars ); + // consider the case of empty AIG + if ( Aig_ManNodeNum(pAig) == 0 ) + { + pPars->nIters = 0; + // Ntl_ManFinalize() needs the following to satisfy an assertion + Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) ); + return Aig_ManDupOrdered(pAig); + } + // check and update parameters + assert( Aig_ManRegNum(pAig) > 0 ); + assert( pPars->nFramesK > 0 ); + if ( pPars->nFramesK > 1 ) + pPars->fSkipCheck = 0; + // perform partitioning + if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig)) + || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) ) + return Ssw_SignalCorrespondencePart( pAig, pPars ); + // start the induction manager + p = Ssw_ManCreate( pAig, pPars ); + // compute candidate equivalence classes +// p->pPars->nConstrs = 1; + if ( p->pPars->nConstrs == 0 ) + { + // perform one round of seq simulation and generate candidate equivalence classes + p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose ); + p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); + Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual ); + } + else + { + // create trivial equivalence classes with all nodes being candidates for constant 1 + p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); + Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex ); + } + // perform refinement of classes + pAigNew = Ssw_SignalCorrespondenceRefine( p ); // cleanup Ssw_ManStop( p ); return pAigNew; |