Synthesis for mesh of LUTs.

1 files changed, 23 insertions, 8 deletions

diff --git a/src/sat/bmc/bmcMesh.c b/src/sat/bmc/bmcMesh.c
index 3ced0dd7..ff443711 100644
--- a/src/sat/bmc/bmcMesh.c
+++ b/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" );