Adding BLIF dumping to "lutexact".

berkeley-abc · Aug 14, 2024 · c239168 · c239168
1 parent 324ceea
commit c239168
Show file tree

Hide file tree

Showing 2 changed files with 116 additions and 2 deletions.
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
@@ -1228,6 +1228,61 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl )
+{
+    int i, k, b, iVar;
+    char pFileName[1000];
+    sprintf( pFileName, "%s.blif", p->pPars->pTtStr );
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL ) return;
+    fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() );
+    fprintf( pFile, ".model %s\n", p->pPars->pTtStr );
+    fprintf( pFile, ".inputs" );
+    for ( k = 0; k < p->nVars; k++ )
+        fprintf( pFile, " %c", 'a'+k );
+    fprintf( pFile, "\n.outputs F\n" );    
+    for ( i = p->nObjs - 1; i >= p->nVars; i-- )
+    {
+        fprintf( pFile, ".names" );
+        for ( k = 0; k < p->nLutSize; k++ )
+        {
+            iVar = Exa3_ManFindFanin( p, i, k );
+            if ( iVar >= 0 && iVar < p->nVars )
+                fprintf( pFile, " %c", 'a'+iVar );
+            else
+                fprintf( pFile, " %02d", iVar );
+        }
+        if ( i == p->nObjs - 1 )
+            fprintf( pFile, " F\n" );
+        else 
+            fprintf( pFile, " %02d\n", i );
+        int iVarStart = 1 + p->LutMask*(i - p->nVars);
+        for ( k = 0; k < p->LutMask; k++ )
+        {
+            int Val = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+k); 
+            if ( Val == 0 )
+                continue;
+            for ( b = 0; b < p->nLutSize; b++ )
+                fprintf( pFile, "%d", ((k+1) >> b) & 1 );
+            fprintf( pFile, " %d\n", i != p->nObjs - 1 || !fCompl );
+        }
+    }
+    fprintf( pFile, ".end\n\n" );
+    fclose( pFile );
+    printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
+}
+
 
 /**Function*************************************************************
 
@@ -1483,8 +1538,10 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
     else 
         printf( "The problem has no solution.\n" );
     printf( "Added = %d.  Tried = %d.  ", p->nUsed[1], p->nUsed[0] );
-    Exa3_ManFree( p );
     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
+    if ( iMint == -1 )
+        Exa3_ManDumpBlif( p, fCompl );
+    Exa3_ManFree( p );
 }
 
 /**Function*************************************************************

diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c
@@ -1176,6 +1176,61 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl )
+{
+    int i, k, b, iVar;
+    char pFileName[1000];
+    sprintf( pFileName, "%s.blif", p->pPars->pTtStr );
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL ) return;
+    fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() );
+    fprintf( pFile, ".model %s\n", p->pPars->pTtStr );
+    fprintf( pFile, ".inputs" );
+    for ( k = 0; k < p->nVars; k++ )
+        fprintf( pFile, " %c", 'a'+k );
+    fprintf( pFile, "\n.outputs F\n" );    
+    for ( i = p->nObjs - 1; i >= p->nVars; i-- )
+    {
+        fprintf( pFile, ".names" );
+        for ( k = 0; k < p->nLutSize; k++ )
+        {
+            iVar = Exa3_ManFindFanin( p, i, k );
+            if ( iVar >= 0 && iVar < p->nVars )
+                fprintf( pFile, " %c", 'a'+iVar );
+            else
+                fprintf( pFile, " %02d", iVar );
+        }
+        if ( i == p->nObjs - 1 )
+            fprintf( pFile, " F\n" );
+        else 
+            fprintf( pFile, " %02d\n", i );
+        int iVarStart = 1 + p->LutMask*(i - p->nVars);
+        for ( k = 0; k < p->LutMask; k++ )
+        {
+            int Val = sat_solver_var_value(p->pSat, iVarStart+k); 
+            if ( Val == 0 )
+                continue;
+            for ( b = 0; b < p->nLutSize; b++ )
+                fprintf( pFile, "%d", ((k+1) >> b) & 1 );
+            fprintf( pFile, " %d\n", i != p->nObjs - 1 || !fCompl );
+        }
+    }
+    fprintf( pFile, ".end\n\n" );
+    fclose( pFile );
+    printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
+}
+
 
 /**Function*************************************************************
 
@@ -1364,8 +1419,10 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars )
     }
     if ( iMint == -1 )
         Exa3_ManPrintSolution( p, fCompl );
-    Exa3_ManFree( p );
     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
+    if ( iMint == -1 )
+        Exa3_ManDumpBlif( p, fCompl );
+    Exa3_ManFree( p );
 }