From 74ff01bfb54e9f0a68ac88b827521a422269a144 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 15 May 2008 08:01:00 -0700 Subject: Version abc80515 --- src/aig/fra/fra.h | 27 ++++++++- src/aig/fra/fraSec.c | 154 +++++++++++++++++++++++++++++++++++++-------------- 2 files changed, 137 insertions(+), 44 deletions(-) (limited to 'src/aig/fra') diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index f7ad40dd..7cb846fa 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -51,6 +51,7 @@ extern "C" { typedef struct Fra_Par_t_ Fra_Par_t; typedef struct Fra_Ssw_t_ Fra_Ssw_t; +typedef struct Fra_Sec_t_ Fra_Sec_t; typedef struct Fra_Man_t_ Fra_Man_t; typedef struct Fra_Cla_t_ Fra_Cla_t; typedef struct Fra_Sml_t_ Fra_Sml_t; @@ -87,7 +88,7 @@ struct Fra_Par_t_ int fDontShowBar; // does not show progressbar during fraiging }; -// seq SAT sweeping parametesr +// seq SAT sweeping parameters struct Fra_Ssw_t_ { int nPartSize; // size of the partition @@ -107,6 +108,27 @@ struct Fra_Ssw_t_ float TimeLimit; // the runtime budget for this call }; +// SEC parametesr +struct Fra_Sec_t_ +{ + int fTryComb; // try CEC call as a preprocessing step + int fTryBmc; // try BMC call as a preprocessing step + int nFramesMax; // the max number of frames used for induction + int fPhaseAbstract; // enables phase abstraction + int fRetimeFirst; // enables most-forward retiming at the beginning + int fRetimeRegs; // enables min-register retiming at the beginning + int fFraiging; // enables fraiging at the beginning + int fInterpolation; // enables interpolation + int fReachability; // enables BDD based reachability + int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove + int fVerbose; // enables verbose reporting of statistics + int fVeryVerbose; // enables very verbose reporting + int TimeLimit; // enables the timeout + // internal parameters + int fRecursive; // set to 1 when SEC is called recursively + int fReportSolution; // enables report solution in a special form +}; + // FRAIG equivalence classes struct Fra_Cla_t_ { @@ -329,7 +351,8 @@ extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR ); extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); /*=== fraSec.c ========================================================*/ -extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit ); +extern void Fra_SecSetDefaultParams( Fra_Sec_t * p ); +extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec ); /*=== fraSim.c ========================================================*/ extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ); extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ); diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index db8027d9..b8f93f57 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -40,12 +40,44 @@ SeeAlso [] ***********************************************************************/ -int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit ) +void Fra_SecSetDefaultParams( Fra_Sec_t * p ) +{ + memset( p, 0, sizeof(Fra_Sec_t) ); + p->fTryComb = 1; // try CEC call as a preprocessing step + p->fTryBmc = 1; // try BMC call as a preprocessing step + p->nFramesMax = 2; // the max number of frames used for induction + p->fPhaseAbstract = 1; // enables phase abstraction + p->fRetimeFirst = 1; // enables most-forward retiming at the beginning + p->fRetimeRegs = 1; // enables min-register retiming at the beginning + p->fFraiging = 1; // enables fraiging at the beginning + p->fInterpolation = 1; // enables interpolation + p->fReachability = 1; // enables BDD based reachability + p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove + p->fVerbose = 0; // enables verbose reporting of statistics + p->fVeryVerbose = 0; // enables very verbose reporting + p->TimeLimit = 0; // enables the timeout + // internal parameters + p->fReportSolution = 1; // enables specialized format for reporting solution +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec ) { Fra_Ssw_t Pars, * pPars = &Pars; Fra_Sml_t * pSml; Aig_Man_t * pNew, * pTemp; int nFrames, RetValue, nIter, clk, clkTotal = clock(); + int TimeOut = 0; int fLatchCorr = 0; float TimeLeft = 0.0; @@ -58,8 +90,8 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetime // prepare parameters memset( pPars, 0, sizeof(Fra_Ssw_t) ); pPars->fLatchCorr = fLatchCorr; - pPars->fVerbose = fVeryVerbose; - if ( fVerbose ) + pPars->fVerbose = pParSec->fVeryVerbose; + if ( pParSec->fVerbose ) { printf( "Original miter: Latches = %5d. Nodes = %6d.\n", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); @@ -72,7 +104,7 @@ clk = clock(); pNew = Aig_ManReduceLaches( pNew, 0 ); if ( pNew->nRegs ) pNew = Aig_ManConstReduce( pNew, 0 ); - if ( fVerbose ) + if ( pParSec->fVerbose ) { printf( "Sequential cleanup: Latches = %5d. Nodes = %6d. ", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); @@ -84,14 +116,14 @@ PRT( "Time", clock() - clk ); // perform phase abstraction clk = clock(); - if ( fPhaseAbstract ) + if ( pParSec->fPhaseAbstract ) { extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose ); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 ); Aig_ManStop( pTemp ); - if ( fVerbose ) + if ( pParSec->fVerbose ) { printf( "Phase abstraction: Latches = %5d. Nodes = %6d. ", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); @@ -100,12 +132,12 @@ PRT( "Time", clock() - clk ); } // perform forward retiming - if ( fRetimeFirst && pNew->nRegs ) + if ( pParSec->fRetimeFirst && pNew->nRegs ) { clk = clock(); pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); Aig_ManStop( pTemp ); - if ( fVerbose ) + if ( pParSec->fVerbose ) { printf( "Forward retiming: Latches = %5d. Nodes = %6d. ", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); @@ -120,22 +152,24 @@ clk = clock(); pNew = Aig_ManDupOrdered( pTemp = pNew ); // pNew = Aig_ManDupDfs( pTemp = pNew ); Aig_ManStop( pTemp ); - if ( RetValue == -1 && TimeLimit ) + if ( RetValue == -1 && pParSec->TimeLimit ) { - TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); + TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { printf( "Runtime limit exceeded.\n" ); RetValue = -1; + TimeOut = 1; goto finish; } } - pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, fVeryVerbose, &nIter, TimeLeft ); + pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft ); if ( pNew == NULL ) { pNew = pTemp; RetValue = -1; + TimeOut = 1; goto finish; } p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL; @@ -148,7 +182,7 @@ PRT( "Time", clock() - clkTotal ); return RetValue; } - if ( fVerbose ) + if ( pParSec->fVerbose ) { printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ", nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); @@ -156,25 +190,26 @@ PRT( "Time", clock() - clk ); } } - if ( RetValue == -1 && TimeLimit ) + if ( RetValue == -1 && pParSec->TimeLimit ) { - TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); + TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { printf( "Runtime limit exceeded.\n" ); RetValue = -1; + TimeOut = 1; goto finish; } } // perform fraiging - if ( fFraiging ) + if ( pParSec->fFraiging ) { clk = clock(); pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 ); Aig_ManStop( pTemp ); - if ( fVerbose ) + if ( pParSec->fVerbose ) { printf( "Fraiging: Latches = %5d. Nodes = %6d. ", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); @@ -189,20 +224,21 @@ PRT( "Time", clock() - clk ); if ( RetValue >= 0 ) goto finish; - if ( RetValue == -1 && TimeLimit ) + if ( RetValue == -1 && pParSec->TimeLimit ) { - TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); + TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { printf( "Runtime limit exceeded.\n" ); RetValue = -1; + TimeOut = 1; goto finish; } } // perform min-area retiming - if ( fRetimeRegs && pNew->nRegs ) + if ( pParSec->fRetimeRegs && pNew->nRegs ) { extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); clk = clock(); @@ -213,7 +249,7 @@ clk = clock(); Aig_ManStop( pTemp ); pNew = Aig_ManDupOrdered( pTemp = pNew ); Aig_ManStop( pTemp ); - if ( fVerbose ) + if ( pParSec->fVerbose ) { printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); @@ -224,16 +260,17 @@ PRT( "Time", clock() - clk ); // perform seq sweeping while increasing the number of frames RetValue = Fra_FraigMiterStatus( pNew ); if ( RetValue == -1 ) - for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 ) + for ( nFrames = 1; nFrames <= pParSec->nFramesMax; nFrames *= 2 ) { - if ( RetValue == -1 && TimeLimit ) + if ( RetValue == -1 && pParSec->TimeLimit ) { - TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); + TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { printf( "Runtime limit exceeded.\n" ); RetValue = -1; + TimeOut = 1; goto finish; } } @@ -246,11 +283,12 @@ clk = clock(); { pNew = pTemp; RetValue = -1; + TimeOut = 1; goto finish; } Aig_ManStop( pTemp ); RetValue = Fra_FraigMiterStatus( pNew ); - if ( fVerbose ) + if ( pParSec->fVerbose ) { printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ", nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); @@ -260,7 +298,7 @@ PRT( "Time", clock() - clk ); break; // perform retiming -// if ( fRetimeFirst && pNew->nRegs ) +// if ( pParSec->fRetimeFirst && pNew->nRegs ) if ( pNew->nRegs ) { extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); @@ -272,7 +310,7 @@ clk = clock(); Aig_ManStop( pTemp ); pNew = Aig_ManDupOrdered( pTemp = pNew ); Aig_ManStop( pTemp ); - if ( fVerbose ) + if ( pParSec->fVerbose ) { printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); @@ -290,7 +328,7 @@ clk = clock(); // pNew = Dar_ManRewriteDefault( pTemp = pNew ); pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0 ); Aig_ManStop( pTemp ); - if ( fVerbose ) + if ( pParSec->fVerbose ) { printf( "Rewriting: Latches = %5d. Nodes = %6d. ", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); @@ -302,7 +340,7 @@ PRT( "Time", clock() - clk ); { clk = clock(); pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) ); - if ( fVerbose ) + if ( pParSec->fVerbose ) { printf( "Seq simulation : Latches = %5d. Nodes = %6d. ", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); @@ -327,14 +365,14 @@ PRT( "Time", clock() - clkTotal ); // try interplation clk = clock(); - if ( RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 ) + if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 ) { extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth ); int Depth; pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); - RetValue = Saig_Interpolate( pNew, 5000, 0, 1, fVeryVerbose, &Depth ); - if ( fVerbose ) + RetValue = Saig_Interpolate( pNew, 5000, 0, 1, pParSec->fVeryVerbose, &Depth ); + if ( pParSec->fVerbose ) { if ( RetValue == 1 ) printf( "Property proved using interpolation. " ); @@ -349,7 +387,7 @@ PRT( "Time", clock() - clk ); } // try reachability analysis - if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 && Aig_ManRegNum(pNew) > 0 ) + if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < 150 ) { extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); @@ -371,14 +409,16 @@ PRT( "Time", clock() - clk ); iCount = 0; for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ ) { + int TimeLimitCopy = 0; // get the remaining time for this output - if ( TimeLimit ) + if ( pParSec->TimeLimit ) { - TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); + TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); if ( TimeLeft == 0.0 ) { printf( "Runtime limit exceeded.\n" ); + TimeOut = 1; goto finish; } TimeLimit2 = 1 + (int)TimeLeft; @@ -390,12 +430,23 @@ PRT( "Time", clock() - clk ); iCount++; printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter ); pNew2 = Aig_ManDupOneOutput( pNew, i ); - RetValue2 = Fra_FraigSec( pNew2, nFramesMax, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit2 ); + + TimeLimitCopy = pParSec->TimeLimit; + pParSec->TimeLimit = TimeLimit2; + pParSec->fRecursive = 1; + RetValue2 = Fra_FraigSec( pNew2, pParSec ); + pParSec->fRecursive = 0; + pParSec->TimeLimit = TimeLimitCopy; + Aig_ManStop( pNew2 ); if ( RetValue2 == 0 ) goto finish; if ( RetValue2 == -1 ) + { fOneUnsolved = 1; + if ( pParSec->fStopOnFirstFail ) + break; + } } if ( fOneUnsolved ) RetValue = -1; @@ -410,23 +461,42 @@ finish: { printf( "Networks are equivalent. " ); PRT( "Time", clock() - clkTotal ); + if ( pParSec->fReportSolution && !pParSec->fRecursive ) + { + printf( "SOLUTION: PASS " ); +PRT( "Time", clock() - clkTotal ); + } } else if ( RetValue == 0 ) { printf( "Networks are NOT EQUIVALENT. " ); PRT( "Time", clock() - clkTotal ); + if ( pParSec->fReportSolution && !pParSec->fRecursive ) + { + printf( "SOLUTION: FAIL " ); +PRT( "Time", clock() - clkTotal ); + } } - else + else { - static int Counter = 1; - char pFileName[1000]; printf( "Networks are UNDECIDED. " ); PRT( "Time", clock() - clkTotal ); - sprintf( pFileName, "sm%03d.aig", Counter++ ); - Ioa_WriteAiger( pNew, pFileName, 0, 0 ); - printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName ); + if ( pParSec->fReportSolution && !pParSec->fRecursive ) + { + printf( "SOLUTION: UNDECIDED " ); +PRT( "Time", clock() - clkTotal ); + } + if ( !TimeOut ) + { + static int Counter = 1; + char pFileName[1000]; + sprintf( pFileName, "sm%03d.aig", Counter++ ); + Ioa_WriteAiger( pNew, pFileName, 0, 0 ); + printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName ); + } } - Aig_ManStop( pNew ); + if ( pNew ) + Aig_ManStop( pNew ); return RetValue; } -- cgit v1.2.3