diff options
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 34 | ||||
| -rw-r--r-- | src/base/abci/abcDar.c | 16 |
2 files changed, 42 insertions, 8 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; } |