Version abc61128

4 files changed, 164 insertions, 37 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9613ab40..4164f67a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -934,8 +934,9 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fUseBdds;
     int fNaive;
+    int fReorder;
     int fVerbose;
-    extern void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose );
+    extern void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fReorder, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -944,9 +945,10 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     fUseBdds = 0;
     fNaive   = 0;
+    fReorder = 1;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "bnvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "bnrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -956,6 +958,9 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'n':
             fNaive ^= 1;
             break;
+        case 'r':
+            fReorder ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -975,19 +980,22 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "This command works only for combinational networks.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsStrash(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
+        Abc_NtkSymmetries( pNtk, fUseBdds, fNaive, fReorder, fVerbose );
+    else
     {
-        fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" );
-        return 1;
+        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        Abc_NtkSymmetries( pNtk, fUseBdds, fNaive, fReorder, fVerbose );
+        Abc_NtkDelete( pNtk );
     }
-    Abc_NtkSymmetries( pNtk, fUseBdds, fNaive, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_symm [-nbvh]\n" );
+    fprintf( pErr, "usage: print_symm [-bnrvh]\n" );
     fprintf( pErr, "\t         computes symmetries of the PO functions\n" );
     fprintf( pErr, "\t-b     : toggle BDD-based or SAT-based computations [default = %s].\n", fUseBdds? "BDD": "SAT" );  
     fprintf( pErr, "\t-n     : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" );  
+    fprintf( pErr, "\t-r     : enable dynamic BDD variable reordering [default = %s].\n", fReorder? "yes": "no" );  
     fprintf( pErr, "\t-v     : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -7082,7 +7090,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     fRecovery   = 1;
     fSwitching  = 0;
     fLatchPaths = 0;
-    fVerbose    = 0;
+    fVerbose    = 1;
     DelayTarget =-1;
     nLutSize    =-1;
     Extra_UtilGetoptReset();
@@ -7383,19 +7391,19 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
-    pPars->Mode        = 1;
-    pPars->nLutSize    = 4;
-//    pPars->pLutLib    = Abc_FrameReadLibLut();
-    pPars->nCutsMax    = 2;
-    pPars->fSeq        = 0;
-    pPars->fLatchPaths = 0;
-    pPars->nLatches    = 0;
-    pPars->pTimesArr   = Abc_NtkGetCiArrivalFloats(pNtk);
-    pPars->pTimesReq   = NULL;
+    pPars->Mode        =  0;
+    pPars->nLutSize    =  5;
+//    pPars->pLutLib    =  Abc_FrameReadLibLut();
+    pPars->nCutsMax    = 10;
+    pPars->fArea       =  0;
+    pPars->fFancy      =  0;
+    pPars->fLatchPaths =  0;
+    pPars->fSeq        =  0;
+    pPars->nLatches    =  0;
     pPars->DelayTarget = -1;
-    pPars->fVerbose    = 0;
+    pPars->fVerbose    =  1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MKCDlsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MKCDaflsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7443,6 +7451,12 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->DelayTarget <= 0.0 ) 
                 goto usage;
             break;
+        case 'a':
+            pPars->fArea ^= 1;
+            break;
+        case 'f':
+            pPars->fFancy ^= 1;
+            break;
         case 'l':
             pPars->fLatchPaths ^= 1;
             break;
@@ -7467,7 +7481,13 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pPars->Mode < 0 || pPars->Mode > 4 )
     {
         fprintf( pErr, "Incorrect mapping mode.\n" );
-        return 1;
+        goto usage;
+    }
+
+    if ( pPars->nCutsMax < 2 || pPars->nCutsMax >= (1<<12) )
+    {
+        fprintf( pErr, "Incorrect number of cuts.\n" );
+        goto usage;
     }
 
     // set the latch paths
@@ -7527,7 +7547,7 @@ usage:
         sprintf( LutSize, "library" );
     else
         sprintf( LutSize, "%d", pPars->nLutSize );
