Version abc70115

Makefile

@@ -11,7 +11,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd src/base/io src/base/main src
 	src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo \
 	src/map/fpga src/map/mapper src/map/mio src/map/super src/map/if \
 	src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \
-	src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim src/opt/ret src/opt/kit \
+	src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim src/opt/ret src/opt/res src/opt/kit \
 	src/sat/asat src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig 	
 
 default: $(PROG)

abc.dsp

@@ -1653,6 +1653,42 @@ SOURCE=.\src\opt\kit\kitSop.c
 SOURCE=.\src\opt\kit\kitTruth.c
 # End Source File
 # End Group
+# Begin Group "res"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\res\res.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resFilter.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resSim.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resStrash.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resUpdate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\res\resWin.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "map"
 

src/base/abc/abcDfs.c

@@ -533,7 +533,7 @@ void Abc_NtkNodeSupport_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
     // mark the node as visited
     Abc_NodeSetTravIdCurrent( pNode );
     // collect the CI
-    if ( Abc_ObjIsCi(pNode) )
+    if ( Abc_ObjIsCi(pNode) || Abc_ObjFaninNum(pNode) == 0 )
     {
         Vec_PtrPush( vNodes, pNode );
         return;

src/base/abc/abcFunc.c

@@ -765,6 +765,65 @@ DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot )
     return bFunc;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Construct BDDs and mark AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ConvertAigToAig_rec( Abc_Ntk_t * pNtkAig, Hop_Obj_t * pObj )
