Other changes to enable new features in the mapper (bug fix).

6 files changed, 464 insertions, 81 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index a7fa7d2d..fb7abae9 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -212,6 +212,7 @@ struct Abc_Ntk_t_
     float *           pLutTimes;     // arrivals/requireds/slacks using LUT-delay model
     Vec_Ptr_t *       vOnehots;      // names of one-hot-encoded registers
     Vec_Int_t *       vObjPerm;      // permutation saved
+    Vec_Vec_t *       vRealPos;      // additional PO info
     // node attributes
     Vec_Ptr_t *       vAttrs;        // managers of various node attributes (node functionality, global BDDs, etc)
 };
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 3ec71680..ac488114 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -111,6 +111,7 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
     pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
     pNtkNew->nConstrs = pNtk->nConstrs;
     pNtkNew->nRealPos = pNtk->nRealPos;
+    pNtkNew->vRealPos = pNtk->vRealPos ? Vec_VecDup( pNtk->vRealPos ) : NULL;
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -165,6 +166,7 @@ Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc
     pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
     pNtkNew->nConstrs = pNtk->nConstrs;
     pNtkNew->nRealPos = pNtk->nRealPos;
+    pNtkNew->vRealPos = pNtk->vRealPos ? Vec_VecDup( pNtk->vRealPos ) : NULL;
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -1045,6 +1047,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
         Vec_VecFree( (Vec_Vec_t *)pNtk->vOnehots );
     Vec_PtrFreeP( &pNtk->vLtlProperties );
     Vec_IntFreeP( &pNtk->vObjPerm );
+    Vec_VecFreeP( &pNtk->vRealPos );
     ABC_FREE( pNtk );
 }
 
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 96339842..0cf4fbbf 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -42,6 +42,7 @@ extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
 extern void Abc_NtkCollectPoDrivers( If_Man_t * p, Abc_Ntk_t * pNtk );
 extern void Abc_NtkCreateChoiceDrivers( If_Man_t * p );
 extern void Abc_NtkFreePoDrivers( If_Man_t * p, Abc_Ntk_t * pNtk );
+extern void Abc_NtkRecreatePoDrivers( If_Man_t * p, Abc_Ntk_t * pNtkNew );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -239,6 +240,37 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     return pIfMan;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Box mapping procedures.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_MapBoxSetPrevNext( Vec_Ptr_t * vDrivers, Vec_Int_t * vMapIn, Vec_Int_t * vMapOut, int Id )
+{
+    Abc_Obj_t * pNode;
+    pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+2);
+    Vec_IntWriteEntry( vMapIn, Abc_ObjId(Abc_ObjFanin0(pNode)), Id );
+    pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+4);
+    Vec_IntWriteEntry( vMapOut, Abc_ObjId(Abc_ObjFanin0(pNode)), Id );
+}
+static inline int Abc_MapBox2Next( Vec_Ptr_t * vDrivers, Vec_Int_t * vMapIn, Vec_Int_t * vMapOut, int Id )
+{
+    Abc_Obj_t * pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+4);
+    return Vec_IntEntry( vMapIn, Abc_ObjId(Abc_ObjFanin0(pNode)) );
+}
+static inline int Abc_MapBox2Prev( Vec_Ptr_t * vDrivers, Vec_Int_t * vMapIn, Vec_Int_t * vMapOut, int Id )
+{
+    Abc_Obj_t * pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+2);
+    return Vec_IntEntry( vMapOut, Abc_ObjId(Abc_ObjFanin0(pNode)) );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Creates the mapped network.]
@@ -254,7 +286,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
 {
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pNode, * pNodeNew, * pExor;
+    Abc_Obj_t * pNode, * pNodeNew;
     Vec_Int_t * vCover;
     int i, nDupGates;
     // create the new network
@@ -271,84 +303,24 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     If_ObjSetCopy( If_ManConst1(pIfMan), Abc_NtkCreateNodeConst1(pNtkNew) );
     Abc_NtkForEachCi( pNtk, pNode, i )
         If_ObjSetCopy( If_ManCi(pIfMan, i), pNode->pCopy );
+
     // process the nodes in topological order
     vCover = Vec_IntAlloc( 1 << 16 );
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
-    if ( pIfMan->pPars->fEnableRealPos )
-    {
-        // collect drivers
-        Vec_Ptr_t * vDrivers, * vFanins;
-        int nRealLuts, nStopPoint;
-        vDrivers = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
-        Abc_NtkForEachCo( pNtk, pNode, i )
-        {
-            Extra_ProgressBarUpdate( pProgress, i, "Final" );
-            pNodeNew = Abc_NodeFromIf_rec( pNtkNew, pIfMan, If_ObjFanin0(If_ManCo(pIfMan, i)), vCover );
-            pNodeNew = Abc_ObjNotCond( pNodeNew, If_ObjFaninC0(If_ManCo(pIfMan, i)) );
-//            Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
-            if ( Abc_ObjIsComplement(pNodeNew) )
-                pNodeNew = Abc_NtkCreateNodeInv( pNtkNew, Abc_ObjRegular(pNodeNew) );
-            else
-                pNodeNew = Abc_NtkCreateNodeBuf( pNtkNew, pNodeNew );
-            Vec_PtrPush( vDrivers, pNodeNew );
-        }
-        nStopPoint = Abc_NtkObjNumMax( pNtkNew );
-
-        // update drivers
-        vFanins = Vec_PtrAlloc( 2 );
-        for ( i = pNtk->nRealPos; i <  Abc_NtkPoNum(pNtk); i += 5 )
-        {
-            // create first XOR
-            Vec_PtrClear( vFanins );
-            Vec_PtrPush( vFanins, (Abc_Obj_t *)Vec_PtrEntry(vDrivers, i+0) );
-            Vec_PtrPush( vFanins, (Abc_Obj_t *)Vec_PtrEntry(vDrivers, i+1) );
-            pExor = Abc_NtkCreateNodeExor( pNtkNew, vFanins );
-            // update polarity
-            if ( strstr( Abc_ObjName(Abc_NtkPo(pNtk, i)), "SUB" ) != NULL )
-                pExor->pData = Hop_Not( (Hop_Obj_t *) pExor->pData );
-            // create second XOR
-            Vec_PtrClear( vFanins );
-            Vec_PtrPush( vFanins, pExor );
-            Vec_PtrPush( vFanins, (Abc_Obj_t *)Vec_PtrEntry(vDrivers, i+2) );
-            pNode = Abc_NtkCreateNodeExor( pNtkNew, vFanins );
-            Vec_PtrWriteEntry( vDrivers, i+3, pNode );
-            // create MUX
-            pNode = Abc_NtkCreateNodeMux( pNtkNew, pExor, 
-                (Abc_Obj_t *)Vec_PtrEntry(vDrivers, i+2), 
-                (Abc_Obj_t *)Vec_PtrEntry(vDrivers, i+1) );
-            Vec_PtrWriteEntry( vDrivers, i+4, pNode );
-        }
-        Vec_PtrFree( vFanins );
-        // connect drivers
-        Abc_NtkForEachCo( pNtk, pNode, i )
-            Abc_ObjAddFanin( pNode->pCopy, (Abc_Obj_t *)Vec_PtrEntry(vDrivers, i) );
-        Vec_PtrFree( vDrivers );
-        // sweep
-        nDupGates = Abc_NtkCleanup( pNtkNew, 0 );
-//        printf( "The number of removed nodes = %d.\n", nDupGates );
-        // count non-trivial LUTs nodes
-        nRealLuts = 0;
-        Abc_NtkForEachNode( pNtkNew, pNode, i )
-        {
-            if ( (int)Abc_ObjId(pNode) > nStopPoint )
-                break;
-            if ( Abc_ObjFaninNum(pNode) > 1 )
-                nRealLuts++;
-        }
-        printf( "The number of real LUTs = %d.\n", nRealLuts );
-    }
-    else
+    Abc_NtkForEachCo( pNtk, pNode, i )
     {
-        Abc_NtkForEachCo( pNtk, pNode, i )
-        {
-            Extra_ProgressBarUpdate( pProgress, i, "Final" );
-            pNodeNew = Abc_NodeFromIf_rec( pNtkNew, pIfMan, If_ObjFanin0(If_ManCo(pIfMan, i)), vCover );
-            pNodeNew = Abc_ObjNotCond( pNodeNew, If_ObjFaninC0(If_ManCo(pIfMan, i)) );
-            Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
-        }
+        Extra_ProgressBarUpdate( pProgress, i, "Final" );
+        pNodeNew = Abc_NodeFromIf_rec( pNtkNew, pIfMan, If_ObjFanin0(If_ManCo(pIfMan, i)), vCover );
+        pNodeNew = Abc_ObjNotCond( pNodeNew, If_ObjFaninC0(If_ManCo(pIfMan, i)) );
+        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
     Extra_ProgressBarStop( pProgress );
     Vec_IntFree( vCover );
+
+    // update PO drivers
+    if ( pIfMan->pPars->fEnableRealPos )
+        Abc_NtkRecreatePoDrivers( pIfMan, pNtkNew );
+
     // remove the constant node if not used
     pNodeNew = (Abc_Obj_t *)If_ObjCopy( If_ManConst1(pIfMan) );
     if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
@@ -361,7 +333,12 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     // decouple the PO driver nodes to reduce the number of levels
     nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, !pIfMan->pPars->fUseBuffs );
     if ( nDupGates && pIfMan->pPars->fVerbose )
-        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    {
+        if ( pIfMan->pPars->fUseBuffs )
+            printf( "Added %d buffers/inverters to decouple the CO drivers.\n", nDupGates );
+        else
+            printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    }
     return pNtkNew;
 }
 
