Version abc80429

11 files changed, 213 insertions, 41 deletions

diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c
index e7675420..e812da3d 100644
--- a/src/aig/bdc/bdcCore.c
+++ b/src/aig/bdc/bdcCore.c
@@ -64,7 +64,7 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
     Bdc_Man_t * p;
     p = ALLOC( Bdc_Man_t, 1 );
     memset( p, 0, sizeof(Bdc_Man_t) );
-    assert( pPars->nVarsMax > 2 && pPars->nVarsMax < 16 );
+    assert( pPars->nVarsMax > 1 && pPars->nVarsMax < 16 );
     p->pPars = pPars;
     p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
     p->nDivsLimit = 200;
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 7607d17c..a0fca09d 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -547,6 +547,9 @@ extern int             Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t
 extern int             Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
 /*=== kitPla.c ==========================================================*/
 extern int             Kit_PlaIsConst0( char * pSop );
+extern int             Kit_PlaIsConst1( char * pSop );
+extern int             Kit_PlaIsBuf( char * pSop );
+extern int             Kit_PlaIsInv( char * pSop );
 extern int             Kit_PlaGetVarNum( char * pSop );
 extern int             Kit_PlaGetCubeNum( char * pSop );
 extern int             Kit_PlaIsComplement( char * pSop );
diff --git a/src/aig/kit/kitHop.c b/src/aig/kit/kitHop.c
index 86ec5a88..044633bc 100644
--- a/src/aig/kit/kitHop.c
+++ b/src/aig/kit/kitHop.c
@@ -130,6 +130,7 @@ Hop_Obj_t * Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec
     Kit_Graph_t * pGraph;
     Hop_Obj_t * pFunc;
     // perform factoring
+    Vec_IntClear( vMemory );
     pGraph = Kit_SopFactor( vCover, 0, nVars, vMemory );
     // convert graph to the AIG
     pFunc = Kit_GraphToHop( pMan, pGraph );
diff --git a/src/aig/kit/kitPla.c b/src/aig/kit/kitPla.c
index be8f594a..776762c2 100644
--- a/src/aig/kit/kitPla.c
+++ b/src/aig/kit/kitPla.c
@@ -47,6 +47,62 @@ int Kit_PlaIsConst0( char * pSop )
 
 /**Function*************************************************************
 
+  Synopsis    [Checks if the cover is constant 1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_PlaIsConst1( char * pSop )
+{
+    return pSop[0] == ' ' && pSop[1] == '1';
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the cover is a buffer.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_PlaIsBuf( char * pSop )
+{
+    if ( pSop[4] != 0 )
+        return 0;
+    if ( (pSop[0] == '1' && pSop[2] == '1') || (pSop[0] == '0' && pSop[2] == '0') )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the cover is an inverter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_PlaIsInv( char * pSop )
+{
+    if ( pSop[4] != 0 )
+        return 0;
+    if ( (pSop[0] == '0' && pSop[2] == '1') || (pSop[0] == '1' && pSop[2] == '0') )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reads the number of variables in the cover.]
 
   Description []
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 0ba62bea..1028bd97 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -198,25 +198,25 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
     for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \
         if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else
 
-#define Ntl_ModelForEachPi( pNtl, pObj, i )                                     \
-    Vec_PtrForEachEntry( pNtl->vPis, pObj, i )
-#define Ntl_ModelForEachPo( pNtl, pObj, i )                                     \
-    Vec_PtrForEachEntry( pNtl->vPos, pObj, i )
-#define Ntl_ModelForEachObj( pNtl, pObj, i )                                    \
-    for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \
+#define Ntl_ModelForEachPi( pNwk, pObj, i )                                     \
+    Vec_PtrForEachEntry( pNwk->vPis, pObj, i )
+#define Ntl_ModelForEachPo( pNwk, pObj, i )                                     \
+    Vec_PtrForEachEntry( pNwk->vPos, pObj, i )
+#define Ntl_ModelForEachObj( pNwk, pObj, i )                                    \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
         if ( pObj == NULL ) {} else
-#define Ntl_ModelForEachLatch( pNtl, pObj, i )                                  \
-    for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \
+#define Ntl_ModelForEachLatch( pNwk, pObj, i )                                  \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
         if ( (pObj) == NULL || !Ntl_ObjIsLatch(pObj) ) {} else
-#define Ntl_ModelForEachNode( pNtl, pObj, i )                                   \
-    for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \
+#define Ntl_ModelForEachNode( pNwk, pObj, i )                                   \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
         if ( (pObj) == NULL || !Ntl_ObjIsNode(pObj) ) {} else
-#define Ntl_ModelForEachBox( pNtl, pObj, i )                                    \
-    for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \
+#define Ntl_ModelForEachBox( pNwk, pObj, i )                                    \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
         if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else
-#define Ntl_ModelForEachNet( pNtl, pNet, i )                                    \
-    for ( i = 0; i < pNtl->nTableSize; i++ )                                    \
-        for ( pNet = pNtl->pTable[i]; pNet; pNet = pNet->pNext ) 
+#define Ntl_ModelForEachNet( pNwk, pNet, i )                                    \
+    for ( i = 0; i < pNwk->nTableSize; i++ )                                    \
+        for ( pNet = pNwk->pTable[i]; pNet; pNet = pNet->pNext ) 
 
 #define Ntl_ObjForEachFanin( pObj, pFanin, i )                                  \
     for ( i = 0; (i < (pObj)->nFanins) && ((pFanin) = (pObj)->pFanio[i]); i++ )
@@ -296,6 +296,8 @@ extern void            Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
 extern void            Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName );
 /*=== ntlUtil.c ==========================================================*/
 extern int             Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
