New SAT-based optimization package.

src/base/abci/abc.c

@@ -55,6 +55,7 @@
 #include "sat/bmc/bmc.h"
 #include "proof/ssc/ssc.h"
 #include "opt/sfm/sfm.h"
+#include "opt/sbd/sbd.h"
 #include "bool/rpo/rpo.h"
 #include "map/mpm/mpm.h"
 #include "opt/fret/fretime.h"
@@ -481,6 +482,7 @@ static int Abc_CommandAbc9Acec               ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Esop               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Exorcism           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Mfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Mfsd               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexMerge           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1122,6 +1124,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&esop",         Abc_CommandAbc9Esop,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&exorcism",     Abc_CommandAbc9Exorcism,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mfs",          Abc_CommandAbc9Mfs,          0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&mfsd",         Abc_CommandAbc9Mfsd,         0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
@@ -40829,6 +40832,132 @@ usage:
   Synopsis    []
 
   Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars );
+    Gia_Man_t * pTemp; int c;
+    Sbd_Par_t Pars, * pPars = &Pars;
+    Sbd_ParSetDefault( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCavwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLutSize < 0 )
+                goto usage;
+            break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTfoLevels = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTfoLevels < 0 )
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTfoFanMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTfoFanMax < 0 )
+                goto usage;
+            break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nWinSizeMax < 0 )
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 )
+                goto usage;
+            break;
+        case 'a':
+            pPars->fArea ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Mfs(): There is no AIG.\n" );
+        return 0;
+    }
+    if ( Gia_ManBufNum(pAbc->pGia) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Mfs(): This command does not work with barrier buffers.\n" );
+        return 1;
+    }
+    if ( Gia_ManHasMapping(pAbc->pGia) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has mapping (run &st to unmap).\n" );
+        return 0;
+    }
+    pTemp = Sbd_NtkPerform( pAbc->pGia, pPars );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &mfsd [-KWFMC <num>] [-avwh]\n" );
+    Abc_Print( -2, "\t           performs SAT-based delay-oriented AIG optimization\n" );
+    Abc_Print( -2, "\t-K <num> : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n",         pPars->nLutSize );
+    Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n",             pPars->nTfoLevels );
+    Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n",                pPars->nTfoFanMax );
+    Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n",    pPars->nWinSizeMax );
+    Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n",   pPars->nBTLimit );
+    Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n",                        pPars->fArea? "area": "area+edges" );
+    Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n",                        pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w       : toggle printing detailed stats for each node [default = %s]\n",                pPars->fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
 
   SideEffects []
 

src/base/io/ioWriteDot.c

@@ -74,7 +74,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     Abc_Obj_t * pNode, * pFanin;
     char * pSopString;
     int LevelMin, LevelMax, fHasCos, Level, i, k, fHasBdds, fCompl, Prev;
-    int Limit = 300;
+    int Limit = 500;
 
     assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
 

src/misc/util/utilTruth.h

@@ -266,6 +266,28 @@ static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords,
         for ( w = 0; w < nWords; w++ )
             pOut[w] = pIn1[w] & pIn2[w];
 }
