Version abc70608

4 files changed, 258 insertions, 66 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1e0fed0c..d5321e6d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -330,7 +330,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Kit_TruthCountMintermsPrecomp();
 //    Kit_DsdPrecompute4Vars();
 
-    Dar_LibStart();
+//    Dar_LibStart();
 } 
 
 /**Function*************************************************************
@@ -346,7 +346,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 ***********************************************************************/
 void Abc_End()
 {
-    Dar_LibStop();
+//    Dar_LibStop();
 
     Abc_NtkFraigStoreClean();
 //    Rwt_Man4ExplorePrint();
@@ -5931,7 +5931,7 @@ usage:
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;//, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
     int nLevels;
 //    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
@@ -5940,6 +5940,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern int Pr_ManProofTest( char * pFileName );
     extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk );
     extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk );
+    extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -6049,8 +6050,21 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Abc_Ntk4VarTable( pNtk );
 //    Dat_NtkGenerateArrays( pNtk );
 
-    return 0;
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Network should be strashed. Command has failed.\n" );
+        return 1;
+    }
+    pNtkRes = Abc_NtkDar( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
 
+    return 0;
 usage:
     fprintf( pErr, "usage: test [-h]\n" );
     fprintf( pErr, "\t         testbench for new procedures\n" );
@@ -7286,6 +7300,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fAllNodes;
     int fExdc;
     int c;
+    int fPartition = 0;
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -7307,7 +7322,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pParams->fVerbose   =    0; // the verbosiness flag
     pParams->fVerboseP  =    0; // the verbosiness flag
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscpvaeh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscptvaeh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7360,6 +7375,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             pParams->fVerbose ^= 1;
             break;
+        case 't':
+            fPartition ^= 1;
+            break;
         case 'a':
             fAllNodes ^= 1;
             break;
@@ -7388,13 +7406,28 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pParams->fVerboseP = pParams->fTryProve;
 
     // get the new network
-    if ( Abc_NtkIsStrash(pNtk) )
-        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
+    if ( fPartition )
+    {
+        pNtkRes = Abc_NtkDup( pNtk );
+        if ( Abc_NtkIsStrash(pNtk) )
+            Abc_NtkFraigPartitionedTime( pNtk, &Params );
+        else
+        {
+            pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
+            Abc_NtkFraigPartitionedTime( pNtk, &Params );
+            Abc_NtkDelete( pNtk );
+        }
+    }
     else
     {
-        pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
-        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
-        Abc_NtkDelete( pNtk );
+        if ( Abc_NtkIsStrash(pNtk) )
+            pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
+        else
+        {
+            pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
+            pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
+            Abc_NtkDelete( pNtk );
+        }
     }
     if ( pNtkRes == NULL )
     {
@@ -7411,7 +7444,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     sprintf( Buffer, "%d", pParams->nBTLimit );
-    fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvah]\n" );
+    fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvtah]\n" );
     fprintf( pErr, "\t         transforms a logic network into a functionally reduced AIG\n" );
     fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n",     pParams->nPatsRand );
     fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsDyna );
@@ -7423,6 +7456,7 @@ usage:
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n",                       pParams->fVerbose?  "yes": "no" );
     fprintf( pErr, "\t-e     : toggle functional sweeping using EXDC [default = %s]\n",       fExdc? "yes": "no" );
     fprintf( pErr, "\t-a     : toggle between all nodes and DFS nodes [default = %s]\n",      fAllNodes? "all": "dfs" );
