Synthesis for mesh of LUTs.

abclib.dsp

@@ -1967,6 +1967,10 @@ SOURCE=.\src\sat\bmc\bmcMesh.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bmc\bmcMesh2.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bmc\bmcMulti.c
 # End Source File
 # Begin Source File

src/base/abci/abc.c

@@ -38036,13 +38036,15 @@ usage:
 int Abc_CommandAbc9Mesh( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose );
+    extern void Bmc_MeshTest2( Gia_Man_t * p, int X, int Y, int T, int fVerbose );
     int X =  4;
     int Y =  4;
     int T =  3;
+    int fUseSatoko = 1;
     int c, fVerbose = 1;
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "XYTh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "XYTsh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -38079,6 +38081,9 @@ int Abc_CommandAbc9Mesh( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( T < 2 )
                 goto usage;
             break;
+        case 's':
+            fUseSatoko ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -38108,15 +38113,19 @@ int Abc_CommandAbc9Mesh( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "The depth of the AIG (%d) cannot be larger than the latency (%d).\n", Gia_ManLevelNum(pAbc->pGia), T );
         return 1;
     }
-    Bmc_MeshTest( pAbc->pGia, X, Y, T, fVerbose );
+    if ( fUseSatoko )
+        Bmc_MeshTest( pAbc->pGia, X, Y, T, fVerbose );
+    else
+        Bmc_MeshTest2( pAbc->pGia, X, Y, T, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &mesh [-XYT num] [-h]\n" );
+    Abc_Print( -2, "usage: &mesh [-XYT num] [-sh]\n" );
     Abc_Print( -2, "\t         creates a mesh architecture for the given AIG\n" );
     Abc_Print( -2, "\t-X num : horizontal size of the mesh (X >= 3) [default = %d]\n", X );
     Abc_Print( -2, "\t-Y num : vertical size of the mesh (Y >= 3) [default = %d]\n", Y );
     Abc_Print( -2, "\t-T num : the latency of the mesh (T >= 2) [default = %d]\n", T );
+    Abc_Print( -2, "\t-s     : toggle using new SAT solver Satoko [default = %s]\n", fUseSatoko? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;

src/sat/bmc/bmcMesh.c

@@ -51,7 +51,7 @@ inline int Bmc_MeshUVar( int Me[102][102], int x, int y ) { return Me[x][y] + Me
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Bmc_MeshVarValue( satoko_t * p, int v )
+static inline Bmc_MeshVarValue( satoko_t * p, int v )
 {
     int value = var_value(p, v) != VAR_UNASSING ? var_value(p, v) : var_polarity(p, v);
     return value == LIT_TRUE;
@@ -141,7 +141,7 @@ void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose )
     for ( y = 0; y < Y; y++ )
     for ( x = 0; x < X; x++ )
     {
-        printf( "%3d %3d %3d    %s", iVar, iVar+T, iVar+T+G, x == X-1 ? "\n":"" );
+        //printf( "%3d %3d %3d    %s", iVar, iVar+T, iVar+T+G, x == X-1 ? "\n":"" );
         Me[x][y] = iVar;
         iVar += T + G + NCPARS + 1;
     }
@@ -212,6 +212,7 @@ void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose )
             pLits[0] = Abc_Var2Lit( iGVar+g, 1 );
             pLits[1] = Abc_Var2Lit( iUVar, 0 );
             RetValue = satoko_add_clause( pSat, pLits, 2 );  assert( RetValue );
+            nClauses++;
         }
 
         // at least one time is used
@@ -219,12 +220,14 @@ void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose )
         for ( t = 1; t < T; t++ )
             pLits[t] = Abc_Var2Lit( iTVar+t, 0 );
         RetValue = satoko_add_clause( pSat, pLits, T );  assert( RetValue );
+        nClauses++;
 
         // at least one config is used
         pLits[0] = Abc_Var2Lit( iUVar, 1 );
         for ( c = 0; c < NCPARS; c++ )
             pLits[c+1] = Abc_Var2Lit( iCVar+c, 0 );
         RetValue = satoko_add_clause( pSat, pLits, NCPARS+1 );  assert( RetValue );
+        nClauses++;
 
         // constraints for each time
         for ( t = 1; t < T; t++ )
@@ -250,6 +253,14 @@ void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose )
 
                 nClauses += 2;
             }
+            for ( g = 0; g < I; g++ )
+            for ( c = 4; c < NCPARS; c++ )
+            {
+                pLits[0] = Abc_Var2Lit( iGVar+g, 1 );
+                pLits[1] = Abc_Var2Lit( iCVar+c, 1 );
+                RetValue = satoko_add_clause( pSat, pLits, 2 );  assert( RetValue );
+                nClauses++;
+            }
             // node
             for ( g = I; g < G; g++ )
             for ( c = 0; c < 12; c++ )
@@ -347,13 +358,13 @@ void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose )
             continue;
         }
         printf( "Satisfying solution found. " );
-
+/*
         iVar = solver_varnum(pSat);
         for ( i = 0; i < iVar; i++ )
             if ( Bmc_MeshVarValue(pSat, i) )
                 printf( "%d ", i );
         printf( "\n" );
-
+*/
         break;
     }
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
@@ -361,20 +372,20 @@ void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose )
     {
         // count the number of nodes and buffers
         int nBuffs = 0, nNodes = 0;
-        for ( x = 1; x < X-1; x++ )
         for ( y = 1; y < Y-1; y++ )
+        for ( x = 1; x < X-1; x++ )
         {
             int iCVar = Bmc_MeshCVar( Me, x, y );
             for ( c = 0; c < 4; c++ )
                 if ( Bmc_MeshVarValue(pSat, iCVar+c) )
                 {
-                    printf( "Buffer x=%d y=%d  (var = %d; config = %d)\n", x, y, iCVar+c, c );
+                    //printf( "Buffer y=%d x=%d  (var = %d; config = %d)\n", y, x, iCVar+c, c );
                     nBuffs++;
                 }
             for ( c = 4; c < NCPARS; c++ )
                 if ( Bmc_MeshVarValue(pSat, iCVar+c) )
                 {
-                    printf( "Node   x=%d y=%d  (var = %d; config = %d)\n", x, y, iCVar+c, c );
+                    //printf( "Node   y=%d x=%d  (var = %d; config = %d)\n", y, x, iCVar+c, c );
                     nNodes++;
                 }
         }
@@ -400,7 +411,11 @@ void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose )
                         printf( " %c%-2d ", 'a' + g, t );
                         fFound = 1;
                     }
-                if ( !fFound )
+                if ( fFound )
+                    continue;
+                if ( x == 0 || x == X-1 || y == 0 || y == Y-1 ) // boundary
+                    printf( "  *  " );
+                else
                     printf( "     " );
             }
             printf( "\n" );

src/sat/bmc/module.make

@@ -22,5 +22,6 @@ SRC +=    src/sat/bmc/bmcBCore.c \
     src/sat/bmc/bmcLoad.c \
     src/sat/bmc/bmcMaxi.c \
     src/sat/bmc/bmcMesh.c \
+    src/sat/bmc/bmcMesh2.c \
     src/sat/bmc/bmcMulti.c \
     src/sat/bmc/bmcUnroll.c