Version abc71208

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;
 }