From 9604ecb1745da3bde720cd7be5ee8f89dc6bd5ff Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 27 May 2008 08:01:00 -0700 Subject: Version abc80527 --- src/aig/saig/saig.h | 1 + src/aig/saig/saigBmc.c | 6 ++- src/aig/saig/saigHaig.c | 115 +++++++++++++++++++++++---------------------- src/aig/saig/saigRetStep.c | 8 ++++ 4 files changed, 73 insertions(+), 57 deletions(-) (limited to 'src/aig/saig') diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 49d3f5ef..67f38758 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -89,6 +89,7 @@ extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int /*=== saigPhase.c ==========================================================*/ extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose ); /*=== saigRetFwd.c ==========================================================*/ +extern void Saig_ManMarkAutonomous( Aig_Man_t * p ); extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose ); /*=== saigRetMin.c ==========================================================*/ extern Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut ); diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 2d5af2d3..32b2d186 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -191,7 +191,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim } else pFrames = Saig_ManFramesBmc( pAig, nFrames ); - *piFrame = nFrames; + if ( piFrame ) + *piFrame = nFrames; if ( fVerbose ) { printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", @@ -281,7 +282,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim } else { - *piFrame = i / Saig_ManPoNum(pAig); + if ( piFrame ) + *piFrame = i / Saig_ManPoNum(pAig); RetValue = -1; break; } diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c index 4250ca79..8a75ae1f 100644 --- a/src/aig/saig/saigHaig.c +++ b/src/aig/saig/saigHaig.c @@ -195,7 +195,7 @@ int Aig_ManMapHaigNodes( Aig_Man_t * pHaig ) SeeAlso [] ***********************************************************************/ -int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames ) +int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, int clkSynth ) { int nBTLimit = 0; Aig_Man_t * pFrames, * pTemp; @@ -203,7 +203,7 @@ int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int n sat_solver * pSat; Aig_Obj_t * pObj1, * pObj2; int i, RetValue1, RetValue2, Counter, Lits[2], nOvers; - int clk = clock(); + int clk = clock(), clkVerif; nOvers = Aig_ManMapHaigNodes( pHaig ); @@ -226,57 +226,6 @@ clk = clock(); // pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) ); pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) ); -/* - // print the statistic into a file - { - FILE * pTable; - Aig_Man_t * pTemp, * pHaig2; - - pHaig2 = pAig->pManHaig; - pAig->pManHaig = NULL; - pTemp = Aig_ManDupDfs( pAig ); - pAig->pManHaig = pHaig2; - - Aig_ManSeqCleanup( pTemp ); - - pTable = fopen( "stats.txt", "a+" ); - fprintf( pTable, "%s ", p->pName ); - fprintf( pTable, "%d ", Saig_ManPiNum(p) ); - fprintf( pTable, "%d ", Saig_ManPoNum(p) ); - - fprintf( pTable, "%d ", Saig_ManRegNum(p) ); - fprintf( pTable, "%d ", Aig_ManNodeNum(p) ); - fprintf( pTable, "%d ", Aig_ManLevelNum(p) ); - - fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) ); - fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) ); - fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) ); - - fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) ); - fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) ); - fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) ); - fprintf( pTable, "\n" ); - fclose( pTable ); - - - pTable = fopen( "stats2.txt", "a+" ); - fprintf( pTable, "%s ", p->pSpec ); - fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) ); - fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) ); - - fprintf( pTable, "%d ", pCnf->nVars ); - fprintf( pTable, "%d ", pCnf->nClauses ); - fprintf( pTable, "%d ", pCnf->nLiterals ); - - fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 ); - fprintf( pTable, "%d ", pFrames->nAsserts/2 ); - fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 ); - fprintf( pTable, "\n" ); - fclose( pTable ); - - Aig_ManStop( pTemp ); - } -*/ // pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts ); @@ -375,11 +324,66 @@ clk = clock(); } printf( " \r" ); PRT( "Solving ", clock() - clk ); +clkVerif = clock() - clk; if ( Counter ) printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 ); else printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 ); + // print the statistic into a file + { + FILE * pTable; + Aig_Man_t * pTemp, * pHaig2; + + pHaig2 = pAig->pManHaig; + pAig->pManHaig = NULL; + pTemp = Aig_ManDupDfs( pAig ); + pAig->pManHaig = pHaig2; + + Aig_ManSeqCleanup( pTemp ); + + pTable = fopen( "stats.txt", "a+" ); + fprintf( pTable, "%s ", p->pName ); + fprintf( pTable, "%d ", Saig_ManPiNum(p) ); + fprintf( pTable, "%d ", Saig_ManPoNum(p) ); + + fprintf( pTable, "%d ", Saig_ManRegNum(p) ); + fprintf( pTable, "%d ", Aig_ManNodeNum(p) ); + fprintf( pTable, "%d ", Aig_ManLevelNum(p) ); + + fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) ); + fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) ); + fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) ); + + fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) ); + fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) ); + fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) ); + + fprintf( pTable, "%.2f", (float)(clkSynth)/(float)(CLOCKS_PER_SEC) ); + fprintf( pTable, "\n" ); + fclose( pTable ); + + + pTable = fopen( "stats2.txt", "a+" ); + fprintf( pTable, "%s ", p->pName ); + fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) ); + fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) ); + + fprintf( pTable, "%d ", pCnf->nVars ); + fprintf( pTable, "%d ", pCnf->nClauses ); + fprintf( pTable, "%d ", pCnf->nLiterals ); + + fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 ); + fprintf( pTable, "%d ", pFrames->nAsserts/2 ); + fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 ); + + fprintf( pTable, "%.2f", (float)(clkVerif)/(float)(CLOCKS_PER_SEC) ); + fprintf( pTable, "\n" ); + fclose( pTable ); + + Aig_ManStop( pTemp ); + } + // clean up Aig_ManStop( pFrames ); Cnf_DataFree( pCnf ); @@ -617,7 +621,7 @@ Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fReti Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; Aig_Man_t * pNew, * pTemp; Aig_Obj_t * pObj; - int i, k, nStepsReal, clk = clock(); + int i, k, nStepsReal, clk = clock(), clkSynth; Dar_ManDefaultRwrParams( pParsRwr ); clk = clock(); @@ -679,6 +683,7 @@ clk = clock(); } } PRT( "Synthesis time ", clock() - clk ); +clkSynth = clock() - clk; // use the haig for verification // Aig_ManAntiCleanup( pNew->pManHaig ); @@ -699,7 +704,7 @@ PRT( "Synthesis time ", clock() - clk ); } else { - if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig ) ) + if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig, clkSynth ) ) printf( "Constructing SAT solver has failed.\n" ); } diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c index fe726702..e2502761 100644 --- a/src/aig/saig/saigRetStep.c +++ b/src/aig/saig/saigRetStep.c @@ -62,6 +62,10 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug assert( Aig_ObjPioNum(pFanin0) > 0 ); assert( Aig_ObjPioNum(pFanin1) > 0 ); + // skip latch guns + if ( !Aig_ObjIsTravIdCurrent(p, pFanin0) && !Aig_ObjIsTravIdCurrent(p, pFanin1) ) + return NULL; + // get the inputs of these registers pInput0 = Saig_ManLi( p, Aig_ObjPioNum(pFanin0) - Saig_ManPiNum(p) ); pInput1 = Saig_ManLi( p, Aig_ObjPioNum(pFanin1) - Saig_ManPiNum(p) ); @@ -90,6 +94,9 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug pObjLo->PioNum = Aig_ManPiNum(p) - 1; p->nRegs++; + // make sure the register is retimable. + Aig_ObjSetTravIdCurrent(p, pObjLo); + //printf( "Reg = %4d. Reg = %4d. Compl = %d. Phase = %d.\n", // pFanin0->PioNum, pFanin1->PioNum, Aig_IsComplement(pObjNew), fCompl ); @@ -177,6 +184,7 @@ int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs ) p->fCreatePios = 1; if ( fForward ) { + Saig_ManMarkAutonomous( p ); for ( s = 0; s < nSteps; s++ ) { Aig_ManForEachNode( p, pObj, i ) -- cgit v1.2.3