Infrastructure for using the results of exact SAT-based synthesis during mapping.

8 files changed, 106 insertions, 31 deletions

diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 9a72f576..26f549d0 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -926,7 +926,7 @@ Gia_Man_t * Gia_ManFromIfAig( If_Man_t * pIfMan )
     Vec_Int_t * vAig;
     int i, k;
     assert( pIfMan->pPars->pLutStruct == NULL );
-    assert( pIfMan->pPars->fDelayOpt || pIfMan->pPars->fDsdBalance || pIfMan->pPars->fUserRecLib );
+    assert( pIfMan->pPars->fDelayOpt || pIfMan->pPars->fDsdBalance || pIfMan->pPars->fUserRecLib || pIfMan->pPars->fUserSesLib );
     // create new manager
     pNew = Gia_ManStart( If_ManObjNum(pIfMan) );
     Gia_ManHashAlloc( pNew );
@@ -1783,8 +1783,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
             pCutBest = If_ObjCutBest( pIfObj );
             // perform sorting of cut leaves by delay, so that the slowest pin drives the fastest input of the LUT
             if ( !pIfMan->pPars->fUseTtPerm && !pIfMan->pPars->fDelayOpt && !pIfMan->pPars->fDelayOptLut && !pIfMan->pPars->fDsdBalance && 
-                 !pIfMan->pPars->pLutStruct && !pIfMan->pPars->fUserRecLib && !pIfMan->pPars->nGateSize && !pIfMan->pPars->fEnableCheck75 && 
-                 !pIfMan->pPars->fEnableCheck75u && !pIfMan->pPars->fEnableCheck07 && !pIfMan->pPars->fUseDsdTune && 
+                 !pIfMan->pPars->pLutStruct && !pIfMan->pPars->fUserRecLib && !pIfMan->pPars->fUserSesLib && !pIfMan->pPars->nGateSize && 
+                 !pIfMan->pPars->fEnableCheck75 && !pIfMan->pPars->fEnableCheck75u && !pIfMan->pPars->fEnableCheck07 && !pIfMan->pPars->fUseDsdTune && 
                  !pIfMan->pPars->fUseCofVars && !pIfMan->pPars->fUseAndVars )
                 If_CutRotatePins( pIfMan, pCutBest );
             // collect leaves of the best cut
@@ -2117,7 +2117,7 @@ Gia_Man_t * Gia_ManPerformMappingInt( Gia_Man_t * p, If_Par_t * pPars )
     ABC_FREE( p->pCellStr );
     Vec_IntFreeP( &p->vConfigs );
     // disable cut minimization when GIA strucure is needed
-    if ( !pPars->fDelayOpt && !pPars->fDelayOptLut && !pPars->fDsdBalance && !pPars->fUserRecLib && !pPars->fDeriveLuts && !pPars->fUseDsd && !pPars->fUseTtPerm )
+    if ( !pPars->fDelayOpt && !pPars->fDelayOptLut && !pPars->fDsdBalance && !pPars->fUserRecLib && !pPars->fUserSesLib && !pPars->fDeriveLuts && !pPars->fUseDsd && !pPars->fUseTtPerm )
         pPars->fCutMin = 0;
     // translate into the mapper
     pIfMan = Gia_ManToIf( p, pPars );    
@@ -2142,7 +2142,7 @@ Gia_Man_t * Gia_ManPerformMappingInt( Gia_Man_t * p, If_Par_t * pPars )
             Abc_Print( 0, "Switching activity computation for designs with boxes is disabled.\n" );
     }
     if ( p->pManTime )
-        pIfMan->pManTim = Tim_ManDup( (Tim_Man_t *)p->pManTime, pPars->fDelayOpt || pPars->fDelayOptLut || pPars->fDsdBalance || pPars->fUserRecLib );
+        pIfMan->pManTim = Tim_ManDup( (Tim_Man_t *)p->pManTime, pPars->fDelayOpt || pPars->fDelayOptLut || pPars->fDsdBalance || pPars->fUserRecLib || pPars->fUserSesLib );
 //    Tim_ManPrint( pIfMan->pManTim );
     if ( !If_ManPerformMapping( pIfMan ) )
     {
@@ -2150,7 +2150,7 @@ Gia_Man_t * Gia_ManPerformMappingInt( Gia_Man_t * p, If_Par_t * pPars )
         return NULL;
     }
     // transform the result of mapping into the new network
