diff options
| -rw-r--r-- | src/aig/fra/fra.h | 5 | ||||
| -rw-r--r-- | src/aig/fra/fraInd.c | 17 | ||||
| -rw-r--r-- | src/aig/fra/fraLcr.c | 15 | ||||
| -rw-r--r-- | src/aig/fra/fraSec.c | 91 | ||||
| -rw-r--r-- | src/aig/ntl/ntlFraig.c | 2 | ||||
| -rw-r--r-- | src/aig/saig/saigInter.c | 2 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 69 | ||||
| -rw-r--r-- | src/base/abci/abcDar.c | 97 | ||||
| -rw-r--r-- | src/map/pcm/module.make | 0 | ||||
| -rw-r--r-- | src/map/ply/module.make | 0 |
10 files changed, 240 insertions, 58 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 7311d414..f7ad40dd 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -104,6 +104,7 @@ struct Fra_Ssw_t_ int fUse1Hot; // use one-hotness constraints int fVerbose; // enable verbose output int nIters; // the number of iterations performed + float TimeLimit; // the runtime budget for this call }; // FRAIG equivalence classes @@ -312,7 +313,7 @@ extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars /*=== fraIndVer.c =====================================================*/ extern int Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits ); /*=== fraLcr.c ========================================================*/ -extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter ); +extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); @@ -328,7 +329,7 @@ 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 ); +extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit ); /*=== 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/fraInd.c b/src/aig/fra/fraInd.c index b29fa946..99b62856 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -336,9 +336,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams ) Fra_Par_t Pars, * pPars = &Pars; Aig_Obj_t * pObj; Cnf_Dat_t * pCnf; - Aig_Man_t * pManAigNew; + Aig_Man_t * pManAigNew = NULL; int nNodesBeg, nRegsBeg; int nIter, i, clk = clock(), clk2; + int TimeToStop = (pParams->TimeLimit == 0.0)? 0 : clock() + (int)(pParams->TimeLimit * CLOCKS_PER_SEC); if ( Aig_ManNodeNum(pManAig) == 0 ) { @@ -419,6 +420,12 @@ PRT( "Time", clock() - clk ); if ( pPars->fUseImps ) p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr ); + if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop ) + { + printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" ); + goto finish; + } + // perform BMC (for the min number of frames) Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement //Fra_ClassesPrint( p->pCla, 1 ); @@ -442,6 +449,13 @@ PRT( "Time", clock() - clk ); int nLitsOld = Fra_ClassesCountLits(p->pCla); int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0; int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0; + + if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop ) + { + printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" ); + goto finish; + } + // mark the classes as non-refined p->pCla->fRefinement = 0; // derive non-init K-timeframes while implementing e-classes @@ -592,6 +606,7 @@ p->timeTotal = clock() - clk; p->nNodesEnd = Aig_ManNodeNum(pManAigNew); p->nRegsEnd = Aig_ManRegNum(pManAigNew); // free the manager +finish: Fra_ManStop( p ); // check the output // if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 ) diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c index 145bafae..0f5cc207 100644 --- a/src/aig/fra/fraLcr.c +++ b/src/aig/fra/fraLcr.c @@ -526,7 +526,7 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter ) +Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit ) { int nPartSize = 200; int fReprSelect = 0; @@ -536,6 +536,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC Aig_Man_t * pAigPart, * pAigNew = NULL; Vec_Int_t * vPart; int i, nIter, timeSim, clk = clock(), clk2, clk3; + int TimeToStop = (TimeLimit == 0.0)? 0 : clock() + (int)(TimeLimit * CLOCKS_PER_SEC); if ( Aig_ManNodeNum(pAig) == 0 ) { if ( pnIter ) *pnIter = 0; @@ -609,6 +610,15 @@ p->timePart += clock() - clk2; Vec_PtrClear( p->vFraigs ); Vec_PtrForEachEntry( p->vParts, vPart, i ) { + if ( TimeLimit != 0.0 && clock() > TimeToStop ) + { + Vec_PtrForEachEntry( p->vFraigs, pAigPart, i ) + Aig_ManStop( pAigPart ); + Aig_ManCleanMarkA( pAig ); + Aig_ManCleanMarkB( pAig ); + printf( "Fra_FraigLatchCorrespondence(): Runtime limit exceeded.\n" ); + goto finish; + } clk2 = clock(); pAigPart = Fra_LcrCreatePart( p, vPart ); p->timeTrav += clock() - clk2; @@ -649,7 +659,6 @@ clk2 = clock(); p->timePart += clock() - clk2; } } - free( pTemp ); p->nIters = nIter; // move the classes into representatives and reduce AIG @@ -667,6 +676,8 @@ p->timeTotal = clock() - clk; p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); p->nNodesEnd = Aig_ManNodeNum(pAigNew); p->nRegsEnd = Aig_ManRegNum(pAigNew); +finish: + free( pTemp ); Lcr_ManFree( p ); if ( pnIter ) *pnIter = nIter; return pAigNew; diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 9a500680..5146344c 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -40,13 +40,14 @@ SeeAlso [] ***********************************************************************/ -int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ) +int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit ) { Fra_Ssw_t Pars, * pPars = &Pars; Fra_Sml_t * pSml; Aig_Man_t * pNew, * pTemp; int nFrames, RetValue, nIter, clk, clkTotal = clock(); int fLatchCorr = 0; + float TimeLeft = 0.0; // try the miter before solving pNew = Aig_ManDup( p ); @@ -119,7 +120,24 @@ clk = clock(); pNew = Aig_ManDupOrdered( pTemp = pNew ); // pNew = Aig_ManDupDfs( pTemp = pNew ); Aig_ManStop( pTemp ); - pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter ); + 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" ); + RetValue = -1; + goto finish; + } + } + pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter, TimeLeft ); + if ( pNew == NULL ) + { + pNew = pTemp; + RetValue = -1; + goto finish; + } p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL; Aig_ManStop( pTemp ); if ( pNew == NULL ) @@ -138,6 +156,18 @@ PRT( "Time", clock() - clk ); } } + 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" ); + RetValue = -1; + goto finish; + } + } + // perform fraiging if ( fFraiging ) { @@ -159,6 +189,18 @@ PRT( "Time", clock() - clk ); if ( RetValue >= 0 ) goto finish; + 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" ); + RetValue = -1; + goto finish; + } + } + // perform min-area retiming if ( fRetimeRegs && pNew->nRegs ) { @@ -184,9 +226,28 @@ PRT( "Time", clock() - clk ); if ( RetValue == -1 ) for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 ) { + 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" ); + RetValue = -1; + goto finish; + } + } + clk = clock(); pPars->nFramesK = nFrames; + pPars->TimeLimit = TimeLeft; pNew = Fra_FraigInduction( pTemp = pNew, pPars ); + if ( pNew == NULL ) + { + pNew = pTemp; + RetValue = -1; + goto finish; + } Aig_ManStop( pTemp ); RetValue = Fra_FraigMiterStatus( pNew ); if ( fVerbose ) @@ -264,11 +325,33 @@ PRT( "Time", clock() - clkTotal ); // get the miter status RetValue = Fra_FraigMiterStatus( pNew ); + // try interplation +clk = clock(); + if ( RetValue == -1 && Aig_ManRegNum(pNew) > 0 ) + { + 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 ); + if ( fVerbose ) + { + if ( RetValue == 1 ) + printf( "Property proved using interpolation. " ); + else if ( RetValue == 0 ) + printf( "Property DISPROVED with cex at depth %d using interpolation. ", Depth ); + else if ( RetValue == -1 ) + printf( "Property UNDECIDED after interpolation. " ); + else + assert( 0 ); +PRT( "Time", clock() - clk ); + } + } + // try reachability analysis - if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 ) + if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 && Aig_ManRegNum(pNew) > 0 ) { extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ); - assert( Aig_ManRegNum(pNew) > 0 ); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 ); diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index a723c981..1b135212 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -347,7 +347,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose ) // perform SCL for the given design pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p)); - pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL ); + pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 ); Aig_ManStop( pTemp ); // finalize the transformation diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c index ffd32206..c3bb0875 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -519,8 +519,6 @@ int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTrans p->pAigTrans = Saig_ManTransformed( pAig ); else p->pAigTrans = Saig_ManDuplicated( pAig ); -// p->pAigTrans = Dar_ManRwsat( pAigTemp = p->pAigTrans, 1, 0 ); -// Aig_ManStop( pAigTemp ); // derive CNF for the transformed AIG clk = clock(); p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 87c040ad..f914b9c4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -9166,6 +9166,12 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } + if ( Abc_NtkLatchNum(pNtk) > 0 ) + { + fprintf( pErr, "The network has registers. Use \"dprove\".\n" ); + return 1; + } + clk = clock(); if ( Abc_NtkIsStrash(pNtk) ) @@ -13923,7 +13929,7 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - nFrames = 16; + nFrames = 2; fPhaseAbstract = 1; fRetimeFirst = 1; fRetimeRegs = 1; @@ -14020,6 +14026,8 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; + int fTryComb; + int fTryBmc; int nFrames; int fPhaseAbstract; int fRetimeFirst; @@ -14027,31 +14035,55 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) int fFraiging; int fVerbose; int fVeryVerbose; + int TimeLimit; int c; - extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ); + extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, + int nFrames, int fPhaseAbstract, int fRetimeFirst, + int fRetimeRegs, int fFraiging, int fVerbose, + int fVeryVerbose, int TimeLimit ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nFrames = 8; - fPhaseAbstract = 1; - fRetimeFirst = 1; - fRetimeRegs = 1; - fFraiging = 1; - fVerbose = 0; - fVeryVerbose = 0; + fTryComb = 1; + fTryBmc = 1; + nFrames = 2; + fPhaseAbstract = 1; + fRetimeFirst = 1; + fRetimeRegs = 1; + fFraiging = 1; + fVerbose = 0; + fVeryVerbose = 0; + TimeLimit = 300; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cbTFarmfwvh" ) ) != EOF ) { switch ( c ) { + case 'c': + fTryComb ^= 1; + break; + case 'b': + fTryBmc ^= 1; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + TimeLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( TimeLimit < 0 ) + goto usage; + break; case 'F': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } nFrames = atoi(argv[globalUtilOptind]); @@ -14095,13 +14127,16 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) } // perform verification - Abc_NtkDarProve( pNtk, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose ); + Abc_NtkDarProve( pNtk, fTryComb, fTryBmc, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit ); return 0; usage: - fprintf( pErr, "usage: dprove [-F num] [-armfwvh]\n" ); + fprintf( pErr, "usage: dprove [-F num] [-T num] [-carmfwvh]\n" ); fprintf( pErr, "\t performs SEC on the sequential miter\n" ); fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames ); + fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", TimeLimit ); + fprintf( pErr, "\t-c : toggles using CEC before attempting SEC [default = %s]\n", fTryComb? "yes": "no" ); + fprintf( pErr, "\t-b : toggles using BMC before attempting SEC [default = %s]\n", fTryBmc? "yes": "no" ); fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", fPhaseAbstract? "yes": "no" ); fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" ); fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", fRetimeRegs? "yes": "no" ); @@ -14742,7 +14777,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) nBTLimit = 20000; fRewrite = 0; fTransLoop = 1; - fVerbose = 1; + fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Crtvh" ) ) != EOF ) { @@ -17530,11 +17565,11 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv ) int fVeryVerbose; int c; - extern int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ); + extern int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit ); extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ); // set defaults - nFrames = 8; + nFrames = 2; fPhaseAbstract = 0; fRetimeFirst = 0; fRetimeRegs = 0; @@ -17591,7 +17626,7 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv ) pAig = Ntl_ManPrepareSec( pArgvNew[0], pArgvNew[1] ); if ( pAig == NULL ) return 0; - Fra_FraigSec( pAig, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose ); + Fra_FraigSec( pAig, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, 0 ); Aig_ManStop( pAig ); return 0; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index d4771989..75995a60 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1115,7 +1115,7 @@ PRT( "Time", clock() - clkTotal ); Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars ) { Fraig_Params_t Params; - Abc_Ntk_t * pNtkAig, * pNtkFraig; + Abc_Ntk_t * pNtkAig = NULL, * pNtkFraig; Aig_Man_t * pMan, * pTemp; int clk = clock(); @@ -1140,20 +1140,23 @@ PRT( "Initial fraiging time", clock() - clk ); if ( pMan == NULL ) return NULL; +// pPars->TimeLimit = 5.0; pMan = Fra_FraigInduction( pTemp = pMan, pPars ); Aig_ManStop( pTemp ); - - if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) - pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); - else + if ( pMan ) { - Abc_Obj_t * pObj; - int i; - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); - Abc_NtkForEachLatch( pNtkAig, pObj, i ) - Abc_LatchSetInit0( pObj ); + if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + else + { + Abc_Obj_t * pObj; + int i; + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Abc_NtkForEachLatch( pNtkAig, pObj, i ) + Abc_LatchSetInit0( pObj ); + } + Aig_ManStop( pMan ); } - Aig_ManStop( pMan ); return pNtkAig; } @@ -1161,7 +1164,7 @@ PRT( "Initial fraiging time", clock() - clk ); Synopsis [Computes latch correspondence.] - Description [] + Description [] SideEffects [] @@ -1171,23 +1174,26 @@ PRT( "Initial fraiging time", clock() - clk ); Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose ) { Aig_Man_t * pMan, * pTemp; - Abc_Ntk_t * pNtkAig; + Abc_Ntk_t * pNtkAig = NULL; pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) return NULL; - pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL ); + pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL, 0.0 ); Aig_ManStop( pTemp ); - if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) - pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); - else + if ( pMan ) { - Abc_Obj_t * pObj; - int i; - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); - Abc_NtkForEachLatch( pNtkAig, pObj, i ) - Abc_LatchSetInit0( pObj ); + if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + else + { + Abc_Obj_t * pObj; + int i; + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Abc_NtkForEachLatch( pNtkAig, pObj, i ) + Abc_LatchSetInit0( pObj ); + } + Aig_ManStop( pMan ); } - Aig_ManStop( pMan ); return pNtkAig; } @@ -1205,13 +1211,13 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose ) { Aig_Man_t * pMan; - int RetValue, clk = clock(); + int RetValue = -1, clk = clock(); // derive the AIG manager pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) { printf( "Converting miter into AIG has failed.\n" ); - return -1; + return RetValue; } assert( pMan->nRegs > 0 ); pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); @@ -1221,6 +1227,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, in { int iFrame; RetValue = Saig_ManBmcSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose, &iFrame ); + pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; if ( RetValue == 1 ) printf( "No output was asserted in %d frames. ", nFrames ); else if ( RetValue == -1 ) @@ -1239,13 +1246,17 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, in { Fra_Cex_t * pCex = pNtk->pSeqModel; printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame ); + RetValue = 0; } else + { printf( "No output was asserted in %d frames. ", nFrames ); + RetValue = 1; + } } PRT( "Time", clock() - clk ); Aig_ManStop( pMan ); - return 1; + return RetValue; } /**Function************************************************************* @@ -1298,10 +1309,38 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ) +int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit ) { Aig_Man_t * pMan; int RetValue; + if ( fTryComb ) + { + Prove_Params_t Params, * pParams = &Params; + Abc_Ntk_t * pNtkComb; + int RetValue, clk = clock(); + // create combinational network + pNtkComb = Abc_NtkDup( pNtk ); + Abc_NtkMakeComb( pNtkComb, 1 ); + // solve it using combinational equivalence checking + Prove_ParamsSetDefault( pParams ); + RetValue = Abc_NtkIvyProve( &pNtkComb, pParams ); + // transfer model if given + pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL; + Abc_NtkDelete( pNtkComb ); + // return the result, if solved + if ( RetValue == 1 ) + { + printf( "Networks are equivalent after CEC. " ); + PRT( "Time", clock() - clk ); + return RetValue; + } + } + if ( fTryBmc ) + { + RetValue = Abc_NtkDarBmc( pNtk, 10, 1000, 0, 1, 0 ); + if ( RetValue == 0 ) + return RetValue; + } // derive the AIG manager pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) @@ -1311,7 +1350,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fPhaseAbstract, int fRet } assert( pMan->nRegs > 0 ); // perform verification - RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose ); + RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; if ( pNtk->pSeqModel ) { @@ -1405,7 +1444,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhase assert( pMan->nRegs > 0 ); // perform verification - RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose ); + RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, 0 ); Aig_ManStop( pMan ); return RetValue; } diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/src/map/pcm/module.make diff --git a/src/map/ply/module.make b/src/map/ply/module.make new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/src/map/ply/module.make |