+static inline void Abc_TtAndCompl( word * pOut, word * pIn1, int fCompl1, word * pIn2, int fCompl2, int nWords )
+{
+    int w;
+    if ( fCompl1 )
+    {
+        if ( fCompl2 )
+            for ( w = 0; w < nWords; w++ )
+                pOut[w] = ~pIn1[w] & ~pIn2[w];
+        else
+            for ( w = 0; w < nWords; w++ )
+                pOut[w] = ~pIn1[w] & pIn2[w];
+    }
+    else
+    {
+        if ( fCompl2 )
+            for ( w = 0; w < nWords; w++ )
+                pOut[w] = pIn1[w] & ~pIn2[w];
+        else
+            for ( w = 0; w < nWords; w++ )
+                pOut[w] = pIn1[w] & pIn2[w];
+    }
+}
 static inline void Abc_TtAndSharp( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
 {
     int w;
@@ -288,6 +310,12 @@ static inline void Abc_TtOr( word * pOut, word * pIn1, word * pIn2, int nWords )
     for ( w = 0; w < nWords; w++ )
         pOut[w] = pIn1[w] | pIn2[w];
 }
+static inline void Abc_TtOrXor( word * pOut, word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] |= pIn1[w] ^ pIn2[w];
+}
 static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
 {
     int w;

src/opt/sbd/sbd.h

@@ -35,42 +35,21 @@ 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
+    int             nLutSize;     // target LUT size
+    int             nTfoLevels;   // the number of TFO levels (windowing)
+    int             nTfoFanMax;   // the max number of fanouts (windowing)
+    int             nWinSizeMax;  // maximum window size (windowing)
+    int             nBTLimit;     // maximum number of SAT conflicts 
+    int             nWords;       // simulation word count
+    int             fArea;        // area-oriented optimization
+    int             fVerbose;     // verbose flag
+    int             fVeryVerbose; // verbose flag
 };
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -82,16 +61,7 @@ struct Sbd_Par_t_
 /*=== 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 );
+extern Gia_Man_t *  Sbd_NtkPerform( Gia_Man_t * p, Sbd_Par_t * pPars );
 
 
 ABC_NAMESPACE_HEADER_END

src/opt/sbd/sbdInt.h

@@ -34,6 +34,7 @@
 #include "misc/vec/vec.h"
 #include "sat/bsat/satSolver.h"
 #include "misc/util/utilNam.h"
+#include "misc/util/utilTruth.h"
 #include "map/scl/sclLib.h"
 #include "map/scl/sclCon.h"
 #include "bool/kit/kit.h"

src/opt/sbd/sbdSat.c

@@ -37,6 +37,179 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#define SBD_LUTS_MAX   2
+#define SBD_SIZE_MAX   4
+#define SBD_DIV_MAX   16
+
+// new AIG manager
+typedef struct Sbd_Pro_t_ Sbd_Pro_t;
+struct Sbd_Pro_t_
+{
+    int             nLuts;  // LUT count
+    int             nSize;  // LUT size
+    int             nDivs;  // divisor count
+    int             nVars;  // intermediate variables (nLuts * nSize)
+    int             nPars;  // total parameter count (nLuts * (1 << nSize) + nLuts * nSize * nDivs) 
+    int             pPars1[SBD_LUTS_MAX][1<<SBD_SIZE_MAX];            // lut parameters
+    int             pPars2[SBD_LUTS_MAX][SBD_SIZE_MAX][SBD_DIV_MAX];  // topo parameters
+    int             pVars[SBD_LUTS_MAX][SBD_SIZE_MAX+1];              // internal variables
+    int             pDivs[SBD_DIV_MAX];                               // divisor variables (external)
+};
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Sbd_ProblemSetup( Sbd_Pro_t * p, int nLuts, int nSize, int nDivs )
+{
+    Vec_Int_t * vCnf = Vec_IntAlloc( 1000 );
+    int i, k, d, v, n, iVar = 0;
+    assert( nLuts >= 1 && nLuts <= 2 );
+    memset( p, 0, sizeof(Sbd_Pro_t) );
+    p->nLuts = nLuts;
+    p->nSize = nSize;
+    p->nDivs = nDivs;
+    p->nVars = nLuts * nSize;
+    p->nPars = nLuts * (1 << nSize) + nLuts * nSize * nDivs;
+    // set parameters
+    for ( i = 0; i < nLuts; i++ )
+    for ( k = 0; k < (1 << nSize); k++ )
+        p->pPars1[i][k] = iVar++;
+    for ( i = 0; i < nLuts; i++ )
+    for ( k = 0; k < nSize; k++ )
+    for ( d = 0; d < nDivs; d++ )
+        p->pPars2[i][k][d] = iVar++;
+    // set intermediate variables
+    for ( i = 0; i < nLuts; i++ )
+    for ( k = 0; k < nSize; k++ )
+        p->pVars[i][k] = iVar++;
+    // set top variables 
+    for ( i = 1; i < nLuts; i++ )
+        p->pVars[i][nSize] = p->pVars[i-1][0];
+    // set divisor variables
+    for ( d = 0; d < nDivs; d++ )
+        p->pDivs[d] = iVar++;
+    assert( iVar == p->nPars + p->nVars + p->nDivs );
+
+    // input compatiblity clauses
+    for ( i = 0; i < nLuts; i++ )
+    for ( k = (i > 0); k < nSize; k++ )
+    for ( d = 0; d < nDivs; d++ )
+    for ( n = 0; n < nDivs; n++ )
+    {
+        if ( n < d )
+        {
+            Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
+            Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][n], 0) );
+            Vec_IntPush( vCnf, -1 );
+        }
+        else if ( k < nSize-1 )
+        {
+            Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
+            Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k+1][n], 0) );
+            Vec_IntPush( vCnf, -1 );
+        }
+    }
+
+    // create LUT clauses
+    for ( i = 0; i < nLuts; i++ )
+    for ( k = 0; k < (1 << nSize); k++ )
+    for ( n = 0; n < 2; n++ )
+    {
+        for ( v = 0; v < nSize; v++ )
+            Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][v], (k >> v) & 1) );
+        Vec_IntPush( vCnf, Abc_Var2Lit(p->pVars[i][nSize], n) );
+        Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], !n) );
+        Vec_IntPush( vCnf, -1 );
+    }
+
+    // create input clauses
+    for ( i = 0; i < nLuts; i++ )
+    for ( k = (i > 0); k < nSize; k++ )
+    for ( d = 0; d < nDivs; d++ )
+    for ( n = 0; n < 2; n++ )
+    {
+        Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
+        Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], n) );
+        Vec_IntPush( vCnf, Abc_Var2Lit(p->pDivs[d], !n) );
+        Vec_IntPush( vCnf, -1 );
+    }
+
+    return vCnf;
+}
+// add clauses to the don't-care computation solver
+void Sbd_ProblemLoad1( Sbd_Pro_t * p, Vec_Int_t * vCnf, int iStartVar, int * pDivVars, int iTopVar, sat_solver * pSat )
+{
+    int pLits[8], nLits, i, k, iLit, RetValue;
+    int ThisTopVar = p->pVars[0][p->nSize];
+    int FirstDivVar = p->nPars + p->nVars;
+    // add clauses
+    for ( i = 0; i < Vec_IntSize(vCnf); i++ )
+    {
+        assert( Vec_IntEntry(vCnf, i) != -1 );
+        for ( k = i+1; k < Vec_IntSize(vCnf); k++ )
+            if ( Vec_IntEntry(vCnf, i) == -1 )
+                break;
+        nLits = 0;
+        Vec_IntForEachEntryStartStop( vCnf, iLit, i, i, k ) {
+            if ( Abc_Lit2Var(iLit) == ThisTopVar )
+                pLits[nLits++] = Abc_Var2Lit( ThisTopVar, Abc_LitIsCompl(iLit) );
+            else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
+                pLits[nLits++] = Abc_Var2Lit( pDivVars[Abc_Lit2Var(iLit)-FirstDivVar], Abc_LitIsCompl(iLit) );
+            else
+                pLits[nLits++] = iLit + 2 * iStartVar;
+        }
+        assert( nLits <= 8 );
+        RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
+        assert( RetValue );
+    }
+}
+// add clauses to the functionality evaluation solver
+void Sbd_ProblemLoad2( Sbd_Pro_t * p, Vec_Wec_t * vCnf, int iStartVar, int * pDivVarValues, int iTopVarValue, sat_solver * pSat )
+{
+    Vec_Int_t * vLevel;
+    int pLits[8], nLits, i, k, iLit, RetValue;
+    int ThisTopVar = p->pVars[0][p->nSize];
+    int FirstDivVar = p->nPars + p->nVars;
+    int FirstIntVar = p->nPars;
+    // add clauses
+    Vec_WecForEachLevel( vCnf, vLevel, i )
+    {
+        nLits = 0;
+        Vec_IntForEachEntry( vLevel, iLit, k ) {
+            if ( Abc_Lit2Var(iLit) == ThisTopVar )
+            {
+                if ( Abc_LitIsCompl(iLit) == iTopVarValue )
+                    break;
+                continue;
+            }
+            else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
+            {
+                if ( Abc_LitIsCompl(iLit) == pDivVarValues[Abc_Lit2Var(iLit)-FirstDivVar] )
+                    break;
+                continue;
+            }
+            else if ( Abc_Lit2Var(iLit) >= FirstIntVar )
+                pLits[nLits++] = iLit + 2 * iStartVar;
+            else
+                pLits[nLits++] = iLit;
+        }
+        if ( k < Vec_IntSize(vLevel) )
+            continue;
+        assert( nLits <= 8 );
+        RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
+        assert( RetValue );
+    }
+}
+
+
 /**Function*************************************************************
 
   Synopsis    []