diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 69 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 97 |
2 files changed, 120 insertions, 46 deletions
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; } |