-    fprintf( pErr, "usage: if [-M num] [-K num] [-C num] [-D float] [-lsvh]\n" );
+    fprintf( pErr, "usage: if [-M num] [-K num] [-C num] [-D float] [-aflsvh]\n" );
     fprintf( pErr, "\t           performs FPGA mapping of the network as follows:\n" );
     fprintf( pErr, "\t               1 - delay only\n" );
     fprintf( pErr, "\t               2 - area only\n" );
@@ -7537,6 +7557,8 @@ usage:
     fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < 32) [default = %s]\n", LutSize );
     fprintf( pErr, "\t-C num   : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
     fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );  
+    fprintf( pErr, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
+    fprintf( pErr, "\t-f       : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" );
     fprintf( pErr, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
     fprintf( pErr, "\t-s       : toggles sequential mapping [default = %s]\n", pPars->fSeq? "yes": "no" );
     fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 6b3e0e7c..70971952 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -29,6 +29,7 @@ static If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
 static Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk );
 static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj );
 static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t * pCut );
+static Hop_Obj_t * Abc_NodeIfToHop2( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -56,6 +57,10 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Performing FPGA mapping with choices.\n" );
 
+    // get timing information
+    pPars->pTimesArr = Abc_NtkGetCiArrivalFloats(pNtk);
+    pPars->pTimesReq = NULL;
+
     // perform FPGA mapping
     pIfMan = Abc_NtkToIf( pNtk, pPars );    
     if ( pIfMan == NULL )
@@ -115,7 +120,7 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
         pNode->pCopy = (Abc_Obj_t *)If_ManCreatePi( pIfMan );
 
     // load the AIG into the mapper
-    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
     Abc_AigForEachAnd( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
@@ -212,7 +217,8 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
     If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
         Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf) );
     // derive the function of this node
-    pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pCutBest );
+//    pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pCutBest );
+    pNodeNew->pData = Abc_NodeIfToHop2( pNtkNew->pManFunc, pIfMan, pIfObj );
     If_ObjSetCopy( pIfObj, pNodeNew );
     return pNodeNew;
 }
@@ -280,6 +286,76 @@ Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t *
     return gFunc;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively derives the truth table for the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited )
+{
+    If_Cut_t * pCut;
+    Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
+    // get the best cut
+    pCut = If_ObjCutTriv(pIfObj);
+    // if the cut is visited, return the result
+    if ( If_CutData(pCut) )
+        return If_CutData(pCut);
+    // compute the functions of the children
+    gFunc0 = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj->pFanin0, vVisited );
+    gFunc1 = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj->pFanin1, vVisited );
+    // get the function of the cut
+    gFunc  = Hop_And( pHopMan, Hop_NotCond(gFunc0, pIfObj->fCompl0), Hop_NotCond(gFunc1, pIfObj->fCompl1) );  
+    gFunc  = Hop_NotCond( gFunc, pCut->Phase );
+    assert( If_CutData(pCut) == NULL );
+    If_CutSetData( pCut, gFunc );
+    // add this cut to the visited list
+    Vec_PtrPush( vVisited, pCut );
+    return gFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table for one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NodeIfToHop2( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj )
+{
+    If_Cut_t * pCut;
+    Hop_Obj_t * gFunc;
+    If_Obj_t * pLeaf;
+    int i;
+    // get the best cut
+    pCut = If_ObjCutBest(pIfObj);
+    assert( pCut->nLeaves > 1 );
+    // set the leaf variables
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetData( If_ObjCutTriv(pLeaf), Hop_IthVar(pHopMan, i) );
+    // recursively compute the function while collecting visited cuts
+    Vec_PtrClear( pIfMan->vTemp );
+    gFunc = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); 
+//    printf( "%d ", Vec_PtrSize(p->vTemp) );
+    // clean the cuts
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetData( If_ObjCutTriv(pLeaf), NULL );
+    Vec_PtrForEachEntry( pIfMan->vTemp, pCut, i )
+        If_CutSetData( pCut, NULL );
+    return gFunc;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index bd035eb0..fd5a38e1 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -269,15 +269,16 @@ DdManager * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDrop
     pObj = Abc_AigConst1(pNtk);
     if ( Abc_ObjFanoutNum(pObj) > 0 )
     {
-        Abc_ObjSetGlobalBdd( pObj, dd->one );
-        Cudd_Ref( dd->one );
+        bFunc = dd->one;
+        Abc_ObjSetGlobalBdd( pObj, bFunc );   Cudd_Ref( bFunc );
     }
     // set the elementary variables
     Abc_NtkForEachCi( pNtk, pObj, i )
         if ( Abc_ObjFanoutNum(pObj) > 0 )
         {
-            Abc_ObjSetGlobalBdd( pObj, dd->vars[i] );
-            Cudd_Ref( dd->vars[i] );
+            bFunc = dd->vars[i];
+//            bFunc = dd->vars[Abc_NtkCiNum(pNtk) - 1 - i];
+            Abc_ObjSetGlobalBdd( pObj, bFunc );  Cudd_Ref( bFunc );
         }
 
     // collect the global functions of the COs
