Merge remote-tracking branch 'origin/master' into acd

src/aig/gia/giaDeep.c

@@ -55,6 +55,7 @@ Gia_Man_t * Gia_ManDeepSynOne( int nNoImpr, int TimeOut, int nAnds, int Seed, in
         Abc_Random(0);
     for ( i = 0; i < IterMax; i++ )
     {
+        char * pCompress2rs = "balance -l; resub -K 6 -l; rewrite -l; resub -K 6 -N 2 -l; refactor -l; resub -K 8 -l; balance -l; resub -K 8 -N 2 -l; rewrite -l; resub -K 10 -l; rewrite -z -l; resub -K 10 -N 2 -l; balance -l; resub -K 12 -l; refactor -z -l; resub -K 12 -N 2 -l; rewrite -z -l; balance -l";
         unsigned Rand = Abc_Random(0);
         int fDch = Rand & 1;
         //int fCom = (Rand >> 1) & 3;
@@ -62,16 +63,16 @@ Gia_Man_t * Gia_ManDeepSynOne( int nNoImpr, int TimeOut, int nAnds, int Seed, in
         int fFx  = (Rand >> 2) & 1;
         int KLut = fUseTwo ? 2 + (i % 5) : 3 + (i % 4);
         int fChange = 0;
-        char Command[1000];
+        char Command[2000];
-        char * pComp = NULL;
+        char pComp[1000];
         if ( fCom == 3 )
-            pComp = "; &put; compress2rs; compress2rs; compress2rs; &get";
+            sprintf( pComp, "; &put; %s; %s; %s; &get", pCompress2rs, pCompress2rs, pCompress2rs );
         else if ( fCom == 2 )
-            pComp = "; &put; compress2rs; compress2rs; &get";
+            sprintf( pComp, "; &put; %s; %s; &get", pCompress2rs, pCompress2rs );
         else if ( fCom == 1 )
-            pComp = "; &put; compress2rs; &get";
+            sprintf( pComp, "; &put; %s; &get", pCompress2rs );
         else if ( fCom == 0 )
-            pComp = "; &dc2";
+            sprintf( pComp, "; &dc2" );
         sprintf( Command, "&dch%s; &if -a -K %d; &mfs -e -W 20 -L 20%s%s",
             fDch ? " -f" : "", KLut, fFx ? "; &fx; &st" : "", pComp );
         if ( Abc_FrameIsBatchMode() )

src/aig/gia/giaDup.c

@@ -788,6 +788,11 @@ Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p )
         pNew->vConfigs = Vec_IntDup( p->vConfigs );
     if ( p->pCellStr )
         pNew->pCellStr = Abc_UtilStrsav( p->pCellStr );
+    // copy names if present
+    if ( p->vNamesIn )
+        pNew->vNamesIn = Vec_PtrDupStr( p->vNamesIn );
+    if ( p->vNamesOut )
+        pNew->vNamesOut = Vec_PtrDupStr( p->vNamesOut );        
     return pNew;
 }
 Gia_Man_t * Gia_ManDupRemovePis( Gia_Man_t * p, int nRemPis )

src/aig/gia/giaMan.c

@@ -1787,6 +1787,101 @@ void Gia_ManDumpVerilogNoInterAssign( Gia_Man_t * p, char * pFileName, Vec_Int_t
     Gia_ManSetRegNum( p, nRegs );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManPrintOneName( FILE * pFile, char * pName, int Size )
+{
+    int i;
+    for ( i = 0; i < Size; i++ )
+        fprintf( pFile, "%c", pName[i] );
+}
+int Gia_ManCountSymbs( char * pName )
+{
+    int i;
+    for ( i = 0; pName[i]; i++ )
+        if ( pName[i] == '[' )
+            break;
+    return i;
+}
+int Gia_ManReadRangeNum( char * pName, int Size )
+{
+    if ( pName[Size] == 0 )
+        return -1;
+    assert( pName[Size] == '[' );
+    return atoi(pName+Size+1);
+}
+Vec_Int_t * Gia_ManCountSymbsAll( Vec_Ptr_t * vNames )
+{
+    char * pNameLast = (char *)Vec_PtrEntry(vNames, 0), * pName;
+    int i, nSymbsLast = Gia_ManCountSymbs(pNameLast);
+    Vec_Int_t * vArray = Vec_IntAlloc( Vec_PtrSize(vNames) * 2 );
+    Vec_IntPush( vArray, 0 );
+    Vec_IntPush( vArray, nSymbsLast );
+    Vec_PtrForEachEntryStart( char *, vNames, pName, i, 1 )
+    {
+        int nSymbs = Gia_ManCountSymbs(pName);
+        if ( nSymbs == nSymbsLast && !strncmp(pName, pNameLast, nSymbsLast) )
+            continue;
+        Vec_IntPush( vArray, i );
+        Vec_IntPush( vArray, nSymbs );
+        pNameLast  = pName;
+        nSymbsLast = nSymbs;
+    }
+    return vArray;
+}
+void Gia_ManDumpIoList( Gia_Man_t * p, FILE * pFile, int fOuts )
+{
+    Vec_Ptr_t * vNames = fOuts ? p->vNamesOut : p->vNamesIn;
+    if ( vNames == NULL )
+        fprintf( pFile, "_%c_", fOuts ? 'o' : 'i' );
+    else
+    {
+        Vec_Int_t * vArray = Gia_ManCountSymbsAll( vNames );
+        int iName, Size, i;
+        Vec_IntForEachEntryDouble( vArray, iName, Size, i )
+        {
+            if ( i ) fprintf( pFile, ", " );
+            Gia_ManPrintOneName( pFile, (char *)Vec_PtrEntry(vNames, iName), Size );
+        }
+        Vec_IntFree( vArray );            
+    }
+}
+void Gia_ManDumpIoRanges( Gia_Man_t * p, FILE * pFile, int fOuts )
+{
+    Vec_Ptr_t * vNames = fOuts ? p->vNamesOut : p->vNamesIn;
+    if ( p->vNamesOut == NULL )
+        fprintf( pFile, "%s [%d:0] _%c_;\n", fOuts ? "output" : "input", fOuts ? Gia_ManPoNum(p)-1 : Gia_ManPiNum(p)-1, fOuts ? 'o' : 'i' );
+    else
+    {
+        Vec_Int_t * vArray = Gia_ManCountSymbsAll( vNames );
+        int iName, Size, i;
+        Vec_IntForEachEntryDouble( vArray, iName, Size, i )
+        {
+            int iNameNext    = Vec_IntSize(vArray) > i+2 ? Vec_IntEntry(vArray, i+2) : Vec_PtrSize(vNames);
+            char * pName     = (char *)Vec_PtrEntry(vNames, iName);
+            char * pNameLast = (char *)Vec_PtrEntry(vNames, iNameNext-1);
+            assert( !strncmp(pName, pNameLast, Size) );
+            int NumBeg = Gia_ManReadRangeNum( pName,     Size );
+            int NumEnd = Gia_ManReadRangeNum( pNameLast, Size );
+            fprintf( pFile, "  %s ", fOuts ? "output" : "input" );
+            if ( NumBeg != -1 && iName < iNameNext-1 )
+                fprintf( pFile, "[%d:%d] ", NumEnd, NumBeg );
+            Gia_ManPrintOneName( pFile, pName, Size );
+            fprintf( pFile, ";\n" );                
+        }
+        Vec_IntFree( vArray );            
+    }
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -1820,9 +1915,14 @@ void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName )
     fprintf( pFile, "module " );
     Gia_ManDumpModuleName( pFile, p->pName );
     fprintf( pFile, "_wrapper" );
-    fprintf( pFile, " ( _i_, _o_ );\n\n" );
+    fprintf( pFile, " ( " );
-    fprintf( pFile, "  input  [%d:0] _i_;\n",   Gia_ManCiNum(p)-1 );
+    Gia_ManDumpIoList( p, pFile, 0 );
-    fprintf( pFile, "  output [%d:0] _o_;\n\n", Gia_ManCoNum(p)-1 );
+    fprintf( pFile, ", " );
+    Gia_ManDumpIoList( p, pFile, 1 );    
+    fprintf( pFile, " );\n\n" );
+    Gia_ManDumpIoRanges( p, pFile, 0 );
+    Gia_ManDumpIoRanges( p, pFile, 1 );
+    fprintf( pFile, "\n" );
 
     fprintf( pFile, "  wire " );
     Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
@@ -1834,9 +1934,13 @@ void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName )
 
     fprintf( pFile, "  assign { " );
     Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL );
-    fprintf( pFile, " } = _i_;\n\n" );
+    fprintf( pFile, " } = { " );
+    Gia_ManDumpIoList( p, pFile, 0 );    
+    fprintf( pFile, " };\n\n" );    
 
-    fprintf( pFile, "  assign _o_ = { " );
+    fprintf( pFile, "  assign { " );
+    Gia_ManDumpIoList( p, pFile, 1 );       
+    fprintf( pFile, " } = { " );    
     Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL );
     fprintf( pFile, " };\n\n" );
 
@@ -1922,9 +2026,14 @@ void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName )
     fprintf( pFile, "module " );
     Gia_ManDumpModuleName( pFile, p->pName );
     fprintf( pFile, "_wrapper" );
-    fprintf( pFile, " ( _i_, _o_ );\n\n" );
+    fprintf( pFile, " ( " );
-    fprintf( pFile, "  input  [%d:0] _i_;\n",   Gia_ManCiNum(p)-1 );
+    Gia_ManDumpIoList( p, pFile, 0 );
-    fprintf( pFile, "  output [%d:0] _o_;\n\n", Gia_ManCoNum(p)-1 );
+    fprintf( pFile, ", " );
+    Gia_ManDumpIoList( p, pFile, 1 );    
+    fprintf( pFile, " );\n\n" );
+    Gia_ManDumpIoRanges( p, pFile, 0 );
+    Gia_ManDumpIoRanges( p, pFile, 1 );
+    fprintf( pFile, "\n" );
 
     fprintf( pFile, "  wire " );
     Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
@@ -1936,9 +2045,13 @@ void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName )
 
     fprintf( pFile, "  assign { " );
     Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL );
-    fprintf( pFile, " } = _i_;\n\n" );
+    fprintf( pFile, " } = { " );
+    Gia_ManDumpIoList( p, pFile, 0 );    
+    fprintf( pFile, " };\n\n" );    
 
-    fprintf( pFile, "  assign _o_ = { " );
+    fprintf( pFile, "  assign { " );
+    Gia_ManDumpIoList( p, pFile, 1 );       
+    fprintf( pFile, " } = { " );    
     Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL );
     fprintf( pFile, " };\n\n" );
 

src/base/cmd/cmd.c

@@ -37,6 +37,7 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 
 static int CmdCommandTime          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int CmdCommandSleep         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandEcho          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandQuit          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandAbcrc         ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -90,6 +91,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
     Cmd_HistoryRead( pAbc );
 
     Cmd_CommandAdd( pAbc, "Basic", "time",          CmdCommandTime,            0 );
+    Cmd_CommandAdd( pAbc, "Basic", "sleep",         CmdCommandSleep,           0 );
     Cmd_CommandAdd( pAbc, "Basic", "echo",          CmdCommandEcho,            0 );
     Cmd_CommandAdd( pAbc, "Basic", "quit",          CmdCommandQuit,            0 );
     Cmd_CommandAdd( pAbc, "Basic", "abcrc",         CmdCommandAbcrc,           0 );
@@ -228,6 +230,65 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv )
     return 1;
 }
 
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int CmdCommandSleep( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    abctime clkStop;
+    char * pFileName = NULL;
+    int c, nSecs = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nSecs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nSecs < 0 )
+                goto usage;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( argc == globalUtilOptind + 1 ) {
+        FILE * pFile = NULL;
+        pFileName = argv[globalUtilOptind];
+        while ( (pFile = fopen(pFileName, "rb")) == NULL );
+        if ( pFile != NULL )
+            fclose( pFile );
+    }
+
+    clkStop = Abc_Clock() + nSecs * CLOCKS_PER_SEC;
+    while ( Abc_Clock() < clkStop );
+    return 0;
+
+  usage:
+    fprintf( pAbc->Err, "usage: sleep [-N <num>] [-h] <file_name>\n" );
+    fprintf( pAbc->Err, "\t              puts ABC to sleep for some time\n" );
+    fprintf( pAbc->Err, "\t-N num      : time duration in seconds [default = %d]\n", nSecs );    
+    fprintf( pAbc->Err, "\t-h          : toggle printing the command usage\n" );
+    fprintf( pAbc->Err, "\t<file_name> : (optional) waiting begins after the file is created\n" );    
+    return 1;
+}
 /**Function********************************************************************
 
   Synopsis    []

src/base/wlc/wlc.h

@@ -448,7 +448,7 @@ extern void           Wlc_NtkDeleteSim( Vec_Ptr_t * p );
 extern int            Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd );
 /*=== wlcReadVer.c ========================================================*/
 extern char *         Wlc_PrsConvertInitValues( Wlc_Ntk_t * p );
-extern Wlc_Ntk_t *    Wlc_ReadVer( char * pFileName, char * pStr );
+extern Wlc_Ntk_t *    Wlc_ReadVer( char * pFileName, char * pStr, int fInter );
 /*=== wlcUif.c ========================================================*/
 extern Vec_Int_t *    Wlc_NtkCollectAddMult( Wlc_Ntk_t * p, Wlc_BstPar_t * pPar, int * pCountA, int * CountM );
 extern int            Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 );

src/base/wlc/wlcBlast.c

@@ -2667,6 +2667,71 @@ Vec_Int_t * Wlc_ComputePerm( Wlc_Ntk_t * pNtk, int nPis )
     return vPerm;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_TransferPioNames( Wlc_Ntk_t * p, Gia_Man_t * pNew )
+{
+    int fSkipBitRange = 0;
+    Wlc_Obj_t * pObj; int i, k;
+    Vec_PtrFreeP( &pNew->vNamesIn );
+    Vec_PtrFreeP( &pNew->vNamesOut );
+    pNew->vNamesIn = Vec_PtrAlloc( Gia_ManPiNum(pNew) );
+    pNew->vNamesOut = Vec_PtrAlloc( Gia_ManPoNum(pNew) );
+    // create input names
+    Wlc_NtkForEachCi( p, pObj, i )
+    if ( Wlc_ObjIsPi(pObj) )
+    {
+        char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
+        int nRange = Wlc_ObjRange( pObj );
+        if ( fSkipBitRange && nRange == 1 )
+            Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(pName) );
+        else
+            for ( k = 0; k < nRange; k++ )
+            {
+                char Buffer[1000];
+                sprintf( Buffer, "%s[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
+                Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
+                //printf( "Writing %s\n", Buffer );
+            }
+    }    
+    // add real primary outputs
+    Wlc_NtkForEachCo( p, pObj, i )
+    if ( Wlc_ObjIsPo(pObj) )
+    {
+        char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
+        int nRange = Wlc_ObjRange( pObj );
+        if ( fSkipBitRange && nRange == 1 )
+            Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
+        else
+            for ( k = 0; k < nRange; k++ )
+            {
+                char Buffer[1000];
+                sprintf( Buffer, "%s[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
+                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
+            }
+    }
+    if ( Vec_PtrSize(pNew->vNamesIn) != Gia_ManPiNum(pNew) ) 
+        printf( "The number of input bits (%d) does not match the number of primary inputs (%d) in the current AIG.\n", Vec_PtrSize(pNew->vNamesIn), Gia_ManPiNum(pNew) );
+    if ( Vec_PtrSize(pNew->vNamesOut) != Gia_ManPoNum(pNew) ) 
+        printf( "The number of output bits (%d) does not match the number of primary inputs (%d) in the current AIG.\n", Vec_PtrSize(pNew->vNamesOut), Gia_ManPoNum(pNew) );
+    if ( Vec_PtrSize(pNew->vNamesIn) != Gia_ManPiNum(pNew) || Vec_PtrSize(pNew->vNamesOut) != Gia_ManPoNum(pNew) ) 
+    {
+        Vec_PtrFreeP( &pNew->vNamesIn );
+        Vec_PtrFreeP( &pNew->vNamesOut );
+    }
+    else
+        printf( "Successfully transferred the primary input/output names from the word-level design to the current AIG.\n" );
+}
+    
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/wlc/wlcCom.c

@@ -149,14 +149,16 @@ void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )
 ******************************************************************************/
 int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    extern void Wlc_TransferPioNames( Wlc_Ntk_t * p, Gia_Man_t * pNew );
     FILE * pFile;
     Wlc_Ntk_t * pNtk = NULL;
     char * pFileName = NULL;
     int fOldParser   =    0;
     int fPrintTree   =    0;
+    int fInter       =    0;
     int c, fVerbose  =    0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "opvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "opivh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -166,6 +168,9 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             fPrintTree ^= 1;
             break;
+        case 'i':
+            fInter ^= 1;
+            break;  
         case 'v':
             fVerbose ^= 1;
             break;
@@ -194,7 +199,11 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform reading
     if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  ) 
-        pNtk = Wlc_ReadVer( pFileName, NULL );
+    {
+        pNtk = Wlc_ReadVer( pFileName, NULL, fInter );
+        if ( fInter && pAbc->pGia )
+            Wlc_TransferPioNames( pNtk, pAbc->pGia );
+    }
     else if ( !strcmp( Extra_FileNameExtension(pFileName), "smt" ) || !strcmp( Extra_FileNameExtension(pFileName), "smt2" )  )
         pNtk = Wlc_ReadSmt( pFileName, fOldParser, fPrintTree );
     else if ( !strcmp( Extra_FileNameExtension(pFileName), "ndr" )  )
@@ -207,10 +216,11 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_AbcUpdateNtk( pAbc, pNtk );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%read [-opvh] <file_name>\n" );
+    Abc_Print( -2, "usage: %%read [-opivh] <file_name>\n" );
     Abc_Print( -2, "\t         reads word-level design from Verilog file\n" );
     Abc_Print( -2, "\t-o     : toggle using old SMT-LIB parser [default = %s]\n", fOldParser? "yes": "no" );
     Abc_Print( -2, "\t-p     : toggle printing parse SMT-LIB tree [default = %s]\n", fPrintTree? "yes": "no" );
+    Abc_Print( -2, "\t-i     : toggle reading interface only [default = %s]\n", fInter? "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/base/wlc/wlcReadVer.c

@@ -951,7 +951,7 @@ int Wlc_PrsReadDeclaration( Wlc_Prs_t * p, char * pStart )
     }
     return 1;
 }
-int Wlc_PrsDerive( Wlc_Prs_t * p )
+int Wlc_PrsDerive( Wlc_Prs_t * p, int fInter )
 {
     Wlc_Obj_t * pObj;
     char * pStart, * pName;
@@ -1031,6 +1031,8 @@ startword:
             while ( (pName = Wlc_PrsStrtok( NULL, "(,)" )) )
             {
                 pName = Wlc_PrsSkipSpaces( pName );
+                if ( fInter && Wlc_PrsStrCmp( pName, "wire" ) )
+                    return 0;
                 if ( Wlc_PrsStrCmp( pName, "input" ) || Wlc_PrsStrCmp( pName, "output" ) || Wlc_PrsStrCmp( pName, "wire" ) )
                 {
                     if ( !Wlc_PrsReadDeclaration( p, pName ) )
@@ -1095,12 +1097,16 @@ startword:
         // these are read as part of the interface
         else if ( Wlc_PrsStrCmp( pStart, "input" ) || Wlc_PrsStrCmp( pStart, "output" ) || Wlc_PrsStrCmp( pStart, "wire" ) || Wlc_PrsStrCmp( pStart, "reg" ) )
         {
+            if ( fInter && (Wlc_PrsStrCmp( pStart, "wire" ) || Wlc_PrsStrCmp( pStart, "reg" )) )
+                return 0;            
             if ( !Wlc_PrsReadDeclaration( p, pStart ) )
                 return 0;
         }
         else if ( Wlc_PrsStrCmp( pStart, "assign" ) )
         {
             int Type, NameId, fFound, XValue = 0;
+            if ( fInter )
+                return 0;
             pStart += strlen("assign");
             // read name
             pStart = Wlc_PrsFindName( pStart, &pName );
@@ -1159,6 +1165,8 @@ startword:
         {
             // THIS IS A HACK to detect always statement representing combinational MUX
             int NameId, NameIdOut = -1, fFound, nValues, fDefaultFound = 0;
+            if ( fInter )
+                return 0;
             // find control
             pStart = Wlc_PrsFindWord( pStart, "case", &fFound );
             if ( pStart == NULL )
@@ -1682,7 +1690,7 @@ startword:
     }
     return 1;
 }
-Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr )
+Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr, int fInter )
 {
     Wlc_Prs_t * p;
     Wlc_Ntk_t * pNtk = NULL;
@@ -1696,8 +1704,23 @@ Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr )
     if ( !Wlc_PrsPrepare( p ) )
         goto finish;
     // parse models
-    if ( !Wlc_PrsDerive( p ) )
+    if ( !Wlc_PrsDerive( p, fInter ) )
+    {
+        if ( fInter )
+        {
+            printf( "Finished deriving interface for module \"%s\".\n", p->pNtk->pName );
+            pNtk = p->pNtk;  p->pNtk = NULL;
+            pNtk->pSpec = Abc_UtilStrsav( pFileName );
+            if ( Vec_IntSize(&pNtk->vNameIds) == 0 ) 
+            {
+                Vec_Int_t * vTemp = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) );
+                pNtk->vNameIds = *vTemp, Vec_IntZero(vTemp);
+                Vec_IntFree( vTemp );
+            }
+            return pNtk;
+        }
         goto finish;
+    }
     // derive topological order
     if ( p->pNtk )
     {
@@ -1728,7 +1751,7 @@ finish:
 void Io_ReadWordTest( char * pFileName )
 {
     Gia_Man_t * pNew;
-    Wlc_Ntk_t * pNtk = Wlc_ReadVer( pFileName, NULL );
+    Wlc_Ntk_t * pNtk = Wlc_ReadVer( pFileName, NULL, 0 );
     if ( pNtk == NULL )
         return;
     Wlc_WriteVer( pNtk, "test.v", 0, 0 );

src/map/scl/sclLiberty.c

@@ -281,26 +281,38 @@ static inline char * Scl_LibertyFindMatch( char * pPos, char * pEnd )
     assert( *pPos == '(' || *pPos == '{' );
     if ( *pPos == '(' )
     {
-        for ( ; pPos < pEnd; pPos++ )
+      ++Counter;
-        {
+      ++pPos;
-            if ( *pPos == '(' )
+      for ( ; pPos < pEnd; pPos++ )
+      {
+            // Invariant: Counter > 0.
+            if ( *pPos == '(' ) {
                 Counter++;
-            if ( *pPos == ')' )
+                continue;
+            }
+            else if ( *pPos == ')' ) {
                 Counter--;
-            if ( Counter == 0 )
+                if ( Counter == 0 )
-                break;
+                  break;
+            }
         }
     }
     else
     {
+        ++Counter;
+        ++pPos;
         for ( ; pPos < pEnd; pPos++ )
         {
-            if ( *pPos == '{' )
+            // Invariant: Counter > 0.
+            if ( *pPos == '{' ) {
                 Counter++;
-            if ( *pPos == '}' )
+                continue;
+            }
+            else if ( *pPos == '}' ) {
                 Counter--;
-            if ( Counter == 0 )
+                if ( Counter == 0 )
-                break;
+                  break;
+            }
         }
     }
     assert( *pPos == ')' || *pPos == '}' );
@@ -317,10 +329,14 @@ static inline Scl_Pair_t Scl_LibertyUpdateHead( Scl_Tree_t * p, Scl_Pair_t Head
     char * pChar;
     for ( pChar = pBeg; pChar < pEnd; pChar++ )
     {
-        if ( *pChar == '\n' )
+        if ( *pChar == '\n' ) {
             p->nLines++;
-        if ( Scl_LibertyCharIsSpace(*pChar) )
+            // Note: Scl_LibertyCharIsSpace returns true for '\n', so we can
+            // continue here and save the call to Scl_LibertyCharIsSpace.
             continue;
+        } else if ( Scl_LibertyCharIsSpace(*pChar) ) {
+            continue;
+        }
         pLastNonSpace = pChar;
         if ( pFirstNonSpace == NULL )
             pFirstNonSpace = pChar;