Skip to content

A
abc
Commit 47036e1e by Alan Mishchenko
Options

Version abc80511_2

parent 582cf0b9
Showing with 240 additions and 58 deletions
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 );
......
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 )
......
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;
......
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 );
......
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
......
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) );
......
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;
......
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;
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment