Modified SCL gate library to read/write gate formula.

6 files changed, 159 insertions, 15 deletions

diff --git a/src/map/mio/exp.h b/src/map/mio/exp.h
index 766ed38a..73a8f683 100644
--- a/src/map/mio/exp.h
+++ b/src/map/mio/exp.h
@@ -177,7 +177,7 @@ static inline word Exp_Truth6Lit( int nVars, int Lit, word * puFanins, word * pu
     if ( Lit == EXP_CONST1 )
         return ~0;
     if ( Lit < 2 * nVars )
-        return (Lit&1) ? ~puFanins[Lit/2] : puFanins[Lit/2];
+        return  (Lit&1) ? ~puFanins[Lit/2] : puFanins[Lit/2];
     return (Lit&1) ? ~puNodes[Lit/2-nVars] : puNodes[Lit/2-nVars];
 }
 static inline word Exp_Truth6( int nVars, Vec_Int_t * p, word * puFanins )
@@ -197,11 +197,77 @@ static inline word Exp_Truth6( int nVars, Vec_Int_t * p, word * puFanins )
     puNodes = ABC_CALLOC( word, Exp_NodeNum(p) );
     for ( i = 0; i < Exp_NodeNum(p); i++ )
         puNodes[i] = Exp_Truth6Lit( nVars, Vec_IntEntry(p, 2*i+0), puFanins, puNodes ) & 
-                  Exp_Truth6Lit( nVars, Vec_IntEntry(p, 2*i+1), puFanins, puNodes );
+                     Exp_Truth6Lit( nVars, Vec_IntEntry(p, 2*i+1), puFanins, puNodes );
     Res = Exp_Truth6Lit( nVars, Vec_IntEntryLast(p), puFanins, puNodes );
     ABC_FREE( puNodes );
     return Res;
 }
+static inline void Exp_TruthLit( int nVars, int Lit, word ** puFanins, word ** puNodes, word * pRes, int nWords )
+{
+    int w;
+    if ( Lit == EXP_CONST0 )
+        for ( w = 0; w < nWords; w++ )
+            pRes[w] = 0;
+    else if ( Lit == EXP_CONST1 )
+        for ( w = 0; w < nWords; w++ )
+            pRes[w] = ~(word)0;
+    else if ( Lit < 2 * nVars )
+        for ( w = 0; w < nWords; w++ )
+            pRes[w] = (Lit&1) ? ~puFanins[Lit/2][w] : puFanins[Lit/2][w];
+    else
+        for ( w = 0; w < nWords; w++ )
+            pRes[w] = (Lit&1) ? ~puNodes[Lit/2-nVars][w] : puNodes[Lit/2-nVars][w];
+}
+static inline void Exp_Truth( int nVars, Vec_Int_t * p, word * pRes )
+{
+    static word Truth6[6] = {
+        ABC_CONST(0xAAAAAAAAAAAAAAAA),
+        ABC_CONST(0xCCCCCCCCCCCCCCCC),
+        ABC_CONST(0xF0F0F0F0F0F0F0F0),
+        ABC_CONST(0xFF00FF00FF00FF00),
+        ABC_CONST(0xFFFF0000FFFF0000),
+        ABC_CONST(0xFFFFFFFF00000000)
+    };
+    word ** puFanins, ** puNodes, * pTemp0, * pTemp1;
+    int i, w, nWords = (nVars <= 6 ? 1 : 1 << (nVars-6));
+    // create elementary variables
+    puFanins = ABC_ALLOC( word *, nVars );
+    for ( i = 0; i < nVars; i++ )
+        puFanins[i] = ABC_ALLOC( word, nWords );
+    // assign elementary truth tables
+    for ( i = 0; i < nVars; i++ )
+        if ( i < 6 )
+            for ( w = 0; w < nWords; w++ )
+                puFanins[i][w] = Truth6[i];
+        else
+            for ( w = 0; w < nWords; w++ )
+                puFanins[i][w] = (w & (1 << (i-6))) ? ~(word)0 : 0;
+    // create intermediate nodes
+    puNodes = ABC_ALLOC( word *, Exp_NodeNum(p) );
+    for ( i = 0; i < Exp_NodeNum(p); i++ )
+        puNodes[i] = ABC_ALLOC( word, nWords );
+    // evaluate the expression
+    pTemp0 = ABC_ALLOC( word, nWords );
+    pTemp1 = ABC_ALLOC( word, nWords );
+    for ( i = 0; i < Exp_NodeNum(p); i++ )
+    {
+        Exp_TruthLit( nVars, Vec_IntEntry(p, 2*i+0), puFanins, puNodes, pTemp0, nWords );
+        Exp_TruthLit( nVars, Vec_IntEntry(p, 2*i+1), puFanins, puNodes, pTemp1, nWords );
+        for ( w = 0; w < nWords; w++ )
+            puNodes[i][w] = pTemp0[w] & pTemp1[w];
+    }
+    ABC_FREE( pTemp0 );
+    ABC_FREE( pTemp1 );
+    // copy the final result
+    Exp_TruthLit( nVars, Vec_IntEntryLast(p), puFanins, puNodes, pRes, nWords );
+    // cleanup
+    for ( i = 0; i < nVars; i++ )
+        ABC_FREE( puFanins[i] );
+    ABC_FREE( puFanins );
+    for ( i = 0; i < Exp_NodeNum(p); i++ )
+        ABC_FREE( puNodes[i] );
+    ABC_FREE( puNodes );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h
index 72803cd7..ed297a1b 100644
--- a/src/map/mio/mio.h
+++ b/src/map/mio/mio.h
@@ -136,6 +136,7 @@ extern int               Mio_LibraryReadExclude( char * ExcludeFile, st__table *
 extern int               Mio_LibraryParseFormulas( Mio_Library_t * pLib );
 /*=== mioParse.c =============================================================*/
 extern Vec_Int_t *       Mio_ParseFormula( char * pFormInit, char ** ppVarNames, int nVars );
+extern Vec_Wrd_t *       Mio_ParseFormulaTruth( char * pFormInit, char ** ppVarNames, int nVars );
 extern int               Mio_ParseCheckFormula( Mio_Gate_t * pGate, char * pForm );
 /*=== mioSop.c =============================================================*/
 extern char *            Mio_LibDeriveSop( int nVars, Vec_Int_t * vExpr, Vec_Str_t * vStr );
diff --git a/src/map/mio/mioFunc.c b/src/map/mio/mioFunc.c
index c63a3794..67126749 100644
--- a/src/map/mio/mioFunc.c
+++ b/src/map/mio/mioFunc.c
@@ -257,12 +257,14 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
 
     // derive expression 
     pGate->vExpr = Mio_ParseFormula( pGate->pForm, (char **)pPinNames, nPins );
+//    Mio_ParseFormulaTruthTest( pGate->pForm, (char **)pPinNames, nPins );
     // derive cover
     pGate->pSop = Mio_LibDeriveSop( nPins, pGate->vExpr, pGate->pLib->vCube );
     pGate->pSop = Mio_SopRegister( (Mem_Flex_t *)pGate->pLib->pMmFlex, pGate->pSop );
     // derive truth table
     if ( nPins <= 6 )
         pGate->uTruth = Exp_Truth6( nPins, pGate->vExpr, NULL );
+
 /*
     // verify
     if ( pGate->nInputs <= 6 )
diff --git a/src/map/mio/mioParse.c b/src/map/mio/mioParse.c
index 21348498..c709e589 100644
--- a/src/map/mio/mioParse.c
+++ b/src/map/mio/mioParse.c
@@ -384,6 +384,37 @@ Vec_Int_t * Mio_ParseFormula( char * pFormInit, char ** ppVarNames, int nVars )
 
 /**Function*************************************************************
 
+  Synopsis    [Derives the TT corresponding to the equation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Mio_ParseFormulaTruth( char * pFormInit, char ** ppVarNames, int nVars )
+{
+    Vec_Int_t * vExpr;
+    Vec_Wrd_t * vTruth;
+    // derive expression
+    vExpr = Mio_ParseFormula( pFormInit, ppVarNames, nVars );
+    // convert it into a truth table
+    vTruth = Vec_WrdStart( Abc_Truth6WordNum(nVars) );
+    Exp_Truth( nVars, vExpr, Vec_WrdArray(vTruth) );
+    Vec_IntFree( vExpr );
+    return vTruth;
+}
+void Mio_ParseFormulaTruthTest( char * pFormInit, char ** ppVarNames, int nVars )
+{
+    Vec_Wrd_t * vTruth;
+    vTruth = Mio_ParseFormulaTruth( pFormInit, ppVarNames, nVars );
+//    Kit_DsdPrintFromTruth( (unsigned *)Vec_WrdArray(vTruth), nVars ); printf( "\n" );
+    Vec_WrdFree( vTruth );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks if the gate's formula essentially depends on all variables.]
 
   Description []
diff --git a/src/map/scl/sclFile.c b/src/map/scl/sclFile.c
index 794820b3..a170b5c7 100644
--- a/src/map/scl/sclFile.c
+++ b/src/map/scl/sclFile.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "sclInt.h"
+#include "map/mio/mio.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -74,7 +75,7 @@ static void Abc_SclReadLibrary( Vec_Str_t * vOut, int * pPos, SC_Lib * p )
 {
     int i, j, k, n;
     int version = Vec_StrGetI( vOut, pPos );
-    assert( version == ABC_SCL_CUR_VERSION ); // wrong version of the file
+    assert( version == 5 || version == ABC_SCL_CUR_VERSION ); // wrong version of the file
 
     // Read non-composite fields:
     p->pName                 = Vec_StrGetS(vOut, pPos);
@@ -137,7 +138,7 @@ static void Abc_SclReadLibrary( Vec_Str_t * vOut, int * pPos, SC_Lib * p )
             Vec_PtrPush( pCell->vPins, pPin );
 
             pPin->dir      = sc_dir_Input;
-            pPin->pName     = Vec_StrGetS(vOut, pPos); 
+            pPin->pName    = Vec_StrGetS(vOut, pPos); 
             pPin->rise_cap = Vec_StrGetF(vOut, pPos);
             pPin->fall_cap = Vec_StrGetF(vOut, pPos);
         }
@@ -148,18 +149,53 @@ static void Abc_SclReadLibrary( Vec_Str_t * vOut, int * pPos, SC_Lib * p )
             Vec_PtrPush( pCell->vPins, pPin );
 
             pPin->dir          = sc_dir_Output;
-            pPin->pName         = Vec_StrGetS(vOut, pPos); 
+            pPin->pName        = Vec_StrGetS(vOut, pPos); 
             pPin->max_out_cap  = Vec_StrGetF(vOut, pPos);
             pPin->max_out_slew = Vec_StrGetF(vOut, pPos);
 
             k = Vec_StrGetI(vOut, pPos);
             assert( k == pCell->n_inputs );
 
-            // read functions
-            assert( Vec_WrdSize(pPin->vFunc) == 0 );
-            Vec_WrdGrow( pPin->vFunc, Abc_Truth6WordNum(pCell->n_inputs) );
-            for ( k = 0; k < Vec_WrdCap(pPin->vFunc); k++ )
-                Vec_WrdPush( pPin->vFunc, Vec_StrGetW(vOut, pPos) );
+            // read function
+            if ( version == 5 )
+            { 
+                // formula is not given
+                assert( Vec_WrdSize(pPin->vFunc) == 0 );
+                Vec_WrdGrow( pPin->vFunc, Abc_Truth6WordNum(pCell->n_inputs) );
+                for ( k = 0; k < Vec_WrdCap(pPin->vFunc); k++ )
+                    Vec_WrdPush( pPin->vFunc, Vec_StrGetW(vOut, pPos) );
+            }
+            else
+            {
+                // (possibly empty) formula is always given
+                assert( version == ABC_SCL_CUR_VERSION );
+                assert( pPin->func_text == NULL );
+                pPin->func_text = Vec_StrGetS(vOut, pPos); 
+                if ( pPin->func_text[0] == 0 )
+                {
+                    // formula is not given - read truth table
+                    ABC_FREE( pPin->func_text );
+                    assert( Vec_WrdSize(pPin->vFunc) == 0 );
+                    Vec_WrdGrow( pPin->vFunc, Abc_Truth6WordNum(pCell->n_inputs) );
+                    for ( k = 0; k < Vec_WrdCap(pPin->vFunc); k++ )
+                        Vec_WrdPush( pPin->vFunc, Vec_StrGetW(vOut, pPos) );
+                }
+                else
+                {
+                    // formula is given - derive truth table
+                    SC_Pin * pPin2;
+                    Vec_Ptr_t * vNames;
+                    // collect input names
+                    vNames = Vec_PtrAlloc( pCell->n_inputs );
+                    SC_CellForEachPinIn( pCell, pPin2, n )
+                        Vec_PtrPush( vNames, pPin2->pName );
+                    // derive truth table
+                    assert( Vec_WrdSize(pPin->vFunc) == 0 );
+                    Vec_WrdFree( pPin->vFunc );
+                    pPin->vFunc = Mio_ParseFormulaTruth( pPin->func_text, (char **)Vec_PtrArray(vNames), pCell->n_inputs );
+                    Vec_PtrFree( vNames );
+                }
+            }
 
             // Read 'rtiming': (pin-to-pin timing tables for this particular output)
             for ( k = 0; k < pCell->n_inputs; k++ )
@@ -361,10 +397,18 @@ static void Abc_SclWriteLibrary( Vec_Str_t * vOut, SC_Lib * p )
             Vec_StrPutF( vOut, pPin->max_out_slew );
 
             // write function
-            assert( Vec_WrdSize(pPin->vFunc) == Abc_Truth6WordNum(pCell->n_inputs) );
-            Vec_StrPutI( vOut, pCell->n_inputs );
-            Vec_WrdForEachEntry( pPin->vFunc, uWord, k ) // -- 'size = 1u << (n_vars - 6)'
-                Vec_StrPutW( vOut, uWord );  // -- 64-bit number, written uncompressed (low-byte first)
+            if ( pPin->func_text == NULL )
+            {
+                // formula is not given - write empty string
+                Vec_StrPutS( vOut, "" );
+                // write truth table
+                assert( Vec_WrdSize(pPin->vFunc) == Abc_Truth6WordNum(pCell->n_inputs) );
+                Vec_StrPutI( vOut, pCell->n_inputs );
+                Vec_WrdForEachEntry( pPin->vFunc, uWord, k ) // -- 'size = 1u << (n_vars - 6)'
+                    Vec_StrPutW( vOut, uWord );  // -- 64-bit number, written uncompressed (low-byte first)
+            }
+            else // formula is given
+                Vec_StrPutS( vOut, pPin->func_text );
 
             // Write 'rtiming': (pin-to-pin timing tables for this particular output)
             assert( Vec_PtrSize(pPin->vRTimings) == pCell->n_inputs );
diff --git a/src/map/scl/sclInt.h b/src/map/scl/sclInt.h
index 5a9336d8..9818c8c8 100644
--- a/src/map/scl/sclInt.h
+++ b/src/map/scl/sclInt.h
@@ -41,7 +41,7 @@ ABC_NAMESPACE_HEADER_START
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#define ABC_SCL_CUR_VERSION 5
+#define ABC_SCL_CUR_VERSION 6
 
 typedef enum  
 {