@@ -462,6 +463,31 @@ DdManager * Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the shared size of global BDDs of the COs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkSizeOfGlobalBdds( Abc_Ntk_t * pNtk ) 
+{
+    Vec_Ptr_t * vFuncsGlob;
+    Abc_Obj_t * pObj;
+    int RetValue, i;
+    // complement the global functions
+    vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Vec_PtrPush( vFuncsGlob, Abc_ObjGlobalBdd(pObj) );
+    RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
+    Vec_PtrFree( vFuncsGlob );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the BDD of the logic cone of the node.]
 
   Description []
diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c
index d3fcb7c9..0f76065c 100644
--- a/src/base/abci/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
-static void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose );
+static void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fReorder, int fVerbose );
 static void Abc_NtkSymmetriesUsingSandS( Abc_Ntk_t * pNtk, int fVerbose );
 static void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVerbose );
 static void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms );
@@ -44,10 +44,10 @@ static void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose )
+void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fReorder, int fVerbose )
 {
-    if ( fUseBdds )
-        Abc_NtkSymmetriesUsingBdds( pNtk, fNaive, fVerbose );
+    if ( fUseBdds || fNaive )
+        Abc_NtkSymmetriesUsingBdds( pNtk, fNaive, fReorder, fVerbose );
     else
         Abc_NtkSymmetriesUsingSandS( pNtk, fVerbose );
 }
@@ -81,15 +81,19 @@ void Abc_NtkSymmetriesUsingSandS( Abc_Ntk_t * pNtk, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose )
+void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fReorder, int fVerbose )
 {
     DdManager * dd;
     int clk, clkBdd, clkSym;
+    int fGarbCollect = 1;
 
     // compute the global functions
 clk = clock();
-    dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
+    dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, fReorder, fVerbose );
+    printf( "Shared BDD size = %d nodes.\n", Abc_NtkSizeOfGlobalBdds(pNtk) ); 
     Cudd_AutodynDisable( dd );
+    if ( !fGarbCollect )
+        Cudd_DisableGarbageCollection( dd );
     Cudd_zddVarsFromBddVars( dd, 2 );
 clkBdd = clock() - clk;
     // create the collapsed network
@@ -97,11 +101,10 @@ clk = clock();
     Ntk_NetworkSymmsBdd( dd, pNtk, fNaive, fVerbose );
 clkSym = clock() - clk;
     // undo the global functions
-//    Abc_NtkFreeGlobalBdds( pNtk );
-//    Extra_StopManager( dd );
-//    pNtk->pManGlob = NULL;
     Abc_NtkFreeGlobalBdds( pNtk, 1 );
-
+printf( "Statistics of BDD-based symmetry detection:\n" );
+printf( "Algorithm = %s. Reordering = %s. Garbage collection = %s.\n", 
+       fNaive? "naive" : "fast", fReorder? "yes" : "no", fGarbCollect? "yes" : "no" );
 PRT( "Constructing BDDs", clkBdd );
 PRT( "Computing symms  ", clkSym );
 PRT( "TOTAL            ", clkBdd + clkSym );