diff options
Diffstat (limited to 'src/aig/fra')
-rw-r--r-- | src/aig/fra/fra.h | 2 | ||||
-rw-r--r-- | src/aig/fra/fraCec.c | 8 | ||||
-rw-r--r-- | src/aig/fra/fraClaus.c | 15 | ||||
-rw-r--r-- | src/aig/fra/fraHot.c | 3 | ||||
-rw-r--r-- | src/aig/fra/fraMan.c | 3 | ||||
-rw-r--r-- | src/aig/fra/fraSec.c | 24 |
6 files changed, 35 insertions, 20 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 44cfe847..7311d414 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -226,7 +226,7 @@ struct Fra_Man_t_ //////////////////////////////////////////////////////////////////////// static inline unsigned * Fra_ObjSim( Fra_Sml_t * p, int Id ) { return p->pData + p->nWordsTotal * Id; } -static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); } +static inline unsigned Fra_ObjRandomSim() { return Aig_ManRandom(0); } static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i]; } static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; } diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index 05f2493a..e91478a4 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -47,14 +47,16 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe int status, RetValue, clk = clock(); Vec_Int_t * vCiIds; - assert( Aig_ManPoNum(pMan) == 1 ); + assert( Aig_ManRegNum(pMan) == 0 ); pMan->pData = NULL; // derive CNF - pCnf = Cnf_Derive( pMan, 0 ); -// pCnf = Cnf_DeriveSimple( pMan, 0 ); + pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) ); +// pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); // convert into the SAT solver pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + // add the OR clause for the outputs + Cnf_DataWriteOrClause( pSat, pCnf ); vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); Cnf_DataFree( pCnf ); // solve SAT diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c index c9ea4907..6f0a2012 100644 --- a/src/aig/fra/fraClaus.c +++ b/src/aig/fra/fraClaus.c @@ -606,7 +606,8 @@ int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs ) // simulate the AIG clk = clock(); - srand( 0xAABBAABB ); +// srand( 0xAABBAABB ); + Aig_ManRandom(1); pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames ); if ( p->fTarget && pSeq->fNonConstOut ) { @@ -661,7 +662,8 @@ PRT( "Infoseq", clock() - clk ); // perform combinational simulation clk = clock(); - srand( 0xAABBAABB ); +// srand( 0xAABBAABB ); + Aig_ManRandom(1); pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref ); if ( p->fVerbose ) { @@ -728,7 +730,8 @@ int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs ) // simulate the AIG clk = clock(); - srand( 0xAABBAABB ); +// srand( 0xAABBAABB ); + Aig_ManRandom(1); pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames ); if ( p->fTarget && pSeq->fNonConstOut ) { @@ -743,7 +746,8 @@ if ( p->fVerbose ) // perform combinational simulation clk = clock(); - srand( 0xAABBAABB ); +// srand( 0xAABBAABB ); + Aig_ManRandom(1); pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref ); if ( p->fVerbose ) { @@ -1614,7 +1618,8 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p ) int * pStart, * pVar2Id; int clk = clock(); // simulate the circuit with nCombSimWords * 32 = 64K patterns - srand( 0xAABBAABB ); +// srand( 0xAABBAABB ); + Aig_ManRandom(1); pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords ); // create mapping from SAT vars to node IDs pVar2Id = ALLOC( int, p->pCnf->nVars ); diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c index 222f5bcc..b2156193 100644 --- a/src/aig/fra/fraHot.c +++ b/src/aig/fra/fraHot.c @@ -333,7 +333,8 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots ) // generate random sim-info at register outputs vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords ); - srand( 0xAABBAABB ); +// srand( 0xAABBAABB ); + Aig_ManRandom(1); for ( i = 0; i < nRegs; i++ ) { pSim1 = Vec_PtrEntry( vSimInfo, i ); diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index da7c37a3..b8cf13c5 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -120,7 +120,8 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll ); memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); // set random number generator - srand( 0xABCABC ); +// srand( 0xABCABC ); + Aig_ManRandom(1); // set the pointer to the manager Aig_ManForEachObj( p->pManAig, pObj, i ) pObj->pData = p; diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 64222a47..9a500680 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -44,21 +44,20 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetime { Fra_Ssw_t Pars, * pPars = &Pars; Fra_Sml_t * pSml; - Aig_Man_t * pNew = NULL, * pTemp; + Aig_Man_t * pNew, * pTemp; int nFrames, RetValue, nIter, clk, clkTotal = clock(); int fLatchCorr = 0; // try the miter before solving - RetValue = Fra_FraigMiterStatus( p ); - if ( RetValue == 0 || RetValue == 1 ) + pNew = Aig_ManDup( p ); + RetValue = Fra_FraigMiterStatus( pNew ); + if ( RetValue >= 0 ) goto finish; // prepare parameters memset( pPars, 0, sizeof(Fra_Ssw_t) ); pPars->fLatchCorr = fLatchCorr; pPars->fVerbose = fVeryVerbose; - - pNew = Aig_ManDup( p ); if ( fVerbose ) { printf( "Original miter: Latches = %5d. Nodes = %6d.\n", @@ -78,6 +77,9 @@ clk = clock(); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } + RetValue = Fra_FraigMiterStatus( pNew ); + if ( RetValue >= 0 ) + goto finish; // perform phase abstraction clk = clock(); @@ -150,6 +152,13 @@ PRT( "Time", clock() - clk ); } } + if ( pNew->nRegs == 0 ) + RetValue = Fra_FraigCec( &pNew, 0 ); + + RetValue = Fra_FraigMiterStatus( pNew ); + if ( RetValue >= 0 ) + goto finish; + // perform min-area retiming if ( fRetimeRegs && pNew->nRegs ) { @@ -262,9 +271,7 @@ PRT( "Time", clock() - clkTotal ); assert( Aig_ManRegNum(pNew) > 0 ); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); -clk = clock(); RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 ); -PRT( "Time", clock() - clk ); } finish: @@ -289,8 +296,7 @@ PRT( "Time", clock() - clkTotal ); Ioa_WriteAiger( pNew, pFileName, 0, 0 ); printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName ); } - if ( pNew ) - Aig_ManStop( pNew ); + Aig_ManStop( pNew ); return RetValue; } |