diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/cnf/cnf.h | 2 | ||||
-rw-r--r-- | src/aig/cnf/cnfMan.c | 93 | ||||
-rw-r--r-- | src/aig/cnf/cnfUtil.c | 1 | ||||
-rw-r--r-- | src/aig/fra/fra.h | 2 | ||||
-rw-r--r-- | src/aig/fra/fraCec.c | 35 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 2 | ||||
-rw-r--r-- | src/aig/ntl/ntl.h | 1 | ||||
-rw-r--r-- | src/aig/ntl/ntlExtract.c | 4 | ||||
-rw-r--r-- | src/aig/ntl/ntlFraig.c | 4 | ||||
-rw-r--r-- | src/aig/ntl/ntlUtil.c | 58 | ||||
-rw-r--r-- | src/aig/nwk/nwkTiming.c | 20 | ||||
-rw-r--r-- | src/aig/saig/saigInter.c | 2 |
12 files changed, 198 insertions, 26 deletions
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index bf109b17..5c742f5d 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -140,6 +140,8 @@ extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ); extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); extern int Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf ); +extern int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ); +extern void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf ); /*=== cnfMap.c ========================================================*/ extern void Cnf_DeriveMapping( Cnf_Man_t * p ); extern int Cnf_ManMapForCnf( Cnf_Man_t * p ); diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index fc71f936..e3e6bfe1 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -20,6 +20,7 @@ #include "cnf.h" #include "satSolver.h" +#include "zlib.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -237,7 +238,7 @@ void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ) SeeAlso [] ***********************************************************************/ -void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ) +void Cnf_DataWriteIntoFile_old( Cnf_Dat_t * p, char * pFileName, int fReadable ) { FILE * pFile; int * pLit, * pStop, i; @@ -270,6 +271,39 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ) SeeAlso [] ***********************************************************************/ +void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ) +{ + gzFile pFile; + int * pLit, * pStop, i; + pFile = gzopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" ); + return; + } + gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" ); + gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); + for ( i = 0; i < p->nClauses; i++ ) + { + for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) + gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); + gzprintf( pFile, "0\n" ); + } + gzprintf( pFile, "\n" ); + gzclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Writes CNF into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ) { sat_solver * pSat; @@ -379,6 +413,63 @@ int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) return 1; } +/**Function************************************************************* + + Synopsis [Adds the OR-clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ) +{ + sat_solver * pSat = p; + Aig_Obj_t * pObj; + int i, Lit; + Aig_ManForEachPo( pCnf->pMan, pObj, i ) + { + Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Transforms polarity of the internal veriables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf ) +{ + Aig_Obj_t * pObj; + int * pVarToPol; + int i, iVar; + // create map from the variable number to its polarity + pVarToPol = CALLOC( int, pCnf->nVars ); + Aig_ManForEachObj( pCnf->pMan, pObj, i ) + if ( !Aig_ObjIsPo(pObj) && pCnf->pVarNums[pObj->Id] >= 0 ) + pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase; + // transform literals + for ( i = 0; i < pCnf->nLiterals; i++ ) + { + iVar = lit_var(pCnf->pClauses[0][i]); + assert( iVar < pCnf->nVars ); + if ( pVarToPol[iVar] ) + pCnf->pClauses[0][i] = lit_neg( pCnf->pClauses[0][i] ); + } + free( pVarToPol ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c index cd47cb58..3738fee5 100644 --- a/src/aig/cnf/cnfUtil.c +++ b/src/aig/cnf/cnfUtil.c @@ -140,6 +140,7 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped else { pCutBest = pObj->pData; +// assert( pCutBest->nFanins > 0 ); assert( pCutBest->Cost < 127 ); aArea = pCutBest->Cost; Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i ) diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index e9e7ad9c..6721634e 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -282,7 +282,7 @@ static inline int Fra_ImpCreate( int Left, int Right ) //////////////////////////////////////////////////////////////////////// /*=== fraCec.c ========================================================*/ -extern int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ); +extern int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ); extern int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose ); extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose ); /*=== fraClass.c ========================================================*/ diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index d67839a4..e5940992 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -40,7 +40,7 @@ SeeAlso [] ***********************************************************************/ -int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ) +int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ) { sat_solver * pSat; Cnf_Dat_t * pCnf; @@ -53,6 +53,10 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe // derive CNF pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) ); // pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); + + if ( fFlipBits ) + Cnf_DataTranformPolarity( pCnf ); + // convert into SAT solver pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); if ( pSat == NULL ) @@ -60,12 +64,27 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe Cnf_DataFree( pCnf ); return 1; } - // add the OR clause for the outputs - if ( !Cnf_DataWriteOrClause( pSat, pCnf ) ) + + + if ( fAndOuts ) { - sat_solver_delete( pSat ); - Cnf_DataFree( pCnf ); - return 1; + // assert each output independently + if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) ) + { + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return 1; + } + } + else + { + // add the OR clause for the outputs + if ( !Cnf_DataWriteOrClause( pSat, pCnf ) ) + { + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return 1; + } } vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); Cnf_DataFree( pCnf ); @@ -160,7 +179,7 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose ) // if SAT only, solve without iteration clk = clock(); - RetValue = Fra_FraigSat( pAig, (sint64)2*nBTLimitStart, (sint64)0, 0 ); + RetValue = Fra_FraigSat( pAig, (sint64)2*nBTLimitStart, (sint64)0, 1, 0, 0 ); if ( fVerbose ) { printf( "Initial SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) ); @@ -228,7 +247,7 @@ PRT( "Time", clock() - clk ); if ( RetValue == -1 ) { clk = clock(); - RetValue = Fra_FraigSat( pAig, (sint64)nBTLimitLast, (sint64)0, 0 ); + RetValue = Fra_FraigSat( pAig, (sint64)nBTLimitLast, (sint64)0, 1, 0, 0 ); if ( fVerbose ) { printf( "Final SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) ); diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index ab076472..1935bb7f 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -437,6 +437,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams ) // start the fraig manager for this run p = Fra_ManStart( pManAig, pPars ); + p->pPars->nBTLimitNode = 0; // derive and refine e-classes using K initialized frames if ( fUseOldSimulation ) { @@ -529,6 +530,7 @@ p->timeTrav += clock() - clk2; pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); else pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); +// Cnf_DataTranformPolarity( pCnf ); //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index e1d3edd1..b0f3b1fb 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -377,6 +377,7 @@ extern ABC_DLL void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManSetZeroInitValues( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManTransformInitValues( Ntl_Man_t * p ); extern ABC_DLL Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVerbose ); +extern ABC_DLL void Ntl_ManFilterRegisterClasses( Aig_Man_t * pAig, Vec_Int_t * vRegClasses, int fVerbose ); extern ABC_DLL int Ntl_ManLatchNum( Ntl_Man_t * p ); extern ABC_DLL int Ntl_ManIsComb( Ntl_Man_t * p ); extern ABC_DLL int Ntl_ModelCombLeafNum( Ntl_Mod_t * p ); diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index f6f1ebb2..f4d33cf1 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -649,9 +649,9 @@ Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize ) if ( pAig->vClockDoms ) { if ( Vec_VecSize(pAig->vClockDoms) == 0 ) - printf( "Clock domains are small. Seq synthesis is not performed.\n" ); + printf( "Register classes are small. Seq synthesis is not performed.\n" ); else - printf( "Performing seq synthesis for %d clock domains.\n", Vec_VecSize(pAig->vClockDoms) ); + printf( "Performing seq synthesis for %d register classes.\n", Vec_VecSize(pAig->vClockDoms) ); printf( "\n" ); } return pAig; diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index 6449cc33..bd39956e 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -320,6 +320,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe // perform SCL for the given design pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose ); Aig_ManStop( pTemp ); + if ( pNew->vRegClasses && Vec_IntSize(pNew->vRegClasses) && pAigCol->pReprs ) + Ntl_ManFilterRegisterClasses( pAigCol, pNew->vRegClasses, fVerbose ); // finalize the transformation pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose ); @@ -353,6 +355,8 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose ) // perform SCL for the given design pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 ); Aig_ManStop( pTemp ); + if ( p->vRegClasses && Vec_IntSize(p->vRegClasses) && pAigCol->pReprs ) + Ntl_ManFilterRegisterClasses( pAigCol, p->vRegClasses, fVerbose ); // finalize the transformation pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose ); diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c index 4fd1762c..51f3b818 100644 --- a/src/aig/ntl/ntlUtil.c +++ b/src/aig/ntl/ntlUtil.c @@ -403,7 +403,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer printf( "The number of register clases = %d.\n", nClasses ); for ( i = 0; i <= ClassMax; i++ ) if ( pClassNums[i] ) - printf( "%d:%d ", i, pClassNums[i] ); + printf( "(%d, %d) ", i, pClassNums[i] ); printf( "\n" ); } // skip if there is only one class @@ -416,7 +416,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer vPart = Vec_IntStartNatural( Vec_IntSize(pMan->vRegClasses) ); Vec_PtrPush( vParts, vPart ); } - printf( "There is only one clock domain with %d registers.\n", Vec_IntSize(pMan->vRegClasses) ); + printf( "There is only one class with %d registers.\n", Vec_IntSize(pMan->vRegClasses) ); free( pClassNums ); return (Vec_Vec_t *)vParts; } @@ -434,12 +434,13 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer Vec_PtrPush( vParts, vPart ); } free( pClassNums ); + Vec_VecSort( (Vec_Vec_t *)vParts, 1 ); // report the selected classes if ( fVerbose ) { printf( "The number of selected register clases = %d.\n", Vec_PtrSize(vParts) ); Vec_PtrForEachEntry( vParts, vPart, i ) - printf( "%d:%d ", i, Vec_IntSize(vPart) ); + printf( "(%d, %d) ", i, Vec_IntSize(vPart) ); printf( "\n" ); } return (Vec_Vec_t *)vParts; @@ -447,6 +448,57 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer /**Function************************************************************* + Synopsis [Filter register clases using clock-domain information.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManFilterRegisterClasses( Aig_Man_t * pAig, Vec_Int_t * vRegClasses, int fVerbose ) +{ + Aig_Obj_t * pObj, * pRepr; + int i, k, nOmitted, nTotal; + if ( pAig->pReprs == NULL ) + return; + assert( pAig->nRegs > 0 ); + Aig_ManForEachPi( pAig, pObj, i ) + pObj->PioNum = -1; + k = 0; + Aig_ManForEachLoSeq( pAig, pObj, i ) + pObj->PioNum = k++; + // consider equivalences + nOmitted = nTotal = 0; + Aig_ManForEachObj( pAig, pObj, i ) + { + pRepr = pAig->pReprs[pObj->Id]; + if ( pRepr == NULL ) + continue; + nTotal++; + assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsPi(pRepr) || Aig_ObjIsConst1(pRepr) ); + if ( Aig_ObjIsConst1(pRepr) ) + continue; + assert( pObj->PioNum >= 0 && pRepr->PioNum >= 0 ); + // remove equivalence if they belong to different classes + if ( Vec_IntEntry( vRegClasses, pObj->PioNum ) == + Vec_IntEntry( vRegClasses, pRepr->PioNum ) ) + continue; + pAig->pReprs[pObj->Id] = NULL; + nOmitted++; + } + Aig_ManForEachPi( pAig, pObj, i ) + pObj->PioNum = -1; + if ( fVerbose ) + printf( "Omitted %d (out of %d) equivs due to register class mismatch.\n", + nOmitted, nTotal ); +} + + +/**Function************************************************************* + Synopsis [Counts the number of CIs in the model.] Description [] diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c index 64508474..fc56b387 100644 --- a/src/aig/nwk/nwkTiming.c +++ b/src/aig/nwk/nwkTiming.c @@ -589,14 +589,14 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj ) { if ( pManTime ) { - // it may happen that a box-input (CO) was already marked as visited - // when some other box-input of the same box was visited - here we undo this iBox = Tim_ManBoxForCo( pManTime, pTemp->PioId ); - if ( Tim_ManIsCoTravIdCurrent( pManTime, pTemp->PioId ) ) - Tim_ManSetPreviousTravIdBoxInputs( pManTime, iBox ); - Tim_ManSetCoArrival( pManTime, pTemp->PioId, tArrival ); if ( iBox >= 0 ) // this CO is an input of the box { + // it may happen that a box-input (CO) was already marked as visited + // when some other box-input of the same box was visited - here we undo this + if ( Tim_ManIsCoTravIdCurrent( pManTime, pTemp->PioId ) ) + Tim_ManSetPreviousTravIdBoxInputs( pManTime, iBox ); + Tim_ManSetCoArrival( pManTime, pTemp->PioId, tArrival ); Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox ); iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox ); nTerms = Tim_ManBoxOutputNum( pManTime, iBox ); @@ -673,14 +673,14 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj ) { if ( pManTime ) { - // it may happen that a box-output (CI) was already marked as visited - // when some other box-output of the same box was visited - here we undo this iBox = Tim_ManBoxForCi( pManTime, pTemp->PioId ); - if ( Tim_ManIsCiTravIdCurrent( pManTime, pTemp->PioId ) ) - Tim_ManSetPreviousTravIdBoxOutputs( pManTime, iBox ); - Tim_ManSetCiRequired( pManTime, pTemp->PioId, tRequired ); if ( iBox >= 0 ) // this CI is an output of the box { + // it may happen that a box-output (CI) was already marked as visited + // when some other box-output of the same box was visited - here we undo this + if ( Tim_ManIsCiTravIdCurrent( pManTime, pTemp->PioId ) ) + Tim_ManSetPreviousTravIdBoxOutputs( pManTime, iBox ); + Tim_ManSetCiRequired( pManTime, pTemp->PioId, tRequired ); Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox ); iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox ); nTerms = Tim_ManBoxInputNum( pManTime, iBox ); diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c index afc4a34a..ae8d02ec 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -412,7 +412,7 @@ int Saig_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ) pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); RetValue = Fra_FraigMiterStatus( pAigTemp ); Aig_ManStop( pAigTemp ); -// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0 ); +// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 ); } assert( RetValue != -1 ); Aig_ManStop( pMiter ); |