From cb899ec848984b194a9c227c7a01f147454ce591 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 12 May 2008 08:01:00 -0700 Subject: Version abc80512 --- src/aig/aig/aig.h | 1 + src/aig/aig/aigDup.c | 44 +++++++++++++++++++++++ src/aig/fra/fraLcr.c | 2 +- src/aig/fra/fraSec.c | 61 +++++++++++++++++++++++++++---- src/aig/saig/saig.h | 2 +- src/aig/saig/saigBmc.c | 94 ++++++++++++++++++++++++++++++++++++++++++++++-- src/aig/saig/saigInter.c | 8 +++++ src/base/abci/abc.c | 26 +++++++++++--- src/base/abci/abcDar.c | 6 ++-- src/base/main/main.c | 2 +- src/map/pcm/module.make | 0 src/map/ply/module.make | 0 12 files changed, 226 insertions(+), 20 deletions(-) delete mode 100644 src/map/pcm/module.make delete mode 100644 src/map/ply/module.make diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 1450ad21..bbb5cb6e 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -478,6 +478,7 @@ extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl ); +extern Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum ); /*=== aigFanout.c ==========================================================*/ extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ); extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ); diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c index 55dc5625..fc01e7f0 100644 --- a/src/aig/aig/aigDup.c +++ b/src/aig/aig/aigDup.c @@ -787,6 +787,50 @@ Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates AIG with only one primary output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + assert( Aig_ManRegNum(p) > 0 ); + assert( iPoNum < Aig_ManPoNum(p)-Aig_ManRegNum(p) ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + // set registers + pNew->nRegs = p->nRegs; + pNew->nTruePis = p->nTruePis; + pNew->nTruePos = 1; + // duplicate internal nodes + Aig_ManForEachNode( p, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create the PO + pObj = Aig_ManPo( p, iPoNum ); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + // create register inputs with MUXes + Aig_ManForEachLiSeq( p, pObj, i ) + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + Aig_ManCleanup( pNew ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c index 0f5cc207..e5222e2e 100644 --- a/src/aig/fra/fraLcr.c +++ b/src/aig/fra/fraLcr.c @@ -542,7 +542,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC if ( pnIter ) *pnIter = 0; return Aig_ManDupOrdered(pAig); } - assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManRegNum(pAig) > 0 ); // simulate the AIG clk2 = clock(); diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 5146344c..db8027d9 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -120,7 +120,7 @@ clk = clock(); pNew = Aig_ManDupOrdered( pTemp = pNew ); // pNew = Aig_ManDupDfs( pTemp = pNew ); Aig_ManStop( pTemp ); - if ( TimeLimit ) + if ( RetValue == -1 && TimeLimit ) { TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); @@ -131,7 +131,7 @@ clk = clock(); goto finish; } } - pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter, TimeLeft ); + pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, fVeryVerbose, &nIter, TimeLeft ); if ( pNew == NULL ) { pNew = pTemp; @@ -156,7 +156,7 @@ PRT( "Time", clock() - clk ); } } - if ( TimeLimit ) + if ( RetValue == -1 && TimeLimit ) { TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); @@ -189,7 +189,7 @@ PRT( "Time", clock() - clk ); if ( RetValue >= 0 ) goto finish; - if ( TimeLimit ) + if ( RetValue == -1 && TimeLimit ) { TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); @@ -226,7 +226,7 @@ PRT( "Time", clock() - clk ); if ( RetValue == -1 ) for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 ) { - if ( TimeLimit ) + if ( RetValue == -1 && TimeLimit ) { TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); TimeLeft = AIG_MAX( TimeLeft, 0.0 ); @@ -327,13 +327,13 @@ PRT( "Time", clock() - clkTotal ); // try interplation clk = clock(); - if ( RetValue == -1 && Aig_ManRegNum(pNew) > 0 ) + if ( 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, 10000, 0, 1, 0, &Depth ); + RetValue = Saig_Interpolate( pNew, 5000, 0, 1, fVeryVerbose, &Depth ); if ( fVerbose ) { if ( RetValue == 1 ) @@ -357,6 +357,53 @@ PRT( "Time", clock() - clk ); RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 ); } + // try one-output at a time + if ( RetValue == -1 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) > 1 ) + { + Aig_Man_t * pNew2; + int i, TimeLimit2, RetValue2, fOneUnsolved = 0, iCount, Counter = 0; + // count unsolved outputs + for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ ) + if ( !Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) ) + Counter++; + printf( "*** The miter has %d outputs (out of %d total) unsolved in the multi-output form.\n", + Counter, Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) ); + iCount = 0; + for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ ) + { + // get the remaining time for this output + if ( TimeLimit ) + { + TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)); + TimeLeft = AIG_MAX( TimeLeft, 0.0 ); + if ( TimeLeft == 0.0 ) + { + printf( "Runtime limit exceeded.\n" ); + goto finish; + } + TimeLimit2 = 1 + (int)TimeLeft; + } + else + TimeLimit2 = 0; + if ( Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) ) + continue; + 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 ); + Aig_ManStop( pNew2 ); + if ( RetValue2 == 0 ) + goto finish; + if ( RetValue2 == -1 ) + fOneUnsolved = 1; + } + if ( fOneUnsolved ) + RetValue = -1; + else + RetValue = 1; + printf( "*** Finished running separate outputs of the miter.\n" ); + } + finish: // report the miter if ( RetValue == 1 ) diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index f0eb7099..b9b7de40 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -76,7 +76,7 @@ static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { //////////////////////////////////////////////////////////////////////// /*=== saigBmc.c ==========================================================*/ -extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose, int * piFrame ); +extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame ); /*=== saigCone.c ==========================================================*/ extern void Saig_ManPrintCones( Aig_Man_t * p ); /*=== saigInter.c ==========================================================*/ diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 3a6aa611..f6a42c8b 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -80,6 +80,90 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) return pFrames; } +/**Function************************************************************* + + Synopsis [Returns the number of internal nodes that are not counted yet.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( !Aig_ObjIsNode(pObj) ) + return 0; + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return 0; + Aig_ObjSetTravIdCurrent(p, pObj); + return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) + + Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Create timeframes of the manager for BMC.] + + Description [The resulting manager is combinational. The primary inputs + corresponding to register outputs are ordered first. POs correspond to + the property outputs in each time-frame. + The unrolling is stopped as soon as the number of nodes in the frames + exceeds the given maximum size.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo; + int i, f, Counter = 0; + assert( Saig_ManRegNum(pAig) > 0 ); + pFrames = Aig_ManStart( nSizeMax ); + Aig_ManIncrementTravId( pFrames ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); + // create variables for register outputs + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_ManConst0( pFrames ); + // add timeframes + Counter = 0; + for ( f = 0; f < nFrames; f++ ) + { + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create POs for this frame + Saig_ManForEachPo( pAig, pObj, i ) + { + pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) ); + if ( Counter >= nSizeMax ) + { + Aig_ManCleanup( pFrames ); + return pFrames; + } + } + if ( f == nFrames - 1 ) + break; + // save register inputs + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Aig_ObjChild0Copy(pObj); + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; + } + Aig_ManCleanup( pFrames ); + return pFrames; +} + /**Function************************************************************* Synopsis [Performs BMC for the given AIG.] @@ -91,7 +175,7 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) SeeAlso [] ***********************************************************************/ -int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fRewrite, int fVerbose, int * piFrame ) +int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame ) { sat_solver * pSat; Cnf_Dat_t * pCnf; @@ -101,7 +185,13 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fRewri *piFrame = -1; // derive the timeframes clk = clock(); - pFrames = Saig_ManFramesBmc( pAig, nFrames ); + if ( nSizeMax > 0 ) + { + pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax ); + nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0); + } + else + pFrames = Saig_ManFramesBmc( pAig, nFrames ); if ( fVerbose ) { printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c index c3bb0875..3adcc568 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -566,6 +566,14 @@ p->timeCnf += clock() - clk; // iterate the interpolation procedure for ( i = 0; ; i++ ) { + if ( p->nFrames + i >= 100 ) + { + if ( fVerbose ) + printf( "Reached limit (%d) on the number of timeframes.\n", 100 ); + p->timeTotal = clock() - clkTotal; + Saig_ManagerFree( p ); + return -1; + } // perform interplation clk = clock(); RetValue = Saig_PerformOneStep( p ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f914b9c4..5725aaf0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -12713,6 +12713,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fWriteImps = 0; pPars->fUse1Hot = 0; pPars->fVerbose = 0; + pPars->TimeLimit = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF ) { @@ -14657,25 +14658,27 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; int nFrames; + int nSizeMax; int nBTLimit; int fRewrite; int fNewAlgo; int fVerbose; - extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose ); + extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nFrames = 10; + nFrames = 20; + nSizeMax = 100000; nBTLimit = 10000; fRewrite = 0; fNewAlgo = 1; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCravh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FNCravh" ) ) != EOF ) { switch ( c ) { @@ -14690,6 +14693,17 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nFrames < 0 ) goto usage; break; + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nSizeMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nSizeMax < 0 ) + goto usage; + break; case 'C': if ( globalUtilOptind >= argc ) { @@ -14731,13 +14745,14 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Does not work for combinational networks.\n" ); return 0; } - Abc_NtkDarBmc( pNtk, nFrames, nBTLimit, fRewrite, fNewAlgo, fVerbose ); + Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nBTLimit, fRewrite, fNewAlgo, fVerbose ); return 0; usage: - fprintf( pErr, "usage: bmc [-F num] [-C num] [-ravh]\n" ); + fprintf( pErr, "usage: bmc [-FNC num] [-ravh]\n" ); fprintf( pErr, "\t perform bounded model checking\n" ); fprintf( pErr, "\t-F num : the number of time frames [default = %d]\n", nFrames ); + fprintf( pErr, "\t-N num : the max number of nodes in the frames [default = %d]\n", nSizeMax ); fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit ); fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); fprintf( pErr, "\t-a : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" ); @@ -17069,6 +17084,7 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fWriteImps = 0; pPars->fUse1Hot = 0; pPars->fVerbose = 0; + pPars->TimeLimit = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF ) { diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 75995a60..ef1fbebc 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1208,7 +1208,7 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose ) +int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose ) { Aig_Man_t * pMan; int RetValue = -1, clk = clock(); @@ -1226,7 +1226,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, in if ( fNewAlgo ) { int iFrame; - RetValue = Saig_ManBmcSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose, &iFrame ); + RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; if ( RetValue == 1 ) printf( "No output was asserted in %d frames. ", nFrames ); @@ -1337,7 +1337,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, i } if ( fTryBmc ) { - RetValue = Abc_NtkDarBmc( pNtk, 10, 1000, 0, 1, 0 ); + RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, 1000, 0, 1, 0 ); if ( RetValue == 0 ) return RetValue; } diff --git a/src/base/main/main.c b/src/base/main/main.c index 26740258..7ecbe48e 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -217,7 +217,7 @@ int main( int argc, char * argv[] ) break; } } - + // if the memory should be freed, quit packages if ( fStatus < 0 ) { diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make deleted file mode 100644 index e69de29b..00000000 diff --git a/src/map/ply/module.make b/src/map/ply/module.make deleted file mode 100644 index e69de29b..00000000 -- cgit v1.2.3