@@ -779,10 +756,56 @@ Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_NtkMarkMux( Abc_Obj_t * pDriver, Abc_Obj_t ** ppNode1, Abc_Obj_t ** ppNode2 )
+{
+    Abc_Obj_t * pNodeC, * pNodeT, * pNodeE;
+    If_Obj_t * pIfObj;
+
+    *ppNode1 = NULL;
+    *ppNode2 = NULL;
+    if ( pDriver == NULL )
+        return;
+    if ( !Abc_NodeIsMuxType(pDriver) )
+        return;
+
+    pNodeC = Abc_NodeRecognizeMux( pDriver, &pNodeT, &pNodeE );
+
+    pIfObj = If_Regular( (If_Obj_t *)Abc_ObjFanin0(pDriver)->pCopy );
+    if ( If_ObjIsAnd(pIfObj) )
+        pIfObj->fSkipCut = 1;
+    pIfObj = If_Regular( (If_Obj_t *)Abc_ObjFanin1(pDriver)->pCopy );
+    if ( If_ObjIsAnd(pIfObj) )
+        pIfObj->fSkipCut = 1;
+/*
+    pIfObj = If_Regular( (If_Obj_t *)Abc_ObjRegular(pNodeC)->pCopy );
+    if ( If_ObjIsAnd(pIfObj) )
+        pIfObj->fSkipCut = 1;
+    pIfObj = If_Regular( (If_Obj_t *)Abc_ObjRegular(pNodeT)->pCopy );
+    if ( If_ObjIsAnd(pIfObj) )
+        pIfObj->fSkipCut = 1;
+    pIfObj = If_Regular( (If_Obj_t *)Abc_ObjRegular(pNodeE)->pCopy );
+    if ( If_ObjIsAnd(pIfObj) )
+        pIfObj->fSkipCut = 1;
+*/
+    *ppNode1 = Abc_ObjRegular(pNodeC);
+    *ppNode2 = Abc_ObjRegular(pNodeT);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets PO drivers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_NtkCollectPoDrivers( If_Man_t * p, Abc_Ntk_t * pNtk )
 {
     Vec_Int_t * vTemp;
-    Abc_Obj_t * pObj;
+    Abc_Obj_t * pObj, * pDriver;
     If_Obj_t * pIfObj;
     int i, g, nGroups;
     if ( pNtk->nRealPos == 0 )
@@ -828,6 +851,72 @@ void Abc_NtkCollectPoDrivers( If_Man_t * p, Abc_Ntk_t * pNtk )
         Vec_IntFree( vTemp );
     }
 //    printf( "\n" );
+    return;
+
+    // highlight inner logic
+    for ( i = pNtk->nRealPos; i <  Abc_NtkPoNum(pNtk); i += 5 )
+    {
+        Abc_Obj_t * pNode1, * pNode2;
+
+        pObj = Abc_NtkPo( pNtk, i + 4 );
+        pDriver = Abc_ObjFanin0( pObj );
+        Abc_NtkMarkMux( pDriver, &pNode1, &pNode2 );
+
+        pObj = Abc_NtkPo( pNtk, i + 3 );
+        pDriver = Abc_ObjFanin0( pObj );
+        Abc_NtkMarkMux( pDriver, &pNode1, &pNode2 );
+
+        if ( pNode1 == NULL )
+            continue;
+
+        assert( Abc_ObjRegular(pNode1) != Abc_ObjRegular(pNode2) );
+//        Abc_NtkMarkMux( pNode1, &pNode1, &pNode2 );
+//        Abc_NtkMarkMux( pNode2, &pNode1, &pNode2 );
+    }
+
+    {
+        Vec_Int_t * vInfo;
+        int i, k, numPo;
+
+        Vec_VecForEachLevelInt( pNtk->vRealPos, vInfo, i )
+        {
+            numPo = Vec_IntEntry( vInfo, 0 );
+            pObj = Abc_NtkPo( pNtk, numPo+2 );
+            pDriver = Abc_ObjFanin0( pObj );
+            pIfObj = If_Regular( (If_Obj_t *)pDriver->pCopy );
+            pIfObj->fSkipCut = 0;
+
+            numPo = Vec_IntEntryLast( vInfo );
+            pObj = Abc_NtkPo( pNtk, numPo+4 );
+            pDriver = Abc_ObjFanin0( pObj );
+            pIfObj = If_Regular( (If_Obj_t *)pDriver->pCopy );
+            pIfObj->fSkipCut = 0;
+
+            Vec_IntForEachEntry( vInfo, numPo, k )
+            {
+                pObj = Abc_NtkPo( pNtk, numPo+0 );
+                pDriver = Abc_ObjFanin0( pObj );
+                pIfObj = If_Regular( (If_Obj_t *)pDriver->pCopy );
+                pIfObj->fSkipCut = 0;
+
+                pObj = Abc_NtkPo( pNtk, numPo+1 );
+                pDriver = Abc_ObjFanin0( pObj );
+                pIfObj = If_Regular( (If_Obj_t *)pDriver->pCopy );
+                pIfObj->fSkipCut = 0;
+
+                pObj = Abc_NtkPo( pNtk, numPo+2 );
+                pDriver = Abc_ObjFanin0( pObj );
+                pIfObj = If_Regular( (If_Obj_t *)pDriver->pCopy );
+                pIfObj->fSkipCut = 0;
+
+                pObj = Abc_NtkPo( pNtk, numPo+3 );
+                pDriver = Abc_ObjFanin0( pObj );
+                pIfObj = If_Regular( (If_Obj_t *)pDriver->pCopy );
+                pIfObj->fSkipCut = 0;
+            }
+        }
+    }
+
 }
 
 
