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

2 files changed, 32 insertions, 8 deletions

diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
index 04d2ebee..40a5a6ca 100644
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -1020,13 +1020,15 @@ 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 )
+// this procedure takes TT and input arrival times (pArrTimeProfile) and return the smallest output arrival time;
+// it also returns the pin-to-pin delays (pPerm) between each cut leaf and the cut output and the cut area cost (Cost)
+// the area cost should not exceed 2048, if the cut is implementable; otherwise, it should be ABC_INFINITY
+int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * pPerm, int * Cost )
 {
-    return 0;
+    *Cost = ABC_INFINITY;
+    return ABC_INFINITY;
 }
-// this procedure returns a new node whose output in terms of the given fanins whose output 
+// this procedure returns a new node whose output in terms of the given fanins 
 // 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 )
 {
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index c764c74c..7e102312 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -29,7 +29,7 @@ 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    Abc_ExactDelayCost( int nVars, word * pTruth, int * pArrTimeProfile );
+extern int    Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * pPerm, int * Cost );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -149,7 +149,18 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         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) ); 
+        {
+            int Cost = 0;
+            pCut->fUser = 1;
+            pCut->Delay = (float)Abc_ExactDelayCost( If_CutTruthW(p, pCut), If_CutLeaveNum(pCut), If_CutArrTimeProfile(p, pCut), If_CutPerm(pCut), &Cost ); 
+            if ( Cost == ABC_INFINITY )
+            {
+                for ( v = 0; v < If_CutLeaveNum(pCut); v++ )
+                    If_CutPerm(pCut)[v] = IF_BIG_CHAR;
+                pCut->Cost = IF_COST_MAX;
+                pCut->fUseless = 1;
+            }
+        }
         else if ( p->pPars->fDelayOptLut )
             pCut->Delay = If_CutLutBalanceEval( p, pCut );
         else if( p->pPars->nGateSize > 0 )
@@ -362,7 +373,18 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         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) ); 
+        {
+            int Cost = 0;
+            pCut->fUser = 1;
+            pCut->Delay = (float)Abc_ExactDelayCost( If_CutTruthW(p, pCut), If_CutLeaveNum(pCut), If_CutArrTimeProfile(p, pCut), If_CutPerm(pCut), &Cost ); 
+            if ( Cost == ABC_INFINITY )
+            {
+                for ( v = 0; v < If_CutLeaveNum(pCut); v++ )
+                    If_CutPerm(pCut)[v] = IF_BIG_CHAR;
+                pCut->Cost = IF_COST_MAX;
+                pCut->fUseless = 1;
+            }
+        }
         else if ( p->pPars->fDelayOptLut )
             pCut->Delay = If_CutLutBalanceEval( p, pCut );
         else if( p->pPars->nGateSize > 0 )