Version abc80207

7 files changed, 344 insertions, 38 deletions

diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index de517705..c882672b 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -1025,7 +1025,7 @@ int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk )
     return LevelsMax;
 }
 
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Recursively detects combinational loops.]
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 266f8075..4b872aa3 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3130,7 +3130,7 @@ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nWindow      = 62;
     pPars->nCands       =  5;
     pPars->nSimWords    =  4;
-    pPars->nGrowthLevel =  0;
+    pPars->nGrowthLevel =  1;
     pPars->fArea        =  0;
     pPars->fVerbose     =  0;
     pPars->fVeryVerbose =  0;
@@ -3225,7 +3225,7 @@ usage:
     fprintf( pErr, "\t-W <NM>  : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
     fprintf( pErr, "\t-C <num> : the max number of resub candidates (1 <= n) [default = %d]\n", pPars->nCands );
     fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
-    fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
+    fprintf( pErr, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     fprintf( pErr, "\t-a       : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" );
     fprintf( pErr, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w       : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
@@ -3264,13 +3264,15 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nDepthMax    =  20;
     pPars->nDivMax      = 200;
     pPars->nWinSizeMax  = 300;
-    pPars->nGrowthLevel =   0;
+    pPars->nGrowthLevel =   1;
     pPars->fResub       =   1;
     pPars->fArea        =   0;
+    pPars->fMoreEffort  =   0;
+    pPars->fSwapEdge    =   0;
     pPars->fVerbose     =   0;
     pPars->fVeryVerbose =   0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLravwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLraesvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3335,6 +3337,12 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             pPars->fArea ^= 1;
             break;
+        case 'e':
+            pPars->fMoreEffort ^= 1;
+            break;
+        case 's':
+            pPars->fSwapEdge ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -3368,15 +3376,17 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: mfs [-WFDML <num>] [-arvh]\n" );
+    fprintf( pErr, "usage: mfs [-WFDML <num>] [-raesvh]\n" );
     fprintf( pErr, "\t           performs don't-care-based optimization of logic networks\n" );
     fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
     fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
     fprintf( pErr, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
     fprintf( pErr, "\t-M <num> : the max size of  window to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
-    fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
-    fprintf( pErr, "\t-a       : toggle minimizing area or edges [default = %s]\n", pPars->fArea? "area": "edges" );
+    fprintf( pErr, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     fprintf( pErr, "\t-r       : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" );
+    fprintf( pErr, "\t-a       : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
+    fprintf( pErr, "\t-e       : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
+    fprintf( pErr, "\t-s       : toggle evaluation of edge swapping [default = %s]\n", pPars->fSwapEdge? "yes": "no" );
     fprintf( pErr, "\t-v       : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w       : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : print the command usage\n");
@@ -6208,12 +6218,14 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fSorter;
     int fMesh;
     int fFpga;
+    int fOneHot;
     int fVerbose;
     char * FileName;
     extern void Abc_GenAdder( char * pFileName, int nVars );
     extern void Abc_GenSorter( char * pFileName, int nVars );
     extern void Abc_GenMesh( char * pFileName, int nVars );
     extern void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars );
+    extern void Abc_GenOneHot( char * pFileName, int nVars );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -6226,9 +6238,10 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     fSorter = 0;
     fMesh = 0;
     fFpga = 0;
+    fOneHot = 0;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmfvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmftvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -6255,6 +6268,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             fFpga ^= 1;
             break;
+        case 't':
+            fOneHot ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -6282,18 +6298,21 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_GenFpga( FileName, 4, 3, 10 );
 //        Abc_GenFpga( FileName, 2, 2, 3 );
 //        Abc_GenFpga( FileName, 3, 2, 5 );
+    else if ( fOneHot )
+        Abc_GenOneHot( FileName, nVars );
     else
         printf( "Type of circuit is not specified.\n" );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: gen [-N] [-asmfvh] <file>\n" );
+    fprintf( pErr, "usage: gen [-N num] [-asmftvh] <file>\n" );
     fprintf( pErr, "\t         generates simple circuits\n" );
     fprintf( pErr, "\t-N num : the number of variables [default = %d]\n", nVars );  
     fprintf( pErr, "\t-a     : generate ripple-carry adder [default = %s]\n", fAdder? "yes": "no" );  
     fprintf( pErr, "\t-s     : generate a sorter [default = %s]\n", fSorter? "yes": "no" );  
     fprintf( pErr, "\t-m     : generate a mesh [default = %s]\n", fMesh? "yes": "no" );  
     fprintf( pErr, "\t-f     : generate a LUT FPGA structure [default = %s]\n", fFpga? "yes": "no" );  
+    fprintf( pErr, "\t-t     : generate one-hotness conditions [default = %s]\n", fOneHot? "yes": "no" );  
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     fprintf( pErr, "\t<file> : output file name\n");
@@ -6634,7 +6653,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
     extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
-    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
+//    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
     extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
 //    extern void Abc_NtkDarTestBlif( char * pFileName );
 
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index bfb41374..0b66c476 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -504,6 +504,48 @@ void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars )
     fclose( pFile );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Generates structure of L K-LUTs implementing an N-var function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_GenOneHot( char * pFileName, int nVars )
+{
+    FILE * pFile;
+    int i, k, Counter, nDigitsIn, nDigitsOut;
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# One-hotness condition for %d vars generated by ABC on %s\n", nVars, Extra_TimeStamp() );
+    fprintf( pFile, ".model 1hot_%dvars\n", nVars );
+    fprintf( pFile, ".inputs" );
+    nDigitsIn = Extra_Base10Log( nVars );
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " i%0*d", nDigitsIn, i );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, ".outputs" );
+    nDigitsOut = Extra_Base10Log( nVars * (nVars - 1) / 2 );
+    for ( i = 0; i < nVars * (nVars - 1) / 2; i++ )
+        fprintf( pFile, " o%0*d", nDigitsOut, i );
+    fprintf( pFile, "\n" );
+    Counter = 0;
+    for ( i = 0; i < nVars; i++ )
+        for ( k = i+1; k < nVars; k++ )
+        {
+            fprintf( pFile, ".names i%0*d i%0*d o%0*d\n", nDigitsIn, i, nDigitsIn, k, nDigitsOut, Counter ); 
+            fprintf( pFile, "11 0\n" ); 
+            Counter++;
+        }
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+    fclose( pFile );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 257d930f..a054a474 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -1130,6 +1130,7 @@ int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd )
     pNode = Abc_NtkCreatePo( pNtk );
     Abc_ObjAddFanin( pNode, pMiter );
     Abc_ObjAssignName( pNode, "miter", NULL );
+    Abc_NtkOrderCisCos( pNtk );
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtk ) )
     {
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 2dc03d5c..8640b7a8 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -46,6 +46,7 @@ static int CmdCommandRecall        ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int CmdCommandEmpty         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 #ifdef WIN32
 static int CmdCommandLs            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int CmdCommandScrGen        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 #endif
 static int CmdCommandSis           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandMvsis         ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -86,6 +87,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Basic", "empty",     CmdCommandEmpty,          0); 
 #ifdef WIN32
     Cmd_CommandAdd( pAbc, "Basic", "ls",        CmdCommandLs,             0 );
+    Cmd_CommandAdd( pAbc, "Basic", "scrgen",    CmdCommandScrGen,         0 );
 #endif
 
     Cmd_CommandAdd( pAbc, "Various", "sis",     CmdCommandSis,            1); 
@@ -1068,17 +1070,6 @@ usage:
 
 
 #ifdef WIN32
-/**Function*************************************************************
-
-  Synopsis    [Command to print the contents of the current directory (Windows).]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 #include <io.h>
 
 // these structures are defined in <io.h> but are for some reason invisible
@@ -1097,6 +1088,20 @@ extern long _findfirst( char *filespec, struct _finddata_t *fileinfo );
 extern int  _findnext( long handle, struct _finddata_t *fileinfo );
 extern int  _findclose( long handle );
 
+extern char * _getcwd( char * buffer, int maxlen );
+extern int    _chdir( const char *dirname );
+
+/**Function*************************************************************
+
+  Synopsis    [Command to print the contents of the current directory (Windows).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int CmdCommandLs( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     struct _finddata_t c_file;
@@ -1181,15 +1186,238 @@ int CmdCommandLs( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "Usage: ls [-l] [-b]\n" );
+    fprintf( pAbc->Err, "usage: ls [-l] [-b]\n" );
     fprintf( pAbc->Err, "       print the file names in the current directory\n" );
     fprintf( pAbc->Err, "        -l : print in the long format [default = short]\n" );
     fprintf( pAbc->Err, "        -b : print only .mv files [default = all]\n" );
     return 1; 
 }
-#endif
 
 
+/**Function*************************************************************
+
+  Synopsis    [Generates the script for running ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CmdCommandScrGen( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    struct _finddata_t c_file;
+    long   hFile;
+    FILE * pFile = NULL;
+    char * pFileStr = "test.s";
+    char * pDirStr = NULL;
+    char * pComStr = "ps";
+    char * pWriteStr = NULL;
+    char   Buffer[1000], Line[2000];
+    int    nFileNameMax, nFileNameCur;
+    int    Counter = 0;
+    int    fUseCurrent;
+    char   c;
+
+    fUseCurrent = 0;
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "FDCWch") ) != EOF )
+    {
+        switch (c)
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-F\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pFileStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-D\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pDirStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-C\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pComStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-W\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pWriteStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'c':
+            fUseCurrent ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+//    printf( "File = %s.\n", pFileStr );
+//    printf( "Dir = %s.\n", pDirStr );
+//    printf( "Com = %s.\n", pComStr );
+    if ( pDirStr == NULL )
+        fUseCurrent = 1;
+
+    if ( _getcwd( Buffer, 1000 ) == NULL )
+    {
+        printf( "Cannot get the current directory.\n" );
+        return 0;
+    }
+    if ( fUseCurrent )
+        pFile = fopen( pFileStr, "w" );
+    if ( pDirStr )
+    {
+        if ( _chdir(pDirStr) )
+        {
+            printf( "Cannot change to directory: %s\n", pDirStr );
+            return 0;
+        }
+    }
+    if ( !fUseCurrent )
+        pFile = fopen( pFileStr, "w" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file %s.\n", pFileStr );
+        if ( pDirStr && _chdir(Buffer) )
+        {
+            printf( "Cannot change to the current directory: %s\n", Buffer );
+            return 0;
+        }
+        return 0;
+    }
+
+    // find the first file in the directory
+    if( (hFile = _findfirst( "*.*", &c_file )) == -1L )
+    {
+        if ( pDirStr )
+            printf( "No files in the current directory.\n" );
+        else
+            printf( "No files in directory: %s\n", pDirStr );
+        if ( pDirStr && _chdir(Buffer) )
+        {
+            printf( "Cannot change to the current directory: %s\n", Buffer );
+            return 0;
+        }
+    }
+
+    // get the longest file name
+    {
+        nFileNameMax = 0;
+        do
+        {
+            // skip script and txt files
+            nFileNameCur = strlen(c_file.name);
+            if ( c_file.name[nFileNameCur-1] == '.' )
+                continue;
+            if ( nFileNameCur > 2 &&
+                 c_file.name[nFileNameCur-1] == 's' && 
+                 c_file.name[nFileNameCur-2] == '.' ) 
+                 continue;
+            if ( nFileNameCur > 4 &&
+                 c_file.name[nFileNameCur-1] == 't' && 
+                 c_file.name[nFileNameCur-2] == 'x' && 
+                 c_file.name[nFileNameCur-3] == 't' && 
+                 c_file.name[nFileNameCur-4] == '.' ) 
+                 continue;
+            if ( nFileNameMax < nFileNameCur )
+                nFileNameMax = nFileNameCur;
+        }
+        while( _findnext( hFile, &c_file ) == 0 );
+        _findclose( hFile );
+    }
+
+    // print the script file
+    {
+        if( (hFile = _findfirst( "*.*", &c_file )) == -1L )
+        {
+            if ( pDirStr )
+                printf( "No files in the current directory.\n" );
+            else
+                printf( "No files in directory: %s\n", pDirStr );
+        }
+        fprintf( pFile, "# Script file produced by ABC on %s\n", Extra_TimeStamp() );
+        fprintf( pFile, "# Command line was: scrgen -F %s -D %s -C \"%s\"%s%s\n", 
+            pFileStr, pDirStr, pComStr, pWriteStr?" -W ":"", pWriteStr?pWriteStr:"" );
+        do
+        {
+            // skip script and txt files
+            nFileNameCur = strlen(c_file.name);
+            if ( c_file.name[nFileNameCur-1] == '.' )
+                continue;
+            if ( nFileNameCur > 2 &&
+                 c_file.name[nFileNameCur-1] == 's' && 
+                 c_file.name[nFileNameCur-2] == '.' ) 
+                 continue;
+            if ( nFileNameCur > 4 &&
+                 c_file.name[nFileNameCur-1] == 't' && 
+                 c_file.name[nFileNameCur-2] == 'x' && 
+                 c_file.name[nFileNameCur-3] == 't' && 
+                 c_file.name[nFileNameCur-4] == '.' ) 
+                 continue;
+            sprintf( Line, "r %s%s%-*s ; %s", pDirStr?pDirStr:"", pDirStr?"/":"", nFileNameMax, c_file.name, pComStr );
+            for ( c = (int)strlen(Line)-1; c >= 0; c-- )
+                if ( Line[c] == '\\' )
+                    Line[c] = '/';
+            fprintf( pFile, "%s", Line );
+            if ( pWriteStr )
+            {
+                sprintf( Line, " ; w %s/%-*s", pWriteStr, nFileNameMax, c_file.name );
+                for ( c = (int)strlen(Line)-1; c >= 0; c-- )
+                    if ( Line[c] == '\\' )
+                        Line[c] = '/';
+                fprintf( pFile, "%s", Line );
+            }
+            fprintf( pFile, "\n", Line );
+        }
+        while( _findnext( hFile, &c_file ) == 0 );
+        _findclose( hFile );
+    }
+    fclose( pFile );
+    if ( pDirStr && _chdir(Buffer) )
+    {
+        printf( "Cannot change to the current directory: %s\n", Buffer );
+        return 0;
+    }
+
+    // report
+    if ( fUseCurrent )
+        printf( "Script file \"%s\" was saved in the current directory.\n", pFileStr );
+    else
+        printf( "Script file \"%s\" was saved in directory: %s\n", pFileStr, pDirStr );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: scrgen -F <str> -D <str> -C <str> -W <str> -ch\n" );
+    fprintf( pAbc->Err, "\t          generates script for running ABC\n" );
+    fprintf( pAbc->Err, "\t-F str  : the name of the script file [default = \"test.s\"]\n" );
+    fprintf( pAbc->Err, "\t-D str  : the directory to read files from [default = current]\n" );
+    fprintf( pAbc->Err, "\t-C str  : the sequence of commands to run [default = \"ps\"]\n" );
+    fprintf( pAbc->Err, "\t-W str  : the directory to write the resulting files [default = no writing]\n" );
+    fprintf( pAbc->Err, "\t-c      : toggle placing file in current/target dir [default = %s]\n", fUseCurrent? "current": "target" );
+    fprintf( pAbc->Err, "\t-h      : print the command usage\n\n");
+    fprintf( pAbc->Err, "\tExample : scrgen -F test1.s -D a/in -C \"ps; st; ps\" -W a/out\n" );
+    return 1; 
+}
+#endif
+
 
 #ifdef WIN32
 #define unlink _unlink
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index d0750178..ffa25c7f 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -218,7 +218,20 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
     p->pNtkCur = pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
     // read the model name
     if ( strcmp( p->vTokens->pArray[0], ".model" ) == 0 )
-        pNtk->pName = Extra_UtilStrsav( p->vTokens->pArray[1] );
+    {
+        char * pToken, * pPivot;
+        if ( Vec_PtrSize(p->vTokens) != 2 )
+        {
+            p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
+            sprintf( p->sError, "The .model line does not have exactly two entries." );
+            Io_ReadBlifPrintErrorMessage( p );
+            return NULL;
+        }
+        for ( pPivot = pToken = Vec_PtrEntry(p->vTokens, 1); *pToken; pToken++ )
+            if ( *pToken == '/' || *pToken == '\\' )
+                pPivot = pToken+1;
+        pNtk->pName = Extra_UtilStrsav( pPivot );
+    }
     else if ( strcmp( p->vTokens->pArray[0], ".exdc" ) != 0 ) 
     {
         printf( "%s: File parsing skipped after line %d (\"%s\").\n", p->pFileName, 
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 97f2fbf3..8a1fe309 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -90,7 +90,7 @@ static Io_MvMod_t *      Io_MvModAlloc();
 static void              Io_MvModFree( Io_MvMod_t * p );
 static char *            Io_MvLoadFile( char * pFileName );
 static void              Io_MvReadPreparse( Io_MvMan_t * p );
-static void              Io_MvReadInterfaces( Io_MvMan_t * p );
+static int               Io_MvReadInterfaces( Io_MvMan_t * p );
 static Abc_Lib_t *       Io_MvParse( Io_MvMan_t * p );
 static int               Io_MvParseLineModel( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineInputs( Io_MvMod_t * p, char * pLine );
@@ -128,7 +128,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     FILE * pFile;
     Io_MvMan_t * p;
     Abc_Ntk_t * pNtk;
-    Abc_Lib_t * pDesign;
+    Abc_Lib_t * pDesign = NULL;
     char * pDesignName;
     int RetValue, i;
 
@@ -161,10 +161,9 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     p->pDesign->pManFunc = NULL;
     // prepare the file for parsing
     Io_MvReadPreparse( p );
-    // parse interfaces of each network
-    Io_MvReadInterfaces( p );
-    // construct the network
-    pDesign = Io_MvParse( p );
+    // parse interfaces of each network and construct the network
+    if ( Io_MvReadInterfaces( p ) )
+        pDesign = Io_MvParse( p );
     if ( p->sError[0] )
         fprintf( stdout, "%s\n", p->sError );
     Io_MvFree( p );
@@ -646,7 +645,7 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static void Io_MvReadInterfaces( Io_MvMan_t * p )
+static int Io_MvReadInterfaces( Io_MvMan_t * p )
 {
     Io_MvMod_t * pMod;
     char * pLine;
@@ -656,22 +655,23 @@ static void Io_MvReadInterfaces( Io_MvMan_t * p )
     {
         // parse the model
         if ( !Io_MvParseLineModel( pMod, pMod->pName ) )
-            return;
+            return 0;
         // add model to the design
         if ( !Abc_LibAddModel( p->pDesign, pMod->pNtk ) )
         {
             sprintf( p->sError, "Line %d: Model %s is defined twice.", Io_MvGetLine(p, pMod->pName), pMod->pName );
-            return;
+            return 0;
         }
         // parse the inputs
         Vec_PtrForEachEntry( pMod->vInputs, pLine, k )
             if ( !Io_MvParseLineInputs( pMod, pLine ) )
-                return;
+                return 0;
         // parse the outputs
         Vec_PtrForEachEntry( pMod->vOutputs, pLine, k )
             if ( !Io_MvParseLineOutputs( pMod, pLine ) )
-                return;
+                return 0;
     }
+    return 1;
 }
 
 
@@ -767,7 +767,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
 static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    char * pToken;
+    char * pToken, * pPivot;
     Io_MvSplitIntoTokens( vTokens, pLine, '\0' );
     pToken = Vec_PtrEntry( vTokens, 0 );
     assert( !strcmp(pToken, "model") );
@@ -782,7 +782,10 @@ static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine )
         p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLIFMV, 1 );
     else 
         p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
-    p->pNtk->pName = Extra_UtilStrsav( Vec_PtrEntry(vTokens, 1) );
+    for ( pPivot = pToken = Vec_PtrEntry(vTokens, 1); *pToken; pToken++ )
+        if ( *pToken == '/' || *pToken == '\\' )
+            pPivot = pToken+1;
+    p->pNtk->pName = Extra_UtilStrsav( pPivot );
     return 1;
 }