diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2009-04-10 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2009-04-10 08:01:00 -0700 |
| commit | ccd1b57264d3bf1514410747cdcf6e4731ac7f2a (patch) | |
| tree | 17993c239735ee63c4e8ed69cb1c3df7eacecc6d | |
| parent | df6fdd1dffd8ce83dfc4a7868ebdd25241f8f24b (diff) | |
| download | abc-ccd1b57264d3bf1514410747cdcf6e4731ac7f2a.tar.gz abc-ccd1b57264d3bf1514410747cdcf6e4731ac7f2a.tar.bz2 abc-ccd1b57264d3bf1514410747cdcf6e4731ac7f2a.zip | |
Version abc90410
36 files changed, 1196 insertions, 171 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 1750a7b7..38ba167f 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -514,10 +514,10 @@ extern void Aig_ManStopMemory( Aig_Man_t * p ); /*=== aigMffc.c ==========================================================*/ extern int Aig_NodeRef_rec( Aig_Obj_t * pNode, unsigned LevelMin ); extern int Aig_NodeDeref_rec( Aig_Obj_t * pNode, unsigned LevelMin, float * pPower, float * pProbs ); -extern int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp ); -extern int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower ); -extern int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves ); -extern int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult ); +extern int Aig_NodeMffcSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp ); +extern int Aig_NodeMffcLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower ); +extern int Aig_NodeMffcLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves ); +extern int Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult ); /*=== aigObj.c ==========================================================*/ extern Aig_Obj_t * Aig_ObjCreatePi( Aig_Man_t * p ); extern Aig_Obj_t * Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver ); diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c index febe8a0c..eeaf4c91 100644 --- a/src/aig/aig/aigDup.c +++ b/src/aig/aig/aigDup.c @@ -476,15 +476,9 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p ) pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); // duplicate representation of choice nodes if ( p->pEquivs ) - { - pNew->pEquivs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) ); - memset( pNew->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) ); - } + pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) ); if ( p->pReprs ) - { - pNew->pReprs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) ); - memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) ); - } + pNew->pReprs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) ); // create the PIs Aig_ManCleanData( p ); // duplicate internal nodes diff --git a/src/aig/aig/aigMffc.c b/src/aig/aig/aigMffc.c index 2c648382..b902e609 100644 --- a/src/aig/aig/aigMffc.c +++ b/src/aig/aig/aigMffc.c @@ -144,7 +144,7 @@ int Aig_NodeRefLabel_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin ) SeeAlso [] ***********************************************************************/ -void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin, Vec_Ptr_t * vSupp, int fTopmost, Aig_Obj_t * pObjSkip ) +void Aig_NodeMffcSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin, Vec_Ptr_t * vSupp, int fTopmost, Aig_Obj_t * pObjSkip ) { // skip visited nodes if ( Aig_ObjIsTravIdCurrent(p, pNode) ) @@ -158,8 +158,8 @@ void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin, } assert( Aig_ObjIsNode(pNode) ); // recur on the children - Aig_NodeMffsSupp_rec( p, Aig_ObjFanin0(pNode), LevelMin, vSupp, 0, pObjSkip ); - Aig_NodeMffsSupp_rec( p, Aig_ObjFanin1(pNode), LevelMin, vSupp, 0, pObjSkip ); + Aig_NodeMffcSupp_rec( p, Aig_ObjFanin0(pNode), LevelMin, vSupp, 0, pObjSkip ); + Aig_NodeMffcSupp_rec( p, Aig_ObjFanin1(pNode), LevelMin, vSupp, 0, pObjSkip ); } /**Function************************************************************* @@ -173,7 +173,7 @@ void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin, SeeAlso [] ***********************************************************************/ -int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp ) +int Aig_NodeMffcSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp ) { int ConeSize1, ConeSize2; if ( vSupp ) Vec_PtrClear( vSupp ); @@ -187,7 +187,7 @@ int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t assert( Aig_ObjIsNode(pNode) ); Aig_ManIncrementTravId( p ); ConeSize1 = Aig_NodeDeref_rec( pNode, LevelMin, NULL, NULL ); - Aig_NodeMffsSupp_rec( p, pNode, LevelMin, vSupp, 1, NULL ); + Aig_NodeMffcSupp_rec( p, pNode, LevelMin, vSupp, 1, NULL ); ConeSize2 = Aig_NodeRef_rec( pNode, LevelMin ); assert( ConeSize1 == ConeSize2 ); assert( ConeSize1 > 0 ); @@ -205,7 +205,7 @@ int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t SeeAlso [] ***********************************************************************/ -int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower ) +int Aig_NodeMffcLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower ) { int ConeSize1, ConeSize2; assert( (pPower != NULL) == (p->vProbs != NULL) ); @@ -230,7 +230,7 @@ int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower ) SeeAlso [] ***********************************************************************/ -int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves ) +int Aig_NodeMffcLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves ) { Aig_Obj_t * pObj; int i, ConeSize1, ConeSize2; @@ -259,7 +259,7 @@ int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves SeeAlso [] ***********************************************************************/ -int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult ) +int Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult ) { Aig_Obj_t * pObj, * pLeafBest; int i, LevelMax, ConeSize1, ConeSize2, ConeCur1, ConeCur2, ConeBest; @@ -294,7 +294,7 @@ int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves // collect the cut nodes Vec_PtrClear( vResult ); Aig_ManIncrementTravId( p ); - Aig_NodeMffsSupp_rec( p, pNode, 0, vResult, 1, pLeafBest ); + Aig_NodeMffcSupp_rec( p, pNode, 0, vResult, 1, pLeafBest ); // ref the nodes ConeCur2 = Aig_NodeRef_rec( pLeafBest, 0 ); assert( ConeCur1 == ConeCur2 ); diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index 1fd85768..6e0cb3e8 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -1520,7 +1520,7 @@ void Aig_ManChoiceEval( Aig_Man_t * p ) printf( "Choice node = %5d. Level = %2d. Choices = %d. { ", pNode->Id, pNode->Level, Counter ); for ( pTemp = pNode; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) ) { - Counter = Aig_NodeMffsSupp( p, pTemp, 0, vSupp ); + Counter = Aig_NodeMffcSupp( p, pTemp, 0, vSupp ); printf( "S=%d N=%d L=%d ", Vec_PtrSize(vSupp), Counter, pTemp->Level ); } printf( "}\n" ); diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h index a965730f..5cb8d345 100644 --- a/src/aig/cec/cec.h +++ b/src/aig/cec/cec.h @@ -125,6 +125,7 @@ struct Cec_ParCor_t_ int nBTLimit; // conflict limit at a node int fLatchCorr; // consider only latch outputs int fUseRings; // use rings + int fMakeChoices; // use equilvaences as choices int fUseCSat; // use circuit-based solver int fFirstStop; // stop on the first sat output int fUseSmartCnf; // use smart CNF computation @@ -139,8 +140,8 @@ struct Cec_ParChc_t_ int nWords; // the number of simulation words int nRounds; // the number of simulation rounds int nBTLimit; // conflict limit at a node - int fFirstStop; // stop on the first sat output - int fUseSmartCnf; // use smart CNF computation + int fUseRings; // use rings + int fUseCSat; // use circuit-based solver int fVeryVerbose; // verbose stats int fVerbose; // verbose stats }; diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c index ee9f6d3c..7ec3dad4 100644 --- a/src/aig/cec/cecCec.c +++ b/src/aig/cec/cecCec.c @@ -70,7 +70,7 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose ) extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ); extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs ); Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter ); - Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp ); + Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 ); int RetValue, iOut, nOuts, clkTotal = clock(); Gia_ManStop( pTemp ); // run CEC on this miter diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c index 2a619e39..0662d73d 100644 --- a/src/aig/cec/cecChoice.c +++ b/src/aig/cec/cecChoice.c @@ -19,17 +19,172 @@ ***********************************************************************/ #include "cecInt.h" +#include "giaAig.h" +#include "dch.h" //////////////////////////////////////////////////////////////////////// /// 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 ); +//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); + pNew = Gia_ManCleanup( pTemp = pNew ); +//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) ); + Gia_ManStop( pTemp ); + return pNew; +} + + +/**Function************************************************************* + Synopsis [] Description [] @@ -39,9 +194,293 @@ SeeAlso [] ***********************************************************************/ -Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars ) +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->nRounds = 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 ); + Cec_ManSimClassesRefine( pSim ); + // prepare SAT solving + Cec_ManSatSetDefaultParams( pParsSat ); + pParsSat->nBTLimit = pPars->nBTLimit; + pParsSat->fVerbose = pPars->fVerbose; + if ( pPars->fVerbose ) + { + printf( "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 ) + printf( "The refinement was not finished. The result may be incorrect.\n" ); + Cec_ManSimStop( pSim ); + clkTotal = clock() - clkTotal; + // report the results + if ( pPars->fVerbose ) + { + ABC_PRTP( "Srm ", clkSrm, clkTotal ); + ABC_PRTP( "Sat ", clkSat, clkTotal ); + ABC_PRTP( "Sim ", clkSim, clkTotal ); + ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); + ABC_PRT( "TOTAL", clkTotal ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return pObj->Value; + Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) ); + if ( Gia_ObjIsCo(pObj) ) + return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) ); + return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Derives the miter of several AIGs for choice computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ) +{ + Gia_Man_t * pNew, * pGia, * pGia0; + int i, k, iNode, nNodes; + // make sure they have equal parameters + assert( Vec_PtrSize(vGias) > 0 ); + pGia0 = Vec_PtrEntry( vGias, 0 ); + Vec_PtrForEachEntry( vGias, pGia, i ) + { + assert( Gia_ManCiNum(pGia) == Gia_ManCiNum(pGia0) ); + assert( Gia_ManCoNum(pGia) == Gia_ManCoNum(pGia0) ); + assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) ); + Gia_ManFillValue( pGia ); + Gia_ManConst0(pGia)->Value = 0; + } + // start the new manager + pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) ); + pNew->pName = Gia_UtilStrsav( pGia0->pName ); + // create new CIs and assign them to the old manager CIs + for ( k = 0; k < Gia_ManCiNum(pGia0); k++ ) + { + iNode = Gia_ManAppendCi(pNew); + Vec_PtrForEachEntry( vGias, pGia, i ) + Gia_ManCi( pGia, k )->Value = iNode; + } + // create internal nodes + Gia_ManHashAlloc( pNew ); + for ( k = 0; k < Gia_ManCoNum(pGia0); k++ ) + { + Vec_PtrForEachEntry( vGias, pGia, i ) + Gia_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) ); + } + Gia_ManHashStop( pNew ); + // check the presence of dangling nodes + nNodes = Gia_ManHasDandling( pNew ); + assert( nNodes == 0 ); + // finalize +// Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia0) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Computes choices for the vector of AIGs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Cec_ManChoiceComputationVec( Vec_Ptr_t * vGias, Cec_ParChc_t * pPars ) +{ + Gia_Man_t * pMiter, * pNew; + int RetValue; + // compute equivalences of the miter + pMiter = Gia_ManChoiceMiter( vGias ); + RetValue = Cec_ManChoiceComputation_int( pMiter, pPars ); + // derive AIG with choices + pNew = Gia_ManEquivToChoices( pMiter, Vec_PtrSize(vGias) ); + Gia_ManHasChoices( pNew ); + Gia_ManStop( pMiter ); + // report the results + if ( pPars->fVerbose ) + { +// printf( "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 ) + { + Vec_Ptr_t * vGias; + vGias = Vec_PtrAlloc( 1 ); + Vec_PtrPush( vGias, pAig ); + pGia = Cec_ManChoiceComputationVec( vGias, pParsChc ); + Vec_PtrFree( vGias ); + } + 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( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) { - return NULL; + Cec_ParChc_t ParsChc, * pParsChc = &ParsChc; + Vec_Ptr_t * vGias; + Gia_Man_t * pGia; + Aig_Man_t * pAig; + int i; + if ( pPars->fVerbose ) + ABC_PRT( "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; + vGias = Vec_PtrAlloc( 10 ); + Vec_PtrForEachEntry( vAigs, pAig, i ) + Vec_PtrPush( vGias, Gia_ManFromAig(pAig) ); + pGia = Cec_ManChoiceComputationVec( vGias, pParsChc ); + Gia_ManSetRegNum( pGia, Gia_ManRegNum(Vec_PtrEntry(vGias, 0)) ); + Vec_PtrForEachEntry( vGias, pAig, i ) + Gia_ManStop( (Gia_Man_t *)pAig ); + Vec_PtrFree( vGias ); + pAig = Gia_ManToAig( pGia, 1 ); + Gia_ManStop( pGia ); + return pAig; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c index ca0a3665..dc0fc0d0 100644 --- a/src/aig/cec/cecCore.c +++ b/src/aig/cec/cecCore.c @@ -199,8 +199,8 @@ void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p ) p->nWords = 15; // the number of simulation words p->nRounds = 15; // the number of simulation rounds p->nBTLimit = 1000; // conflict limit at a node - p->fFirstStop = 0; // stop on the first sat output - p->fUseSmartCnf = 0; // use smart CNF computation + p->fUseRings = 1; // use rings + p->fUseCSat = 0; // use circuit-based solver p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats } diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c index dccd90b0..8e97e207 100644 --- a/src/aig/cec/cecCorr.c +++ b/src/aig/cec/cecCorr.c @@ -566,6 +566,35 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore /**Function************************************************************* + Synopsis [Resimulates counter-examples derived by the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore ) +{ + Vec_Ptr_t * vSimInfo; + int RetValue = 0, iStart = 0; + Gia_ManSetRefs( pSim->pAig ); + pSim->pPars->nRounds = 1; + vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords ); + while ( iStart < Vec_IntSize(vCexStore) ) + { + Cec_ManStartSimInfo( vSimInfo, 0 ); + iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart ); + RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo ); + } + assert( iStart == Vec_IntSize(vCexStore) ); + Vec_PtrFree( vSimInfo ); + return RetValue; +} + +/**Function************************************************************* + Synopsis [Updates equivalence classes by marking those that timed out.] Description [Returns 1 if all ndoes are proved.] @@ -613,9 +642,10 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu return 1; } + /**Function************************************************************* - Synopsis [Marks all the nodes as proved.] + Synopsis [Duplicates the AIG in the DFS order.] Description [] @@ -624,22 +654,59 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu SeeAlso [] ***********************************************************************/ -void Gia_ManSetProvedNodes( Gia_Man_t * p ) +void Gia_ManCorrReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) { - Gia_Obj_t * pObj; - int i, nLits = 0; - Gia_ManForEachObj1( p, pObj, i ) + Gia_Obj_t * pRepr; + if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) { - if ( Gia_ObjRepr(p, i) == GIA_VOID ) - continue; - Gia_ObjSetProved( p, i ); - nLits++; + Gia_ManCorrReduce_rec( pNew, p, pRepr ); + pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + return; } -// printf( "Identified %d proved literals.\n", nLits ); + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin1(pObj) ); + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } /**Function************************************************************* + Synopsis [Reduces AIG using equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + Gia_ManSetPhase( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + + +/**Function************************************************************* + Synopsis [Prints statistics during solving.] Description [] @@ -649,7 +716,7 @@ void Gia_ManSetProvedNodes( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time ) +void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time ) { int nLits, CounterX = 0, Counter0 = 0, Counter = 0; int i, Entry, nProve = 0, nDispr = 0, nFail = 0; @@ -685,7 +752,7 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int /**Function************************************************************* - Synopsis [Top-level procedure for register correspondence.] + Synopsis [Internal procedure for register correspondence.] Description [] @@ -694,26 +761,26 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int SeeAlso [] ***********************************************************************/ -Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) +int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) { + int nIterMax = 100000; int nAddFrames = 1; // additional timeframes to simulate Vec_Str_t * vStatus; Vec_Int_t * vOutputs; Vec_Int_t * vCexStore; - Gia_Man_t * pNew, * pTemp; 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 r, RetValue, clkTotal = clock(); + int clkSat = 0, clkSim = 0, clkSrm = 0; int clk2, clk = clock(); ABC_FREE( pAig->pReprs ); ABC_FREE( pAig->pNexts ); if ( Gia_ManRegNum(pAig) == 0 ) { printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); - return NULL; + return 0; } Gia_ManRandom( 1 ); // prepare simulation manager @@ -736,10 +803,10 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) printf( "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n", Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat ); - Cec_ManLCorrPrintStats( pAig, NULL, 0, clock() - clk ); + Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk ); } // perform refinement of equivalence classes - for ( r = 0; r < 100000; r++ ) + for ( r = 0; r < nIterMax; r++ ) { clk = clock(); // perform speculative reduction @@ -776,7 +843,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) clkSim += clock() - clk2; Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); if ( pPars->fVerbose ) - Cec_ManLCorrPrintStats( pAig, vStatus, r+1, clock() - clk ); + Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk ); Vec_StrFree( vStatus ); Vec_IntFree( vOutputs ); //Gia_ManEquivPrintClasses( pAig, 1, 0 ); @@ -811,7 +878,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) fChanges = 1; } if ( pPars->fVerbose ) - Cec_ManLCorrPrintStats( pAig, vStatus, -1, clock() - clkBmc ); + Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc ); // recycle Vec_IntFree( vCexStore ); Vec_StrFree( vStatus ); @@ -822,20 +889,55 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) else { if ( pPars->fVerbose ) - Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk ); + Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk ); } // check the overflow - if ( r == 100000 ) + if ( r == nIterMax ) printf( "The refinement was not finished. The result may be incorrect.\n" ); Cec_ManSimStop( pSim ); clkTotal = clock() - clkTotal; + // report the results + if ( pPars->fVerbose ) + { + ABC_PRTP( "Srm ", clkSrm, clkTotal ); + ABC_PRTP( "Sat ", clkSat, clkTotal ); + ABC_PRTP( "Sim ", clkSim, clkTotal ); + ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); + ABC_PRT( "TOTAL", clkTotal ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Top-level procedure for register correspondence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) +{ + Gia_Man_t * pNew, * pTemp; + int RetValue; + RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars ); // derive reduced AIG - Gia_ManSetProvedNodes( pAig ); - Gia_ManEquivImprove( pAig ); - pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 ); -//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 ); - pNew = Gia_ManSeqCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); + if ( pPars->fMakeChoices ) + { + pNew = Gia_ManEquivToChoices( pAig, 1 ); + Gia_ManHasChoices( pNew ); + } + else + { + Gia_ManEquivImprove( pAig ); + pNew = Gia_ManCorrReduce( pAig ); + pNew = Gia_ManSeqCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + //Gia_WriteAiger( pNew, "reduced.aig", 0, 0 ); + } // report the results if ( pPars->fVerbose ) { @@ -844,11 +946,6 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) 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) ); - ABC_PRTP( "Srm ", clkSrm, clkTotal ); - ABC_PRTP( "Sat ", clkSat, clkTotal ); - ABC_PRTP( "Sim ", clkSim, clkTotal ); - ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); - ABC_PRT( "TOTAL", clkTotal ); } return pNew; } diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h index 22bd292b..1fd48d55 100644 --- a/src/aig/cec/cecInt.h +++ b/src/aig/cec/cecInt.h @@ -166,7 +166,8 @@ struct Cec_ManFra_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== cecCore.c ============================================================*/ +/*=== cecCorr.c ============================================================*/ +extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time ); /*=== cecClass.c ============================================================*/ extern int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i ); extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p ); diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index 28f3a637..b19950b3 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -126,7 +126,7 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ) { unsigned * pInfo0, * pInfo1; int f, i, k, w, RetValue = 0; - assert( Gia_ManRegNum(p->pAig) > 0 ); +// assert( Gia_ManRegNum(p->pAig) > 0 ); assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nRounds ); for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ ) { diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c index cfa4594d..7b23aa33 100644 --- a/src/aig/dar/darLib.c +++ b/src/aig/dar/darLib.c @@ -730,7 +730,7 @@ int Dar_LibCutMarkMffc( Aig_Man_t * p, Aig_Obj_t * pRoot, int nLeaves, float * p for ( i = 0; i < nLeaves; i++ ) Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs++; // label MFFC with current ID - nNodes = Aig_NodeMffsLabel( p, pRoot, pPower ); + nNodes = Aig_NodeMffcLabel( p, pRoot, pPower ); // unmark the cut leaves for ( i = 0; i < nLeaves; i++ ) Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs--; diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c index 6118dd71..5f6c5520 100644 --- a/src/aig/dar/darRefact.c +++ b/src/aig/dar/darRefact.c @@ -376,14 +376,14 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore ); if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) ) { - p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL ); + p->GainBest = Aig_NodeMffcSupp( p->pAig, pObj, 0, NULL ); p->pGraphBest = Kit_GraphCreateConst0(); Vec_PtrCopy( p->vLeavesBest, vCut ); return p->GainBest; } if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) ) { - p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL ); + p->GainBest = Aig_NodeMffcSupp( p->pAig, pObj, 0, NULL ); p->pGraphBest = Kit_GraphCreateConst1(); Vec_PtrCopy( p->vLeavesBest, vCut ); return p->GainBest; @@ -528,7 +528,7 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) // get the bounded MFFC size clk = clock(); nLevelMin = ABC_MAX( 0, Aig_ObjLevel(pObj) - 10 ); - nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut ); + nNodesSaved = Aig_NodeMffcSupp( pAig, pObj, nLevelMin, vCut ); if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider { p->timeCuts += clock() - clk; @@ -538,15 +538,15 @@ p->timeCuts += clock() - clk; if ( Vec_PtrSize(vCut) > p->pPars->nLeafMax ) // get one reconv-driven cut { Aig_ManFindCut( pObj, vCut, p->vCutNodes, p->pPars->nLeafMax, 50 ); - nNodesSaved = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut ); + nNodesSaved = Aig_NodeMffcLabelCut( p->pAig, pObj, vCut ); } else if ( Vec_PtrSize(vCut) < p->pPars->nLeafMax - 2 && p->pPars->fExtend ) { if ( !Dar_ObjCutLevelAchieved(vCut, nLevelMin) ) { - if ( Aig_NodeMffsExtendCut( pAig, pObj, vCut, vCut2 ) ) + if ( Aig_NodeMffcExtendCut( pAig, pObj, vCut, vCut2 ) ) { - nNodesSaved2 = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut ); + nNodesSaved2 = Aig_NodeMffcLabelCut( p->pAig, pObj, vCut ); assert( nNodesSaved2 == nNodesSaved ); } if ( Vec_PtrSize(vCut2) > p->pPars->nLeafMax ) diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index 383b5b6b..66e6371d 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -435,6 +435,7 @@ ABC_PRT( "Choicing time ", clock() - clk ); Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars ) { extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); + extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); int fVerbose = pPars->fVerbose; int fConstruct = 0; @@ -444,7 +445,8 @@ Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars ) clk = clock(); // vAigs = Dar_ManChoiceSynthesisExt(); - vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose ); +// vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose ); + vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, 0 ); // swap the first and last network // this should lead to the primary choice being "better" because of synthesis @@ -458,9 +460,9 @@ clk = clock(); if ( fVerbose ) { -ABC_PRT( "Synthesis time", clock() - clk ); +//ABC_PRT( "Synthesis time", clock() - clk ); } -// pPars->timeSynth = clock() - clk; + pPars->timeSynth = clock() - clk; clk = clock(); /* @@ -469,7 +471,11 @@ clk = clock(); else pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose ); */ - pMan = Dch_ComputeChoices( vAigs, pPars ); + // perform choice computation + if ( pPars->fUseGia ) + pMan = Cec_ComputeChoices( vAigs, pPars ); + else + pMan = Dch_ComputeChoices( vAigs, pPars ); // reconstruct the network pMan = Aig_ManDupDfsGuided( pTemp = pMan, Vec_PtrEntry(vAigs,0) ); @@ -483,6 +489,8 @@ clk = clock(); } // reset levels Aig_ManChoiceLevel( pMan ); + ABC_FREE( pMan->pName ); + ABC_FREE( pMan->pSpec ); pMan->pName = Aig_UtilStrsav( pTemp->pName ); pMan->pSpec = Aig_UtilStrsav( pTemp->pSpec ); diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h index a5a56da6..6157a811 100644 --- a/src/aig/dch/dch.h +++ b/src/aig/dch/dch.h @@ -46,8 +46,10 @@ struct Dch_Pars_t_ int nSatVarMax; // the max number of SAT variables int fSynthesis; // set to 1 to perform synthesis int fPolarFlip; // uses polarity adjustment - int fSimulateTfo; // uses simulatin of TFO classes + int fSimulateTfo; // uses simulation of TFO classes int fPower; // uses power-aware rewriting + int fUseGia; // uses GIA package + int fUseCSat; // uses circuit-based solver int fVerbose; // verbose stats int timeSynth; // synthesis runtime int nNodesAhead; // the lookahead in terms of nodes diff --git a/src/aig/dch/dchAig.c b/src/aig/dch/dchAig.c index 239ece18..d38a1304 100644 --- a/src/aig/dch/dchAig.c +++ b/src/aig/dch/dchAig.c @@ -72,7 +72,7 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ) { assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) ); assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) ); - nNodes += Aig_ManNodeNum(pAig); + nNodes += Aig_ManNodeNum(pAig2); Aig_ManCleanData( pAig2 ); } // map constant nodes diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index feee5472..2d633d5c 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -418,6 +418,7 @@ static inline int Gia_ObjVisitColor( Gia_Man_t * p, int Id, int c ) { i static inline int Gia_ObjDiffColors( Gia_Man_t * p, int i, int j ) { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) && (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); } static inline int Gia_ObjDiffColors2( Gia_Man_t * p, int i, int j ) { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) || (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); } +static inline Gia_Obj_t * Gia_ObjNextObj( Gia_Man_t * p, int Id ) { return p->pNexts[Id] == 0 ? NULL : Gia_ManObj( p, p->pNexts[Id] );} static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { return p->pNexts[Id]; } static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; } @@ -535,6 +536,8 @@ extern Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p ); /*=== giaEquiv.c ==========================================================*/ extern int Gia_ManCheckTopoOrder( Gia_Man_t * p ); extern int * Gia_ManDeriveNexts( Gia_Man_t * p ); +extern void Gia_ManDeriveReprs( Gia_Man_t * p ); +extern int Gia_ManEquivCountClasses( Gia_Man_t * p ); extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter ); extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ); extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose ); @@ -544,6 +547,7 @@ extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int f extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut ); extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ); extern void Gia_ManEquivImprove( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots ); /*=== giaFanout.c =========================================================*/ extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); extern void Gia_ObjRemoveFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); @@ -629,6 +633,8 @@ extern Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut ); extern void Gia_ManPrintCounterExample( Gia_Cex_t * p ); extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ); +extern int Gia_ManHasChoices( Gia_Man_t * p ); +extern int Gia_ManHasDandling( Gia_Man_t * p ); #ifdef __cplusplus } diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index 601b85af..a4f1ab44 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -45,19 +45,24 @@ static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t * SeeAlso [] ***********************************************************************/ -void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Obj_t * pObj ) +void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) { - if ( pObj->pData ) + Aig_Obj_t * pNext; + if ( pObj->iData ) return; - if ( Aig_ObjIsPi(pObj) ) - { - pObj->iData = Gia_ManAppendCi( pNew ); - return; - } assert( Aig_ObjIsNode(pObj) ); - Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) ); - Gia_ManFromAig_rec( pNew, Aig_ObjFanin1(pObj) ); + Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) ); + Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin1(pObj) ); pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) ); + if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) ) + { + int iObjNew, iNextNew; + Gia_ManFromAig_rec( pNew, p, pNext ); + iObjNew = Gia_Lit2Var(pObj->iData); + iNextNew = Gia_Lit2Var(pNext->iData); + if ( pNew->pNexts ) + pNew->pNexts[iObjNew] = iNextNew; + } } /**Function************************************************************* @@ -76,26 +81,25 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ) Gia_Man_t * pNew; Aig_Obj_t * pObj; int i; - // add fake POs to all the dangling nodes (choices) - Aig_ManForEachNode( p, pObj, i ) - assert( Aig_ObjRefs(pObj) > 0 ); // create the new manager pNew = Gia_ManStart( Aig_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); + // create room to store equivalences + if ( p->pEquivs ) + pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) ); // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->iData = 1; Aig_ManForEachPi( p, pObj, i ) - { -// if ( Aig_ObjRefs(pObj) == 0 ) - pObj->iData = Gia_ManAppendCi( pNew ); - } + pObj->iData = Gia_ManAppendCi( pNew ); // add logic for the POs Aig_ManForEachPo( p, pObj, i ) - Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) ); + Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) ); Aig_ManForEachPo( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) ); Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) ); + if ( pNew->pNexts ) + Gia_ManDeriveReprs( pNew ); return pNew; } @@ -117,7 +121,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ) int i; // create the new manager pNew = Gia_ManStart( Aig_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Gia_UtilStrsav( p->pName ); // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->iData = 1; @@ -127,12 +131,12 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ) Aig_ManForEachNode( p, pObj, i ) if ( Aig_ObjRefs(pObj) == 0 ) { - Gia_ManFromAig_rec( pNew, pObj ); + Gia_ManFromAig_rec( pNew, p, pObj ); Gia_ManAppendCo( pNew, pObj->iData ); } // add logic for the POs Aig_ManForEachPo( p, pObj, i ) - Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) ); + Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) ); Aig_ManForEachPo( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) ); Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) ); @@ -152,17 +156,27 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ) ***********************************************************************/ void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gia_Obj_t * pObj ) { + Gia_Obj_t * pNext; if ( ppNodes[Gia_ObjId(p, pObj)] ) return; if ( Gia_ObjIsCi(pObj) ) - { ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew ); - return; + else + { + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) ); + Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) ); + ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) ); + } + if ( pNew->pEquivs && (pNext = Gia_ObjNextObj(p, Gia_ObjId(p, pObj))) ) + { + Aig_Obj_t * pObjNew, * pNextNew; + Gia_ManToAig_rec( pNew, ppNodes, p, pNext ); + pObjNew = ppNodes[Gia_ObjId(p, pObj)]; + pNextNew = ppNodes[Gia_ObjId(p, pNext)]; + if ( pNew->pEquivs ) + pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew); } - assert( Gia_ObjIsAnd(pObj) ); - Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) ); - Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) ); - ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) ); } /**Function************************************************************* @@ -176,37 +190,31 @@ void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gi SeeAlso [] ***********************************************************************/ -Aig_Man_t * Gia_ManToAig( Gia_Man_t * p ) +Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ) { Aig_Man_t * pNew; Aig_Obj_t ** ppNodes; Gia_Obj_t * pObj; int i; - + assert( !fChoices || (p->pNexts && p->pReprs) ); // create the new manager pNew = Aig_ManStart( Gia_ManAndNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); - ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); +// pNew->pSpec = Gia_UtilStrsav( p->pName ); + // duplicate representation of choice nodes + if ( fChoices ) + pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) ); // create the PIs + ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) ); ppNodes[0] = Aig_ManConst0(pNew); Gia_ManForEachCi( p, pObj, i ) - { -// if ( Aig_ObjRefs(pObj) == 0 ) - ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew ); - } - + ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew ); // add logic for the POs Gia_ManForEachCo( p, pObj, i ) { Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) ); ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) ); } -/* - Gia_ManForEachCo( p, pObj, i ) - Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) ); - Gia_ManForEachCo( p, pObj, i ) - ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) ); -*/ Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) ); ABC_FREE( ppNodes ); return pNew; @@ -230,7 +238,7 @@ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit ) pGia = Gia_ManFromAig( p ); pGia = Gia_ManUnrollAndCofactor( pTemp = pGia, nFrames, nCofFanLit, 1 ); Gia_ManStop( pTemp ); - pMan = Gia_ManToAig( pGia ); + pMan = Gia_ManToAig( pGia, 0 ); Gia_ManStop( pGia ); return pMan; } diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h index 07cf7bae..0c0ee598 100644 --- a/src/aig/gia/giaAig.h +++ b/src/aig/gia/giaAig.h @@ -48,7 +48,7 @@ /*=== giaAig.c =============================================================*/ extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ); extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ); -extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p ); +extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ); #ifdef __cplusplus } diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 8dbc0cab..afe9164f 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -413,7 +413,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ) pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 ); pName = Gia_FileNameGeneric( pFileName ); pNew->pName = Gia_UtilStrsav( pName ); -// pNew->pSpec = Aig_UtilStrsav( pFileName ); +// pNew->pSpec = Gia_UtilStrsav( pFileName ); ABC_FREE( pName ); // prepare the array of nodes diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index bd5297e4..63748403 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -387,6 +387,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ) { if ( pObj->fMark0 ) continue; + pObj->fMark0 = 0; if ( Gia_ObjIsAnd(pObj) ) pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); else if ( Gia_ObjIsCi(pObj) ) @@ -396,14 +397,32 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ) } else if ( Gia_ObjIsCo(pObj) ) { - Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj); - +// Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj); pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); nRis += Gia_ObjIsRi(p, pObj); } } assert( nRos == nRis ); Gia_ManSetRegNum( pNew, nRos ); + if ( p->pReprs && p->pNexts ) + { + Gia_Obj_t * pRepr; + pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + Gia_ObjSetRepr( pNew, i, GIA_VOID ); + Gia_ManForEachObj1( p, pObj, i ) + { + if ( !~pObj->Value ) + continue; + pRepr = Gia_ObjReprObj( p, i ); + if ( pRepr == NULL ) + continue; + assert( ~pRepr->Value ); + if ( Gia_Lit2Var(pObj->Value) != Gia_Lit2Var(pRepr->Value) ) + Gia_ObjSetRepr( pNew, Gia_Lit2Var(pObj->Value), Gia_Lit2Var(pRepr->Value) ); + } + pNew->pNexts = Gia_ManDeriveNexts( pNew ); + } return pNew; } diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index f802e15d..cdee73d0 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -94,7 +94,8 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p ) { unsigned * pNexts, * pTails; int i; - assert( p->pReprs ); + assert( p->pReprs != NULL ); + assert( p->pNexts == NULL ); pNexts = ABC_CALLOC( unsigned, Gia_ManObjNum(p) ); pTails = ABC_ALLOC( unsigned, Gia_ManObjNum(p) ); for ( i = 0; i < Gia_ManObjNum(p); i++ ) @@ -112,6 +113,37 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p ) /**Function************************************************************* + Synopsis [Given points to the next objects, derives representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDeriveReprs( Gia_Man_t * p ) +{ + int i, iObj; + assert( p->pReprs == NULL ); + assert( p->pNexts != NULL ); + p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + Gia_ObjSetRepr( p, i, GIA_VOID ); + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + { + if ( p->pNexts[i] == 0 ) + continue; + if ( p->pReprs[i].iRepr != GIA_VOID ) + continue; + // next is set, repr is not set + for ( iObj = p->pNexts[i]; iObj; iObj = p->pNexts[iObj] ) + p->pReprs[iObj].iRepr = i; + } +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -186,6 +218,25 @@ int Gia_ManEquivCountLitsAll( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ +int Gia_ManEquivCountClasses( Gia_Man_t * p ) +{ + int i, Counter = 0; + for ( i = 1; i < Gia_ManObjNum(p); i++ ) + Counter += Gia_ObjIsHead(p, i); + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits ) { int nLitsReal = Gia_ManEquivCountLitsAll( p ); @@ -966,6 +1017,246 @@ void Gia_ManEquivImprove( Gia_Man_t * p ) // p->pNexts = Gia_ManDeriveNexts( p ); } + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNode.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ObjCheckTfi_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode, Vec_Ptr_t * vVisited ) +{ + // check the trivial cases + if ( pNode == NULL ) + return 0; + if ( Gia_ObjIsCi(pNode) ) + return 0; +// if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode +// return 0; + if ( pNode == pOld ) + return 1; + // skip the visited node + if ( pNode->fMark0 ) + return 0; + pNode->fMark0 = 1; + Vec_PtrPush( vVisited, pNode ); + // check the children + if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin0(pNode), vVisited ) ) + return 1; + if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin1(pNode), vVisited ) ) + return 1; + // check equivalent nodes + return Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjNextObj(p, Gia_ObjId(p, pNode)), vVisited ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNode.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ObjCheckTfi( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode ) +{ + Vec_Ptr_t * vVisited; + Gia_Obj_t * pObj; + int RetValue, i; + assert( !Gia_IsComplement(pOld) ); + assert( !Gia_IsComplement(pNode) ); + vVisited = Vec_PtrAlloc( 100 ); + RetValue = Gia_ObjCheckTfi_rec( p, pOld, pNode, vVisited ); + Vec_PtrForEachEntry( vVisited, pObj, i ) + pObj->fMark0 = 0; + Vec_PtrFree( vVisited ); + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [Adds the next entry while making choices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManAddNextEntry_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode ) +{ + if ( Gia_ObjNext(p, Gia_ObjId(p, pOld)) == 0 ) + { + Gia_ObjSetNext( p, Gia_ObjId(p, pOld), Gia_ObjId(p, pNode) ); + return; + } + Gia_ManAddNextEntry_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pOld)), pNode ); +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + Gia_Obj_t * pRepr, * pReprNew, * pObjNew; + if ( ~pObj->Value ) + return; + if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) + { + if ( Gia_ObjIsConst0(pRepr) ) + { + pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + return; + } + Gia_ManEquivToChoices_rec( pNew, p, pRepr ); + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) ); + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( Gia_LitRegular(pObj->Value) == Gia_LitRegular(pRepr->Value) ) + { + assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) ); + return; + } + assert( pRepr->Value < pObj->Value ); + pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) ); + pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) ); + if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) ) + { + assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew ); + pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + return; + } + if ( !Gia_ObjCheckTfi( pNew, pReprNew, pObjNew ) ) + { + assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 ); + Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) ); + Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew ); + } + pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) ); + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Removes choices, which contain fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManRemoveBadChoices( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, iObj, iPrev, Counter = 0; + // mark nodes with fanout + Gia_ManForEachObj( p, pObj, i ) + { + pObj->fMark0 = 0; + if ( Gia_ObjIsAnd(pObj) ) + { + Gia_ObjFanin0(pObj)->fMark0 = 1; + Gia_ObjFanin1(pObj)->fMark0 = 1; + } + else if ( Gia_ObjIsCo(pObj) ) + Gia_ObjFanin0(pObj)->fMark0 = 1; + } + // go through the classes and remove + Gia_ManForEachClass( p, i ) + { + for ( iPrev = i, iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iPrev) ) + { + if ( !Gia_ManObj(p, iObj)->fMark0 ) + { + iPrev = iObj; + continue; + } + Gia_ObjSetRepr( p, iObj, GIA_VOID ); + Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) ); + Gia_ObjSetNext( p, iObj, 0 ); + Counter++; + } + } + // remove the marks + Gia_ManCleanMark0( p ); +// printf( "Removed %d bad choices.\n", Counter ); +} + +/**Function************************************************************* + + Synopsis [Reduces AIG using equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pRepr; + int i; + assert( (Gia_ManCoNum(p) % nSnapshots) == 0 ); + Gia_ManSetPhase( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); + pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) ); + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + Gia_ObjSetRepr( pNew, i, GIA_VOID ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachRo( p, pObj, i ) + if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) + { + assert( Gia_ObjIsConst0(pRepr) || Gia_ObjIsRo(p, pRepr) ); + pObj->Value = pRepr->Value; + } + Gia_ManHashAlloc( pNew ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + if ( i % nSnapshots == 0 ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + Gia_ManRemoveBadChoices( pNew ); +// Gia_ManEquivPrintClasses( pNew, 0, 0 ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); +// Gia_ManEquivPrintClasses( pNew, 0, 0 ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index f69ac266..7f4da081 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -158,7 +158,7 @@ void Gia_ManPrintPlacement( Gia_Man_t * p ) void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ) { if ( p->pName ) - printf( "%8s : ", p->pName ); + printf( "%-8s : ", p->pName ); printf( "i/o =%7d/%7d", Gia_ManPiNum(p), Gia_ManPoNum(p) ); if ( Gia_ManRegNum(p) ) printf( " ff =%7d", Gia_ManRegNum(p) ); @@ -166,6 +166,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ) printf( " lev =%5d", Gia_ManLevelNum(p) ); printf( " cut =%5d", Gia_ManCrossCut(p) ); printf( " mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) ); + if ( Gia_ManHasDandling(p) ) + printf( " ch =%5d", Gia_ManEquivCountClasses(p) ); if ( fSwitch ) { if ( p->pSwitching ) diff --git a/src/aig/gia/giaScl.c b/src/aig/gia/giaScl.c index cf72104f..5ac8e04a 100644 --- a/src/aig/gia/giaScl.c +++ b/src/aig/gia/giaScl.c @@ -41,12 +41,15 @@ ***********************************************************************/ int Gia_ManCombMarkUsed_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) { + if ( pObj == NULL ) + return 0; if ( !pObj->fMark0 ) return 0; pObj->fMark0 = 0; assert( Gia_ObjIsAnd(pObj) ); return 1 + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin0(pObj) ) - + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin1(pObj) ); + + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin1(pObj) ) + + (p->pNexts ? Gia_ManCombMarkUsed_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pObj)) ) : 0); } /**Function************************************************************* @@ -88,6 +91,7 @@ Gia_Man_t * Gia_ManCleanup( Gia_Man_t * p ) return Gia_ManDupMarked( p ); } + /**Function************************************************************* Synopsis [Marks CIs/COs/ANDs unreachable from POs.] diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 5716c1a0..54bc98dd 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -858,6 +858,114 @@ int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ) return ConeSize1; } +/**Function************************************************************* + + Synopsis [Returns 1 if AIG has choices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManHasChoices( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, Counter1 = 0, Counter2 = 0; + int nFailNoRepr = 0; + int nFailHaveRepr = 0; + int nChoiceNodes = 0; + int nChoices = 0; + if ( p->pReprs == NULL || p->pNexts == NULL ) + return 0; + // check if there are any representatives + Gia_ManForEachObj( p, pObj, i ) + { + if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) ) + Counter1++; + if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) ) + Counter2++; + } + if ( Counter1 == 0 ) + { + printf( "Warning: AIG has repr data-strucure but not reprs.\n" ); + return 0; + } +// printf( "%d nodes have reprs.\n", Counter1 ); +// printf( "%d nodes have nexts.\n", Counter2 ); + // check if there are any internal nodes without fanout + // make sure all nodes without fanout have representatives + // make sure all nodes with fanout have no representatives + ABC_FREE( p->pRefs ); + Gia_ManCreateRefs( p ); + Gia_ManForEachAnd( p, pObj, i ) + { + if ( Gia_ObjRefs(p, pObj) == 0 ) + { + if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL ) + nFailNoRepr++; + else + nChoices++; + } + else + { + if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL ) + nFailHaveRepr++; + if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL ) + nChoiceNodes++; + } + if ( Gia_ObjReprObj( p, i ) ) + assert( Gia_ObjRepr(p, i) < i ); + } + if ( nChoices == 0 ) + return 0; + if ( nFailNoRepr ) + { + printf( "Gia_ManHasChoices(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr ); +// return 0; + } + if ( nFailHaveRepr ) + { + printf( "Gia_ManHasChoices(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr ); +// return 0; + } +// printf( "Gia_ManHasChoices(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if AIG has dangling nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManHasDandling( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, Counter = 0; + Gia_ManForEachObj( p, pObj, i ) + { + pObj->fMark0 = 0; + if ( Gia_ObjIsAnd(pObj) ) + { + Gia_ObjFanin0(pObj)->fMark0 = 1; + Gia_ObjFanin1(pObj)->fMark0 = 1; + } + else if ( Gia_ObjIsCo(pObj) ) + Gia_ObjFanin0(pObj)->fMark0 = 1; + } + Gia_ManForEachAnd( p, pObj, i ) + Counter += !pObj->fMark0; + Gia_ManCleanMark0( p ); + return Counter; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ivy/ivyRwr.c b/src/aig/ivy/ivyRwr.c index 8bfeb03c..af425079 100644 --- a/src/aig/ivy/ivyRwr.c +++ b/src/aig/ivy/ivyRwr.c @@ -96,9 +96,9 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV } if ( nGain > 0 ) { // print stats on the MFFC - extern void Ivy_NodeMffsConeSuppPrint( Ivy_Obj_t * pNode ); + extern void Ivy_NodeMffcConeSuppPrint( Ivy_Obj_t * pNode ); printf( "Node %6d : Gain = %4d ", pNode->Id, nGain ); - Ivy_NodeMffsConeSuppPrint( pNode ); + Ivy_NodeMffcConeSuppPrint( pNode ); } */ // complement the FF if needed diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index 8fce7904..ce6ebf85 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -392,7 +392,7 @@ void Ssw_ClassesPrintOne( Ssw_Cla_t * p, Aig_Obj_t * pRepr ) printf( "{ " ); Ssw_ClassForEachNode( p, pRepr, pObj, i ) printf( "%d(%d,%d,%d) ", pObj->Id, pObj->Level, - Aig_SupportSize(p->pAig,pObj), Aig_NodeMffsSupp(p->pAig,pObj,0,NULL) ); + Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) ); printf( "}\n" ); } @@ -420,7 +420,7 @@ void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose ) Aig_ManForEachObj( p->pAig, pObj, i ) if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) printf( "%d(%d,%d,%d) ", pObj->Id, pObj->Level, - Aig_SupportSize(p->pAig,pObj), Aig_NodeMffsSupp(p->pAig,pObj,0,NULL) ); + Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) ); printf( "}\n" ); Ssw_ManForEachClass( p, ppClass, i ) { diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 2869352c..73a487e9 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -779,7 +779,7 @@ extern ABC_DLL int Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode ); extern ABC_DLL int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode ); extern ABC_DLL int Abc_NodeMffcLabelAig( Abc_Obj_t * pNode ); extern ABC_DLL int Abc_NodeMffcLabel( Abc_Obj_t * pNode ); -extern ABC_DLL void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ); +extern ABC_DLL void Abc_NodeMffcConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ); extern ABC_DLL int Abc_NodeDeref_rec( Abc_Obj_t * pNode ); extern ABC_DLL int Abc_NodeRef_rec( Abc_Obj_t * pNode ); /*=== abcRefactor.c ==========================================================*/ diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index d6ab7ea1..3e233d90 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -741,7 +741,7 @@ Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode vCone = Vec_PtrAlloc( 100 ); vSupp = Vec_PtrAlloc( 100 ); Abc_NodeDeref_rec( pNode ); - Abc_NodeMffsConeSupp( pNode, vCone, vSupp ); + Abc_NodeMffcConeSupp( pNode, vCone, vSupp ); Abc_NodeRef_rec( pNode ); // create the PIs Vec_PtrForEachEntry( vSupp, pObj, i ) diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c index fadb492a..ec89eaed 100644 --- a/src/base/abc/abcRefs.c +++ b/src/base/abc/abcRefs.c @@ -260,7 +260,7 @@ int Abc_NodeRef_rec( Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost ) +void Abc_NodeMffcConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost ) { Abc_Obj_t * pFanin; int i; @@ -276,7 +276,7 @@ void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * } // recur on the children Abc_ObjForEachFanin( pNode, pFanin, i ) - Abc_NodeMffsConeSupp_rec( pFanin, vCone, vSupp, 0 ); + Abc_NodeMffcConeSupp_rec( pFanin, vCone, vSupp, 0 ); // collect the internal node if ( vCone ) Vec_PtrPush( vCone, pNode ); // printf( "%d ", pNode->Id ); @@ -293,14 +293,14 @@ void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * SeeAlso [] ***********************************************************************/ -void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ) +void Abc_NodeMffcConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ) { assert( Abc_ObjIsNode(pNode) ); assert( !Abc_ObjIsComplement(pNode) ); if ( vCone ) Vec_PtrClear( vCone ); if ( vSupp ) Vec_PtrClear( vSupp ); Abc_NtkIncrementTravId( pNode->pNtk ); - Abc_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 ); + Abc_NodeMffcConeSupp_rec( pNode, vCone, vSupp, 1 ); // printf( "\n" ); } @@ -315,7 +315,7 @@ void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSu SeeAlso [] ***********************************************************************/ -void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode ) +void Abc_NodeMffcConeSuppPrint( Abc_Obj_t * pNode ) { Vec_Ptr_t * vCone, * vSupp; Abc_Obj_t * pObj; @@ -323,7 +323,7 @@ void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode ) vCone = Vec_PtrAlloc( 100 ); vSupp = Vec_PtrAlloc( 100 ); Abc_NodeDeref_rec( pNode ); - Abc_NodeMffsConeSupp( pNode, vCone, vSupp ); + Abc_NodeMffcConeSupp( pNode, vCone, vSupp ); Abc_NodeRef_rec( pNode ); printf( "Node = %6s : Supp = %3d Cone = %3d (", Abc_ObjName(pNode), Vec_PtrSize(vSupp), Vec_PtrSize(vCone) ); @@ -345,7 +345,7 @@ void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside ) +int Abc_NodeMffcInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside ) { Abc_Obj_t * pObj; int i, Count1, Count2; @@ -355,7 +355,7 @@ int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vIns // dereference the node Count1 = Abc_NodeDeref_rec( pNode ); // collect the nodes inside the MFFC - Abc_NodeMffsConeSupp( pNode, vInside, NULL ); + Abc_NodeMffcConeSupp( pNode, vInside, NULL ); // reference it back Count2 = Abc_NodeRef_rec( pNode ); assert( Count1 == Count2 ); @@ -376,7 +376,7 @@ int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vIns SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode ) +Vec_Ptr_t * Abc_NodeMffcInsideCollect( Abc_Obj_t * pNode ) { Vec_Ptr_t * vInside; int Count1, Count2; @@ -384,7 +384,7 @@ Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode ) Count1 = Abc_NodeDeref_rec( pNode ); // collect the nodes inside the MFFC vInside = Vec_PtrAlloc( 10 ); - Abc_NodeMffsConeSupp( pNode, vInside, NULL ); + Abc_NodeMffcConeSupp( pNode, vInside, NULL ); // reference it back Count2 = Abc_NodeRef_rec( pNode ); assert( Count1 == Count2 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c48b7e95..8ac8b241 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -9515,7 +9515,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Dch_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcvh" ) ) != EOF ) { switch ( c ) { @@ -9561,6 +9561,12 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': pPars->fSimulateTfo ^= 1; break; + case 'g': + pPars->fUseGia ^= 1; + break; + case 'c': + pPars->fUseCSat ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -9591,7 +9597,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dch [-WCS num] [-sptvh]\n" ); + fprintf( pErr, "usage: dch [-WCS num] [-sptgcvh]\n" ); fprintf( pErr, "\t computes structural choices using a new approach\n" ); fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords ); fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); @@ -9599,6 +9605,8 @@ usage: fprintf( pErr, "\t-s : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" ); fprintf( pErr, "\t-p : toggle power-aware rewriting [default = %s]\n", pPars->fPower? "yes": "no" ); fprintf( pErr, "\t-t : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" ); + fprintf( pErr, "\t-g : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" ); + fprintf( pErr, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -21820,6 +21828,7 @@ usage: int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + extern Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk ); Gia_Man_t * pAig; Aig_Man_t * pMan; int c, fVerbose = 0; @@ -21845,12 +21854,15 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "The current network should be strashed.\n" ); return 1; } +// if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) ) +// { +// printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pAbc->pNtkCur) ); +// Abc_AigCleanup(pAbc->pNtkCur->pManFunc); +// } if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) ) - { - printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pAbc->pNtkCur) ); - Abc_AigCleanup(pAbc->pNtkCur->pManFunc); - } - pMan = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 ); + pMan = Abc_NtkToDarChoices( pAbc->pNtkCur ); + else + pMan = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 ); pAig = Gia_ManFromAig( pMan ); Aig_ManStop( pMan ); if ( pAig == NULL ) @@ -21886,6 +21898,7 @@ usage: int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); + extern Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ); Aig_Man_t * pMan; FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -21917,9 +21930,27 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } - pMan = Gia_ManToAig( pAbc->pAig ); - pNtk = Abc_NtkFromAigPhase( pMan ); - Aig_ManStop( pMan ); + if ( Gia_ManHasDandling(pAbc->pAig) == 0 ) + { + pMan = Gia_ManToAig( pAbc->pAig, 0 ); + pNtk = Abc_NtkFromAigPhase( pMan ); + Aig_ManStop( pMan ); + } + else + { + Abc_Ntk_t * pNtkNoCh; +// printf( "Transforming AIG with %d choice nodes.\n", Gia_ManEquivCountClasses(pAbc->pAig) ); + // create network without choices + pMan = Gia_ManToAig( pAbc->pAig, 0 ); + pNtkNoCh = Abc_NtkFromAigPhase( pMan ); + pNtkNoCh->pName = Extra_UtilStrsav(pMan->pName); + Aig_ManStop( pMan ); + // derive network with choices + pMan = Gia_ManToAig( pAbc->pAig, 1 ); + pNtk = Abc_NtkFromDarChoices( pNtkNoCh, pMan ); + Abc_NtkDelete( pNtkNoCh ); + Aig_ManStop( pMan ); + } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); return 0; @@ -22204,7 +22235,7 @@ int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc9Show(): There is no AIG.\n" ); return 1; } - pMan = Gia_ManToAig( pAbc->pAig ); + pMan = Gia_ManToAig( pAbc->pAig, 0 ); Aig_ManShow( pMan, 0, NULL ); Aig_ManStop( pMan ); return 0; @@ -23400,7 +23431,7 @@ usage: fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); - fprintf( stdout, "\t-r : toggle using implication rings for equivalence classes [default = %s]\n", pPars->fUseRings? "yes": "no" ); + fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" ); fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); @@ -23425,7 +23456,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Cec_ManCorSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrecvh" ) ) != EOF ) { switch ( c ) { @@ -23457,6 +23488,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': pPars->fUseRings ^= 1; break; + case 'e': + pPars->fMakeChoices ^= 1; + break; case 'c': pPars->fUseCSat ^= 1; break; @@ -23483,12 +23517,13 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &scorr [-FC num] [-frcvh]\n" ); + fprintf( stdout, "usage: &scorr [-FC num] [-frecvh]\n" ); fprintf( stdout, "\t performs signal correpondence computation\n" ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); - fprintf( stdout, "\t-r : toggle using implication rings for equivalence classes [default = %s]\n", pPars->fUseRings? "yes": "no" ); + fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" ); + fprintf( stdout, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" ); fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); @@ -23513,7 +23548,7 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Cec_ManChcSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Ccvh" ) ) != EOF ) { switch ( c ) { @@ -23528,6 +23563,9 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nBTLimit < 0 ) goto usage; break; + case 'c': + pPars->fUseCSat ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -23540,8 +23578,6 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc9Choice(): There is no AIG.\n" ); return 1; } - printf("The command is not yet ready.\n" ); - return 0; pAbc->pAig = Cec_ManChoiceComputation( pTemp = pAbc->pAig, pPars ); if ( pAbc->pAig == NULL ) { @@ -23553,9 +23589,10 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &choice [-C num] [-vh]\n" ); + fprintf( stdout, "usage: &choice [-C num] [-cvh]\n" ); fprintf( stdout, "\t performs computation of structural choices\n" ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); + fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c index 48c2f8e0..cc97796f 100644 --- a/src/base/abci/abcCut.c +++ b/src/base/abci/abcCut.c @@ -586,7 +586,7 @@ Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) Abc_Obj_t * pObj;//, * pTemp; int i;//, k; int nNodesTotal = 0, nMffcsTotal = 0; - extern Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode ); + extern Vec_Ptr_t * Abc_NodeMffcInsideCollect( Abc_Obj_t * pNode ); vAttrs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) + 1 ); // Abc_NtkForEachCi( pNtk, pObj, i ) @@ -615,7 +615,7 @@ Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) { if ( Vec_IntEntry( vAttrs, pObj->Id ) ) { - vNodes = Abc_NodeMffsInsideCollect( pObj ); + vNodes = Abc_NodeMffcInsideCollect( pObj ); Vec_PtrForEachEntry( vNodes, pTemp, k ) if ( pTemp != pObj ) Vec_IntWriteEntry( vAttrs, pTemp->Id, 0 ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 840068d6..a5973153 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -896,6 +896,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars ) { extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose ); + extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); Vec_Ptr_t * vAigs; Aig_Man_t * pMan, * pTemp; @@ -911,6 +912,10 @@ clk = clock(); // vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fVerbose ); vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 ); Aig_ManStop( pMan ); + // swap around the first and the last + pTemp = Vec_PtrPop( vAigs ); + Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) ); + Vec_PtrWriteEntry( vAigs, 0, pTemp ); } else { @@ -918,7 +923,10 @@ clk = clock(); Vec_PtrPush( vAigs, pMan ); } pPars->timeSynth = clock() - clk; - pMan = Dch_ComputeChoices( vAigs, pPars ); + if ( pPars->fUseGia ) + pMan = Cec_ComputeChoices( vAigs, pPars ); + else + pMan = Dch_ComputeChoices( vAigs, pPars ); pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan ); // pNtkAig = Abc_NtkFromDar( pNtk, pMan ); Aig_ManStop( pMan ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index d47dfe1f..10e3ba2d 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -704,9 +704,9 @@ void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk ) { Abc_Obj_t * pNode; int i; - extern void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode ); + extern void Abc_NodeMffcConeSuppPrint( Abc_Obj_t * pNode ); Abc_NtkForEachNode( pNtk, pNode, i ) - Abc_NodeMffsConeSuppPrint( pNode ); + Abc_NodeMffcConeSuppPrint( pNode ); } /**Function************************************************************* diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index 861a5e66..655f158e 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -1624,7 +1624,7 @@ void Abc_ManResubCleanup( Abc_ManRes_t * p ) ***********************************************************************/ Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps, bool fUpdateLevel, bool fVerbose ) { - extern int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside ); + extern int Abc_NodeMffcInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside ); Dec_Graph_t * pGraph; int Required; int clk; @@ -1639,7 +1639,7 @@ Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * // collect the MFFC clk = clock(); - p->nMffc = Abc_NodeMffsInside( pRoot, vLeaves, p->vTemp ); + p->nMffc = Abc_NodeMffcInside( pRoot, vLeaves, p->vTemp ); p->timeMffc += clock() - clk; assert( p->nMffc > 0 ); diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index 8957743c..54db0641 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -728,7 +728,7 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f // write the comment fprintfBz2Aig( &b, "c" ); if ( pNtk->pName && strlen(pNtk->pName) > 0 ) - fprintfBz2Aig( &b, "n%s%c", pNtk->pName, '\0' ); + fprintfBz2Aig( &b, "\n%s%c", pNtk->pName, '\0' ); fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() ); fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" ); |