-    if ( pIfMan->pPars->fDelayOpt || pIfMan->pPars->fDsdBalance || pIfMan->pPars->fUserRecLib )
+    if ( pIfMan->pPars->fDelayOpt || pIfMan->pPars->fDsdBalance || pIfMan->pPars->fUserRecLib || pIfMan->pPars->fUserSesLib )
         pNew = Gia_ManFromIfAig( pIfMan );
     else
         pNew = Gia_ManFromIfLogic( pIfMan );
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 78313e8f..fcb2d989 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -643,6 +643,9 @@ extern ABC_DLL int                Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkIsAcyclicWithBoxes( Abc_Ntk_t * pNtk );
 extern ABC_DLL Vec_Ptr_t *        Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis );
 /*=== abcExact.c ==========================================================*/
+extern ABC_DLL int                Abc_ExactInputNum();
+extern ABC_DLL int                Abc_ExactIsRunning();
+extern ABC_DLL Abc_Obj_t *        Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins );
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose );
 /*=== abcFanio.c ==========================================================*/
 extern ABC_DLL void               Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 244255da..703fd63d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -16495,7 +16495,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     If_ManSetDefaultPars( pPars );
     pPars->pLutLib = (If_LibLut_t *)Abc_FrameReadLibLut();
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRNTXYDEWSqaflepmrsdbgxyojiktncvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRNTXYDEWSqaflepmrsdbgxyuojiktncvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -16700,6 +16700,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'y':
             pPars->fUserRecLib ^= 1;
             break;
+        case 'u':
+            pPars->fUserSesLib ^= 1;
+            break;
         case 'o':
             pPars->fUseBuffs ^= 1;
             break;
@@ -16843,7 +16846,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->fExpRed = 0;
     }
     // modify the subgraph recording
-    if ( pPars->fUserRecLib )
+    if ( pPars->fUserRecLib || pPars->fUserSesLib )
     {
         pPars->fTruth      =  1;
         pPars->fCutMin     =  1;
@@ -16921,6 +16924,20 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
     }
+
+    if ( pPars->fUserSesLib )
+    {
+        if ( !Abc_ExactIsRunning() )
+        {
+            printf( "LMS manager is not running (use \"rec_start3\").\n" );
+            return 0;
+        }
+        if ( Abc_ExactInputNum() != pPars->nLutSize )
+        {
+            printf( "The number of library inputs (%d) different from the K parameters (%d).\n", Abc_ExactInputNum(), pPars->nLutSize );
+            return 0;
+        }
+    }
  
     // complain if truth tables are requested but the cut size is too large
     if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )
@@ -16984,7 +17001,7 @@ usage:
         sprintf(LutSize, "library" );
     else
         sprintf(LutSize, "%d", pPars->nLutSize );
-    Abc_Print( -2, "usage: if [-KCFAGRNTXY num] [-DEW float] [-S str] [-qarlepmsdbgxyojiktncvh]\n" );
+    Abc_Print( -2, "usage: if [-KCFAGRNTXY num] [-DEW float] [-S str] [-qarlepmsdbgxyuojiktncvh]\n" );
     Abc_Print( -2, "\t           performs FPGA technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     Abc_Print( -2, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -17013,6 +17030,7 @@ usage:
     Abc_Print( -2, "\t-g       : toggles delay optimization by SOP balancing [default = %s]\n", pPars->fDelayOpt? "yes": "no" );
     Abc_Print( -2, "\t-x       : toggles delay optimization by DSD balancing [default = %s]\n", pPars->fDsdBalance? "yes": "no" );
     Abc_Print( -2, "\t-y       : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" );
+    Abc_Print( -2, "\t-u       : toggles delay optimization with SAT-based library [default = %s]\n", pPars->fUserSesLib? "yes": "no" );
     Abc_Print( -2, "\t-o       : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" );
     Abc_Print( -2, "\t-j       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
     Abc_Print( -2, "\t-i       : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" );
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
index 1bb7973a..04d2ebee 100644
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -1003,6 +1003,36 @@ void Abc_ExactTest( int fVerbose )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [APIs for integraging with the mapper.]
+
+***********************************************************************/
+// may need to have a static pointer to the SAT-based synthesis engine and/or loaded library
+// this procedure should return 1, if the engine/library are available, and 0 otherwise
+int Abc_ExactIsRunning()
+{
+    return 0;
+}
+// this procedure returns the number of inputs of the library
+// for example, somebody may try to map into 10-cuts while the library only contains 8-functions
+int Abc_ExactInputNum()
+{
+    return 0;
+}
+// this procedure takes input arrival times (pArrTimeProfile) and 
+// return the output smallest possible output arrival time
+int Abc_ExactDelayCost( int nVars, word * pTruth, int * pArrTimeProfile )
+{
+    return 0;
+}
+// this procedure returns a new node whose output in terms of the given fanins whose output 
+// has the smallest possible arrival time (in agreement with the above Abc_ExactDelayCost)
+Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins )
+{
+    return NULL;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index c45eaec5..85164d04 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -116,7 +116,7 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     pPars->pTimesReq = Abc_NtkGetCoRequiredFloats(pNtk);
 
     // update timing info to reflect logic level
-    if ( (pPars->fDelayOpt || pPars->fDsdBalance || pPars->fUserRecLib) && pNtk->pManTime )
+    if ( (pPars->fDelayOpt || pPars->fDsdBalance || pPars->fUserRecLib || pPars->fUserSesLib) && pNtk->pManTime )
     {
         int c;
         if ( pNtk->AndGateDelay == 0.0 )
@@ -318,7 +318,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     // create the new network
     if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
-    else if ( pIfMan->pPars->fUseSops || pIfMan->pPars->nGateSize > 0 )
+    else if ( pIfMan->pPars->fUseSops || pIfMan->pPars->fUserSesLib || pIfMan->pPars->nGateSize > 0 )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
     else
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
@@ -445,12 +445,20 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
         return pNodeNew;
     assert( pIfObj->Type == IF_AND );
     // get the parameters of the best cut
+    pCutBest = If_ObjCutBest( pIfObj );
+    if ( pIfMan->pPars->fUserSesLib )
+    {
+        // create the subgraph composed of Abc_Obj_t nodes based on the given cut
+        Abc_Obj_t * pFanins[IF_MAX_FUNC_LUTSIZE];
+        If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
+            pFanins[i] = Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover);
+        return Abc_ExactBuildNode( If_CutTruthW(pIfMan, pCutBest), If_CutLeaveNum(pCutBest), If_CutArrTimeProfile(pIfMan, pCutBest), pFanins );
+    }
     // create a new node 
     pNodeNew = Abc_NtkCreateNode( pNtkNew );
-    pCutBest = If_ObjCutBest( pIfObj );
-//    printf( "%d 0x%02X %d\n", pCutBest->nLeaves, 0xff & *If_CutTruth(pCutBest), pIfMan->pPars->pFuncCost(pCutBest) );
 //    if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays )
-    if ( !pIfMan->pPars->fDelayOpt && !pIfMan->pPars->fDelayOptLut && !pIfMan->pPars->fDsdBalance && !pIfMan->pPars->fUseTtPerm && !pIfMan->pPars->pLutStruct && !pIfMan->pPars->fUserRecLib && !pIfMan->pPars->nGateSize )
+    if ( !pIfMan->pPars->fDelayOpt && !pIfMan->pPars->fDelayOptLut && !pIfMan->pPars->fDsdBalance && !pIfMan->pPars->fUseTtPerm && 
+         !pIfMan->pPars->pLutStruct && !pIfMan->pPars->fUserRecLib && !pIfMan->pPars->fUserSesLib && !pIfMan->pPars->nGateSize )
         If_CutRotatePins( pIfMan, pCutBest );
     if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
     {
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 0282a1bd..ca7e0411 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -124,6 +124,7 @@ struct If_Par_t_
     int                fDelayOptLut;  // delay optimization for LUTs
     int                fDsdBalance;   // special delay optimization
     int                fUserRecLib;   // use recorded library
+    int                fUserSesLib;   // use SAT-based synthesis
     int                fBidec;        // use bi-decomposition
     int                fUse34Spec;    // use specialized matching
     int                fUseBat;       // use one specialized feature
@@ -263,6 +264,7 @@ struct If_Man_t_
     int                nBestCutSmall[2];
     int                nCountNonDec[2];
     Vec_Int_t *        vCutData;      // cut data storage
+    int                pArrTimeProfile[IF_MAX_FUNC_LUTSIZE];
 
     // timing manager
     Tim_Man_t *        pManTim;
@@ -616,6 +618,7 @@ extern void            If_ManDerefNodeCutSet( If_Man_t * p, If_Obj_t * pObj );
 extern void            If_ManDerefChoiceCutSet( If_Man_t * p, If_Obj_t * pObj );
 extern void            If_ManSetupSetAll( If_Man_t * p, int nCrossCut );
 /*=== ifMap.c =============================================================*/
+extern int *           If_CutArrTimeProfile( If_Man_t * p, If_Cut_t * pCut );
 extern void            If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess, int fFirst );
 extern void            If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess );
 extern int             If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPreprocess, int fFirst, char * pLabel );
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 9e0c5a70..9b8d75ad 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -753,7 +753,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
 
     if ( !pCut->fUseless && 
          (p->pPars->fUseDsd || p->pPars->fUseBat || 
-          p->pPars->pLutStruct || p->pPars->fUserRecLib || 
+          p->pPars->pLutStruct || p->pPars->fUserRecLib || p->pPars->fUserSesLib || 
           p->pPars->fEnableCheck07 || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || 
           p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || p->pPars->fEnableCheck75u) )
     {
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index c4053f52..c764c74c 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -28,7 +28,8 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 
 extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars );
-extern int    If_CutDelayRecCost3(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj);
+extern int    If_CutDelayRecCost3( If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj );
+extern int    Abc_ExactDelayCost( int nVars, word * pTruth, int * pArrTimeProfile );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -80,6 +81,25 @@ float If_CutDelaySpecial( If_Man_t * p, If_Cut_t * pCut, int fCarry )
     return Delay;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns arrival time profile of the cut.]
+
+  Description [The procedure returns static storage, which should not be
+  deallocated and is only valid until before the procedure is called again.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * If_CutArrTimeProfile( If_Man_t * p, If_Cut_t * pCut )
+{
+    int i;
+    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+        p->pArrTimeProfile[i] = (int)If_ObjCutBest(If_CutLeaf(p, pCut, i))->Delay;
+    return p->pArrTimeProfile;
+}
 
 /**Function*************************************************************
 
@@ -99,7 +119,8 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     If_Cut_t * pCut0R, * pCut1R;
     int fFunc0R, fFunc1R;
     int i, k, v, iCutDsd, fChange;
-    int fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || p->pPars->pLutStruct != NULL;
+    int fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUserSesLib || 
+        p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || p->pPars->pLutStruct != NULL;
     int fUseAndCut = (p->pPars->nAndDelay > 0) || (p->pPars->nAndArea > 0);
     assert( !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 );
     assert( !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 );
@@ -127,6 +148,8 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
             pCut->Delay = If_CutDsdBalanceEval( p, pCut, NULL );
         else if ( p->pPars->fUserRecLib )
             pCut->Delay = If_CutDelayRecCost3( p, pCut, pObj ); 
+        else if ( p->pPars->fUserSesLib )
+            pCut->Delay = Abc_ExactDelayCost( If_CutLeaveNum(pCut), If_CutTruthW(p, pCut), If_CutArrTimeProfile(p, pCut) ); 
         else if ( p->pPars->fDelayOptLut )
             pCut->Delay = If_CutLutBalanceEval( p, pCut );
         else if( p->pPars->nGateSize > 0 )
@@ -333,23 +356,13 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
             continue;
         // check if the cut satisfies the required times
         if ( p->pPars->fDelayOpt )
-        {
             pCut->Delay = If_CutSopBalanceEval( p, pCut, NULL );
-//            if ( pCut->Delay >= pObj->Level && pCut->nLeaves > 2 )
-//                pCut->Delay += 1;
-        }
         else if ( p->pPars->fDsdBalance )
-        {
             pCut->Delay = If_CutDsdBalanceEval( p, pCut, NULL );
-//            if ( pCut->Delay >= pObj->Level && pCut->nLeaves > 2 )
-//                pCut->Delay += 1;
-        }
         else if ( p->pPars->fUserRecLib )
-        {
             pCut->Delay = If_CutDelayRecCost3( p, pCut, pObj ); 
-//            if ( pCut->Delay >= pObj->Level && pCut->nLeaves > 2 )
-//                pCut->Delay += 1;
-        }
+        else if ( p->pPars->fUserSesLib )
+            pCut->Delay = Abc_ExactDelayCost( If_CutLeaveNum(pCut), If_CutTruthW(p, pCut), If_CutArrTimeProfile(p, pCut) ); 
         else if ( p->pPars->fDelayOptLut )
             pCut->Delay = If_CutLutBalanceEval( p, pCut );
         else if( p->pPars->nGateSize > 0 )
@@ -378,7 +391,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     if ( !fPreprocess || pCutSet->ppCuts[0]->Delay <= pObj->Required + p->fEpsilon )
     {
         If_CutCopy( p, If_ObjCutBest(pObj), pCutSet->ppCuts[0] );
-        if(p->pPars->fUserRecLib)
+        if ( p->pPars->fUserRecLib || p->pPars->fUserSesLib )
             assert(If_ObjCutBest(pObj)->Cost < IF_COST_MAX && If_ObjCutBest(pObj)->Delay < ABC_INFINITY);
     }
     // add the trivial cut to the set
@@ -421,7 +434,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
     If_Set_t * pCutSet;
     If_Obj_t * pTemp;
     If_Cut_t * pCutTemp, * pCut;
-    int i, fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUse34Spec;
+    int i, fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUserSesLib || p->pPars->fUse34Spec;
     assert( pObj->pEquiv != NULL );
 
     // prepare