diff options
Diffstat (limited to 'src/aig/cec/cecChoice.c')
| -rw-r--r-- | src/aig/cec/cecChoice.c | 409 |
1 files changed, 0 insertions, 409 deletions
diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c deleted file mode 100644 index 076b34a2..00000000 --- a/src/aig/cec/cecChoice.c +++ /dev/null @@ -1,409 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecChoice.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinational equivalence checking.] - - Synopsis [Computation of structural choices.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecChoice.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cecInt.h" -#include "giaAig.h" -#include "dch.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ); - -extern int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore ); -extern int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Computes the real value of the literal w/o spec reduction.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Cec_ManCombSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) -{ - assert( Gia_ObjIsAnd(pObj) ); - Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); - Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj) ); - return Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); -} - -/**Function************************************************************* - - Synopsis [Recursively performs speculative reduction for the object.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) -{ - Gia_Obj_t * pRepr; - if ( ~pObj->Value ) - return; - if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) - { - Cec_ManCombSpecReduce_rec( pNew, p, pRepr ); - pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); - return; - } - pObj->Value = Cec_ManCombSpecReal( pNew, p, pObj ); -} - -/**Function************************************************************* - - Synopsis [Derives SRM for signal correspondence.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Cec_ManCombSpecReduce( Gia_Man_t * p, Vec_Int_t ** pvOutputs, int fRings ) -{ - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, * pRepr; - Vec_Int_t * vXorLits; - int i, iPrev, iObj, iPrevNew, iObjNew; - assert( p->pReprs != NULL ); - Gia_ManSetPhase( p ); - Gia_ManFillValue( p ); - pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); - Gia_ManHashAlloc( pNew ); - Gia_ManConst0(p)->Value = 0; - Gia_ManForEachCi( p, pObj, i ) - pObj->Value = Gia_ManAppendCi(pNew); - *pvOutputs = Vec_IntAlloc( 1000 ); - vXorLits = Vec_IntAlloc( 1000 ); - if ( fRings ) - { - Gia_ManForEachObj1( p, pObj, i ) - { - if ( Gia_ObjIsConst( p, i ) ) - { - iObjNew = Cec_ManCombSpecReal( pNew, p, pObj ); - iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ); - if ( iObjNew != 0 ) - { - Vec_IntPush( *pvOutputs, 0 ); - Vec_IntPush( *pvOutputs, i ); - Vec_IntPush( vXorLits, iObjNew ); - } - } - else if ( Gia_ObjIsHead( p, i ) ) - { - iPrev = i; - Gia_ClassForEachObj1( p, i, iObj ) - { - iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) ); - iObjNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) ); - iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); - iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); - if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) - { - Vec_IntPush( *pvOutputs, iPrev ); - Vec_IntPush( *pvOutputs, iObj ); - Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) ); - } - iPrev = iObj; - } - iObj = i; - iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) ); - iObjNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) ); - iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); - iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); - if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) - { - Vec_IntPush( *pvOutputs, iPrev ); - Vec_IntPush( *pvOutputs, iObj ); - Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) ); - } - } - } - } - else - { - Gia_ManForEachObj1( p, pObj, i ) - { - pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); - if ( pRepr == NULL ) - continue; - iPrevNew = Gia_ObjIsConst(p, i)? 0 : Cec_ManCombSpecReal( pNew, p, pRepr ); - iObjNew = Cec_ManCombSpecReal( pNew, p, pObj ); - iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); - if ( iPrevNew != iObjNew ) - { - Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) ); - Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) ); - Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) ); - } - } - } - Vec_IntForEachEntry( vXorLits, iObjNew, i ) - Gia_ManAppendCo( pNew, iObjNew ); - Vec_IntFree( vXorLits ); - Gia_ManHashStop( pNew ); -//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); - pNew = Gia_ManCleanup( pTemp = pNew ); -//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) ); - Gia_ManStop( pTemp ); - return pNew; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars ) -{ - int nItersMax = 1000; - Vec_Str_t * vStatus; - Vec_Int_t * vOutputs; - Vec_Int_t * vCexStore; - Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; - Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; - Cec_ManSim_t * pSim; - Gia_Man_t * pSrm; - int r, RetValue; - int clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock(); - int clk2, clk = clock(); - ABC_FREE( pAig->pReprs ); - ABC_FREE( pAig->pNexts ); - Gia_ManRandom( 1 ); - // prepare simulation manager - Cec_ManSimSetDefaultParams( pParsSim ); - pParsSim->nWords = pPars->nWords; - pParsSim->nFrames = pPars->nRounds; - pParsSim->fVerbose = pPars->fVerbose; - pParsSim->fLatchCorr = 0; - pParsSim->fSeqSimulate = 0; - // create equivalence classes of registers - pSim = Cec_ManSimStart( pAig, pParsSim ); - Cec_ManSimClassesPrepare( pSim, -1 ); - Cec_ManSimClassesRefine( pSim ); - // prepare SAT solving - Cec_ManSatSetDefaultParams( pParsSat ); - pParsSat->nBTLimit = pPars->nBTLimit; - pParsSat->fVerbose = pPars->fVerbose; - if ( pPars->fVerbose ) - { - Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n", - Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->fUseRings, pPars->fUseCSat ); - Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk ); - } - // perform refinement of equivalence classes - for ( r = 0; r < nItersMax; r++ ) - { - clk = clock(); - // perform speculative reduction - clk2 = clock(); - pSrm = Cec_ManCombSpecReduce( pAig, &vOutputs, pPars->fUseRings ); - assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManCiNum(pSrm) == Gia_ManCiNum(pAig) ); - clkSrm += clock() - clk2; - if ( Gia_ManCoNum(pSrm) == 0 ) - { - if ( pPars->fVerbose ) - Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk ); - Vec_IntFree( vOutputs ); - Gia_ManStop( pSrm ); - break; - } -//Gia_DumpAiger( pSrm, "choicesrm", r, 2 ); - // found counter-examples to speculation - clk2 = clock(); - if ( pPars->fUseCSat ) - vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); - else - vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); - Gia_ManStop( pSrm ); - clkSat += clock() - clk2; - if ( Vec_IntSize(vCexStore) == 0 ) - { - if ( pPars->fVerbose ) - Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk ); - Vec_IntFree( vCexStore ); - Vec_StrFree( vStatus ); - Vec_IntFree( vOutputs ); - break; - } - // refine classes with these counter-examples - clk2 = clock(); - RetValue = Cec_ManResimulateCounterExamplesComb( pSim, vCexStore ); - Vec_IntFree( vCexStore ); - clkSim += clock() - clk2; - Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); - if ( pPars->fVerbose ) - Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk ); - Vec_StrFree( vStatus ); - Vec_IntFree( vOutputs ); -//Gia_ManEquivPrintClasses( pAig, 1, 0 ); - } - // check the overflow - if ( r == nItersMax ) - Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" ); - Cec_ManSimStop( pSim ); - clkTotal = clock() - clkTotal; - // report the results - if ( pPars->fVerbose ) - { - Abc_PrintTimeP( 1, "Srm ", clkSrm, clkTotal ); - Abc_PrintTimeP( 1, "Sat ", clkSat, clkTotal ); - Abc_PrintTimeP( 1, "Sim ", clkSim, clkTotal ); - Abc_PrintTimeP( 1, "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); - Abc_PrintTime( 1, "TOTAL", clkTotal ); - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Computes choices for the vector of AIGs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc_t * pPars ) -{ - Gia_Man_t * pNew; - int RetValue; - // compute equivalences of the miter -// pMiter = Gia_ManChoiceMiter( vGias ); -// Gia_ManSetRegNum( pMiter, 0 ); - RetValue = Cec_ManChoiceComputation_int( pGia, pPars ); - // derive AIG with choices - pNew = Gia_ManEquivToChoices( pGia, nGias ); - Gia_ManHasChoices( pNew ); -// Gia_ManStop( pMiter ); - // report the results - if ( pPars->fVerbose ) - { -// Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", -// Gia_ManAndNum(pAig), Gia_ManAndNum(pNew), -// 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), -// Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), -// 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) ); - } - return pNew; -} - -/**Function************************************************************* - - Synopsis [Computes choices for one AIGs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc ) -{ -// extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars ); - Dch_Pars_t Pars, * pPars = &Pars; - Aig_Man_t * pMan, * pManNew; - Gia_Man_t * pGia; - if ( 0 ) - { - pGia = Cec_ManChoiceComputationVec( pAig, 3, pParsChc ); - } - else - { - pMan = Gia_ManToAig( pAig, 0 ); - Dch_ManSetDefaultParams( pPars ); - pPars->fUseGia = 1; - pPars->nBTLimit = pParsChc->nBTLimit; - pPars->fUseCSat = pParsChc->fUseCSat; - pPars->fVerbose = pParsChc->fVerbose; - pManNew = Dar_ManChoiceNew( pMan, pPars ); - pGia = Gia_ManFromAig( pManNew ); - Aig_ManStop( pManNew ); -// Aig_ManStop( pMan ); - } - return pGia; -} - -/**Function************************************************************* - - Synopsis [Performs computation of AIGs with choices.] - - Description [Takes several AIGs and performs choicing.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars ) -{ - Cec_ParChc_t ParsChc, * pParsChc = &ParsChc; - Aig_Man_t * pAig; - if ( pPars->fVerbose ) - Abc_PrintTime( 1, "Synthesis time", pPars->timeSynth ); - Cec_ManChcSetDefaultParams( pParsChc ); - pParsChc->nBTLimit = pPars->nBTLimit; - pParsChc->fUseCSat = pPars->fUseCSat; - if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 ) - pParsChc->nBTLimit = 100; - pParsChc->fVerbose = pPars->fVerbose; - pGia = Cec_ManChoiceComputationVec( pGia, 3, pParsChc ); - Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) ); - pAig = Gia_ManToAig( pGia, 1 ); - Gia_ManStop( pGia ); - return pAig; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |