Skip to content

A
abc
Commit 74ff01bf by Alan Mishchenko
Options

Version abc80515

parent 37b6c727
Showing with 334 additions and 246 deletions
abc.rc
...@@ -56,6 +56,7 @@ alias r3f retime -M 3 -f ...@@ -56,6 +56,7 @@ alias r3f retime -M 3 -f
alias r3b retime -M 3 -b alias r3b retime -M 3 -b
alias ren renode alias ren renode
alias rh read_hie alias rh read_hie
alias ri read_init
alias rl read_blif alias rl read_blif
alias rb read_bench alias rb read_bench
alias ret retime alias ret retime
......
src/aig/fra/fra.h
...@@ -51,6 +51,7 @@ extern "C" { ...@@ -51,6 +51,7 @@ extern "C" {
typedef struct Fra_Par_t_ Fra_Par_t; typedef struct Fra_Par_t_ Fra_Par_t;
typedef struct Fra_Ssw_t_ Fra_Ssw_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_Man_t_ Fra_Man_t;
typedef struct Fra_Cla_t_ Fra_Cla_t; typedef struct Fra_Cla_t_ Fra_Cla_t;
typedef struct Fra_Sml_t_ Fra_Sml_t; typedef struct Fra_Sml_t_ Fra_Sml_t;
...@@ -87,7 +88,7 @@ struct Fra_Par_t_ ...@@ -87,7 +88,7 @@ struct Fra_Par_t_
int fDontShowBar; // does not show progressbar during fraiging int fDontShowBar; // does not show progressbar during fraiging
}; };
// seq SAT sweeping parametesr // seq SAT sweeping parameters
struct Fra_Ssw_t_ struct Fra_Ssw_t_
{ {
int nPartSize; // size of the partition int nPartSize; // size of the partition
...@@ -107,6 +108,27 @@ struct Fra_Ssw_t_ ...@@ -107,6 +108,27 @@ struct Fra_Ssw_t_
float TimeLimit; // the runtime budget for this call 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 // FRAIG equivalence classes
struct Fra_Cla_t_ struct Fra_Cla_t_
{ {
...@@ -329,7 +351,8 @@ extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig ...@@ -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_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 ); extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
/*=== fraSec.c ========================================================*/ /*=== 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 ========================================================*/ /*=== fraSim.c ========================================================*/
extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ); extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ); extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
......
src/aig/fra/fraSec.c
...@@ -40,12 +40,44 @@ ...@@ -40,12 +40,44 @@
SeeAlso [] 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_Ssw_t Pars, * pPars = &Pars;
Fra_Sml_t * pSml; Fra_Sml_t * pSml;
Aig_Man_t * pNew, * pTemp; Aig_Man_t * pNew, * pTemp;
int nFrames, RetValue, nIter, clk, clkTotal = clock(); int nFrames, RetValue, nIter, clk, clkTotal = clock();
int TimeOut = 0;
int fLatchCorr = 0; int fLatchCorr = 0;
float TimeLeft = 0.0; float TimeLeft = 0.0;
...@@ -58,8 +90,8 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetime ...@@ -58,8 +90,8 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetime
// prepare parameters // prepare parameters
memset( pPars, 0, sizeof(Fra_Ssw_t) ); memset( pPars, 0, sizeof(Fra_Ssw_t) );
pPars->fLatchCorr = fLatchCorr; pPars->fLatchCorr = fLatchCorr;
pPars->fVerbose = fVeryVerbose; pPars->fVerbose = pParSec->fVeryVerbose;
if ( fVerbose ) if ( pParSec->fVerbose )
{ {
printf( "Original miter: Latches = %5d. Nodes = %6d.\n", printf( "Original miter: Latches = %5d. Nodes = %6d.\n",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
...@@ -72,7 +104,7 @@ clk = clock(); ...@@ -72,7 +104,7 @@ clk = clock();
pNew = Aig_ManReduceLaches( pNew, 0 ); pNew = Aig_ManReduceLaches( pNew, 0 );
if ( pNew->nRegs ) if ( pNew->nRegs )
pNew = Aig_ManConstReduce( pNew, 0 ); pNew = Aig_ManConstReduce( pNew, 0 );
if ( fVerbose ) if ( pParSec->fVerbose )
{ {
printf( "Sequential cleanup: Latches = %5d. Nodes = %6d. ", printf( "Sequential cleanup: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
...@@ -84,14 +116,14 @@ PRT( "Time", clock() - clk ); ...@@ -84,14 +116,14 @@ PRT( "Time", clock() - clk );
// perform phase abstraction // perform phase abstraction
clk = clock(); clk = clock();
if ( fPhaseAbstract ) if ( pParSec->fPhaseAbstract )
{ {
extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose ); extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose );
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 ); pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
if ( fVerbose ) if ( pParSec->fVerbose )
{ {
printf( "Phase abstraction: Latches = %5d. Nodes = %6d. ", printf( "Phase abstraction: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
...@@ -100,12 +132,12 @@ PRT( "Time", clock() - clk ); ...@@ -100,12 +132,12 @@ PRT( "Time", clock() - clk );
} }
// perform forward retiming // perform forward retiming
if ( fRetimeFirst && pNew->nRegs ) if ( pParSec->fRetimeFirst && pNew->nRegs )
{ {
clk = clock(); clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
if ( fVerbose ) if ( pParSec->fVerbose )
{ {
printf( "Forward retiming: Latches = %5d. Nodes = %6d. ", printf( "Forward retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
...@@ -120,22 +152,24 @@ clk = clock(); ...@@ -120,22 +152,24 @@ clk = clock();
pNew = Aig_ManDupOrdered( pTemp = pNew ); pNew = Aig_ManDupOrdered( pTemp = pNew );
// pNew = Aig_ManDupDfs( pTemp = pNew ); // pNew = Aig_ManDupDfs( pTemp = pNew );
Aig_ManStop( pTemp ); 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 ); TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 ) if ( TimeLeft == 0.0 )
{ {
printf( "Runtime limit exceeded.\n" ); printf( "Runtime limit exceeded.\n" );
RetValue = -1; RetValue = -1;
TimeOut = 1;
goto finish; 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 ) if ( pNew == NULL )
{ {
pNew = pTemp; pNew = pTemp;
RetValue = -1; RetValue = -1;
TimeOut = 1;
goto finish; goto finish;
} }
p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL; p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
...@@ -148,7 +182,7 @@ PRT( "Time", clock() - clkTotal ); ...@@ -148,7 +182,7 @@ PRT( "Time", clock() - clkTotal );
return RetValue; return RetValue;
} }
if ( fVerbose ) if ( pParSec->fVerbose )
{ {
printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ", printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ",
nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
...@@ -156,25 +190,26 @@ PRT( "Time", clock() - clk ); ...@@ -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 ); TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 ) if ( TimeLeft == 0.0 )
{ {
printf( "Runtime limit exceeded.\n" ); printf( "Runtime limit exceeded.\n" );
RetValue = -1; RetValue = -1;
TimeOut = 1;
goto finish; goto finish;
} }
} }
// perform fraiging // perform fraiging
if ( fFraiging ) if ( pParSec->fFraiging )
{ {
clk = clock(); clk = clock();
pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 ); pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
if ( fVerbose ) if ( pParSec->fVerbose )
{ {
printf( "Fraiging: Latches = %5d. Nodes = %6d. ", printf( "Fraiging: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
...@@ -189,20 +224,21 @@ PRT( "Time", clock() - clk ); ...@@ -189,20 +224,21 @@ PRT( "Time", clock() - clk );
if ( RetValue >= 0 ) if ( RetValue >= 0 )
goto finish; 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 ); TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 ) if ( TimeLeft == 0.0 )
{ {
printf( "Runtime limit exceeded.\n" ); printf( "Runtime limit exceeded.\n" );
RetValue = -1; RetValue = -1;
TimeOut = 1;
goto finish; goto finish;
} }
} }
// perform min-area retiming // 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 ); extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
clk = clock(); clk = clock();
...@@ -213,7 +249,7 @@ clk = clock(); ...@@ -213,7 +249,7 @@ clk = clock();
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
pNew = Aig_ManDupOrdered( pTemp = pNew ); pNew = Aig_ManDupOrdered( pTemp = pNew );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
if ( fVerbose ) if ( pParSec->fVerbose )
{ {
printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ", printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
...@@ -224,16 +260,17 @@ PRT( "Time", clock() - clk ); ...@@ -224,16 +260,17 @@ PRT( "Time", clock() - clk );
// perform seq sweeping while increasing the number of frames // perform seq sweeping while increasing the number of frames
RetValue = Fra_FraigMiterStatus( pNew ); RetValue = Fra_FraigMiterStatus( pNew );
if ( RetValue == -1 ) 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 ); TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 ) if ( TimeLeft == 0.0 )
{ {
printf( "Runtime limit exceeded.\n" ); printf( "Runtime limit exceeded.\n" );
RetValue = -1; RetValue = -1;
TimeOut = 1;
goto finish; goto finish;
} }
} }
...@@ -246,11 +283,12 @@ clk = clock(); ...@@ -246,11 +283,12 @@ clk = clock();
{ {
pNew = pTemp; pNew = pTemp;
RetValue = -1; RetValue = -1;
TimeOut = 1;
goto finish; goto finish;
} }
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
RetValue = Fra_FraigMiterStatus( pNew ); RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose ) if ( pParSec->fVerbose )
{ {
printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ", printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ",
nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
...@@ -260,7 +298,7 @@ PRT( "Time", clock() - clk ); ...@@ -260,7 +298,7 @@ PRT( "Time", clock() - clk );
break; break;
// perform retiming // perform retiming
// if ( fRetimeFirst && pNew->nRegs ) // if ( pParSec->fRetimeFirst && pNew->nRegs )
if ( 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 ); 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(); ...@@ -272,7 +310,7 @@ clk = clock();
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
pNew = Aig_ManDupOrdered( pTemp = pNew ); pNew = Aig_ManDupOrdered( pTemp = pNew );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
if ( fVerbose ) if ( pParSec->fVerbose )
{ {
printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ", printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
...@@ -290,7 +328,7 @@ clk = clock(); ...@@ -290,7 +328,7 @@ clk = clock();
// pNew = Dar_ManRewriteDefault( pTemp = pNew ); // pNew = Dar_ManRewriteDefault( pTemp = pNew );
pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0 ); pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0 );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
if ( fVerbose ) if ( pParSec->fVerbose )
{ {
printf( "Rewriting: Latches = %5d. Nodes = %6d. ", printf( "Rewriting: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
...@@ -302,7 +340,7 @@ PRT( "Time", clock() - clk ); ...@@ -302,7 +340,7 @@ PRT( "Time", clock() - clk );
{ {
clk = clock(); clk = clock();
pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) ); 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. ", printf( "Seq simulation : Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
...@@ -327,14 +365,14 @@ PRT( "Time", clock() - clkTotal ); ...@@ -327,14 +365,14 @@ PRT( "Time", clock() - clkTotal );
// try interplation // try interplation
clk = clock(); 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 ); extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
int Depth; int Depth;
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
RetValue = Saig_Interpolate( pNew, 5000, 0, 1, fVeryVerbose, &Depth ); RetValue = Saig_Interpolate( pNew, 5000, 0, 1, pParSec->fVeryVerbose, &Depth );
if ( fVerbose ) if ( pParSec->fVerbose )
{ {
if ( RetValue == 1 ) if ( RetValue == 1 )
printf( "Property proved using interpolation. " ); printf( "Property proved using interpolation. " );
...@@ -349,7 +387,7 @@ PRT( "Time", clock() - clk ); ...@@ -349,7 +387,7 @@ PRT( "Time", clock() - clk );
} }
// try reachability analysis // 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 ); 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); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
...@@ -371,14 +409,16 @@ PRT( "Time", clock() - clk ); ...@@ -371,14 +409,16 @@ PRT( "Time", clock() - clk );
iCount = 0; iCount = 0;
for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ ) for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
{ {
int TimeLimitCopy = 0;
// get the remaining time for this output // 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 ); TimeLeft = AIG_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 ) if ( TimeLeft == 0.0 )
{ {
printf( "Runtime limit exceeded.\n" ); printf( "Runtime limit exceeded.\n" );
TimeOut = 1;
goto finish; goto finish;
} }
TimeLimit2 = 1 + (int)TimeLeft; TimeLimit2 = 1 + (int)TimeLeft;
...@@ -390,12 +430,23 @@ PRT( "Time", clock() - clk ); ...@@ -390,12 +430,23 @@ PRT( "Time", clock() - clk );
iCount++; iCount++;
printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter ); printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
pNew2 = Aig_ManDupOneOutput( pNew, i ); 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 ); Aig_ManStop( pNew2 );
if ( RetValue2 == 0 ) if ( RetValue2 == 0 )
goto finish; goto finish;
if ( RetValue2 == -1 ) if ( RetValue2 == -1 )
{
fOneUnsolved = 1; fOneUnsolved = 1;
if ( pParSec->fStopOnFirstFail )
break;
}
} }
if ( fOneUnsolved ) if ( fOneUnsolved )
RetValue = -1; RetValue = -1;
...@@ -410,22 +461,41 @@ finish: ...@@ -410,22 +461,41 @@ finish:
{ {
printf( "Networks are equivalent. " ); printf( "Networks are equivalent. " );
PRT( "Time", clock() - clkTotal ); PRT( "Time", clock() - clkTotal );
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: PASS " );
PRT( "Time", clock() - clkTotal );
}
} }
else if ( RetValue == 0 ) else if ( RetValue == 0 )
{ {
printf( "Networks are NOT EQUIVALENT. " ); printf( "Networks are NOT EQUIVALENT. " );
PRT( "Time", clock() - clkTotal ); 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. " ); printf( "Networks are UNDECIDED. " );
PRT( "Time", clock() - clkTotal ); PRT( "Time", clock() - clkTotal );
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++ ); sprintf( pFileName, "sm%03d.aig", Counter++ );
Ioa_WriteAiger( pNew, pFileName, 0, 0 ); Ioa_WriteAiger( pNew, pFileName, 0, 0 );
printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName ); printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
} }
}
if ( pNew )
Aig_ManStop( pNew ); Aig_ManStop( pNew );
return RetValue; return RetValue;
} }
......
src/aig/ioa/ioaUtil.c
...@@ -69,20 +69,10 @@ int Ioa_FileSize( char * pFileName ) ...@@ -69,20 +69,10 @@ int Ioa_FileSize( char * pFileName )
***********************************************************************/ ***********************************************************************/
char * Ioa_FileNameGeneric( char * FileName ) char * Ioa_FileNameGeneric( char * FileName )
{ {
char * pDot; char * pDot, * pRes;
char * pUnd;
char * pRes;
// find the generic name of the file
pRes = Aig_UtilStrsav( FileName ); pRes = Aig_UtilStrsav( FileName );
// find the pointer to the "." symbol in the file name if ( (pDot = strrchr( pRes, '.' )) )
// pUnd = strstr( FileName, "_" ); *pDot = 0;
pUnd = NULL;
pDot = strstr( FileName, "." );
if ( pUnd )
pRes[pUnd - FileName] = 0;
else if ( pDot )
pRes[pDot - FileName] = 0;
return pRes; return pRes;
} }
...@@ -107,8 +97,7 @@ char * Ioa_FileNameGenericAppend( char * pBase, char * pSuffix ) ...@@ -107,8 +97,7 @@ char * Ioa_FileNameGenericAppend( char * pBase, char * pSuffix )
return Buffer; return Buffer;
} }
strcpy( Buffer, pBase ); strcpy( Buffer, pBase );
pDot = strstr( Buffer, "." ); if ( (pDot = strrchr( Buffer, '.' )) )
if ( pDot )
*pDot = 0; *pDot = 0;
strcat( Buffer, pSuffix ); strcat( Buffer, pSuffix );
// find the last occurrance of slash // find the last occurrance of slash
......
src/aig/nwk/nwkMan.c
...@@ -174,19 +174,10 @@ int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl ) ...@@ -174,19 +174,10 @@ int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl )
***********************************************************************/ ***********************************************************************/
char * Nwk_FileNameGeneric( char * FileName ) char * Nwk_FileNameGeneric( char * FileName )
{ {
char * pDot; char * pDot, * pRes;
char * pUnd;
char * pRes;
// find the generic name of the file
pRes = Aig_UtilStrsav( FileName ); pRes = Aig_UtilStrsav( FileName );
// find the pointer to the "." symbol in the file name if ( (pDot = strrchr( pRes, '.' )) )
// pUnd = strstr( FileName, "_" ); *pDot = 0;
pUnd = NULL;
pDot = strstr( FileName, "." );
if ( pUnd )
pRes[pUnd - FileName] = 0;
else if ( pDot )
pRes[pDot - FileName] = 0;
return pRes; return pRes;
} }
......
src/aig/saig/saigBmc.c
...@@ -182,7 +182,6 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim ...@@ -182,7 +182,6 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
Aig_Man_t * pFrames, * pAigTemp; Aig_Man_t * pFrames, * pAigTemp;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int status, clk, Lit, i, RetValue = 1; int status, clk, Lit, i, RetValue = 1;
*piFrame = -1;
// derive the timeframes // derive the timeframes
clk = clock(); clk = clock();
if ( nSizeMax > 0 ) if ( nSizeMax > 0 )
...@@ -192,6 +191,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim ...@@ -192,6 +191,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
} }
else else
pFrames = Saig_ManFramesBmc( pAig, nFrames ); pFrames = Saig_ManFramesBmc( pAig, nFrames );
*piFrame = nFrames;
if ( fVerbose ) if ( fVerbose )
{ {
printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
......
src/aig/saig/saigInter.c
...@@ -178,6 +178,7 @@ Aig_Man_t * Saig_ManTransformed( Aig_Man_t * p ) ...@@ -178,6 +178,7 @@ Aig_Man_t * Saig_ManTransformed( Aig_Man_t * p )
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
{ {
pObj = Aig_Mux( pNew, pCtrl, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) ); pObj = Aig_Mux( pNew, pCtrl, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
// pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) );
Aig_ObjCreatePo( pNew, pObj ); Aig_ObjCreatePo( pNew, pObj );
} }
Aig_ManCleanup( pNew ); Aig_ManCleanup( pNew );
...@@ -566,10 +567,10 @@ p->timeCnf += clock() - clk; ...@@ -566,10 +567,10 @@ p->timeCnf += clock() - clk;
// iterate the interpolation procedure // iterate the interpolation procedure
for ( i = 0; ; i++ ) for ( i = 0; ; i++ )
{ {
if ( p->nFrames + i >= 100 ) if ( p->nFrames + i >= 75 )
{ {
if ( fVerbose ) if ( fVerbose )
printf( "Reached limit (%d) on the number of timeframes.\n", 100 ); printf( "Reached limit (%d) on the number of timeframes.\n", 75 );
p->timeTotal = clock() - clkTotal; p->timeTotal = clock() - clkTotal;
Saig_ManagerFree( p ); Saig_ManagerFree( p );
return -1; return -1;
......
src/base/abc/1.txt deleted 100644 → 0
Comparing files abcDfs.c and C:\_PROJECTS\AARON\FRETIME\SRC\BASE\ABC\ABCDFS.C
***** abcDfs.c
return pNode->Level;
assert( Abc_ObjIsNode( pNode ) );
// if this node is already visited, return
***** C:\_PROJECTS\AARON\FRETIME\SRC\BASE\ABC\ABCDFS.C
return pNode->Level;
assert( Abc_ObjIsNode( pNode ) || pNode->Type == ABC_OBJ_CONST1);
// if this node is already visited, return
*****
***** abcDfs.c
return pNode->Level;
assert( Abc_ObjIsNode( pNode ) );
// if this node is already visited, return
***** C:\_PROJECTS\AARON\FRETIME\SRC\BASE\ABC\ABCDFS.C
return pNode->Level;
assert( Abc_ObjIsNode( pNode ) || pNode->Type == ABC_OBJ_CONST1);
// if this node is already visited, return
*****
src/base/abc/abcBlifMv.c
...@@ -135,6 +135,7 @@ static inline int Abc_StringGetNumber( char ** ppStr ) ...@@ -135,6 +135,7 @@ static inline int Abc_StringGetNumber( char ** ppStr )
***********************************************************************/ ***********************************************************************/
int Abc_NodeStrashBlifMv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ) int Abc_NodeStrashBlifMv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
{ {
int fAddFreeVars = 1;
char * pSop; char * pSop;
Abc_Obj_t ** pValues, ** pValuesF, ** pValuesF2; Abc_Obj_t ** pValues, ** pValuesF, ** pValuesF2;
Abc_Obj_t * pTemp, * pTemp2, * pFanin, * pFanin2, * pNet; Abc_Obj_t * pTemp, * pTemp2, * pFanin, * pFanin2, * pNet;
...@@ -168,7 +169,17 @@ int Abc_NodeStrashBlifMv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ) ...@@ -168,7 +169,17 @@ int Abc_NodeStrashBlifMv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
else else
Index = Abc_StringGetNumber( &pSop ); Index = Abc_StringGetNumber( &pSop );
assert( Index < nValues ); assert( Index < nValues );
////////////////////////////////////////////
// adding free variables for binary ND-constants
if ( fAddFreeVars && nValues == 2 && *pSop == '-' )
{
pValues[1] = Abc_NtkCreatePi(pNtkNew);
pValues[0] = Abc_ObjNot( pValues[1] );
Abc_ObjAssignName( pValues[1], "free_var_", Abc_ObjName(pValues[1]) );
}
else
pValues[Index] = Abc_AigConst1(pNtkNew); pValues[Index] = Abc_AigConst1(pNtkNew);
////////////////////////////////////////////
// save the values in the fanout net // save the values in the fanout net
pNet->pCopy = (Abc_Obj_t *)pValues; pNet->pCopy = (Abc_Obj_t *)pValues;
return 1; return 1;
...@@ -414,6 +425,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ) ...@@ -414,6 +425,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
for ( v = 0; v < nValues; v++ ) for ( v = 0; v < nValues; v++ )
{ {
pValues[v] = Abc_NtkCreatePi( pNtkNew ); pValues[v] = Abc_NtkCreatePi( pNtkNew );
if ( nValuesMax == 2 )
Abc_ObjAssignName( pValues[v], Abc_ObjName(pNet), NULL );
else
Abc_NtkConvertAssignName( pValues[v], pNet, v ); Abc_NtkConvertAssignName( pValues[v], pNet, v );
} }
// save the values in the fanout net // save the values in the fanout net
...@@ -432,6 +446,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ) ...@@ -432,6 +446,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
for ( v = 0; v < nValues; v++ ) for ( v = 0; v < nValues; v++ )
{ {
pValues[v] = Abc_NtkCreateBo( pNtkNew ); pValues[v] = Abc_NtkCreateBo( pNtkNew );
if ( nValuesMax == 2 )
Abc_ObjAssignName( pValues[v], Abc_ObjName(pNet), NULL );
else
Abc_NtkConvertAssignName( pValues[v], pNet, v ); Abc_NtkConvertAssignName( pValues[v], pNet, v );
nCount1++; nCount1++;
} }
...@@ -455,6 +472,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ) ...@@ -455,6 +472,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
for ( k = 0; k < nBits; k++ ) for ( k = 0; k < nBits; k++ )
{ {
pBits[k] = Abc_NtkCreatePi( pNtkNew ); pBits[k] = Abc_NtkCreatePi( pNtkNew );
if ( nValuesMax == 2 )
Abc_ObjAssignName( pBits[k], Abc_ObjName(pNet), NULL );
else
Abc_NtkConvertAssignName( pBits[k], pNet, k ); Abc_NtkConvertAssignName( pBits[k], pNet, k );
} }
// encode the values // encode the values
...@@ -484,6 +504,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ) ...@@ -484,6 +504,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
for ( k = 0; k < nBits; k++ ) for ( k = 0; k < nBits; k++ )
{ {
pBits[k] = Abc_NtkCreateBo( pNtkNew ); pBits[k] = Abc_NtkCreateBo( pNtkNew );
if ( nValuesMax == 2 )
Abc_ObjAssignName( pBits[k], Abc_ObjName(pNet), NULL );
else
Abc_NtkConvertAssignName( pBits[k], pNet, k ); Abc_NtkConvertAssignName( pBits[k], pNet, k );
nCount1++; nCount1++;
} }
...@@ -522,15 +545,18 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ) ...@@ -522,15 +545,18 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
continue; continue;
pNet = Abc_ObjFanin0(pObj); pNet = Abc_ObjFanin0(pObj);
// skip marked nets // skip marked nets
if ( Abc_NodeIsTravIdCurrent(pNet) ) // if ( Abc_NodeIsTravIdCurrent(pNet) )
continue; // continue;
Abc_NodeSetTravIdCurrent( pNet ); // Abc_NodeSetTravIdCurrent( pNet );
nValues = Abc_ObjMvVarNum(pNet); nValues = Abc_ObjMvVarNum(pNet);
pValues = (Abc_Obj_t **)pNet->pCopy; pValues = (Abc_Obj_t **)pNet->pCopy;
for ( v = 0; v < nValues; v++ ) for ( v = 0; v < nValues; v++ )
{ {
pTemp = Abc_NtkCreatePo( pNtkNew ); pTemp = Abc_NtkCreatePo( pNtkNew );
Abc_ObjAddFanin( pTemp, pValues[v] ); Abc_ObjAddFanin( pTemp, pValues[v] );
if ( nValuesMax == 2 )
Abc_ObjAssignName( pTemp, Abc_ObjName(pNet), NULL );
else
Abc_NtkConvertAssignName( pTemp, pNet, v ); Abc_NtkConvertAssignName( pTemp, pNet, v );
} }
} }
...@@ -540,21 +566,24 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ) ...@@ -540,21 +566,24 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
continue; continue;
pNet = Abc_ObjFanin0(pObj); pNet = Abc_ObjFanin0(pObj);
// skip marked nets // skip marked nets
if ( Abc_NodeIsTravIdCurrent(pNet) ) // if ( Abc_NodeIsTravIdCurrent(pNet) )
continue; // continue;
Abc_NodeSetTravIdCurrent( pNet ); // Abc_NodeSetTravIdCurrent( pNet );
nValues = Abc_ObjMvVarNum(pNet); nValues = Abc_ObjMvVarNum(pNet);
pValues = (Abc_Obj_t **)pNet->pCopy; pValues = (Abc_Obj_t **)pNet->pCopy;
for ( v = 0; v < nValues; v++ ) for ( v = 0; v < nValues; v++ )
{ {
pTemp = Abc_NtkCreateBi( pNtkNew ); pTemp = Abc_NtkCreateBi( pNtkNew );
Abc_ObjAddFanin( pTemp, pValues[v] ); Abc_ObjAddFanin( pTemp, pValues[v] );
if ( nValuesMax == 2 )
Abc_ObjAssignName( pTemp, Abc_ObjName(pNet), NULL );
else
Abc_NtkConvertAssignName( pTemp, pNet, v ); Abc_NtkConvertAssignName( pTemp, pNet, v );
nCount2++; nCount2++;
} }
} }
} }
else else // if ( fPositional == 0 )
{ {
Abc_NtkForEachCo( pNtk, pObj, i ) Abc_NtkForEachCo( pNtk, pObj, i )
{ {
...@@ -562,9 +591,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ) ...@@ -562,9 +591,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
continue; continue;
pNet = Abc_ObjFanin0(pObj); pNet = Abc_ObjFanin0(pObj);
// skip marked nets // skip marked nets
if ( Abc_NodeIsTravIdCurrent(pNet) ) // if ( Abc_NodeIsTravIdCurrent(pNet) )
continue; // continue;
Abc_NodeSetTravIdCurrent( pNet ); // Abc_NodeSetTravIdCurrent( pNet );
nValues = Abc_ObjMvVarNum(pNet); nValues = Abc_ObjMvVarNum(pNet);
pValues = (Abc_Obj_t **)pNet->pCopy; pValues = (Abc_Obj_t **)pNet->pCopy;
nBits = Extra_Base2Log( nValues ); nBits = Extra_Base2Log( nValues );
...@@ -576,6 +605,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ) ...@@ -576,6 +605,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
pBit = Abc_AigOr( pNtkNew->pManFunc, pBit, pValues[v] ); pBit = Abc_AigOr( pNtkNew->pManFunc, pBit, pValues[v] );
pTemp = Abc_NtkCreatePo( pNtkNew ); pTemp = Abc_NtkCreatePo( pNtkNew );
Abc_ObjAddFanin( pTemp, pBit ); Abc_ObjAddFanin( pTemp, pBit );
if ( nValuesMax == 2 )
Abc_ObjAssignName( pTemp, Abc_ObjName(pNet), NULL );
else
Abc_NtkConvertAssignName( pTemp, pNet, k ); Abc_NtkConvertAssignName( pTemp, pNet, k );
} }
} }
...@@ -585,9 +617,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ) ...@@ -585,9 +617,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
continue; continue;
pNet = Abc_ObjFanin0(pObj); pNet = Abc_ObjFanin0(pObj);
// skip marked nets // skip marked nets
if ( Abc_NodeIsTravIdCurrent(pNet) ) // if ( Abc_NodeIsTravIdCurrent(pNet) )
continue; // continue;
Abc_NodeSetTravIdCurrent( pNet ); // Abc_NodeSetTravIdCurrent( pNet );
nValues = Abc_ObjMvVarNum(pNet); nValues = Abc_ObjMvVarNum(pNet);
pValues = (Abc_Obj_t **)pNet->pCopy; pValues = (Abc_Obj_t **)pNet->pCopy;
nBits = Extra_Base2Log( nValues ); nBits = Extra_Base2Log( nValues );
...@@ -599,6 +631,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ) ...@@ -599,6 +631,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
pBit = Abc_AigOr( pNtkNew->pManFunc, pBit, pValues[v] ); pBit = Abc_AigOr( pNtkNew->pManFunc, pBit, pValues[v] );
pTemp = Abc_NtkCreateBi( pNtkNew ); pTemp = Abc_NtkCreateBi( pNtkNew );
Abc_ObjAddFanin( pTemp, pBit ); Abc_ObjAddFanin( pTemp, pBit );
if ( nValuesMax == 2 )
Abc_ObjAssignName( pTemp, Abc_ObjName(pNet), NULL );
else
Abc_NtkConvertAssignName( pTemp, pNet, k ); Abc_NtkConvertAssignName( pTemp, pNet, k );
nCount2++; nCount2++;
} }
...@@ -607,8 +642,32 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk ) ...@@ -607,8 +642,32 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
if ( Abc_NtkLatchNum(pNtk) ) if ( Abc_NtkLatchNum(pNtk) )
{ {
Vec_Ptr_t * vTemp;
Abc_Obj_t * pLatch, * pObjLi, * pObjLo; Abc_Obj_t * pLatch, * pObjLi, * pObjLo;
int i; int i;
// move free vars to the front among the PIs
vTemp = Vec_PtrAlloc( Vec_PtrSize(pNtkNew->vPis) );
Abc_NtkForEachPi( pNtkNew, pObj, i )
if ( strncmp( Abc_ObjName(pObj), "free_var_", 9 ) == 0 )
Vec_PtrPush( vTemp, pObj );
Abc_NtkForEachPi( pNtkNew, pObj, i )
if ( strncmp( Abc_ObjName(pObj), "free_var_", 9 ) != 0 )
Vec_PtrPush( vTemp, pObj );
assert( Vec_PtrSize(vTemp) == Vec_PtrSize(pNtkNew->vPis) );
Vec_PtrFree( pNtkNew->vPis );
pNtkNew->vPis = vTemp;
// move free vars to the front among the CIs
vTemp = Vec_PtrAlloc( Vec_PtrSize(pNtkNew->vCis) );
Abc_NtkForEachCi( pNtkNew, pObj, i )
if ( strncmp( Abc_ObjName(pObj), "free_var_", 9 ) == 0 )
Vec_PtrPush( vTemp, pObj );
Abc_NtkForEachCi( pNtkNew, pObj, i )
if ( strncmp( Abc_ObjName(pObj), "free_var_", 9 ) != 0 )
Vec_PtrPush( vTemp, pObj );
assert( Vec_PtrSize(vTemp) == Vec_PtrSize(pNtkNew->vCis) );
Vec_PtrFree( pNtkNew->vCis );
pNtkNew->vCis = vTemp;
// create registers
assert( nCount1 == nCount2 ); assert( nCount1 == nCount2 );
for ( i = 0; i < nCount1; i++ ) for ( i = 0; i < nCount1; i++ )
{ {
......
src/base/abc/abcFanio.c
...@@ -92,6 +92,10 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ) ...@@ -92,6 +92,10 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
{ {
int x = 0; int x = 0;
} }
if ( pObj->Id == 1960 )
{
int x = 0;
}
// printf( "Adding fanin of %s ", Abc_ObjName(pObj) ); // printf( "Adding fanin of %s ", Abc_ObjName(pObj) );
// printf( "to be %s\n", Abc_ObjName(pFanin) ); // printf( "to be %s\n", Abc_ObjName(pFanin) );
} }
......
src/base/abci/abc.c
...@@ -13915,34 +13915,24 @@ usage: ...@@ -13915,34 +13915,24 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
Fra_Sec_t SecPar, * pSecPar = &SecPar;
FILE * pOut, * pErr; FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtk1, * pNtk2; Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
int fDelete1, fDelete2; int fDelete1, fDelete2;
char ** pArgvNew; char ** pArgvNew;
int nArgcNew; int nArgcNew;
int nFrames;
int fPhaseAbstract;
int fRetimeFirst;
int fRetimeRegs;
int fFraiging;
int fVerbose;
int fVeryVerbose;
int c; int c;
extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ); extern void Fra_SecSetDefaultParams( Fra_Sec_t * p );
extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * p );
pNtk = Abc_FrameReadNtk(pAbc); pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc); pErr = Abc_FrameReadErr(pAbc);
// set defaults // set defaults
nFrames = 2; Fra_SecSetDefaultParams( pSecPar );
fPhaseAbstract = 1; pSecPar->TimeLimit = 300;
fRetimeFirst = 1;
fRetimeRegs = 1;
fFraiging = 1;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF )
{ {
...@@ -13954,28 +13944,28 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -13954,28 +13944,28 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nFrames = atoi(argv[globalUtilOptind]); pSecPar->nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nFrames < 0 ) if ( pSecPar->nFramesMax < 0 )
goto usage; goto usage;
break; break;
case 'a': case 'a':
fPhaseAbstract ^= 1; pSecPar->fPhaseAbstract ^= 1;
break; break;
case 'r': case 'r':
fRetimeFirst ^= 1; pSecPar->fRetimeFirst ^= 1;
break; break;
case 'm': case 'm':
fRetimeRegs ^= 1; pSecPar->fRetimeRegs ^= 1;
break; break;
case 'f': case 'f':
fFraiging ^= 1; pSecPar->fFraiging ^= 1;
break; break;
case 'w': case 'w':
fVeryVerbose ^= 1; pSecPar->fVeryVerbose ^= 1;
break; break;
case 'v': case 'v':
fVerbose ^= 1; pSecPar->fVerbose ^= 1;
break; break;
default: default:
goto usage; goto usage;
...@@ -13994,7 +13984,7 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -13994,7 +13984,7 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
// perform verification // perform verification
Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose ); Abc_NtkDarSec( pNtk1, pNtk2, pSecPar );
if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
...@@ -14003,13 +13993,13 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -14003,13 +13993,13 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
usage: usage:
fprintf( pErr, "usage: dsec [-F num] [-armfwvh] <file1> <file2>\n" ); fprintf( pErr, "usage: dsec [-F num] [-armfwvh] <file1> <file2>\n" );
fprintf( pErr, "\t performs inductive sequential equivalence checking\n" ); fprintf( pErr, "\t performs inductive sequential equivalence checking\n" );
fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames ); fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", fPhaseAbstract? "yes": "no" ); fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" );
fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" ); fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", fRetimeRegs? "yes": "no" ); fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" );
fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" ); fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tfile1 : (optional) the file with the first network\n"); fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
fprintf( pErr, "\tfile2 : (optional) the file with the second network\n"); fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
...@@ -14031,50 +14021,31 @@ usage: ...@@ -14031,50 +14021,31 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
Fra_Sec_t SecPar, * pSecPar = &SecPar;
FILE * pOut, * pErr; FILE * pOut, * pErr;
Abc_Ntk_t * pNtk; Abc_Ntk_t * pNtk;
int fTryComb;
int fTryBmc;
int nFrames;
int fPhaseAbstract;
int fRetimeFirst;
int fRetimeRegs;
int fFraiging;
int fVerbose;
int fVeryVerbose;
int TimeLimit;
int c; int c;
extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, extern void Fra_SecSetDefaultParams( Fra_Sec_t * p );
int nFrames, int fPhaseAbstract, int fRetimeFirst, extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar );
int fRetimeRegs, int fFraiging, int fVerbose,
int fVeryVerbose, int TimeLimit );
pNtk = Abc_FrameReadNtk(pAbc); pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc); pErr = Abc_FrameReadErr(pAbc);
// set defaults // set defaults
fTryComb = 1; Fra_SecSetDefaultParams( pSecPar );
fTryBmc = 1; pSecPar->TimeLimit = 300;
nFrames = 2;
fPhaseAbstract = 1;
fRetimeFirst = 1;
fRetimeRegs = 1;
fFraiging = 1;
fVerbose = 0;
fVeryVerbose = 0;
TimeLimit = 300;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cbTFarmfwvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "cbTFarmfwvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 'c': case 'c':
fTryComb ^= 1; pSecPar->fTryComb ^= 1;
break; break;
case 'b': case 'b':
fTryBmc ^= 1; pSecPar->fTryBmc ^= 1;
break; break;
case 'T': case 'T':
if ( globalUtilOptind >= argc ) if ( globalUtilOptind >= argc )
...@@ -14082,9 +14053,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -14082,9 +14053,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
TimeLimit = atoi(argv[globalUtilOptind]); pSecPar->TimeLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( TimeLimit < 0 ) if ( pSecPar->TimeLimit < 0 )
goto usage; goto usage;
break; break;
case 'F': case 'F':
...@@ -14093,40 +14064,34 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -14093,40 +14064,34 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nFrames = atoi(argv[globalUtilOptind]); pSecPar->nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nFrames < 0 ) if ( pSecPar->nFramesMax < 0 )
goto usage; goto usage;
break; break;
case 'a': case 'a':
fPhaseAbstract ^= 1; pSecPar->fPhaseAbstract ^= 1;
break; break;
case 'r': case 'r':
fRetimeFirst ^= 1; pSecPar->fRetimeFirst ^= 1;
break; break;
case 'm': case 'm':
fRetimeRegs ^= 1; pSecPar->fRetimeRegs ^= 1;
break; break;
case 'f': case 'f':
fFraiging ^= 1; pSecPar->fFraiging ^= 1;
break; break;
case 'w': case 'w':
fVeryVerbose ^= 1; pSecPar->fVeryVerbose ^= 1;
break; break;
case 'v': case 'v':
fVerbose ^= 1; pSecPar->fVerbose ^= 1;
break; break;
default: default:
goto usage; goto usage;
} }
} }
if ( Abc_NtkLatchNum(pNtk) == 0 )
{
printf( "The network has no latches. Running combinational command \"iprove\".\n" );
Cmd_CommandExecute( pAbc, "orpos; st; iprove" );
return 0;
}
if ( !Abc_NtkIsStrash(pNtk) ) if ( !Abc_NtkIsStrash(pNtk) )
{ {
printf( "This command works only for structrally hashed networks. Run \"st\".\n" ); printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
...@@ -14134,22 +14099,22 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -14134,22 +14099,22 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
// perform verification // perform verification
Abc_NtkDarProve( pNtk, fTryComb, fTryBmc, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit ); Abc_NtkDarProve( pNtk, pSecPar );
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: dprove [-F num] [-T num] [-cbarmfwvh]\n" ); fprintf( pErr, "usage: dprove [-F num] [-T num] [-cbarmfwvh]\n" );
fprintf( pErr, "\t performs SEC on the sequential miter\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-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", TimeLimit ); fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", pSecPar->TimeLimit );
fprintf( pErr, "\t-c : toggles using CEC before attempting SEC [default = %s]\n", fTryComb? "yes": "no" ); fprintf( pErr, "\t-c : toggles using CEC before attempting SEC [default = %s]\n", pSecPar->fTryComb? "yes": "no" );
fprintf( pErr, "\t-b : toggles using BMC before attempting SEC [default = %s]\n", fTryBmc? "yes": "no" ); fprintf( pErr, "\t-b : toggles using BMC before attempting SEC [default = %s]\n", pSecPar->fTryBmc? "yes": "no" );
fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", fPhaseAbstract? "yes": "no" ); fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" );
fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" ); fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", fRetimeRegs? "yes": "no" ); fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" );
fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" ); fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-h : print the command usage\n");
return 1; return 1;
} }
...@@ -17575,29 +17540,22 @@ usage: ...@@ -17575,29 +17540,22 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
Fra_Sec_t SecPar, * pSecPar = &SecPar;
Aig_Man_t * pAig; Aig_Man_t * pAig;
char ** pArgvNew; char ** pArgvNew;
int nArgcNew; int nArgcNew;
int nFrames;
int fPhaseAbstract;
int fRetimeFirst;
int fRetimeRegs;
int fFraiging;
int fVerbose;
int fVeryVerbose;
int c; int c;
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 void Fra_SecSetDefaultParams( Fra_Sec_t * pSecPar );
extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pSecPar );
extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ); extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
// set defaults // set defaults
nFrames = 2; Fra_SecSetDefaultParams( pSecPar );
fPhaseAbstract = 0; pSecPar->nFramesMax = 2;
fRetimeFirst = 0; pSecPar->fPhaseAbstract = 0;
fRetimeRegs = 0; pSecPar->fRetimeFirst = 0;
fFraiging = 1; pSecPar->fRetimeRegs = 0;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF )
{ {
...@@ -17609,28 +17567,28 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -17609,28 +17567,28 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" ); fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nFrames = atoi(argv[globalUtilOptind]); pSecPar->nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nFrames < 0 ) if ( pSecPar->nFramesMax < 0 )
goto usage; goto usage;
break; break;
case 'a': case 'a':
fPhaseAbstract ^= 1; pSecPar->fPhaseAbstract ^= 1;
break; break;
case 'r': case 'r':
fRetimeFirst ^= 1; pSecPar->fRetimeFirst ^= 1;
break; break;
case 'm': case 'm':
fRetimeRegs ^= 1; pSecPar->fRetimeRegs ^= 1;
break; break;
case 'f': case 'f':
fFraiging ^= 1; pSecPar->fFraiging ^= 1;
break; break;
case 'w': case 'w':
fVeryVerbose ^= 1; pSecPar->fVeryVerbose ^= 1;
break; break;
case 'v': case 'v':
fVerbose ^= 1; pSecPar->fVerbose ^= 1;
break; break;
default: default:
goto usage; goto usage;
...@@ -17648,20 +17606,20 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -17648,20 +17606,20 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
pAig = Ntl_ManPrepareSec( pArgvNew[0], pArgvNew[1] ); pAig = Ntl_ManPrepareSec( pArgvNew[0], pArgvNew[1] );
if ( pAig == NULL ) if ( pAig == NULL )
return 0; return 0;
Fra_FraigSec( pAig, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, 0 ); Fra_FraigSec( pAig, pSecPar );
Aig_ManStop( pAig ); Aig_ManStop( pAig );
return 0; return 0;
usage: usage:
fprintf( stdout, "usage: *dsec [-F num] [-armfwvh] <file1> <file2>\n" ); fprintf( stdout, "usage: *dsec [-F num] [-armfwvh] <file1> <file2>\n" );
fprintf( stdout, "\t performs sequential equivalence checking for two designs\n" ); fprintf( stdout, "\t performs sequential equivalence checking for two designs\n" );
fprintf( stdout, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames ); fprintf( stdout, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
fprintf( stdout, "\t-a : toggles the use of phase abstraction [default = %s]\n", fPhaseAbstract? "yes": "no" ); fprintf( stdout, "\t-a : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" );
fprintf( stdout, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" ); fprintf( stdout, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" );
fprintf( stdout, "\t-m : toggles min-register retiming [default = %s]\n", fRetimeRegs? "yes": "no" ); fprintf( stdout, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" );
fprintf( stdout, "\t-f : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" ); fprintf( stdout, "\t-f : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" );
fprintf( stdout, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( stdout, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" );
fprintf( stdout, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); fprintf( stdout, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n"); fprintf( stdout, "\t-h : print the command usage\n");
fprintf( stdout, "\tfile1 : the file with the first design\n"); fprintf( stdout, "\tfile1 : the file with the first design\n");
fprintf( stdout, "\tfile2 : the file with the second design\n"); fprintf( stdout, "\tfile2 : the file with the second design\n");
......
src/base/abci/abcDar.c
...@@ -1229,7 +1229,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in ...@@ -1229,7 +1229,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame ); RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( RetValue == 1 ) if ( RetValue == 1 )
printf( "No output was asserted in %d frames. ", nFrames ); printf( "No output was asserted in %d frames. ", iFrame );
else if ( RetValue == -1 ) else if ( RetValue == -1 )
printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit ); printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
else // if ( RetValue == 0 ) else // if ( RetValue == 0 )
...@@ -1309,15 +1309,17 @@ PRT( "Time", clock() - clk ); ...@@ -1309,15 +1309,17 @@ PRT( "Time", clock() - clk );
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
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 ) int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
{ {
Aig_Man_t * pMan; Aig_Man_t * pMan;
int RetValue; int RetValue, clkTotal = clock();
if ( fTryComb ) if ( pSecPar->fTryComb || Abc_NtkLatchNum(pNtk) == 0 )
{ {
Prove_Params_t Params, * pParams = &Params; Prove_Params_t Params, * pParams = &Params;
Abc_Ntk_t * pNtkComb; Abc_Ntk_t * pNtkComb;
int RetValue, clk = clock(); int RetValue, clk = clock();
if ( Abc_NtkLatchNum(pNtk) == 0 )
printf( "The network has no latches. Running CEC.\n" );
// create combinational network // create combinational network
pNtkComb = Abc_NtkDup( pNtk ); pNtkComb = Abc_NtkDup( pNtk );
Abc_NtkMakeComb( pNtkComb, 1 ); Abc_NtkMakeComb( pNtkComb, 1 );
...@@ -1332,15 +1334,28 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, i ...@@ -1332,15 +1334,28 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, i
{ {
printf( "Networks are equivalent after CEC. " ); printf( "Networks are equivalent after CEC. " );
PRT( "Time", clock() - clk ); PRT( "Time", clock() - clk );
if ( pSecPar->fReportSolution )
{
printf( "SOLUTION: PASS " );
PRT( "Time", clock() - clkTotal );
}
return RetValue; return RetValue;
} }
} }
if ( fTryBmc ) if ( pSecPar->fTryBmc )
{ {
RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, 1000, 0, 1, 0 ); RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, 2000, 0, 1, 0 );
if ( RetValue == 0 ) if ( RetValue == 0 )
{
printf( "Networks are not equivalent.\n" );
if ( pSecPar->fReportSolution )
{
printf( "SOLUTION: FAIL " );
PRT( "Time", clock() - clkTotal );
}
return RetValue; return RetValue;
} }
}
// derive the AIG manager // derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 0, 1 ); pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL ) if ( pMan == NULL )
...@@ -1350,7 +1365,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, i ...@@ -1350,7 +1365,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, i
} }
assert( pMan->nRegs > 0 ); assert( pMan->nRegs > 0 );
// perform verification // perform verification
RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit ); RetValue = Fra_FraigSec( pMan, pSecPar );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel ) if ( pNtk->pSeqModel )
{ {
...@@ -1372,7 +1387,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, i ...@@ -1372,7 +1387,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, i
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose ) int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
{ {
// Fraig_Params_t Params; // Fraig_Params_t Params;
Aig_Man_t * pMan; Aig_Man_t * pMan;
...@@ -1392,8 +1407,8 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhase ...@@ -1392,8 +1407,8 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhase
extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error // report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames ); pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, pSecPar->nFramesMax );
Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames ); Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, pSecPar->nFramesMax );
FREE( pMiter->pModel ); FREE( pMiter->pModel );
Abc_NtkDelete( pMiter ); Abc_NtkDelete( pMiter );
return 0; return 0;
...@@ -1444,7 +1459,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhase ...@@ -1444,7 +1459,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhase
assert( pMan->nRegs > 0 ); assert( pMan->nRegs > 0 );
// perform verification // perform verification
RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, 0 ); RetValue = Fra_FraigSec( pMan, pSecPar );
Aig_ManStop( pMan ); Aig_ManStop( pMan );
return RetValue; return RetValue;
} }
......
src/base/io/io.c
...@@ -683,7 +683,7 @@ int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -683,7 +683,7 @@ int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage; goto usage;
} }
} }
if ( argc != globalUtilOptind + 1 ) if ( argc != globalUtilOptind && argc != globalUtilOptind + 1 )
goto usage; goto usage;
if ( pNtk == NULL ) if ( pNtk == NULL )
...@@ -692,7 +692,16 @@ int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -692,7 +692,16 @@ int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1; return 1;
} }
// get the input file name // get the input file name
if ( argc == globalUtilOptind + 1 )
pFileName = argv[globalUtilOptind]; pFileName = argv[globalUtilOptind];
else if ( pNtk->pSpec )
pFileName = Extra_FileNameGenericAppend( pNtk->pSpec, ".init" );
else
{
printf( "File name should be given on the command line.\n" );
return 1;
}
// read the file using the corresponding file reader // read the file using the corresponding file reader
pNtk = Abc_NtkDup( pNtk ); pNtk = Abc_NtkDup( pNtk );
Io_ReadBenchInit( pNtk, pFileName ); Io_ReadBenchInit( pNtk, pFileName );
......
src/misc/extra/extraUtilFile.c
...@@ -160,20 +160,10 @@ char * Extra_FileNameAppend( char * pBase, char * pSuffix ) ...@@ -160,20 +160,10 @@ char * Extra_FileNameAppend( char * pBase, char * pSuffix )
***********************************************************************/ ***********************************************************************/
char * Extra_FileNameGeneric( char * FileName ) char * Extra_FileNameGeneric( char * FileName )
{ {
char * pDot; char * pDot, * pRes;
char * pUnd;
char * pRes;
// find the generic name of the file
pRes = Extra_UtilStrsav( FileName ); pRes = Extra_UtilStrsav( FileName );
// find the pointer to the "." symbol in the file name if ( (pDot = strrchr( pRes, '.' )) )
// pUnd = strstr( FileName, "_" ); *pDot = 0;
pUnd = NULL;
pDot = strstr( FileName, "." );
if ( pUnd )
pRes[pUnd - FileName] = 0;
else if ( pDot )
pRes[pDot - FileName] = 0;
return pRes; return pRes;
} }
...@@ -193,8 +183,7 @@ char * Extra_FileNameGenericAppend( char * pBase, char * pSuffix ) ...@@ -193,8 +183,7 @@ char * Extra_FileNameGenericAppend( char * pBase, char * pSuffix )
static char Buffer[1000]; static char Buffer[1000];
char * pDot; char * pDot;
strcpy( Buffer, pBase ); strcpy( Buffer, pBase );
pDot = strstr( Buffer, "." ); if ( (pDot = strrchr( Buffer, '.' )) )
if ( pDot )
*pDot = 0; *pDot = 0;
strcat( Buffer, pSuffix ); strcat( Buffer, pSuffix );
return Buffer; return Buffer;
......
src/sat/bsat/satSolver.c
...@@ -789,7 +789,7 @@ clause* sat_solver_propagate(sat_solver* s) ...@@ -789,7 +789,7 @@ clause* sat_solver_propagate(sat_solver* s)
return confl; return confl;
} }
static inline int clause_cmp (const void* x, const void* y) { static int clause_cmp (const void* x, const void* y) {
return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; } return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
void sat_solver_reducedb(sat_solver* s) void sat_solver_reducedb(sat_solver* s)
......
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