Version abc71130

5 files changed, 333 insertions, 11 deletions

diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 3072e40f..79b76348 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -913,7 +913,7 @@ int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pObj, * pObjCi;
+    Abc_Obj_t * pObj, * pObjCi, * pFanin;
     int i, nCiId, fRetValue = 1;
     assert( !Abc_NtkIsNetlist(pNtk) );
     Abc_NtkForEachCo( pNtk, pObj, i )
@@ -923,9 +923,11 @@ int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk )
             continue;
         pObjCi = Abc_NtkObj( pNtk, nCiId );
         assert( !strcmp( Abc_ObjName(pObj), Abc_ObjName(pObjCi) ) );
-        if ( Abc_ObjFanin0(pObj) != pObjCi )
+        pFanin = Abc_ObjFanin0(pObj);
+        if ( pFanin != pObjCi )
         {
-            printf( "Abc_NtkCheck: A CI/CO pair share the name (%s) but do not link directly.\n", Abc_ObjName(pObj) );
+            printf( "Abc_NtkCheck: A CI/CO pair share the name (%s) but do not link directly. The name of the CO fanin is %s.\n", 
+                Abc_ObjName(pObj), Abc_ObjName(Abc_ObjFanin0(pObj)) );
             fRetValue = 0;
         }
     }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3f9ffb40..20aa7247 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -164,6 +164,7 @@ static int Abc_CommandPipe           ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSeq            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnseq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRetime         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDRetime        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqFpga        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqMap         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqSweep       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -333,6 +334,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "undc",          Abc_CommandUndc,             1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "pipe",          Abc_CommandPipe,             1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "dretime",       Abc_CommandDRetime,          1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "ssweep",        Abc_CommandSeqSweep,         1 );
@@ -6189,7 +6191,7 @@ usage:
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk;//, * pNtkRes;
     int c;
     int nLevels;
     int fVerbose;
@@ -6204,14 +6206,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     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_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
+    extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fVerbose = 0;
-    nLevels = 1000;
+    fVerbose = 1;
+    nLevels  = 1000;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
     {
@@ -6324,13 +6328,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 */
-/*
+
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
         return 0;
     }
-*/
+
+/*
     if ( Abc_NtkIsStrash(pNtk) )
     {
         fprintf( stdout, "Currently only works for logic circuits.\n" );
@@ -6348,6 +6353,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+*/
+//    Abc_NtkDarHaigRecord( pNtk );
+    Abc_NtkDarClau( pNtk, 1000, fVerbose );
     return 0;
 usage:
     fprintf( pErr, "usage: test [-h]\n" );
@@ -10818,6 +10826,106 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int nStepsMax;
+    int fFastAlgo;
+    int fVerbose;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nStepsMax = 100000;
+    fFastAlgo = 0;
+    fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Savh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-S\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nStepsMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nStepsMax < 0 ) 
+                goto usage;
+            break;
+        case 'a':
+            fFastAlgo ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "The network has no latches. Retiming is not performed.\n" );
+        return 0;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+        return 0;
+    }
+
+    // perform the retiming
+    if ( fFastAlgo )
+        pNtkRes = Abc_NtkDarRetime( pNtk, nStepsMax, fVerbose );
+    else
+        pNtkRes = Abc_NtkDarRetimeF( pNtk, nStepsMax, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Retiming has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dretime [-S num] [-avh]\n" );
+    fprintf( pErr, "\t         retimes the current network forward\n" );
+    fprintf( pErr, "\t-S num : the max number of retiming steps to perform [default = %d]\n", nStepsMax );
+    fprintf( pErr, "\t-a     : enables a fast algorithm [default = %s]\n", fFastAlgo? "yes": "no" );
+    fprintf( pErr, "\t-v     : enables verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ab8614fb..67f22eb7 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -87,7 +87,8 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
     if ( fRegisters )
     {
         pMan->nRegs = Abc_NtkLatchNum(pNtk);
-        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
+//        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
+        pMan->vFlopNums = NULL;
     }
     // transfer the pointers to the basic nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
@@ -198,7 +199,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pObjNew, * pLatch;
     Aig_Obj_t * pObj, * pObjLo, * pObjLi;
-    int i;
+    int i, iNodeId;
 //    assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
     // perform strashing
     pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
@@ -242,7 +243,12 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     {
         if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
             break;
-        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+        iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(Abc_NtkCo(pNtkNew, i)), ABC_OBJ_PI, ABC_OBJ_BO );
+        if ( iNodeId >= 0 )
+            pObjNew = Abc_NtkObj( pNtkNew, iNodeId );
+        else
+            pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
+        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
     }
     // if there are assertions, add them
     if ( pMan->nAsserts > 0 )
@@ -1270,6 +1276,9 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManReduceLachesCount( pMan );
+    if ( pMan->vFlopNums )
+        Vec_IntFree( pMan->vFlopNums ); 
+    pMan->vFlopNums = NULL;
 
     pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
     Aig_ManStop( pTemp );
@@ -1284,6 +1293,65 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return NULL;
+//    Aig_ManReduceLachesCount( pMan );
+    if ( pMan->vFlopNums )
+        Vec_IntFree( pMan->vFlopNums ); 
+    pMan->vFlopNums = NULL;
+
+    pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
+    Aig_ManStop( pTemp );
+
+//    pMan = Aig_ManReduceLaches( pMan, 1 );
+//    pMan = Aig_ManConstReduce( pMan, 1 );
+
+    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
+{
+    Aig_Man_t * pMan;
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return;
+//    Aig_ManReduceLachesCount( pMan );
+    if ( pMan->vFlopNums )
+        Vec_IntFree( pMan->vFlopNums ); 
+    pMan->vFlopNums = NULL;
+    Aig_ManHaigRecord( pMan );
+    Aig_ManStop( pMan );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs random simulation.]
 
   Description []
@@ -1322,6 +1390,39 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
+{
+    extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose );
+    Aig_Man_t * pMan;
+    if ( Abc_NtkPoNum(pNtk) != 1 )
+    {
+        printf( "The number of outputs should be 1.\n" );
+        return 1;
+    }
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return 1;
+//    Aig_ManReduceLachesCount( pMan );
+    if ( pMan->vFlopNums )
+        Vec_IntFree( pMan->vFlopNums ); 
+    pMan->vFlopNums = NULL;
+
+    Fra_Clau( pMan, nStepsMax, fVerbose );
+    Aig_ManStop( pMan );
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 941ef7a7..ed314fcd 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -348,6 +348,8 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Abc_Ntk_t * pTemp;
         pNtk = Io_ReadBlif( pFileName, fCheck );
+        if ( pNtk == NULL )
+            return 1;
         pNtk = Abc_NtkToLogic( pTemp = pNtk );
         Abc_NtkDelete( pTemp );
     }
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index 7a217fd7..322ce720 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -58,6 +58,7 @@ static int  Ver_ParseAlways( Ver_Man_t * p, Abc_Ntk_t * pNtk );
 static int  Ver_ParseInitial( Ver_Man_t * p, Abc_Ntk_t * pNtk );
 static int  Ver_ParseAssign( Ver_Man_t * p, Abc_Ntk_t * pNtk );
 static int  Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType );
+static int  Ver_ParseFlopStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk );
 static int  Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate );
 static int  Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox );
 static int  Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox );
@@ -472,6 +473,9 @@ int Ver_ParseModule( Ver_Man_t * pMan )
         else if ( !strcmp( pWord, "not" ) )
             RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOT );
 
+        else if ( !strcmp( pWord, "dff" ) )
+            RetValue = Ver_ParseFlopStandard( pMan, pNtk );
+
         else if ( !strcmp( pWord, "assign" ) )
             RetValue = Ver_ParseAssign( pMan, pNtk );
         else if ( !strcmp( pWord, "always" ) )
@@ -1366,6 +1370,105 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga
 
 /**Function*************************************************************
 
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseFlopStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Obj_t * pNetLi, * pNetLo, * pLatch;
+    char * pWord, Symbol;
+
+    // convert from the blackbox into the network with local functions representated by AIGs
+    if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
+        return 0;
+
+    // this is gate name - throw it away
+    if ( Ver_StreamPopChar(p) != '(' )
+    {
+        sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    Ver_ParseSkipComments( pMan );
+
+    // parse the output name
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+    // get the net corresponding to this output
+    pNetLo = Ver_ParseFindNet( pNtk, pWord );
+    if ( pNetLo == NULL )
+    {
+        sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    Symbol = Ver_StreamPopChar(p);
+    if ( Symbol == ')' )
+    {
+        sprintf( pMan->sError, "Cannot parse the flop." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    // skip comma
+    if ( Symbol != ',' )
+    {
+        sprintf( pMan->sError, "Cannot parse the flop." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    Ver_ParseSkipComments( pMan );
+
+    // parse the output name
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+    // get the net corresponding to this output
+    pNetLi = Ver_ParseFindNet( pNtk, pWord );
+    if ( pNetLi == NULL )
+    {
+        sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    Symbol = Ver_StreamPopChar(p);
+    if ( Symbol != ')' )
+    {
+        sprintf( pMan->sError, "Cannot parse the flop." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    if ( Ver_StreamPopChar(p) != ';' )
+    {
+        sprintf( pMan->sError, "Cannot parse the flop." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // create the latch
+    pLatch = Ver_ParseCreateLatch( pNtk, pNetLi, pNetLo );
+    Abc_LatchSetInit0( pLatch );
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the index of the given pin the gate.]
 
   Description []
@@ -1606,6 +1709,12 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
     pNode->pCopy = (Abc_Obj_t *)vBundles;
     while ( 1 )
     {
+/*
+        if ( Ver_StreamGetLineNumber(pMan->pReader) == 5967 )
+        {
+           int x = 0;
+        }
+*/
         // allocate the bundle (formal name + array of actual nets)
         pBundle = ALLOC( Ver_Bundle_t, 1 );
         pBundle->pNameFormal = NULL;