Skip to content

A
abc
Commit 6074fa3a by Alan Mishchenko
Options

Version abc80316

parent 9b059e30
Showing with 33 additions and 18 deletions
src/aig/fra/fra.h
......@@ -328,7 +328,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 fRetimeFirst, int fVerbose, int fVeryVerbose );
extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose );
/*=== fraSim.c ========================================================*/
extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
......
src/aig/fra/fraSec.c
......@@ -40,7 +40,7 @@
SeeAlso []
***********************************************************************/
int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose )
{
Fra_Ssw_t Pars, * pPars = &Pars;
Fra_Sml_t * pSml;
......@@ -113,6 +113,8 @@ PRT( "Time", clock() - clk );
}
// perform fraiging
if ( fFraiging )
{
clk = clock();
pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 );
Aig_ManStop( pTemp );
......@@ -122,6 +124,7 @@ clk = clock();
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
}
// perform seq sweeping while increasing the number of frames
RetValue = Fra_FraigMiterStatus( pNew );
......
src/base/abci/abc.c
......@@ -13390,23 +13390,25 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
int nArgcNew;
int c;
int fRetimeFirst;
int fFraiging;
int fVerbose;
int fVeryVerbose;
int nFrames;
extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );
extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFrames =16;
fRetimeFirst = 1;
fVerbose = 0;
fVeryVerbose = 0;
nFrames = 16;
fRetimeFirst = 1;
fFraiging = 1;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Krfwvh" ) ) != EOF )
{
switch ( c )
{
......@@ -13424,6 +13426,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fRetimeFirst ^= 1;
break;
case 'f':
fFraiging ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
......@@ -13447,17 +13452,18 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// perform verification
Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
return 0;
usage:
fprintf( pErr, "usage: dsec [-K num] [-rwvh] <file1> <file2>\n" );
fprintf( pErr, "usage: dsec [-K num] [-rfwvh] <file1> <file2>\n" );
fprintf( pErr, "\t performs inductive sequential equivalence checking\n" );
fprintf( pErr, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames );
fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
......@@ -13485,11 +13491,12 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
int fRetimeFirst;
int fFraiging;
int fVerbose;
int fVeryVerbose;
int nFrames;
extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );
extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
......@@ -13498,10 +13505,11 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nFrames = 16;
fRetimeFirst = 1;
fFraiging = 1;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Frfwvh" ) ) != EOF )
{
switch ( c )
{
......@@ -13519,6 +13527,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fRetimeFirst ^= 1;
break;
case 'f':
fFraiging ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
......@@ -13542,14 +13553,15 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// perform verification
Abc_NtkDarProve( pNtk, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
Abc_NtkDarProve( pNtk, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
return 0;
usage:
fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" );
fprintf( pErr, "usage: dprove [-F num] [-rfwvh]\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-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
......
src/base/abci/abcDar.c
......@@ -1186,7 +1186,7 @@ PRT( "Time", clock() - clk );
SeeAlso []
***********************************************************************/
int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pMan;
int RetValue;
......@@ -1199,7 +1199,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbo
}
assert( pMan->nRegs > 0 );
// perform verification
RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
{
......@@ -1221,7 +1221,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbo
SeeAlso []
***********************************************************************/
int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose )
{
// Fraig_Params_t Params;
Aig_Man_t * pMan;
......@@ -1293,7 +1293,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
assert( pMan->nRegs > 0 );
// perform verification
RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
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