summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abc.c34
-rw-r--r--src/base/abci/abcDar.c16
-rw-r--r--src/base/io/ioReadAiger.c4
3 files changed, 44 insertions, 10 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 20aa7247..3b238779 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6193,8 +6193,11 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;//, * pNtkRes;
int c;
+ int fBmc;
+ int nFrames;
int nLevels;
int fVerbose;
+ int fVeryVerbose;
// extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
// extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
@@ -6207,20 +6210,34 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
- extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
+ extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int fVerbose, int fVeryVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
+ fVeryVerbose = 0;
fVerbose = 1;
- nLevels = 1000;
+ fBmc = 1;
+ nFrames = 1;
+ nLevels = 200;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FNbvwh" ) ) != EOF )
{
switch ( c )
{
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFrames < 0 )
+ goto usage;
+ break;
case 'N':
if ( globalUtilOptind >= argc )
{
@@ -6232,9 +6249,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nLevels < 0 )
goto usage;
break;
+ case 'b':
+ fBmc ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
+ case 'w':
+ fVeryVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -6355,12 +6378,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/
// Abc_NtkDarHaigRecord( pNtk );
- Abc_NtkDarClau( pNtk, 1000, fVerbose );
+ Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
return 0;
usage:
- fprintf( pErr, "usage: test [-h]\n" );
+ fprintf( pErr, "usage: test [-vwh]\n" );
fprintf( pErr, "\t testbench for new procedures\n" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-w : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 67f22eb7..e23b04dd 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -56,12 +56,20 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachCi( pNtk, pObj, i )
if ( i < Abc_NtkPiNum(pNtk) )
+ {
assert( Abc_ObjIsPi(pObj) );
+ if ( !Abc_ObjIsPi(pObj) )
+ printf( "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
+ }
else
assert( Abc_ObjIsBo(pObj) );
Abc_NtkForEachCo( pNtk, pObj, i )
if ( i < Abc_NtkPoNum(pNtk) )
+ {
assert( Abc_ObjIsPo(pObj) );
+ if ( !Abc_ObjIsPo(pObj) )
+ printf( "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
+ }
else
assert( Abc_ObjIsBi(pObj) );
// print warning about initial values
@@ -1401,9 +1409,10 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
SeeAlso []
***********************************************************************/
-int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
+int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int fVerbose, int fVeryVerbose )
{
- extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose );
+ extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose );
+ extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nClauses, int fBmc, int fVerbose, int fVeryVerbose );
Aig_Man_t * pMan;
if ( Abc_NtkPoNum(pNtk) != 1 )
{
@@ -1418,7 +1427,8 @@ int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
- Fra_Clau( pMan, nStepsMax, fVerbose );
+// Fra_Clau( pMan, nStepsMax, fVerbose, fVeryVerbose );
+ Fra_Claus( pMan, nFrames, nStepsMax, fBmc, fVerbose, fVeryVerbose );
Aig_ManStop( pMan );
return 1;
}
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index d3c4c878..273b2d5a 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -237,8 +237,8 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
Counter++;
}
- if ( Counter )
- printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
+// if ( Counter )
+// printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
}
else
{