Merging two branches.

src/aig/gia/gia.h

@@ -483,6 +483,7 @@ static inline int          Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj
 static inline void         Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit )  { Vec_IntWriteEntry(&p->vCopies, Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj), iLit);  }
 static inline int          Gia_ObjCopyArray( Gia_Man_t * p, int iObj )                          { return Vec_IntEntry(&p->vCopies, iObj);                                          }
 static inline void         Gia_ObjSetCopyArray( Gia_Man_t * p, int iObj, int iLit )             { Vec_IntWriteEntry(&p->vCopies, iObj, iLit);                                      }
+static inline void         Gia_ManCleanCopyArray( Gia_Man_t * p )                               { Vec_IntFill( &p->vCopies, Gia_ManObjNum(p), -1 );                                }
 
 static inline int          Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj));   }
 static inline int          Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj));   }
@@ -1088,6 +1089,7 @@ extern Gia_Man_t *         Gia_ManDupOrderDfsChoices( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop );
 extern Gia_Man_t *         Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres );
+extern Gia_Man_t *         Gia_ManDupSelectedOutputs( Gia_Man_t * p, Vec_Int_t * vOutsLeft );
 extern Gia_Man_t *         Gia_ManDupOrderAiger( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis );
 extern Gia_Man_t *         Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
@@ -1345,6 +1347,7 @@ extern float               Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames,
 extern Vec_Int_t *         Gia_ManComputeSwitchProbs( Gia_Man_t * pGia, int nFrames, int nPref, int fProbOne );
 extern Vec_Flt_t *         Gia_ManPrintOutputProb( Gia_Man_t * p );
 /*=== giaTim.c ===========================================================*/
+extern int                 Gia_ManBoxNum( Gia_Man_t * p );
 extern int                 Gia_ManIsSeqWithBoxes( Gia_Man_t * p );
 extern int                 Gia_ManIsNormalized( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupNormalize( Gia_Man_t * p );
@@ -1353,7 +1356,9 @@ extern Gia_Man_t *         Gia_ManDupUnshuffleInputs( Gia_Man_t * p );
 extern int                 Gia_ManLevelWithBoxes( Gia_Man_t * p );
 extern int                 Gia_ManLutLevelWithBoxes( Gia_Man_t * p );
 extern void *              Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres );
+extern void *              Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBoxesLeft );
 extern Gia_Man_t *         Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres );
+extern Gia_Man_t *         Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxesLeft );
 extern Gia_Man_t *         Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres );
 extern int                 Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit, char * pFileSpec );
 /*=== giaTruth.c ===========================================================*/

src/aig/gia/giaDup.c

@@ -254,6 +254,38 @@ Gia_Man_t * Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates AIG while putting objects in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupSelectedOutputs( Gia_Man_t * p, Vec_Int_t * vOutsLeft )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i, iOut;
+    assert( Gia_ManRegNum(p) == 0 );
+    assert( Gia_ManPoNum(p) >= Vec_IntSize(vOutsLeft) );
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Vec_IntForEachEntry( vOutsLeft, iOut, i )
+        Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(Gia_ManPo(p, iOut)) );
+    Vec_IntForEachEntry( vOutsLeft, iOut, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, iOut)) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the AIG in the DFS order.]
 
   Description []

src/aig/gia/giaFadds.c

