Support for sequential designs in word-level Verilog.

5 files changed, 196 insertions, 79 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 8eecf8b2..a485873c 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -43,10 +43,10 @@ ABC_NAMESPACE_HEADER_START
 typedef enum { 
     WLC_OBJ_NONE = 0,      // 00: unknown
     WLC_OBJ_PI,            // 01: primary input 
-    WLC_OBJ_PO,            // 02: primary output 
-    WLC_OBJ_BO,            // 03: box output
-    WLC_OBJ_BI,            // 04: box input
-    WLC_OBJ_FF,            // 05: flop
+    WLC_OBJ_PO,            // 02: primary output (unused)
+    WLC_OBJ_FO,            // 03: flop output
+    WLC_OBJ_FI,            // 04: flop input (unused)
+    WLC_OBJ_FF,            // 05: flop (unused)
     WLC_OBJ_CONST,         // 06: constant
     WLC_OBJ_BUF,           // 07: buffer
     WLC_OBJ_MUX,           // 08: multiplexer
@@ -88,6 +88,10 @@ typedef enum {
 } Wlc_ObjType_t;
 
 
+// Unlike AIG managers and logic networks in ABC, this network treats POs and FIs 
+// as attributes of internal nodes and *not* as separate types of objects.
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -98,7 +102,9 @@ struct Wlc_Obj_t_ // 16 bytes
     unsigned               Type    :  6;       // node type
     unsigned               Signed  :  1;       // signed
     unsigned               Mark    :  1;       // user mark
-    unsigned               nFanins : 24;       // fanin count
+    unsigned               fIsPo   :  1;       // this is PO
+    unsigned               fIsFi   :  1;       // this is FI
+    unsigned               nFanins : 22;       // fanin count
     unsigned               End     : 16;       // range end
     unsigned               Beg     : 16;       // range begin
     union { int            Fanins[2];          // fanin IDs
@@ -138,7 +144,7 @@ static inline int          Wlc_NtkPiNum( Wlc_Ntk_t * p )
 static inline int          Wlc_NtkPoNum( Wlc_Ntk_t * p )                          { return Vec_IntSize(&p->vPos);                                         }
 static inline int          Wlc_NtkCiNum( Wlc_Ntk_t * p )                          { return Vec_IntSize(&p->vCis);                                         }
 static inline int          Wlc_NtkCoNum( Wlc_Ntk_t * p )                          { return Vec_IntSize(&p->vCos);                                         }
-static inline int          Wlc_NtkFfNum( Wlc_Ntk_t * p )                          { return Vec_IntSize(&p->vFfs);                                         }
+static inline int          Wlc_NtkFfNum( Wlc_Ntk_t * p )                          { return Vec_IntSize(&p->vCis) - Vec_IntSize(&p->vPis);                 }
 
 static inline Wlc_Obj_t *  Wlc_NtkObj( Wlc_Ntk_t * p, int Id )                    { assert(Id > 0 && Id < p->nObjsAlloc); return p->pObjs + Id;           }
 static inline Wlc_Obj_t *  Wlc_NtkPi( Wlc_Ntk_t * p, int i )                      { return Wlc_NtkObj( p, Vec_IntEntry(&p->vPis, i) );                    }
@@ -147,8 +153,13 @@ static inline Wlc_Obj_t *  Wlc_NtkCi( Wlc_Ntk_t * p, int i )
 static inline Wlc_Obj_t *  Wlc_NtkCo( Wlc_Ntk_t * p, int i )                      { return Wlc_NtkObj( p, Vec_IntEntry(&p->vCos, i) );                    }
 static inline Wlc_Obj_t *  Wlc_NtkFf( Wlc_Ntk_t * p, int i )                      { return Wlc_NtkObj( p, Vec_IntEntry(&p->vFfs, i) );                    }
 
+static inline int          Wlc_ObjIsPi( Wlc_Obj_t * p )                           { return p->Type == WLC_OBJ_PI;                                         }
+static inline int          Wlc_ObjIsPo( Wlc_Obj_t * p )                           { return p->fIsPo;                                                      }
+static inline int          Wlc_ObjIsCi( Wlc_Obj_t * p )                           { return p->Type == WLC_OBJ_PI || p->Type == WLC_OBJ_FO;                }
+static inline int          Wlc_ObjIsCo( Wlc_Obj_t * p )                           { return p->fIsPo || p->fIsFi;                                          }
+
 static inline int          Wlc_ObjId( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )           { return pObj - p->pObjs;                                               }
-static inline int          Wlc_ObjPioId( Wlc_Obj_t * p )                          { assert(p->Type==WLC_OBJ_PI||p->Type==WLC_OBJ_PO);return p->Fanins[1]; }
+static inline int          Wlc_ObjCiId( Wlc_Obj_t * p )                           { assert( Wlc_ObjIsCi(p) ); return p->Fanins[1];                        }
 static inline int          Wlc_ObjFaninNum( Wlc_Obj_t * p )                       { return p->nFanins;                                                    }
 static inline int          Wlc_ObjHasArray( Wlc_Obj_t * p )                       { return p->nFanins > 2 || p->Type == WLC_OBJ_CONST;                    }
 static inline int *        Wlc_ObjFanins( Wlc_Obj_t * p )                         { return Wlc_ObjHasArray(p) ? p->pFanins[0] : p->Fanins;                }
@@ -174,12 +185,15 @@ static inline void         Wlc_NtkCleanCopy( Wlc_Ntk_t * p )
 static inline int          Wlc_NtkHasCopy( Wlc_Ntk_t * p )                        { return Vec_IntSize( &p->vCopies ) > 0;                                }
 static inline void         Wlc_ObjSetCopy( Wlc_Ntk_t * p, int iObj, int i )       { Vec_IntWriteEntry( &p->vCopies, iObj, i );                            }
 static inline int          Wlc_ObjCopy( Wlc_Ntk_t * p, int iObj )                 { return Vec_IntEntry( &p->vCopies, iObj );                             }
+static inline Wlc_Obj_t *  Wlc_ObjCopyObj(Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj) {return Wlc_NtkObj(pNew, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)));}
 
 static inline void         Wlc_NtkCleanNameId( Wlc_Ntk_t * p )                    { Vec_IntFill( &p->vNameIds, p->nObjsAlloc, 0 );                        }
 static inline int          Wlc_NtkHasNameId( Wlc_Ntk_t * p )                      { return Vec_IntSize( &p->vNameIds ) > 0;                               }
 static inline void         Wlc_ObjSetNameId( Wlc_Ntk_t * p, int iObj, int i )     { Vec_IntWriteEntry( &p->vNameIds, iObj, i );                           }
 static inline int          Wlc_ObjNameId( Wlc_Ntk_t * p, int iObj )               { return Vec_IntEntry( &p->vNameIds, iObj );                            }
 
+static inline Wlc_Obj_t *  Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )       { assert( pObj->Type == WLC_OBJ_FO ); return Wlc_NtkCo(p, Wlc_NtkCoNum(p) - Wlc_NtkCiNum(p) + Wlc_ObjCiId(pObj)); } 
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -198,6 +212,8 @@ static inline int          Wlc_ObjNameId( Wlc_Ntk_t * p, int iObj )
     for ( i = 0; (i < Wlc_NtkCiNum(p)) && (((pCi) = Wlc_NtkCi(p, i)), 1); i++ )
 #define Wlc_NtkForEachCo( p, pCo, i )                                               \
     for ( i = 0; (i < Wlc_NtkCoNum(p)) && (((pCo) = Wlc_NtkCo(p, i)), 1); i++ )
+#define Wlc_NtkForEachFf( p, pFf, i )                                               \
+    for ( i = 0; (i < Vec_IntSize(&p->vFfs)) && (((pFf) = Wlc_NtkFf(p, i)), 1); i++ )
 
 #define Wlc_ObjForEachFanin( pObj, iFanin, i )                                      \
     for ( i = 0; (i < Wlc_ObjFaninNum(pObj)) && (((iFanin) = Wlc_ObjFaninId(pObj, i)), 1); i++ )
@@ -214,6 +230,8 @@ extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p );
 /*=== wlcNtk.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_NtkAlloc( char * pName, int nObjsAlloc );
 extern int            Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg );
+extern void           Wlc_ObjSetCi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj );
+extern void           Wlc_ObjSetCo( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int fFlopInput );
 extern char *         Wlc_ObjName( Wlc_Ntk_t * p, int iObj );
 extern void           Wlc_ObjUpdateType( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int Type );
 extern void           Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 538154c4..36175020 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -343,6 +343,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
     int nBits = Wlc_NtkPrepareBits( p );
     int nRange, nRange0, nRange1, nRange2;
     int i, k, b, iFanin, iLit, * pFans0, * pFans1, * pFans2;
+    int nFFins = 0, nFFouts = 0;
     vBits  = Vec_IntAlloc( nBits );
     vTemp0 = Vec_IntAlloc( 1000 );
     vTemp1 = Vec_IntAlloc( 1000 );
@@ -357,8 +358,8 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
     // create primary inputs
     Wlc_NtkForEachObj( p, pObj, i )
     {
-        int nAndPrev = Gia_ManObjNum(pNew);
 //        char * pName = Wlc_ObjName(p, i);
+        int nAndPrev = Gia_ManAndNum(pNew);
         nRange  = Wlc_ObjRange( pObj );
         nRange0 = Wlc_ObjFaninNum(pObj) > 0 ? Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) ) : -1;
         nRange1 = Wlc_ObjFaninNum(pObj) > 1 ? Wlc_ObjRange( Wlc_ObjFanin1(p, pObj) ) : -1;
@@ -367,14 +368,16 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
         pFans1  = Wlc_ObjFaninNum(pObj) > 1 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId1(pObj)) ) : NULL;
         pFans2  = Wlc_ObjFaninNum(pObj) > 2 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId2(pObj)) ) : NULL;
         Vec_IntClear( vRes );
-        if ( pObj->Type == WLC_OBJ_PI )
+        if ( Wlc_ObjIsCi(pObj) )
         {
             for ( k = 0; k < nRange; k++ )
                 Vec_IntPush( vRes, Gia_ManAppendCi(pNew) );
+            if ( pObj->Type == WLC_OBJ_FO )
+                nFFouts += Vec_IntSize(vRes);
         }
-        else if ( pObj->Type == WLC_OBJ_PO || pObj->Type == WLC_OBJ_BUF )
+        else if ( pObj->Type == WLC_OBJ_BUF )
         {
-            if ( pObj->Type == WLC_OBJ_BUF && pObj->Signed && !Wlc_ObjFanin0(p, pObj)->Signed ) // unsign->sign
+            if ( pObj->Signed && !Wlc_ObjFanin0(p, pObj)->Signed ) // unsign->sign
             {
                 int nRangeMax = Abc_MaxInt( nRange0, nRange );
                 int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, 0 );
@@ -533,19 +536,23 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
             Vec_IntPush( vRes, Wlc_BlastReduction( pNew, pFans0, nRange, pObj->Type ) );
         else if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB ) 
         {
-            int * pArg0 = Wlc_VecLoadFanins( vRes,   pFans0, nRange0, nRange, Wlc_ObjFanin0(p, pObj)->Signed );
-            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRange, Wlc_ObjFanin1(p, pObj)->Signed );
+            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
+            int * pArg0 = Wlc_VecLoadFanins( vRes,   pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed );
+            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjFanin1(p, pObj)->Signed );
             if ( pObj->Type == WLC_OBJ_ARI_ADD )
                 Wlc_BlastAdder( pNew, pArg0, pArg1, nRange ); // result is in pFan0 (vRes)
             else 
                 Wlc_BlastSubtract( pNew, pArg0, pArg1, nRange ); // result is in pFan0 (vRes)
+            Vec_IntShrink( vRes, nRange );
         }
         else if ( pObj->Type == WLC_OBJ_ARI_MULTI )
         {
-            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRange, Wlc_ObjFanin0(p, pObj)->Signed );
-            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRange, Wlc_ObjFanin1(p, pObj)->Signed );
+            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
+            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed );
+            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjFanin1(p, pObj)->Signed );
             assert( nRange0 <= nRange && nRange1 <= nRange );
             Wlc_BlastMultiplier( pNew, pArg0, pArg1, nRange, vTemp2, vRes );
+            Vec_IntShrink( vRes, nRange );
         }
         else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_MODULUS )
         {
@@ -567,8 +574,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
         assert( Vec_IntSize(vBits) == Wlc_ObjCopy(p, i) );
         Vec_IntAppend( vBits, vRes );
         pPrev = pObj;
-        if ( pObj->Type != WLC_OBJ_PI && pObj->Type != WLC_OBJ_PO )
-            p->nAnds[pObj->Type] += Gia_ManObjNum(pNew) - nAndPrev;
+        p->nAnds[pObj->Type] += Gia_ManAndNum(pNew) - nAndPrev;
     }
     p->nAnds[0] = Gia_ManAndNum(pNew);
     assert( nBits == Vec_IntSize(vBits) );
@@ -576,18 +582,21 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
     Vec_IntFree( vTemp1 );
     Vec_IntFree( vTemp2 );
     Vec_IntFree( vRes );
-    // create POs
-    Wlc_NtkForEachPo( p, pObj, i )
+    // create COs
+    Wlc_NtkForEachCo( p, pObj, i )
     {
         nRange = Wlc_ObjRange( pObj );
-        nRange0 = Wlc_ObjFaninNum(pObj) > 0 ? Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) ) : -1;
-        assert( nRange == nRange0 );
         pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) );
         for ( k = 0; k < nRange; k++ )
             Gia_ManAppendCo( pNew, pFans0[k] );
+        if ( pObj->fIsFi )
+            nFFins += nRange;
     }
     Vec_IntFree( vBits );
     Vec_IntErase( &p->vCopies );
+    // set the number of registers
+    assert( nFFins == nFFouts );
+    Gia_ManSetRegNum( pNew, nFFins );
     // finalize and cleanup
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index a70327a6..933e9585 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -107,9 +107,30 @@ Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc )
     p->iObj = 1;
     return p;
 }
+void Wlc_ObjSetCi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
+{
+    assert( Wlc_ObjIsCi(pObj) );
+    assert( Wlc_ObjFaninNum(pObj) == 0 );
+    pObj->Fanins[1] = Vec_IntSize(&p->vCis);
+    Vec_IntPush( &p->vCis, Wlc_ObjId(p, pObj) );
+    if ( pObj->Type == WLC_OBJ_PI )
+        Vec_IntPush( &p->vPis, Wlc_ObjId(p, pObj) );
+}
+void Wlc_ObjSetCo( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int fFlopInput )
+{
+//    pObj->Fanins[1] = Vec_IntSize(&p->vCos);
+    Vec_IntPush( &p->vCos, Wlc_ObjId(p, pObj) );
+    if ( !fFlopInput )
+        Vec_IntPush( &p->vPos, Wlc_ObjId(p, pObj) );
+    if ( fFlopInput )
+        pObj->fIsFi = 1;
+    else
+        pObj->fIsPo = 1;
+}
 int Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg )
 {
     Wlc_Obj_t * pObj;
+    assert( Type != WLC_OBJ_PO && Type != WLC_OBJ_FI );
     if ( p->iObj == p->nObjsAlloc )
     {
         p->pObjs = ABC_REALLOC( Wlc_Obj_t, p->pObjs, 2 * p->nObjsAlloc );
@@ -121,16 +142,8 @@ int Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg )
     pObj->Signed = Signed;
     pObj->End    = End;
     pObj->Beg    = Beg;
-    if ( Type == WLC_OBJ_PI )
-    {
-        pObj->Fanins[1] = Vec_IntSize(&p->vPis);
-        Vec_IntPush( &p->vPis, p->iObj );
-    }
-    else if ( Type == WLC_OBJ_PO )
-    {
-        pObj->Fanins[1] = Vec_IntSize(&p->vPos);
-        Vec_IntPush( &p->vPos, p->iObj );
-    }
+    if ( Wlc_ObjIsCi(pObj) )
+        Wlc_ObjSetCi( p, pObj );
     p->nObjs[Type]++;
     return p->iObj++;
 }
@@ -144,13 +157,7 @@ char * Wlc_ObjName( Wlc_Ntk_t * p, int iObj )
 }                          
 void Wlc_ObjUpdateType( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int Type )
 {
-    if ( pObj->Type == WLC_OBJ_PO )
-    {
-//        if ( Type != WLC_OBJ_BUF )
-//            printf( "Primary outputs should be driven by buffers.\n" );
-        assert( Type == WLC_OBJ_BUF );
-        return;
-    }
+    assert( pObj->Type == WLC_OBJ_NONE );
     p->nObjs[pObj->Type]--;
     pObj->Type = Type;
     p->nObjs[pObj->Type]++;
@@ -274,20 +281,18 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
     Wlc_NtkForEachObj( p, pObj, i )
     {
 //        char * pName = Wlc_ObjName(p, i);
-//        if ( pObj->Type == WLC_OBJ_ARI_MULTI )
         if ( Wlc_ObjSign(pObj) > 0x1FFFFF )
             printf( "Object %6d has range %d, which is reduced to %d in the statistics.\n", 
                 i, Wlc_ObjRange(pObj), Wlc_ObjRange(pObj) & 0xFFFFF );
         if ( pObj->Beg )
             printf( "Object %6d has non-standard range %d=[%d:%d]\n", i, Wlc_ObjRange(pObj), pObj->End, pObj->Beg );
        // 0-input types
-        if ( pObj->Type == WLC_OBJ_PI || pObj->Type == WLC_OBJ_CONST || pObj->Type == WLC_OBJ_BIT_CONCAT )
+        if ( Wlc_ObjIsCi(pObj) || pObj->Type == WLC_OBJ_CONST || pObj->Type == WLC_OBJ_BIT_CONCAT )
             Sign = Wlc_NtkPrintDistribMakeSign( Wlc_ObjSign(pObj), 0, 0 );
         // 1-input types
-        else if ( pObj->Type == WLC_OBJ_BUF    || pObj->Type == WLC_OBJ_PO          || pObj->Type == WLC_OBJ_BI ||
+        else if ( pObj->Type == WLC_OBJ_BUF    || pObj->Type == WLC_OBJ_BIT_SELECT  || pObj->Type == WLC_OBJ_TABLE ||
              pObj->Type == WLC_OBJ_BIT_ZEROPAD || pObj->Type == WLC_OBJ_BIT_SIGNEXT || 
-             pObj->Type == WLC_OBJ_BIT_NOT     || pObj->Type == WLC_OBJ_LOGIC_NOT   || pObj->Type == WLC_OBJ_ARI_MINUS || 
-             pObj->Type == WLC_OBJ_BIT_SELECT  || pObj->Type == WLC_OBJ_TABLE )
+             pObj->Type == WLC_OBJ_BIT_NOT     || pObj->Type == WLC_OBJ_LOGIC_NOT   || pObj->Type == WLC_OBJ_ARI_MINUS )
             Sign = Wlc_NtkPrintDistribMakeSign( Wlc_ObjSign(pObj), Wlc_ObjSign(Wlc_ObjFanin0(p, pObj)), 0 );
         // 2-input types (including MUX)
         else 
@@ -296,7 +301,7 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
         Wlc_NtkPrintDistribAddOne( vTypes, vOccurs, pObj->Type, Sign );
     }
     // print by occurrence
-    printf( "Format: type ID : occurance  name ... (occurrence)<output_range>=<input_range>.<input_range>\n" );
+    printf( "ID  :  name  occurrence (occurrence)<output_range>=<input_range>.<input_range> ...\n" );
     for ( i = 0; i < WLC_OBJ_NUMBER; i++ )
     {
         Vec_Wrd_t * vType  = (Vec_Wrd_t *)Vec_PtrEntry( vTypes, i );
@@ -436,12 +441,12 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p )
     Wlc_NtkCleanCopy( p );
     vFanins = Vec_IntAlloc( 100 );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
-    Wlc_NtkForEachPi( p, pObj, i )
-        Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
-    Wlc_NtkForEachPo( p, pObj, i )
-        Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjFaninId0(pObj), vFanins );
-    Wlc_NtkForEachPo( p, pObj, i )
+    Wlc_NtkForEachCi( p, pObj, i )
         Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+    Wlc_NtkForEachCo( p, pObj, i )
+        Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+    Wlc_NtkForEachCo( p, pObj, i )
+        Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
     Vec_IntFree( vFanins );
     return pNew;
 }
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index f943337c..63d5c19a 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -658,11 +658,11 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t *
 int Wlc_PrsReadDeclaration( Wlc_Prs_t * p, char * pStart )
 {
     int fFound = 0, Type = WLC_OBJ_NONE, iObj; 
-    int Signed = 0, Beg = 0, End = 0, NameId;
+    int Signed = 0, Beg = 0, End = 0, NameId, fIsPo = 0;
     if ( Wlc_PrsStrCmp( pStart, "input" ) )
-        Type = WLC_OBJ_PI, pStart += strlen("input");
+        pStart += strlen("input"), Type = WLC_OBJ_PI;
     else if ( Wlc_PrsStrCmp( pStart, "output" ) )
-        Type = WLC_OBJ_PO, pStart += strlen("output");
+        pStart += strlen("output"), fIsPo = 1;
     pStart = Wlc_PrsSkipSpaces( pStart );
     if ( Wlc_PrsStrCmp( pStart, "wire" ) )
         pStart += strlen("wire");
@@ -685,6 +685,7 @@ int Wlc_PrsReadDeclaration( Wlc_Prs_t * p, char * pStart )
         if ( fFound )
             return Wlc_PrsWriteErrorMessage( p, pStart, "Name %s is declared more than once.", pName );
         iObj = Wlc_ObjAlloc( p->pNtk, Type, Signed, End, Beg );
+        if ( fIsPo ) Wlc_ObjSetCo( p->pNtk, Wlc_NtkObj(p->pNtk, iObj), 0 );
         assert( iObj == NameId );
         // check next definition
         pStart = Wlc_PrsSkipSpaces( pStart );
@@ -707,6 +708,7 @@ int Wlc_PrsReadDeclaration( Wlc_Prs_t * p, char * pStart )
 }
 int Wlc_PrsDerive( Wlc_Prs_t * p )
 {
+    Wlc_Obj_t * pObj;
     char * pStart, * pName;
     int i;
     // go through the directives
@@ -719,9 +721,21 @@ startword:
             pName = strtok( pStart + strlen("module"), " \r\n\t(,)" );
             if ( pName == NULL )
                 return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read model name." );
+            // THIS IS A HACK to skip definitions of modules beginning with "CPL_"
+            if ( Wlc_PrsStrCmp( pName, "CPL_" ) )
+            {
+                while ( ++i < Vec_IntSize(p->vStarts) )
+                {
+                    pStart = Wlc_PrsStr(p, Vec_IntEntry(p->vStarts, i));
+                    pStart = strstr( pStart, "endmodule" );
+                    if ( pStart != NULL )
+                        break;
+                }
+                continue;
+            }
             if ( Wlc_PrsStrCmp( pName, "table" ) )
             {
-                // THIS IS A HACK TO DETECT tables
+                // THIS IS A HACK to detect table module descriptions
                 int Width1 = -1, Width2 = -1;
                 int v, b, Value, nBits, nInts;
                 unsigned * pTable;
@@ -784,6 +798,14 @@ startword:
             Vec_Int_t * vTemp = Vec_IntStartNatural( Wlc_NtkObjNumMax(p->pNtk) );
             Vec_IntAppend( &p->pNtk->vNameIds, vTemp );
             Vec_IntFree( vTemp );
+            // move FO/FI to be part of CI/CO
+            assert( (Vec_IntSize(&p->pNtk->vFfs) & 1) == 0 );
+            Wlc_NtkForEachFf( p->pNtk, pObj, i )
+                if ( i & 1 )
+                    Wlc_ObjSetCo( p->pNtk, pObj, 1 );
+                else
+                    Wlc_ObjSetCi( p->pNtk, pObj );
+            Vec_IntClear( &p->pNtk->vFfs );
             break;
         }
         // these are read as part of the interface
@@ -807,7 +829,7 @@ startword:
             Type = Wlc_PrsFindDefinition( p, pStart, p->vFanins );
             if ( Type )
             {
-                Wlc_Obj_t * pObj = Wlc_NtkObj( p->pNtk, NameId );
+                pObj = Wlc_NtkObj( p->pNtk, NameId );
                 Wlc_ObjUpdateType( p->pNtk, pObj, Type );
                 Wlc_ObjAddFanins( p->pNtk, pObj, p->vFanins );
             }
@@ -816,7 +838,7 @@ startword:
         }
         else if ( Wlc_PrsStrCmp( pStart, "table" ) )
         {
-            // THIS IS A HACK TO DETECT tables
+            // THIS IS A HACK to detect tables
             int NameId, fFound, iTable = atoi( pStart + strlen("table") );
             // find opening
             pStart = Wlc_PrsFindSymbol( pStart, '(' );
@@ -844,15 +866,13 @@ startword:
             NameId = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
             if ( !fFound )
                 return Wlc_PrsWriteErrorMessage( p, pStart, "Name %s is not declared.", pName );
-            {
-                Wlc_Obj_t * pObj = Wlc_NtkObj( p->pNtk, NameId );
-                Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_TABLE );
-                Wlc_ObjAddFanins( p->pNtk, pObj, p->vFanins );
-            }
+            pObj = Wlc_NtkObj( p->pNtk, NameId );
+            Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_TABLE );
+            Wlc_ObjAddFanins( p->pNtk, pObj, p->vFanins );
         }
         else if ( Wlc_PrsStrCmp( pStart, "always" ) )
         {
-            // THIS IS A HACK TO DETECT tables
+            // THIS IS A HACK to detect always statement representing combinational MUX
             int NameId, NameIdOut = -1, fFound;
             // find control
             pStart = Wlc_PrsFindWord( pStart, "case", &fFound );
@@ -918,18 +938,58 @@ startword:
                 break;
             }
             // check range of the control
+            pObj = Wlc_NtkObj( p->pNtk, Vec_IntEntry(p->vFanins, 0) );
+            if ( (1 << Wlc_ObjRange(pObj)) != Vec_IntSize(p->vFanins) - 1 )
+                return Wlc_PrsWriteErrorMessage( p, pStart, "The number of values in the case statement is wrong.", pName );
+            pObj = Wlc_NtkObj( p->pNtk, NameIdOut );
+            Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_MUX );
+            Wlc_ObjAddFanins( p->pNtk, pObj, p->vFanins );
+            goto startword;
+        }
+        else if ( Wlc_PrsStrCmp( pStart, "CPL_FF" ) )
+        {
+            int NameId = -1, NameIdOut = -1, fFound, nBits = 1, fFlopOut;
+            pStart += strlen("CPL_FF");
+            if ( pStart[0] == '#' )
+                nBits = atoi(pStart+1);
+            // read names
+            while ( 1 )
             {
-                Wlc_Obj_t * pObj = Wlc_NtkObj( p->pNtk, Vec_IntEntry(p->vFanins, 0) );
-                if ( (1 << Wlc_ObjRange(pObj)) != Vec_IntSize(p->vFanins) - 1 )
-                    return Wlc_PrsWriteErrorMessage( p, pStart, "The number of values in the case statement is wrong.", pName );
-                pObj = Wlc_NtkObj( p->pNtk, NameIdOut );
-                Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_MUX );
-                Wlc_ObjAddFanins( p->pNtk, pObj, p->vFanins );
-                goto startword;
+                pStart = Wlc_PrsFindSymbol( pStart, '.' );
+                if ( pStart == NULL )
+                    break;
+                pStart = Wlc_PrsSkipSpaces( pStart+1 );
+                if ( pStart[0] != 'd' && (pStart[0] != 'q' || pStart[1] == 'b') )
+                    continue;
+                fFlopOut = (pStart[0] == 'd');
+                pStart = Wlc_PrsFindSymbol( pStart, '(' );
+                if ( pStart == NULL )
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read opening paranthesis in the flop description." );
+                pStart = Wlc_PrsFindName( pStart+1, &pName );
+                if ( pStart == NULL )
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read name inside flop description." );
+                if ( fFlopOut )
+                    NameIdOut = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                else 
+                    NameId = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                if ( !fFound )
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Name %s is not declared.", pName );
             }
+            if ( NameId == -1 || NameIdOut == -1 )
+                return Wlc_PrsWriteErrorMessage( p, pStart, "Name of flop input or flop output is missing." );
+            // create flop output
+            pObj = Wlc_NtkObj( p->pNtk, NameId );
+            Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_FO );
+            Vec_IntPush( &p->pNtk->vFfs, NameId );
+            if ( nBits != Wlc_ObjRange(pObj) )
+                printf( "Warning!  Flop input has bit-width (%d) that differs from the declaration (%d)\n", nBits, Wlc_ObjRange(pObj) );
+            // create flop input
+            pObj = Wlc_NtkObj( p->pNtk, NameIdOut );
+            Vec_IntPush( &p->pNtk->vFfs, NameIdOut );
+            if ( nBits != Wlc_ObjRange(pObj) )
+                printf( "Warning!  Flop output has bit-width (%d) that differs from the declaration (%d)\n", nBits, Wlc_ObjRange(pObj) );
         }
-//        else if ( Wlc_PrsStrCmp( pStart, "CPL_FF" ) )
-        else
+        else if ( pStart[0] != '`' )
         {
             pStart = Wlc_PrsFindName( pStart, &pName );
             return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read line beginning with %s.", pName );
diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c
index 6a615887..afc1f9ba 100644
--- a/src/base/wlc/wlcWriteVer.c
+++ b/src/base/wlc/wlcWriteVer.c
@@ -151,17 +151,21 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
         sprintf( Range, "%s[%d:%d]%*s", pObj->Signed ? "signed ":"       ", pObj->End, pObj->Beg, 8-nDigits, "" );
         fprintf( pFile, "  " );
         if ( pObj->Type == WLC_OBJ_PI )
-            fprintf( pFile, "input  wire %s %s", Range, pName );
-        else if ( pObj->Type == WLC_OBJ_PO )
-            fprintf( pFile, "output wire %s %-16s = %s", Range, pName, pName0 );
+            fprintf( pFile, "input  " );
+        else if ( pObj->fIsPo )
+            fprintf( pFile, "output " );
+        else
+            fprintf( pFile, "       " );
+        if ( Wlc_ObjIsCi(pObj) )
+            fprintf( pFile, "wire %s %s", Range, pName );
         else if ( pObj->Type == WLC_OBJ_TABLE )
         {
             // wire [3:0] s4972; table0 s4972_Index(s4971, s4972);
-            fprintf( pFile, "       wire %s %s ;              table%d s%d_Index(%s, %s)", Range, pName, Wlc_ObjTableId(pObj), i, pName0, pName );
+            fprintf( pFile, "wire %s %s ;              table%d s%d_Index(%s, %s)", Range, pName, Wlc_ObjTableId(pObj), i, pName0, pName );
         }
         else if ( pObj->Type == WLC_OBJ_CONST )
         {
-            fprintf( pFile, "       wire %s %-16s = %d\'%sh", Range, pName, Wlc_ObjRange(pObj), pObj->Signed ? "s":"" );
+            fprintf( pFile, "wire %s %-16s = %d\'%sh", Range, pName, Wlc_ObjRange(pObj), pObj->Signed ? "s":"" );
             Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pObj), (Wlc_ObjRange(pObj) + 3) / 4 );
         }
         else if ( pObj->Type == WLC_OBJ_ROTATE_R || pObj->Type == WLC_OBJ_ROTATE_L )
@@ -172,7 +176,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
             int Num1 = Wlc_ObjRange(pObj) - Num0;
             assert( pShift->Type == WLC_OBJ_CONST );
             assert( Num0 > 0 && Num0 < Wlc_ObjRange(pObj) );
-            fprintf( pFile, "       wire %s %-16s = ", Range, Wlc_ObjName(p, i) );
+            fprintf( pFile, "wire %s %-16s = ", Range, Wlc_ObjName(p, i) );
             if ( pObj->Type == WLC_OBJ_ROTATE_R )
                 fprintf( pFile, "(%s >> %d) | (%s << %d)", pName0, Num0, pName0, Num1 );
             else
@@ -180,7 +184,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
         }
         else if ( pObj->Type == WLC_OBJ_MUX && Wlc_ObjFaninNum(pObj) > 3 )
         {
-            fprintf( pFile, "       reg %s ;\n", pName );
+            fprintf( pFile, "reg %s ;\n", pName );
             fprintf( pFile, "       " );
             fprintf( pFile, "always @( " );
             Wlc_ObjForEachFanin( pObj, iFanin, k )
@@ -204,11 +208,11 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
         }
         else
         {
-            fprintf( pFile, "       wire %s %-16s = ", Range, Wlc_ObjName(p, i) );
+            fprintf( pFile, "wire %s %-16s = ", Range, Wlc_ObjName(p, i) );
             if ( pObj->Type == WLC_OBJ_BUF )
                 fprintf( pFile, "%s", pName0 );
             else if ( pObj->Type == WLC_OBJ_MUX )
-                fprintf( pFile, "%s ? %s : %s", pName0, Wlc_ObjName(p, Wlc_ObjFaninId1(pObj)), Wlc_ObjName(p, Wlc_ObjFaninId2(pObj)) );
+                fprintf( pFile, "%s ? %s : %s", pName0, Wlc_ObjName(p, Wlc_ObjFaninId2(pObj)), Wlc_ObjName(p, Wlc_ObjFaninId1(pObj)) );
             else if ( pObj->Type == WLC_OBJ_BIT_NOT )
                 fprintf( pFile, "~%s", pName0 );
             else if ( pObj->Type == WLC_OBJ_LOGIC_NOT )
@@ -283,6 +287,27 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
         }
         fprintf( pFile, " ;\n" );
     }
+    Wlc_NtkForEachCi( p, pObj, i )
+    {
+        char * pName  = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
+        assert( i == Wlc_ObjCiId(pObj) );
+        if ( pObj->Type == WLC_OBJ_PI )
+            continue;
+//  CPL_FF#9  I_32890_reg ( .q ( E_42304 )  , .qbar (  )  , .d ( E_42305 )  , .clk ( E_65040 )  ,
+//                .arst ( E_65037 )  , .arstval ( E_62126 )  );
+        fprintf( pFile, "         " );
+        fprintf( pFile, "CPL_FF" );
+        if ( Wlc_ObjRange(pObj) > 1 )
+            fprintf( pFile, "#%d", Wlc_ObjRange(pObj) );
+        fprintf( pFile, " %reg%d (",       i );
+        fprintf( pFile, " .q( %s ),",      pName );
+        fprintf( pFile, " .qbar()," );
+        fprintf( pFile, " .d( %s ),",      Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFoToFi(p, pObj))) );
+        fprintf( pFile, " .clk( %s ),",    "1\'b0" );
+        fprintf( pFile, " .arst( %s ),",   "1\'b0" );
+        fprintf( pFile, " .arstval( %s )", "1\'b0" );
+        fprintf( pFile, " ) ;\n" );
+    }
     fprintf( pFile, "endmodule\n\n" );
 } 
 void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName )