Experiments with word-level retiming.

12 files changed, 2200 insertions, 5 deletions

diff --git a/Makefile b/Makefile
index 5aa884e1..e0e8b8f0 100644
--- a/Makefile
+++ b/Makefile
@@ -16,7 +16,7 @@ OS := $(shell uname -s)
 MODULES := \
 	$(wildcard src/ext*) \
 	src/base/abc src/base/abci src/base/cmd src/base/io src/base/main src/base/exor \
-	src/base/ver src/base/wlc src/base/acb src/base/bac src/base/cba src/base/pla src/base/test \
+	src/base/ver src/base/wlc src/base/wln src/base/acb src/base/bac src/base/cba src/base/pla src/base/test \
 	src/map/mapper src/map/mio src/map/super src/map/if \
 	src/map/amap src/map/cov src/map/scl src/map/mpm \
 	src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/nm \
diff --git a/abclib.dsp b/abclib.dsp
index b0769c80..fe23c746 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1106,6 +1106,38 @@ SOURCE=.\src\base\acb\acbSets.h
 SOURCE=.\src\base\acb\acbUtil.c
 # End Source File
 # End Group
+# Begin Group "wln"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\wln\wln.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\wln\wln.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\wln\wlnNdr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\wln\wlnNtk.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\wln\wlnObj.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\wln\wlnRetime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\wln\wlnWriteVer.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "bdd"
 
diff --git a/src/aig/miniaig/abcOper.h b/src/aig/miniaig/abcOper.h
index 5719d883..6ee043af 100644
--- a/src/aig/miniaig/abcOper.h
+++ b/src/aig/miniaig/abcOper.h
@@ -60,7 +60,7 @@ typedef enum {
     ABC_OPER_BIT_NXOR,     // 18
     ABC_OPER_BIT_SHARP,    // 19
     ABC_OPER_BIT_SHARPL,   // 20
-    ABC_OPER_BIT_MUX,      // 21
+    ABC_OPER_BIT_MUX,      // 21  fanins are: {Ctrl, Data1, Data0}
     ABC_OPER_BIT_MAJ,      // 22
 
     ABC_OPER_ABC,          // 23
@@ -86,7 +86,7 @@ typedef enum {
     ABC_OPER_LOGIC_XOR,    // 41
     ABC_OPER_LOGIC_XNOR,   // 42
 
-    ABC_OPER_SEL_NMUX,     // 43
+    ABC_OPER_SEL_NMUX,     // 43  fanins are: {Ctrl, Data0, Data1, Data2, ...}
     ABC_OPER_SEL_SEL,      // 44
     ABC_OPER_SEL_PSEL,     // 45
     ABC_OPER_SEL_ENC,      // 46
@@ -217,11 +217,14 @@ static inline char * Abc_OperName( int Type )
     if ( Type == ABC_OPER_SHIFT_ROTL   )   return "rotL";   
     if ( Type == ABC_OPER_SHIFT_ROTR   )   return "rotR";   
 
+    if ( Type == ABC_OPER_DFFRSE       )   return "DFFRSE";    
+
     if ( Type == ABC_OPER_SLICE        )   return "[:]";    
     if ( Type == ABC_OPER_CONCAT       )   return "{}";     
     if ( Type == ABC_OPER_ZEROPAD      )   return "zPad";   
     if ( Type == ABC_OPER_SIGNEXT      )   return "sExt";   
 
+    if ( Type == ABC_OPER_CONST        )   return "const";  
     if ( Type == ABC_OPER_TABLE        )   return "table";  
     if ( Type == ABC_OPER_LAST         )   return NULL;     
     assert( 0 );
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 9785d273..5b99cb00 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -40,6 +40,7 @@ static int  Abc_CommandMemAbs     ( Abc_Frame_t * pAbc, int argc, char ** argv )
 static int  Abc_CommandBlast      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandBlastMem   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandGraft      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandRetime     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandProfile    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandShow       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -85,6 +86,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Word level", "%blast",       Abc_CommandBlast,      0 );
     Cmd_CommandAdd( pAbc, "Word level", "%blastmem",    Abc_CommandBlastMem,   0 );
     Cmd_CommandAdd( pAbc, "Word level", "%graft",       Abc_CommandGraft,      0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%retime",      Abc_CommandRetime,     0 );
     Cmd_CommandAdd( pAbc, "Word level", "%profile",     Abc_CommandProfile,    0 );
     Cmd_CommandAdd( pAbc, "Word level", "%short_names", Abc_CommandShortNames, 0 );
     Cmd_CommandAdd( pAbc, "Word level", "%show",        Abc_CommandShow,       0 );
@@ -1168,7 +1170,7 @@ int Abc_CommandBlastMem( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pNtk == NULL )
     {
-        Abc_Print( 1, "Abc_CommandGraft(): There is no current design.\n" );
+        Abc_Print( 1, "Abc_CommandBlastMem(): There is no current design.\n" );
         return 0;
     }
     pNtk = Wlc_NtkMemBlast( pNtk );
@@ -1239,6 +1241,63 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
+int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Wln_NtkRetimeTest( char * pFileName );
+    FILE * pFile;
+    char * pFileName = NULL;
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+    {
+        printf( "Abc_CommandRetime(): Input file name should be given on the command line.\n" );
+        return 0;
+    }
+    // get the file name
+    pFileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( pFileName, "r" )) == NULL )
+    {
+        Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName );
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".ndr", NULL, NULL, NULL, NULL )) )
+            Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
+        Abc_Print( 1, "\n" );
+        return 0;
+    }
+    fclose( pFile );
+    Wln_NtkRetimeTest( pFileName );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%retime [-vh]\n" );
+    Abc_Print( -2, "\t         performs retiming for the NDR design\n" );
+    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;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
 int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
@@ -1754,7 +1813,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc );
     //pNtk = Wlc_NtkDupSingleNodes( pNtk );
     //Wlc_AbcUpdateNtk( pAbc, pNtk );
-    Ndr_ModuleTestDec();
+    //Wln_ReadNdrTest();
     //pNtk = Wlc_NtkMemAbstractTest( pNtk );
     //Wlc_AbcUpdateNtk( pAbc, pNtk );
     return 0;
diff --git a/src/base/wln/module.make b/src/base/wln/module.make
new file mode 100644
index 00000000..6689baf0
--- /dev/null
+++ b/src/base/wln/module.make
@@ -0,0 +1,6 @@
+SRC +=    src/base/wln/wln.c \
+    src/base/wln/wlnNdr.c \
+    src/base/wln/wlnNtk.c \
+    src/base/wln/wlnObj.c \
+    src/base/wln/wlnRetime.c \
+    src/base/wln/wlnWriteVer.c 
diff --git a/src/base/wln/wln.c b/src/base/wln/wln.c
new file mode 100644
index 00000000..2fbe26e0
--- /dev/null
+++ b/src/base/wln/wln.c
@@ -0,0 +1,51 @@
+/**CFile****************************************************************
+
+  FileName    [wln.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Word-level network.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 23, 2018.]
+
+  Revision    [$Id: wln.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wln.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wln/wln.h b/src/base/wln/wln.h
new file mode 100644
index 00000000..c862b262
--- /dev/null
+++ b/src/base/wln/wln.h
@@ -0,0 +1,259 @@
+/**CFile****************************************************************
+
+  FileName    [wlc.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 22, 2014.]
+
+  Revision    [$Id: wlc.h,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__base__wln__wln_h
+#define ABC__base__wln__wln_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig/gia/gia.h"
+#include "misc/vec/vecHash.h"
+#include "misc/extra/extra.h"
+#include "misc/util/utilNam.h"
+#include "misc/util/utilTruth.h"
+#include "aig/miniaig/abcOper.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START 
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Wln_Vec_t_  Wln_Vec_t;
+struct Wln_Vec_t_ 
+{
+    int                    nCap;
+    int                    nSize;
+    union { int            Array[2];  
+            int *          pArray[1]; };
+};
+
+typedef struct Wln_Ntk_t_  Wln_Ntk_t;
+struct Wln_Ntk_t_ 
+{
+    char *                 pName;                // model name
+    char *                 pSpec;                // input file name
+    int                    fSmtLib;              // derived from SMT-LIB
+    Vec_Int_t              vCis;                 // combinational inputs
+    Vec_Int_t              vCos;                 // combinational outputs
+    Vec_Int_t              vFfs;                 // flops
+    Vec_Int_t              vTypes;               // object types   
+    Wln_Vec_t *            vFanins;              // object fanins (exceptions: const, select)
+    Vec_Int_t              vRanges;              // object ranges
+    Hash_IntMan_t *        pRanges;              // object ranges
+    Vec_Int_t              vNameIds;             // object name IDs
+    Vec_Int_t              vInstIds;             // object name IDs
+    Abc_Nam_t *            pManName;             // object names
+    Vec_Str_t              vSigns;               // object signedness
+    int                    nTravIds;             // counter of traversal IDs
+    Vec_Int_t              vTravIds;             // trav IDs of the objects
+    Vec_Int_t              vCopies;              // object first bits
+    Vec_Int_t              vBits;                // object mapping into AIG nodes
+    Vec_Int_t              vLevels;              // object levels
+    Vec_Int_t              vRefs;                // object reference counters
+    Vec_Int_t              vFanout;              // static fanout
+    Vec_Int_t              vFaninAttrs;          // static fanin attributes
+    Vec_Int_t              vFaninLists;          // static fanin attributes
+    Vec_Ptr_t *            vTables;              // tables
+    int                    nObjs[ABC_OPER_LAST]; // counter of objects of each type
+    int                    nAnds[ABC_OPER_LAST]; // counter of AND gates after blasting
+};
+
+static inline int          Wln_NtkObjNum( Wln_Ntk_t * p )                        { return Vec_IntSize(&p->vTypes);                                            }
+static inline int          Wln_NtkCiNum( Wln_Ntk_t * p )                         { return Vec_IntSize(&p->vCis);                                              }
+static inline int          Wln_NtkCoNum( Wln_Ntk_t * p )                         { return Vec_IntSize(&p->vCos);                                              }
+static inline int          Wln_NtkFfNum( Wln_Ntk_t * p )                         { return Vec_IntSize(&p->vFfs);                                              }
+static inline int          Wln_NtkPiNum( Wln_Ntk_t * p )                         { return Wln_NtkCiNum(p) - Wln_NtkFfNum(p);                                  }
+static inline int          Wln_NtkPoNum( Wln_Ntk_t * p )                         { return Wln_NtkCoNum(p) - Wln_NtkFfNum(p);                                  }
+
+static inline int          Wln_NtkCi( Wln_Ntk_t * p, int i )                     { return Vec_IntEntry(&p->vCis, i);                                          }
+static inline int          Wln_NtkCo( Wln_Ntk_t * p, int i )                     { return Vec_IntEntry(&p->vCos, i);                                          }
+static inline int          Wln_NtkFf( Wln_Ntk_t * p, int i )                     { return Vec_IntEntry(&p->vFfs, i);                                          }
+
+static inline int          Wln_ObjType( Wln_Ntk_t * p, int i )                   { return Vec_IntEntry(&p->vTypes, i);                                        }
+static inline int          Wln_ObjIsNone( Wln_Ntk_t * p, int i )                 { return Wln_ObjType(p, i) == ABC_OPER_NONE;                                 }
+static inline int          Wln_ObjIsCi( Wln_Ntk_t * p, int i )                   { return Wln_ObjType(p, i) == ABC_OPER_CI;                                   }
+static inline int          Wln_ObjIsCo( Wln_Ntk_t * p, int i )                   { return Wln_ObjType(p, i) == ABC_OPER_CO;                                   }
+static inline int          Wln_ObjIsCio( Wln_Ntk_t * p, int i )                  { return Wln_ObjType(p, i) == ABC_OPER_CI || Wln_ObjType(p, i)==ABC_OPER_CO; }
+static inline int          Wln_ObjIsFon( Wln_Ntk_t * p, int i )                  { return Wln_ObjType(p, i) == ABC_OPER_FON;                                  }
+static inline int          Wln_ObjIsFf( Wln_Ntk_t * p, int i )                   { return Wln_ObjType(p, i) == ABC_OPER_DFFRSE;                               }
+static inline int          Wln_ObjIsConst( Wln_Ntk_t * p, int i )                { return Wln_ObjType(p, i) == ABC_OPER_CONST;                                }
+static inline int          Wln_ObjIsSlice( Wln_Ntk_t * p, int i )                { return Wln_ObjType(p, i) == ABC_OPER_SLICE;                                }
+static inline int          Wln_ObjIsRotate( Wln_Ntk_t * p, int i )               { return Wln_ObjType(p, i) == ABC_OPER_SHIFT_ROTL || Wln_ObjType(p, i) == ABC_OPER_SHIFT_ROTR; }
+static inline int          Wln_ObjIsTable( Wln_Ntk_t * p, int i )                { return Wln_ObjType(p, i) == ABC_OPER_TABLE;                                }
+
+static inline int          Wln_ObjFaninNum( Wln_Ntk_t * p, int i )               { return p->vFanins[i].nSize;                                                }
+static inline int *        Wln_ObjFanins( Wln_Ntk_t * p, int i )                 { return Wln_ObjFaninNum(p, i) > 2 ? p->vFanins[i].pArray[0]    : p->vFanins[i].Array;    }
+static inline int          Wln_ObjFanin( Wln_Ntk_t * p, int i, int f )           { return Wln_ObjFaninNum(p, i) > 2 ? p->vFanins[i].pArray[0][f] : p->vFanins[i].Array[f]; }
+static inline void         Wln_ObjSetFanin( Wln_Ntk_t * p, int i, int f, int v ) { Wln_ObjFanins( p, i )[f] = v;                                              }
+static inline int          Wln_ObjFanin0( Wln_Ntk_t * p, int i )                 { return Wln_ObjFanin( p, i, 0 );                                            }
+static inline int          Wln_ObjFanin1( Wln_Ntk_t * p, int i )                 { return Wln_ObjFanin( p, i, 1 );                                            }
+static inline int          Wln_ObjFanin2( Wln_Ntk_t * p, int i )                 { return Wln_ObjFanin( p, i, 2 );                                            }
+
+static inline int          Wln_ObjRangeId( Wln_Ntk_t * p, int i )                { return Vec_IntEntry( &p->vRanges, i );                                     }
+static inline int          Wln_ObjRangeEnd( Wln_Ntk_t * p, int i )               { return Hash_IntObjData0( p->pRanges, Wln_ObjRangeId(p, i) );               }
+static inline int          Wln_ObjRangeBeg( Wln_Ntk_t * p, int i )               { return Hash_IntObjData1( p->pRanges, Wln_ObjRangeId(p, i) );               }
+static inline int          Wln_ObjRangeIsReversed( Wln_Ntk_t * p, int i )        { return Wln_ObjRangeEnd(p, i) < Wln_ObjRangeBeg(p, i);                      }
+static inline int          Wln_ObjRange( Wln_Ntk_t * p, int i )                  { return 1 + Abc_AbsInt(Wln_ObjRangeEnd(p, i)-Wln_ObjRangeBeg(p, i));        }
+        
+static inline int          Wln_ObjIsSigned( Wln_Ntk_t * p, int i )               { return (int)Vec_StrEntry(&p->vSigns, i);                                   }
+static inline void         Wln_ObjSetSigned( Wln_Ntk_t * p, int i )              { Vec_StrSetEntry(&p->vSigns, i, (char)1);                                   }
+static inline int          Wln_ObjIsSignedFanin0( Wln_Ntk_t * p, int i )         { return Wln_ObjIsSigned( p, p->fSmtLib ? i : Wln_ObjFanin0(p, i) );         }
+static inline int          Wln_ObjIsSignedFanin1( Wln_Ntk_t * p, int i )         { return Wln_ObjIsSigned( p, p->fSmtLib ? i : Wln_ObjFanin1(p, i) );         }
+static inline int          Wln_ObjIsSignedFanin01( Wln_Ntk_t * p, int i )        { return Wln_ObjIsSignedFanin0( p, i ) && Wln_ObjIsSignedFanin1( p, i );     }
+static inline int          Wln_ObjSign( Wln_Ntk_t * p, int i )                   { return Abc_Var2Lit( Wln_ObjRange(p, i), Wln_ObjIsSigned(p, i) );           }
+
+static inline void         Wln_NtkCleanCopy( Wln_Ntk_t * p )                     { Vec_IntFill( &p->vCopies, Vec_IntCap(&p->vTypes), 0 );                     }
+static inline int          Wln_NtkHasCopy( Wln_Ntk_t * p )                       { return Vec_IntSize( &p->vCopies ) > 0;                                     }
+static inline void         Wln_ObjSetCopy( Wln_Ntk_t * p, int i, int c )         { Vec_IntWriteEntry( &p->vCopies, i, c );                                    }
+static inline int          Wln_ObjCopy( Wln_Ntk_t * p, int i )                   { return Vec_IntEntry( &p->vCopies, i );                                     }
+
+static inline void         Wln_NtkCleanLevel( Wln_Ntk_t * p )                    { Vec_IntFill( &p->vLevels, Vec_IntCap(&p->vTypes), 0 );                     }
+static inline int          Wln_NtkHasLevel( Wln_Ntk_t * p )                      { return Vec_IntSize( &p->vLevels ) > 0;                                     }
+static inline void         Wln_ObjSetLevel( Wln_Ntk_t * p, int i, int l )        { Vec_IntWriteEntry( &p->vLevels, i, l );                                    }
+static inline int          Wln_ObjLevel( Wln_Ntk_t * p, int i )                  { return Vec_IntEntry( &p->vLevels, i );                                     }
+
+static inline void         Wln_NtkCleanNameId( Wln_Ntk_t * p )                   { Vec_IntFill( &p->vNameIds, Vec_IntCap(&p->vTypes), 0 );                    }
+static inline int          Wln_NtkHasNameId( Wln_Ntk_t * p )                     { return Vec_IntSize( &p->vNameIds ) > 0;                                    }
+static inline void         Wln_ObjSetNameId( Wln_Ntk_t * p, int i, int n )       { Vec_IntWriteEntry( &p->vNameIds, i, n );                                   }
+static inline int          Wln_ObjNameId( Wln_Ntk_t * p, int i )                 { return Vec_IntEntry( &p->vNameIds, i );                                    }
+
+static inline void         Wln_NtkCleanInstId( Wln_Ntk_t * p )                   { Vec_IntFill( &p->vInstIds, Vec_IntCap(&p->vTypes), 0 );                    }
+static inline int          Wln_NtkHasInstId( Wln_Ntk_t * p )                     { return Vec_IntSize( &p->vInstIds ) > 0;                                    }
+static inline void         Wln_ObjSetInstId( Wln_Ntk_t * p, int i, int n )       { Vec_IntWriteEntry( &p->vInstIds, i, n );                                   }
+static inline int          Wln_ObjInstId( Wln_Ntk_t * p, int i )                 { return Vec_IntEntry( &p->vInstIds, i );                                    }
+
+static inline void         Wln_NtkCleanRefs( Wln_Ntk_t * p )                     { Vec_IntFill( &p->vRefs, Vec_IntCap(&p->vTypes), 0 );                       }
+static inline int          Wln_NtkHasRefs( Wln_Ntk_t * p )                       { return Vec_IntSize( &p->vRefs ) > 0;                                       }
+static inline void         Wln_ObjSetRefs( Wln_Ntk_t * p, int i, int n )         { Vec_IntWriteEntry( &p->vRefs, i, n );                                      }
+static inline int          Wln_ObjRefs( Wln_Ntk_t * p, int i )                   { return Vec_IntEntry( &p->vRefs, i );                                       }
+static inline int          Wln_ObjRefsInc( Wln_Ntk_t * p, int i )                { return (*Vec_IntEntryP( &p->vRefs, i ))++;                                 }
+static inline int          Wln_ObjRefsDec( Wln_Ntk_t * p, int i )                { return --(*Vec_IntEntryP( &p->vRefs, i ));                                 }
+static inline void         Wln_ObjRefsFaninInc( Wln_Ntk_t * p, int i, int k )    { Wln_ObjRefsInc( p, Wln_ObjFanin(p, i, k) );                                }
+static inline void         Wln_ObjRefsFaninDec( Wln_Ntk_t * p, int i, int k )    { Wln_ObjRefsDec( p, Wln_ObjFanin(p, i, k) );                                }
+
+static inline int          Wln_ObjFanoutNum( Wln_Ntk_t * p, int i )              { return Vec_IntEntry( &p->vRefs, i );                                       }
+static inline int *        Wln_ObjFanouts( Wln_Ntk_t * p, int i )                { return Vec_IntEntryP( &p->vFanout, Vec_IntEntry(&p->vFanout, i) );         }
+static inline int          Wln_ObjFanout( Wln_Ntk_t * p, int i, int f )          { return Wln_ObjFanouts( p, i )[f];                                          }
+static inline void         Wln_ObjSetFanout( Wln_Ntk_t * p, int i, int f, int v ){ Wln_ObjFanouts( p, i )[f] = v;                                             }
+
+static inline void         Wln_NtkIncrementTravId( Wln_Ntk_t * p )               { if (!p->nTravIds++) Vec_IntFill(&p->vTravIds, Vec_IntCap(&p->vTypes), 0);  }       
+static inline void         Wln_ObjSetTravIdCurrent( Wln_Ntk_t * p, int i )       { Vec_IntWriteEntry( &p->vTravIds, i, p->nTravIds );                         }
+static inline int          Wln_ObjIsTravIdCurrent( Wln_Ntk_t * p, int i )        { return (Vec_IntEntry(&p->vTravIds, i) == p->nTravIds);                     }   
+static inline int          Wln_ObjIsTravIdPrevious( Wln_Ntk_t * p, int i )       { return (Vec_IntEntry(&p->vTravIds, i) == p->nTravIds-1);                   }   
+static inline int          Wln_ObjCheckTravId( Wln_Ntk_t * p, int i )            { if ( Wln_ObjIsTravIdCurrent(p, i) ) return 1; Wln_ObjSetTravIdCurrent(p, i); return 0; }   
+
+static inline int          Wln_ObjCioId( Wln_Ntk_t * p, int i )                  { assert( Wln_ObjIsCio(p, i) ); return Wln_ObjFanin1(p, i);                  }
+static inline int          Wln_ObjIsPi( Wln_Ntk_t * p, int i )                   { return Wln_ObjIsCi(p, i) && Wln_ObjCioId(p, i) <  Wln_NtkPiNum(p);         } 
+static inline int          Wln_ObjIsPo( Wln_Ntk_t * p, int i )                   { return Wln_ObjIsCo(p, i) && Wln_ObjCioId(p, i) <  Wln_NtkPoNum(p);         } 
+static inline int          Wln_ObjIsRo( Wln_Ntk_t * p, int i )                   { return Wln_ObjIsCi(p, i) && Wln_ObjCioId(p, i) >= Wln_NtkPiNum(p);         } 
+static inline int          Wln_ObjIsRi( Wln_Ntk_t * p, int i )                   { return Wln_ObjIsCo(p, i) && Wln_ObjCioId(p, i) >= Wln_NtkPoNum(p);         } 
+static inline int          Wln_ObjRoToRi( Wln_Ntk_t * p, int i )                 { assert( Wln_ObjIsRo(p, i) ); return Wln_NtkCo(p, Wln_NtkCoNum(p) - Wln_NtkCiNum(p) + Wln_ObjCioId(p, i)); } 
+static inline int          Wln_ObjRiToRo( Wln_Ntk_t * p, int i )                 { assert( Wln_ObjIsRi(p, i) ); return Wln_NtkCi(p, Wln_NtkCiNum(p) - Wln_NtkCoNum(p) + Wln_ObjCioId(p, i)); } 
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                             ITERATORS                            ///
+////////////////////////////////////////////////////////////////////////
+
+#define Wln_NtkForEachObj( p, i )                                                   \
+    for ( i = 1; i < Wln_NtkObjNum(p); i++ )
+#define Wln_NtkForEachObjReverse( p, i )                                            \
+    for ( i = Wln_NtkObjNum(p) - 1; i >  0; i-- )
+#define Wln_NtkForEachObjInternal( p, i )                                           \
+    for ( i = 1; i < Wln_NtkObjNum(p); i++ ) if ( Wln_ObjIsCio(p, i) ) {} else 
+
+#define Wln_NtkForEachPi( p, iPi, i )                                               \
+    for ( i = 0; (i < Wln_NtkPiNum(p)) && (((iPi) = Wln_NtkCi(p, i)), 1); i++ )
+#define Wln_NtkForEachPo( p, iPo, i )                                               \
+    for ( i = 0; (i < Wln_NtkPoNum(p)) && (((iPo) = Wln_NtkCo(p, i)), 1); i++ )
+#define Wln_NtkForEachCi( p, iCi, i )                                               \
+    for ( i = 0; (i < Wln_NtkCiNum(p)) && (((iCi) = Wln_NtkCi(p, i)), 1); i++ )
+#define Wln_NtkForEachCo( p, iCo, i )                                               \
+    for ( i = 0; (i < Wln_NtkCoNum(p)) && (((iCo) = Wln_NtkCo(p, i)), 1); i++ )
+#define Wln_NtkForEachFf( p, iFf, i )                                               \
+    for ( i = 0; (i < Wln_NtkFfNum(p)) && (((iFf) = Wln_NtkFf(p, i)), 1); i++ )
+
+#define Wln_ObjForEachFanin( p, iObj, iFanin, i )                                   \
+    for ( i = 0; (i < Wln_ObjFaninNum(p, iObj)) && (((iFanin) = Wln_ObjFanin(p, iObj, i)), 1); i++ ) if ( !iFanin ) {} else
+#define Wln_ObjForEachFaninReverse( pObj, iFanin, i )                               \
+    for ( i = Wln_ObjFaninNum(p, iObj) - 1; (i >= 0) && (((iFanin) = Wln_ObjFanin(p, iObj, i)), 1); i-- ) if ( !iFanin ) {} else
+
+#define Wln_ObjForEachFanoutStatic( p, iObj, iFanout, i )                           \
+    for ( i = 0; (i < Wln_ObjRefs(p, iObj)) && (((iFanout) = Wln_ObjFanout(p, iObj, i)), 1); i++ )
+
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== wlcNdr.c ========================================================*/
+extern Wln_Ntk_t *    Wln_ReadNdr( char * pFileName );
+extern void           Wln_WriteNdr( Wln_Ntk_t * pNtk, char * pFileName );
+extern Wln_Ntk_t *    Wln_NtkFromNdr( void * pData );
+extern void *         Wln_NtkToNdr( Wln_Ntk_t * pNtk );
+/*=== wlcNtk.c ========================================================*/
+extern Wln_Ntk_t *    Wln_NtkAlloc( char * pName, int nObjsMax );
+extern void           Wln_NtkFree( Wln_Ntk_t * p );
+extern int            Wln_NtkMemUsage( Wln_Ntk_t * p );
+extern void           Wln_NtkPrint( Wln_Ntk_t * p );
+extern Wln_Ntk_t *    Wln_NtkDupDfs( Wln_Ntk_t * p );
+extern void           Wln_NtkCreateRefs( Wln_Ntk_t * p );
+extern void           Wln_NtkStartFaninMap( Wln_Ntk_t * p, Vec_Int_t * vFaninMap, int nMulti );
+extern void           Wln_NtkStartFanoutMap( Wln_Ntk_t * p, Vec_Int_t * vFanoutMap, Vec_Int_t * vFanoutNums, int nMulti );
+extern void           Wln_NtkStaticFanoutStart( Wln_Ntk_t * p );
+extern void           Wln_NtkStaticFanoutStop( Wln_Ntk_t * p );
+extern void           Wln_NtkStaticFanoutTest( Wln_Ntk_t * p );
+/*=== wlcObj.c ========================================================*/
+extern char *         Wln_ObjName( Wln_Ntk_t * p, int iObj );
+extern char *         Wln_ObjConstString( Wln_Ntk_t * p, int iObj );
+extern void           Wln_ObjUpdateType( Wln_Ntk_t * p, int iObj, int Type );
+extern void           Wln_ObjSetConst( Wln_Ntk_t * p, int iObj, int NameId );
+extern void           Wln_ObjSetSlice( Wln_Ntk_t * p, int iObj, int SliceId );
+extern void           Wln_ObjAddFanin( Wln_Ntk_t * p, int iObj, int i );
+extern int            Wln_ObjAddFanins( Wln_Ntk_t * p, int iObj, Vec_Int_t * vFanins );
+extern int            Wln_ObjAlloc( Wln_Ntk_t * p, int Type, int Signed, int End, int Beg );
+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 );
+/*=== wlcWriteVer.c ========================================================*/
+extern void           Wln_WriteVer( Wln_Ntk_t * p, char * pFileName );
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/wln/wlnNdr.c b/src/base/wln/wlnNdr.c
new file mode 100644
index 00000000..c87100a2
--- /dev/null
+++ b/src/base/wln/wlnNdr.c
@@ -0,0 +1,332 @@
+/**CFile****************************************************************
+
+  FileName    [wlnNdr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Word-level network.]
+
+  Synopsis    [Constructing WLN network from NDR data structure.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 23, 2018.]
+
+  Revision    [$Id: wlnNdr.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wln.h"
+#include "aig/miniaig/ndr.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Wln_NtkToNdr( Wln_Ntk_t * p )
+{
+    Vec_Int_t * vFanins;
+    int i, k, iObj, iFanin;
+    // create a new module
+    void * pDesign = Ndr_Create( 1 );
+    int ModId = Ndr_AddModule( pDesign, 1 );
+    // add primary inputs
+    Wln_NtkForEachPi( p, iObj, i ) 
+    {
+        Ndr_AddObject( pDesign, ModId, ABC_OPER_CI, 0,   
+            Wln_ObjRangeEnd(p, iObj), Wln_ObjRangeBeg(p, iObj), Wln_ObjIsSigned(p, iObj),   
+            0, NULL,  1, &iObj,  NULL  ); // no fanins
+    }
+    // add internal nodes 
+    vFanins = Vec_IntAlloc( 10 );
+    Wln_NtkForEachObjInternal( p, iObj ) 
+    {
+        Vec_IntClear( vFanins );
+        Wln_ObjForEachFanin( p, iObj, iFanin, k )
+            Vec_IntPush( vFanins, iFanin );
+        Ndr_AddObject( pDesign, ModId, Wln_ObjType(p, iObj), 0,   
+            Wln_ObjRangeEnd(p, iObj), Wln_ObjRangeBeg(p, iObj), Wln_ObjIsSigned(p, iObj),   
+            Vec_IntSize(vFanins), Vec_IntArray(vFanins), 1, &iObj,  
+            Wln_ObjIsConst(p, iObj) ? Wln_ObjConstString(p, iObj) : NULL ); 
+    }
+    Vec_IntFree( vFanins );
+    // add primary outputs
+    Wln_NtkForEachPo( p, iObj, i ) 
+    {
+        Ndr_AddObject( pDesign, ModId, ABC_OPER_CO, 0,                   
+            Wln_ObjRangeEnd(p, iObj), Wln_ObjRangeBeg(p, iObj), Wln_ObjIsSigned(p, iObj),   
+            1, &iObj,  0, NULL,  NULL ); 
+    }
+    return pDesign;
+}
+void Wln_WriteNdr( Wln_Ntk_t * p, char * pFileName )
+{
+    void * pDesign = Wln_NtkToNdr( p );
+    Ndr_Write( pFileName, pDesign );
+    Ndr_Delete( pDesign );
+    printf( "Dumped the current design into file \"%s\".\n", pFileName );
+}
+void Wln_NtkToNdrTest( Wln_Ntk_t * p )
+{
+    // transform
+    void * pDesign = Wln_NtkToNdr( p );
+
+    // collect names     
+    char ** ppNames = ABC_ALLOC( char *, Wln_NtkObjNum(p) + 1 ); int i;
+    Wln_NtkForEachObj( p, i ) 
+        ppNames[i] = Abc_UtilStrsav(Wln_ObjName(p, i));
+
+    // verify by writing Verilog
+    Ndr_WriteVerilog( NULL, pDesign, ppNames );
+    Ndr_Write( "test.ndr", pDesign );
+
+    // cleanup
+    Ndr_Delete( pDesign );
+    Wln_NtkForEachObj( p, i ) 
+        ABC_FREE( ppNames[i] );
+    ABC_FREE( ppNames );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ndr_ObjGetRange( Ndr_Data_t * p, int Obj, int * End, int * Beg )
+{
+    int * pArray, nArray = Ndr_ObjReadArray( p, Obj, NDR_RANGE, &pArray );
+    int Signed = 0; *End = *Beg = 0;
+    if ( nArray == 0 )
+        return 0;
+    if ( nArray == 3 )
+        Signed = 1;
+    if ( nArray == 1 )
+        *End = *Beg = pArray[0];
+    else
+        *End = pArray[0], *Beg = pArray[1];
+    return Signed;
+}
+void Ndr_NtkPrintObjects( Wln_Ntk_t * pNtk )
+{
+    int k, iObj, iFanin;
+    printf( "Node IDs and their fanins:\n" );
+    Wln_NtkForEachObj( pNtk, iObj )
+    {
+        printf( "%5d = ", iObj );
+        Wln_ObjForEachFanin( pNtk, iObj, iFanin, k )
+            printf( "%5d ", iFanin );
+        for (      ; k < 4; k++ )
+            printf( "      " );
+        printf( "    Name Id %d ", Wln_ObjNameId(pNtk, iObj) );
+        if ( Wln_ObjIsPi(pNtk, iObj) )
+            printf( "  pi  " );
+        if ( Wln_ObjIsPo(pNtk, iObj) )
+            printf( "  po  " );
+        printf( "\n" );
+    }
+}
+void Wln_NtkCheckIntegrity( void * pData )
+{
+    Ndr_Data_t * p = (Ndr_Data_t *)pData;  
+    Vec_Int_t * vMap = Vec_IntAlloc( 100 );
+    int Mod = 2, Obj;
+    Ndr_ModForEachObj( p, Mod, Obj )
+    {
+        int NameId  = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
+        if ( NameId == -1 )
+        {
+            int Type = Ndr_ObjReadBody( p, Obj, NDR_OPERTYPE );
+            if ( Type != ABC_OPER_CO )
+                printf( "Internal object %d of type %s has no output name.\n", Obj, Abc_OperName(Type) );
+            continue;
+        }
+        if ( Vec_IntGetEntry(vMap, NameId) > 0 )
+            printf( "Output name %d is used more than once (obj %d and obj %d).\n", NameId, Vec_IntGetEntry(vMap, NameId), Obj );
+        Vec_IntSetEntry( vMap, NameId, Obj );
+    }
+    Ndr_ModForEachObj( p, Mod, Obj )
+    {
+        int Type = Ndr_ObjReadBody( p, Obj, NDR_OPERTYPE );
+        int i, * pArray, nArray  = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
+        for ( i = 0; i < nArray; i++ )
+            if ( Vec_IntGetEntry(vMap, pArray[i]) == 0 && !(Type == ABC_OPER_DFFRSE && (i >= 5 || i <= 7)) )
+                printf( "Input name %d appearing as fanin %d of obj %d is not used as output name in any object.\n", pArray[i], i, Obj );
+    }
+    Vec_IntFree( vMap );
+}
+Wln_Ntk_t * Wln_NtkFromNdr( void * pData )
+{
+    Ndr_Data_t * p = (Ndr_Data_t *)pData;  
+    Vec_Int_t * vName2Obj, * vFanins = Vec_IntAlloc( 100 );
+    Vec_Ptr_t * vConstStrings = Vec_PtrAlloc( 100 );
+    int Mod = 2, i, k, iFanin, iObj, Obj, * pArray, nDigits, fFound, NameId, NameIdMax;
+    Wln_Ntk_t * pTemp, * pNtk = Wln_NtkAlloc( "top", Ndr_DataObjNum(p, Mod) );
+    Wln_NtkCheckIntegrity( pData );
+    //pNtk->pSpec = Abc_UtilStrsav( pFileName );
+    // construct network and save name IDs
+    Wln_NtkCleanNameId( pNtk );
+    Wln_NtkCleanInstId( pNtk );
+    Ndr_ModForEachPi( p, Mod, Obj )
+    {
+        int End, Beg, Signed = Ndr_ObjGetRange(p, Obj, &End, &Beg);
+        int iObj = Wln_ObjAlloc( pNtk, ABC_OPER_CI, Signed, End, Beg );
+        int NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
+        int InstId = Ndr_ObjReadBody( p, Obj, NDR_NAME );
+        Wln_ObjSetNameId( pNtk, iObj, NameId );
+        if ( InstId > 0 ) Wln_ObjSetInstId( pNtk, iObj, InstId );
+    }
+    Ndr_ModForEachNode( p, Mod, Obj )
+    {
+        int End, Beg, Signed = Ndr_ObjGetRange(p, Obj, &End, &Beg);
+        int Type    = Ndr_ObjReadBody( p, Obj, NDR_OPERTYPE );
+        int nArray  = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
+        Vec_Int_t F = {nArray, nArray, pArray}, * vTemp = &F;
+        int iObj    = Wln_ObjAlloc( pNtk, Type, Signed, End, Beg );
+        int NameId  = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
+        int InstId  = Ndr_ObjReadBody( p, Obj, NDR_NAME );
+        Vec_IntClear( vFanins );
+        Vec_IntAppend( vFanins, vTemp );
+        assert( Type != ABC_OPER_DFF );
+        if ( Wln_ObjIsSlice(pNtk, iObj) )
+            Wln_ObjSetSlice( pNtk, iObj, Hash_Int2ManInsert(pNtk->pRanges, End, Beg, 0) );
+        else if ( Wln_ObjIsConst(pNtk, iObj) )
+            Vec_PtrPush( vConstStrings, (char *)Ndr_ObjReadBodyP(p, Obj, NDR_FUNCTION) );
+//        else if ( Type == ABC_OPER_BIT_MUX && Vec_IntSize(vFanins) == 3 )
+//            ABC_SWAP( int, Wln_ObjFanins(pNtk, iObj)[1], Wln_ObjFanins(pNtk, iObj)[2] );
+        Wln_ObjAddFanins( pNtk, iObj, vFanins );
+        Wln_ObjSetNameId( pNtk, iObj, NameId );
+        if ( InstId > 0 ) Wln_ObjSetInstId( pNtk, iObj, InstId );
+        if ( Type == ABC_OPER_ARI_SMUL )
+        {
+            assert( Wln_ObjFaninNum(pNtk, iObj) == 2 );
+            Wln_ObjSetSigned( pNtk, Wln_ObjFanin0(pNtk, iObj) );
+            Wln_ObjSetSigned( pNtk, Wln_ObjFanin1(pNtk, iObj) );
+        }
+    }
+    // mark primary outputs
+    Ndr_ModForEachPo( p, Mod, Obj )
+    {
+        int End, Beg, Signed = Ndr_ObjGetRange(p, Obj, &End, &Beg);
+        int nArray  = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
+        int iObj    = Wln_ObjAlloc( pNtk, ABC_OPER_CO, Signed, End, Beg );
+        int NameId  = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
+        int InstId  = Ndr_ObjReadBody( p, Obj, NDR_NAME );
+        assert( nArray == 1 && NameId == -1 && InstId == -1 );
+        Wln_ObjAddFanin( pNtk, iObj, pArray[0] );
+    }
+    Vec_IntFree( vFanins );
+    // remove instance names if they are not given
+    //Vec_IntPrint( &pNtk->vInstIds );
+    if ( Vec_IntCountPositive(&pNtk->vInstIds) == 0 )
+        Vec_IntErase( &pNtk->vInstIds );
+    // map name IDs into object IDs
+    vName2Obj = Vec_IntInvert( &pNtk->vNameIds, 0 );
+    Wln_NtkForEachObj( pNtk, i )
+        Wln_ObjForEachFanin( pNtk, i, iFanin, k )
+            Wln_ObjSetFanin( pNtk, i, k, Vec_IntEntry(vName2Obj, iFanin) );
+    Vec_IntFree(vName2Obj);
+    // create fake object names
+    NameIdMax = Vec_IntFindMax(&pNtk->vNameIds);
+    nDigits = Abc_Base10Log( NameIdMax+1 );
+    pNtk->pManName = Abc_NamStart( NameIdMax+1, 10 );
+    for ( i = 1; i <= NameIdMax; i++ )
+    {
+        char pName[20]; sprintf( pName, "s%0*d", nDigits, i );
+        NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
+        assert( !fFound && i == NameId );
+    }
+    // add const strings
+    i = 0;
+    Wln_NtkForEachObj( pNtk, iObj )
+        if ( Wln_ObjIsConst(pNtk, iObj) )
+            Wln_ObjSetConst( pNtk, iObj, Abc_NamStrFindOrAdd(pNtk->pManName, (char *)Vec_PtrEntry(vConstStrings, i++), NULL) );
+    assert( i == Vec_PtrSize(vConstStrings) );
+    Vec_PtrFree( vConstStrings );
+    //Ndr_NtkPrintObjects( pNtk );
+    //Wln_WriteVer( pNtk, "temp_ndr.v", 0, 0 );
+    // derive topological order
+    pNtk = Wln_NtkDupDfs( pTemp = pNtk );
+    Wln_NtkFree( pTemp );
+    //Ndr_NtkPrintObjects( pNtk );
+    //pNtk->fMemPorts = 1;          // the network contains memory ports
+    //pNtk->fEasyFfs = 1;           // the network contains simple flops
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Wln_Ntk_t * Wln_ReadNdr( char * pFileName )
+{
+    void * pData = Ndr_Read( pFileName );
+    Wln_Ntk_t * pNtk = Wln_NtkFromNdr( pData );
+    //char * ppNames[10] = { NULL, "a", "b", "c", "d", "e", "f", "g", "h", "i" };
+    //Ndr_WriteVerilog( NULL, pData, ppNames );
+    Ndr_Delete( pData );
+    return pNtk;
+}
+void Wln_ReadNdrTest()
+{
+    Wln_Ntk_t * pNtk = Wln_ReadNdr( "D:\\temp\\brijesh\\for_alan_dff_warning\\work_fir_filter_fir_filter_proc_out.ndr" );
+    //Wln_Ntk_t * pNtk = Wln_ReadNdr( "flop.ndr" );
+    Wln_WriteVer( pNtk, "test__test.v" );
+    Wln_NtkPrint( pNtk );
+    Wln_NtkStaticFanoutTest( pNtk );
+    Wln_NtkFree( pNtk );
+}
+void Wln_NtkRetimeTest( char * pFileName )
+{
+    void * pData = Ndr_Read( pFileName );
+    Wln_Ntk_t * pNtk = Wln_NtkFromNdr( pData );
+    Ndr_Delete( pData );
+    if ( !Wln_NtkHasInstId(pNtk) )
+        printf( "The design has no delay information.\n" );
+    else
+    {
+        Vec_Int_t * vMoves = Wln_NtkRetime( pNtk );
+        Vec_IntPrint( vMoves );
+        Vec_IntFree( vMoves );
+    }
+    Wln_NtkFree( pNtk );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wln/wlnNtk.c b/src/base/wln/wlnNtk.c
new file mode 100644
index 00000000..39c03964
--- /dev/null
+++ b/src/base/wln/wlnNtk.c
@@ -0,0 +1,321 @@
+/**CFile****************************************************************
+
+  FileName    [wlnNtk.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Word-level network.]
+
+  Synopsis    [Network construction procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 23, 2018.]
+
+  Revision    [$Id: wlnNtk.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wln.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creating networks.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Wln_Ntk_t * Wln_NtkAlloc( char * pName, int nObjsMax )
+{
+    Wln_Ntk_t * p; int i;
+    p = ABC_CALLOC( Wln_Ntk_t, 1 );
+    p->pName = pName ? Extra_FileNameGeneric( pName ) : NULL;
+    Vec_IntGrow( &p->vCis, 111 );
+    Vec_IntGrow( &p->vCos, 111 );
+    Vec_IntGrow( &p->vFfs, 111 );
+    Vec_IntGrow( &p->vTypes,  nObjsMax+1 );
+    Vec_StrGrow( &p->vSigns,  nObjsMax+1 );
+    Vec_IntGrow( &p->vRanges, nObjsMax+1 );
+    Vec_IntPush( &p->vTypes,  -1 );
+    Vec_StrPush( &p->vSigns,  -1 );
+    Vec_IntPush( &p->vRanges, -1 );
+    p->vFanins = ABC_CALLOC( Wln_Vec_t, nObjsMax+1 );
+    p->pRanges = Hash_IntManStart( 1000 );
+    for ( i = 0; i < 65; i++ )
+        Hash_Int2ManInsert( p->pRanges, i, i, 0 );
+    for ( i = 1; i < 64; i++ )
+        Hash_Int2ManInsert( p->pRanges, i, 0, 0 );
+    assert( Hash_IntManEntryNum(p->pRanges) == 128 );
+    return p;
+}
+void Wln_NtkFree( Wln_Ntk_t * p )
+{
+    int i;
+    for ( i = 0; i < Wln_NtkObjNum(p); i++ )
+        if ( Wln_ObjFaninNum(p, i) > 2 ) 
+            ABC_FREE( p->vFanins[i].pArray[0] );
+    ABC_FREE( p->vFanins );
+
+    if ( p->pRanges )  Hash_IntManStop( p->pRanges );
+    if ( p->pManName ) Abc_NamStop( p->pManName );
+
+    ABC_FREE( p->vCis.pArray );
+    ABC_FREE( p->vCos.pArray );
+    ABC_FREE( p->vFfs.pArray );
+
+    ABC_FREE( p->vTypes.pArray );
+    ABC_FREE( p->vSigns.pArray );
+    ABC_FREE( p->vRanges.pArray );
+    ABC_FREE( p->vNameIds.pArray );
+    ABC_FREE( p->vInstIds.pArray );
+    ABC_FREE( p->vTravIds.pArray );
+    ABC_FREE( p->vCopies.pArray );
+    ABC_FREE( p->vBits.pArray );
+    ABC_FREE( p->vLevels.pArray );
+    ABC_FREE( p->vRefs.pArray );
+    ABC_FREE( p->vFanout.pArray );
+    ABC_FREE( p->vFaninAttrs.pArray );
+    ABC_FREE( p->vFaninLists.pArray );
+
+    ABC_FREE( p->pName );
+    ABC_FREE( p->pSpec );
+    ABC_FREE( p );
+}
+int Wln_NtkMemUsage( Wln_Ntk_t * p )
+{
+    int Mem = sizeof(Wln_Ntk_t);
+    Mem += 4 * p->vCis.nCap;
+    Mem += 4 * p->vCos.nCap;
+    Mem += 4 * p->vFfs.nCap;
+    Mem += 1 * p->vTypes.nCap;
+    Mem += 4 * p->vRanges.nCap;
+    Mem += 4 * p->vNameIds.nCap;
+    Mem += 4 * p->vInstIds.nCap;
+    Mem += 4 * p->vTravIds.nCap;
+    Mem += 4 * p->vCopies.nCap;
+    Mem += 4 * p->vBits.nCap;
+    Mem += 4 * p->vLevels.nCap;
+    Mem += 4 * p->vRefs.nCap;
+    Mem += 4 * p->vFanout.nCap;
+    Mem += 4 * p->vFaninAttrs.nCap;
+    Mem += 4 * p->vFaninLists.nCap;
+    Mem += 20 * Hash_IntManEntryNum(p->pRanges);
+    Mem += Abc_NamMemUsed(p->pManName);
+    return Mem;
+}
+void Wln_NtkPrint( Wln_Ntk_t * p )
+{
+    int iObj;
+    printf( "Printing %d objects of network \"%s\":\n", Wln_NtkObjNum(p), p->pName );
+    Wln_NtkForEachObj( p, iObj )
+        Wln_ObjPrint( p, iObj );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicating network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wln_NtkTransferNames( Wln_Ntk_t * pNew, Wln_Ntk_t * p )
+{
+    assert( pNew->pManName  == NULL && p->pManName != NULL );
+    pNew->pManName = p->pManName; 
+    p->pManName = NULL;
+    assert( !Wln_NtkHasCopy(pNew)   && Wln_NtkHasCopy(p)   );
+    if ( Wln_NtkHasNameId(p) )
+    {
+        int i;
+        assert( !Wln_NtkHasNameId(pNew) && Wln_NtkHasNameId(p) );
+        Wln_NtkCleanNameId( pNew );
+        Wln_NtkForEachObj( p, i ) 
+            if ( Wln_ObjCopy(p, i) && i < Vec_IntSize(&p->vNameIds) && Wln_ObjNameId(p, i) )
+                Wln_ObjSetNameId( pNew, Wln_ObjCopy(p, i), Wln_ObjNameId(p, i) );
+        Vec_IntErase( &p->vNameIds );
+    }
+    if ( Wln_NtkHasInstId(p) )
+    {
+        int i;
+        assert( !Wln_NtkHasInstId(pNew) && Wln_NtkHasInstId(p) );
+        Wln_NtkCleanInstId( pNew );
+        Wln_NtkForEachObj( p, i ) 
+            if ( Wln_ObjCopy(p, i) && i < Vec_IntSize(&p->vInstIds) && Wln_ObjInstId(p, i) )
+                Wln_ObjSetInstId( pNew, Wln_ObjCopy(p, i), Wln_ObjInstId(p, i) );
+        Vec_IntErase( &p->vInstIds );
+    }
+}
+int Wln_ObjDup( Wln_Ntk_t * pNew, Wln_Ntk_t * p, int iObj )
+{
+    int i, iFanin, iObjNew = Wln_ObjClone( pNew, p, iObj );
+    Wln_ObjForEachFanin( p, iObj, iFanin, i )
+        Wln_ObjAddFanin( pNew, iObjNew, Wln_ObjCopy(p, iFanin) );
+    if ( Wln_ObjIsConst(p, iObj) )
+        Wln_ObjSetConst( pNew, iObjNew, Wln_ObjFanin0(p, iObj) );
+    else if ( Wln_ObjIsSlice(p, iObj) || Wln_ObjIsRotate(p, iObj) || Wln_ObjIsTable(p, iObj) )
+        Wln_ObjSetFanin( p, iObjNew, 1, Wln_ObjFanin1(p, iObj) );
+    Wln_ObjSetCopy( p, iObj, iObjNew );
+    return iObjNew;
+}
+int Wln_NtkDupDfs_rec( Wln_Ntk_t * pNew, Wln_Ntk_t * p, int iObj )
+{
+    int i, iFanin;
+    if ( iObj == 0 )
+        return 0;
+    if ( Wln_ObjCopy(p, iObj) )
+        return Wln_ObjCopy(p, iObj);
+    //printf( "Visiting node %d\n", iObj );
+    assert( !Wln_ObjIsFf(p, iObj) );
+    Wln_ObjForEachFanin( p, iObj, iFanin, i )
+        Wln_NtkDupDfs_rec( pNew, p, iFanin );
+    return Wln_ObjDup( pNew, p, iObj );
+}
+Wln_Ntk_t * Wln_NtkDupDfs( Wln_Ntk_t * p )
+{
+    int i, k, iObj, iFanin;
+    Wln_Ntk_t * pNew = Wln_NtkAlloc( p->pName, Wln_NtkObjNum(p) );
+    pNew->fSmtLib = p->fSmtLib;
+    if ( p->pSpec ) pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Wln_NtkCleanCopy( p );
+    Wln_NtkForEachCi( p, iObj, i )
+        Wln_ObjDup( pNew, p, iObj );
+    Wln_NtkForEachFf( p, iObj, i )
+        Wln_ObjSetCopy( p, iObj, Wln_ObjClone(pNew, p, iObj) );
+    Wln_NtkForEachCo( p, iObj, i )
+        Wln_NtkDupDfs_rec( pNew, p, iObj );
+    Wln_NtkForEachFf( p, iObj, i )
+        Wln_ObjForEachFanin( p, iObj, iFanin, k )
+            Wln_ObjAddFanin( pNew, Wln_ObjCopy(p, iObj), Wln_NtkDupDfs_rec(pNew, p, iFanin) );
+    if ( Wln_NtkHasNameId(p) )
+        Wln_NtkTransferNames( pNew, p );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create fanin/fanout map.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wln_NtkCreateRefs( Wln_Ntk_t * p )  
+{
+    int k, iObj, iFanin;
+    Wln_NtkCleanRefs( p );
+    Wln_NtkForEachObj( p, iObj )
+        Wln_ObjForEachFanin( p, iObj, iFanin, k )
+            Wln_ObjRefsInc( p, iFanin );
+}
+int Wln_NtkFaninNum( Wln_Ntk_t * p )
+{
+    int iObj, nEdges = 0;
+    Wln_NtkForEachObj( p, iObj )
+        nEdges += Wln_ObjFaninNum(p, iObj);
+    return nEdges;
+}
+void Wln_NtkStartFaninMap( Wln_Ntk_t * p, Vec_Int_t * vFaninMap, int nMulti )
+{
+    int iObj, iOffset = Wln_NtkObjNum(p);
+    Vec_IntFill( vFaninMap, iOffset + nMulti * Wln_NtkFaninNum(p), 0 );
+    Wln_NtkForEachObj( p, iObj )
+    {
+        Vec_IntWriteEntry( vFaninMap, iObj, iOffset );
+        iOffset += nMulti * Wln_ObjFaninNum(p, iObj);
+    }
+    assert( iOffset == Vec_IntSize(vFaninMap) );
+}
+void Wln_NtkStartFanoutMap( Wln_Ntk_t * p, Vec_Int_t * vFanoutMap, Vec_Int_t * vFanoutNums, int nMulti )
+{
+    int iObj, iOffset = Wln_NtkObjNum(p);
+    Vec_IntFill( vFanoutMap, iOffset + nMulti * Vec_IntSum(vFanoutNums), 0 );
+    Wln_NtkForEachObj( p, iObj )
+    {
+        Vec_IntWriteEntry( vFanoutMap, iObj, iOffset );
+        iOffset += nMulti * Wln_ObjRefs(p, iObj);
+    }
+    assert( iOffset == Vec_IntSize(vFanoutMap) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Static fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wln_NtkStaticFanoutStart( Wln_Ntk_t * p )
+{
+    int k, iObj, iFanin;
+    Vec_Int_t * vRefsCopy = Vec_IntAlloc(0);
+    Wln_NtkCreateRefs( p );
+    Wln_NtkStartFanoutMap( p, &p->vFanout, &p->vRefs, 1 );
+    ABC_SWAP( Vec_Int_t, *vRefsCopy, p->vRefs );
+    // add fanouts
+    Wln_NtkCleanRefs( p );
+    Wln_NtkForEachObj( p, iObj )
+        Wln_ObjForEachFanin( p, iObj, iFanin, k )
+            Wln_ObjSetFanout( p, iFanin, Wln_ObjRefsInc(p, iFanin), iObj );
+    // double-check the current number of fanouts added
+    Wln_NtkForEachObj( p, iObj )
+        assert( Wln_ObjRefs(p, iObj) == Vec_IntEntry(vRefsCopy, iObj) );
+    Vec_IntFree( vRefsCopy );
+}
+void Wln_NtkStaticFanoutStop( Wln_Ntk_t * p )
+{
+    Vec_IntErase( &p->vRefs );
+    Vec_IntErase( &p->vFanout );
+}
+void Wln_NtkStaticFanoutTest( Wln_Ntk_t * p )
+{
+    int k, iObj, iFanout;
+    printf( "Printing fanouts of %d objects of network \"%s\":\n", Wln_NtkObjNum(p), p->pName );
+    Wln_NtkStaticFanoutStart( p );
+    Wln_NtkForEachObj( p, iObj )
+    {
+        Wln_ObjPrint( p, iObj );
+        printf( "   Fanouts : " );
+        Wln_ObjForEachFanoutStatic( p, iObj, iFanout, k )
+            printf( "%5d ", iFanout );
+        printf( "\n" );
+    }
+    Wln_NtkStaticFanoutStop( p );
+    printf( "\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wln/wlnObj.c b/src/base/wln/wlnObj.c
new file mode 100644
index 00000000..ec373304
--- /dev/null
+++ b/src/base/wln/wlnObj.c
@@ -0,0 +1,151 @@
+/**CFile****************************************************************
+
+  FileName    [wlnObj.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Word-level network.]
+
+  Synopsis    [Object construction procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 23, 2018.]
+
+  Revision    [$Id: wlnObj.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wln.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creating objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Wln_ObjName( Wln_Ntk_t * p, int iObj )
+{
+    static char Buffer[100];
+    if ( Wln_NtkHasNameId(p) && Wln_ObjNameId(p, iObj) )
+        return Abc_NamStr( p->pManName, Wln_ObjNameId(p, iObj) );
+    sprintf( Buffer, "n%d", iObj );
+    return Buffer;
+}                          
+char * Wln_ObjConstString( Wln_Ntk_t * p, int iObj )
+{
+    assert( Wln_ObjIsConst(p, iObj) );
+    return Abc_NamStr( p->pManName, Wln_ObjFanin0(p, iObj) );
+}                          
+void Wln_ObjUpdateType( Wln_Ntk_t * p, int iObj, int Type )
+{
+    assert( Wln_ObjIsNone(p, iObj) );
+    p->nObjs[Wln_ObjType(p, iObj)]--;
+    Vec_IntWriteEntry( &p->vTypes, iObj, Type );
+    p->nObjs[Wln_ObjType(p, iObj)]++;
+}
+void Wln_ObjSetConst( Wln_Ntk_t * p, int iObj, int NameId )
+{
+    assert( Wln_ObjIsConst(p, iObj) );
+    Wln_ObjSetFanin( p, iObj, 0, NameId );
+}
+void Wln_ObjSetSlice( Wln_Ntk_t * p, int iObj, int SliceId )
+{
+    assert( Wln_ObjIsSlice(p, iObj) );
+    Wln_ObjSetFanin( p, iObj, 1, SliceId );
+}
+void Wln_ObjAddFanin( Wln_Ntk_t * p, int iObj, int i )        
+{ 
+    Wln_Vec_t * pVec = p->vFanins + iObj;
+    if ( Wln_ObjFaninNum(p, iObj) < 2 )
+        pVec->Array[pVec->nSize++] = i;
+    else if ( Wln_ObjFaninNum(p, iObj) == 2 )
+    {
+        int * pArray = ABC_ALLOC( int, 4 );
+        pArray[0] = pVec->Array[0];
+        pArray[1] = pVec->Array[1];
+        pArray[2] = i;
+        pVec->pArray[0] = pArray;
+        pVec->nSize     = 3;
+        pVec->nCap      = 4;
+    }
+    else 
+    {
+        if ( pVec->nSize == pVec->nCap )
+            pVec->pArray[0] = ABC_REALLOC( int, pVec->pArray[0], (pVec->nCap = 2*pVec->nSize) ); 
+        assert( pVec->nSize < pVec->nCap );
+        pVec->pArray[0][pVec->nSize++] = i;
+    }
+}
+int Wln_ObjAddFanins( Wln_Ntk_t * p, int iObj, Vec_Int_t * vFanins )
+{
+    int i, iFanin;
+    Vec_IntForEachEntry( vFanins, iFanin, i )
+        Wln_ObjAddFanin( p, iObj, iFanin );
+    return iObj;
+}
+int Wln_ObjAlloc( Wln_Ntk_t * p, int Type, int Signed, int End, int Beg )
+{
+    int iObj = Vec_IntSize(&p->vTypes);
+    if ( iObj == Vec_IntCap(&p->vTypes) )
+    {
+        p->vFanins = ABC_REALLOC( Wln_Vec_t, p->vFanins, 2 * iObj );
+        memset( p->vFanins + iObj, 0, sizeof(Wln_Vec_t) * iObj );
+        Vec_IntGrow( &p->vTypes, 2 * iObj );
+    }
+    assert( iObj == Vec_StrSize(&p->vSigns) );
+    assert( iObj == Vec_IntSize(&p->vRanges) );
+    Vec_IntPush( &p->vTypes, Type );
+    Vec_StrPush( &p->vSigns, (char)Signed );
+    Vec_IntPush( &p->vRanges, Hash_Int2ManInsert(p->pRanges, End, Beg, 0) );
+    if ( Wln_ObjIsCi(p, iObj) ) Wln_ObjSetFanin( p, iObj, 1, Vec_IntSize(&p->vCis) ), Vec_IntPush( &p->vCis, iObj );
+    if ( Wln_ObjIsCo(p, iObj) ) Wln_ObjSetFanin( p, iObj, 1, Vec_IntSize(&p->vCos) ), Vec_IntPush( &p->vCos, iObj );
+    if ( Wln_ObjIsFf(p, iObj) ) Vec_IntPush( &p->vFfs, iObj );
+    p->nObjs[Type]++;
+    return iObj;
+}
+int Wln_ObjClone( Wln_Ntk_t * pNew, Wln_Ntk_t * p, int iObj )
+{
+    return Wln_ObjAlloc( pNew, Wln_ObjType(p, iObj), Wln_ObjIsSigned(p, iObj), Wln_ObjRangeEnd(p, iObj), Wln_ObjRangeBeg(p, iObj) );
+}
+int Wln_ObjCreateCo( Wln_Ntk_t * p, int iFanin )
+{
+    int iCo = Wln_ObjClone( p, p, iFanin );
+    Wln_ObjUpdateType( p, iCo, ABC_OPER_CO );
+    Wln_ObjAddFanin( p, iCo, iFanin );
+    return iCo;
+}
+void Wln_ObjPrint( Wln_Ntk_t * p, int iObj )
+{
+    int k, iFanin, Type = Wln_ObjType(p, iObj);
+    printf( "Obj %6d : Type = %6s  Fanins = %d : ", iObj, Abc_OperName(Type), Wln_ObjFaninNum(p, iObj) );
+    Wln_ObjForEachFanin( p, iObj, iFanin, k )
+        printf( "%5d ", iFanin );
+    printf( "\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wln/wlnRetime.c b/src/base/wln/wlnRetime.c
new file mode 100644
index 00000000..7d28e22e
--- /dev/null
+++ b/src/base/wln/wlnRetime.c
@@ -0,0 +1,487 @@
+/**CFile****************************************************************
+
+  FileName    [wlnRetime.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Word-level network.]
+
+  Synopsis    [Retiming.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 23, 2018.]
+
+  Revision    [$Id: wlnRetime.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wln.h"
+#include "misc/vec/vecHsh.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Wln_Ret_t_ Wln_Ret_t;
+struct Wln_Ret_t_ 
+{
+    Wln_Ntk_t *       pNtk;         // static netlist
+    Vec_Int_t         vFanins;      // fanins and edge places
+    Vec_Int_t         vFanouts;     // fanouts and edge places
+    Vec_Int_t         vEdgeLinks;   // edge links
+    Vec_Int_t         vFfClasses;   // flop classes
+    Vec_Int_t         vNodeDelays;  // object delays
+    Vec_Int_t         vPathDelays;  // delays from sources to sinks
+    Vec_Int_t         vSources;     // critical sources
+    Vec_Int_t         vSinks;       // critical sinks
+    Vec_Int_t         vFront;       // retiming frontier
+    Vec_Int_t         vMoves;       // retiming moves (paired with delay)
+    int               nClasses;     // the number of flop classes
+    int               DelayMax;     // critical delay at any time
+};
+
+static inline int *   Wln_RetFanins( Wln_Ret_t * p, int i )  { return Vec_IntEntryP( &p->vFanins,  Vec_IntEntry(&p->vFanins, i) );  }
+static inline int *   Wln_RetFanouts( Wln_Ret_t * p, int i ) { return Vec_IntEntryP( &p->vFanouts, Vec_IntEntry(&p->vFanouts, i) ); }
+
+#define Wln_RetForEachFanin( p, iObj, iFanin, pLink, i )    \
+    for ( i = 0; (i < Wln_ObjFaninNum(p->pNtk, iObj)) &&    \
+         (((iFanin) = Wln_RetFanins(p, iObj)[2*i]), 1) &&   \
+           ((pLink) = (Wln_RetFanins(p, iObj)+2*i+1)); i++ ) if ( !iFanin )  {} else
+
+#define Wln_RetForEachFanout( p, iObj, iFanout, pLink, i )  \
+    for ( i = 0; (i < Wln_ObjRefs(p->pNtk, iObj)) &&        \
+        (((iFanout) = Wln_RetFanouts(p, iObj)[2*i]), 1) &&  \
+           ((pLink) = Vec_IntEntryP(&p->vFanins, Wln_RetFanouts(p, iObj)[2*i+1])); i++ ) if ( !iFanout ) {} else
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Retiming manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Wln_RetComputeFfClasses( Wln_Ntk_t * pNtk, Vec_Int_t * vClasses )
+{
+    int i, k, iObj, nClasses;
+    Hsh_VecMan_t * p = Hsh_VecManStart( 10 );
+    Vec_Int_t * vFlop = Vec_IntAlloc( 6 ); 
+    Vec_IntFill( vClasses, Wln_NtkObjNum(pNtk), -1 );
+    Wln_NtkForEachFf( pNtk, iObj, i )
+    {
+        Vec_IntClear( vFlop );
+        for ( k = 1; k <= 6; k++ )
+            Vec_IntPush( vFlop, Wln_ObjFanin(pNtk, iObj, k) );
+        Vec_IntWriteEntry( vClasses, iObj, Hsh_VecManAdd(p, vFlop) );
+    }
+    nClasses = Hsh_VecSize( p );
+    Hsh_VecManStop( p );
+    Vec_IntFree( vFlop );
+    printf( "Detected %d flop classes.\n", nClasses );
+    return nClasses;
+}
+Wln_Ret_t * Wln_RetAlloc( Wln_Ntk_t * pNtk )
+{
+    Wln_Ret_t * p; int k, iObj, iFanin;
+    Vec_Int_t * vRefsCopy = Vec_IntAlloc(0);
+    p = ABC_CALLOC( Wln_Ret_t, 1 );
+    p->pNtk = pNtk;
+    Wln_NtkCreateRefs( pNtk );
+    Wln_NtkStartFaninMap( pNtk, &p->vFanins, 2 );
+    Wln_NtkStartFanoutMap( pNtk, &p->vFanouts, &pNtk->vRefs, 2 );
+    ABC_SWAP( Vec_Int_t, *vRefsCopy, pNtk->vRefs );
+    Wln_NtkCleanRefs( pNtk );
+    Vec_IntGrow( &p->vEdgeLinks, 10*Wln_NtkFfNum(pNtk) );
+    Vec_IntPushTwo( &p->vEdgeLinks, -1, -1 );
+    Wln_NtkForEachObj( pNtk, iObj )
+        Wln_ObjForEachFanin( pNtk, iObj, iFanin, k )
+        {
+            int * pFanins  = Wln_RetFanins( p, iObj );
+            int * pFanouts = Wln_RetFanouts( p, iFanin );
+            int Index      = Wln_ObjRefsInc( pNtk, iFanin );
+            pFanins[2*k+0]      = iFanin;
+            pFanins[2*k+1]      = Wln_ObjIsFf(pNtk, iFanin) ? Vec_IntSize(&p->vEdgeLinks) : 0;
+            pFanouts[2*Index+0] = iObj;
+            pFanouts[2*Index+1] = Vec_IntEntry(&p->vFanins, iObj) + 2*k + 1;
+            if ( Wln_ObjIsFf(pNtk, iFanin) )
+                Vec_IntPushTwo( &p->vEdgeLinks, 0, iFanin );
+        }
+    // double-check the current number of fanouts added
+    Wln_NtkForEachObj( pNtk, iObj )
+        assert( Wln_ObjRefs(pNtk, iObj) == Vec_IntEntry(vRefsCopy, iObj) );
+    Vec_IntFree( vRefsCopy );
+    // other data
+    p->nClasses = Wln_RetComputeFfClasses( pNtk, &p->vFfClasses );
+    ABC_SWAP( Vec_Int_t, p->vNodeDelays, pNtk->vInstIds );
+    Vec_IntGrow( &p->vSources, 1000 );
+    Vec_IntGrow( &p->vSinks, 1000 );
+    Vec_IntGrow( &p->vFront, 1000 );
+    Vec_IntGrow( &p->vMoves, 1000 );
+    return p;
+}
+void Wln_RetFree( Wln_Ret_t * p )
+{
+    ABC_FREE( p->vFanins.pArray );
+    ABC_FREE( p->vFanouts.pArray );
+    ABC_FREE( p->vEdgeLinks.pArray );
+    ABC_FREE( p->vFfClasses.pArray );
+    ABC_FREE( p->vNodeDelays.pArray );
+    ABC_FREE( p->vPathDelays.pArray );
+    ABC_FREE( p->vSources.pArray );
+    ABC_FREE( p->vSinks.pArray );
+    ABC_FREE( p->vFront.pArray );
+    ABC_FREE( p->vMoves.pArray );
+    ABC_FREE( p );
+}
+int Wln_RetMemUsage( Wln_Ret_t * p )
+{
+    int Mem = sizeof(Wln_Ret_t);
+    Mem += 4 * p->vFanins.nCap;
+    Mem += 4 * p->vFanouts.nCap;
+    Mem += 4 * p->vEdgeLinks.nCap;
+    Mem += 4 * p->vFfClasses.nCap;
+    Mem += 4 * p->vNodeDelays.nCap;
+    Mem += 4 * p->vPathDelays.nCap;
+    Mem += 4 * p->vSources.nCap;
+    Mem += 4 * p->vSinks.nCap;
+    Mem += 4 * p->vFront.nCap;
+    Mem += 4 * p->vMoves.nCap;
+    return Mem;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delay propagation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wln_RetMarkChanges_rec( Wln_Ret_t * p, int iObj )
+{
+    int k, iFanout, * pLink, * pDelay = Vec_IntEntryP( &p->vPathDelays, iObj );
+    if ( *pDelay < 0 )
+        return;
+    *pDelay = -1;
+    Wln_RetForEachFanout( p, iObj, iFanout, pLink, k )
+        if ( !pLink[0] )
+            Wln_RetMarkChanges_rec( p, iFanout );
+}
+int Wln_RetPropDelay_rec( Wln_Ret_t * p, int iObj )
+{
+    int k, iFanin, * pLink, * pDelay = Vec_IntEntryP( &p->vPathDelays, iObj );
+    if ( *pDelay >= 0 )
+        return *pDelay;
+    Wln_RetForEachFanin( p, iObj, iFanin, pLink, k )
+        if ( pLink[0] )
+            *pDelay = Abc_MaxInt(*pDelay, 0);
+        else
+            *pDelay = Abc_MaxInt(*pDelay, Wln_RetPropDelay_rec(p, iFanin));
+    *pDelay += Vec_IntEntry( &p->vNodeDelays, iObj );
+    return *pDelay;
+}
+int Wln_RetPropDelay( Wln_Ret_t * p, Vec_Int_t * vFront )
+{
+    int i, iObj, DelayMax = 0;
+    if ( vFront )
+    {
+        Vec_IntForEachEntry( vFront, iObj, i )
+            Wln_RetMarkChanges_rec( p, iObj );
+    }
+    else
+    {
+        Vec_IntFill( &p->vPathDelays, Wln_NtkObjNum(p->pNtk), -1 );
+        Wln_NtkForEachCi( p->pNtk, iObj, i )
+            Vec_IntWriteEntry( &p->vPathDelays, iObj, 0 );
+    }
+    Vec_IntClear( &p->vSinks );
+    Wln_NtkForEachObj( p->pNtk, iObj )
+        if ( !Wln_ObjIsCo(p->pNtk, iObj) )
+        {
+            int Delay = Wln_RetPropDelay_rec(p, iObj);
+            if ( DelayMax == Delay )
+                Vec_IntPush( &p->vSinks, iObj );
+            else if ( DelayMax < Delay )
+            {
+                DelayMax = Delay;
+                Vec_IntFill( &p->vSinks, 1, iObj );
+            }
+        }
+    return DelayMax;
+}
+
+void Wln_RetFindSources_rec( Wln_Ret_t * p, int iObj )
+{
+    int k, iFanin, * pLink, FaninDelay, fTerm = 1;
+    if ( Wln_ObjIsCi(p->pNtk, iObj) || Wln_ObjCheckTravId(p->pNtk, iObj) )
+        return;
+    FaninDelay = Vec_IntEntry( &p->vPathDelays, iObj ) - Vec_IntEntry( &p->vNodeDelays, iObj );
+    Wln_RetForEachFanin( p, iObj, iFanin, pLink, k )
+    {
+        if ( !pLink[0] )
+            continue;
+        fTerm = 0;
+        if ( Vec_IntEntry(&p->vPathDelays, iFanin) == FaninDelay )
+            Wln_RetFindSources_rec( p, iFanin );
+    }
+    if ( fTerm )
+        Vec_IntPush( &p->vSources, iObj );
+}
+void Wln_RetFindSources( Wln_Ret_t * p )
+{
+    int i, iObj;
+    Vec_IntClear( &p->vSources );
+    Wln_NtkIncrementTravId( p->pNtk );
+    Vec_IntForEachEntry( &p->vSinks, iObj, i )
+        Wln_RetFindSources_rec( p, iObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retimability check.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Wln_RetHeadToTail( Wln_Ret_t * p, int * pHead )
+{
+    int * pLink;
+    assert( pHead[0] );
+    pLink = Vec_IntEntryP( &p->vEdgeLinks, pHead[0] );
+    if ( pLink[0] == 0 )
+        return pHead;
+    return Wln_RetHeadToTail( p, pLink );
+}
+
+static inline int Wln_RetCheckForwardOne( Wln_Ret_t * p, int iObj )
+{
+    int k, iFanin, * pLink, iFlop, Class = -1;
+    Wln_RetForEachFanin( p, iObj, iFanin, pLink, k )
+    {
+        if ( !pLink[0] )
+            return 0;
+        iFlop = Vec_IntEntry( &p->vEdgeLinks, pLink[0] + 1 );
+        assert( Wln_ObjIsFf( p->pNtk, iFlop ) );
+        if ( Class == -1 )
+            Class = Vec_IntEntry( &p->vFfClasses, iFlop );
+        else if ( Class != Vec_IntEntry( &p->vFfClasses, iFlop ) )
+            return 0;
+    }
+    return 1;
+}
+int Wln_RetCheckForward( Wln_Ret_t * p, Vec_Int_t * vSet )
+{
+    int i, iObj;
+    Vec_IntForEachEntry( vSet, iObj, i )
+        if ( !Wln_RetCheckForwardOne( p, iObj ) )
+            return 0;
+    return 1;
+}
+
+static inline int Wln_RetCheckBackwardOne( Wln_Ret_t * p, int iObj )
+{
+    int k, iFanin, * pLink, iFlop, Class = -1;
+    Wln_RetForEachFanout( p, iObj, iFanin, pLink, k )
+    {
+        if ( !pLink[0] )
+            return 0;
+        pLink = Wln_RetHeadToTail( p, pLink );
+        iFlop = Vec_IntEntry( &p->vEdgeLinks, pLink[0] + 1 );
+        assert( Wln_ObjIsFf( p->pNtk, iFlop ) );
+        if ( Class == -1 )
+            Class = Vec_IntEntry( &p->vFfClasses, iFlop );
+        else if ( Class != Vec_IntEntry( &p->vFfClasses, iFlop ) )
+            return 0;
+    }
+    return 1;
+}
+int Wln_RetCheckBackward( Wln_Ret_t * p, Vec_Int_t * vSet )
+{
+    int i, iObj;
+    Vec_IntForEachEntry( vSet, iObj, i )
+        if ( !Wln_RetCheckBackwardOne( p, iObj ) )
+            return 0;
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Moving flops.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Wln_RetRemoveOneFanin( Wln_Ret_t * p, int iObj )
+{
+    int k, iFanin, * pLink, iFlop, iFlop1 = -1;
+    int * pFanins  = Wln_RetFanins( p, iObj );
+    Wln_RetForEachFanin( p, iObj, iFanin, pLink, k )
+    {
+        assert( pLink[0] );
+        pFanins[2*k+1] = Vec_IntEntry( &p->vEdgeLinks, pLink[0] );
+        iFlop = Vec_IntEntry( &p->vEdgeLinks, pLink[0] + 1 );
+        assert( Wln_ObjIsFf( p->pNtk, iFlop ) );
+        if ( iFlop1 == -1 )
+            iFlop1 = iFlop;
+    }
+    return iFlop1;
+}
+int Wln_RetRemoveOneFanout( Wln_Ret_t * p, int iObj )
+{
+    int k, iFanin, * pLink, iFlop, iFlop1 = -1;
+    int * pFanins  = Wln_RetFanins( p, iObj );
+    Wln_RetForEachFanout( p, iObj, iFanin, pLink, k )
+    {
+        assert( pLink[0] );
+        pLink = Wln_RetHeadToTail( p, pLink );
+        iFlop = Vec_IntEntry( &p->vEdgeLinks, pLink[0] + 1 );
+        pLink[0] = 0;
+        assert( Wln_ObjIsFf( p->pNtk, iFlop ) );
+        if ( iFlop1 == -1 )
+            iFlop1 = iFlop;
+    }
+    return iFlop1;
+}
+void Wln_RetInsertOneFanin( Wln_Ret_t * p, int iObj, int iFlop )
+{
+    int k, iFanin, * pLink;
+    int * pFanins  = Wln_RetFanins( p, iObj );
+    assert( Wln_ObjIsFf( p->pNtk, iFlop ) );
+    Wln_RetForEachFanin( p, iObj, iFanin, pLink, k )
+    {
+        int iHead = pFanins[2*k+1];
+        pFanins[2*k+1] = Vec_IntSize(&p->vEdgeLinks);
+        Vec_IntPushTwo( &p->vEdgeLinks, iHead, iFlop );
+    }
+}
+void Wln_RetInsertOneFanout( Wln_Ret_t * p, int iObj, int iFlop )
+{
+    int k, iFanin, * pLink;
+    assert( Wln_ObjIsFf( p->pNtk, iFlop ) );
+    Wln_RetForEachFanout( p, iObj, iFanin, pLink, k )
+    {
+        if ( pLink[0] )
+            pLink = Wln_RetHeadToTail( p, pLink );
+        pLink = Vec_IntEntryP( &p->vEdgeLinks, pLink[0] );
+        assert( pLink[0] == 0 );
+        pLink[0] = Vec_IntSize(&p->vEdgeLinks);
+        Vec_IntPushTwo( &p->vEdgeLinks, 0, iFlop );
+    }
+}
+void Wln_RetRetimeForward( Wln_Ret_t * p, Vec_Int_t * vSet )
+{
+    int i, iObj, iFlop;
+    Vec_IntForEachEntry( vSet, iObj, i )
+    {
+        iFlop = Wln_RetRemoveOneFanin( p, iObj );
+        Wln_RetInsertOneFanout( p, iObj, iFlop );
+    }
+}
+void Wln_RetRetimeBackward( Wln_Ret_t * p, Vec_Int_t * vSet )
+{
+    int i, iObj, iFlop;
+    Vec_IntForEachEntry( vSet, iObj, i )
+    {
+        iFlop = Wln_RetRemoveOneFanout( p, iObj );
+        Wln_RetInsertOneFanin( p, iObj, iFlop );
+    }
+}
+void Wln_RetAddToMoves( Wln_Ret_t * p, Vec_Int_t * vSet, int Delay, int fForward )
+{
+    int i, iObj;
+    if ( vSet == NULL )
+    {
+        Vec_IntPushTwo( &p->vMoves, 0, Delay );
+        return;
+    }
+    Vec_IntForEachEntry( vSet, iObj, i )
+    {
+        int NameId = Vec_IntEntry( &p->pNtk->vNameIds, iObj );
+        Vec_IntPushTwo( &p->vMoves, fForward ? NameId : -NameId, Delay );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retiming computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wln_NtkRetime( Wln_Ntk_t * pNtk )
+{
+    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);
+    p->DelayMax = Wln_RetPropDelay( p, NULL );
+    Wln_RetFindSources( p );
+    Wln_RetAddToMoves( p, NULL, p->DelayMax, 0 );
+    while ( Vec_IntSize(vSources) || Vec_IntSize(vSinks) )
+    {
+        int fForward  = Vec_IntSize(vSources) && Wln_RetCheckForward( p, vSources );
+        int fBackward = Vec_IntSize(vSinks)   && Wln_RetCheckBackward( p, vSinks );
+        if ( !fForward && !fBackward )
+        {
+            printf( "Cannot retime forward and backward.\n" );
+            break;
+        }
+        Vec_IntSort( vSources, 0 );
+        Vec_IntSort( vSinks, 0 );
+        if ( Vec_IntTwoCountCommon(vSources, vSinks) )
+        {
+            printf( "Cannot reduce delay by retiming.\n" );
+            break;
+        }
+        Vec_IntClear( vFront );
+        if ( (fForward && !fBackward) || (fForward && fBackward && Vec_IntSize(vSources) < Vec_IntSize(vSinks)) )
+            Wln_RetRetimeForward( p, vSources ), Vec_IntAppend( vFront, vSources ), fForward = 1, fBackward = 0;
+        else
+            Wln_RetRetimeBackward( p, vSinks ),  Vec_IntAppend( vFront, vSources ), fForward = 0, fBackward = 1;
+        p->DelayMax = Wln_RetPropDelay( p, vFront );
+        Wln_RetAddToMoves( p, vFront, p->DelayMax, fForward );
+        Wln_RetFindSources( p );
+        if ( 2*Vec_IntSize(&p->vEdgeLinks) > Vec_IntCap(&p->vEdgeLinks) )
+            Vec_IntGrow( &p->vEdgeLinks, 4*Vec_IntSize(&p->vEdgeLinks) );
+    }
+    ABC_SWAP( Vec_Int_t, *vMoves, p->vMoves );
+    Wln_RetFree( p );
+    return vMoves;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wln/wlnWriteVer.c b/src/base/wln/wlnWriteVer.c
new file mode 100644
index 00000000..1c37e311
--- /dev/null
+++ b/src/base/wln/wlnWriteVer.c
@@ -0,0 +1,494 @@
+/**CFile****************************************************************
+
+  FileName    [wlnWriteVer.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Word-level network.]
+
+  Synopsis    [Writing Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 23, 2018.]
+
+  Revision    [$Id: wlnWriteVer.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wln.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wln_WriteTableOne( FILE * pFile, int nFans, int nOuts, word * pTable, int Id )
+{
+    int m, nMints = (1<<nFans);
+//    Abc_TtPrintHexArrayRev( stdout, pTable, nMints );  printf( "\n" );
+    assert( nOuts > 0 && nOuts <= 64 && (64 % nOuts) == 0 );
+    fprintf( pFile, "module table%d(ind, val);\n", Id );
+    fprintf( pFile, "  input  [%d:0] ind;\n", nFans-1 );
+    fprintf( pFile, "  output [%d:0] val;\n", nOuts-1 );
+    fprintf( pFile, "  reg    [%d:0] val;\n", nOuts-1 );
+    fprintf( pFile, "  always @(ind)\n" );
+    fprintf( pFile, "  begin\n" );
+    fprintf( pFile, "    case (ind)\n" );
+    for ( m = 0; m < nMints; m++ )
+    fprintf( pFile, "      %d\'h%x: val = %d\'h%x;\n", nFans, m, nOuts, (unsigned)((pTable[(nOuts * m) >> 6] >> ((nOuts * m) & 63)) & Abc_Tt6Mask(nOuts)) );
+    fprintf( pFile, "    endcase\n" );
+    fprintf( pFile, "  end\n" );
+    fprintf( pFile, "endmodule\n" );
+    fprintf( pFile, "\n" );
+}
+void Wln_WriteTables( FILE * pFile, Wln_Ntk_t * p )
+{
+    Vec_Int_t * vNodes;
+    word * pTable; 
+    int i, iObj;
+    if ( p->vTables == NULL || Vec_PtrSize(p->vTables) == 0 )
+        return;
+    // map tables into their nodes
+    vNodes = Vec_IntStart( Vec_PtrSize(p->vTables) );
+    Wln_NtkForEachObj( p, iObj )
+        if ( Wln_ObjType(p, iObj) == ABC_OPER_TABLE )
+            Vec_IntWriteEntry( vNodes, Wln_ObjFanin1(p, iObj), iObj );
+    // write tables
+    Vec_PtrForEachEntry( word *, p->vTables, pTable, i )
+    {
+        int iNode  = Vec_IntEntry( vNodes, i );
+        int iFanin = Wln_ObjFanin0( p, iNode );
+        Wln_WriteTableOne( pFile, Wln_ObjRange(p, iFanin), Wln_ObjRange(p, iNode), pTable, i );
+    }
+    Vec_IntFree( vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This was used to add POs to each node except PIs and MUXes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wln_WriteAddPos( Wln_Ntk_t * p )
+{
+    int iObj;
+    Wln_NtkForEachObj( p, iObj )
+        if ( !Wln_ObjIsCio(p, iObj) )
+            Wln_ObjCreateCo( p, iObj );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wln_WriteVerIntVec( FILE * pFile, Wln_Ntk_t * p, Vec_Int_t * vVec, int Start )
+{
+    char * pName;
+    int LineLength  = Start;
+    int NameCounter = 0;
+    int AddedLength, i, iObj;
+    Vec_IntForEachEntry( vVec, iObj, i )
+    {
+        pName = Wln_ObjName( p, iObj );
+        // get the line length after this name is written
+        AddedLength = strlen(pName) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > 70 )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = Start;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", pName, (i==Vec_IntSize(vVec)-1)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+} 
+void Wln_WriteVerInt( FILE * pFile, Wln_Ntk_t * p )
+{
+    int k, j, iObj, iFanin;
+    char Range[100];
+    fprintf( pFile, "module %s ( ", p->pName );
+    fprintf( pFile, "\n   " );
+    if ( Wln_NtkCiNum(p) > 0 )
+    {
+        Wln_WriteVerIntVec( pFile, p, &p->vCis, 3 );
+        fprintf( pFile, ",\n   " );
+    }
+    if ( Wln_NtkCoNum(p) > 0 )
+        Wln_WriteVerIntVec( pFile, p, &p->vCos, 3 );
+    fprintf( pFile, "  );\n" );
+    Wln_NtkForEachObj( p, iObj )
+    {
+        int End = Wln_ObjRangeEnd(p, iObj);
+        int Beg = Wln_ObjRangeBeg(p, iObj);
+        int nDigits = Abc_Base10Log(Abc_AbsInt(End)+1) + Abc_Base10Log(Abc_AbsInt(Beg)+1) + (int)(End < 0) + (int)(Beg < 0);
+        sprintf( Range, "%s[%d:%d]%*s", (!p->fSmtLib && Wln_ObjIsSigned(p, iObj)) ? "signed ":"       ", End, Beg, 8-nDigits, "" );
+        fprintf( pFile, "  " );
+        if ( Wln_ObjIsCi(p, iObj) )
+            fprintf( pFile, "input  " );
+        else if ( Wln_ObjIsCo(p, iObj) )
+            fprintf( pFile, "output " );
+        else
+            fprintf( pFile, "       " );
+        if ( Wln_ObjIsCio(p, iObj) )
+        {
+            fprintf( pFile, "wire %s %s ;\n", Range, Wln_ObjName(p, iObj) );
+            if ( Wln_ObjIsCi(p, iObj) )
+                continue;
+            fprintf( pFile, "  assign                         " );
+            fprintf( pFile, "%-16s = %s ;\n", Wln_ObjName(p, iObj), Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            continue;
+        }
+        if ( Wln_ObjType(p, iObj) == ABC_OPER_SEL_NMUX || Wln_ObjType(p, iObj) == ABC_OPER_SEL_SEL )
+            fprintf( pFile, "reg  %s ", Range );
+        else
+            fprintf( pFile, "wire %s ", Range );
+        if ( Wln_ObjType(p, iObj) == ABC_OPER_TABLE )
+        {
+            // wire [3:0] s4972; table0 s4972_Index(s4971, s4972);
+            fprintf( pFile, "%s ;              table%d", Wln_ObjName(p, iObj), Wln_ObjFanin1(p, iObj) );
+            fprintf( pFile, " s%d_Index(%s, ", iObj, Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            fprintf( pFile, "%s)",             Wln_ObjName(p, iObj) );
+        }
+        else if ( Wln_ObjIsConst(p, iObj) )
+            fprintf( pFile, "%-16s = %s", Wln_ObjName(p, iObj), Wln_ObjConstString(p, iObj) );
+        else if ( Wln_ObjType(p, iObj) == ABC_OPER_SHIFT_ROTR || Wln_ObjType(p, iObj) == ABC_OPER_SHIFT_ROTL )
+        {
+            //  wire [27:0] s4960 = (s57 >> 17) | (s57 << 11);
+            int Num0 = Wln_ObjFanin1(p, iObj);
+            int Num1 = Wln_ObjRange(p, iObj) - Num0;
+            assert( Num0 > 0 && Num0 < Wln_ObjRange(p, iObj) );
+            fprintf( pFile, "%-16s = ", Wln_ObjName(p, iObj) );
+            if ( Wln_ObjType(p, iObj) == ABC_OPER_SHIFT_ROTR )
+                fprintf( pFile, "(%s >> %d) | (%s << %d)", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)), Num0, Wln_ObjName(p, Wln_ObjFanin0(p, iObj)), Num1 );
+            else
+                fprintf( pFile, "(%s << %d) | (%s >> %d)", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)), Num0, Wln_ObjName(p, Wln_ObjFanin0(p, iObj)), Num1 );
+        }
+        else if ( Wln_ObjType(p, iObj) == ABC_OPER_SEL_NMUX )
+        {
+            fprintf( pFile, "%s ;\n", Wln_ObjName(p, iObj) );
+            fprintf( pFile, "         " );
+            fprintf( pFile, "always @( " );
+            Wln_ObjForEachFanin( p, iObj, iFanin, k )
+                fprintf( pFile, "%s%s", k ? " or ":"", Wln_ObjName(p, Wln_ObjFanin(p, iObj, k)) );
+            fprintf( pFile, " )\n" );
+            fprintf( pFile, "           " );
+            fprintf( pFile, "begin\n" );
+            fprintf( pFile, "             " );
+            fprintf( pFile, "case ( %s )\n", Wln_ObjName(p, Wln_ObjFanin(p, iObj, 0)) );
+            Wln_ObjForEachFanin( p, iObj, iFanin, k )
+            {
+                if ( !k ) continue;
+                fprintf( pFile, "               " );
+                fprintf( pFile, "%d : %s = ", k-1, Wln_ObjName(p, iObj) );
+                fprintf( pFile, "%s ;\n", Wln_ObjName(p, Wln_ObjFanin(p, iObj, k)) );
+            }
+            fprintf( pFile, "             " );
+            fprintf( pFile, "endcase\n" );
+            fprintf( pFile, "           " );
+            fprintf( pFile, "end\n" );
+            continue;
+        }
+        else if ( Wln_ObjType(p, iObj) == ABC_OPER_SEL_SEL )
+        {
+            fprintf( pFile, "%s ;\n", Wln_ObjName(p, iObj) );
+            fprintf( pFile, "         " );
+            fprintf( pFile, "always @( " );
+            Wln_ObjForEachFanin( p, iObj, iFanin, k )
+                fprintf( pFile, "%s%s", k ? " or ":"", Wln_ObjName(p, Wln_ObjFanin(p, iObj, k)) );
+            fprintf( pFile, " )\n" );
+            fprintf( pFile, "           " );
+            fprintf( pFile, "begin\n" );
+            fprintf( pFile, "             " );
+            fprintf( pFile, "case ( %s )\n", Wln_ObjName(p, Wln_ObjFanin(p, iObj, 0)) );
+            Wln_ObjForEachFanin( p, iObj, iFanin, k )
+            {
+                if ( !k ) continue;
+                fprintf( pFile, "               " );
+                fprintf( pFile, "%d\'b", Wln_ObjFaninNum(p, iObj)-1 );
+                for ( j = Wln_ObjFaninNum(p, iObj)-1; j > 0; j-- )
+                    fprintf( pFile, "%d", (int)(j==k) );
+                fprintf( pFile, " : %s = ", Wln_ObjName(p, iObj) );
+                fprintf( pFile, "%s ;\n", Wln_ObjName(p, Wln_ObjFanin(p, iObj, k)) );
+            }
+            fprintf( pFile, "               " );
+            fprintf( pFile, "default" );
+            fprintf( pFile, " : %s = ", Wln_ObjName(p, iObj) );
+            fprintf( pFile, "%d\'b", Wln_ObjRange(p, iObj) );
+            for ( j = Wln_ObjRange(p, iObj)-1; j >= 0; j-- )
+                fprintf( pFile, "%d", 0 );
+            fprintf( pFile, " ;\n" );
+            fprintf( pFile, "             " );
+            fprintf( pFile, "endcase\n" );
+            fprintf( pFile, "           " );
+            fprintf( pFile, "end\n" );
+            continue;
+        }
+        else if ( Wln_ObjType(p, iObj) == ABC_OPER_SEL_DEC )
+        {
+            int nRange = Wln_ObjRange(p, Wln_ObjFanin0(p, iObj));
+            assert( (1 << nRange) == Wln_ObjRange(p, iObj) );
+            fprintf( pFile, "%s ;\n", Wln_ObjName(p, iObj) );
+            for ( k = 0; k < Wln_ObjRange(p, iObj); k++ )
+            {
+                fprintf( pFile, "         " );
+                fprintf( pFile, "wire " );
+                fprintf( pFile, "%s_", Wln_ObjName(p, iObj) );
+                for ( j = 0; j < nRange; j++ )
+                    fprintf( pFile, "%d", (k >> (nRange-1-j)) & 1 );
+                fprintf( pFile, " = " );
+                for ( j = 0; j < nRange; j++ )
+                    fprintf( pFile, "%s%s%s[%d]", 
+                        j ? " & ":"", ((k >> (nRange-1-j)) & 1) ? " ":"~", 
+                        Wln_ObjName(p, Wln_ObjFanin(p, iObj, 0)), nRange-1-j );
+                fprintf( pFile, " ;\n" );
+            }
+            fprintf( pFile, "         " );
+            fprintf( pFile, "assign %s = { ", Wln_ObjName(p, iObj) );
+            for ( k = Wln_ObjRange(p, iObj)-1; k >= 0; k-- )
+            {
+                fprintf( pFile, "%s%s_", k < Wln_ObjRange(p, iObj)-1 ? ", ":"", Wln_ObjName(p, iObj) );
+                for ( j = 0; j < nRange; j++ )
+                    fprintf( pFile, "%d", (k >> (nRange-1-j)) & 1 );
+            }
+            fprintf( pFile, " } ;\n" );
+            continue;
+        }
+        else if ( Wln_ObjType(p, iObj) == ABC_OPER_ARI_ADDSUB )
+        {
+            // out = mode ? a+b+cin : a-b-cin
+            fprintf( pFile, "%s ;\n", Wln_ObjName(p, iObj) );
+            fprintf( pFile, "         " );
+            fprintf( pFile, "assign " );
+            fprintf( pFile, "%s = %s ? %s + %s + %s : %s - %s - %s ;\n", 
+                        Wln_ObjName(p, iObj), Wln_ObjName(p, Wln_ObjFanin0(p, iObj)),
+                        Wln_ObjName(p, Wln_ObjFanin2(p, iObj)), Wln_ObjName(p, Wln_ObjFanin(p, iObj,3)), Wln_ObjName(p, Wln_ObjFanin1(p, iObj)),
+                        Wln_ObjName(p, Wln_ObjFanin2(p, iObj)), Wln_ObjName(p, Wln_ObjFanin(p, iObj,3)), Wln_ObjName(p, Wln_ObjFanin1(p, iObj)) 
+                   );
+            continue;
+        }
+        else if ( Wln_ObjType(p, iObj) == ABC_OPER_RAMR || Wln_ObjType(p, iObj) == ABC_OPER_RAMW )
+        {
+            if ( 1 )
+            {
+                fprintf( pFile, "%s ;\n", Wln_ObjName(p, iObj) );
+                fprintf( pFile, "         " );
+                fprintf( pFile, "%s (", Wln_ObjType(p, iObj) == ABC_OPER_RAMR ? "ABC_READ" : "ABC_WRITE" );
+                Wln_ObjForEachFanin( p, iObj, iFanin, k )
+                    fprintf( pFile, " .%s(%s),", k==0 ? "mem_in" : (k==1 ? "addr": "data"), Wln_ObjName(p, iFanin) );
+                fprintf( pFile, " .%s(%s) ) ;\n", Wln_ObjType(p, iObj) == ABC_OPER_RAMR ? "data" : "mem_out", Wln_ObjName(p, iObj) );
+                continue;
+            }
+            else
+            {
+                int nBitsMem  = Wln_ObjRange(p,  Wln_ObjFanin(p, iObj, 0) );
+                //int nBitsAddr = Wln_ObjRange(p,  Wln_ObjFanin(p, iObj, 1) );
+                int nBitsDat  = Wln_ObjType(p, iObj) == ABC_OPER_RAMR ? Wln_ObjRange(p, iObj) : Wln_ObjRange(p, Wln_ObjFanin(p, iObj, 2));
+                int Depth     = nBitsMem / nBitsDat;
+                assert( nBitsMem % nBitsDat == 0 );
+                fprintf( pFile, "%s ;\n", Wln_ObjName(p, iObj) );
+                fprintf( pFile, "         " );
+                fprintf( pFile, "%s_%d (", Wln_ObjType(p, iObj) == ABC_OPER_RAMR ? "CPL_MEM_READ" : "CPL_MEM_WRITE", Depth );
+                Wln_ObjForEachFanin( p, iObj, iFanin, k )
+                    fprintf( pFile, " .%s(%s),", k==0 ? "mem_data_in" : (k==1 ? "addr_in": "data_in"), Wln_ObjName(p, iFanin) );
+                fprintf( pFile, " .%s(%s) ) ;\n", "data_out", Wln_ObjName(p, iObj) );
+                continue;
+            }
+        }
+        else if ( Wln_ObjType(p, iObj) == ABC_OPER_DFFRSE )
+        {
+            fprintf( pFile, "%s ;\n", Wln_ObjName(p, iObj) );
+            continue;
+        }
+        else 
+        {
+            fprintf( pFile, "%-16s = ", Wln_ObjName(p, iObj) );
+            if ( Wln_ObjType(p, iObj) == ABC_OPER_BIT_BUF )
+                fprintf( pFile, "%s", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_BIT_MUX )
+            {
+                fprintf( pFile, "%s ? ", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+                fprintf( pFile, "%s : ", Wln_ObjName(p, Wln_ObjFanin1(p, iObj)) );
+                fprintf( pFile, "%s",    Wln_ObjName(p, Wln_ObjFanin2(p, iObj)) );
+            }
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_ARI_MIN )
+                fprintf( pFile, "-%s", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_BIT_INV )
+                fprintf( pFile, "~%s", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_LOGIC_NOT )
+                fprintf( pFile, "!%s", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_RED_AND )
+                fprintf( pFile, "&%s", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_RED_OR )
+                fprintf( pFile, "|%s", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_RED_XOR )
+                fprintf( pFile, "^%s", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_RED_NAND )
+                fprintf( pFile, "~&%s", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_RED_NOR )
+                fprintf( pFile, "~|%s", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_RED_NXOR )
+                fprintf( pFile, "~^%s", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_SLICE )
+                fprintf( pFile, "%s [%d:%d]", Wln_ObjName(p, Wln_ObjFanin0(p, iObj)), Wln_ObjRangeEnd(p, iObj), Wln_ObjRangeBeg(p, iObj) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_SIGNEXT )
+                fprintf( pFile, "{ {%d{%s[%d]}}, %s }", Wln_ObjRange(p, iObj) - Wln_ObjRange(p, Wln_ObjFanin0(p, iObj)), Wln_ObjName(p, Wln_ObjFanin0(p, iObj)), Wln_ObjRange(p, Wln_ObjFanin0(p, iObj)) - 1, Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_ZEROPAD )
+                fprintf( pFile, "{ {%d{1\'b0}}, %s }", Wln_ObjRange(p, iObj) - Wln_ObjRange(p, Wln_ObjFanin0(p, iObj)), Wln_ObjName(p, Wln_ObjFanin0(p, iObj)) );
+            else if ( Wln_ObjType(p, iObj) == ABC_OPER_CONCAT )
+            {
+                fprintf( pFile, "{" );
+                Wln_ObjForEachFanin( p, iObj, iFanin, k )
+                    fprintf( pFile, " %s%s", Wln_ObjName(p, Wln_ObjFanin(p, iObj, k)), k == Wln_ObjFaninNum(p, iObj)-1 ? "":"," );
+                fprintf( pFile, " }" );
+            }
+            else
+            {
+                fprintf( pFile, "%s ", Wln_ObjName(p, Wln_ObjFanin(p, iObj, 0)) );
+                if ( Wln_ObjType(p, iObj) == ABC_OPER_SHIFT_R )
+                    fprintf( pFile, ">>" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_SHIFT_RA )
+                    fprintf( pFile, ">>>" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_SHIFT_L )
+                    fprintf( pFile, "<<" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_SHIFT_LA )
+                    fprintf( pFile, "<<<" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_BIT_AND )
+                    fprintf( pFile, "&" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_BIT_OR )
+                    fprintf( pFile, "|" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_BIT_XOR )
+                    fprintf( pFile, "^" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_BIT_NAND )
+                    fprintf( pFile, "~&" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_BIT_NOR )
+                    fprintf( pFile, "~|" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_BIT_NXOR )
+                    fprintf( pFile, "~^" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_LOGIC_IMPL )
+                    fprintf( pFile, "=>" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_LOGIC_AND )
+                    fprintf( pFile, "&&" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_LOGIC_OR )
+                    fprintf( pFile, "||" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_LOGIC_XOR )
+                    fprintf( pFile, "^^" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_COMP_EQU )
+                    fprintf( pFile, "==" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_COMP_NOTEQU )
+                    fprintf( pFile, "!=" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_COMP_LESS )
+                    fprintf( pFile, "<" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_COMP_MORE )
+                    fprintf( pFile, ">" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_COMP_LESSEQU )
+                    fprintf( pFile, "<=" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_COMP_MOREEQU )
+                    fprintf( pFile, ">=" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_ARI_ADD )
+                    fprintf( pFile, "+" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_ARI_SUB )
+                    fprintf( pFile, "-" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_ARI_MUL )
+                    fprintf( pFile, "*" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_ARI_DIV )
+                    fprintf( pFile, "/" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_ARI_REM )
+                    fprintf( pFile, "%%" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_ARI_MOD )
+                    fprintf( pFile, "%%" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_ARI_POW )
+                    fprintf( pFile, "**" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_ARI_SQRT )
+                    fprintf( pFile, "@" );
+                else if ( Wln_ObjType(p, iObj) == ABC_OPER_ARI_SQUARE )
+                    fprintf( pFile, "#" );
+                else 
+                {
+                    //assert( 0 );
+                    printf( "Failed to write node \"%s\" with unknown operator type (%d).\n", Wln_ObjName(p, iObj), Wln_ObjType(p, iObj) );
+                    fprintf( pFile, "???\n" );
+                    continue;
+                }
+                fprintf( pFile, " %s", Wln_ObjName(p, Wln_ObjFanin(p, iObj, 1)) );
+                if ( Wln_ObjFaninNum(p, iObj) == 3 && Wln_ObjType(p, iObj) == ABC_OPER_ARI_ADD ) 
+                    fprintf( pFile, " + %s", Wln_ObjName(p, Wln_ObjFanin(p, iObj, 2)) );
+            }
+        }
+        fprintf( pFile, " ;%s\n", (p->fSmtLib && Wln_ObjIsSigned(p, iObj)) ? " // signed SMT-LIB operator" : "" );
+    }
+    iFanin = 0;
+    // write DFFs in the end
+    fprintf( pFile, "\n" );
+    Wln_NtkForEachFf( p, iObj, j )
+    {
+        char * pInNames[8] = {"d", "clk", "reset", "set", "enable", "async", "sre", "init"};
+        fprintf( pFile, "         " );
+        fprintf( pFile, "%s (", "ABC_DFFRSE" );
+        Wln_ObjForEachFanin( p, iObj, iFanin, k )
+            if ( iFanin ) fprintf( pFile, " .%s(%s),", pInNames[k], Wln_ObjName(p, iFanin) );
+        fprintf( pFile, " .%s(%s) ) ;\n", "q", Wln_ObjName(p, iObj) );
+    }
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "endmodule\n\n" );
+} 
+void Wln_WriteVer( Wln_Ntk_t * p, char * pFileName )
+{
+    FILE * pFile;
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Wln_WriteVer(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+    fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", p->pName, Extra_TimeStamp() );
+    fprintf( pFile, "\n" );
+    Wln_WriteTables( pFile, p );
+//    if ( fAddCos )
+//        Wln_WriteAddPos( p );
+    Wln_WriteVerInt( pFile, p );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+