Version abc50806

abc.dsp

@@ -42,7 +42,7 @@ RSC=rc.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
-# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\sop\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c
 # ADD BASE RSC /l 0x409 /d "NDEBUG"
 # ADD RSC /l 0x409 /d "NDEBUG"
 BSC32=bscmake.exe
@@ -66,7 +66,7 @@ LINK32=link.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
-# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\sop\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /GZ /c
 # ADD BASE RSC /l 0x409 /d "_DEBUG"
 # ADD RSC /l 0x409 /d "_DEBUG"
 BSC32=bscmake.exe
@@ -145,6 +145,10 @@ SOURCE=.\src\base\abc\abcFunc.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abc\abcFxu.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abc\abcInt.h
 # End Source File
 # Begin Source File
@@ -964,6 +968,66 @@ SOURCE=.\src\sat\fraig\fraigVec.c
 
 # PROP Default_Filter ""
 # End Group
+# Begin Group "fxu"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxu.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxu.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuCreate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuHeapD.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuHeapS.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuList.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuMatrix.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuPair.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuPrint.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuReduce.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuSelect.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuSingle.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\fxu\fxuUpdate.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "map"
 

abc.rc

@@ -11,7 +11,7 @@ alias r read
 alias rl read_blif
 alias rb read_bench
 alias rv read_verilog
-alias rsup read_super
+alias rsup read_super mcnc5_old.super
 alias rlib read_library
 alias sa set autoexec ps
 alias so source -x

src/base/abc/abc.h

@@ -480,6 +480,7 @@ extern bool               Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose );
 extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk );
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
+extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
 extern int                Abc_SopGetCubeNum( char * pSop );
 extern int                Abc_SopGetLitNum( char * pSop );
 extern int                Abc_SopGetVarNum( char * pSop );

src/base/abc/abcAttach.c

@@ -267,6 +267,8 @@ void Abc_AttachComputeTruth( char * pSop, unsigned uTruthsIn[][2], unsigned * uT
             }
             uTruthRes[0] |= uSignCube[0];
         }
+        if ( Abc_SopGetPhase(pSop) == 0 )
+            uTruthRes[0] = ~uTruthRes[0];
         if ( nInputs < 5 )
             uTruthRes[0] &= ATTACH_MASK(1<<nInputs);
     }
@@ -295,6 +297,13 @@ void Abc_AttachComputeTruth( char * pSop, unsigned uTruthsIn[][2], unsigned * uT
             uTruthRes[0] |= uSignCube[0];
             uTruthRes[1] |= uSignCube[1];
         }
+
+        // complement if the SOP is complemented
+        if ( Abc_SopGetPhase(pSop) == 0 )
+        {
+            uTruthRes[0] = ~uTruthRes[0];
+            uTruthRes[1] = ~uTruthRes[1];
+        }
     }
 }
 

src/base/abc/abcDfs.c