+    fprintf( pErr, "\t-t     : toggle using partitioned representation [default = %s]\n",     fPartition? "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 0863061b..81278515 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -25,62 +25,12 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk );
-static Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Gives the current ABC network to AIG manager for processing.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
-{
-    Abc_Ntk_t * pNtkAig;
-    Dar_Man_t * pMan;//, * pTemp;
-    assert( Abc_NtkIsStrash(pNtk) );
-    // convert to the AIG manager
-    pMan = Abc_NtkToDar( pNtk );
-    if ( pMan == NULL )
-        return NULL;
-    if ( !Dar_ManCheck( pMan ) )
-    {
-        printf( "Abc_NtkDar: AIG check has failed.\n" );
-        Dar_ManStop( pMan );
-        return NULL;
-    }
-    // perform balance
-    Dar_ManPrintStats( pMan );
-//    Dar_ManDumpBlif( pMan, "aig_temp.blif" );
-    pMan->pPars = Dar_ManDefaultParams();
-    Dar_ManRewrite( pMan );
-    Dar_ManPrintStats( pMan );
-    // convert from the AIG manager
-    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
-    if ( pNtkAig == NULL )
-        return NULL;
-    Dar_ManStop( pMan );
-    // make sure everything is okay
-    if ( !Abc_NtkCheck( pNtkAig ) )
-    {
-        printf( "Abc_NtkDar: The network check has failed.\n" );
-        Abc_NtkDelete( pNtkAig );
-        return NULL;
-    }
-    return pNtkAig;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Converts the network from the AIG manager into ABC.]
 
   Description []
@@ -96,7 +46,7 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj;
     int i;
     // create the manager
-    pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) );
+    pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
     // transfer the pointers to the basic nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Dar_ManConst1(pMan);
     Abc_NtkForEachCi( pNtk, pObj, i )
@@ -122,14 +72,14 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan )
+Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan )
 {
     Vec_Ptr_t * vNodes;
     Abc_Ntk_t * pNtkNew;
     Dar_Obj_t * pObj;
     int i;
     // perform strashing
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // transfer the pointers to the basic nodes
     Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
     Dar_ManForEachPi( pMan, pObj, i )
@@ -147,6 +97,159 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan )
     return pNtkNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
+    Dar_Obj_t * pObj;
+    int i;
+//    assert( Dar_ManLatchNum(pMan) > 0 );
+    // perform strashing
+    pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // transfer the pointers to the basic nodes
+    Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+    Dar_ManForEachPi( pMan, pObj, i )
+        pObj->pData = Abc_NtkPi(pNtkNew, i);
+    // create latches of the new network
+    Dar_ManForEachObj( pMan, pObj, i )
+    {
+        if ( !Dar_ObjIsLatch(pObj) )
+            continue;
+        pObjNew = Abc_NtkCreateLatch( pNtkNew );
+        pFaninNew0 = Abc_NtkCreateBi( pNtkNew );
+        pFaninNew1 = Abc_NtkCreateBo( pNtkNew );
+        Abc_ObjAddFanin( pObjNew, pFaninNew0 );
+        Abc_ObjAddFanin( pFaninNew1, pObjNew );
+        Abc_LatchSetInit0( pObjNew );
+        pObj->pData = Abc_ObjFanout0( pObjNew );
+    }
+    Abc_NtkAddDummyBoxNames( pNtkNew );
+    // rebuild the AIG
+    vNodes = Dar_ManDfs( pMan );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // add the first fanin
+        pObj->pData = pFaninNew0 = (Abc_Obj_t *)Dar_ObjChild0Copy(pObj);
+        if ( Dar_ObjIsBuf(pObj) )
+            continue;
+        // add the second fanin
+        pFaninNew1 = (Abc_Obj_t *)Dar_ObjChild1Copy(pObj);
+        // create the new node
+        if ( Dar_ObjIsExor(pObj) )
+            pObj->pData = pObjNew = Abc_AigXor( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+        else
+            pObj->pData = pObjNew = Abc_AigAnd( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+    }
+    Vec_PtrFree( vNodes );
+    // connect the PO nodes
+    Dar_ManForEachPo( pMan, pObj, i )
+    {
+        pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj );
+        Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew );
+    }
+    // connect the latches
+    Dar_ManForEachObj( pMan, pObj, i )
+    {
+        if ( !Dar_ObjIsLatch(pObj) )
+            continue;
+        pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj );
+        Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew );
+    }
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect latch values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch;
+    int i, * pArray;
+    pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pArray[i] = Abc_LatchIsInit1(pLatch);
+    return pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkAig;
+    Dar_Man_t * pMan;//, * pTemp;
+    int * pArray;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    // convert to the AIG manager
+    pMan = Abc_NtkToDar( pNtk );
+    if ( pMan == NULL )
+        return NULL;
+    if ( !Dar_ManCheck( pMan ) )
+    {
+        printf( "Abc_NtkDar: AIG check has failed.\n" );
+        Dar_ManStop( pMan );
+        return NULL;
+    }
+    // perform balance
+    Dar_ManPrintStats( pMan );
+
+    pArray = Abc_NtkGetLatchValues(pNtk);
+    Dar_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray );
+    free( pArray );
+
+//    Dar_ManDumpBlif( pMan, "aig_temp.blif" );
+//    pMan->pPars = Dar_ManDefaultParams();
+//    Dar_ManRewrite( pMan );
+    Dar_ManPrintStats( pMan );
+    // convert from the AIG manager
+    if ( Dar_ManLatchNum(pMan) )
+        pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan );
+    else
+        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    if ( pNtkAig == NULL )
+        return NULL;
+    Dar_ManStop( pMan );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_NtkDar: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+    }
+    return pNtkAig;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 30e49af2..fa6771b3 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -687,7 +687,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
         // set the number of networks stored
         Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 );
     }
