diff options
Diffstat (limited to 'src/aig/fra')
| -rw-r--r-- | src/aig/fra/fraInd.c | 9 | ||||
| -rw-r--r-- | src/aig/fra/fraSec.c | 6 | ||||
| -rw-r--r-- | src/aig/fra/fraSim.c | 5 |
3 files changed, 14 insertions, 6 deletions
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 98025280..f45e8af0 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -147,6 +147,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) ); // add timeframes +// pManFraig->fAddStrash = 1; for ( f = 0; f < p->nFramesAll - 1; f++ ) { // set the constraints on the latch outputs @@ -163,6 +164,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k ) Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) ); } +// pManFraig->fAddStrash = 0; // mark the asserts pManFraig->nAsserts = Aig_ManPoNum(pManFraig); // add the POs for the latch outputs of the last frame @@ -348,7 +350,9 @@ PRT( "Time", clock() - clk ); // mark the classes as non-refined p->pCla->fRefinement = 0; // derive non-init K-timeframes while implementing e-classes +clk2 = clock(); p->pManFraig = Fra_FramesWithClasses( p ); +p->timeTrav += clock() - clk2; //Aig_ManDumpBlif( p->pManFraig, "testaig.blif" ); // perform AIG rewriting @@ -406,6 +410,9 @@ PRT( "Time", clock() - clk ); p->nSatCallsRecent = 0; p->nSatCallsSkipped = 0; Fra_FraigSweep( p ); + +// Sat_SolverPrintStats( stdout, p->pSat ); + // remove FRAIG and SAT solver Aig_ManStop( p->pManFraig ); p->pManFraig = NULL; sat_solver_delete( p->pSat ); p->pSat = NULL; @@ -425,7 +432,7 @@ PRT( "Time", clock() - clk ); } } /* - // check implications using simulation + // verify implications using simulation if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) { int Temp, clk = clock(); diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 0919e035..f9bbfe44 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -169,7 +169,7 @@ PRT( "Time", clock() - clk ); // perform fraiging clk = clock(); - pNew = Fra_FraigEquivence( pTemp = pNew, 1000 ); + pNew = Fra_FraigEquivence( pTemp = pNew, 100 ); Aig_ManStop( pTemp ); if ( fVerbose ) { @@ -199,13 +199,14 @@ PRT( "Time", clock() - clk ); clk = clock(); pNew = Aig_ManDup( pTemp = pNew, 1 ); Aig_ManStop( pTemp ); - pNew = Dar_ManRewriteDefault( pTemp = pNew ); + pNew = Dar_ManRewriteDefault( pNew ); if ( fVerbose ) { printf( "Rewriting: Latches = %5d. Nodes = %6d. ", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } + // perform retiming clk = clock(); pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); @@ -218,6 +219,7 @@ clk = clock(); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } + if ( pNew->nRegs ) pNew = Aig_ManConstReduce( pNew, 0 ); diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index d379cf53..b77c775a 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -432,12 +432,11 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat ) // assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) ); // flip one bit of the last frame - if ( fUseDist1 && p->nFrames == 2 ) + if ( fUseDist1 ) //&& p->nFrames == 2 ) { Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 ); for ( i = 0; i < Limit; i++ ) - Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 ); -// Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, nTruePis*(p->nFrames-2) + i)->Id ), i+1 ); + Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 ); } } } |