Merged in msoeken/abc-exact (pull request #35)

Updates to delay-estimation API with exact synthesis

1 files changed, 192 insertions, 49 deletions

diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
index 94325f4a..d739118a 100644
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -50,6 +50,10 @@ static word s_Truths8[32] = {
     ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF)
 };
 
+#define ABC_EXACT_SOL_NVARS  0
+#define ABC_EXACT_SOL_NFUNC  1
+#define ABC_EXACT_SOL_NGATES 2
+
 typedef struct Ses_Man_t_ Ses_Man_t;
 struct Ses_Man_t_
 {
@@ -120,9 +124,15 @@ struct Ses_TruthEntry_t_
 typedef struct Ses_Store_t_ Ses_Store_t;
 struct Ses_Store_t_
 {
+    int                fMakeAIG;                       /* create AIG instead of general network */
     int                fVerbose;                       /* be verbose */
     int                nBTLimit;                       /* conflict limit */
+    int                nEntriesCount;                  /* number of entries */
     Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */
+
+    unsigned long      nCutCount;
+    unsigned long      pCutCount[9];
+    unsigned long      nCacheHit;
 };
 
 static Ses_Store_t * s_pSesStore = NULL;
@@ -155,13 +165,19 @@ static int Abc_NormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int * ma
     return delta;
 }
 
-static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fVerbose )
+static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fMakeAIG, int fVerbose )
 {
     Ses_Store_t * pStore = ABC_CALLOC( Ses_Store_t, 1 );
-    pStore->fVerbose = fVerbose;
-    pStore->nBTLimit = nBTLimit;
+    pStore->fMakeAIG      = fMakeAIG;
+    pStore->fVerbose      = fVerbose;
+    pStore->nBTLimit      = nBTLimit;
+    pStore->nEntriesCount = 0;
     memset( pStore->pEntries, 0, SES_STORE_TABLE_SIZE );
 
+    pStore->nCutCount = 0;
+    memset( pStore->pCutCount, 0, 9 );
+    pStore->nCacheHit = 0;
+
     return pStore;
 }
 
@@ -294,6 +310,7 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr
 
         /* item has been added */
         fAdded = 1;
+        pStore->nEntriesCount++;
     }
     else
         /* item was already present */
@@ -350,6 +367,85 @@ char * Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int *
     return pTiEntry->pNetwork;
 }
 
+static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename )
+{
+    int i;
+    Ses_TruthEntry_t * pTEntry;
+    Ses_TimesEntry_t * pTiEntry;
+    FILE * pFile;
+
+    pFile = fopen( pFilename, "wb" );
+    if (pFile == NULL)
+    {
+        printf( "cannot open file \"%s\" for writing\n", pFilename );
+        return;
+    }
+
+    fwrite( &pStore->nEntriesCount, sizeof( int ), 1, pFile );
+
+    for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i )
+        if ( pStore->pEntries[i] )
+        {
+            pTEntry = pStore->pEntries[i];
+
+            while ( pTEntry )
+            {
+                pTiEntry = pTEntry->head;
+                while ( pTiEntry )
+                {
+                    fwrite( pTEntry->pTruth, sizeof( word ), 4, pFile );
+                    fwrite( &pTEntry->nVars, sizeof( int ), 1, pFile );
+                    fwrite( pTiEntry->pArrTimeProfile, sizeof( int ), 8, pFile );
+                    fwrite( pTiEntry->pNetwork, sizeof( char ), 3 + 4 * pTiEntry->pNetwork[ABC_EXACT_SOL_NGATES] + 2 + pTiEntry->pNetwork[ABC_EXACT_SOL_NVARS], pFile );
+                    pTiEntry = pTiEntry->next;
+                }
+                pTEntry = pTEntry->next;
+            }
+        }
+
+
+    fclose( pFile );
+}
+
+static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename )
+{
+    int i, nEntries;
+    word pTruth[4];
+    int nVars;
+    int pArrTimeProfile[8];
+    char pHeader[3];
+    char * pNetwork;
+    FILE * pFile;
+
+    pFile = fopen( pFilename, "rb" );
+    if (pFile == NULL)
+    {
+        printf( "cannot open file \"%s\" for reading\n", pFilename );
+        return;
+    }
+
+    fread( &nEntries, sizeof( int ), 1, pFile );
+
+    for ( i = 0; i < nEntries; ++i )
+    {
+        fread( pTruth, sizeof( word ), 4, pFile );
+        fread( &nVars, sizeof( int ), 1, pFile );
+        fread( pArrTimeProfile, sizeof( int ), 8, pFile );
+        fread( pHeader, sizeof( char ), 3, pFile );
+
+        pNetwork = ABC_CALLOC( char, 3 + 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS] );
+        pNetwork[0] = pHeader[0];
+        pNetwork[1] = pHeader[1];
+        pNetwork[2] = pHeader[2];
+
+        fread( pNetwork + 3, sizeof( char ), 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS], pFile );
+
+        Ses_StoreAddEntry( pStore, pTruth, nVars, pArrTimeProfile, pNetwork );
+    }
+
+    fclose( pFile );
+}
+
 static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fMakeAIG, int fVerbose )
 {
     int h, i;
@@ -524,7 +620,7 @@ static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int
     assert( value );
 }
 