-//    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
+    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
     return 1;
 }
 
@@ -734,7 +734,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
     Fraig_ParamsSetDefault( &Params );
     Params.nPatsRand  = nWordsMin * 32; // the number of words of random simulation info
     Params.nPatsDyna  = nWordsMin * 32; // the number of words of dynamic simulation info
-    Params.nBTLimit   = 99;             // the max number of backtracks to perform
+    Params.nBTLimit   = 999999;             // the max number of backtracks to perform
     Params.fFuncRed   =  1;             // performs only one level hashing
     Params.fFeedBack  =  1;             // enables solver feedback
     Params.fDist1Pats =  1;             // enables distance-1 patterns
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 748868de..787e3f88 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -698,12 +698,67 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
     // derive the final network
     pNtkFraig = Abc_NtkPartStitchChoices( pNtk, vFraigs );
     Vec_PtrForEachEntry( vFraigs, pNtkAig, i )
+    {
+//        Abc_NtkPrintStats( stdout, pNtkAig, 0 );
         Abc_NtkDelete( pNtkAig );
+    }
     Vec_PtrFree( vFraigs );
 
     return pNtkFraig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Stitches together several networks with choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams )
+{
+    extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+    extern void * Abc_FrameGetGlobalFrame();
+
+    Vec_Vec_t * vParts;
+    Vec_Ptr_t * vFraigs, * vOne;
+    Abc_Ntk_t * pNtkAig, * pNtkFraig;
+    int i;
+    int clk = clock();
+
+    // perform partitioning
+    assert( Abc_NtkIsStrash(pNtk) );
+//    vParts = Abc_NtkPartitionNaive( pNtk, 20 );
+    vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
+
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
+
+    // fraig each partition
+    vFraigs = Vec_PtrAlloc( Vec_VecSize(vParts) );
+    Vec_VecForEachLevel( vParts, vOne, i )
+    {
+        pNtkAig = Abc_NtkCreateConeArray( pNtk, vOne, 0 );
+        pNtkFraig = Abc_NtkFraig( pNtkAig, pParams, 0, 0 );
+        Vec_PtrPush( vFraigs, pNtkFraig );
+        Abc_NtkDelete( pNtkAig );
+
+        printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) );
+    }
+    Vec_VecFree( vParts );
+
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
+
+    // derive the final network
+    Vec_PtrForEachEntry( vFraigs, pNtkAig, i )
+        Abc_NtkDelete( pNtkAig );
+    Vec_PtrFree( vFraigs );
+
+    PRT( "Partitioned fraiging time", clock() - clk );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////