Experiments with retiming (adding new APIs).

15 files changed, 132 insertions, 53 deletions

diff --git a/src/aig/miniaig/ndr.h b/src/aig/miniaig/ndr.h
index b33d9c6d..c854debe 100644
--- a/src/aig/miniaig/ndr.h
+++ b/src/aig/miniaig/ndr.h
@@ -579,6 +579,8 @@ static inline void * Ndr_Read( char * pFileName )
     // check file size
     fseek( pFile, 0, SEEK_END );
     nFileSize = ftell( pFile ); 
+    if ( nFileSize % 5 != 0 )
+        return NULL;
     assert( nFileSize % 5 == 0 );
     rewind( pFile );
     // create structure
diff --git a/src/base/main/abcapis.h b/src/base/main/abcapis.h
index 9ac2036a..e384896d 100644
--- a/src/base/main/abcapis.h
+++ b/src/base/main/abcapis.h
@@ -81,6 +81,11 @@ extern ABC_DLL void   Abc_FrameGiaInputMiniLut( Abc_Frame_t * pAbc, void * pMini
 extern ABC_DLL void * Abc_FrameGiaOutputMiniLut( Abc_Frame_t * pAbc );
 extern ABC_DLL char * Abc_FrameGiaOutputMiniLutAttr( Abc_Frame_t * pAbc, void * pMiniLut );
 
+// procedures to input/output NDR data-structure
+extern ABC_DLL void   Abc_FrameInputNdr( Abc_Frame_t * pAbc, void * pData );
+extern ABC_DLL void * Abc_FrameOutputNdr( Abc_Frame_t * pAbc );
+extern ABC_DLL int  * Abc_FrameOutputNdrArray( Abc_Frame_t * pAbc );
+
 // procedures to set CI/CO arrival/required times
 extern ABC_DLL void   Abc_NtkSetCiArrivalTime( Abc_Frame_t * pAbc, int iCi, float Rise, float Fall );
 extern ABC_DLL void   Abc_NtkSetCoRequiredTime( Abc_Frame_t * pAbc, int iCo, float Rise, float Fall );
diff --git a/src/base/main/main.h b/src/base/main/main.h
index d7f68be4..2efb3358 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -89,7 +89,7 @@ extern ABC_DLL void            Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p,
 extern ABC_DLL void            Abc_FrameUnmapAllNetworks( Abc_Frame_t * p );
 extern ABC_DLL void            Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
 
-extern ABC_DLL void               Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
+extern ABC_DLL void            Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
 extern ABC_DLL Abc_Frame_t *   Abc_FrameGetGlobalFrame();
 extern ABC_DLL Abc_Frame_t *   Abc_FrameReadGlobalFrame();
 
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index eff730d8..1d54f4e4 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -22,6 +22,7 @@
 #include "mainInt.h"
 #include "bool/dec/dec.h"
 #include "map/if/if.h"
+#include "aig/miniaig/ndr.h"
 
 #ifdef ABC_USE_CUDD
 #include "bdd/extrab/extraBdd.h"
@@ -83,6 +84,10 @@ int         Abc_FrameReadCexRegNum( Abc_Frame_t * p )        { return s_GlobalFr
 int         Abc_FrameReadCexPo( Abc_Frame_t * p )            { return s_GlobalFrame->pCex->iPo;    }               
 int         Abc_FrameReadCexFrame( Abc_Frame_t * p )         { return s_GlobalFrame->pCex->iFrame; }               
 
+void        Abc_FrameInputNdr( Abc_Frame_t * pAbc, void * pData ) { Ndr_Delete(s_GlobalFrame->pNdr); s_GlobalFrame->pNdr = pData;                        }
+void *      Abc_FrameOutputNdr( Abc_Frame_t * pAbc )         { void * pData = s_GlobalFrame->pNdr; s_GlobalFrame->pNdr = NULL; return pData;             }  
+int *       Abc_FrameOutputNdrArray( Abc_Frame_t * pAbc )    { int * pArray = s_GlobalFrame->pNdrArray; s_GlobalFrame->pNdrArray = NULL; return pArray;  }
+
 void        Abc_FrameSetLibLut( void * pLib )                { s_GlobalFrame->pLibLut   = pLib;    } 
 void        Abc_FrameSetLibBox( void * pLib )                { s_GlobalFrame->pLibBox   = pLib;    } 
 void        Abc_FrameSetLibGen( void * pLib )                { s_GlobalFrame->pLibGen   = pLib;    } 
@@ -232,7 +237,9 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     ABC_FREE( p->pCex );
     Vec_IntFreeP( &p->pAbcWlcInv );
     Abc_NamDeref( s_GlobalFrame->pJsonStrs );
-    Vec_WecFreeP(&s_GlobalFrame->vJsonObjs );    
+    Vec_WecFreeP( &s_GlobalFrame->vJsonObjs );  
+    Ndr_Delete( s_GlobalFrame->pNdr );
+    ABC_FREE( s_GlobalFrame->pNdrArray );
 
     Gia_ManStopP( &p->pGiaMiniAig );
     Gia_ManStopP( &p->pGiaMiniLut );
@@ -240,6 +247,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     Vec_IntFreeP( &p->vCopyMiniLut );
     ABC_FREE( p->pArray );
     ABC_FREE( p->pBoxes );
+    
 
     ABC_FREE( p );
     s_GlobalFrame = NULL;
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index e55e6e7f..7317c36f 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -150,6 +150,8 @@ struct Abc_Frame_t_
     Vec_Int_t *     vCopyMiniLut;
     int *           pArray;
     int *           pBoxes;
+    void *          pNdr;
+    int *           pNdrArray;
 
     Abc_Frame_Callback_BmcFrameDone_Func pFuncOnFrameDone;
 };
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 3a84031e..6547da13 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -282,6 +282,7 @@ static inline int          Wlc_ObjIsPi( Wlc_Obj_t * p )
 static inline int          Wlc_ObjIsPo( Wlc_Obj_t * p )                             { return p->fIsPo;                                                         }
 static inline int          Wlc_ObjIsCi( Wlc_Obj_t * p )                             { return p->Type == WLC_OBJ_PI || p->Type == WLC_OBJ_FO;                   }
 static inline int          Wlc_ObjIsCo( Wlc_Obj_t * p )                             { return p->fIsPo || p->fIsFi;                                             }
+static inline int          Wlc_ObjIsFf( Wlc_Ntk_t * p, int i )                      { return Wlc_NtkObj(p, i)->Type == WLC_OBJ_FF;                             }
 
 static inline int          Wlc_ObjId( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )             { return pObj - p->pObjs;                                                  }
 static inline int          Wlc_ObjCiId( Wlc_Obj_t * p )                             { assert( Wlc_ObjIsCi(p) ); return p->Fanins[1];                           }
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 6df2c840..90ad0671 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "wlc.h"
+#include "base/wln/wln.h"
 #include "base/main/mainInt.h"
 #include "aig/miniaig/ndr.h"
 
@@ -1250,7 +1251,7 @@ usage:
 ******************************************************************************/
 int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Wln_NtkRetimeTest( char * pFileName );
+    extern void Wln_NtkRetimeTest( char * pFileName, int fVerbose );
     FILE * pFile;
     char * pFileName = NULL;
     int c, fVerbose  = 0;
@@ -1268,6 +1269,23 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
+    if ( pAbc->pNdr )
+    {
+        Vec_Int_t * vMoves;
+        Wln_Ntk_t * pNtk = Wln_NtkFromNdr( pAbc->pNdr );
+        Wln_NtkRetimeCreateDelayInfo( pNtk );
+        if ( pNtk == NULL )
+        {
+            printf( "Transforming NDR into internal represnetation has failed.\n" );
+            return 0;
+        }
+        vMoves = Wln_NtkRetime( pNtk, fVerbose );
+        Wln_NtkFree( pNtk );
+        ABC_FREE( pAbc->pNdrArray );
+        if ( vMoves ) pAbc->pNdrArray = Vec_IntReleaseNewArray( vMoves );
+        Vec_IntFreeP( &vMoves );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
     {
         printf( "Abc_CommandRetime(): Input file name should be given on the command line.\n" );
@@ -1284,7 +1302,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     fclose( pFile );
-    Wln_NtkRetimeTest( pFileName );
+    Wln_NtkRetimeTest( pFileName, fVerbose );
     return 0;
 usage:
     Abc_Print( -2, "usage: %%retime [-vh]\n" );
diff --git a/src/base/wlc/wlcNdr.c b/src/base/wlc/wlcNdr.c
index 16c7d778..7591aaf3 100644
--- a/src/base/wlc/wlcNdr.c
+++ b/src/base/wlc/wlcNdr.c
@@ -499,7 +499,8 @@ Wlc_Ntk_t * Wlc_ReadNdr( char * pFileName )
     Wlc_Ntk_t * pNtk = Wlc_NtkFromNdr( pData );
     //char * ppNames[10] = { NULL, "a", "b", "c", "d", "e", "f", "g", "h", "i" };
     //Ndr_WriteVerilog( NULL, pData, ppNames );
-    Ndr_Delete( pData );
+    //Ndr_Delete( pData );
+    Abc_FrameInputNdr( Abc_FrameGetGlobalFrame(), pData );
     return pNtk;
 }
 void Wlc_ReadNdrTest()
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index f64fccaf..8038d9e6 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -357,8 +357,8 @@ int Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p )
 ***********************************************************************/
 void Wlc_NtkCreateLevels_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
 {
-    int k, iFanin, Level = 0;
-    if ( Vec_IntEntry(&p->vLevels, Wlc_ObjId(p, pObj)) > 0 )
+    int k, iFanin, Level = 0, iObj = Wlc_ObjId(p, pObj);
+    if ( Wlc_ObjIsCi(pObj) || Wlc_ObjIsFf(p, iObj) || Wlc_ObjFaninNum(pObj) == 0 || Wlc_ObjLevel(p, pObj) > 0 )
         return;
     Wlc_ObjForEachFanin( pObj, iFanin, k ) if ( iFanin )
         Wlc_NtkCreateLevels_rec( p, Wlc_NtkObj(p, iFanin) );
@@ -368,11 +368,18 @@ void Wlc_NtkCreateLevels_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
 }
 int Wlc_NtkCreateLevels( Wlc_Ntk_t * p )
 {
-    Wlc_Obj_t * pObj;  int i;
+    Wlc_Obj_t * pObj;  int i, LeveMax = 0;
     Vec_IntFill( &p->vLevels, Wlc_NtkObjNumMax(p), 0 );
-    Wlc_NtkForEachCo( p, pObj, i )
+    Wlc_NtkForEachObj( p, pObj, i )
         Wlc_NtkCreateLevels_rec( p, pObj );
-    return Vec_IntFindMax( &p->vLevels );
+    Wlc_NtkForEachObj( p, pObj, i )
+        if ( !Wlc_ObjIsCi(pObj) && Wlc_ObjFaninNum(pObj) )
+            Vec_IntAddToEntry( &p->vLevels, i, 1 );
+    LeveMax = Vec_IntFindMax( &p->vLevels );
+    Wlc_NtkForEachFf2( p, pObj, i )
+        Vec_IntWriteEntry( &p->vLevels, Wlc_ObjId(p, pObj), LeveMax+1 );
+    Wlc_NtkPrintObjects( p ); 
+    return LeveMax+1;
 }
 
 /**Function*************************************************************
@@ -662,6 +669,8 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fTwoSides, int fVerbose )
 void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
 {
     printf( "%8d  :  ", Wlc_ObjId(p, pObj) );
+    if ( Vec_IntSize(&p->vLevels) )
+        printf( "Lev = %2d  ", Vec_IntEntry(&p->vLevels, Wlc_ObjId(p,pObj)) );
     printf( "%6d%s = ", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s" : " " );
     if ( pObj->Type == WLC_OBJ_PI )
     {
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index d8187bd4..e2b61c6f 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1284,7 +1284,7 @@ startword:
         else if ( Wlc_PrsStrCmp( pStart, "ABC_DFFRSE" ) )
         {
             int NameId[10] = {0}, fFound, fFlopIn, fFlopClk, fFlopRst, fFlopSet, fFlopEna, fFlopAsync, fFlopSre, fFlopInit, fFlopOut;
-            pStart += strlen("ABC_DFF");
+            pStart += strlen("ABC_DFFRSE");
             while ( 1 )
             {
                 pStart = Wlc_PrsFindSymbol( pStart, '.' );
@@ -1348,7 +1348,7 @@ startword:
         else if ( Wlc_PrsStrCmp( pStart, "ABC_DFF" ) )
         {
             int NameId = -1, NameIdIn = -1, NameIdOut = -1, fFound, nBits = 1, fFlopIn, fFlopOut;
-            pStart += strlen("ABC_DFFRSE");
+            pStart += strlen("ABC_DFF");
             while ( 1 )
             {
                 pStart = Wlc_PrsFindSymbol( pStart, '.' );
diff --git a/src/base/wlc/wlcShow.c b/src/base/wlc/wlcShow.c
index b78437e8..50da3e5b 100644
--- a/src/base/wlc/wlcShow.c
+++ b/src/base/wlc/wlcShow.c
@@ -237,13 +237,31 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
     // the labeling node of this level
     fprintf( pFile, "  Level%d;\n",  0 );
     // generate the CI nodes
-    Wlc_NtkForEachCi( p, pNode, i )
+    Wlc_NtkForEachObj( p, pNode, i )
     {
+        if ( !Wlc_ObjIsCi(pNode) && Wlc_ObjFaninNum(pNode) > 0 )
+            continue;
         if ( vBold && !pNode->Mark )
             continue;
-        fprintf( pFile, "  Node%d [label = \"%d:%s %d\"", Wlc_ObjId(p, pNode), Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) ); 
-        fprintf( pFile, ", shape = %s", i < Wlc_NtkPiNum(p) ? "triangle" : "box" );
-        fprintf( pFile, ", color = coral, fillcolor = coral" );
+        if ( pNode->Type == WLC_OBJ_CONST )
+        {
+            //char * pName = Wlc_ObjName(p, i);
+            fprintf( pFile, "  Node%d [label = \"%d:%d\'h", i, i, Wlc_ObjRange(pNode) ); 
+            if ( Wlc_ObjRange(pNode) > 64 )
+            {
+                Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pNode), 16 );
+                fprintf( pFile, "..." );
+            }
+            else
+                Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pNode), (Wlc_ObjRange(pNode) + 3) / 4 );
+            fprintf( pFile, "\"" ); 
+        }
+        else
+        {
+            fprintf( pFile, "  Node%d [label = \"%d:%s %d\"", Wlc_ObjId(p, pNode), Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) ); 
+            fprintf( pFile, ", shape = %s", (Vec_IntSize(&p->vFfs2) > 0 || i < Wlc_NtkPiNum(p)) ? "triangle" : "box" );
+            fprintf( pFile, ", color = coral, fillcolor = coral" );
+        }
         fprintf( pFile, "];\n" );
     }
     fprintf( pFile, "}" );
diff --git a/src/base/wln/wln.h b/src/base/wln/wln.h
index c862b262..c4fbf997 100644
--- a/src/base/wln/wln.h
+++ b/src/base/wln/wln.h
@@ -244,7 +244,8 @@ extern int            Wln_ObjClone( Wln_Ntk_t * pNew, Wln_Ntk_t * p, int iObj );
 extern int            Wln_ObjCreateCo( Wln_Ntk_t * p, int iFanin );
 extern void           Wln_ObjPrint( Wln_Ntk_t * p, int iObj );
 /*=== wlcRetime.c ========================================================*/
-extern Vec_Int_t *    Wln_NtkRetime( Wln_Ntk_t * p );
+extern Vec_Int_t *    Wln_NtkRetime( Wln_Ntk_t * p, int fVerbose );
+extern void           Wln_NtkRetimeCreateDelayInfo( Wln_Ntk_t * pNtk );
 /*=== wlcWriteVer.c ========================================================*/
 extern void           Wln_WriteVer( Wln_Ntk_t * p, char * pFileName );
 
diff --git a/src/base/wln/wlnNdr.c b/src/base/wln/wlnNdr.c
index 012622e9..411dfaeb 100644
--- a/src/base/wln/wlnNdr.c
+++ b/src/base/wln/wlnNdr.c
@@ -293,7 +293,8 @@ Wln_Ntk_t * Wln_NtkFromNdr( void * pData )
 Wln_Ntk_t * Wln_ReadNdr( char * pFileName )
 {
     void * pData = Ndr_Read( pFileName );
-    Wln_Ntk_t * pNtk = Wln_NtkFromNdr( pData );
+    Wln_Ntk_t * pNtk = pData ? Wln_NtkFromNdr( pData ) : NULL;
+    if ( pNtk ) return NULL;
     //char * ppNames[10] = { NULL, "a", "b", "c", "d", "e", "f", "g", "h", "i" };
     //Ndr_WriteVerilog( NULL, pData, ppNames );
     Ndr_Delete( pData );
@@ -308,40 +309,21 @@ void Wln_ReadNdrTest()
     Wln_NtkStaticFanoutTest( pNtk );
     Wln_NtkFree( pNtk );
 }
-void Wln_NtkRetimeTest( char * pFileName )
+void Wln_NtkRetimeTest( char * pFileName, int fVerbose  )
 {
+    Vec_Int_t * vMoves;
     void * pData = Ndr_Read( pFileName );
-    Wln_Ntk_t * pNtk = Wln_NtkFromNdr( pData );
-    Ndr_Delete( pData );
-    if ( Wln_NtkHasInstId(pNtk) )
-        Vec_IntErase( &pNtk->vInstIds );
-    if ( !Wln_NtkHasInstId(pNtk) )
-    {
-        int iObj;
-        printf( "The design has no delay information.\n" );
-        Wln_NtkCleanInstId(pNtk);
-        Wln_NtkForEachObj( pNtk, iObj )
-            if ( Wln_ObjIsFf(pNtk, iObj) )
-                Wln_ObjSetInstId( pNtk, iObj, 1 );
-            else if ( !Wln_ObjIsCio(pNtk, iObj) && Wln_ObjFaninNum(pNtk, iObj) > 0 )
-                Wln_ObjSetInstId( pNtk, iObj, 10 );
-        printf( "Assuming user-specified delays for internal nodes.\n" );
-    }
-/*
-    else
-    {
-        int iObj;
-        Wln_NtkForEachObj( pNtk, iObj )
-            if ( !Wln_ObjIsCio(pNtk, iObj) && Wln_ObjFaninNum(pNtk, iObj) > 0 && !Wln_ObjIsFf(pNtk, iObj) )
-                printf( "Obj %5d : NameId = %6d  InstId = %6d\n", iObj, Wln_ObjNameId(pNtk, iObj), Wln_ObjInstId(pNtk, iObj) );
-    }
-*/
-    //else
+    Wln_Ntk_t * pNtk = pData ? Wln_NtkFromNdr( pData ) : NULL;
+    if ( pNtk == NULL ) 
     {
-        Vec_Int_t * vMoves = Wln_NtkRetime( pNtk );
-        //Vec_IntPrint( vMoves );
-        Vec_IntFree( vMoves );
+        printf( "Retiming network is not available.\n" );
+        return;
     }
+    Ndr_Delete( pData );
+    Wln_NtkRetimeCreateDelayInfo( pNtk );
+    vMoves = Wln_NtkRetime( pNtk, fVerbose );
+    //Vec_IntPrint( vMoves );
+    Vec_IntFree( vMoves );
     Wln_NtkFree( pNtk );
 }
 
diff --git a/src/base/wln/wlnRetime.c b/src/base/wln/wlnRetime.c
index 4ef8b53c..d1b8884c 100644
--- a/src/base/wln/wlnRetime.c
+++ b/src/base/wln/wlnRetime.c
@@ -76,7 +76,8 @@ static inline int *   Wln_RetFanouts( Wln_Ret_t * p, int i ) { return Vec_IntEnt
 void Wln_RetPrintObj( Wln_Ret_t * p, int iObj )
 {
     int k, iFanin, Type = Wln_ObjType(p->pNtk, iObj), * pLink;
-    printf( "Obj %6d : Type = %6s  Fanins = %d : ", iObj, Abc_OperName(Type), Wln_ObjFaninNum(p->pNtk, iObj) );
+    printf( "Obj %6d : Type = %6s  NameId = %5d  InstId = %5d  Fanins = %d : ", 
+        iObj, Abc_OperName(Type), Wln_ObjNameId(p->pNtk, iObj), Wln_ObjInstId(p->pNtk, iObj), Wln_ObjFaninNum(p->pNtk, iObj) );
     Wln_RetForEachFanin( p, iObj, iFanin, pLink, k )
     {
         printf( "%5d ", iFanin );
@@ -159,7 +160,8 @@ Wln_Ret_t * Wln_RetAlloc( Wln_Ntk_t * pNtk )
     Vec_IntFree( vRefsCopy );
     // other data
     p->nClasses = Wln_RetComputeFfClasses( pNtk, &p->vFfClasses );
-    ABC_SWAP( Vec_Int_t, p->vNodeDelays, pNtk->vInstIds );
+    //ABC_SWAP( Vec_Int_t, p->vNodeDelays, pNtk->vInstIds );
+    Vec_IntAppend( &p->vNodeDelays, &pNtk->vInstIds );
     Vec_IntGrow( &p->vSources, 1000 );
     Vec_IntGrow( &p->vSinks, 1000 );
     Vec_IntGrow( &p->vFront, 1000 );
@@ -474,7 +476,7 @@ void Wln_RetAddToMoves( Wln_Ret_t * p, Vec_Int_t * vSet, int Delay, int fForward
     {
         int NameId = Vec_IntEntry( &p->pNtk->vNameIds, iObj );
         Vec_IntPush( &p->vMoves, fForward ? -NameId : NameId );
-        printf( " %d", fForward ? -iObj : iObj );
+        printf( " %d (NameID = %d)  ", fForward ? -iObj : iObj, fForward ? -NameId : NameId );
     }
     Vec_IntPush( &p->vMoves, 0 );
     printf( "\n" );
@@ -491,14 +493,32 @@ void Wln_RetAddToMoves( Wln_Ret_t * p, Vec_Int_t * vSet, int Delay, int fForward
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Wln_NtkRetime( Wln_Ntk_t * pNtk )
+void Wln_NtkRetimeCreateDelayInfo( Wln_Ntk_t * pNtk )
+{
+    if ( Wln_NtkHasInstId(pNtk) )
+        Vec_IntErase( &pNtk->vInstIds );
+    if ( !Wln_NtkHasInstId(pNtk) )
+    {
+        int iObj;
+        printf( "The design has no delay information.\n" );
+        Wln_NtkCleanInstId(pNtk);
+        Wln_NtkForEachObj( pNtk, iObj )
+            if ( Wln_ObjIsFf(pNtk, iObj) )
+                Wln_ObjSetInstId( pNtk, iObj, 1 );
+            else if ( !Wln_ObjIsCio(pNtk, iObj) && Wln_ObjFaninNum(pNtk, iObj) > 0 )
+                Wln_ObjSetInstId( pNtk, iObj, 10 );
+        printf( "Assuming user-specified delays for internal nodes.\n" );
+    }
+}
+Vec_Int_t * Wln_NtkRetime( Wln_Ntk_t * pNtk, int fVerbose )
 {
     Wln_Ret_t * p = Wln_RetAlloc( pNtk );
     Vec_Int_t * vSources = &p->vSources;
     Vec_Int_t * vSinks   = &p->vSinks;
     Vec_Int_t * vFront   = &p->vFront;
     Vec_Int_t * vMoves   = Vec_IntAlloc(0);
-    //Wln_RetPrint( p );
+    if ( fVerbose )
+        Wln_RetPrint( p );
     Wln_RetMarkChanges( p, NULL );
     p->DelayMax = Wln_RetPropDelay( p );
     Wln_RetFindSources( p );
@@ -554,6 +574,11 @@ Vec_Int_t * Wln_NtkRetime( Wln_Ntk_t * pNtk )
     }
     ABC_SWAP( Vec_Int_t, *vMoves, p->vMoves );
     Wln_RetFree( p );
+    if ( fVerbose )
+    {
+        printf( "\nThe resulting moves recorded in terms of name IDs of the NDR nodes:\n" );
+        Vec_IntPrint( vMoves );
+    }
     return vMoves;
 }
 
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index a0527ab9..dd478a1c 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -327,6 +327,13 @@ static inline int * Vec_IntReleaseArray( Vec_Int_t * p )
     p->pArray = NULL;
     return pArray;
 }
+static inline int * Vec_IntReleaseNewArray( Vec_Int_t * p )
+{
+    int * pArray = ABC_ALLOC( int, p->nSize+1 );
+    pArray[0] = p->nSize+1;
+    memcpy( pArray+1, p->pArray, sizeof(int)*p->nSize );
+    return pArray;
+}
 
 /**Function*************************************************************