+{
+    assert( !Hop_IsComplement(pObj) );
+    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
+        return;
+    Abc_ConvertAigToAig_rec( pNtkAig, Hop_ObjFanin0(pObj) ); 
+    Abc_ConvertAigToAig_rec( pNtkAig, Hop_ObjFanin1(pObj) );
+    pObj->pData = Abc_AigAnd( pNtkAig->pManFunc, (Abc_Obj_t *)Hop_ObjChild0Copy(pObj), (Abc_Obj_t *)Hop_ObjChild1Copy(pObj) ); 
+    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
+    Hop_ObjSetMarkA( pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from AIG to BDD representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_ConvertAigToAig( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pObjOld )
+{
+    Hop_Man_t * pHopMan;
+    Hop_Obj_t * pRoot;
+    Abc_Obj_t * pFanin;
+    int i;
+    // get the local AIG
+    pHopMan = pObjOld->pNtk->pManFunc;
+    pRoot = pObjOld->pData;
+    // check the case of a constant
+    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
+        return Abc_ObjNotCond( Abc_AigConst1(pNtkAig->pManFunc), Hop_IsComplement(pRoot) );
+    // assign the fanin nodes
+    Abc_ObjForEachFanin( pObjOld, pFanin, i )
+        Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
+    // construct the AIG
+    Abc_ConvertAigToAig_rec( pNtkAig, Hop_Regular(pRoot) );
+    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
+    // return the result
+    return Abc_ObjNotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Unmaps the network.]

src/base/abci/abc.c

@@ -59,6 +59,7 @@ static int Abc_CommandCleanup        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSweep          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFastExtract    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDisjoint       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMfs            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandRewrite        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRefactor       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -193,6 +194,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "sweep",         Abc_CommandSweep,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Abc_CommandFastExtract,      1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "dsd",           Abc_CommandDisjoint,         1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "mfs",           Abc_CommandMfs,              1 );
 
     Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
@@ -2513,6 +2515,109 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nWindow;
+    int nSimWords;
+    int fVerbose;
+    int fVeryVerbose;
+    // external functions
+    extern int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerbose, int fVeryVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nWindow      = 33;
+    nSimWords    =  8;
+    fVerbose     =  1;
+    fVeryVerbose =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WSvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nWindow = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nWindow < 1 || nWindow > 99 ) 
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nSimWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nSimWords < 2 || nSimWords > 256 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkHasAig(pNtk) )
+    {
+        fprintf( pErr, "This command can only be applied to AIG logic network (run \"aig\").\n" );
+        return 1;
+    }
+
+    // modify the current network
+    if ( !Abc_NtkResynthesize( pNtk, nWindow, nSimWords, fVerbose, fVeryVerbose ) )
+    {
+        fprintf( pErr, "Resynthesis has failed.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: mfs [-W <NM>] [-S <n>] [-vwh]\n" );
+    fprintf( pErr, "\t          performs resubstitution-based resynthesis with don't-cares\n" );
+    fprintf( pErr, "\t-W <NM> : specifies the windowing paramters (00 < NM <= 99) [default = %d%d]\n", nWindow/10, nWindow%10 );
+    fprintf( pErr, "\t-S <n>  : specifies the number of simulation words (2 <= n <= 256) [default = %d]\n", nSimWords );
+    fprintf( pErr, "\t-v      : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-w      : toggle printout subgraph statistics [default = %s]\n", fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h      : print the command usage\n");
+    return 1;
+} 
+
+
 /**Function*************************************************************
 
   Synopsis    []

src/base/abci/abcIvy.c

@@ -199,7 +199,7 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int
 //    for ( i = 0; i < nIters; i++ )
 //        Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
     Ivy_ManRewriteSeq( pMan, 0, 0 );
-    Ivy_ManRewriteSeq( pMan, 1, 0 );
+//    Ivy_ManRewriteSeq( pMan, 1, 0 );
 //printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) );
 //    Ivy_ManHaigPostprocess( pMan, fVerbose );
 //timeRetime = clock() - timeRetime;

src/map/if/if.h

@@ -125,6 +125,7 @@ struct If_Man_t_
     float              fEpsilon;      // epsilon used for comparison
     float              RequiredGlo;   // global required times
     float              AreaGlo;       // global area
+    int                nNets;         // the sum total of fanins of all LUTs in the mapping
     int                nCutsUsed;     // the number of cuts currently used
     int                nCutsMerged;   // the total number of cuts merged
     unsigned *         puTemp[4];     // used for the truth table computation

src/map/if/ifMap.c

@@ -277,8 +277,8 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequi
         if ( p->pPars->fVerbose )
         {
             char Symb = (Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A');
-            printf( "%c:  Del = %6.2f. Area = %8.2f. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
+            printf( "%c:  Del = %6.2f. Area = %8.2f. Nets = %6d. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
-                Symb, p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+                Symb, p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
             PRT( "T", clock() - clk );
 //    printf( "Max number of cuts = %d. Average number of cuts = %5.2f.\n", 
 //        p->nCutsMax, 1.0 * p->nCutsMerged / If_ManAndNum(p) );

src/map/if/ifPrepro.c

@@ -100,8 +100,8 @@ void If_ManPerformMappingPreprocess( If_Man_t * p )
     If_ManComputeRequired( p, 1 );
     if ( p->pPars->fVerbose )
     {
-        printf( "S:  Del = %6.2f. Area = %8.2f. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
+        printf( "S:  Del = %6.2f. Area = %8.2f. Nets = %6d. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
-            p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+            p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
         PRT( "T", clock() - clk );
     }
 }

src/map/if/ifReduce.c

@@ -55,28 +55,30 @@ void If_ManImproveMapping( If_Man_t * p )
     If_ManComputeRequired( p, 0 );
     if ( p->pPars->fVerbose )
     {
-        printf( "E:  Del = %6.2f. Area = %8.2f. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
+        printf( "E:  Del = %6.2f. Area = %8.2f. Nets = %6d. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
-            p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+            p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
         PRT( "T", clock() - clk );
     }
+
 /*
     clk = clock();
     If_ManImproveReduce( p, p->pPars->nLutSize );
     If_ManComputeRequired( p, 0 );
     if ( p->pPars->fVerbose )
     {
-        printf( "R:  Del = %6.2f. Area = %8.2f. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
+        printf( "R:  Del = %6.2f. Area = %8.2f. Nets = %6d. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
-            p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+            p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
         PRT( "T", clock() - clk );
     }
-
+*/
+/*
     clk = clock();
     If_ManImproveExpand( p, p->pPars->nLutSize );
     If_ManComputeRequired( p, 0 );
     if ( p->pPars->fVerbose )
     {
-        printf( "E:  Del = %6.2f. Area = %8.2f. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
+        printf( "E:  Del = %6.2f. Area = %8.2f. Nets = %6d. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
-            p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+            p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
         PRT( "T", clock() - clk );
     }
 */

src/map/if/ifUtil.c

@@ -147,6 +147,7 @@ void If_ManComputeRequired( If_Man_t * p, int fFirstTime )
     If_Obj_t * pObj;
     int i;
     // compute area, clean required times, collect nodes used in the mapping
+    p->nNets = 0;
     p->AreaGlo = If_ManScanMapping( p );
     // get the global required times
     p->RequiredGlo = If_ManDelayMax( p, 0 );
@@ -206,6 +207,7 @@ float If_ManScanMapping_rec( If_Man_t * p, If_Obj_t * pObj, If_Obj_t ** ppStore
     ppStore[pObj->Level] = pObj;
     // visit the transitive fanin of the selected cut
     pCutBest = If_ObjCutBest(pObj);
+    p->nNets += pCutBest->nLeaves;
     aArea = If_CutLutArea( p, pCutBest );
     If_CutForEachLeaf( p, pCutBest, pLeaf, i )
         aArea += If_ManScanMapping_rec( p, pLeaf, ppStore );

src/misc/vec/vecPtr.h

@@ -149,6 +149,32 @@ static inline Vec_Ptr_t * Vec_PtrAllocArrayCopy( void ** pArray, int nSize )
     return p;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Allocates the array of simulation info.]
+
+  Description [Allocates the array containing given number of entries, 
+  each of which contains given number of unsigned words of simulation data.
+  The resulting array can be freed using regular procedure Vec_PtrFree().
+  It is the responsibility of the user to ensure this array is never grown.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrAllocSimInfo( int nEntries, int nWords )
+{
+    void ** pMemory;
+    unsigned * pInfo;
+    int i;
+    pMemory = (void **)ALLOC( char, (sizeof(void *) + sizeof(unsigned) * nWords) * nEntries );
+    pInfo = (unsigned *)(pMemory + nEntries);
+    for ( i = 0; i < nEntries; i++ )
+        pMemory[i] = pInfo + i * nWords;
+    return Vec_PtrAllocArray( pMemory, nEntries );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Duplicates the integer array.]

src/misc/vec/vecVec.h

@@ -61,6 +61,8 @@ struct Vec_Vec_t_
 #define Vec_VecForEachEntry( vGlob, pEntry, i, k )                                            \
     for ( i = 0; i < Vec_VecSize(vGlob); i++ )                                                \
         Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
+#define Vec_VecForEachEntryLevel( vGlob, pEntry, i, Level )                                   \
+        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, Level), pEntry, i ) 
 #define Vec_VecForEachEntryStart( vGlob, pEntry, i, k, LevelStart )                           \
     for ( i = LevelStart; i < Vec_VecSize(vGlob); i++ )                                       \
         Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 

src/opt/res/module.make

@@ -0,0 +1,7 @@
+SRC +=  src/opt/res/resCore.c \
+    src/opt/res/resFilter.c \
+    src/opt/res/resSat.c \
+    src/opt/res/resSim.c \
+    src/opt/res/resStrash.c \
+    src/opt/res/resUpdate.c \
+    src/opt/res/resWin.c

src/opt/res/res.h

@@ -0,0 +1,112 @@
+/**CFile****************************************************************
+
+  FileName    [res.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: res.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __RES_H__
+#define __RES_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Res_Win_t_ Res_Win_t;
+struct Res_Win_t_
+{
+    // the general data
+    int              nWinTfiMax; // the fanin levels
+    int              nWinTfoMax; // the fanout levels
+    int              nLevDivMax; // the maximum divisor level
+    int              nLevLeaves; // the level where leaves begin
+    Abc_Obj_t *      pNode;      // the node in the center
+    // the window data
+    Vec_Vec_t *      vLevels;    // nodes by level
+    Vec_Ptr_t *      vLeaves;    // leaves of the window
+    Vec_Ptr_t *      vRoots;     // roots of the window
+    Vec_Ptr_t *      vDivs;      // the candidate divisors of the node
+};
+
+typedef struct Res_Sim_t_ Res_Sim_t;
+struct Res_Sim_t_
+{
+    Abc_Ntk_t *      pAig;       // AIG for simulation
+    // simulation parameters
+    int              nWords;     // the number of simulation words
+    int              nPats;      // the number of patterns
+    int              nWordsOut;  // the number of simulation words in the output patterns
+    int              nPatsOut;   // the number of patterns in the output patterns 
+    // simulation info
+    Vec_Ptr_t *      vPats;      // input simulation patterns
+    Vec_Ptr_t *      vPats0;     // input simulation patterns
+    Vec_Ptr_t *      vPats1;     // input simulation patterns
+    Vec_Ptr_t *      vOuts;      // output simulation info
+    int              nPats0;     // the number of 0-patterns accumulated
+    int              nPats1;     // the number of 1-patterns accumulated
+    // resub candidates
+    Vec_Vec_t *      vCands;     // resubstitution candidates
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== resFilter.c ==========================================================*/
+extern Vec_Ptr_t *   Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim );
+/*=== resSat.c ==========================================================*/
+extern Hop_Obj_t *   Res_SatFindFunction( Hop_Man_t * pMan, Res_Win_t * pWin, Vec_Ptr_t * vFanins, Abc_Ntk_t * pAig );
+/*=== resSim.c ==========================================================*/
+extern Res_Sim_t *   Res_SimAlloc( int nWords );
+extern void          Res_SimFree( Res_Sim_t * p );
+extern int           Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig );
+/*=== resStrash.c ==========================================================*/
+extern Abc_Ntk_t *   Res_WndStrash( Res_Win_t * p );
+/*=== resWnd.c ==========================================================*/
+extern void          Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc );
+/*=== resWnd.c ==========================================================*/
+extern Res_Win_t *   Res_WinAlloc();
+extern void          Res_WinFree( Res_Win_t * p );
+extern int           Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, int nLevDivMax, Res_Win_t * p );
+extern void          Res_WinVisitNodeTfo( Res_Win_t * p );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/opt/res/resCore.c

@@ -0,0 +1,103 @@
+/**CFile****************************************************************
+
+  FileName    [resCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Top-level resynthesis procedure.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: resCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "res.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Entrace into the resynthesis package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerbose, int fVeryVerbose )
+{
+    Res_Win_t * pWin;
+    Res_Sim_t * pSim;
+    Abc_Ntk_t * pAig;
+    Abc_Obj_t * pObj;
+    Hop_Obj_t * pFunc;
+    Vec_Ptr_t * vFanins;
+    int i, nNodesOld;
+    assert( Abc_NtkHasAig(pNtk) );
+    assert( nWindow > 0 && nWindow < 100 );
+    // start the window
+    pWin = Res_WinAlloc();
+    pSim = Res_SimAlloc( nSimWords );
+    // set the number of levels
+    Abc_NtkLevel( pNtk );
+    // try resynthesizing nodes in the topological order
+    nNodesOld = Abc_NtkObjNumMax(pNtk);
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( !Abc_ObjIsNode(pObj) )
+            continue;
+        if ( pObj->Id > nNodesOld )
+            break;
+        // create the window for this node
+        if ( !Res_WinCompute(pObj, nWindow/10, nWindow%10, pObj->Level - 1, pWin) )
+            continue;
+        // create the AIG for the window
+        pAig = Res_WndStrash( pWin );
+        // prepare simulation info
+        if ( !Res_SimPrepare( pSim, pAig ) )
+        {
+            Abc_NtkDelete( pAig );
+            continue;
+        }
+        // find resub candidates for the node
+        vFanins = Res_FilterCandidates( pWin, pSim );
+        // check using SAT
+        pFunc = Res_SatFindFunction( pNtk->pManFunc, pWin, vFanins, pAig );
+        Abc_NtkDelete( pAig );
+        if ( pFunc == NULL )
+            continue;
+        // update the network
+        Res_UpdateNetwork( pObj, vFanins, pFunc );
+    }
+    Res_WinFree( pWin );
+    Res_SimFree( pSim );
+    // check the resulting network
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        fprintf( stdout, "Abc_NtkResynthesize(): Network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/res/resFilter.c

@@ -0,0 +1,53 @@
+/**CFile****************************************************************
+
+  FileName    [resFilter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resFilter.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "res.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim )
+{
+    return NULL;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/res/resSat.c

@@ -0,0 +1,55 @@
+/**CFile****************************************************************
+
+  FileName    [resSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Interface with the SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resSat.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "res.h"
+#include "hop.h"
+//#include "bf.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Res_SatFindFunction( Hop_Man_t * pMan, Res_Win_t * pWin, Vec_Ptr_t * vFanins, Abc_Ntk_t * pAig )
+{
+    return NULL;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/res/resSim.c

@@ -0,0 +1,433 @@
+/**CFile****************************************************************
+
+  FileName    [resSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Simulation engine.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resSim.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "res.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// generating random unsigned (#define RAND_MAX 0x7fff)
+#define SIM_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Res_Sim_t * Res_SimAlloc( int nWords )
+{
+    Res_Sim_t * p;
+    p = ALLOC( Res_Sim_t, 1 );
+    memset( p, 0, sizeof(Res_Sim_t) );
+    // simulation info
+    p->nWords = nWords;
+    p->nPats = 8 * sizeof(unsigned) * p->nWords;
+    p->nWordsOut = p->nPats * p->nWords;
+    p->nPatsOut = p->nPats * p->nPats;
+    // resub candidates
+    p->vPats = Vec_PtrAllocSimInfo( 1024, p->nWords );
+    p->vPats0 = Vec_PtrAllocSimInfo( 128, p->nWords );
+    p->vPats1 = Vec_PtrAllocSimInfo( 128, p->nWords );
+    p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut );
+    p->vCands = Vec_VecStart( 16 );
+    // set siminfo for the constant node
+    memset( Vec_PtrEntry(p->vPats,0), 0xff, sizeof(unsigned) * p->nWords );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+    assert( Abc_NtkIsStrash(pAig) );
+    p->pAig = pAig;
+    if ( Vec_PtrSize(p->vPats) < Abc_NtkObjNumMax(pAig)+1 )
+    {
+        Vec_PtrFree( p->vPats );
+        p->vPats = Vec_PtrAllocSimInfo( Abc_NtkObjNumMax(pAig)+1, p->nWords );
+    }
+    if ( Vec_PtrSize(p->vPats0) < Abc_NtkPiNum(pAig) )
+    {
+        Vec_PtrFree( p->vPats0 );
+        p->vPats0 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords );
+    }
+    if ( Vec_PtrSize(p->vPats1) < Abc_NtkPiNum(pAig) )
+    {
+        Vec_PtrFree( p->vPats1 );
+        p->vPats1 = Vec_PtrAllocSimInfo( Abc_NtkPiNum(pAig), p->nWords );
+    }
+    if ( Vec_PtrSize(p->vOuts) < Abc_NtkPoNum(pAig) )
+    {
+        Vec_PtrFree( p->vOuts );
+        p->vOuts = Vec_PtrAllocSimInfo( Abc_NtkPoNum(pAig), p->nWordsOut );
+    }
+    // clean storage info for patterns
+    memset( Vec_PtrEntry(p->vPats0,0), 0, sizeof(unsigned) * p->nWords * Abc_NtkPiNum(pAig) );
+    memset( Vec_PtrEntry(p->vPats1,0), 0, sizeof(unsigned) * p->nWords * Abc_NtkPiNum(pAig) );
+    p->nPats0 = 0;
+    p->nPats1 = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Free simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimFree( Res_Sim_t * p )
+{
+    Vec_PtrFree( p->vPats );
+    Vec_PtrFree( p->vPats0 );
+    Vec_PtrFree( p->vPats1 );
+    Vec_PtrFree( p->vOuts );
+    Vec_VecFree( p->vCands );
+    free( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sets random PI simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimSetRandom( Res_Sim_t * p )
+{
+    Abc_Obj_t * pObj;
+    unsigned * pInfo;
+    int i, w;
+    Abc_NtkForEachPi( p->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        for ( w = 0; w < p->nWords; w++ )
+            pInfo[w] = SIM_RANDOM_UNSIGNED;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets given PI simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimSetGiven( Res_Sim_t * p, Vec_Ptr_t * vInfo )
+{
+    Abc_Obj_t * pObj;
+    unsigned * pInfo, * pInfo2;
+    int i, w;
+    Abc_NtkForEachPi( p->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        pInfo2 = Vec_PtrEntry( vInfo, i );
+        for ( w = 0; w < p->nWords; w++ )
+            pInfo[w] = pInfo2[w];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPerformOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
+{
+    unsigned * pInfo, * pInfo1, * pInfo2;
+    int k, fComp1, fComp2;
+    // simulate the internal nodes
+    assert( Abc_ObjIsNode(pNode) );
+    pInfo  = Vec_PtrEntry(vSimInfo, pNode->Id);
+    pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+    pInfo2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode));
+    fComp1 = Abc_ObjFaninC0(pNode);
+    fComp2 = Abc_ObjFaninC1(pNode);
+    if ( fComp1 && fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] = ~pInfo1[k] & ~pInfo2[k];
+    else if ( fComp1 && !fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] = ~pInfo1[k] &  pInfo2[k];
+    else if ( !fComp1 && fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] =  pInfo1[k] & ~pInfo2[k];
+    else // if ( fComp1 && fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] =  pInfo1[k] &  pInfo2[k];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one PO node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimTransferOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
+{
+    unsigned * pInfo, * pInfo1;
+    int k, fComp1;
+    // simulate the internal nodes
+    assert( Abc_ObjIsCo(pNode) );
+    pInfo  = Vec_PtrEntry(vSimInfo, pNode->Id);
+    pInfo1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+    fComp1 = Abc_ObjFaninC0(pNode);
+    if ( fComp1 )
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] = ~pInfo1[k];
+    else 
+        for ( k = 0; k < nSimWords; k++ )
+            pInfo[k] =  pInfo1[k];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPerformRound( Res_Sim_t * p )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_AigForEachAnd( p->pAig, pObj, i )
+        Res_SimPerformOne( pObj, p->vPats, p->nWords );
+    Abc_NtkForEachPo( p->pAig, pObj, i )
+        Res_SimTransferOne( pObj, p->vPats, p->nWords );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Processes simulation patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimProcessPats( Res_Sim_t * p )
+{
+    Abc_Obj_t * pCare, * pNode, * pObj;
+    unsigned * pInfoCare, * pInfoNode;
+    int i, j;
+    pCare = Abc_NtkPo( p->pAig, 0 );
+    pNode = Abc_NtkPo( p->pAig, 0 );
+    pInfoCare = Vec_PtrEntry( p->vPats, pCare->Id );
+    pInfoNode = Vec_PtrEntry( p->vPats, pNode->Id );
+    for ( i = 0; i < p->nPats; i++ )
+    {
+        if ( !Abc_InfoHasBit(pInfoCare, i) )
+            continue;
+        if ( !Abc_InfoHasBit(pInfoNode, i) )
+        {
+            if ( p->nPats0 < p->nPats )
+            {
+                Abc_NtkForEachPi( p->pAig, pObj, j )
+                    if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
+                        Abc_InfoSetBit( Vec_PtrEntry(p->vPats0, j), p->nPats0 );
+                p->nPats0++;
+            }
+        }
+        else
+        {
+            if ( p->nPats1 < p->nPats )
+            {
+                Abc_NtkForEachPi( p->pAig, pObj, j )
+                    if ( Abc_InfoHasBit( Vec_PtrEntry(p->vPats, pObj->Id), i ) )
+                        Abc_InfoSetBit( Vec_PtrEntry(p->vPats1, j), p->nPats1 );
+                p->nPats1++;
+            }
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the simulation info to fill the space.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPadSimInfo( Vec_Ptr_t * vPats, int nPats, int nWords )
+{
+    unsigned * pInfo;
+    int i, w, iWords;
+    iWords = nPats / (8 * sizeof(unsigned));
+    if ( iWords == nWords )
+        return;
+    Vec_PtrForEachEntry( vPats, pInfo, i )
+        for ( w = iWords; w < nWords; i++ )
+            pInfo[w] = pInfo[0];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the simulation info to fill the space.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimDeriveInfoDuplicate( Res_Sim_t * p )
+{
+    unsigned * pInfo, * pInfo2;
+    Abc_Obj_t * pObj;
+    int i, j, w;
+    Abc_NtkForEachPo( p->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        pInfo2 = Vec_PtrEntry( p->vOuts, i );
+        for ( j = 0; j < p->nPats; j++ )
+            for ( w = 0; w < p->nWords; w++ )
+                *pInfo2++ = pInfo[w];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Complement the simulation info if necessary.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimDeriveInfoComplement( Res_Sim_t * p )
+{
+    unsigned * pInfo, * pInfo2;
+    Abc_Obj_t * pObj;
+    int i, j, w;
+    Abc_NtkForEachPo( p->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
+        pInfo2 = Vec_PtrEntry( p->vOuts, i );
+        for ( j = 0; j < p->nPats; j++, pInfo2 += p->nWords )
+            if ( Abc_InfoHasBit( pInfo, j ) )
+                for ( w = 0; w < p->nWords; w++ )
+                    pInfo2[w] = ~pInfo2[w];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares simulation info for candidate filtering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+    int Limit = 20;
+    // prepare the manager
+    Res_SimAdjust( p, pAig );
+    // collect 0/1 simulation info
+    while ( p->nPats0 < p->nPats || p->nPats1 < p->nPats || Limit-- == 0 )
+    {
+        Res_SimSetRandom( p );
+        Res_SimPerformRound( p );
+        Res_SimProcessPats( p );
+    }
+    if ( p->nPats0 < 32 || p->nPats1 < 32 )
+        return 0;
+    // create bit-matrix info
+    if ( p->nPats0 < p->nPats )
+        Res_SimPadSimInfo( p->vPats0, p->nPats0, p->nWords );
+    if ( p->nPats1 < p->nPats )
+        Res_SimPadSimInfo( p->vPats1, p->nPats1, p->nWords );
+    // resimulate 0-patterns
+    Res_SimSetGiven( p, p->vPats0 );
+    Res_SimPerformRound( p );
+    Res_SimDeriveInfoDuplicate( p );
+    // resimulate 1-patterns
+    Res_SimSetGiven( p, p->vPats1 );
+    Res_SimPerformRound( p );
+    Res_SimDeriveInfoComplement( p );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/res/resStrash.c

@@ -0,0 +1,105 @@
+/**CFile****************************************************************
+
+  FileName    [resStrash.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Strashes the window.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resStrash.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "res.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Abc_Obj_t * Abc_ConvertAigToAig( Abc_Ntk_t * pAig, Abc_Obj_t * pObjOld );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Structurally hashes the given window.]
+
+  Description [The first PO is the observability condition. The second 
+  is the node's function. The remaining POs are the candidate divisors.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
+{
+    Vec_Ptr_t * vPairs;
+    Abc_Ntk_t * pAig;
+    Abc_Obj_t * pObj, * pMiter;
+    int i, k;
+    assert( Abc_NtkHasAig(p->pNode->pNtk) );
+    // create the network
+    pAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    // duplicate the name and the spec
+    pAig->pName = Extra_UtilStrsav( "window" );
+    // create the inputs
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        pObj->pCopy = Abc_NtkCreatePi( pAig );
+    // go through the nodes in the topological order
+    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves + 1, (int)p->pNode->Level + p->nWinTfoMax )
+    {
+        pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
+        pObj->pCopy = Abc_ObjNotCond( pObj->pCopy, pObj == p->pNode );
+    }
+    // collect the PO outputs
+    vPairs = Vec_PtrAlloc( 2 * Vec_PtrSize(p->vRoots) );
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+    {
+        Vec_PtrPush( vPairs, pObj->pCopy );
+        Vec_PtrPush( vPairs, NULL );
+    }
+    // mark the TFO of the node
+    Res_WinVisitNodeTfo( p );
+    // redo strashing in the TFO
+    p->pNode->pCopy = Abc_ObjNot( p->pNode->pCopy );
+    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->pNode->Level + 1, (int)p->pNode->Level + p->nWinTfoMax )
+    {
+        if ( Abc_NodeIsTravIdCurrent(pObj) )
+            pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
+    }
+    // collect the PO outputs
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+        Vec_PtrWriteEntry( vPairs, 2 * i + 1, pObj->pCopy );
+    // add the miter
+    pMiter = Abc_AigMiter( pAig->pManFunc, vPairs );
+    Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pMiter );
+    Vec_PtrFree( vPairs );
+    // add the node
+    Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), p->pNode->pCopy );
+    // add the divisors
+    Vec_PtrForEachEntry( p->vDivs, pObj, i )
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );
+    // check the resulting network
+    if ( !Abc_NtkCheck( pAig ) )
+        fprintf( stdout, "Res_WndStrash(): Network check has failed.\n" );
+    return pAig;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/res/resUpdate.c

@@ -0,0 +1,51 @@
+/**CFile****************************************************************
+
+  FileName    [resUpdate.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Updates the network after changes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resUpdate.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "res.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/res/resWin.c

@@ -0,0 +1,456 @@
+/**CFile****************************************************************
+
+  FileName    [resWin.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    [Windowing algorithm.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resWin.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "res.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Res_Win_t * Res_WinAlloc()
+{
+    Res_Win_t * p;
+    p = ALLOC( Res_Win_t, 1 );
+    memset( p, 0, sizeof(Res_Win_t) );
+    p->vLevels = Vec_VecStart( 128 );
+    p->vLeaves = Vec_PtrAlloc( 512 );
+    p->vRoots  = Vec_PtrAlloc( 512 );
+    p->vDivs   = Vec_PtrAlloc( 512 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinFree( Res_Win_t * p )
+{
+    Vec_VecFree( p->vLevels );
+    Vec_PtrFree( p->vLeaves );
+    Vec_PtrFree( p->vRoots  );
+    Vec_PtrFree( p->vDivs   );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one node to the window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
+{
+    assert( !pObj->fMarkA );
+    pObj->fMarkA = 1;
+    Vec_VecPush( p->vLevels, pObj->Level, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Expands the frontier by one level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinCollectTfiOne( Res_Win_t * p, int Level )
+{
+    Vec_Ptr_t * vFront;
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k;
+    assert( Level > 0 );
+    vFront = Vec_VecEntry( p->vLevels, Level );
+    Vec_PtrForEachEntry( vFront, pObj, i )
+    {
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            if ( !pFanin->fMarkA )
+                Res_WinAddNode( p, pFanin );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes in the limited TFI of the node.]
+
+  Description [Marks the collected nodes with the current trav ID.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinCollectTfi( Res_Win_t * p )
+{
+    int i;
+    // expand storage for levels
+    if ( Vec_VecSize( p->vLevels ) <= (int)p->pNode->Level + p->nWinTfoMax )
+        Vec_VecExpand( p->vLevels, (int)p->pNode->Level + p->nWinTfoMax );
+    // start the frontier
+    Vec_VecClear( p->vLevels );
+    Res_WinAddNode( p, p->pNode );
+    // add one level at a time
+    for ( i = p->pNode->Level; i > p->nLevLeaves; i-- )
+        Res_WinCollectTfiOne( p, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFO of the collected nodes up to the given level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinSweepTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit || pObj == pNode )
+        return;
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return;
+    Abc_NodeSetTravIdCurrent( pObj );
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Res_WinSweepTfo_rec( pFanout, nLevelLimit, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFO of the collected nodes up to the given level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinSweepTfo( Res_Win_t * p )
+{
+    Abc_Obj_t * pObj;
+    int i, k;
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevLeaves )
+        Res_WinSweepTfo_rec( pObj, p->pNode->Level + p->nWinTfoMax, p->pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively collects the roots.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    assert( Abc_ObjIsNode(pObj) );
+    assert( Abc_NodeIsTravIdCurrent(pObj) );
+    // check if the node has all fanouts marked
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        if ( !Abc_NodeIsTravIdCurrent(pObj) )
+            break;
+    // if some of the fanouts are unmarked, add the node to the root
+    if ( i < Abc_ObjFanoutNum(pObj) ) 
+    {
+        Vec_PtrPush( vRoots, pObj );
+        return;
+    }
+    // otherwise, call recursively
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Res_WinCollectRoots_rec( pFanout, vRoots );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the roots of the window.]
+
+  Description [Roots of the window are the nodes that have at least
+  one fanout that it not in the TFO of the leaves.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinCollectRoots( Res_Win_t * p )
+{
+    Vec_PtrClear( p->vRoots );
+    Res_WinCollectRoots_rec( p->pNode, p->vRoots );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively augments the window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    if ( !Abc_NodeIsTravIdCurrent(pObj) )
+        return;
+    if ( pObj->fMarkA )
+        return;
+    Res_WinAddNode( p, pObj );
+    // visit the fanins of the node
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Res_WinAddMissing_rec( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds to the window visited nodes in the TFI of the roots.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinAddMissing( Res_Win_t * p )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+        Res_WinAddMissing_rec( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect all the nodes that fanin into the window nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinCollectLeaves( Res_Win_t * p )
+{
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, f;
+    // add the leaves
+    Vec_PtrClear( p->vLeaves );
+    // collect the nodes below the given level
+    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevLeaves )
+        Vec_PtrPush( p->vLeaves, pObj );
+    // add to leaves the fanins of the nodes above the given level
+    Vec_VecForEachEntryStart( p->vLevels, pObj, i, k, p->nLevLeaves + 1 )
+    {
+        Abc_ObjForEachFanin( pObj, pFanin, f )
+        {
+            if ( !pFanin->fMarkA )
+            {
+                pFanin->fMarkA = 1;
+                Vec_PtrPush( p->vLeaves, pFanin );
+            }
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinVisitNodeTfo( Res_Win_t * p )
+{
+    // mark the TFO of the node
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Res_WinSweepTfo_rec( p->pNode, p->nLevDivMax, NULL );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinCollectDivisors( Res_Win_t * p )
+{
+    Abc_Obj_t * pObj, * pFanout, * pFanin;
+    int i, k, f, m;
+    // mark the TFO of the node
+    Res_WinVisitNodeTfo( p );
+    // go through all the legal levels and check if their fanouts can be divisors
+    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax - 1 )
+    {
+        Abc_ObjForEachFanout( pObj, pFanout, f )
+        {
+            // skip COs
+            if ( !Abc_ObjIsNode(pFanout) ) 
+                continue;
+            // skip nodes in the TFO of node
+            if ( Abc_NodeIsTravIdCurrent(pFanout) )
+                continue;
+            // skip nodes that are already added
+            if ( pFanout->fMarkA )
+                continue;
+            // skip nodes with large level
+            if ( (int)pFanout->Level > p->nLevDivMax )
+                continue;
+            // skip nodes whose fanins are not in the cone
+            Abc_ObjForEachFanin( pFanout, pFanin, m )
+                if ( !pFanin->fMarkA )
+                    break;
+            if ( m < Abc_ObjFaninNum(pFanin) )
+                continue;
+            // add the node
+            Res_WinAddNode( p, pFanout );
+        }
+    }
+    // collect the divisors below the line
+    Vec_PtrClear( p->vDivs );
+    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax )
+        Vec_PtrPush( p->vDivs, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinUnmark( Res_Win_t * p )
+{
+    Vec_Ptr_t * vLevel;
+    Abc_Obj_t * pObj;
+    int i, k;
+    Vec_VecForEachEntry( p->vLevels, pObj, i, k )
+        pObj->fMarkA = 0;
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        pObj->fMarkA = 0;
+    // remove leaves from the set
+    Vec_VecForEachLevelStartStop( p->vLevels, vLevel, i, 0, p->nLevLeaves )
+        Vec_PtrClear( vLevel );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, int nLevDivMax, Res_Win_t * p )
+{
+    assert( Abc_ObjIsNode(pNode) );
+    assert( nWinTfiMax > 0 && nWinTfoMax > 0 );
+    // initialize the window
+    p->pNode = pNode;
+    p->nWinTfiMax = nWinTfiMax;
+    p->nWinTfoMax = nWinTfoMax;
+    p->nLevDivMax = nLevDivMax;
+    p->nLevLeaves = ABC_MAX( 0, p->pNode->Level - p->nWinTfiMax - 1 );
+    // collect the nodes in TFI cone of pNode down to the given level (nWinTfiMax)
+    Res_WinCollectTfi( p );
+    // mark the TFO of the collected nodes up to the given level (nWinTfoMax)
+    Res_WinSweepTfo( p );
+    // find the roots of the window
+    Res_WinCollectRoots( p );
+    // add the nodes in the TFI of the roots that are not yet in the window
+    Res_WinAddMissing( p );
+    // find the leaves of the window
+    Res_WinCollectLeaves( p );
+    // collect the divisors up to the given maximum divisor level (nLevDivMax)
+    if ( nLevDivMax >= 0 )
+        Res_WinCollectDivisors( p );
+    else
+        Vec_PtrClear( p->vDivs );
+    // unmark window nodes
+    Res_WinUnmark( p );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/res/res_.c

@@ -0,0 +1,50 @@
+/**CFile****************************************************************
+
+  FileName    [res_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: res_.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "res.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+