@@ -223,9 +223,12 @@ int Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk )
     }
     else
     {
-        Abc_NtkForEachCo( pNtk, pNode, i )
+//        Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_NtkForEachNode( pNtk, pNode, i )
         {
-            pDriver = Abc_ObjFanin0( pNode );
+//            pDriver = Abc_ObjFanin0( pNode );
+            pDriver = pNode;
+
             Abc_NtkGetLevelNum_rec( pDriver );
             if ( LevelsMax < pDriver->Level )
                 LevelsMax = pDriver->Level;

src/base/abc/abcFxu.c

+/**CFile****************************************************************
+
+  FileName    [abcFxu.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Interface with the fast extract package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcFxu.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fxu.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+static bool Abc_NtkFxuCheck( Abc_Ntk_t * pNtk );
+static void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p );
+static void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast_extract on the current network.]
+
+  Description [Takes the network and the maximum number of nodes to extract.
+  Uses the concurrent double-cube and single cube divisor extraction procedure.
+  Modifies the network in the end, after extracting all nodes. Note that 
+  Ntk_NetworkSweep() may increase the performance of this procedure because 
+  the single-literal nodes will not be created in the sparse matrix. Returns 1 
+  if the network has been changed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
+{
+    assert( Abc_NtkIsLogicBdd(pNtk) || Abc_NtkIsLogicSop(pNtk) );
+    // convert nodes to SOPs
+    if ( Abc_NtkIsLogicBdd(pNtk) )
+        Abc_NtkBddToSop(pNtk);
+    else
+    { // to make sure the SOPs are SCC-free
+//        Abc_NtkSopToBdd(pNtk);
+//        Abc_NtkBddToSop(pNtk);
+    }
+    // check if the network meets the requirements
+    if ( !Abc_NtkFxuCheck(pNtk) )
+    {
+        printf( "Abc_NtkFastExtract: Nodes have duplicated or complemented fanins. FXU is not performed.\n" );
+        return 0;
+    }
+    // sweep removes useless nodes
+    Abc_NtkCleanup( pNtk, 0 );
+    // collect information about the covers
+    // make sure all covers are SCC free
+    // allocate literal array for each cover
+    Abc_NtkFxuCollectInfo( pNtk, p );
+    // call the fast extract procedure
+    // returns the number of divisor extracted
+    if ( Fxu_FastExtract(p) > 0 )
+    {
+        // update the network
+        Abc_NtkFxuReconstruct( pNtk, p );
+        // make sure everything is okay
+        if ( !Abc_NtkCheck( pNtk ) )
+            printf( "Abc_NtkFastExtract: The network check has failed.\n" );
+        return 1;
+    }
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Makes sure the nodes do not have complemented and duplicated fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkFxuCheck( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode, * pFanin1, * pFanin2;
+    int n, i, k;
+    Abc_NtkForEachNode( pNtk, pNode, n )
+    {
+        Abc_ObjForEachFanin( pNode, pFanin1, i )
+        {
+            if ( Abc_ObjFaninC(pNode, i) )
+                return 0;
+            Abc_ObjForEachFanin( pNode, pFanin2, k )
+            {
+                if ( i == k )
+                    continue;
+                if ( pFanin1 == pFanin2 )
+                    return 0;
+            }
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect information about the network for fast_extract.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    // add information to the manager
+    p->pManSop    = pNtk->pManFunc;
+    p->vSops      = Vec_PtrAlloc(0);
+    p->vFanins    = Vec_PtrAlloc(0);
+    p->vSopsNew   = Vec_PtrAlloc(0);
+    p->vFaninsNew = Vec_PtrAlloc(0);
+    Vec_PtrFill( p->vSops,      pNtk->vObjs->nSize, NULL );
+    Vec_PtrFill( p->vFanins,    pNtk->vObjs->nSize, NULL );
+    Vec_PtrFill( p->vSopsNew,   pNtk->vObjs->nSize + p->nNodesExt, NULL );
+    Vec_PtrFill( p->vFaninsNew, pNtk->vObjs->nSize + p->nNodesExt, NULL );
+    // add SOPs and fanin array
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_SopGetVarNum(pNode->pData) < 2 )
+            continue;
+        if ( Abc_SopGetCubeNum(pNode->pData) < 1 )
+            continue;
+        p->vSops->pArray[i]   = pNode->pData;
+        p->vFanins->pArray[i] = &pNode->vFanins;
+    }
+    p->nNodesOld = pNtk->vObjs->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFxuFreeInfo( Fxu_Data_t * p )
+{
+    int i;
+    // free the arrays of new fanins
+    if ( p->vFaninsNew )
+        for ( i = 0; i < p->vFaninsNew->nSize; i++ )
+            if ( p->vFaninsNew->pArray[i] )
+                Vec_IntFree( p->vFaninsNew->pArray[i] );
+    // free the arrays
+    if ( p->vSops      ) Vec_PtrFree( p->vSops      );
+    if ( p->vSopsNew   ) Vec_PtrFree( p->vSopsNew   );
+    if ( p->vFanins    ) Vec_PtrFree( p->vFanins    );
+    if ( p->vFaninsNew ) Vec_PtrFree( p->vFaninsNew );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recostructs the network after FX.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
+{
+    Vec_Fan_t * vFaninsOld;
+    Vec_Int_t * vFanins;
+    Abc_Obj_t * pNode, * pFanin;
+    int i, k;
+
+    assert( p->vFanins->nSize < p->vFaninsNew->nSize );
+    // create the new nodes
+    for ( i = p->vFanins->nSize; i < p->vFanins->nSize + p->nNodesNew; i++ )
+    {
+        // start the node
+        pNode = Abc_NtkCreateNode( pNtk );
+        assert( i == (int)pNode->Id );
+    }
+    // update the old nodes
+    for ( i = 0; i < p->vFanins->nSize; i++ )
+    {
+        // the new array of fanins
+        vFanins = p->vFaninsNew->pArray[i];
+        if ( vFanins == NULL )
+            continue;
+        // remove old fanins
+        pNode = Abc_NtkObj( pNtk, i );
+        vFaninsOld = &pNode->vFanins;
+        for ( k = vFaninsOld->nSize - 1; k >= 0; k-- )
+        {
+            pFanin = Abc_NtkObj( pNtk, vFaninsOld->pArray[k].iFan );
+            Abc_ObjDeleteFanin( pNode, pFanin );
+        }
+        // add new fanins
+        vFanins = p->vFaninsNew->pArray[i];
+        for ( k = 0; k < vFanins->nSize; k++ )
+        {
+            pFanin = Abc_NtkObj( pNtk, vFanins->pArray[k] );
+            Abc_ObjAddFanin( pNode, pFanin );
+        }
+        pNode->pData = p->vSopsNew->pArray[i];
+        assert( pNode->pData != NULL );
+    }
+    // set up the new nodes
+    for ( i = p->vFanins->nSize; i < p->vFanins->nSize + p->nNodesNew; i++ )
+    {
+        // get the new node
+        pNode = Abc_NtkObj( pNtk, i );
+        // add the fanins
+        vFanins = p->vFaninsNew->pArray[i];
+        for ( k = 0; k < vFanins->nSize; k++ )
+        {
+            pFanin = Abc_NtkObj( pNtk, vFanins->pArray[k] );
+            Abc_ObjAddFanin( pNode, pFanin );
+        }
+        pNode->pData = p->vSopsNew->pArray[i];
+        assert( pNode->pData != NULL );
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcMap.c

@@ -33,6 +33,12 @@ static Abc_Obj_t *  Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNode
 static Abc_Obj_t *  Abc_NodeFromMapPhase_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int fPhase );
 static Abc_Obj_t *  Abc_NodeFromMapSuper_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, Map_Super_t * pSuper, Abc_Obj_t * pNodePis[], int nNodePis );
 static Abc_Obj_t *  Abc_NtkFixCiDriver( Abc_Obj_t * pNode );
+
+static Abc_Ntk_t *  Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk );
+static void         Abc_NodeSuperChoice( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode );
+static void         Abc_NodeFromMapCutPhase( Abc_Ntk_t * pNtkNew, Map_Cut_t * pCut, int fPhase );
+static Abc_Obj_t *  Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Super_t * pSuper, Abc_Obj_t * pNodePis[], int nNodePis );
+
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -53,8 +59,8 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
 {
     int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
-
     Map_Man_t * pMan;
+    int clk;
 
     assert( Abc_NtkIsAig(pNtk) );
 
@@ -81,11 +87,13 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
     pMan = Abc_NtkToMap( pNtk, DelayTarget, fRecovery, fVerbose );
     if ( pMan == NULL )
         return NULL;
+clk = clock();
     if ( !Map_Mapping( pMan ) )
     {
         Map_ManFree( pMan );
         return NULL;
     }
+    Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk );
 
     // reconstruct the network after mapping
     pNtkNew = Abc_NtkFromMap( pMan, pNtk );
@@ -432,6 +440,265 @@ Abc_Obj_t * Abc_NtkFixCiDriver( Abc_Obj_t * pNode )
 
 
 
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
+{
+    int fCheck = 1;
+    Abc_Ntk_t * pNtkNew;
+
+    Map_Man_t * pMan;
+
+    assert( Abc_NtkIsAig(pNtk) );
+
+    // check that the library is available
+    if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == NULL )
+    {
+        printf( "The current library is not available.\n" );
+        return 0;
+    }
+
+    // derive the supergate library
+    if ( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) == NULL && Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) )
+    {
+        printf( "A simple supergate library is derived from gate library \"%s\".\n", 
+            Mio_LibraryReadName(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame())) );
+        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
+    }
+
+    // print a warning about choice nodes
+    if ( Abc_NtkCountChoiceNodes( pNtk ) )
+        printf( "Performing mapping with choices.\n" );
+
+    // perform the mapping
+    pMan = Abc_NtkToMap( pNtk, -1, 1, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    if ( !Map_Mapping( pMan ) )
+    {
+        Map_ManFree( pMan );
+        return NULL;
+    }
+
+    // reconstruct the network after mapping
+    pNtkNew = Abc_NtkFromMapSuperChoice( pMan, pNtk );
+    if ( pNtkNew == NULL )
+        return NULL;
+    Map_ManFree( pMan );
+
+    // make sure that everything is okay
+    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkMap: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Ntk_t * pNtkNew, * pNtkNew2;
+    Abc_Obj_t * pNode;
+    int i;
+
+    // save the pointer to the mapped nodes
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pNext = pNode->pCopy;
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        pNode->pNext = pNode->pCopy;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        pNode->pNext = pNode->pCopy;
+
+    // duplicate the network
+    pNtkNew2 = Abc_NtkDup( pNtk );
+    pNtkNew  = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1 );
+    Abc_NtkBddToSop( pNtkNew );
+
+    // set the old network to point to the new network
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = pNode->pCopy->pCopy;
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        pNode->pCopy = pNode->pCopy->pCopy;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        pNode->pCopy = pNode->pCopy->pCopy;
+    Abc_NtkDelete( pNtkNew2 );
+
+    // set the pointers from the mapper to the new nodes
+    Abc_NtkForEachCi( pNtk, pNode, i )
+    {
+        Map_NodeSetData( Map_ManReadInputs(pMan)[i], 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) );
+        Map_NodeSetData( Map_ManReadInputs(pMan)[i], 1, (char *)pNode->pCopy );
+    }
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        Map_NodeSetData( (Map_Node_t *)pNode->pNext, 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) );
+        Map_NodeSetData( (Map_Node_t *)pNode->pNext, 1, (char *)pNode->pCopy );
+    }
+
+    // assign the mapping of the required phase to the POs
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        Abc_NodeSuperChoice( pNtkNew, pNode );
+    }
+    Extra_ProgressBarStop( pProgress );
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoice( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
+{
+    Map_Node_t * pMapNode = (Map_Node_t *)pNode->pNext;
+    Map_Cut_t * pCuts, * pTemp;
+
+    pCuts = Map_NodeReadCuts(pMapNode);
+    for ( pTemp = Map_CutReadNext(pCuts); pTemp; pTemp = Map_CutReadNext(pTemp) )
+    {
+        Abc_NodeFromMapCutPhase( pNtkNew, pTemp, 0 );
+        Abc_NodeFromMapCutPhase( pNtkNew, pTemp, 1 );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the nodes corrresponding to one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFromMapCutPhase( Abc_Ntk_t * pNtkNew, Map_Cut_t * pCut, int fPhase )
+{
+    Abc_Obj_t * pNodePIs[10];
+    Map_Node_t ** ppLeaves;
+    Map_Super_t * pSuperBest;
+    unsigned uPhaseBest;
+    int i, fInvPin, nLeaves;
+
+    pSuperBest = Map_CutReadSuperBest( pCut, fPhase );
+    if ( pSuperBest == NULL )
+        return;
+
+    // get the information about the best cut 
+    uPhaseBest = Map_CutReadPhaseBest( pCut, fPhase );
+    nLeaves    = Map_CutReadLeavesNum( pCut );
+    ppLeaves   = Map_CutReadLeaves( pCut );
+
+    // collect the PI nodes
+    for ( i = 0; i < nLeaves; i++ )
+    {
+        fInvPin = ((uPhaseBest & (1 << i)) > 0);
+        pNodePIs[i] = (Abc_Obj_t *)Map_NodeReadData( ppLeaves[i], !fInvPin );
+        assert( pNodePIs[i] != NULL );
+    }
+
+    // implement the supergate
+    Abc_NodeFromMapSuperChoice_rec( pNtkNew, pSuperBest, pNodePIs, nLeaves );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the nodes corrresponding to one supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Super_t * pSuper, Abc_Obj_t * pNodePis[], int nNodePis )
+{
+    Mio_Gate_t * pRoot;
+    Map_Super_t ** ppFanins;
+    Abc_Obj_t * pNodeNew, * pNodeFanin;
+    int nFanins, Number, i;
+
+    // get the parameters of the supergate
+    pRoot = Map_SuperReadRoot(pSuper);
+    if ( pRoot == NULL )
+    {
+        Number = Map_SuperReadNum(pSuper);
+        if ( Number < nNodePis )  
+        {
+            return pNodePis[Number];
+        }
+        else
+        {  
+//            assert( 0 );
+            /* It might happen that a super gate with 5 inputs is constructed that
+             * actually depends only on the first four variables; i.e the fifth is a
+             * don't care -- in that case we connect constant node for the fifth
+             * (since the cut only has 4 variables). An interesting question is what
+             * if the first variable (and not the fifth one is the redundant one;
+             * can that happen?) */
+            return Abc_NodeCreateConst0(pNtkNew);
+        }
+    }
+
+    // get information about the fanins of the supergate
+    nFanins  = Map_SuperReadFaninNum( pSuper );
+    ppFanins = Map_SuperReadFanins( pSuper );
+    // create a new node with these fanins
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    for ( i = 0; i < nFanins; i++ )
+    {
+        pNodeFanin = Abc_NodeFromMapSuperChoice_rec( pNtkNew, ppFanins[i], pNodePis, nNodePis );
+        Abc_ObjAddFanin( pNodeNew, pNodeFanin );
+    }
+    pNodeNew->pData = Abc_SopRegister( pNtkNew->pManFunc, Mio_GateReadSop(pRoot) );
+    return pNodeNew;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abc/abcNetlist.c

@@ -67,7 +67,12 @@ Abc_Ntk_t * Abc_NtkLogic( Abc_Ntk_t * pNtk )
             Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
     // create and connect the POs
     Abc_NtkForEachPo( pNtk, pObj, i )
-        Abc_ObjAddFanin( Abc_NtkCreateTermPo(pNtkNew), Abc_ObjFanin0(pObj)->pCopy );
+    {
+        if ( Abc_ObjFaninNum(pObj) == 0 )
+            Abc_ObjAddFanin( Abc_NtkCreateTermPo(pNtkNew), pObj->pCopy );
+        else
+            Abc_ObjAddFanin( Abc_NtkCreateTermPo(pNtkNew), Abc_ObjFanin0(pObj)->pCopy );
+    }
     // connect the latches
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );

src/base/abc/abcPrint.c

@@ -59,7 +59,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
     if ( Abc_NtkIsLogicSop(pNtk) )   
     {
         fprintf( pFile, "  cube = %5d",  Abc_NtkGetCubeNum(pNtk) );
-//        fprintf( pFile, "  lit(sop) = %5d",  Abc_NtkGetLitNum(pNtk) );
+        fprintf( pFile, "  lit(sop) = %5d",  Abc_NtkGetLitNum(pNtk) );
         fprintf( pFile, "  lit(fac) = %5d",  Abc_NtkGetLitFactNum(pNtk) );
     }
     else if ( Abc_NtkIsLogicBdd(pNtk) )

src/base/abc/abcRenode.c

@@ -130,6 +130,8 @@ void Abc_NtkRenodeInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( Abc_ObjIsTerm(Abc_ObjFanin0(pNode)) )
+            continue;
         Abc_NtkRenode_rec( pNtkNew, Abc_ObjFanin0(pNode) );
     }
     Extra_ProgressBarStop( pProgress );

src/base/abc/abcSop.c

@@ -61,6 +61,37 @@ char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName )
 
 /**Function*************************************************************
 
+  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars )
+{
+    char * pSopCover;
+    char * pCube;
+    int i, v;
+    pSopCover = Extra_MmFlexEntryFetch( pMan, nCubes * (nVars + 3) + 1 );
+    for ( i = 0; i < nCubes; i++ )
+    {
+        pCube = pSopCover + i * (nVars + 3);
+        for ( v = 0; v < nVars; v++ )
+            pCube[v] = '-';
+        pCube[nVars + 0] = ' ';
+        pCube[nVars + 1] = '1';
+        pCube[nVars + 2] = '\n';
+    }
+    pSopCover[nCubes * (nVars + 3)] = 0;
+    return pSopCover;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Reads the number of cubes in the cover.]
 
   Description []

src/base/abc/abcStrash.c

@@ -107,6 +107,7 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 
     // perform strashing
     vNodes = Abc_NtkDfs( pNtk );
+//    vNodes = Abc_AigCollectAll( pNtk );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     for ( i = 0; i < vNodes->nSize; i++ )
     {

src/base/abc/abcUtil.c

@@ -768,6 +768,11 @@ Vec_Ptr_t * Abc_AigCollectAll( Abc_Ntk_t * pNtk )
     vNodes = Vec_PtrAlloc( 100 );
     Abc_NtkForEachNode( pNtk, pNode, i )
         Vec_PtrPush( vNodes, pNode );
+
+    // works only if the levels are set!!!
+    if ( !Abc_NtkIsAig(pNtk) )
+        Abc_NtkGetLevelNum(pNtk);
+
     Vec_PtrSort( vNodes, Abc_NodeCompareLevelsIncrease );
     return vNodes;
 }

src/base/abc/abc_.c

+/**CFile****************************************************************
+
+  FileName    [abc_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/map/fpga/fpgaCore.c

@@ -127,12 +127,19 @@ int Fpga_MappingPostProcess( Fpga_Man_t * p )
     float aSwitchTotalPrev, aSwitchTotalCur;
     int Iter, clk;
 
+
 if ( p->fVerbose )
 {
 printf( "Iteration %dD :  Area = %11.1f  ", 0, Fpga_MappingArea( p ) );
 PRT( "Time", p->timeMatch );
 }
 
+
+//    Fpga_MappingExplore( p );
+//    p->fAreaGlo = Fpga_MappingArea( p );
+//    return;
+
+
 //    aAreaTotalCur = FPGA_FLOAT_LARGE;
     aAreaTotalCur = Fpga_MappingSetRefsAndArea( p );
 
@@ -159,6 +166,11 @@ PRT( "Time", clock() - clk );
     } while ( aAreaTotalPrev > 1.02 * aAreaTotalCur );
 
 
+//    Fpga_MappingExplore( p );
+//    p->fAreaGlo = Fpga_MappingArea( p );
+//    return;
+
+
 /*
     // compute the area of each cut
     aAreaTotalCur = Fpga_MappingSetRefsAndArea( p );

src/map/fpga/fpgaInt.h

@@ -334,6 +334,7 @@ extern float             Fpga_TimeComputeArrivalMax( Fpga_Man_t * p );
 extern void              Fpga_TimeComputeRequiredGlobal( Fpga_Man_t * p );
 extern void              Fpga_TimeComputeRequired( Fpga_Man_t * p, float fRequired );
 extern void              Fpga_TimePropagateRequired( Fpga_Man_t * p, Fpga_NodeVec_t * vNodes );
+extern void              Fpga_TimePropagateArrival( Fpga_Man_t * p );
 /*=== fpgaTruth.c ===============================================================*/
 extern void              Fpga_MappingTruths( Fpga_Man_t * pMan );
 /*=== fpgaVec.c =============================================================*/
@@ -368,6 +369,7 @@ extern float             Fpga_MappingGetAreaFlow( Fpga_Man_t * p );
 extern float             Fpga_MappingArea( Fpga_Man_t * pMan );
 extern float             Fpga_MappingComputeCutAreas( Fpga_Man_t * pMan );
 extern float             Fpga_MappingSetRefsAndArea( Fpga_Man_t * pMan );
+extern Fpga_NodeVec_t *  Fpga_MappingCollectRefed( Fpga_Man_t * pMan );
 extern int               Fpga_MappingCountLevels( Fpga_Man_t * pMan );
 extern void              Fpga_MappingUnmark( Fpga_Man_t * pMan );
 extern void              Fpga_MappingUnmark_rec( Fpga_Node_t * pNode );

src/map/fpga/fpgaMatch.c

@@ -724,6 +724,112 @@ clk = clock();
 }
 
 #endif
+
+
+/**function*************************************************************
+
+  synopsis    [Performs area minimization using a heuristic algorithm.]
+
+  description []
+               
+  sideeffects []
+
+  seealso     []
+
+***********************************************************************/
+float Fpga_FindBestNode( Fpga_Man_t * p, Fpga_NodeVec_t * vNodes, Fpga_Node_t ** ppNode, Fpga_Cut_t ** ppCutBest )
+{
+    Fpga_Node_t * pNode;
+    Fpga_Cut_t * pCut;
+    float Gain, CutArea1, CutArea2, CutArea3;
+    int i;
+
+    Gain = 0;
+    for ( i = 0; i < vNodes->nSize; i++ )
+    {
+        pNode = vNodes->pArray[i];
+        // deref the current cut
+        CutArea1 = Fpga_CutDeref( p, pNode, pNode->pCutBest, 0 );
+
+        // ref all the cuts
+        for ( pCut = pNode->pCuts->pNext; pCut; pCut = pCut->pNext )
+        {
+            if ( pCut == pNode->pCutBest )
+                continue;
+            if ( pCut->tArrival > pNode->tRequired )
+                continue;
+
+            CutArea2 = Fpga_CutGetAreaDerefed( p, pCut );
+            if ( Gain < CutArea1 - CutArea2 )
+            {
+                *ppNode = pNode;
+                *ppCutBest = pCut;
+                Gain = CutArea1 - CutArea2;
+            }
+        }
+        // ref the old cut
+        CutArea3 = Fpga_CutRef( p, pNode, pNode->pCutBest, 0 );
+        assert( CutArea1 == CutArea3 );
+    }
+    if ( Gain == 0 )
+        printf( "Returning no gain.\n" );
+
+    return Gain;
+}
+
+/**function*************************************************************
+
+  synopsis    [Performs area minimization using a heuristic algorithm.]
+
+  description []
+               
+  sideeffects []
+
+  seealso     []
+
+***********************************************************************/
+void Fpga_MappingExplore( Fpga_Man_t * p )
+{
+    Fpga_Cut_t * pCutBest;
+    Fpga_Node_t * pNodeBest;
+    Fpga_NodeVec_t * vNodes;
+    float Area, Gain, CutArea1, CutArea2;
+    int i;
+
+    // compute the arrival times
+    Fpga_TimePropagateArrival( p );
+    p->fRequiredGlo = Fpga_TimeComputeArrivalMax( p );
+    Fpga_TimeComputeRequired( p, p->fRequiredGlo );
+
+    // assign the refs
+    Area = Fpga_MappingSetRefsAndArea( p );
+    // collect the nodes
+    vNodes = Fpga_MappingCollectRefed( p );
+    // find the best node to update
+    for ( i = 0; Gain = Fpga_FindBestNode(p, vNodes, &pNodeBest, &pCutBest); i++ )
+    {
+        // update the node
+        assert( pNodeBest->pCutBest != pCutBest );
+        // deref the current cut
+        CutArea1 = Fpga_CutDeref( p, pNodeBest, pNodeBest->pCutBest, 0 );
+        // ref the new cut
+        CutArea2 = Fpga_CutRef( p, pNodeBest, pCutBest, 0 );
+        assert( CutArea1 - CutArea2 == Gain );
+        printf( "Iteration %2d: Gain = %5.2f.\n", i, Gain );
+        // update the node
+        pNodeBest->pCutBest = pCutBest;
+        // collect new nodes
+        Fpga_NodeVecFree( vNodes );
+        vNodes = Fpga_MappingCollectRefed( p );
+        // compute the arrival and required times
+        Fpga_TimePropagateArrival( p );
+        Fpga_TimeComputeRequired( p, p->fRequiredGlo );
+    }
+
+
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/map/fpga/fpgaTime.c

@@ -182,6 +182,34 @@ void Fpga_TimePropagateRequired( Fpga_Man_t * p, Fpga_NodeVec_t * vNodes )
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the required times of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fpga_TimePropagateArrival( Fpga_Man_t * p )
+{
+    Fpga_Node_t * pNode;
+    Fpga_Cut_t * pCut;
+    int i;
+
+    // clean the required times and the fanout counts for all nodes
+    for ( i = 0; i < p->vAnds->nSize; i++ )
+    {
+        pNode = p->vAnds->pArray[i];
+        for ( pCut = pNode->pCuts->pNext; pCut; pCut = pCut->pNext )
+            pCut->tArrival = Fpga_TimeCutComputeArrival( p, pCut );
+    }
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/map/fpga/fpgaUtils.c

@@ -493,6 +493,32 @@ float Fpga_MappingSetRefsAndArea_rec( Fpga_Man_t * pMan, Fpga_Node_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Collect the referenced nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fpga_NodeVec_t * Fpga_MappingCollectRefed( Fpga_Man_t * pMan )
+{
+    Fpga_NodeVec_t * vNodes;
+    int i;
+    vNodes = Fpga_NodeVecAlloc( 100 );
+    for ( i = 0; i < pMan->vNodesAll->nSize; i++ )
+    {
+        if ( Fpga_NodeIsVar(pMan->vNodesAll->pArray[i]) )
+            continue;
+        if ( pMan->vNodesAll->pArray[i]->nRefs )
+            Fpga_NodeVecPush( vNodes, pMan->vNodesAll->pArray[i] );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the number of logic levels not counting PIs/POs.]
 
   Description []

src/map/mapper/mapper.h

@@ -82,6 +82,8 @@ extern Map_Node_t *    Map_ManReadConst1 ( Map_Man_t * p );
 extern Map_Time_t *    Map_ManReadInputArrivals( Map_Man_t * p );
 extern Mio_Library_t * Map_ManReadGenLib ( Map_Man_t * p );
 extern bool            Map_ManReadVerbose( Map_Man_t * p );
+extern float           Map_ManReadAreaFinal( Map_Man_t * p );
+extern float           Map_ManReadRequiredGlo( Map_Man_t * p );
 extern void            Map_ManSetTimeToMap( Map_Man_t * p, int Time );
 extern void            Map_ManSetTimeToNet( Map_Man_t * p, int Time );
 extern void            Map_ManSetTimeSweep( Map_Man_t * p, int Time );
@@ -125,6 +127,7 @@ extern Map_Node_t **   Map_CutReadLeaves( Map_Cut_t * p );
 extern unsigned        Map_CutReadPhaseBest( Map_Cut_t * p, int fPhase );
 extern unsigned        Map_CutReadPhase0( Map_Cut_t * p );
 extern unsigned        Map_CutReadPhase1( Map_Cut_t * p );
+extern Map_Cut_t *     Map_CutReadNext( Map_Cut_t * p );
 
 extern char *          Map_SuperReadFormula( Map_Super_t * p );
 extern Mio_Gate_t *    Map_SuperReadRoot( Map_Super_t * p );

src/map/mapper/mapperCore.c

@@ -82,8 +82,8 @@ int Map_Mapping( Map_Man_t * p )
     p->AreaBase = Map_MappingGetArea( p, p->vMapping );
 if ( p->fVerbose )
 {
-printf( "Delay    : FanViols = %5d  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
-                    0, Map_MappingGetAreaFlow(p), p->AreaBase, 0.0 );
+printf( "Delay    : Delay = %5.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
+                    p->fRequiredGlo, Map_MappingGetAreaFlow(p), p->AreaBase, 0.0 );
 PRT( "Time", p->timeMatch );
 }
     //////////////////////////////////////////////////////////////////////
@@ -103,8 +103,8 @@ PRT( "Time", p->timeMatch );
         p->AreaFinal = Map_MappingGetArea( p, p->vMapping );
 if ( p->fVerbose )
 {
-printf( "AreaFlow : FanViols = %5d  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
-                    0, Map_MappingGetAreaFlow(p), p->AreaFinal, 
+printf( "AreaFlow : Delay = %5.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
+                    p->fRequiredGlo, Map_MappingGetAreaFlow(p), p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
 PRT( "Time", clock() - clk );
 }
@@ -127,8 +127,8 @@ PRT( "Time", clock() - clk );
         p->AreaFinal = Map_MappingGetArea( p, p->vMapping );
 if ( p->fVerbose )
 {
-printf( "Area     : FanViols = %5d  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
-                    0, 0.0, p->AreaFinal, 
+printf( "Area     : Delay = %5.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
+                    p->fRequiredGlo, 0.0, p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
 PRT( "Time", clock() - clk );
 }
@@ -151,8 +151,8 @@ PRT( "Time", clock() - clk );
         p->AreaFinal = Map_MappingGetArea( p, p->vMapping );
 if ( p->fVerbose )
 {
-printf( "Area     : FanViols = %5d  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
-                    0, 0.0, p->AreaFinal, 
+printf( "Area     : Delay = %5.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
+                    p->fRequiredGlo, 0.0, p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
 PRT( "Time", clock() - clk );
 }

src/map/mapper/mapperCreate.c

@@ -52,6 +52,8 @@ Map_Node_t *    Map_ManReadConst1 ( Map_Man_t * p )                     { return
 Map_Time_t *    Map_ManReadInputArrivals( Map_Man_t * p )               { return p->pInputArrivals;}
 Mio_Library_t * Map_ManReadGenLib ( Map_Man_t * p )                     { return p->pSuperLib->pGenlib; }
 bool            Map_ManReadVerbose( Map_Man_t * p )                     { return p->fVerbose;   }
+float           Map_ManReadAreaFinal( Map_Man_t * p )                   { return p->AreaFinal;  }
+float           Map_ManReadRequiredGlo( Map_Man_t * p )                 { return p->fRequiredGlo;  }
 void            Map_ManSetTimeToMap( Map_Man_t * p, int Time )          { p->timeToMap = Time;  }
 void            Map_ManSetTimeToNet( Map_Man_t * p, int Time )          { p->timeToNet = Time;  }
 void            Map_ManSetTimeSweep( Map_Man_t * p, int Time )          { p->timeSweep = Time;  }
@@ -126,6 +128,7 @@ Map_Node_t **   Map_CutReadLeaves( Map_Cut_t * p )                { return p->pp
 unsigned        Map_CutReadPhaseBest( Map_Cut_t * p, int fPhase ) { return p->M[fPhase].uPhaseBest;}
 unsigned        Map_CutReadPhase0( Map_Cut_t * p )                { return p->M[0].uPhaseBest;}
 unsigned        Map_CutReadPhase1( Map_Cut_t * p )                { return p->M[1].uPhaseBest;}
+Map_Cut_t *     Map_CutReadNext( Map_Cut_t * p )                  { return p->pNext;          }
 
 /**Function*************************************************************
 
@@ -190,7 +193,8 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
     p->pSuperLib = Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame());
     p->nVarsMax  = p->pSuperLib->nVarsMax;
     p->fVerbose  = fVerbose;
-    p->fEpsilon  = (float)0.00001;
+//    p->fEpsilon  = (float)0.00001;
+    p->fEpsilon  = (float)0.001;
     assert( p->nVarsMax > 0 );
 
     // start various data structures
@@ -210,6 +214,7 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
     p->vMapping   = Map_NodeVecAlloc( 100 );
     p->vInside    = Map_NodeVecAlloc( 100 );
     p->vFanins    = Map_NodeVecAlloc( 100 );
+    p->vVisited   = Map_NodeVecAlloc( 100 );
 
     // create the PI nodes
     p->nInputs = nInputs;
@@ -253,6 +258,8 @@ void Map_ManFree( Map_Man_t * p )
         Map_NodeVecFree( p->vNodesTemp );
     if ( p->vMapping )    
         Map_NodeVecFree( p->vMapping );
+    if ( p->vVisited )    
+        Map_NodeVecFree( p->vVisited );
     Extra_MmFixedStop( p->mmNodes, 0 );
     Extra_MmFixedStop( p->mmCuts, 0 );
     FREE( p->pInputArrivals );

src/map/mapper/mapperCut.c

@@ -23,9 +23,9 @@
 ////////////////////////////////////////////////////////////////////////
 
 // the largest number of cuts considered
-#define  MAP_CUTS_MAX_COMPUTE   200
+#define  MAP_CUTS_MAX_COMPUTE   1000
 // the largest number of cuts used
-#define  MAP_CUTS_MAX_USE       50
+#define  MAP_CUTS_MAX_USE       250
 
 // temporary hash table to store the cuts
 typedef struct Map_CutTableStrutct_t Map_CutTable_t;
@@ -373,6 +373,14 @@ Map_Cut_t * Map_CutMergeLists( Map_Man_t * p, Map_CutTable_t * pTable,
             pTemp1 = ppArray1[i];
             pTemp2 = ppArray2[k];
 
+            if ( pTemp1->nLeaves == p->nVarsMax && pTemp2->nLeaves == p->nVarsMax )
+            {
+                if ( pTemp1->ppLeaves[0] != pTemp2->ppLeaves[0] )
+                    continue;
+                if ( pTemp1->ppLeaves[1] != pTemp2->ppLeaves[1] )
+                    continue;
+            }
+
             // check if k-feasible cut exists
             nNodes = Map_CutMergeTwo( pTemp1, pTemp2, ppNodes, p->nVarsMax );
             if ( nNodes == 0 )
@@ -397,6 +405,14 @@ Map_Cut_t * Map_CutMergeLists( Map_Man_t * p, Map_CutTable_t * pTable,
             pTemp1 = ppArray1[k];
             pTemp2 = ppArray2[i];
 
+            if ( pTemp1->nLeaves == p->nVarsMax && pTemp2->nLeaves == p->nVarsMax )
+            {
+                if ( pTemp1->ppLeaves[0] != pTemp2->ppLeaves[0] )
+                    continue;
+                if ( pTemp1->ppLeaves[1] != pTemp2->ppLeaves[1] )
+                    continue;
+            }
+
             // check if k-feasible cut exists
             nNodes = Map_CutMergeTwo( pTemp1, pTemp2, ppNodes, p->nVarsMax );
             if ( nNodes == 0 )
@@ -424,6 +440,14 @@ Map_Cut_t * Map_CutMergeLists( Map_Man_t * p, Map_CutTable_t * pTable,
             pTemp1 = ppArray1[k];
             pTemp2 = ppArray2[i];
 
+            if ( pTemp1->nLeaves == p->nVarsMax && pTemp2->nLeaves == p->nVarsMax )
+            {
+                if ( pTemp1->ppLeaves[0] != pTemp2->ppLeaves[0] )
+                    continue;
+                if ( pTemp1->ppLeaves[1] != pTemp2->ppLeaves[1] )
+                    continue;
+            }
+
             // check if k-feasible cut exists
             nNodes = Map_CutMergeTwo( pTemp1, pTemp2, ppNodes, p->nVarsMax );
             if ( nNodes == 0 )

src/map/mapper/mapperInt.h

@@ -121,6 +121,7 @@ struct Map_ManStruct_t_
     unsigned            uTruthsLarge[10][32]; // the elementary truth tables
     int                 nCounts[32];   // the counter of minterms
     int                 nCountsBest[32];// the counter of minterms
+    Map_NodeVec_t *     vVisited;      // the visited cuts during cut computation
 
     // simulation info from the FRAIG manager
     int                 nSimRounds;    // the number of words in the simulation info
@@ -262,13 +263,7 @@ struct Map_CutStruct_t_
     char                nVolume;       // the volume of this cut
     char                fMark;         // the mark to denote visited cut
     char                Phase;         // the mark to denote complemented cut
-//    float               fLevel;        // the average level of the fanins
-
-    unsigned            uTruthTemp[2]; // the temporary truth table used to derive other cuts
-    unsigned            uTruthZero[2]; // the temporary truth table used to derive other cuts
-    unsigned            uTruthDc[2];   // the don't-cares (SDCs) computed for this cut
-
-    Map_Match_t         M[2];          // the matches for the positive/negative phase
+    Map_Match_t         M[2];          // the matches for positive/negative phase
 };
 
 // the supergate internally represented

src/opt/fxu/fxu.c

+/**CFile****************************************************************
+
+  FileName    [fxu.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [The entrance into the fast extract module.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: fxu.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fxuInt.h" 
+//#include "mvc.h"
+#include "fxu.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+/*===== fxuCreate.c ====================================================*/
+extern Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData );
+extern void         Fxu_CreateCovers( Fxu_Matrix * p, Fxu_Data_t * pData );
+
+static int s_MemoryTotal;
+static int s_MemoryPeak;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast_extract on a set of covers.]
+
+  Description [All the covers are given in the array p->ppCovers. 
+  The resulting covers are returned in the array p->ppCoversNew.
+  The number of entries in both cover arrays is equal to the number
+  of all values in the current nodes plus the max expected number 
+  of extracted nodes (p->nValuesCi + p->nValuesInt + p->nValuesExtMax). 
+  The first p->nValuesCi entries, corresponding to the CI nodes, are NULL.
+  The next p->nValuesInt entries, corresponding to the int nodes, are covers
+  from which the divisors are extracted. The last p->nValuesExtMax entries  
+  are reserved for the new covers to be extracted. The number of extracted 
+  covers is returned. This number does not exceed the given number (p->nNodesExt). 
+  Two other things are important for the correct operation of this procedure:
+  (1) The input covers should be SCC-free. (2) The literal array (pCover->pLits) 
+  is allocated in each cover. The i-th entry in the literal array of a cover
+  is the number of the cover in the array p->ppCovers, which represents this
+  literal (variable value) in the given cover.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fxu_FastExtract( Fxu_Data_t * pData )
+{
+    Fxu_Matrix * p;
+    Fxu_Single * pSingle;
+    Fxu_Double * pDouble;
+    int Weight1, Weight2, Weight3;
+
+    s_MemoryTotal = 0;
+    s_MemoryPeak  = 0;
+
+    // create the matrix
+    p = Fxu_CreateMatrix( pData );
+    if ( p == NULL )
+        return -1;
+//    if ( pData->fVerbose )
+//        printf( "Memory usage after construction: Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
+//Fxu_MatrixPrint( NULL, p );
+
+    if ( pData->fOnlyS )
+    {
+        pData->nNodesNew = 0;
+        do
+        {
+            Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
+            if ( pData->fVerbose )
+                printf( "Best single = %3d.\n", Weight1 );
+            if ( Weight1 > 0 || Weight1 == 0 && pData->fUse0 )
+                Fxu_UpdateSingle( p );
+            else
+                break;
+        }
+        while ( ++pData->nNodesNew < pData->nNodesExt );
+    }
+    else if ( pData->fOnlyD )
+    {
+        pData->nNodesNew = 0;
+        do
+        {
+            Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
+            if ( pData->fVerbose )
+                printf( "Best double = %3d.\n", Weight2 );
+            if ( Weight2 > 0 || Weight2 == 0 && pData->fUse0 )
+                Fxu_UpdateDouble( p );
+            else
+                break;
+        }
+        while ( ++pData->nNodesNew < pData->nNodesExt );
+    }
+    else if ( !pData->fUseCompl )
+    {
+        pData->nNodesNew = 0;
+        do
+        {
+            Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
+            Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
+
+            if ( pData->fVerbose )
+                printf( "Best double = %3d. Best single = %3d.\n", Weight2, Weight1 );
+//Fxu_Select( p, &pSingle, &pDouble );
+
+            if ( Weight1 >= Weight2 )
+            {
+                if ( Weight1 > 0 || Weight1 == 0 && pData->fUse0 )
+                    Fxu_UpdateSingle( p );
+                else
+                    break;
+            }
+            else
+            {
+                if ( Weight2 > 0 || Weight2 == 0 && pData->fUse0 )
+                    Fxu_UpdateDouble( p );
+                else
+                    break;
+            }
+        }
+        while ( ++pData->nNodesNew < pData->nNodesExt );
+    }
+    else
+    { // use the complement
+        pData->nNodesNew = 0;
+        do
+        {
+            Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
+            Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
+
+            // select the best single and double
+            Weight3 = Fxu_Select( p, &pSingle, &pDouble );
+            if ( pData->fVerbose )
+                printf( "Best double = %3d. Best single = %3d. Best complement = %3d.\n", 
+                    Weight2, Weight1, Weight3 );
+
+            if ( Weight3 > 0 || Weight3 == 0 && pData->fUse0 )
+                Fxu_Update( p, pSingle, pDouble );
+            else
+                break;
+        }
+        while ( ++pData->nNodesNew < pData->nNodesExt );
+    }
+
+    if ( pData->fVerbose )
+        printf( "Total single = %3d. Total double = %3d. Total compl = %3d.\n", p->nDivs1, p->nDivs2, p->nDivs3 );
+
+    // create the new covers
+    if ( pData->nNodesNew )
+        Fxu_CreateCovers( p, pData );
+    Fxu_MatrixDelete( p );
+//    printf( "Memory usage after delocation:   Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
+    if ( pData->nNodesNew == pData->nNodesExt )
+        printf( "Warning: The limit on the number of extracted divisors has been reached.\n" );
+    return pData->nNodesNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the cubes in the ring.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxu_MatrixRingCubesUnmark( Fxu_Matrix * p )
+{
+    Fxu_Cube * pCube, * pCube2;
+    // unmark the cubes
+    Fxu_MatrixForEachCubeInRingSafe( p, pCube, pCube2 )
+        pCube->pOrder = NULL;
+    Fxu_MatrixRingCubesReset( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the vars in the ring.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxu_MatrixRingVarsUnmark( Fxu_Matrix * p )
+{
+    Fxu_Var * pVar, * pVar2;
+    // unmark the vars
+    Fxu_MatrixForEachVarInRingSafe( p, pVar, pVar2 )
+        pVar->pOrder = NULL;
+    Fxu_MatrixRingVarsReset( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Fxu_MemFetch( Fxu_Matrix * p, int nBytes )
+{
+    s_MemoryTotal += nBytes;
+    if ( s_MemoryPeak < s_MemoryTotal )
+        s_MemoryPeak = s_MemoryTotal;
+//    return malloc( nBytes );
+    return Extra_MmFixedEntryFetch( p->pMemMan );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxu_MemRecycle( Fxu_Matrix * p, char * pItem, int nBytes )
+{
+    s_MemoryTotal -= nBytes;
+//    free( pItem );
+    Extra_MmFixedEntryRecycle( p->pMemMan, pItem );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/fxu/fxu.h

+/**CFile****************************************************************
+
+  FileName    [fxu.h]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [External declarations of fast extract for unate covers.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: fxu.h,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __FXU_H__
+#define __FXU_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+#ifndef bool
+#define bool int
+#endif
+
+typedef struct FxuDataStruct   Fxu_Data_t;
+
+// structure for the FX input/output data 
+struct FxuDataStruct
+{
+    // user specified parameters
+    bool              fOnlyS;           // set to 1 to have only single-cube divs
+    bool              fOnlyD;           // set to 1 to have only double-cube divs
+    bool              fUse0;            // set to 1 to have 0-weight also extracted
+    bool              fUseCompl;        // set to 1 to have complement taken into account
+    bool              fVerbose;         // set to 1 to have verbose output
+    int               nPairsMax;        // the maximum number of cube pairs to consider
+/*
+    // parameters of the network
+    int               fMvNetwork;       // the network has some MV nodes
+    // the information about nodes
+    int               nNodesCi;         // the number of CI nodes of the network
+    int               nNodesInt;        // the number of internal nodes of the network
+    int               nNodesOld;        // the number of CI and int nodes
+    int               nNodesNew;        // the number of added nodes
+    int               nNodesExt;        // the max number of (binary) nodes to be added by FX
+    int               nNodesAlloc;      // the total number of all nodes
+    int *             pNode2Value;      // for each node, the number of its first value
+    // the information about values
+    int               nValuesCi;        // the total number of values of CI nodes
+    int               nValuesInt;       // the total number of values of int nodes
+    int               nValuesOld;       // the number of CI and int values
+    int               nValuesNew;       // the number of values added nodes
+    int               nValuesExt;       // the total number of values of the added nodes
+    int               nValuesAlloc;     // the total number of all values of all nodes
+    int *             pValue2Node;      // for each value, the number of its node
+    // the information about covers
+    Mvc_Cover_t **    ppCovers;         // for each value, the corresponding cover
+    Mvc_Cover_t **    ppCoversNew;      // for each value, the corresponding cover after FX
+    // the MVC manager
+    Mvc_Manager_t *   pManMvc;
+*/
+    // statistics   
+    int               nNodesOld;        // the old number of nodes
+    int               nNodesExt;        // the number of divisors to extract
+    int               nNodesNew;        // the number of divisors extracted
+
+    // the input information
+    Vec_Ptr_t *       vSops;            // the SOPs for each node in the network
+    Vec_Ptr_t *       vFanins;          // the fanins of each node in the network
+    // output information
+    Vec_Ptr_t *       vSopsNew;         // the SOPs for each node in the network after extraction
+    Vec_Ptr_t *       vFaninsNew;       // the fanins of each node in the network after extraction
+    // the SOP manager
+    Extra_MmFlex_t *  pManSop;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFITIONS                            ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/*===== fxu.c ==========================================================*/
+extern int          Fxu_FastExtract( Fxu_Data_t * pData );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+

src/opt/fxu/fxuPrint.c

+/**CFile****************************************************************
+
+  FileName    [fxuPrint.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Various printing procedures.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: fxuPrint.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fxuInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxu_MatrixPrint( FILE * pFile, Fxu_Matrix * p )
+{
+    Fxu_Var * pVar;
+    Fxu_Cube * pCube;
+    Fxu_Double * pDiv;
+    Fxu_Single * pSingle;
+    Fxu_Lit * pLit;
+    Fxu_Pair * pPair;
+    int i, LastNum;
+    int fStdout;
+
+    fStdout = 1;
+    if ( pFile == NULL )
+    {
+        pFile = fopen( "matrix.txt", "w" );
+        fStdout = 0;
+    }
+
+    fprintf( pFile, "Matrix has %d vars, %d cubes, %d literals, %d divisors.\n", 
+        p->lVars.nItems, p->lCubes.nItems, p->nEntries, p->nDivs );
+    fprintf( pFile, "Divisors selected so far: single = %d, double = %d.\n", 
+        p->nDivs1, p->nDivs2 );
+    fprintf( pFile, "\n" );
+
+    // print the numbers on top of the matrix
+    for ( i = 0; i < 12; i++ )
+        fprintf( pFile, " " );
+    Fxu_MatrixForEachVariable( p, pVar )
+        fprintf( pFile, "%d", pVar->iVar % 10 );
+    fprintf( pFile, "\n" );
+
+    // print the rows
+    Fxu_MatrixForEachCube( p, pCube )
+    {
+        fprintf( pFile, "%4d", pCube->iCube );
+        fprintf( pFile, "  " );
+        fprintf( pFile, "%4d", pCube->pVar->iVar );
+        fprintf( pFile, "  " );
+
+        // print the literals
+        LastNum = -1;
+        Fxu_CubeForEachLiteral( pCube, pLit )
+        {
+            for ( i = LastNum + 1; i < pLit->pVar->iVar; i++ )
+                fprintf( pFile, "." );
+            fprintf( pFile, "1" );
+            LastNum = i;
+        }
+        for ( i = LastNum + 1; i < p->lVars.nItems; i++ )
+            fprintf( pFile, "." );
+        fprintf( pFile, "\n" );
+    }
+    fprintf( pFile, "\n" );
+
+    // print the double-cube divisors
+    fprintf( pFile, "The double divisors are:\n" );
+    Fxu_MatrixForEachDouble( p, pDiv, i )
+    {
+        fprintf( pFile, "Divisor #%3d (lit=%d,%d) (w=%2d):  ", 
+            pDiv->Num, pDiv->lPairs.pHead->nLits1, 
+            pDiv->lPairs.pHead->nLits2, pDiv->Weight );
+        Fxu_DoubleForEachPair( pDiv, pPair )
+            fprintf( pFile, " <%d, %d> (b=%d)", 
+                pPair->pCube1->iCube, pPair->pCube2->iCube, pPair->nBase );
+        fprintf( pFile, "\n" );
+    }
+    fprintf( pFile, "\n" );
+
+    // print the divisors associated with each cube
+    fprintf( pFile, "The cubes are:\n" );
+    Fxu_MatrixForEachCube( p, pCube )
+    {
+        fprintf( pFile, "Cube #%3d: ", pCube->iCube );
+        if ( pCube->pVar->ppPairs )
+            Fxu_CubeForEachPair( pCube, pPair, i )
+                fprintf( pFile, " <%d %d> (d=%d) (b=%d)", 
+                    pPair->iCube1, pPair->iCube2, pPair->pDiv->Num, pPair->nBase );
+        fprintf( pFile, "\n" );
+    }
+    fprintf( pFile, "\n" );
+
+    // print the single-cube divisors
+    fprintf( pFile, "The single divisors are:\n" );
+    Fxu_MatrixForEachSingle( p, pSingle )
+    {
+        fprintf( pFile, "Single-cube divisor #%5d: Var1 = %4d. Var2 = %4d. Weight = %2d\n", 
+            pSingle->Num, pSingle->pVar1->iVar, pSingle->pVar2->iVar, pSingle->Weight );
+    }
+    fprintf( pFile, "\n" );
+
+/*
+    {
+        int Index;
+        fprintf( pFile, "Distribution of divisors in the hash table:\n" );
+        for ( Index = 0; Index < p->nTableSize; Index++ )
+            fprintf( pFile, " %d", p->pTable[Index].nItems );
+        fprintf( pFile, "\n" );
+    }
+*/
+    if ( !fStdout )
+        fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxu_MatrixPrintDivisorProfile( FILE * pFile, Fxu_Matrix * p )
+{
+    Fxu_Double * pDiv;
+    int WeightMax;
+    int * pProfile;
+    int Counter1; // the number of -1 weight
+    int CounterL; // the number of less than -1 weight
+    int i;
+
+    WeightMax = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
+    pProfile = ALLOC( int, (WeightMax + 1) );
+    memset( pProfile, 0, sizeof(int) * (WeightMax + 1) );
+
+    Counter1 = 0;
+    CounterL = 0;
+    Fxu_MatrixForEachDouble( p, pDiv, i )
+    {
+        assert( pDiv->Weight <= WeightMax );
+        if ( pDiv->Weight == -1 )
+            Counter1++;
+        else if ( pDiv->Weight < 0 )
+            CounterL++;
+        else
+            pProfile[ pDiv->Weight ]++;
+    }
+
+    fprintf( pFile, "The double divisors profile:\n" );
+    fprintf( pFile, "Weight  < -1 divisors = %6d\n", CounterL );
+    fprintf( pFile, "Weight    -1 divisors = %6d\n", Counter1 );
+    for ( i = 0; i <= WeightMax; i++ )
+        if ( pProfile[i] )
+            fprintf( pFile, "Weight   %3d divisors = %6d\n", i, pProfile[i] );
+    fprintf( pFile, "End of divisor profile printout\n" );
+    FREE( pProfile );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/fxu/fxuReduce.c

+/**CFile****************************************************************
+
+  FileName    [fxuReduce.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Procedures to reduce the number of considered cube pairs.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: fxuReduce.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fxuInt.h"
+#include "fxu.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int Fxu_CountPairDiffs( char * pCover, unsigned char pDiffs[] );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Precomputes the pairs to use for creating two-cube divisors.]
+
+  Description [This procedure takes the matrix with variables and cubes 
+  allocated (p), the original covers of the nodes (i-sets) and their number 
+  (ppCovers,nCovers). The maximum number of pairs to compute and the total 
+  number of pairs in existence. This procedure adds to the storage of
+  divisors exactly the given number of pairs (nPairsMax) while taking
+  first those pairs that have the smallest number of literals in their
+  cube-free form.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax )
+{
+    unsigned char * pnLitsDiff;   // storage for the counters of diff literals
+    int * pnPairCounters;         // the counters of pairs for each number of diff literals
+    Fxu_Cube * pCubeFirst, * pCubeLast;
+    Fxu_Cube * pCube1, * pCube2;
+    Fxu_Var * pVar;
+    int nCubes, nBitsMax, nSum;
+    int CutOffNum, CutOffQuant;
+    int iPair, iQuant, k, c;
+    int clk = clock();
+    char * pSopCover;
+    int nFanins;
+
+    assert( nPairsMax < nPairsTotal );
+
+    // allocate storage for counter of diffs
+    pnLitsDiff = ALLOC( unsigned char, nPairsTotal );
+    // go through the covers and precompute the distances between the pairs
+    iPair    =  0;
+    nBitsMax = -1;
+    for ( c = 0; c < vCovers->nSize; c++ )
+        if ( pSopCover = vCovers->pArray[c] )
+        {
+            nFanins = Abc_SopGetVarNum(pSopCover);
+            // precompute the differences
+            Fxu_CountPairDiffs( pSopCover, pnLitsDiff + iPair );
+            // update the counter
+            nCubes = Abc_SopGetCubeNum( pSopCover );
+            iPair += nCubes * (nCubes - 1) / 2;
+            if ( nBitsMax < nFanins )
+                nBitsMax = nFanins;
+        }
+    assert( iPair == nPairsTotal );
+
+    // allocate storage for counters of cube pairs by difference
+    pnPairCounters = ALLOC( int, 2 * nBitsMax );
+    memset( pnPairCounters, 0, sizeof(int) * 2 * nBitsMax );
+    // count the number of different pairs
+    for ( k = 0; k < nPairsTotal; k++ )
+        pnPairCounters[ pnLitsDiff[k] ]++;
+    // determine what pairs to take starting from the lower
+    // so that there would be exactly pPairsMax pairs
+    assert( pnPairCounters[0] == 0 ); // otherwise, covers are not dup-free
+    assert( pnPairCounters[1] == 0 ); // otherwise, covers are not SCC-free
+    nSum = 0;
+    for ( k = 0; k < 2 * nBitsMax; k++ )
+    {
+        nSum += pnPairCounters[k];
+        if ( nSum >= nPairsMax )
+        {
+            CutOffNum   = k;
+            CutOffQuant = pnPairCounters[k] - (nSum - nPairsMax);
+            break;
+        }
+    }
+    FREE( pnPairCounters );
+
+    // set to 0 all the pairs above the cut-off number and quantity
+    iQuant = 0;
+    iPair  = 0;
+    for ( k = 0; k < nPairsTotal; k++ )
+        if ( pnLitsDiff[k] > CutOffNum ) 
+            pnLitsDiff[k] = 0;
+        else if ( pnLitsDiff[k] == CutOffNum )
+        {
+            if ( iQuant++ >= CutOffQuant )
+                pnLitsDiff[k] = 0;
+            else
+                iPair++;
+        }
+        else
+            iPair++;
+    assert( iPair == nPairsMax );
+
+    // collect the corresponding pairs and add the divisors
+    iPair = 0;
+    for ( c = 0; c < vCovers->nSize; c++ )
+        if ( pSopCover = vCovers->pArray[c] )
+        {
+            // get the var
+            pVar = p->ppVars[2*c+1];
+            // get the first cube
+            pCubeFirst = pVar->pFirst;
+            // get the last cube
+            pCubeLast = pCubeFirst;
+            for ( k = 0; k < pVar->nCubes; k++ )
+                pCubeLast = pCubeLast->pNext;
+            assert( pCubeLast == NULL || pCubeLast->pVar != pVar );
+
+            // go through the cube pairs
+            for ( pCube1 = pCubeFirst; pCube1 != pCubeLast; pCube1 = pCube1->pNext )
+                for ( pCube2 = pCube1->pNext; pCube2 != pCubeLast; pCube2 = pCube2->pNext )
+                    if ( pnLitsDiff[iPair++] )
+                    {   // create the divisors for this pair
+                        Fxu_MatrixAddDivisor( p, pCube1, pCube2 );
+                    }
+        }
+    assert( iPair == nPairsTotal );
+    FREE( pnLitsDiff );
+//PRT( "Preprocess", clock() - clk );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the differences in each cube pair in the cover.]
+
+  Description [Takes the cover (pCover) and the array where the
+  diff counters go (pDiffs). The array pDiffs should have as many
+  entries as there are different pairs of cubes in the cover: n(n-1)/2.
+  Fills out the array pDiffs with the following info: For each cube
+  pair, included in the array is the number of literals in both cubes
+  after they are made cube free.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fxu_CountPairDiffs( char * pCover, unsigned char pDiffs[] )
+{
+    char * pCube1, * pCube2;
+    int nOnes, nCubePairs, nFanins, v;
+    nCubePairs = 0;
+    nFanins = Abc_SopGetVarNum(pCover);
+    Abc_SopForEachCube( pCover, nFanins, pCube1 )
+    Abc_SopForEachCube( pCube1, nFanins, pCube2 )
+    {
+        if ( pCube1 == pCube2 )
+            continue;
+        nOnes = 0;
+        for ( v = 0; v < nFanins; v++ )
+            nOnes += (pCube1[v] != pCube2[v]);
+        pDiffs[nCubePairs++] = nOnes;
+    }
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/fxu/fxuSingle.c

+/**CFile****************************************************************
+
+  FileName    [fxuSingle.c]
+
+  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+  Synopsis    [Procedures to compute the set of single-cube divisors.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: fxuSingle.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fxuInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes and adds all single-cube divisors to storage.]
+
+  Description [This procedure should be called once when the matrix is
+  already contructed before the process of logic extraction begins..]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxu_MatrixComputeSingles( Fxu_Matrix * p )
+{
+    Fxu_Var * pVar;
+    // iterate through the columns in the matrix
+    Fxu_MatrixForEachVariable( p, pVar )
+        Fxu_MatrixComputeSinglesOne( p, pVar );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the single-cube divisors associated with a new column.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
+{
+//    int * pValue2Node = p->pValue2Node;
+    Fxu_Lit * pLitV, * pLitH;
+    Fxu_Var * pVar2;
+    int Coin;
+//    int CounterAll;
+//    int CounterTest;
+    int WeightCur;
+
+    // start collecting the affected vars
+    Fxu_MatrixRingVarsStart( p );
+    // go through all the literals of this variable
+    for ( pLitV = pVar->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
+        // for this literal, go through all the horizontal literals
+        for ( pLitH = pLitV->pHPrev; pLitH; pLitH = pLitH->pHPrev )
+        {
+            // get another variable
+            pVar2 = pLitH->pVar;
+//            CounterAll++;
+            // skip the var if it is already used
+            if ( pVar2->pOrder )
+                continue;
+            // skip the var if it belongs to the same node
+//            if ( pValue2Node[pVar->iVar] == pValue2Node[pVar2->iVar] )
+//                continue;
+            // collect the var
+            Fxu_MatrixRingVarsAdd( p, pVar2 );
+        }
+    // stop collecting the selected vars
+    Fxu_MatrixRingVarsStop( p );
+
+    // iterate through the selected vars
+    Fxu_MatrixForEachVarInRing( p, pVar2 )
+    {
+//        CounterTest++;
+        // count the coincidence
+        Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
+        assert( Coin > 0 );
+        // get the new weight
+        WeightCur = Coin - 2;
+        if ( WeightCur >= 0 )
+            Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
+    }
+
+    // unmark the vars
+    Fxu_MatrixRingVarsUnmark( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the coincidence count of two columns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fxu_SingleCountCoincidence( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2 )
+{
+    Fxu_Lit * pLit1, * pLit2;
+    int Result;
+
+    // compute the coincidence count
+    Result = 0;
+    pLit1  = pVar1->lLits.pHead;
+    pLit2  = pVar2->lLits.pHead;
+    while ( 1 )
+    {
+        if ( pLit1 && pLit2 )
+        {
+            if ( pLit1->pCube->pVar->iVar == pLit2->pCube->pVar->iVar )
+            { // the variables are the same
+                if ( pLit1->iCube == pLit2->iCube )
+                { // the literals are the same
+                    pLit1 = pLit1->pVNext;
+                    pLit2 = pLit2->pVNext;
+                    // add this literal to the coincidence
+                    Result++;
+                }
+                else if ( pLit1->iCube < pLit2->iCube )
+                    pLit1 = pLit1->pVNext;
+                else
+                    pLit2 = pLit2->pVNext;
+            }
+            else if ( pLit1->pCube->pVar->iVar < pLit2->pCube->pVar->iVar )
+                pLit1 = pLit1->pVNext;
+            else
+                pLit2 = pLit2->pVNext;
+        }
+        else if ( pLit1 && !pLit2 )
+            pLit1 = pLit1->pVNext;
+        else if ( !pLit1 && pLit2 )
+            pLit2 = pLit2->pVNext;
+        else
+            break;
+    }
+    return Result;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/fxu/module.make

+SRC +=  fxu.c \
+    fxuCreate.c \
+    fxuHeapD.c \
+    fxuHeapS.c \
+    fxuList.c \
+    fxuMatrix.c \
+    fxuPair.c \
+    fxuPrint.c \
+    fxuReduce.c \
+    fxuSelect.c \
+    fxuSingle.c \
+    fxuUpdate.c