-static void Ses_ManCreateClauses( Ses_Man_t * pSes )
+static int Ses_ManCreateClauses( Ses_Man_t * pSes )
 {
     extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 );
 
@@ -731,10 +827,13 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes )
                 {
                     pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
                     pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, pSes->nMaxDepth ), 1 );
-                    assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) );
+                    if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) )
+                        return 0;
                 }
         }
     }
+
+    return 1;
 }
 
 /**Function*************************************************************
@@ -798,9 +897,6 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes )
 //   delay:     maximum delay to output (taking arrival times into account, not normalized) or 0 if not specified
 //   pin[i]:    pin to pin delay to input i or 0 if not specified or if there is no connection to input i
 // NOTE: since outputs can only point to gates, delay and pin-to-pin times cannot be 0
-#define ABC_EXACT_SOL_NVARS  0
-#define ABC_EXACT_SOL_NFUNC  1
-#define ABC_EXACT_SOL_NGATES 2
 static char * Ses_ManExtractSolution( Ses_Man_t * pSes )
 {
     int nSol, h, i, j, k, l, aj, ak, d, nOp;
@@ -1129,7 +1225,8 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes )
             return 0;
 
         Ses_ManCreateVars( pSes, nGates );
-        Ses_ManCreateClauses( pSes );
+        if ( !Ses_ManCreateClauses( pSes ) )
+            return 0; /* proven UNSAT while creating clauses */
 
         switch ( Ses_ManSolve( pSes ) )
         {
@@ -1350,59 +1447,106 @@ int Abc_ExactInputNum()
     return 8;
 }
 // start exact store manager
-void Abc_ExactStart( int nBTLimit, int fVerbose )
+void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, const char * pFilename )
 {
     if ( !s_pSesStore )
-        s_pSesStore = Ses_StoreAlloc( nBTLimit, fVerbose );
+    {
+        s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose );
+        if ( pFilename )
+            Ses_StoreRead( s_pSesStore, pFilename );
+    }
     else
-        printf( "exact store manager already started\n" );
+        printf( "BMS manager already started\n" );
 }
 // stop exact store manager
-void Abc_ExactStop()
+void Abc_ExactStop( const char * pFilename )
 {
     if ( s_pSesStore )
+    {
+        if ( pFilename )
+            Ses_StoreWrite( s_pSesStore, pFilename );
         Ses_StoreClean( s_pSesStore );
+    }
     else
-        printf( "exact store manager has not been started\n" );
+        printf( "BMS manager has not been started\n" );
+}
+// show statistics about store manager
+void Abc_ExactStats()
+{
+    int i;
+
+    if ( !s_pSesStore )
+    {
+        printf( "BMS manager has not been started\n" );
+        return;
+    }
+
+    printf( "number of considered cuts :" );
+    for ( i = 2; i < 9; ++i )
+        printf( " %d = %lu  ", i, s_pSesStore->pCutCount[i] );
+    printf( " total = %lu\n", s_pSesStore->nCutCount );
+    printf( "cache hits                : %lu\n", s_pSesStore->nCacheHit );
+    printf( "number of entries         : %d\n", s_pSesStore->nEntriesCount );
 }
 // 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, int AigLevel )
 {
-    int i, l;
-    Ses_Man_t * pSes;
+    int i, l, fExists = 0;
+    Ses_Man_t * pSes = NULL;
     char * pSol = NULL, * p;
     int Delay = ABC_INFINITY, nMaxDepth;
     abctime timeStart;
 
     /* some checks */
-    assert( nVars >= 2 && nVars <= 8 );
+    if ( nVars < 2 || nVars > 8 )
+    {
+        printf( "invalid truth table size %d\n", nVars );
+        assert( 0 );
+    }
 
-    nMaxDepth = pArrTimeProfile[0];
-    for ( i = 1; i < nVars; ++i )
-        nMaxDepth = Abc_MaxInt( nMaxDepth, pArrTimeProfile[i] );
-    nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 );
+    /* statistics */
+    s_pSesStore->nCutCount++;
+    s_pSesStore->pCutCount[nVars]++;
 
