Version abc80912

3 files changed, 188 insertions, 4 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3c7314ef..0db761c7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -199,6 +199,7 @@ static int Abc_CommandCycle          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandXsim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSim            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDarPhase       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSynch          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCec            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDCec           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -463,6 +464,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "xsim",          Abc_CommandXsim,             0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "sim",           Abc_CommandSim,              0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "phase",         Abc_CommandDarPhase,         1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "synch",         Abc_CommandSynch,            1 );
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dcec",          Abc_CommandDCec,             0 );
@@ -4862,7 +4864,6 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     nArgcNew = argc - globalUtilOptind;
     if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
         return 1;
-
     // compute the miter
     pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, nPartSize, fImplic, fMulti );
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
@@ -14424,6 +14425,121 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandSynch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtkRes, * pNtk1, * pNtk2, * pNtk;
+    char ** pArgvNew;
+    int nArgcNew;
+    int fDelete1, fDelete2;
+    int c;
+    int nWords;
+    int fVerbose;
+
+    extern Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarSynchOne( Abc_Ntk_t * pNtk, int nWords, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nWords   =  32;
+    fVerbose =   1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Wvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nWords <= 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew == 0 )
+    {
+        if ( pNtk == NULL )
+        {
+            fprintf( pErr, "Empty network.\n" );
+            return 1;
+        }
+        pNtkRes = Abc_NtkDarSynchOne( pNtk, nWords, fVerbose );
+    }
+    else
+    {
+        if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
+            return 1;
+        if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
+        {
+            if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+            if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+            printf( "The network has no latches..\n" );
+            return 0;
+        }
+
+        // modify the current network
+        pNtkRes = Abc_NtkDarSynch( pNtk1, pNtk2, nWords, fVerbose );
+        if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+        if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+    }
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Synchronization has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: synch [-W <num>] [-vh] <file1> <file2>\n" );
+    fprintf( pErr, "\t         derives and applies synchronization sequence\n" );
+    fprintf( pErr, "\t-W num : the number of simulation words [default = %d]\n", nWords );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\tfile1  : (optional) the file with the first design\n");
+    fprintf( pErr, "\tfile2  : (optional) the file with the second design\n\n");
+    fprintf( pErr, "\t         If no designs are given on the command line,\n" );
+    fprintf( pErr, "\t         assumes the current network has no initial state,\n" );
+    fprintf( pErr, "\t         derives synchronization sequence and applies it.\n\n" );
+    fprintf( pErr, "\t         If two designs are given on the command line\n" );
+    fprintf( pErr, "\t         assumes both of them have no initial state,\n" );
+    fprintf( pErr, "\t         derives sequences for both designs, synchorinizes\n" );
+    fprintf( pErr, "\t         them, and creates SEC miter comparing two designs.\n\n" );
+    fprintf( pErr, "\t         If only one design is given on the command line,\n" );
+    fprintf( pErr, "\t         considers the second design to be the current network,\n" );
+    fprintf( pErr, "\t         and derives SEC miter for them, as described above.\n" );
+    return 1;
+}
 
 
 /**Function*************************************************************
@@ -14842,6 +14958,8 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
     {
+        if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+        if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
         printf( "The network has no latches. Used combinational command \"cec\".\n" );
         return 0;
     }
@@ -14960,9 +15078,10 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     nArgcNew = argc - globalUtilOptind;
     if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
         return 1;
-
     if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
     {
+        if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+        if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
         printf( "The network has no latches. Used combinational command \"cec\".\n" );
         return 0;
     }
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 37cd6853..f1e5efb0 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2195,6 +2195,71 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarSynchOne( Abc_Ntk_t * pNtk, int nWords, int fVerbose )
+{
+    extern Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose );
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Saig_SynchSequenceApply( pTemp = pMan, nWords, fVerbose );
+    Aig_ManStop( pTemp );
+    if ( pMan == NULL )
+        return NULL;
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs phase abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, int fVerbose )
+{
+    extern Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, int fVerbose );
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan1, * pMan2, * pMan;
+    pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
+    if ( pMan1 == NULL )
+        return NULL;
+    pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
+    if ( pMan2 == NULL )
+    {
+        Aig_ManStop( pMan1 );
+        return NULL;
+    }
+    pMan = Saig_Synchronize( pMan1, pMan2, nWords, fVerbose );
+    Aig_ManStop( pMan1 );
+    Aig_ManStop( pMan2 );
+    if ( pMan == NULL )
+        return NULL;
+    pNtkAig = Abc_NtkFromAigPhase( pMan );
+    pNtkAig->pName = Extra_UtilStrsav("miter");
+    pNtkAig->pSpec = NULL;
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs phase abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInit, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 52d7eb06..880c2b5f 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -146,7 +146,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     // start the file reader
     p = Io_MvAlloc();
     p->fBlifMv   = fBlifMv;
-    p->fUseReset = 0;
+    p->fUseReset = 1;
     p->pFileName = pFileName;
     p->pBuffer   = Io_MvLoadFile( pFileName );
     if ( p->pBuffer == NULL )
@@ -704,7 +704,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
     int i, k;
     // iterate through the models
     Vec_PtrForEachEntry( p->vModels, pMod, i )
-    {
+    { 
         // check if there any MV lines
         if ( Vec_PtrSize(pMod->vMvs) > 0 )
             Abc_NtkStartMvVars( pMod->pNtk );