+extern int             Ntl_ModelGetFaninMax( Ntl_Mod_t * pRoot );
+extern Ntl_Net_t *     Ntl_ModelFindSimpleNet( Ntl_Net_t * pNetCo );
 extern int             Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
 extern Vec_Ptr_t *     Ntl_ManCollectCiNames( Ntl_Man_t * p );
 extern Vec_Ptr_t *     Ntl_ManCollectCoNames( Ntl_Man_t * p );
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index f278cba8..69219282 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -277,7 +277,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
         Vec_PtrPush( p->vCos, pNet );
         Aig_ObjCreatePo( p->pAig, pNet->pCopy );
     }
-    // visit the nodes starting from latch inputs outputs
+    // visit the nodes starting from latch inputs 
     Ntl_ModelForEachLatch( pRoot, pObj, i )
     {
         pNet = Ntl_ObjFanin0(pObj);
@@ -777,21 +777,22 @@ Nwk_Obj_t * Ntl_ManExtractNwk_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, Nwk_Man_t *
   SeeAlso     []
 
 ***********************************************************************/
-Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig )
+Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pManTime )
 {
     Nwk_Man_t * pNtk;
     Nwk_Obj_t * pNode;
     Ntl_Mod_t * pRoot;
-    Ntl_Net_t * pNet;
+    Ntl_Net_t * pNet, * pNetSimple;
     Ntl_Obj_t * pObj;
     Aig_Obj_t * pAnd;
     Vec_Int_t * vCover, * vMemory;
     int i, k;
     pRoot = Ntl_ManRootModel( p );
-    assert( Ntl_ModelBoxNum(pRoot) == 0 );
-    assert( Ntl_ModelLatchNum(pRoot) == 0 );
-    assert( Ntl_ModelPiNum(pRoot) == Aig_ManPiNum(pAig) );
-    assert( Ntl_ModelPoNum(pRoot) == Aig_ManPoNum(pAig) );
+    if ( Ntl_ModelGetFaninMax(pRoot) > 6 )
+    {
+        printf( "The network contains logic nodes with more than 6 inputs.\n" );
+        return NULL;
+    }
     vCover = Vec_IntAlloc( 100 );
     vMemory = Vec_IntAlloc( 1 << 16 );
     // count the number of fanouts of each net
@@ -803,30 +804,59 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig )
     Ntl_ModelForEachObj( pRoot, pObj, i )
         Ntl_ObjForEachFanin( pObj, pNet, k )
             Ntl_NetIncrementRefs( pNet );