@@ -538,7 +538,7 @@ Tim_Man_t * Gia_ManGenerateTim( int nPis, int nPos, int nBoxes, int nIns, int nO
     curPo = 0;
     for ( i = 0; i < nBoxes; i++ )
     {
-        Tim_ManCreateBox( pMan, curPo, nIns, curPi, nOuts, -1 );
+        Tim_ManCreateBox( pMan, curPo, nIns, curPi, nOuts, 0 );
         curPi += nOuts;
         curPo += nIns;
     }

src/aig/gia/giaMan.c

@@ -105,6 +105,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFreeP( &p->vBarBufs );
     Vec_IntFreeP( &p->vLevels );
     Vec_IntFreeP( &p->vTruths );
+    Vec_IntErase( &p->vCopies );
     Vec_IntFreeP( &p->vTtNums );
     Vec_IntFreeP( &p->vTtNodes );
     Vec_WrdFreeP( &p->vTtMemory );

src/aig/gia/giaTim.c

@@ -35,6 +35,22 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of boxes in the AIG with boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManBoxNum( Gia_Man_t * p )
+{
+    return p->pManTime ? Tim_ManBoxNum((Tim_Man_t *)p->pManTime) : 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns one if this is a seq AIG with non-trivial boxes.]
 
   Description []
@@ -598,9 +614,16 @@ void * Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres )
 {
     Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
     assert( pManTime != NULL );
-    assert( Tim_ManBoxNum(pManTime) == Vec_IntSize(vBoxPres) );
+    assert( Vec_IntSize(vBoxPres) == Tim_ManBoxNum(pManTime) );
     return Tim_ManTrim( pManTime, vBoxPres );
 }
+void * Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBoxesLeft )
+{
+    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
+    assert( pManTime != NULL );
+    assert( Vec_IntSize(vBoxesLeft) <= Tim_ManBoxNum(pManTime) );
+    return Tim_ManReduce( pManTime, vBoxesLeft );
+}
 
 /**Function*************************************************************
 
@@ -615,7 +638,7 @@ void * Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres )
 ***********************************************************************/
 Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * p, Vec_Int_t * vBoxPres )
 {
-    Gia_Man_t * pNew = NULL;
+    Gia_Man_t * pNew;
     Tim_Man_t * pManTime = (Tim_Man_t *)pTime;
     Vec_Int_t * vOutPres = Vec_IntAlloc( 100 );
     int i, k, curPo = 0;
@@ -628,11 +651,29 @@ Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * p, Vec_Int_t * vBox
         curPo += Tim_ManBoxOutputNum(pManTime, i);
     }
     assert( curPo == Gia_ManCoNum(p) );
-//    if ( Vec_IntSize(vOutPres) > 0 )
     pNew = Gia_ManDupOutputVec( p, vOutPres );
     Vec_IntFree( vOutPres );
     return pNew;
 }
+Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * p, Vec_Int_t * vBoxesLeft )
+{
+    Gia_Man_t * pNew;
+    Tim_Man_t * pManTime = (Tim_Man_t *)pTime;
+    int nRealPis = Tim_ManPiNum(pManTime);
+    Vec_Int_t * vOutsLeft = Vec_IntAlloc( 100 );
+    int i, k, iBox, iOutFirst;
+    assert( Vec_IntSize(vBoxesLeft) <= Tim_ManBoxNum(pManTime) );
+    assert( Gia_ManCoNum(p) == Tim_ManCiNum(pManTime) - nRealPis );
+    Vec_IntForEachEntry( vBoxesLeft, iBox, i )
+    {
+        iOutFirst = Tim_ManBoxOutputFirst(pManTime, iBox) - nRealPis;
+        for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, iBox); k++ )
+            Vec_IntPush( vOutsLeft, iOutFirst + k );
+    }
+    pNew = Gia_ManDupSelectedOutputs( p, vOutsLeft );
+    Vec_IntFree( vOutsLeft );
+    return pNew;
+}
 
 /**Function*************************************************************
 

src/base/abc/abcDfs.c

@@ -1460,8 +1460,6 @@ int Abc_NtkIsAcyclicWithBoxes_rec( Abc_Obj_t * pNode )
     Abc_Obj_t * pFanin;
     int fAcyclic, i;
     assert( !Abc_ObjIsNet(pNode) );
-    if ( Abc_ObjIsBo(pNode) )
-        pNode = Abc_ObjFanin0(pNode);
     if ( Abc_ObjIsPi(pNode) || Abc_ObjIsLatch(pNode) || Abc_ObjIsBlackbox(pNode) )
         return 1;
     assert( Abc_ObjIsNode(pNode) || Abc_ObjIsBox(pNode) );
@@ -1485,8 +1483,6 @@ int Abc_NtkIsAcyclicWithBoxes_rec( Abc_Obj_t * pNode )
         if ( Abc_ObjIsBox(pNode) )
             pFanin = Abc_ObjFanin0(pFanin);
         pFanin = Abc_ObjFanin0Ntk(pFanin);
-        // make sure there is no mixing of networks
-        assert( pFanin->pNtk == pNode->pNtk );
         if ( Abc_ObjIsBo(pFanin) )
             pFanin = Abc_ObjFanin0(pFanin);
         // check if the fanin is visited
@@ -1523,6 +1519,8 @@ int Abc_NtkIsAcyclicWithBoxes( Abc_Ntk_t * pNtk )
     Abc_NtkForEachPo( pNtk, pNode, i )
     {
         pNode = Abc_ObjFanin0Ntk(Abc_ObjFanin0(pNode));
+        if ( Abc_ObjIsBo(pNode) )
+            pNode = Abc_ObjFanin0(pNode);
         if ( Abc_NodeIsTravIdPrevious(pNode) )
             continue;
         // traverse the output logic cone
@@ -1537,6 +1535,8 @@ int Abc_NtkIsAcyclicWithBoxes( Abc_Ntk_t * pNtk )
         Abc_NtkForEachLatchInput( pNtk, pNode, i )
         {
             pNode = Abc_ObjFanin0Ntk(Abc_ObjFanin0(pNode));
+            if ( Abc_ObjIsBo(pNode) )
+                pNode = Abc_ObjFanin0(pNode);
             if ( Abc_NodeIsTravIdPrevious(pNode) )
                 continue;
             // traverse the output logic cone

src/base/abci/abc.c

@@ -440,6 +440,7 @@ static int Abc_CommandAbc9Bmci               ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9PoXsim             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Demiter            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Fadds              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Mfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexMerge           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1042,6 +1043,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&poxsim",       Abc_CommandAbc9PoXsim,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&demiter",      Abc_CommandAbc9Demiter,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&fadds",        Abc_CommandAbc9Fadds,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&mfs",          Abc_CommandAbc9Mfs,          0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
@@ -36635,6 +36637,162 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars );
+    Gia_Man_t * pTemp; int c;
+    Sfm_Par_t Pars, * pPars = &Pars;
+    Sfm_ParSetDefault( pPars );
+    pPars->nTfoLevMax  =    5;
+    pPars->nDepthMax   =  100;
+    pPars->nWinSizeMax = 2000; 
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCNdaevwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTfoLevMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTfoLevMax < 0 )
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFanoutMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFanoutMax < 0 )
+                goto usage;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nDepthMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nDepthMax < 0 )
+                goto usage;
+            break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nWinSizeMax < 0 )
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nGrowthLevel = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY )
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 )
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nNodesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nNodesMax < 0 )
+                goto usage;
+            break;
+        case 'd':
+            pPars->fRrOnly ^= 1;
+            break;
+        case 'a':
+            pPars->fArea ^= 1;
+            break;
+        case 'e':
+            pPars->fMoreEffort ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Mfs(): There is no AIG.\n" );
+        return 0;
+    }
+    if ( !Gia_ManHasMapping(pAbc->pGia) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has no mapping.\n" );
+        return 0;
+    }
+    pTemp = Gia_ManPerformMfs( pAbc->pGia, pPars );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &mfs [-WFDMLCN <num>] [-daevwh]\n" );
+    Abc_Print( -2, "\t           performs don't-care-based optimization of logic networks\n" );
+    Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n",             pPars->nTfoLevMax );
+    Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n",                pPars->nFanoutMax );
+    Abc_Print( -2, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n",                   pPars->nDepthMax );
+    Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n",    pPars->nWinSizeMax );
+    Abc_Print( -2, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
+    Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n",   pPars->nBTLimit );
+    Abc_Print( -2, "\t-N <num> : the max number of nodes to try (0 = all) [default = %d]\n",                    pPars->nNodesMax );
+    Abc_Print( -2, "\t-d       : toggle performing redundancy removal [default = %s]\n",                        pPars->fRrOnly? "yes": "no" );
+    Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n",                        pPars->fArea? "area": "area+edges" );
+    Abc_Print( -2, "\t-e       : toggle high-effort resubstitution [default = %s]\n",                           pPars->fMoreEffort? "yes": "no" );
+    Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n",                        pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w       : toggle printing detailed stats for each node [default = %s]\n",                pPars->fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     return -1;

src/base/abci/abcMfs.c

@@ -270,7 +270,6 @@ int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
     p = Abc_NtkExtractMfs( pNtk, pPars->nFirstFixed );
     // perform optimization
     nNodes = Sfm_NtkPerform( p, pPars );
-    // call the fast extract procedure
     if ( nNodes == 0 )
     {
 //        Abc_Print( 1, "The network is not changed by \"mfs\".\n" );
@@ -451,7 +450,6 @@ int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, int nFramesAdd, Vec_Int_t
     pp = Abc_NtkExtractMfs2( pNtk, iPivot );
     // perform optimization
     nNodes = Sfm_NtkPerform( pp, pPars );
-    // call the fast extract procedure
     if ( nNodes == 0 )
     {
 //        Abc_Print( 1, "The network is not changed by \"mfs\".\n" );

src/base/wlc/wlcAbs.c

@@ -152,6 +152,8 @@ Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
     Wlc_NtkCleanCopy( p );
     Wlc_NtkForEachObj( p, pObj, i )
     {
+        if ( i == Vec_IntSize(&p->vCopies) )
+            break;
         if ( pObj->Mark ) {
             // clean
             pObj->Mark = 0;

src/base/wlc/wlcCom.c

@@ -356,8 +356,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     // transform
-//    pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
     pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
+    pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
     Wlc_AbcUpdateNtk( pAbc, pNtk );
     return 0;
 usage:

src/misc/tim/tim.h

@@ -130,6 +130,7 @@ extern Tim_Man_t *     Tim_ManLoad( Vec_Str_t * p, int fHieOnly );
 extern Tim_Man_t *     Tim_ManStart( int nCis, int nCos );
 extern Tim_Man_t *     Tim_ManDup( Tim_Man_t * p, int fUnitDelay );
 extern Tim_Man_t *     Tim_ManTrim( Tim_Man_t * p, Vec_Int_t * vBoxPres );
+extern Tim_Man_t *     Tim_ManReduce( Tim_Man_t * p, Vec_Int_t * vBoxesLeft );
 extern Vec_Int_t *     Tim_ManAlignTwo( Tim_Man_t * pSpec, Tim_Man_t * pImpl );
 extern void            Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t * vOutReqs );
 extern float *         Tim_ManGetArrTimes( Tim_Man_t * p );

src/misc/tim/timMan.c

@@ -239,6 +239,91 @@ Tim_Man_t * Tim_ManTrim( Tim_Man_t * p, Vec_Int_t * vBoxPres )
 
 /**Function*************************************************************
 
+  Synopsis    [Reduces the timing manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Tim_Man_t * Tim_ManReduce( Tim_Man_t * p, Vec_Int_t * vBoxesLeft )
+{
+    Tim_Man_t * pNew;
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
+    float * pDelayTable, * pDelayTableNew;
+    int i, k, iBox, nNewCis, nNewCos, nInputs, nOutputs;
+    assert( Vec_IntSize(vBoxesLeft) <= Tim_ManBoxNum(p) );
+    // count the number of CIs and COs in the trimmed manager
+    nNewCis = Tim_ManPiNum(p);
+    nNewCos = Tim_ManPoNum(p);
+    Vec_IntForEachEntry( vBoxesLeft, iBox, i )
+    {
+        pBox = Tim_ManBox( p, iBox );
+        nNewCis += pBox->nOutputs;
+        nNewCos += pBox->nInputs;
+    }
+    assert( nNewCis <= Tim_ManCiNum(p) );
+    assert( nNewCos <= Tim_ManCoNum(p) );
+    // clear traversal IDs
+    Tim_ManForEachCi( p, pObj, i ) 
+        pObj->TravId = 0;          
+    Tim_ManForEachCo( p, pObj, i ) 
+        pObj->TravId = 0;          
+    // create new manager
+    pNew = Tim_ManStart( nNewCis, nNewCos );
+    // copy box connectivity information
+    memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * Tim_ManPiNum(p) );
+    memcpy( pNew->pCos + nNewCos - Tim_ManPoNum(p), 
+            p->pCos + Tim_ManCoNum(p) - Tim_ManPoNum(p), 
+            sizeof(Tim_Obj_t) * Tim_ManPoNum(p) );
+    // duplicate delay tables
+    if ( Tim_ManDelayTableNum(p) > 0 )
+    {
+        pNew->vDelayTables = Vec_PtrStart( Vec_PtrSize(p->vDelayTables) );
+        Tim_ManForEachTable( p, pDelayTable, i )
+        {
+            if ( pDelayTable == NULL )
+                continue;
+            assert( i == (int)pDelayTable[0] );
+            nInputs   = (int)pDelayTable[1];
+            nOutputs  = (int)pDelayTable[2];
+            pDelayTableNew = ABC_ALLOC( float, 3 + nInputs * nOutputs );
+            pDelayTableNew[0] = (int)pDelayTable[0];
+            pDelayTableNew[1] = (int)pDelayTable[1];
+            pDelayTableNew[2] = (int)pDelayTable[2];
+            for ( k = 0; k < nInputs * nOutputs; k++ )
+                pDelayTableNew[3+k] = pDelayTable[3+k];
+//            assert( (int)pDelayTableNew[0] == Vec_PtrSize(pNew->vDelayTables) );
+            assert( Vec_PtrEntry(pNew->vDelayTables, i) == NULL );
+            Vec_PtrWriteEntry( pNew->vDelayTables, i, pDelayTableNew );
+        }
+    }
+    // duplicate boxes
+    if ( Tim_ManBoxNum(p) > 0 )
+    {
+        int curPi = Tim_ManPiNum(p);
+        int curPo = 0;
+        pNew->vBoxes = Vec_PtrAlloc( Tim_ManBoxNum(p) );
+        Vec_IntForEachEntry( vBoxesLeft, iBox, i )
+        {
+            pBox = Tim_ManBox( p, iBox );
+            Tim_ManCreateBox( pNew, curPo, pBox->nInputs, curPi, pBox->nOutputs, pBox->iDelayTable );
+            Tim_ManBoxSetCopy( pNew, Tim_ManBoxNum(pNew) - 1, iBox );
+            curPi += pBox->nOutputs;
+            curPo += pBox->nInputs;
+        }
+        curPo += Tim_ManPoNum(p);
+        assert( curPi == Tim_ManCiNum(pNew) );
+        assert( curPo == Tim_ManCoNum(pNew) );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Aligns two sets of boxes using the copy field.]
 
   Description []

src/opt/sfm/sfm.h

@@ -77,7 +77,7 @@ extern word *       Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
 extern int          Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i );
 extern int          Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i );
 /*=== sfmWin.c ==========================================================*/
