Extending Liberty parser to handle multi-output cells.

12 files changed, 106 insertions, 21 deletions

diff --git a/src/base/abci/abcAttach.c b/src/base/abci/abcAttach.c
index ad435d6d..89cb53c3 100644
--- a/src/base/abci/abcAttach.c
+++ b/src/base/abci/abcAttach.c
@@ -88,7 +88,7 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
     for ( i = 1; i < nGates; i++ )
         puTruthGates[i] = puTruthGates[i-1] + 2;
     for ( i = 0; i < nGates; i++ )
-        Mio_DeriveTruthTable( ppGates[i], uTruths, Mio_GateReadInputs(ppGates[i]), 6, puTruthGates[i] );
+        Mio_DeriveTruthTable( ppGates[i], uTruths, Mio_GateReadPinNum(ppGates[i]), 6, puTruthGates[i] );
 
     // assign the gates to pNode->pCopy
     Abc_NtkCleanCopy( pNtk );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 71900771..3e974990 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -1049,7 +1049,7 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary )
             Area = Counter * Mio_GateReadArea( ppGates[i] );
             printf( "%-*s   Fanin = %2d   Instance = %8d   Area = %10.2f   %6.2f %%\n", 
                 nGateNameLen, Mio_GateReadName( ppGates[i] ), 
-                Mio_GateReadInputs( ppGates[i] ), 
+                Mio_GateReadPinNum( ppGates[i] ), 
                 Counter, Area, 100.0 * Area / AreaTotal );
         }
         printf( "%-*s                Instance = %8d   Area = %10.2f   %6.2f %%\n", 
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 74b2927d..bb031200 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -533,12 +533,12 @@ int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate, Mio_
     nSize = Vec_PtrSize(vTokens);
     if ( pTwin == NULL )
     {
-        if ( nSize - 3 != Mio_GateReadInputs(pGate) )
+        if ( nSize - 3 != Mio_GateReadPinNum(pGate) )
             return 0;
     }
     else
     {
-        if ( nSize - 3 != Mio_GateReadInputs(pGate) && nSize - 4 != Mio_GateReadInputs(pGate) )
+        if ( nSize - 3 != Mio_GateReadPinNum(pGate) && nSize - 4 != Mio_GateReadPinNum(pGate) )
             return 0;
     }
     // check if the names are in order
@@ -553,7 +553,7 @@ int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate, Mio_
     }
     if ( pTwin == NULL )
     {
-        if ( i == Mio_GateReadInputs(pGate) )
+        if ( i == Mio_GateReadPinNum(pGate) )
             return 1;
         // reorder the pins
         for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
@@ -589,10 +589,10 @@ int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate, Mio_
     }
     else
     {
-        if ( i != Mio_GateReadInputs(pGate) ) // expect the correct order of input pins in the network with twin gates
+        if ( i != Mio_GateReadPinNum(pGate) ) // expect the correct order of input pins in the network with twin gates
             return 0;
         // check the last two entries
-        if ( nSize - 3 == Mio_GateReadInputs(pGate) ) // only one output is available
+        if ( nSize - 3 == Mio_GateReadPinNum(pGate) ) // only one output is available
         {
             pNamePin = Mio_GateReadOutName(pGate);
             Length = strlen(pNamePin);
@@ -614,7 +614,7 @@ int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate, Mio_
             }
             return 0;
         }
-        if ( nSize - 4 == Mio_GateReadInputs(pGate) ) // two outputs are available
+        if ( nSize - 4 == Mio_GateReadPinNum(pGate) ) // two outputs are available
         {
             pNamePin = Mio_GateReadOutName(pGate);
             Length = strlen(pNamePin);
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index aeea1984..47d30b5a 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -1527,7 +1527,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
     Ver_Stream_t * p = pMan->pReader;
     Abc_Obj_t * pNetActual, * pNode, * pNode2 = NULL;
     char * pWord, Symbol;
-    int Input, i, nFanins = Mio_GateReadInputs(pGate);
+    int Input, i, nFanins = Mio_GateReadPinNum(pGate);
 
     // convert from the blackbox into the network with local functions representated by gates
     if ( 1 != pMan->fMapped )
diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c
index 36ad4920..b41dfe54 100644
--- a/src/map/mapper/mapperTree.c
+++ b/src/map/mapper/mapperTree.c
@@ -309,7 +309,7 @@ Map_Super_t * Map_LibraryReadGateTree( Map_SuperLib_t * pLib, char * pBuffer, in
         return NULL;
     }
     // set the max number of fanouts
-    pGate->nFanLimit = s_MapFanoutLimits[ Mio_GateReadInputs(pGate->pRoot) ];
+    pGate->nFanLimit = s_MapFanoutLimits[ Mio_GateReadPinNum(pGate->pRoot) ];
 
     // read the pin-to-pin delay
     for ( i = 0; ( pTemp = strtok( NULL, " \n\0" ) ); i++ )
@@ -336,7 +336,7 @@ Map_Super_t * Map_LibraryReadGateTree( Map_SuperLib_t * pLib, char * pBuffer, in
         pGate->pFanins[i] = pLib->ppSupers[Num];
     }
     pGate->nFanins = i;
-    if ( pGate->nFanins != (unsigned)Mio_GateReadInputs(pGate->pRoot) )
+    if ( pGate->nFanins != (unsigned)Mio_GateReadPinNum(pGate->pRoot) )
     {
         printf( "The number of fanins of a root gate is wrong.\n" );
         return NULL;
diff --git a/src/map/mapper/mapperTree_old.c b/src/map/mapper/mapperTree_old.c
index eafba376..5b491e82 100644
--- a/src/map/mapper/mapperTree_old.c
+++ b/src/map/mapper/mapperTree_old.c
@@ -306,7 +306,7 @@ Map_Super_t * Map_LibraryReadGateTree( Map_SuperLib_t * pLib, char * pBuffer, in
         return NULL;
     }
     // set the max number of fanouts
-    pGate->nFanLimit = s_MapFanoutLimits[ Mio_GateReadInputs(pGate->pRoot) ];
+    pGate->nFanLimit = s_MapFanoutLimits[ Mio_GateReadPinNum(pGate->pRoot) ];
 
     // read the pin-to-pin delay
     for ( i = 0; ( pTemp = strtok( NULL, " \n\0" ) ); i++ )
@@ -333,7 +333,7 @@ Map_Super_t * Map_LibraryReadGateTree( Map_SuperLib_t * pLib, char * pBuffer, in
         pGate->pFanins[i] = pLib->ppSupers[Num];
     }
     pGate->nFanins = i;
-    if ( pGate->nFanins != (unsigned)Mio_GateReadInputs(pGate->pRoot) )
+    if ( pGate->nFanins != (unsigned)Mio_GateReadPinNum(pGate->pRoot) )
     {
         printf( "The number of fanins of a root gate is wrong.\n" );
         return NULL;
diff --git a/src/map/mapper/mapperUtils.c b/src/map/mapper/mapperUtils.c
index 26033fdb..e49c4dd4 100644
--- a/src/map/mapper/mapperUtils.c
+++ b/src/map/mapper/mapperUtils.c
@@ -799,7 +799,7 @@ st_table * Map_CreateTableGate2Super( Map_Man_t * pMan )
         if ( pSuper->nGates == 1 )
         {
             // skip different versions of the same root gate
-            nInputs = Mio_GateReadInputs(pSuper->pRoot);
+            nInputs = Mio_GateReadPinNum(pSuper->pRoot);
             for ( v = 0; v < nInputs; v++ )
                 if ( pSuper->pFanins[v]->Num != nInputs - 1 - v )
                     break;
diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h
index 3aff8790..55612e32 100644
--- a/src/map/mio/mio.h
+++ b/src/map/mio/mio.h
@@ -111,7 +111,7 @@ extern Mio_Pin_t *       Mio_GateReadPins          ( Mio_Gate_t * pGate );
 extern Mio_Library_t *   Mio_GateReadLib           ( Mio_Gate_t * pGate );      
 extern Mio_Gate_t *      Mio_GateReadNext          ( Mio_Gate_t * pGate );      
 extern Mio_Gate_t *      Mio_GateReadTwin          ( Mio_Gate_t * pGate );      
-extern int               Mio_GateReadInputs        ( Mio_Gate_t * pGate );      
+extern int               Mio_GateReadPinNum        ( Mio_Gate_t * pGate );      
 extern double            Mio_GateReadDelayMax      ( Mio_Gate_t * pGate );      
 extern char *            Mio_GateReadSop           ( Mio_Gate_t * pGate );      
 extern word              Mio_GateReadTruth         ( Mio_Gate_t * pGate );
@@ -135,6 +135,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 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 );
 /*=== mioUtils.c =============================================================*/
diff --git a/src/map/mio/mioApi.c b/src/map/mio/mioApi.c
index 2fe23c2c..31d803ab 100644
--- a/src/map/mio/mioApi.c
+++ b/src/map/mio/mioApi.c
@@ -148,7 +148,7 @@ Mio_Pin_t *       Mio_GateReadPins    ( Mio_Gate_t * pGate )            { return
 Mio_Library_t *   Mio_GateReadLib     ( Mio_Gate_t * pGate )            { return pGate->pLib;      }
 Mio_Gate_t *      Mio_GateReadNext    ( Mio_Gate_t * pGate )            { return pGate->pNext;     }
 Mio_Gate_t *      Mio_GateReadTwin    ( Mio_Gate_t * pGate )            { return pGate->pTwin;     }
-int               Mio_GateReadInputs  ( Mio_Gate_t * pGate )            { return pGate->nInputs;   }
+int               Mio_GateReadPinNum  ( Mio_Gate_t * pGate )            { return pGate->nInputs;   }
 double            Mio_GateReadDelayMax( Mio_Gate_t * pGate )            { return pGate->dDelayMax; }
 char *            Mio_GateReadSop     ( Mio_Gate_t * pGate )            { return pGate->pSop;      }
 word              Mio_GateReadTruth   ( Mio_Gate_t * pGate )            { return pGate->nInputs <= 6 ? pGate->uTruth : 0;   }
diff --git a/src/map/mio/mioParse.c b/src/map/mio/mioParse.c
index c68b7dea..a3dfa435 100644
--- a/src/map/mio/mioParse.c
+++ b/src/map/mio/mioParse.c
@@ -382,6 +382,83 @@ Vec_Int_t * Mio_ParseFormula( char * pFormInit, char ** ppVarNames, int nVars )
     return NULL;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Checks if the gate's formula essentially depends on all variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mio_ParseCheckName( Mio_Gate_t * pGate, char ** ppStr )
+{
+    Mio_Pin_t * pPin;
+    int i;
+    for ( pPin = Mio_GateReadPins(pGate), i = 0; pPin; pPin = Mio_PinReadNext(pPin), i++ )
+        if ( !strncmp( *ppStr, Mio_PinReadName(pPin), strlen(Mio_PinReadName(pPin)) ) )
+        {
+            *ppStr += strlen(Mio_PinReadName(pPin)) - 1;
+            return i;
+        }
+    return -1;
+}
+int Mio_ParseCheckFormula( Mio_Gate_t * pGate, char * pForm )
+{
+    Mio_Pin_t * pPin;
+    char * pStr;
+    int i, iPin, fVisit[32] = {0};
+    if ( Mio_GateReadPins(pGate) == NULL )
+        return 1;
+/*
+    // find the equality sign
+    pForm = strstr( pForm, "=" );
+    if ( pForm == NULL )
+    {
+        printf( "Skipping gate \"%s\" because formula \"%s\" has not equality sign (=).\n", pGate->pName, pForm );
+        return 0;
+    }
+*/
+printf( "Checking gate %s\n", pGate->pName );
+
+    for ( pStr = pForm + 1; *pStr; pStr++ )
+    {
+        if ( *pStr == ' ' ||
+             *pStr == MIO_EQN_SYM_OPEN ||   
+             *pStr == MIO_EQN_SYM_CLOSE ||  
+             *pStr == MIO_EQN_SYM_CONST0 || 
+             *pStr == MIO_EQN_SYM_CONST1 || 
+             *pStr == MIO_EQN_SYM_NEG ||    
+             *pStr == MIO_EQN_SYM_NEGAFT || 
+             *pStr == MIO_EQN_SYM_AND ||    
+             *pStr == MIO_EQN_SYM_AND2 ||   
+             *pStr == MIO_EQN_SYM_XOR ||    
+             *pStr == MIO_EQN_SYM_OR ||     
+             *pStr == MIO_EQN_SYM_OR2 
+           )
+           continue;
+        // return the number of the pin which has this name
+        iPin = Mio_ParseCheckName( pGate, &pStr );
+        if ( iPin == -1 )
+        {
+            printf( "Skipping gate \"%s\" because substring \"%s\" does not match with a pin name.\n", pGate->pName, *pStr );
+            return 0;
+        }
+        assert( iPin < 32 );
+        fVisit[iPin] = 1;
+    }
+    // check that all pins are used
+    for ( pPin = Mio_GateReadPins(pGate), i = 0; pPin; pPin = Mio_PinReadNext(pPin), i++ )
+        if ( fVisit[i] == 0 )
+        {
+            printf( "Skipping gate \"%s\" because pin \"%s\" does not appear in the formula \"%s\".\n", pGate->pName, Mio_PinReadName(pPin), pForm );
+            return 0;
+        }
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/mio/mioRead.c b/src/map/mio/mioRead.c
index 53ea7d2d..2d1a747f 100644
--- a/src/map/mio/mioRead.c
+++ b/src/map/mio/mioRead.c
@@ -209,7 +209,14 @@ int Mio_LibraryReadInternal( Mio_Library_t * pLib, char * pBuffer, int fExtended
         pGate = Mio_LibraryReadGate( &pToken, fExtendedFormat );
         if ( pGate == NULL )
             return 1;
-        
+/*
+        // skip the gate if its formula has problems
+        if ( !Mio_ParseCheckFormula(pGate, pGate->pForm) )
+        {
+            Mio_GateDelete( pGate );
+            continue;
+        }
+*/        
         // set the library
         pGate->pLib = pLib;
 
diff --git a/src/map/super/superGate.c b/src/map/super/superGate.c
index 53f3da35..700fef0e 100644
--- a/src/map/super/superGate.c
+++ b/src/map/super/superGate.c
@@ -360,7 +360,7 @@ Super_Man_t * Super_Compute( Super_Man_t * pMan, Mio_Gate_t ** ppGates, int nGat
         {
             if ( pMan->nLevels >= 1 )  // First level gates have been computed
             {
-                if ( Mio_GateReadInputs(ppGates[k]) >= iPruneLimitRoot )
+                if ( Mio_GateReadPinNum(ppGates[k]) >= iPruneLimitRoot )
                     continue;
             }
         }
@@ -386,7 +386,7 @@ Super_Man_t * Super_Compute( Super_Man_t * pMan, Mio_Gate_t ** ppGates, int nGat
 
         if ( pMan->fVerbose )
         {
-            printf ("Trying %d choices for %d inputs\n", t, Mio_GateReadInputs(ppGates[k]) );
+            printf ("Trying %d choices for %d inputs\n", t, Mio_GateReadPinNum(ppGates[k]) );
         }
 
         // resort part of this range by area
@@ -402,7 +402,7 @@ Super_Man_t * Super_Compute( Super_Man_t * pMan, Mio_Gate_t ** ppGates, int nGat
 
         // consider the combinations of gates with the root gate on top
         AreaMio = (float)Mio_GateReadArea(ppGates[k]);
-        nFanins = Mio_GateReadInputs(ppGates[k]);
+        nFanins = Mio_GateReadPinNum(ppGates[k]);
         switch ( nFanins )
         {
         case 0: // should not happen
@@ -1348,7 +1348,7 @@ void Super_WriteLibraryTree_rec( FILE * pFile, Super_Man_t * pMan, Super_Gate_t
     if ( pSuper->fVar || pSuper->Number > 0 )
         return;
     // write the fanins
-    nFanins = Mio_GateReadInputs(pSuper->pRoot);
+    nFanins = Mio_GateReadPinNum(pSuper->pRoot);
     for ( i = 0; i < nFanins; i++ )
         Super_WriteLibraryTree_rec( pFile, pMan, pSuper->pFanins[i], pCounter );
     // finally write the gate