+    // remember netlist objects int the AIG nodes
+    if ( pManTime != NULL ) // logic netlist
+    {
+        assert( Ntl_ModelPiNum(pRoot) == Aig_ManPiNum(pAig) );
+        assert( Ntl_ModelPoNum(pRoot) == Aig_ManPoNum(pAig) );
+        Aig_ManForEachPi( pAig, pAnd, i )
+            pAnd->pData = Ntl_ObjFanout0( Ntl_ModelPi(pRoot, i) );
+        Aig_ManForEachPo( pAig, pAnd, i )
+            pAnd->pData = Ntl_ObjFanin0(Ntl_ModelPo(pRoot, i) );
+    }
+    else // real netlist
+    {
+        assert( p->vCis && p->vCos );
+        Aig_ManForEachPi( pAig, pAnd, i )
+            pAnd->pData = Vec_PtrEntry( p->vCis, i );
+        Aig_ManForEachPo( pAig, pAnd, i )
+            pAnd->pData = Vec_PtrEntry( p->vCos, i );
+    }
     // construct the network
     pNtk = Nwk_ManAlloc();
     pNtk->pName = Aig_UtilStrsav( pAig->pName );
     pNtk->pSpec = Aig_UtilStrsav( pAig->pSpec );
-    Aig_ManSetPioNumbers( pAig );
+//    Aig_ManSetPioNumbers( pAig );
     Aig_ManForEachObj( pAig, pAnd, i )
     {
         if ( Aig_ObjIsPi(pAnd) )
         {
-            pObj = Ntl_ModelPi( pRoot, Aig_ObjPioNum(pAnd) );
-            pNet = Ntl_ObjFanout0(pObj);
+//            pObj = Ntl_ModelPi( pRoot, Aig_ObjPioNum(pAnd) );
+//            pNet = Ntl_ObjFanout0(pObj);
+            pNet = pAnd->pData;
             pNet->fMark = 1;
             pNet->pCopy = Nwk_ManCreateCi( pNtk, (int)(long)pNet->pCopy ); 
         }
         else if ( Aig_ObjIsPo(pAnd) )
         {
-            pObj = Ntl_ModelPo( pRoot, Aig_ObjPioNum(pAnd) );
-            pNet = Ntl_ObjFanin0(pObj);
-            pNet->pCopy = Ntl_ManExtractNwk_rec( p, pNet, pNtk, vCover, vMemory ); 
+//            pObj = Ntl_ModelPo( pRoot, Aig_ObjPioNum(pAnd) );
+//            pNet = Ntl_ObjFanin0(pObj);
+            pNet = pAnd->pData;
             pNode = Nwk_ManCreateCo( pNtk );
-            Nwk_ObjAddFanin( pNode, pNet->pCopy );
+            if ( (pNetSimple = Ntl_ModelFindSimpleNet( pNet )) )
+            {
+                pNetSimple->pCopy = Ntl_ManExtractNwk_rec( p, pNetSimple, pNtk, vCover, vMemory ); 
+                Nwk_ObjAddFanin( pNode, pNetSimple->pCopy );
+                pNode->fInvert = Kit_PlaIsInv( pNet->pDriver->pSop );
+            }
+            else
+            {
+                pNet->pCopy = Ntl_ManExtractNwk_rec( p, pNet, pNtk, vCover, vMemory ); 
+                Nwk_ObjAddFanin( pNode, pNet->pCopy );
+            }
         }
     }
-    Aig_ManCleanPioNumbers( pAig );
+//    Aig_ManCleanPioNumbers( pAig );
     Ntl_ModelForEachNet( pRoot, pNet, i )
     {
         pNet->pCopy = NULL;
@@ -835,6 +865,10 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig )
     Vec_IntFree( vCover );
     Vec_IntFree( vMemory );
     // create timing manager from the current design