@@ -912,6 +1001,182 @@ void Abc_NtkFreePoDrivers( If_Man_t * p, Abc_Ntk_t * pNtk )
     ABC_FREE( p->pDriverCuts );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkIfCheckTfi_rec( Abc_Obj_t * pNode, Abc_Obj_t * pOld )
+{
+    Abc_Obj_t * pFanin;
+    int k;
+    if ( pNode == NULL )
+        return 0;
+    if ( pNode == pOld )
+        return 1;
+    // check the trivial cases
+    if ( Abc_ObjIsCi(pNode) )
+        return 0; 
+    assert( Abc_ObjIsNode(pNode) );
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return 0;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // check the children
+    Abc_ObjForEachFanin( pNode, pFanin, k )
+        if ( Abc_NtkIfCheckTfi_rec( pFanin, pOld ) )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkIfCheckTfi( Abc_Ntk_t * pNtk, Abc_Obj_t * pOld, Abc_Obj_t * pNew )
+{
+    assert( !Abc_ObjIsComplement(pOld) );
+    assert( !Abc_ObjIsComplement(pNew) );
+    Abc_NtkIncrementTravId(pNtk);
+    return Abc_NtkIfCheckTfi_rec( pNew, pOld );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Restores the structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecreatePoDrivers( If_Man_t * p, Abc_Ntk_t * pNtkNew )
+{
+    Abc_Obj_t * pNode, * pExor, * pObj, * pFanin, * pFaninNew;
+    Vec_Ptr_t * vDrivers, * vDriversNew, * vFanins;
+    Vec_Int_t * vInfo, * vNodeMap, * vDriverInvs;
+    int i, k, numPo, nRealLuts, fCompl;
+    if ( pNtkNew->vRealPos == NULL )
+    {
+        printf( "Missing key information.\n" );
+        return;
+    }
+
+    // create drivers
+    vDrivers = Vec_PtrStart( pNtkNew->nRealPos );
+    vDriverInvs = Vec_IntStart( pNtkNew->nRealPos );
+    for ( i = pNtkNew->nRealPos; i < Abc_NtkPoNum(pNtkNew); i++ )
+    {
+        pObj = Abc_NtkPo( pNtkNew, i );
+        if ( Abc_ObjFaninC0(pObj) )
+            pNode = Abc_NtkCreateNodeInv( pNtkNew, Abc_ObjFanin0(pObj) );
+        else
+            pNode = Abc_NtkCreateNodeBuf( pNtkNew, Abc_ObjFanin0(pObj) );
+//        if ( i % 5 == 4 )
+//            printf( "%d", Abc_ObjFaninC0(pObj) );
+        Vec_PtrPush( vDrivers, pNode );
+        Vec_IntPush( vDriverInvs, Abc_ObjFaninC0(pObj) );
+    }
+    assert( Vec_PtrSize( vDrivers ) == Abc_NtkPoNum( pNtkNew ) );
+
+    // create new logic
+    vFanins = Vec_PtrAlloc( 2 );
+    vDriversNew = Vec_PtrStart( Abc_NtkPoNum(pNtkNew) );
+    Vec_VecForEachLevelInt( pNtkNew->vRealPos, vInfo, i )
+    {
+        // find complemented attribute
+        numPo  = Vec_IntEntry( vInfo, 0 );
+        fCompl = (strstr( Abc_ObjName(Abc_NtkPo(pNtkNew, numPo)), "SUB" ) != NULL);
+        // consider parts
+        Vec_IntForEachEntry( vInfo, numPo, k )
+        {
+            // update input
+            if ( k > 0 )
+                Vec_PtrWriteEntry( vDriversNew, numPo+2, pNode );
+            // create first XOR
+            Vec_PtrClear( vFanins );
+            Vec_PtrPush( vFanins, (Abc_Obj_t *)Vec_PtrEntry(vDrivers, numPo+0) );
+            Vec_PtrPush( vFanins, (Abc_Obj_t *)Vec_PtrEntry(vDrivers, numPo+1) );
+            pExor = Abc_NtkCreateNodeExor( pNtkNew, vFanins );
+            // update polarity
+            pExor->pData = Hop_NotCond( (Hop_Obj_t *)pExor->pData, fCompl );
+            // create second XOR
+            Vec_PtrClear( vFanins );
+            Vec_PtrPush( vFanins, pExor );
+            Vec_PtrPush( vFanins, (Abc_Obj_t *)Vec_PtrEntry(vDrivers, numPo+2) ); 
+            pNode = Abc_NtkCreateNodeExor( pNtkNew, vFanins );
+            Vec_PtrWriteEntry( vDriversNew, numPo+3, pNode );
+            // create MUX
+            pNode = Abc_NtkCreateNodeMux( pNtkNew, pExor, 
+                (Abc_Obj_t *)Vec_PtrEntry(vDrivers, numPo+2), 
+                (Abc_Obj_t *)Vec_PtrEntry(vDrivers, numPo+(fCompl ? 0 : 1)) );
+            Vec_PtrWriteEntry( vDriversNew, numPo+4, pNode );
+        }
+    }
+    Vec_PtrFree( vFanins );
+
+    // map internal nodes into PO numbers
+    vNodeMap = Vec_IntStartFull( Abc_NtkObjNumMax(pNtkNew) );
+    Vec_VecForEachLevelInt( pNtkNew->vRealPos, vInfo, i )
+    Vec_IntForEachEntryReverse( vInfo, numPo, k )
+    {
+        pObj = Abc_NtkPo( pNtkNew, numPo+3 );
+        Vec_IntWriteEntry( vNodeMap, Abc_ObjId( Abc_ObjFanin0(pObj) ), numPo+3 );
+        pObj = Abc_NtkPo( pNtkNew, numPo+4 );
+        Vec_IntWriteEntry( vNodeMap, Abc_ObjId( Abc_ObjFanin0(pObj) ), numPo+4 );
+    }
+
+    // replace logic
+    Abc_NtkForEachObj( pNtkNew, pObj, i )
+    {
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            numPo = Vec_IntEntry( vNodeMap, Abc_ObjId(pFanin) );
+            if ( numPo == ~0 )
+                continue;
+            // get the node and the complemented bit
+            pFaninNew = Vec_PtrEntry( vDriversNew, numPo );
+            fCompl    = Vec_IntEntry( vDriverInvs, numPo );
+            if ( fCompl )
+                pFaninNew = Abc_NtkCreateNodeInv( pNtkNew, pFaninNew );
+
+            if ( !Abc_NtkIfCheckTfi( pNtkNew, pObj, pFaninNew ) )
+                Abc_ObjPatchFanin( pObj, pFanin, pFaninNew );
+        }
+    }    
+    Vec_PtrFree( vDrivers );
+    Vec_PtrFree( vDriversNew );
+    Vec_IntFree( vNodeMap );
+    Vec_IntFree( vDriverInvs );
+
+    // sweep
+    Abc_NtkCleanup( pNtkNew, 0 );
+
+    // count non-trivial LUTs nodes
+    nRealLuts = -2 * Vec_VecSizeSize(pNtkNew->vRealPos);
+    Abc_NtkForEachNode( pNtkNew, pNode, i )
+        if ( Abc_ObjFaninNum(pNode) > 1 )
+            nRealLuts++;
+    printf( "The number of real LUTs = %d.\n", nRealLuts );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index e41b78b8..8564331d 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -120,6 +120,8 @@ static Io_MvVar_t *      Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar );
 static int               Io_MvCharIsSpace( char s )  { return s == ' ' || s == '\t' || s == '\r' || s == '\n';  }
 static int               Io_MvCharIsMvSymb( char s ) { return s == '(' || s == ')' || s == '{' || s == '}' || s == '-' || s == ',' || s == '!';  }
 
+static Vec_Vec_t *       Io_MvExtractBoxInfo( Abc_Ntk_t * pNtk );
+
 extern void              Abc_NtkStartMvVars( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
@@ -233,6 +235,8 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     Vec_PtrForEachEntry( char *, vGlobalLtlArray, pLtlProp, i )
         Vec_PtrPush( pNtk->vLtlProperties, pLtlProp );
     Vec_PtrFreeP( &vGlobalLtlArray );
+
+    pNtk->vRealPos = Io_MvExtractBoxInfo( pNtk );
     return pNtk;
 }
 
@@ -2105,6 +2109,106 @@ static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Box mapping procedures.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_MapBoxSetPrevNext( Vec_Ptr_t * vDrivers, Vec_Int_t * vMapIn, Vec_Int_t * vMapOut, int Id )
+{
+    Abc_Obj_t * pNode;
+    pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+2);
+    Vec_IntWriteEntry( vMapIn, Abc_ObjId(Abc_ObjFanin0(Abc_ObjFanin0(pNode))), Id );
+    pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+4);
+    Vec_IntWriteEntry( vMapOut, Abc_ObjId(Abc_ObjFanin0(Abc_ObjFanin0(pNode))), Id );
+}
+static inline int Abc_MapBox2Next( Vec_Ptr_t * vDrivers, Vec_Int_t * vMapIn, Vec_Int_t * vMapOut, int Id )
+{
+    Abc_Obj_t * pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+4);
+    return Vec_IntEntry( vMapIn, Abc_ObjId(Abc_ObjFanin0(Abc_ObjFanin0(pNode))) );
+}
+static inline int Abc_MapBox2Prev( Vec_Ptr_t * vDrivers, Vec_Int_t * vMapIn, Vec_Int_t * vMapOut, int Id )
+{
+    Abc_Obj_t * pNode = (Abc_Obj_t *)Vec_PtrEntry(vDrivers, Id+2);
+    return Vec_IntEntry( vMapOut, Abc_ObjId(Abc_ObjFanin0(Abc_ObjFanin0(pNode))) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Vec_Vec_t * Io_MvExtractBoxInfo( Abc_Ntk_t * pNtk )
+{
+    Vec_Int_t * vMapIn, * vMapOut, * vList;
+    Vec_Ptr_t * vBoxInfo, * vDrivers;
+    Abc_Obj_t * pObj;
+    int i, boxId;
+
+    // quit if there is no boxes
+    if ( pNtk->nRealPos == 0 || (Abc_NtkPoNum(pNtk) - pNtk->nRealPos) % 5 != 0 )
+        return NULL;
+
+    // allocate
+    vBoxInfo = Vec_PtrAlloc( 10 );
+    vDrivers = Vec_PtrAlloc( Abc_NtkPoNum(pNtk) );
+    vMapIn   = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) );
+    vMapOut  = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) );
+
+    // collect drivers
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Vec_PtrPush( vDrivers, Abc_ObjFanin0(Abc_ObjFanin0(pObj)) );
+
+    // map box signals into box numbers            
+    for ( i = pNtk->nRealPos; i < Abc_NtkPoNum(pNtk); i += 5 )
+    {
+//        int k;
+//        for ( k = 0; k < 5; k++ )
+//            printf( "%d ", Abc_ObjFanin0(Abc_ObjFanin0(Abc_ObjFanin0(Abc_NtkPo(pNtk,i+k))))->Id );
+//        printf( "\n" );
+        Abc_MapBoxSetPrevNext( vDrivers, vMapIn, vMapOut, i );
+    }
+
+    // find those that do not have input mapped
+    for ( i = pNtk->nRealPos; i < Abc_NtkPoNum(pNtk); i += 5 )
+    {
+        if ( Abc_MapBox2Prev( vDrivers, vMapIn, vMapOut, i ) != ~0 )
+            continue;
+        // create new list
+        vList = Vec_IntAlloc( 32 );
+        boxId = i;
+        while ( boxId != ~0 )
+        {
+            Vec_IntPush( vList, boxId );
+            boxId = Abc_MapBox2Next( vDrivers, vMapIn, vMapOut, boxId );
+        }
+        Vec_PtrPush( vBoxInfo, vList );
+//printf( " %d", Vec_IntSize(vList) );
+    }
+//printf( "\n" );
+    if ( 5 * Vec_VecSizeSize((Vec_Vec_t *)vBoxInfo) != (Abc_NtkPoNum(pNtk) - pNtk->nRealPos) )
+        printf( "Mismatch in the number of boxes!!!\n" );
+
+    // clean up
+    Vec_IntFree( vMapIn );
+    Vec_IntFree( vMapOut );
+    Vec_PtrFree( vDrivers );
+    return (Vec_Vec_t *)vBoxInfo;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 52cd0c2b..8ac6e4f3 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -231,7 +231,8 @@ struct If_Obj_t_
     unsigned           fVisit  :  1;  // multipurpose mark
     unsigned           fSpec   :  1;  // multipurpose mark
     unsigned           fDriver :  1;  // multipurpose mark
-    unsigned           Level   : 20;  // logic level of the node
+    unsigned           fSkipCut:  1;  // multipurpose mark
+    unsigned           Level   : 19;  // logic level of the node
     int                Id;            // integer ID
     int                IdPio;         // integer ID of PIs/POs
     int                nRefs;         // the number of references
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 8b00ab01..86ecfd99 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -94,8 +94,11 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     If_Cut_t * pCut0, * pCut1, * pCut;
     int i, k;
  
-    assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 1 );
-    assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 1 );
+//    assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 1 );
+//    assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 1 );
+
+    assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 );
+    assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 );
 
     // prepare
     if ( !p->pPars->fSeqMap )
@@ -232,8 +235,11 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     assert( pCutSet->nCuts > 0 );
 
     // add the trivial cut to the set
-    If_ManSetupCutTriv( p, pCutSet->ppCuts[pCutSet->nCuts++], pObj->Id );
-    assert( pCutSet->nCuts <= pCutSet->nCutsMax+1 );
+    if ( !pObj->fSkipCut )
+    {
+        If_ManSetupCutTriv( p, pCutSet->ppCuts[pCutSet->nCuts++], pObj->Id );
+        assert( pCutSet->nCuts <= pCutSet->nCutsMax+1 );
+    }
 
     // update the best cut
     if ( !fPreprocess || pCutSet->ppCuts[0]->Delay <= pObj->Required + p->fEpsilon )
@@ -325,8 +331,11 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
     assert( pCutSet->nCuts > 0 );
 
     // add the trivial cut to the set
-    If_ManSetupCutTriv( p, pCutSet->ppCuts[pCutSet->nCuts++], pObj->Id );
-    assert( pCutSet->nCuts <= pCutSet->nCutsMax+1 );
+    if ( !pObj->fSkipCut )
+    {
+        If_ManSetupCutTriv( p, pCutSet->ppCuts[pCutSet->nCuts++], pObj->Id );
+        assert( pCutSet->nCuts <= pCutSet->nCutsMax+1 );
+    }
 
     // update the best cut
     if ( !fPreprocess || pCutSet->ppCuts[0]->Delay <= pObj->Required + p->fEpsilon )