-    timeStart = Abc_Clock();
+    pSol = Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile );
+    if ( pSol )
+    {
+        s_pSesStore->nCacheHit++;
+        fExists = 1;
+    }
+    else
+    {
+        nMaxDepth = pArrTimeProfile[0];
+        for ( i = 1; i < nVars; ++i )
+            nMaxDepth = Abc_MaxInt( nMaxDepth, pArrTimeProfile[i] );
+        nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 );
 
-    *Cost = ABC_INFINITY;
+        timeStart = Abc_Clock();
 
-    pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, 1 /* fMakeAIG */, s_pSesStore->fVerbose );
-    pSes->nBTLimit = s_pSesStore->nBTLimit;
+        *Cost = ABC_INFINITY;
 
-    while ( 1 ) /* there is improvement */
-    {
-        printf( "try with %d\n", pSes->nMaxDepth );
-        if ( Ses_ManFindMinimumSize( pSes ) )
+        pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, s_pSesStore->fMakeAIG, s_pSesStore->fVerbose );
+        pSes->nBTLimit = s_pSesStore->nBTLimit;
+
+        while ( 1 ) /* there is improvement */
         {
-            if ( pSol )
-                ABC_FREE( pSol );
-            pSol = Ses_ManExtractSolution( pSes );
-            pSes->nMaxDepth--;
+            if ( Ses_ManFindMinimumSize( pSes ) )
+            {
+                if ( pSol )
+                    ABC_FREE( pSol );
+                pSol = Ses_ManExtractSolution( pSes );
+                pSes->nMaxDepth--;
+            }
+            else
+                break;
         }
-        else
-            break;
+
+        pSes->timeTotal = Abc_Clock() - timeStart;
+
+        /* cleanup */
+        Ses_ManClean( pSes );
     }
 
     if ( pSol )
@@ -1414,15 +1558,10 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
             pPerm[l] = *p++;
 
         /* store solution */
-        if ( !Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol ) )
-            ABC_FREE( pSol ); /* store entry already exists, so free solution */
+        if ( !fExists )
+            Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol );
     }
 
-    pSes->timeTotal = Abc_Clock() - timeStart;
-
-    /* cleanup */
-    Ses_ManClean( pSes );
-
     return Delay;
 }
 // this procedure returns a new node whose output in terms of the given fanins
@@ -1430,7 +1569,7 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
 Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins )
 {
     char * pSol;
-    int i;
+    int i, j;
     char const * p;
     Abc_Obj_t * pObj;
     Vec_Ptr_t * pGates;
@@ -1468,6 +1607,11 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile,
         assert( *p == 2 ); /* binary gate */
         ++p;
 
+        /* invert truth table if we are last gate and inverted */
+        if ( i + 1 == pSol[ABC_EXACT_SOL_NGATES] && Abc_LitIsCompl( *( p + 2 ) ) )
+            for ( j = 0; j < 4; ++j )
+                pGateTruth[j] = ( pGateTruth[j] == '0' ) ? '1' : '0';
+
         pSopCover = Abc_SopFromTruthBin( pGateTruth );
         pObj = Abc_NtkCreateNode( pNtk );
         pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover );
@@ -1479,10 +1623,7 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile,
     }
 
     /* output */
-    if ( Abc_LitIsCompl( *p ) )
-        pObj = Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) ) );
-    else
-        pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) );
+    pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) );
 
     Vec_PtrFree( pGates );
 
@@ -1513,7 +1654,7 @@ void Abc_ExactStoreTest( int fVerbose )
     }
     Abc_NodeFreeNames( vNames );
 
-    Abc_ExactStart( 10000, fVerbose );
+    Abc_ExactStart( 10000, 1, fVerbose, NULL );
 
     assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins ) );
 
@@ -1525,7 +1666,9 @@ void Abc_ExactStoreTest( int fVerbose )
     assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins ) );
     (*pArrTimeProfile)--;
 
-    Abc_ExactStop();
+    Abc_ExactStop( NULL );
+
+    Abc_NtkDelete( pNtk );
 }
 
 ////////////////////////////////////////////////////////////////////////