summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-03-16 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2008-03-16 08:01:00 -0700
commit6074fa3a1e76d846b1abd6674891ff7ed5b78175 (patch)
treebe4be52f53152eddcc4b718b9c9c3446dd142f81
parent9b059e3085eaa55817684926b3c508ba7fe0075f (diff)
downloadabc-6074fa3a1e76d846b1abd6674891ff7ed5b78175.tar.gz
abc-6074fa3a1e76d846b1abd6674891ff7ed5b78175.tar.bz2
abc-6074fa3a1e76d846b1abd6674891ff7ed5b78175.zip
Version abc80316
-rw-r--r--src/aig/fra/fra.h2
-rw-r--r--src/aig/fra/fraSec.c5
-rw-r--r--src/base/abci/abc.c36
-rw-r--r--src/base/abci/abcDar.c8
4 files changed, 33 insertions, 18 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index e7583b4b..ee4e9115 100644
--- a/src/aig/fra/fra.h
+++ b/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 );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 75d297cf..bbad2a6e 100644
--- a/src/aig/fra/fraSec.c
+++ b/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 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 204525d9..91133b2a 100644
--- a/src/base/abci/abc.c
+++ b/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");
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 367ba727..78f43aac 100644
--- a/src/base/abci/abcDar.c
+++ b/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;
}