From 6130e39b18b5f53902e4eab14f6d5cdde5219563 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Nov 2010 01:35:04 -0700 Subject: initial commit of public abc --- src/aig/ssw/sswCore.c | 225 +++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 195 insertions(+), 30 deletions(-) (limited to 'src/aig/ssw/sswCore.c') diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 6cb84800..c277d76e 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -20,6 +20,9 @@ #include "sswInt.h" +ABC_NAMESPACE_IMPL_START + + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -46,16 +49,18 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) p->nOverSize = 0; // size of the overlap between partitions p->nFramesK = 1; // the induction depth p->nFramesAddSim = 2; // additional frames to simulate - p->nConstrs = 0; // treat the last nConstrs POs as seq constraints + p->fConstrs = 0; // treat the last nConstrs POs as seq constraints + p->fMergeFull = 0; // enables full merge when constraints are used p->nBTLimit = 1000; // conflict limit at a node p->nBTLimitGlobal = 5000000; // conflict limit for all runs p->nMinDomSize = 100; // min clock domain considered for optimization p->nItersStop = -1; // stop after the given number of iterations p->nResimDelta = 1000; // the internal of nodes to resimulate + p->nStepsMax = -1; // (scorr only) the max number of induction steps p->fPolarFlip = 0; // uses polarity adjustment p->fLatchCorr = 0; // performs register correspondence + p->fOutputCorr = 0; // perform 'PO correspondence' p->fSemiFormal = 0; // enable semiformal filtering - p->fUniqueness = 0; // enable uniqueness constraints p->fDynamic = 0; // dynamic partitioning p->fLocalSim = 0; // local simulation p->fVerbose = 0; // verbose stats @@ -88,6 +93,130 @@ void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p ) p->nBTLimit = 10000; } +/**Function************************************************************* + + Synopsis [Reports improvements for property cones.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ReportConeReductions( Ssw_Man_t * p, Aig_Man_t * pAigInit, Aig_Man_t * pAigStop ) +{ + Aig_Man_t * pAig1, * pAig2, * pAux; + pAig1 = Aig_ManDupOneOutput( pAigInit, 0, 1 ); + pAig1 = Aig_ManScl( pAux = pAig1, 1, 1, 0 ); + Aig_ManStop( pAux ); + pAig2 = Aig_ManDupOneOutput( pAigStop, 0, 1 ); + pAig2 = Aig_ManScl( pAux = pAig2, 1, 1, 0 ); + Aig_ManStop( pAux ); + + p->nNodesBegC = Aig_ManNodeNum(pAig1); + p->nNodesEndC = Aig_ManNodeNum(pAig2); + p->nRegsBegC = Aig_ManRegNum(pAig1); + p->nRegsEndC = Aig_ManRegNum(pAig2); + + Aig_ManStop( pAig1 ); + Aig_ManStop( pAig2 ); +} + +/**Function************************************************************* + + Synopsis [Reports one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ReportOneOutput( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( pObj == Aig_ManConst1(p) ) + printf( "1" ); + else if ( pObj == Aig_ManConst0(p) ) + printf( "0" ); + else + printf( "X" ); +} + +/**Function************************************************************* + + Synopsis [Reports improvements for property cones.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ReportOutputs( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj; + int i; + Saig_ManForEachPo( pAig, pObj, i ) + { + if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) ) + printf( "o" ); + else + printf( "c" ); + Ssw_ReportOneOutput( pAig, Aig_ObjChild0(pObj) ); + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Remove from-equivs that are in the cone of constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose ) +{ + Vec_Ptr_t * vCones; + Aig_Obj_t ** pArray; + Aig_Obj_t * pObj; + int i, nTotal = 0, nRemoved = 0; + // collect the nodes in the cone of constraints + pArray = (Aig_Obj_t **)Vec_PtrArray(pAig->vPos); + pArray += Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig); + vCones = Aig_ManDfsNodes( pAig, pArray, Saig_ManConstrNum(pAig) ); + // remove all the node that are equiv to something and are in the cones + Aig_ManForEachObj( pAig, pObj, i ) + { + if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) ) + continue; + if ( pAig->pReprs[i] != NULL ) + nTotal++; + if ( !Aig_ObjIsTravIdCurrent(pAig, pObj) ) + continue; + if ( pAig->pReprs[i] ) + { + if ( p->pPars->fConstrs && !p->pPars->fMergeFull ) + { + pAig->pReprs[i] = NULL; + nRemoved++; + } + } + } + // collect statistics + p->nConesTotal = Aig_ManPiNum(pAig) + Aig_ManNodeNum(pAig); + p->nConesConstr = Vec_PtrSize(vCones); + p->nEquivsTotal = nTotal; + p->nEquivsConstr = nRemoved; + Vec_PtrFree( vCones ); +} + /**Function************************************************************* Synopsis [Performs computation of signal correspondence with constraints.] @@ -118,9 +247,10 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) if ( !p->pPars->fLatchCorr ) { p->pMSat = Ssw_SatStart( 0 ); - Ssw_ManSweepBmc( p ); - if ( p->pPars->nFramesK > 1 && p->pPars->fUniqueness ) - Ssw_UniqueRegisterPairInfo( p ); + if ( p->pPars->fConstrs ) + Ssw_ManSweepBmcConstr( p ); + else + Ssw_ManSweepBmc( p ); Ssw_SatStop( p->pMSat ); p->pMSat = NULL; Ssw_ManCleanup( p ); @@ -142,10 +272,25 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) Aig_ManStop( pSRed ); } */ + if ( p->pPars->pFunc ) + { + ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); + ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); + } + if ( p->pPars->nStepsMax == 0 ) + { + printf( "Stopped signal correspondence after BMC.\n" ); + goto finalize; + } // refine classes using induction nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0; for ( nIter = 0; ; nIter++ ) { + if ( p->pPars->nStepsMax == nIter ) + { + printf( "Stopped signal correspondence after %d refiment iterations.\n", nIter ); + goto finalize; + } if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter ) { Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p ); @@ -174,19 +319,20 @@ clk = clock(); } else { - if ( p->pPars->fDynamic ) + if ( p->pPars->fConstrs ) + RetValue = Ssw_ManSweepConstr( p ); + else if ( p->pPars->fDynamic ) RetValue = Ssw_ManSweepDyn( p ); else RetValue = Ssw_ManSweep( p ); + p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts; if ( p->pPars->fVerbose ) { printf( "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), p->nConstrReduced, Aig_ManNodeNum(p->pFrames) ); - if ( p->pPars->fUniqueness ) - printf( "U =%4d. ", p->nUniques-nUniques ); - else if ( p->pPars->fDynamic ) + if ( p->pPars->fDynamic ) { printf( "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat ); printf( "R =%4d. ", p->nRecycles-nRecycles ); @@ -211,9 +357,15 @@ clk = clock(); Ssw_ManCleanup( p ); if ( !RetValue ) break; + if ( p->pPars->pFunc ) + ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); } + +finalize: p->pPars->nIters = nIter + 1; p->timeTotal = clock() - clkTotal; + + Ssw_ManUpdateEquivs( p, p->pAig, p->pPars->fVerbose ); pAigNew = Aig_ManDupRepr( p->pAig, 0 ); Aig_ManSeqCleanup( pAigNew ); //Ssw_ClassesPrint( p->ppClasses, 1 ); @@ -221,6 +373,9 @@ p->timeTotal = clock() - clkTotal; p->nLitsEnd = Ssw_ClassesLitNum( p->ppClasses ); p->nNodesEnd = Aig_ManNodeNum(pAigNew); p->nRegsEnd = Aig_ManRegNum(pAigNew); + // cleanup + Aig_ManSetPhase( p->pAig ); + Aig_ManCleanMarkB( p->pAig ); return pAigNew; } @@ -255,13 +410,6 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) return Aig_ManDupOrdered(pAig); } // check and update parameters - if ( pPars->fUniqueness ) - { - pPars->nFramesAddSim = 0; - if ( pPars->nFramesK != 2 ) - printf( "Setting K = 2 for uniqueness constraints to work.\n" ); - pPars->nFramesK = 2; - } if ( pPars->fLatchCorrOpt ) { pPars->fLatchCorr = 1; @@ -291,15 +439,31 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat ); } } - + // start the induction manager p = Ssw_ManCreate( pAig, pPars ); // compute candidate equivalence classes // p->pPars->nConstrs = 1; - if ( p->pPars->nConstrs == 0 ) + if ( p->pPars->fConstrs ) + { + // 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_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit ); + // derive phase bits to satisfy the constraints + if ( Ssw_ManSetConstrPhases( pAig, p->pPars->nFramesK + 1, &p->vInits ) != 0 ) + { + printf( "Ssw_SignalCorrespondence(): The init state does not satisfy the constraints!\n" ); + p->pPars->fVerbose = 0; + Ssw_ManStop( p ); + return NULL; + } + // perform simulation of the first timeframes + Ssw_ManRefineByConstrSim( p ); + } + else { // perform one round of seq simulation and generate candidate equivalence classes - p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose ); + p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose ); // p->ppClasses = Ssw_ClassesPrepareTargets( pAig ); if ( pPars->fLatchCorrOpt ) p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 ); @@ -307,21 +471,16 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); else p->pSml = Ssw_SmlStart( pAig, 0, 1 + p->pPars->nFramesAddSim, 1 ); - Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); - } - 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_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit ); + Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord ); } + // allocate storage if ( p->pPars->fLocalSim ) p->pVisited = ABC_CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) ); // perform refinement of classes pAigNew = Ssw_SignalCorrespondenceRefine( p ); - if ( pPars->fUniqueness ) - printf( "Uniqueness constraints = %3d. Prevented counter-examples = %3d.\n", - p->nUniquesAdded, p->nUniquesUseful ); +// Ssw_ReportOutputs( pAigNew ); + if ( pPars->fConstrs && pPars->fVerbose ) + Ssw_ReportConeReductions( p, pAig, pAigNew ); // cleanup Ssw_ManStop( p ); return pAigNew; @@ -340,10 +499,14 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) ***********************************************************************/ Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) { + Aig_Man_t * pRes; Ssw_Pars_t Pars; if ( pPars == NULL ) Ssw_ManSetDefaultParamsLcorr( pPars = &Pars ); - return Ssw_SignalCorrespondence( pAig, pPars ); + pRes = Ssw_SignalCorrespondence( pAig, pPars ); +// if ( pPars->fConstrs && pPars->fVerbose ) +// Ssw_ReportConeReductions( pAig, pRes ); + return pRes; } @@ -352,3 +515,5 @@ Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) //////////////////////////////////////////////////////////////////////// +ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3