Version abc60614

1 files changed, 786 insertions, 0 deletions

diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c
new file mode 100644
index 00000000..165d84c5
--- /dev/null
+++ b/src/base/abci/abcLut.c
@@ -0,0 +1,786 @@
+/**CFile****************************************************************
+
+  FileName    [abcLut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Superchoicing for K-LUTs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcLut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "cut.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define SCL_LUT_MAX          6   // the maximum LUT size
+#define SCL_VARS_MAX        15   // the maximum number of variables
+#define SCL_NODE_MAX      1000   // the maximum number of nodes
+
+typedef struct Abc_ManScl_t_ Abc_ManScl_t;
+struct Abc_ManScl_t_
+{
+    // paramers
+    int                nLutSize;    // the LUT size
+    int                nCutSizeMax; // the max number of leaves of the cone
+    int                nNodesMax;   // the max number of divisors in the cone
+    int                nWords;      // the number of machine words in sim info
+    // structural representation of the cone
+    Vec_Ptr_t *        vLeaves;     // leaves of the cut
+    Vec_Ptr_t *        vVolume;     // volume of the cut
+    int                pBSet[SCL_VARS_MAX]; // bound set
+    // functional representation of the cone
+    unsigned *         uTruth;      // truth table of the cone
+    // representation of truth tables
+    unsigned **        uVars;       // elementary truth tables
+    unsigned **        uSims;       // truth tables of the nodes
+    unsigned **        uCofs;       // truth tables of the cofactors
+};
+
+static Vec_Ptr_t * s_pLeaves = NULL;
+
+static Cut_Man_t * Abc_NtkStartCutManForScl( Abc_Ntk_t * pNtk, int nLutSize );
+static Abc_ManScl_t * Abc_ManSclStart( int nLutSize, int nCutSizeMax, int nNodesMax );
+static void Abc_ManSclStop( Abc_ManScl_t * p );
+static void Abc_NodeLutMap( Cut_Man_t * pManCuts, Abc_Obj_t * pObj );
+
+static Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * pManScl, Abc_Obj_t * pObj );
+static int Abc_NodeDecomposeStep( Abc_ManScl_t * pManScl );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for K-LUTs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int fVerbose )
+{
+    ProgressBar * pProgress;
+    Abc_ManCut_t * pManCut;
+    Abc_ManScl_t * pManScl;
+    Cut_Man_t * pManCuts;
+    Abc_Obj_t * pObj, * pFanin, * pObjTop;
+    int i, LevelMax, nNodes;
+    int nNodesTried, nNodesDec, nNodesExist, nNodesUsed;
+
+    assert( Abc_NtkIsSopLogic(pNtk) );
+    if ( nLutSize < 3 || nLutSize > SCL_LUT_MAX )
+    {
+        printf( "LUT size (%d) does not belong to the interval: 3 <= LUT size <= %d\n", nLutSize, SCL_LUT_MAX );
+        return 0;
+    }
+    if ( nCutSizeMax <= nLutSize || nCutSizeMax > SCL_VARS_MAX )
+    {
+        printf( "Cut size (%d) does not belong to the interval: LUT size (%d) < Cut size <= %d\n", nCutSizeMax, nLutSize, SCL_VARS_MAX );
+        return 0;
+    }
+
+    assert( nLutSize <= SCL_LUT_MAX );
+    assert( nCutSizeMax <= SCL_VARS_MAX );
+    nNodesTried = nNodesDec = nNodesExist = nNodesUsed = 0;
+
+    // set the delays of the CIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->Level = 0;
+
+//Abc_NtkGetLevelNum( pNtk );
+ 
+    // start the managers
+    pManScl = Abc_ManSclStart( nLutSize, nCutSizeMax, 1000 );
+    pManCuts = Abc_NtkStartCutManForScl( pNtk, nLutSize );
+    pManCut = Abc_NtkManCutStart( nCutSizeMax, 100000, 100000, 100000 );
+    s_pLeaves = Abc_NtkManCutReadCutSmall( pManCut );
+    pManScl->vVolume = Abc_NtkManCutReadVisited( pManCut );
+
+    // process each internal node (assuming topological order of nodes!!!)
+    nNodes = Abc_NtkObjNumMax(pNtk);
+    pProgress = Extra_ProgressBarStart( stdout, nNodes );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+//        if ( i != nNodes-1 )
+//            continue;
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( i >= nNodes )
+            break;
+        if ( Abc_ObjFaninNum(pObj) != 2 )
+            continue;
+        nNodesTried++;
+
+        // map this node using regular cuts
+//        pObj->Level = 0;
+        Abc_NodeLutMap( pManCuts, pObj );
+        // compute the cut
+        pManScl->vLeaves = Abc_NodeFindCut( pManCut, pObj, 0 );
+        if ( Vec_PtrSize(pManScl->vLeaves) <= nLutSize )
+            continue;
+        // get the volume of the cut
+        if ( Vec_PtrSize(pManScl->vVolume) > SCL_NODE_MAX )
+            continue;
+        nNodesDec++;
+
+        // decompose the cut
+        pObjTop = Abc_NodeSuperChoiceLut( pManScl, pObj );
+        if ( pObjTop == NULL )
+            continue;
+        nNodesExist++;
+
+        // if there is no delay improvement, skip; otherwise, update level
+        if ( pObjTop->Level >= pObj->Level )
+        {
+            Abc_NtkDeleteObj_rec( pObjTop );
+            continue;
+        }
+        pObj->Level = pObjTop->Level;
+        nNodesUsed++;
+    }
+    Extra_ProgressBarStop( pProgress );
+
+    // delete the managers
+    Abc_ManSclStop( pManScl );
+    Abc_NtkManCutStop( pManCut );
+    Cut_ManStop( pManCuts );
+
+    // get the largest arrival time
+    LevelMax = 0;
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0( pObj );
+        // skip inv/buf
+        if ( Abc_ObjFaninNum(pFanin) == 1 )
+            pFanin = Abc_ObjFanin0( pFanin );
+        // get the new level
+        LevelMax = ABC_MAX( LevelMax, (int)pFanin->Level );
+    }
+
+    if ( fVerbose )
+    printf( "Try = %d. Dec = %d. Exist = %d. Use = %d. SUPER = %d levels of %d-LUTs.\n", 
+        nNodesTried, nNodesDec, nNodesExist, nNodesUsed, LevelMax, nLutSize );
+//    if ( fVerbose )
+//    printf( "The network is superchoiced for %d levels of %d-LUTs.\n", LevelMax, nLutSize );
+
+    // clean the data field
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pNext = NULL;
+
+    // check
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkSuperChoiceLut: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs LUT mapping of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeLutMap( Cut_Man_t * pManCuts, Abc_Obj_t * pObj )
+{
+    Cut_Cut_t * pCut;
+    Abc_Obj_t * pFanin;
+    int i, DelayMax;
+    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCuts, pObj, 0, 0 );
+    assert( pCut != NULL );
+    assert( pObj->Level == 0 );
+    // go through the cuts
+    pObj->Level = ABC_INFINITY;
+    for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )
+    {
+        DelayMax = 0;
+        for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        {
+            pFanin = Abc_NtkObj( pObj->pNtk, pCut->pLeaves[i] );
+//            assert( Abc_ObjIsCi(pFanin) || pFanin->Level > 0 ); // should hold if node ordering is topological
+            if ( DelayMax < (int)pFanin->Level )
+                DelayMax = pFanin->Level;
+        }
+        if ( (int)pObj->Level > DelayMax )
+            pObj->Level = DelayMax;
+    }
+    assert( pObj->Level < ABC_INFINITY );
+    pObj->Level++;
+//    printf( "%d(%d) ", pObj->Id, pObj->Level );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the cut manager for rewriting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkStartCutManForScl( Abc_Ntk_t * pNtk, int nLutSize )
+{
+    static Cut_Params_t Params, * pParams = &Params;
+    Cut_Man_t * pManCut;
+    Abc_Obj_t * pObj;
+    int i;
+    // start the cut manager
+    memset( pParams, 0, sizeof(Cut_Params_t) );
+    pParams->nVarsMax  = nLutSize; // the max cut size ("k" of the k-feasible cuts)
+    pParams->nKeepMax  = 500;   // the max number of cuts kept at a node
+    pParams->fTruth    = 0;     // compute truth tables
+    pParams->fFilter   = 1;     // filter dominated cuts
+    pParams->fSeq      = 0;     // compute sequential cuts
+    pParams->fDrop     = 0;     // drop cuts on the fly
+    pParams->fVerbose  = 0;     // the verbosiness flag
+    pParams->nIdsMax   = Abc_NtkObjNumMax( pNtk );
+    pManCut = Cut_ManStart( pParams );
+    if ( pParams->fDrop )
+        Cut_ManSetFanoutCounts( pManCut, Abc_NtkFanoutCounts(pNtk) );
+    // set cuts for PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+            Cut_NodeSetTriv( pManCut, pObj->Id );
+    return pManCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_ManScl_t * Abc_ManSclStart( int nLutSize, int nCutSizeMax, int nNodesMax )
+{
+    Abc_ManScl_t * p;
+    int i, k;
+    assert( sizeof(unsigned) == 4 );
+    p = ALLOC( Abc_ManScl_t, 1 );
+    memset( p, 0, sizeof(Abc_ManScl_t) );
+    p->nLutSize    = nLutSize;
+    p->nCutSizeMax = nCutSizeMax;
+    p->nNodesMax   = nNodesMax;
+    p->nWords      = Extra_TruthWordNum(nCutSizeMax);
+    // allocate simulation info
+    p->uVars = (unsigned **)Extra_ArrayAlloc( nCutSizeMax, p->nWords, 4 );
+    p->uSims = (unsigned **)Extra_ArrayAlloc( nNodesMax, p->nWords, 4 );
+    p->uCofs = (unsigned **)Extra_ArrayAlloc( 2 << nLutSize, p->nWords, 4 );
+    memset( p->uVars[0], 0, nCutSizeMax * p->nWords * 4 );
+    // assign elementary truth tables
+    for ( k = 0; k < p->nCutSizeMax; k++ )
+        for ( i = 0; i < p->nWords * 32; i++ )
+            if ( i & (1 << k) )
+                p->uVars[k][i>>5] |= (1 << (i&31));
+    // other data structures
+//    p->vBound = Vec_IntAlloc( nCutSizeMax );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ManSclStop( Abc_ManScl_t * p )
+{
+//    Vec_IntFree( p->vBound );
+    free( p->uVars );
+    free( p->uSims );
+    free( p->uCofs );
+    free( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Abc_NodeSuperChoiceTruth( Abc_ManScl_t * pManScl )
+{
+    Abc_Obj_t * pObj;
+    unsigned * puData0, * puData1, * puData;
+    char * pSop;
+    int i, k;
+    // set elementary truth tables
+    Vec_PtrForEachEntry( pManScl->vLeaves, pObj, i )
+        pObj->pNext = (Abc_Obj_t *)pManScl->uVars[i];
+    // compute truth tables for internal nodes
+    Vec_PtrForEachEntry( pManScl->vVolume, pObj, i )
+    {
+        // set storage for the node's simulation info
+        pObj->pNext = (Abc_Obj_t *)pManScl->uSims[i];
+        // get pointer to the simulation info
+        puData  = (unsigned *)pObj->pNext;
+        puData0 = (unsigned *)Abc_ObjFanin0(pObj)->pNext;
+        puData1 = (unsigned *)Abc_ObjFanin1(pObj)->pNext;
+        // simulate
+        pSop = pObj->pData;
+        if ( pSop[0] == '0' && pSop[1] == '0' )
+            for ( k = 0; k < pManScl->nWords; k++ )
+                puData[k] = ~puData0[k] & ~puData1[k];
+        else if ( pSop[0] == '0' )
+            for ( k = 0; k < pManScl->nWords; k++ )
+                puData[k] = ~puData0[k] & puData1[k];
+        else if ( pSop[1] == '0' )
+            for ( k = 0; k < pManScl->nWords; k++ )
+                puData[k] = puData0[k] & ~puData1[k];
+        else 
+            for ( k = 0; k < pManScl->nWords; k++ )
+                puData[k] = puData0[k] & puData1[k];
+    }
+    return puData;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect2_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vVolume )
+{
+    if ( pObj->fMarkC )
+        return;
+    pObj->fMarkC = 1;
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    Abc_NodeSuperChoiceCollect2_rec( Abc_ObjFanin0(pObj), vVolume );
+    Abc_NodeSuperChoiceCollect2_rec( Abc_ObjFanin1(pObj), vVolume );
+    Vec_PtrPush( vVolume, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect2( Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkC = 1;
+    Vec_PtrClear( vVolume );
+    Abc_NodeSuperChoiceCollect2_rec( pRoot, vVolume );
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkC = 0;
+    Vec_PtrForEachEntry( vVolume, pObj, i )
+        pObj->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume )
+{
+    if ( pObj->fMarkB )
+    {
+        Vec_PtrPush( vLeaves, pObj );
+        pObj->fMarkB = 0;
+    }
+    if ( pObj->fMarkC )
+        return;
+    pObj->fMarkC = 1;
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    Abc_NodeSuperChoiceCollect_rec( Abc_ObjFanin0(pObj), vLeaves, vVolume );
+    Abc_NodeSuperChoiceCollect_rec( Abc_ObjFanin1(pObj), vLeaves, vVolume );
+    Vec_PtrPush( vVolume, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description [Orders the leaves topologically.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect( Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume )
+{
+    Abc_Obj_t * pObj;
+    int i, nLeaves;
+    nLeaves = Vec_PtrSize(vLeaves);
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkB = pObj->fMarkC = 1;
+    Vec_PtrClear( vVolume );
+    Vec_PtrClear( vLeaves );
+    Abc_NodeSuperChoiceCollect_rec( pRoot, vLeaves, vVolume );
+    assert( Vec_PtrSize(vLeaves) == nLeaves );
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkC = 0;
+    Vec_PtrForEachEntry( vVolume, pObj, i )
+        pObj->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeLeavesRemove( Vec_Ptr_t * vLeaves, unsigned uPhase, int nVars )
+{
+    int i;
+    for ( i = nVars - 1; i >= 0; i-- )
+        if ( uPhase & (1 << i) )
+            Vec_PtrRemove( vLeaves, Vec_PtrEntry(vLeaves, i) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeGetLevel( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i, Level;
+    Level = 0;
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Level = ABC_MAX( Level, (int)pFanin->Level );
+    return Level + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * p, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin, * pObjNew;
+    int i, nVars, uSupport, nSuppVars;
+    // collect the cone using DFS (excluding leaves)
+    Abc_NodeSuperChoiceCollect2( pObj, p->vLeaves, p->vVolume );
+    assert( Vec_PtrEntryLast(p->vVolume) == pObj );  
+    // compute the truth table
+    p->uTruth = Abc_NodeSuperChoiceTruth( p );
+    // get the support of this truth table
+    nVars = Vec_PtrSize(p->vLeaves);
+    uSupport = Extra_TruthSupport(p->uTruth, nVars);
+    nSuppVars = Extra_WordCountOnes(uSupport);
+    assert( nSuppVars <= nVars );
+    if ( nSuppVars == 0 )
+    {
+        pObj->Level = 0;
+        return NULL;
+    }
+    if ( nSuppVars == 1 )
+    {
+        // find the variable
+        for ( i = 0; i < nVars; i++ )
+            if ( uSupport & (1 << i) )
+                break;
+        assert( i < nVars );
+        pFanin = Vec_PtrEntry( p->vLeaves, i );
+        pObj->Level = pFanin->Level;
+        return NULL;
+    }
+    // support-minimize the truth table
+    if ( nSuppVars != nVars )
+    {
+        Extra_TruthShrink( p->uCofs[0], p->uTruth, nSuppVars, nVars, uSupport );
+        Extra_TruthCopy( p->uTruth, p->uCofs[0], nVars );
+        Abc_NodeLeavesRemove( p->vLeaves, ((1 << nVars) - 1) & ~uSupport, nVars );
+    }
+//    return NULL;
+    // decompose the truth table recursively
+    while ( Vec_PtrSize(p->vLeaves) > p->nLutSize )
+        if ( !Abc_NodeDecomposeStep( p ) )
+        {
+            Vec_PtrForEachEntry( p->vLeaves, pFanin, i )
+                if ( Abc_ObjIsNode(pFanin) && Abc_ObjFanoutNum(pFanin) == 0 )
+                    Abc_NtkDeleteObj_rec( pFanin );
+            return NULL;
+        }
+    // create the topmost node
+    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
+    Vec_PtrForEachEntry( p->vLeaves, pFanin, i )
+        Abc_ObjAddFanin( pObjNew, pFanin );
+    // create the function
+    pObjNew->pData = Abc_SopCreateFromTruth( pObj->pNtk->pManFunc, Vec_PtrSize(p->vLeaves), p->uTruth ); // need ISOP
+    pObjNew->Level = Abc_NodeGetLevel( pObjNew );
+    return pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure used for sorting the nodes in increasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeCompareLevelsInc( int * pp1, int * pp2 )
+{
+    Abc_Obj_t * pNode1, * pNode2;
+    pNode1 = Vec_PtrEntry(s_pLeaves, *pp1);
+    pNode2 = Vec_PtrEntry(s_pLeaves, *pp2);
+    if ( pNode1->Level < pNode2->Level )
+        return -1;
+    if ( pNode1->Level > pNode2->Level ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Selects the earliest arriving nodes from the array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeDecomposeSort( Abc_Obj_t ** pLeaves, int nVars, int * pBSet, int nLutSize )
+{
+    Abc_Obj_t * pTemp[SCL_VARS_MAX];
+    int i, k, kBest, LevelMin;
+    assert( nLutSize < nVars );
+    assert( nVars <= SCL_VARS_MAX );
+    // copy nodes into the internal storage
+//    printf( "(" );
+    for ( i = 0; i < nVars; i++ )
+    {
+        pTemp[i] = pLeaves[i];
+//        printf( " %d", pLeaves[i]->Level );
+    }
+//    printf( " )\n" );
+    // choose one node at a time
+    for ( i = 0; i < nLutSize; i++ )
+    {
+        kBest = -1;
+        LevelMin = ABC_INFINITY;
+        for ( k = 0; k < nVars; k++ )
+            if ( pTemp[k] && LevelMin > (int)pTemp[k]->Level )
+            {
+                LevelMin = pTemp[k]->Level;
+                kBest = k;
+            }
+        pBSet[i] = kBest;
+        pTemp[kBest] = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeDecomposeStep( Abc_ManScl_t * p )
+{
+    static char pCofClasses[1<<SCL_LUT_MAX][1<<SCL_LUT_MAX];
+    static char nCofClasses[1<<SCL_LUT_MAX];
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObjNew, * pFanin, * pNodesNew[SCL_LUT_MAX];
+    unsigned * pTruthCof, * pTruthClass, * pTruth, uPhase;
+    int i, k, c, v, w, nVars, nVarsNew, nClasses, nCofs;
+    // set the network
+    pNtk = ((Abc_Obj_t *)Vec_PtrEntry(p->vLeaves, 0))->pNtk;
+    // find the earliest nodes
+    nVars = Vec_PtrSize(p->vLeaves);
+    assert( nVars > p->nLutSize );
+/*
+    for ( v = 0; v < nVars; v++ )
+        p->pBSet[v] = v;
+    qsort( (void *)p->pBSet, nVars, sizeof(int), 
+            (int (*)(const void *, const void *)) Abc_NodeCompareLevelsInc );
+*/
+    Abc_NodeDecomposeSort( (Abc_Obj_t **)Vec_PtrArray(p->vLeaves), Vec_PtrSize(p->vLeaves), p->pBSet, p->nLutSize );
+    assert( ((Abc_Obj_t *)Vec_PtrEntry(p->vLeaves, p->pBSet[0]))->Level <=
+        ((Abc_Obj_t *)Vec_PtrEntry(p->vLeaves, p->pBSet[1]))->Level );
+    // cofactor w.r.t. the selected variables
+    Extra_TruthCopy( p->uCofs[1], p->uTruth, nVars );
+    c = 2;
+    for ( v = 0; v < p->nLutSize; v++ )
+        for ( k = 0; k < (1<<v); k++ )
+        {
+            Extra_TruthCopy( p->uCofs[c], p->uCofs[c/2], nVars );
+            Extra_TruthCopy( p->uCofs[c+1], p->uCofs[c/2], nVars );
+            Extra_TruthCofactor0( p->uCofs[c], nVars, p->pBSet[v] );
+            Extra_TruthCofactor1( p->uCofs[c+1], nVars, p->pBSet[v] );
+            c += 2;
+        }
+    assert( c == (2 << p->nLutSize) );
+    // count unique cofactors
+    nClasses = 0;
+    nCofs = (1 << p->nLutSize);
+    for ( i = 0; i < nCofs; i++ )
+    {
+        pTruthCof = p->uCofs[ nCofs + i ];
+        for ( k = 0; k < nClasses; k++ )
+        {
+            pTruthClass = p->uCofs[ nCofs + pCofClasses[k][0] ];
+            if ( Extra_TruthIsEqual( pTruthCof, pTruthClass, nVars ) )
+            {
+                pCofClasses[k][ nCofClasses[k]++ ] = i;
+                break;
+            }
+        }
+        if ( k != nClasses )
+            continue;
+        // not found
+        pCofClasses[nClasses][0] = i;
+        nCofClasses[nClasses] = 1;
+        nClasses++;
+        if ( nClasses > nCofs/2 )
+            return 0;
+    }
+    // the number of cofactors is acceptable
+    nVarsNew = Extra_Base2Log( nClasses );
+    assert( nVarsNew < p->nLutSize );
+    // create the remainder truth table
+    // for each class of cofactors, multiply cofactor truth table by its code
+    Extra_TruthClear( p->uTruth, nVars );
+    for ( k = 0; k < nClasses; k++ )
+    {
+        pTruthClass = p->uCofs[ nCofs + pCofClasses[k][0] ];
+        for ( v = 0; v < nVarsNew; v++ )
+            if ( k & (1 << v) )
+                Extra_TruthAnd( pTruthClass, pTruthClass, p->uVars[p->pBSet[v]], nVars );
+            else
+                Extra_TruthSharp( pTruthClass, pTruthClass, p->uVars[p->pBSet[v]], nVars );
+        Extra_TruthOr( p->uTruth, p->uTruth, pTruthClass, nVars );
+    }
+    // create nodes
+    pTruth = p->uCofs[0];
+    for ( v = 0; v < nVarsNew; v++ )
+    {
+        Extra_TruthClear( pTruth, p->nLutSize );
+        for ( k = 0; k < nClasses; k++ )
+            if ( k & (1 << v) )
+                for ( i = 0; i < nCofClasses[k]; i++ )
+                {
+                    pTruthCof = p->uCofs[1];
+                    Extra_TruthFill( pTruthCof, p->nLutSize );
+                    for ( w = 0; w < p->nLutSize; w++ )
+                        if ( pCofClasses[k][i] & (1 << (p->nLutSize-1-w)) )
+                            Extra_TruthAnd( pTruthCof, pTruthCof, p->uVars[w], p->nLutSize );
+                        else
+                            Extra_TruthSharp( pTruthCof, pTruthCof, p->uVars[w], p->nLutSize );
+                    Extra_TruthOr( pTruth, pTruth, pTruthCof, p->nLutSize );
+                }
+        // implement the node
+        pObjNew = Abc_NtkCreateNode( pNtk );
+        for ( i = 0; i < p->nLutSize; i++ )
+        {
+            pFanin = Vec_PtrEntry( p->vLeaves, p->pBSet[i] );
+            Abc_ObjAddFanin( pObjNew, pFanin );
+        }
+        // create the function
+        pObjNew->pData = Abc_SopCreateFromTruth( pNtk->pManFunc, p->nLutSize, pTruth ); // need ISOP
+        pObjNew->Level = Abc_NodeGetLevel( pObjNew );
+        pNodesNew[v] = pObjNew;
+    }
+    // put the new nodes back into the list
+    for ( v = 0; v < nVarsNew; v++ )
+        Vec_PtrWriteEntry( p->vLeaves, p->pBSet[v], pNodesNew[v] );
+    // compute the variables that should be removed
+    uPhase = 0;
+    for ( v = nVarsNew; v < p->nLutSize; v++ )
+        uPhase |= (1 << p->pBSet[v]);
+    // remove entries from the array
+    Abc_NodeLeavesRemove( p->vLeaves, uPhase, nVars );
+    // update truth table
+    Extra_TruthShrink( p->uCofs[0], p->uTruth, nVars - p->nLutSize + nVarsNew, nVars, ((1 << nVars) - 1) & ~uPhase );
+    Extra_TruthCopy( p->uTruth, p->uCofs[0], nVars );
+    assert( !Extra_TruthVarInSupport( p->uTruth, nVars, nVars - p->nLutSize + nVarsNew ) );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+