New SAT-based optimization package.

8 files changed, 650 insertions, 0 deletions

diff --git a/src/opt/sbd/module.make b/src/opt/sbd/module.make
new file mode 100644
index 00000000..d966e577
--- /dev/null
+++ b/src/opt/sbd/module.make
@@ -0,0 +1,5 @@
+SRC +=    src/opt/sbd/sbd.c \
+    src/opt/sbd/sbdCnf.c \
+    src/opt/sbd/sbdCore.c \
+    src/opt/sbd/sbdSat.c \
+    src/opt/sbd/sbdWin.c
diff --git a/src/opt/sbd/sbd.c b/src/opt/sbd/sbd.c
new file mode 100644
index 00000000..4d86d2ee
--- /dev/null
+++ b/src/opt/sbd/sbd.c
@@ -0,0 +1,53 @@
+/**CFile****************************************************************
+
+  FileName    [sbd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbd.h b/src/opt/sbd/sbd.h
new file mode 100644
index 00000000..946a2ee4
--- /dev/null
+++ b/src/opt/sbd/sbd.h
@@ -0,0 +1,104 @@
+/**CFile****************************************************************
+
+  FileName    [sbd.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sbd.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__opt_sbd__h
+#define ABC__opt_sbd__h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Sbd_Ntk_t_ Sbd_Ntk_t;
+typedef struct Sbd_Par_t_ Sbd_Par_t;
+struct Sbd_Par_t_
+{
+    int             nTfoLevMax;    // the maximum fanout levels
+    int             nTfiLevMax;    // the maximum fanin levels
+    int             nFanoutMax;    // the maximum number of fanouts
+    int             nDepthMax;     // the maximum depth to try
+    int             nVarMax;       // the maximum variable count
+    int             nMffcMin;      // the minimum MFFC size
+    int             nMffcMax;      // the maximum MFFC size
+    int             nDecMax;       // the maximum number of decompositions
+    int             nWinSizeMax;   // the maximum window size
+    int             nGrowthLevel;  // the maximum allowed growth in level
+    int             nBTLimit;      // the maximum number of conflicts in one SAT run
+    int             nNodesMax;     // the maximum number of nodes to try
+    int             iNodeOne;      // one particular node to try
+    int             nFirstFixed;   // the number of first nodes to be treated as fixed
+    int             nTimeWin;      // the size of timing window in percents
+    int             DeltaCrit;     // delay delta in picoseconds
+    int             DelAreaRatio;  // delay/area tradeoff (how many ps we trade for a unit of area)
+    int             fRrOnly;       // perform redundance removal
+    int             fArea;         // performs optimization for area
+    int             fAreaRev;      // performs optimization for area in reverse order
+    int             fMoreEffort;   // performs high-affort minimization
+    int             fUseAndOr;     // enable internal detection of AND/OR gates
+    int             fZeroCost;     // enable zero-cost replacement
+    int             fUseSim;       // enable simulation
+    int             fPrintDecs;    // enable printing decompositions
+    int             fAllBoxes;     // enable preserving all boxes
+    int             fLibVerbose;   // enable library stats
+    int             fDelayVerbose; // enable delay stats
+    int             fVerbose;      // enable basic stats
+    int             fVeryVerbose;  // enable detailed stats
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== sbdCnf.c ==========================================================*/
+/*=== sbdCore.c ==========================================================*/
+extern void         Sbd_ParSetDefault( Sbd_Par_t * pPars );
+extern int          Sbd_NtkPerform( Sbd_Ntk_t * p, Sbd_Par_t * pPars );
+/*=== sbdNtk.c ==========================================================*/
+extern Sbd_Ntk_t *  Sbd_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths );
+extern void         Sbd_NtkFree( Sbd_Ntk_t * p );
+extern Vec_Int_t *  Sbd_NodeReadFanins( Sbd_Ntk_t * p, int i );
+extern word *       Sbd_NodeReadTruth( Sbd_Ntk_t * p, int i );
+extern int          Sbd_NodeReadFixed( Sbd_Ntk_t * p, int i );
+extern int          Sbd_NodeReadUsed( Sbd_Ntk_t * p, int i );
+/*=== sbdWin.c ==========================================================*/
+extern Vec_Int_t *  Sbd_NtkDfs( Sbd_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes );
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/sbd/sbdCnf.c b/src/opt/sbd/sbdCnf.c
new file mode 100644
index 00000000..6291baed
--- /dev/null
+++ b/src/opt/sbd/sbdCnf.c
@@ -0,0 +1,147 @@
+/**CFile****************************************************************
+
+  FileName    [sbdCnf.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [CNF computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sbdCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbd_PrintCnf( Vec_Str_t * vCnf )
+{
+    char Entry;
+    int i, Lit;
+    Vec_StrForEachEntry( vCnf, Entry, i )
+    {
+        Lit = (int)Entry;
+        if ( Lit == -1 )
+            printf( "\n" );
+        else
+            printf( "%s%d ", Abc_LitIsCompl(Lit) ? "-":"", Abc_Lit2Var(Lit) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sbd_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
+{
+    Vec_StrClear( vCnf );
+    if ( Truth == 0 || ~Truth == 0 )
+    {
+//        assert( nVars == 0 );
+        Vec_StrPush( vCnf, (char)(Truth == 0) );
+        Vec_StrPush( vCnf, (char)-1 );
+        return 1;
+    }
+    else 
+    {
+        int i, k, c, RetValue, Literal, Cube, nCubes = 0;
+        assert( nVars > 0 );
+        for ( c = 0; c < 2; c ++ )
+        {
+            Truth = c ? ~Truth : Truth;
+            RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
+            assert( RetValue == 0 );
+            nCubes += Vec_IntSize( vCover );
+            Vec_IntForEachEntry( vCover, Cube, i )
+            {
+                for ( k = 0; k < nVars; k++ )
+                {
+                    Literal = 3 & (Cube >> (k << 1));
+                    if ( Literal == 1 )      // '0'  -> pos lit
+                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
+                    else if ( Literal == 2 ) // '1'  -> neg lit
+                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
+                    else if ( Literal != 0 )
+                        assert( 0 );
+                }
+                Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
+                Vec_StrPush( vCnf, (char)-1 );
+            }
+        }
+        return nCubes;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbd_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar )
+{
+    Vec_Int_t * vClause;
+    char Entry;
+    int i, Lit;
+    Vec_WecClear( vRes );
+    vClause = Vec_WecPushLevel( vRes );
+    Vec_StrForEachEntry( vCnf, Entry, i )
+    {
+        if ( (int)Entry == -1 )
+        {
+            vClause = Vec_WecPushLevel( vRes );
+            continue;
+        }
+        Lit = Abc_Lit2LitV( Vec_IntArray(vFaninMap), (int)Entry );
+        Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
+        Vec_IntPush( vClause, Lit );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c
new file mode 100644
index 00000000..4d86d2ee
--- /dev/null
+++ b/src/opt/sbd/sbdCore.c
@@ -0,0 +1,53 @@
+/**CFile****************************************************************
+
+  FileName    [sbd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbdInt.h b/src/opt/sbd/sbdInt.h
new file mode 100644
index 00000000..1157d02c
--- /dev/null
+++ b/src/opt/sbd/sbdInt.h
@@ -0,0 +1,75 @@
+/**CFile****************************************************************
+
+  FileName    [rsbInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rsbInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__opt_sbdInt__h
+#define ABC__opt_sbdInt__h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "misc/vec/vec.h"
+#include "sat/bsat/satSolver.h"
+#include "misc/util/utilNam.h"
+#include "map/scl/sclLib.h"
+#include "map/scl/sclCon.h"
+#include "bool/kit/kit.h"
+#include "misc/st/st.h"
+#include "map/mio/mio.h"
+#include "base/abc/abc.h"
+#include "sbd.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== sbdCnf.c ==========================================================*/
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/sbd/sbdSat.c b/src/opt/sbd/sbdSat.c
new file mode 100644
index 00000000..16405c06
--- /dev/null
+++ b/src/opt/sbd/sbdSat.c
@@ -0,0 +1,161 @@
+/**CFile****************************************************************
+
+  FileName    [sbd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define MAX_M 12 // max inputs
+#define MAX_N 20 // max nodes
+#define MAX_K  6 // max lutsize
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+sat_solver * Sbd_SolverTopo( int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K] ) // inputs, nodes, lutsize
+{
+    sat_solver * pSat = NULL;
+    Vec_Int_t * vTemp = Vec_IntAlloc(100);
+    // assign vars
+    int RetValue, n, i, k, nVars = 0;
+    for ( n = 0; n < N; n++ )
+    for ( i = 0; i < M+N; i++ )
+    for ( k = 0; k < K; k++ )
+        pVars[n][i][k] = nVars++;
+    printf( "Number of vars = %d.\n", nVars );
+    // add constraints
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, nVars );
+    // each node is used
+    for ( i = 0; i < M+N-1; i++ )
+    {
+        Vec_IntClear( vTemp );
+        for ( n = 0; n < N; n++ )
+        for ( k = 0; k < K; k++ )
+            Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
+        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+        assert( RetValue );
+    }
+    // each fanin of each node is connected
+    for ( n = 0; n < N; n++ )
+    for ( k = 0; k < K; k++ )
+    {
+        Vec_IntClear( vTemp );
+        for ( i = 0; i < M+n; i++ )
+            Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
+        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+        assert( RetValue );
+    }
+    // each fanin is connected once; fanins are ordered; nodes are ordered
+    for ( n = 0; n < N;   n++ )
+    for ( i = 0; i < M+N; i++ )
+    for ( k = 0; k < K;   k++ )
+    {
+        int n2, i2, k2;
+        for ( n2 = 0; n2 <=n;   n2++ )
+        for ( i2 = i; i2 < M+N; i2++ )
+        for ( k2 = k; k2 < K;   k2++ )
+        {
+            if ( n2 == n && i2 == i && k2 == k )
+                continue;
+            Vec_IntPushTwo( vTemp, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n2][i2][k2], 1) );
+            RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+            assert( RetValue );
+        }
+    }
+    Vec_IntFree( vTemp );
+    return pSat;
+}
+void Sbd_SolverTopoPrint( sat_solver * pSat, int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K] ) 
+{
+    int n, i, k;
+    printf( "Solution:\n" );
+    for ( i = M+N-1; i >= 0; i-- )
+    {
+        printf( "%2d %c : ", i, i < M ? 'i' : 'n' );
+        for ( n = 0; n < N; n++ )
+        {
+            for ( k = 0; k < K; k++ )
+                printf( "%c", sat_solver_var_value(pSat, pVars[n][i][k]) ? '*' : '.' );
+            printf( "  " );
+        }
+        printf( "\n" );
+    }
+}
+void Sbd_SolverTopoTest()
+{
+    int M = 4; // inputs
+    int N = 3; // nodes
+    int K = 2; // lutsize
+    int status, nCalls, v, nVars;
+    int pVars[MAX_N][MAX_M+MAX_N][MAX_K]; // 20 x 32 x 6 = 3840
+    Vec_Int_t * vLits = Vec_IntAlloc(100);
+    sat_solver * pSat = Sbd_SolverTopo( M, N, K, pVars );
+    nVars = sat_solver_nvars( pSat );
+    for ( nCalls = 0; nCalls < 1000000; nCalls++ )
+    {
+        // find onset minterm
+        status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+        if ( status == l_Undef )
+            break;
+        if ( status == l_False )
+            break;
+        assert( status == l_True );
+        // print solution
+        Sbd_SolverTopoPrint( pSat, M, N, K, pVars );
+        // remember variable values
+        Vec_IntClear( vLits );
+        for ( v = 0; v < nVars; v++ )
+            if ( sat_solver_var_value(pSat, v) )
+                Vec_IntPush( vLits, Abc_Var2Lit(v, 1) );
+        // add breaking clause
+        status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
+        assert( status );
+    }
+    printf( "Found %d solutions.\n", nCalls );
+    sat_solver_delete( pSat );
+    Vec_IntFree( vLits );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c
new file mode 100644
index 00000000..e8702f7d
--- /dev/null
+++ b/src/opt/sbd/sbdWin.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [sbd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+