+    if ( pManTime )
+        pNtk->pManTime = Tim_ManDup( pManTime, 0 );
+    else
+        pNtk->pManTime = Tim_ManDup( p->pManTime, 0 );
     return pNtk;
 }
 
@@ -861,6 +895,16 @@ Nwk_Man_t * Ntl_ManReadNwk( char * pFileName, Aig_Man_t * pAig, Tim_Man_t * pMan
         return NULL;
     }
     pRoot = Ntl_ManRootModel( pNtl );
+    if ( Ntl_ModelLatchNum(pRoot) != 0 )
+    {
+        printf( "Ntl_ManReadNwk(): The input network has %d registers.\n", Ntl_ModelLatchNum(pRoot) );
+        return NULL;
+    }
+    if ( Ntl_ModelBoxNum(pRoot) != 0 )
+    {
+        printf( "Ntl_ManReadNwk(): The input network has %d boxes.\n", Ntl_ModelBoxNum(pRoot) );
+        return NULL;
+    }
     if ( Ntl_ModelPiNum(pRoot) != Aig_ManPiNum(pAig) )
     {
         printf( "Ntl_ManReadNwk(): The number of primary inputs does not match (%d and %d).\n",
@@ -873,10 +917,8 @@ Nwk_Man_t * Ntl_ManReadNwk( char * pFileName, Aig_Man_t * pAig, Tim_Man_t * pMan
             Ntl_ModelPoNum(pRoot), Aig_ManPoNum(pAig) );
         return NULL;
     }
-    pNtk = Ntl_ManExtractNwk( pNtl, pAig );
+    pNtk = Ntl_ManExtractNwk( pNtl, pAig, pManTime );
     Ntl_ManFree( pNtl );
-    if ( pManTime )
-        pNtk->pManTime = Tim_ManDup( pManTime, 0 );
     return pNtk;
 }
 
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index 83586e42..6849889d 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -51,6 +51,51 @@ int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot )
 
 /**Function*************************************************************
 
+  Synopsis    [Reads the maximum number of fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelGetFaninMax( Ntl_Mod_t * pRoot )
+{
+    Ntl_Obj_t * pNode;
+    int i, nFaninsMax = 0;
+    Ntl_ModelForEachNode( pRoot, pNode, i )
+    {
+        if ( nFaninsMax < Ntl_ObjFaninNum(pNode) )
+            nFaninsMax = Ntl_ObjFaninNum(pNode);
+    }
+    return nFaninsMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [If the net is driven by an inv/buf, returns its fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Net_t * Ntl_ModelFindSimpleNet( Ntl_Net_t * pNetCo )
+{
+    // skip the case when the net is not driven by a node
+    if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
+        return NULL;
+    // skip the case when the node is not an inv/buf
+    if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 )
+        return NULL;
+    return Ntl_ObjFanin0(pNetCo->pDriver);
+}
+
+/**Function*************************************************************
+
   Synopsis    [Connects COs to the internal nodes other than inv/bufs.]
 
   Description [Should be called immediately after reading from file.]
diff --git a/src/aig/nwk/nwkDfs.c b/src/aig/nwk/nwkDfs.c
index ed19f71a..90bab0dc 100644
--- a/src/aig/nwk/nwkDfs.c
+++ b/src/aig/nwk/nwkDfs.c
@@ -267,8 +267,8 @@ Vec_Vec_t * Nwk_ManLevelize( Nwk_Man_t * pNtk )
     vLevels = Vec_VecStart( nLevels + 1 );
     Nwk_ManForEachNode( pNtk, pObj, i )
     {
-        assert( (int)pObj->tArrival <= nLevels );
-        Vec_VecPush( vLevels, (int)pObj->tArrival, pObj );
+        assert( Nwk_ObjLevel(pObj) <= nLevels );
+        Vec_VecPush( vLevels, Nwk_ObjLevel(pObj), pObj );
     }
     return vLevels;
 }
diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c
index aeebac3f..55c5354c 100644
--- a/src/aig/nwk/nwkMan.c
+++ b/src/aig/nwk/nwkMan.c
@@ -118,6 +118,7 @@ void Nwk_ManPrintLutSizes( Nwk_Man_t * p, If_Lib_t * pLutLib )
 int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl )
 {
     extern void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, void * pNtl, char * pFileName );
+    extern void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames );
     static struct ParStruct {
         char * pName;  // name of the best saved network
         int    Depth;  // depth of the best saved network
@@ -154,6 +155,7 @@ int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl )
         ParsBest.nPos  = ParsNew.nPos;
         // writ the network
         Ioa_WriteBlifLogic( pNtk, pNtl, "best.blif" );
+//        Nwk_ManDumpBlif( pNtk, "best_map.blif", NULL, NULL );
         return 1;
     }
     return 0;
@@ -211,6 +213,8 @@ void Nwk_ManPrintStats( Nwk_Man_t * pNtk, If_Lib_t * pLutLib, int fSaveBest, int
         char * pNameGen = pNtk->pSpec? Nwk_FileNameGeneric( pNtk->pSpec ) : "nameless_";
         sprintf( Buffer, "%s_dump.blif", pNameGen );
         Ioa_WriteBlifLogic( pNtk, pNtl, Buffer );
+//        sprintf( Buffer, "%s_dump_map.blif", pNameGen );
+//        Nwk_ManDumpBlif( pNtk, Buffer, NULL, NULL );
         if ( pNtk->pSpec ) free( pNameGen );
     }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d101cfbc..492fefae 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14874,16 +14874,21 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pFile;
     char * pFileName;
     int c;
+    int fMapped;
     extern void * Ioa_ReadBlif( char * pFileName, int fCheck );
     extern Aig_Man_t * Ntl_ManExtract( void * p );
-
+    extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime );
 
     // set defaults
+    fMapped = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'm':
+            fMapped ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -14916,12 +14921,18 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Read(): AIG extraction has failed.\n" );
         return 1;
     }
-
+    if ( fMapped )
+    {
+        pAbc->pAbc8Nwk = Ntl_ManExtractNwk( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, NULL );
+        if ( pAbc->pAbc8Nwk == NULL )
+            printf( "Abc_CommandAbc8Read(): Warning! Mapped network is not extracted.\n" );
+    }
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *r [-h]\n" );
+    fprintf( stdout, "usage: *r [-mh]\n" );
     fprintf( stdout, "\t        reads the design with whiteboxes\n" );
+    fprintf( stdout, "\t-m    : toggle extracting mapped network [default = %s]\n", fMapped? "yes": "no" );
     fprintf( stdout, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -15365,6 +15376,11 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pAbc8Nwk )
     {
+        if ( pAbc->pAbc8Lib == NULL )
+        {
+            printf( "LUT library is not given. Using default 6-LUT library.\n" );
+            pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
+        }
         printf( "MAPPED:  " );
         Nwk_ManPrintStats( pAbc->pAbc8Nwk, pAbc->pAbc8Lib, fSaveBest, fDumpResult, pAbc->pAbc8Ntl );
     }
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 74557a54..bbe81cfd 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -88,7 +88,10 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     {
         // recompute the parameters of the best cut
         pCut->Delay = If_CutDelay( p, pCut );
-        assert( pCut->Delay <= pObj->Required + p->fEpsilon );
+//        assert( pCut->Delay <= pObj->Required + p->fEpsilon );
+        if ( pCut->Delay > pObj->Required + p->fEpsilon )
+            printf( "If_ObjPerformMappingAnd(): Warning! Delay of node %d (%f) exceeds the required times (%f).\n", 
+                pObj->Id, pCut->Delay, pObj->Required + p->fEpsilon );
         pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
         if ( p->pPars->fEdge )
             pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );