Version abc70906

5 files changed, 163 insertions, 56 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 571aa02c..22a8ad54 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -115,6 +115,7 @@ static int Abc_CommandIRewrite       ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandDRewrite       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDRefactor      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDCompress2     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDChoice        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDrwsat         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIRewriteSeq    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIResyn         ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -283,6 +284,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "drw",           Abc_CommandDRewrite,         1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "drf",           Abc_CommandDRefactor,        1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "dcompress2",    Abc_CommandDCompress2,       1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "dchoice",       Abc_CommandDChoice,          1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "drwsat",        Abc_CommandDrwsat,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "irws",          Abc_CommandIRewriteSeq,      1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "iresyn",        Abc_CommandIResyn,           1 );
@@ -2977,8 +2979,8 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
-    printf("This command will be available soon\n");
-    return 0;
+//    printf("This command will be available soon\n");
+//    return 0;
 
     // set defaults
     memset( pPars, 0, sizeof(Lpk_Par_t) );
@@ -6177,6 +6179,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
     int nLevels;
+    int fVerbose;
 //    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 );
@@ -6187,15 +6190,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
     extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
     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 );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fVerbose = 0;
     nLevels = 1000;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -6210,6 +6215,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nLevels < 0 ) 
                 goto usage;
             break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -6311,7 +6319,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
 //    pNtkRes = Abc_NtkDar( pNtk );
-    pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
+//    pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
+    pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -6323,6 +6332,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: test [-h]\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-h     : print the command usage\n");
     return 1;
 }
@@ -7138,6 +7148,84 @@ usage:
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int fBalance, fVerbose, fUpdateLevel, c;
+
+    extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fBalance     = 1;
+    fUpdateLevel = 1;
+    fVerbose     = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "blvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'b':
+            fBalance ^= 1;
+            break;
+        case 'l':
+            fUpdateLevel ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
+    pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dchoice [-blvh]\n" );
+    fprintf( pErr, "\t         performs partitioned choicing using a new AIG package\n" );
+    fprintf( pErr, "\t-b     : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
+    fprintf( pErr, "\t-l     : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -11819,24 +11907,24 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFrames      = 0; // if 0, iterates through frames
+    nFrames      =16;
     fRetimeFirst = 1;
     fVerbose     = 0;
     fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'F':
+        case 'K':
             if ( globalUtilOptind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
                 goto usage;
             }
             nFrames = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFrames <= 0 ) 
+            if ( nFrames < 0 ) 
                 goto usage;
             break;
         case 'r':
@@ -11872,9 +11960,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dsec [-F num] [-rwvh] <file1> <file2>\n" );
+    fprintf( pErr, "usage: dsec [-K num] [-rwvh] <file1> <file2>\n" );
     fprintf( pErr, "\t         performs inductive sequential equivalence checking\n" );
-    fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
+    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-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
@@ -11914,24 +12002,24 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFrames      = 0; // if 0, iterates through frames
-    fRetimeFirst = 1;
-    fVerbose     = 0;
-    fVeryVerbose = 0;
+    nFrames      = 16; 
+    fRetimeFirst =  1;
+    fVerbose     =  0;
+    fVeryVerbose =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'F':
+        case 'K':
             if ( globalUtilOptind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
                 goto usage;
             }
             nFrames = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFrames <= 0 ) 
+            if ( nFrames < 0 ) 
                 goto usage;
             break;
         case 'r':
@@ -11964,9 +12052,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" );
+    fprintf( pErr, "usage: dprove [-K num] [-rwvh]\n" );
     fprintf( pErr, "\t         performs SEC on the sequential miter\n" );
-    fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
+    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-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index f8f7d20e..356a5565 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -67,6 +67,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
     }
     // create the manager
     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
+    pMan->pName = Extra_UtilStrsav( pNtk->pName );
     // save the number of registers
     if ( fRegisters )
         pMan->nRegs = Abc_NtkLatchNum(pNtk);
@@ -250,6 +251,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
     Aig_ManForEachPi( pMan, pObj, i )
         pObj->pData = Abc_NtkCi(pNtkNew, i);
+
     // rebuild the AIG
     vNodes = Aig_ManDfsChoices( pMan );
     Vec_PtrForEachEntry( vNodes, pObj, i )
@@ -265,21 +267,8 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
             pAbcRepr->pData = pAbcObj;
         }
     }
-printf( "Total = %d.  Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) );
+//printf( "Total = %d.  Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) );
     Vec_PtrFree( vNodes );
-/*
-    {
-        Abc_Obj_t * pNode;
-        int k, Counter = 0;
-        Abc_NtkForEachNode( pNtkNew, pNode, k )
-            if ( pNode->pData != 0 )
-            {
-                int x = 0;
-                Counter++;
-            }
-        printf( "Choices = %d.\n", Counter );
-    }
-*/
     // connect the PO nodes
     Aig_ManForEachPo( pMan, pObj, i )
         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
@@ -496,11 +485,11 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
         return NULL;
     Fra_ParamsDefault( pPars );
     pPars->nBTLimitNode = nConfLimit;
-    pPars->fVerbose     = fVerbose;
-    pPars->fProve       = fProve;
+    pPars->fChoicing    = fChoicing;
     pPars->fDoSparse    = fDoSparse;
     pPars->fSpeculate   = fSpeculate;
-    pPars->fChoicing    = fChoicing;
+    pPars->fProve       = fProve;
+    pPars->fVerbose     = fVerbose;
     pMan = Fra_FraigPerform( pTemp = pMan, pPars );
     if ( fChoicing )
         pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
@@ -631,7 +620,7 @@ clk = clock();
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
 {
-    Aig_Man_t * pMan;//, * pTemp;
+    Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
@@ -641,8 +630,8 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel,
 //    Aig_ManPrintStats( pMan );
 
 clk = clock();
-    pMan = Dar_ManCompress2( pMan, fBalance, fUpdateLevel, fVerbose ); 
-//    Aig_ManStop( pTemp );
+    pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fVerbose ); 
+    Aig_ManStop( pTemp );
 //PRT( "time", clock() - clk );
 
 //    Aig_ManPrintStats( pMan );
@@ -662,9 +651,35 @@ clk = clock();
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
+{
+    Aig_Man_t * pMan, * pTemp;
+    Abc_Ntk_t * pNtkAig;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fVerbose );
+    Aig_ManStop( pTemp );
+    pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
 {
-    Aig_Man_t * pMan;//, * pTemp;
+    Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
@@ -674,8 +689,8 @@ Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
 //    Aig_ManPrintStats( pMan );
 
 clk = clock();
-    pMan = Dar_ManRwsat( pMan, fBalance, fVerbose ); 
-//    Aig_ManStop( pTemp );
+    pMan = Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose ); 
+    Aig_ManStop( pTemp );
 //PRT( "time", clock() - clk );
 
 //    Aig_ManPrintStats( pMan );
@@ -1118,8 +1133,10 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbos
     Aig_ManSeqCleanup( pMan );
     if ( fLatchSweep )
     {
-        pMan = Aig_ManReduceLaches( pMan, fVerbose );
-        pMan = Aig_ManConstReduce( pMan, fVerbose );
+        if ( pMan->nRegs )
+            pMan = Aig_ManReduceLaches( pMan, fVerbose );
+        if ( pMan->nRegs )
+            pMan = Aig_ManConstReduce( pMan, fVerbose );
     }
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     Aig_ManStop( pMan );
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 64cb2b38..be8a25f1 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -673,7 +673,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtkAdd )
         }
     }
     Vec_PtrPush( vStore, pNtk );
-    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) );
+//    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) );
     return 1;
 }
 
@@ -704,9 +704,15 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
         printf( "There are no network currently in storage.\n" );
         return NULL;
     }
-    printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) );
+//    printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) );
     pNtk = Vec_PtrEntry( vStore, 0 );
 
+    // swap the first and last network
+    // this should lead to the primary choice being "better" because of synthesis
+    pNtk = Vec_PtrPop( vStore );
+    Vec_PtrPush( vStore, Vec_PtrEntry(vStore,0) );
+    Vec_PtrWriteEntry( vStore, 0, pNtk );
+
     // to determine the number of simulation patterns
     // use the following strategy
     // at least 64 words (32 words random and 32 words dynamic)
@@ -731,7 +737,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
     // perform partitioned computation of structural choices
     pFraig = Abc_NtkFraigPartitioned( vStore, &Params );
     Abc_NtkFraigStoreClean();
-PRT( "Total choicing time", clock() - clk );
+//PRT( "Total choicing time", clock() - clk );
     return pFraig;
 }
 
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index a9c42ceb..bb56c22c 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -299,12 +299,8 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
         }
         else 
         {
-            extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
-            // transform truth table into the decomposition tree
-            Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover );
-            // derive the AIG for the decomposition tree
-            pNodeNew->pData = Kit_GraphToHop( pNtkNew->pManFunc, pGraph );
-            Kit_GraphFree( pGraph );
+            extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
+            pNodeNew->pData = Kit_TruthToHop( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover );
         }
         // complement the node if the cut was complemented
         if ( pCutBest->fCompl )
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c
index 6d4e480b..b839f812 100644
--- a/src/base/abci/abcQbf.c
+++ b/src/base/abci/abcQbf.c
@@ -140,7 +140,7 @@ clkV = clock() - clkV;
             printf( "AIG = %6d  ", Abc_NtkNodeNum(pNtkSyn) );
             Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
             printf( "  " );
-            PRTn( "Syn", clkS );
+//            PRTn( "Syn", clkS );
             PRT( "Ver", clkV );
         }
     }