-extern Vec_Int_t *  Sfm_NtkDfs( Sfm_Ntk_t * p );
+extern Vec_Int_t *  Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft );
 
 
 ABC_NAMESPACE_HEADER_END

src/opt/sfm/sfmCore.c

@@ -258,8 +258,13 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
 {
     int i, k, Counter = 0;
     p->timeTotal = Abc_Clock();
-    if ( pPars->fVerbose && Vec_StrSum(p->vFixed) > 0 )
-        printf( "Performing MFS with %d fixed objects.\n", Vec_StrSum(p->vFixed) );
+    if ( pPars->fVerbose )
+    {
+        int nFixed = p->vFixed ? Vec_StrSum(p->vFixed) : 0;
+        int nEmpty = p->vEmpty ? Vec_StrSum(p->vEmpty) : 0;
+        printf( "Performing MFS with %d PIs, %d POs, %d nodes (%d flexible, %d fixed, %d empty).\n", 
+            p->nPis, p->nPos, p->nNodes, p->nNodes-nFixed, nFixed, nEmpty );
+    }
     p->pPars = pPars;
     Sfm_NtkPrepare( p );
 //    Sfm_ComputeInterpolantCheck( p );

src/opt/sfm/sfmNtk.c

@@ -54,7 +54,8 @@ void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t *
             assert( Vec_IntSize(vArray) == 0 && Vec_StrEntry(vFixed, i) == (char)0 );
         // nodes are in a topo order; POs cannot be fanins
         Vec_IntForEachEntry( vArray, Fanin, k )
-            assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
+//            assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
+            assert( Fanin + nPos < Vec_WecSize(vFanins) );
         // POs have one fanout
         if ( i + nPos >= Vec_WecSize(vFanins) )
             assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 );

src/opt/sfm/sfmSat.c

@@ -91,7 +91,8 @@ int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
             if ( Vec_IntSize(vClause) == 0 )
                 break;
             RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
-            assert( RetValue );
+            if ( RetValue == 0 )
+                return 0;
         }
     }
     if ( Vec_IntSize(p->vTfo) > 0 )
@@ -126,7 +127,8 @@ int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
                 if ( Vec_IntSize(vClause) == 0 )
                     break;
                 RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
-                assert( RetValue );
+                if ( RetValue == 0 )
+                    return 0;
             }
         }
         // create XOR clauses for the roots

src/opt/sfm/sfmWin.c

@@ -125,33 +125,53 @@ static inline int   Sfm_ObjIsTravIdCurrent2( Sfm_Ntk_t * p, int Id )   { return
 
   Synopsis    [Collects used internal nodes in a topological order.]
 
-  Description []
+  Description [Additionally considers objects in groups as a single object
+  and collects them in a topological order together as single entity.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes )
+void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft )
 {
     int i, iFanin;
     if ( Sfm_ObjIsPi(p, iNode) )
         return;
     if ( Sfm_ObjIsTravIdCurrent(p, iNode) )
         return;
+    if ( Vec_IntEntry(vGroupMap, iNode) >= 0 )
+    {
+        int k, iGroup = Abc_Lit2Var( Vec_IntEntry(vGroupMap, iNode) );
+        Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup );
+        Vec_IntForEachEntry( vGroup, iNode, i )
+            assert( Sfm_ObjIsNode(p, iNode) );
+        Vec_IntForEachEntry( vGroup, iNode, i )
+            Sfm_ObjSetTravIdCurrent( p, iNode );
+        Vec_IntForEachEntry( vGroup, iNode, i )
+            Sfm_ObjForEachFanin( p, iNode, iFanin, k )
+                Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft );
+        Vec_IntForEachEntry( vGroup, iNode, i )
+            Vec_IntPush( vNodes, iNode );
+        Vec_IntPush( vBoxesLeft, iGroup );
+    }
+    else
+    {
         Sfm_ObjSetTravIdCurrent(p, iNode);
         Sfm_ObjForEachFanin( p, iNode, iFanin, i )
-        Sfm_NtkDfs_rec( p, iFanin, vNodes );
+            Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft );
         Vec_IntPush( vNodes, iNode );
+    }
 }
-Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p )
+Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft )
 {
     Vec_Int_t * vNodes;
     int i;
+    Vec_IntClear( vBoxesLeft );
     vNodes = Vec_IntAlloc( p->nObjs );
     Sfm_NtkIncrementTravId( p );
     Sfm_NtkForEachPo( p, i )
-        Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes );
+        Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft );
     return vNodes;
 }