Updates to NDR format (flops, memories, signed mult, etc).

8 files changed, 352 insertions, 39 deletions

diff --git a/src/base/acb/acb.h b/src/base/acb/acb.h
index baecd161..76188f2e 100644
--- a/src/base/acb/acb.h
+++ b/src/base/acb/acb.h
@@ -237,7 +237,7 @@ static inline void           Acb_NtkFreeObjCnfs( Acb_Ntk_t * p )             { V
 
 static inline Acb_ObjType_t  Acb_ObjType( Acb_Ntk_t * p, int i )                     { assert(i>0); return (Acb_ObjType_t)(int)(unsigned char)Vec_StrEntry(&p->vObjType, i);                }
 static inline void           Acb_ObjCleanType( Acb_Ntk_t * p, int i )                { assert(i>0); Vec_StrWriteEntry( &p->vObjType, i, (char)ABC_OPER_NONE );                              }
-static inline int            Acb_TypeIsSeq( Acb_ObjType_t Type )                     { return Type >= ABC_OPER_RAM && Type <= ABC_OPER_DFFRS;                                               }
+static inline int            Acb_TypeIsSeq( Acb_ObjType_t Type )                     { return Type >= ABC_OPER_RAM && Type <= ABC_OPER_DFFLAST;                                             }
 static inline int            Acb_TypeIsUnary( Acb_ObjType_t Type )                   { return Type == ABC_OPER_BIT_BUF || Type == ABC_OPER_BIT_INV || Type == ABC_OPER_LOGIC_NOT || Type == ABC_OPER_ARI_MIN || Type == ABC_OPER_ARI_SQRT || Type == ABC_OPER_ARI_ABS || (Type >= ABC_OPER_RED_AND && Type <= ABC_OPER_RED_NXOR);  }
 static inline int            Acb_TypeIsMux( Acb_ObjType_t Type )                     { return Type == ABC_OPER_BIT_MUX || Type == ABC_OPER_SEL_NMUX || Type == ABC_OPER_SEL_SEL || Type == ABC_OPER_SEL_PSEL;  }
 
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 19eb4427..982a9d28 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -44,10 +44,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 (unused)
+    WLC_OBJ_PO,            // 02: primary output
     WLC_OBJ_FO,            // 03: flop output
     WLC_OBJ_FI,            // 04: flop input (unused)
-    WLC_OBJ_FF,            // 05: flop (unused)
+    WLC_OBJ_FF,            // 05: flop
     WLC_OBJ_CONST,         // 06: constant
     WLC_OBJ_BUF,           // 07: buffer
     WLC_OBJ_MUX,           // 08: multiplexer
@@ -98,7 +98,8 @@ typedef enum {
     WLC_OBJ_TABLE,         // 53: bit table
     WLC_OBJ_READ,          // 54: read port
     WLC_OBJ_WRITE,         // 55: write port
-    WLC_OBJ_NUMBER         // 56: unused
+    WLC_OBJ_ARI_ADDSUB,    // 56: adder-subtractor
+    WLC_OBJ_NUMBER         // 57: unused
 } Wlc_ObjType_t;
 // when adding new types, remember to update table Wlc_Names in "wlcNtk.c"
 
@@ -142,6 +143,8 @@ struct Wlc_Ntk_t_
     int                    nObjs[WLC_OBJ_NUMBER]; // counter of objects of each type
     int                    nAnds[WLC_OBJ_NUMBER]; // counter of AND gates after blasting
     int                    fSmtLib;            // the network comes from an SMT-LIB file
+    int                    fMemPorts;          // the network contains memory ports
+    int                    fEasyFfs;           // the network contains simple flops
     int                    nAssert;            // the number of asserts
     // memory for objects
     Wlc_Obj_t *            pObjs;
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index c934da27..9322a3c2 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -1642,7 +1642,7 @@ usage:
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
-    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    //Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -1658,11 +1658,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( pNtk == NULL )
-    {
-        Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
-        return 0;
-    }
+//    if ( pNtk == NULL )
+//    {
+//        Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
+//        return 0;
+//    }
+
     // transform
     //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
     //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
@@ -1671,9 +1672,9 @@ 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 );
-    //Wlc_ReadNdrTest( pNtk );
-    pNtk = Wlc_NtkMemAbstractTest( pNtk );
-    Wlc_AbcUpdateNtk( pAbc, pNtk );
+    Ndr_ModuleTestMemory();
+    //pNtk = Wlc_NtkMemAbstractTest( pNtk );
+    //Wlc_AbcUpdateNtk( pAbc, pNtk );
     return 0;
 usage:
     Abc_Print( -2, "usage: %%test [-vh]\n" );
diff --git a/src/base/wlc/wlcMem.c b/src/base/wlc/wlcMem.c
index ab0c0526..b310afb6 100644
--- a/src/base/wlc/wlcMem.c
+++ b/src/base/wlc/wlcMem.c
@@ -366,6 +366,8 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
     Wlc_NtkCleanCopy( p );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc + 1000 );
     pNew->fSmtLib = p->fSmtLib;
+    pNew->fMemPorts = p->fMemPorts;
+    pNew->fEasyFfs = p->fEasyFfs;
     pNew->vInits = Vec_IntAlloc( 100 );
 
     // duplicate PIs
diff --git a/src/base/wlc/wlcNdr.c b/src/base/wlc/wlcNdr.c
index ea754f08..75601ba8 100644
--- a/src/base/wlc/wlcNdr.c
+++ b/src/base/wlc/wlcNdr.c
@@ -91,6 +91,12 @@ int Ndr_TypeNdr2Wlc( int Type )
     if ( Type == ABC_OPER_ARI_MIN )       return WLC_OBJ_ARI_MINUS;     // 50: arithmetic minus
     if ( Type == ABC_OPER_ARI_SQRT )      return WLC_OBJ_ARI_SQRT;      // 51: integer square root
     if ( Type == ABC_OPER_ARI_SQUARE )    return WLC_OBJ_ARI_SQUARE;    // 52: integer square
+    if ( Type == ABC_OPER_ARI_ADDSUB )    return WLC_OBJ_ARI_ADDSUB;    // 56: adder-subtractor
+    if ( Type == ABC_OPER_ARI_SMUL )      return WLC_OBJ_ARI_MULTI;     // 45: signed multiplier
+    if ( Type == ABC_OPER_DFF )           return WLC_OBJ_FO;            // 03: flop
+    if ( Type == ABC_OPER_DFFRSE )        return WLC_OBJ_FF;            // 05: flop
+    if ( Type == ABC_OPER_RAMR )          return WLC_OBJ_READ;          // 54: read port
+    if ( Type == ABC_OPER_RAMW )          return WLC_OBJ_WRITE;         // 55: write port
     return -1;
 }
 int Ndr_TypeWlc2Ndr( int Type )
@@ -142,6 +148,12 @@ int Ndr_TypeWlc2Ndr( int Type )
     if ( Type == WLC_OBJ_ARI_MINUS )      return ABC_OPER_ARI_MIN;      // 50: arithmetic minus
     if ( Type == WLC_OBJ_ARI_SQRT )       return ABC_OPER_ARI_SQRT;     // 51: integer square root
     if ( Type == WLC_OBJ_ARI_SQUARE )     return ABC_OPER_ARI_SQUARE;   // 52: integer square
+    if ( Type == WLC_OBJ_ARI_ADDSUB )     return ABC_OPER_ARI_ADDSUB;   // 56: adder-subtractor
+    if ( Type == WLC_OBJ_ARI_MULTI )      return ABC_OPER_ARI_SMUL;     // 45: signed multiplier
+    if ( Type == WLC_OBJ_FO )             return ABC_OPER_DFF;          // 03: flop
+    if ( Type == WLC_OBJ_FF )             return ABC_OPER_DFFRSE;       // 05: flop
+    if ( Type == WLC_OBJ_READ )           return ABC_OPER_RAMR;         // 54: read port
+    if ( Type == WLC_OBJ_WRITE )          return ABC_OPER_RAMW;         // 55: write port
     return -1;
 }
 
@@ -337,6 +349,7 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
     int Mod = 2, i, k, Obj, * pArray, nDigits, fFound, NameId, NameIdMax;
     Wlc_Ntk_t * pTemp, * pNtk = Wlc_NtkAlloc( "top", Ndr_DataObjNum(p, Mod)+1 );
     Wlc_NtkCheckIntegrity( pData );
+    Vec_IntClear( &pNtk->vFfs );
     //pNtk->pSpec = Abc_UtilStrsav( pFileName );
     // construct network and save name IDs
     Wlc_NtkCleanNameId( pNtk );
@@ -357,6 +370,25 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
         int NameId  = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
         Vec_IntClear( vFanins );
         Vec_IntAppend( vFanins, vTemp );
+        if ( Type == ABC_OPER_DFF )
+        {
+            // save init state
+            if ( pNtk->vInits == NULL )
+                pNtk->vInits = Vec_IntAlloc( 100 );
+            if ( Vec_IntSize(vFanins) == 2 )
+                Vec_IntPush( pNtk->vInits, Vec_IntPop(vFanins) );
+            else // assume const0 if init is not given
+                Vec_IntPush( pNtk->vInits, -(End-Beg+1) );
+            // save flop output
+            pObj = Wlc_NtkObj(pNtk, iObj);
+            assert( Wlc_ObjType(pObj) == WLC_OBJ_FO );
+            Wlc_ObjSetNameId( pNtk, iObj, NameId );
+            Vec_IntPush( &pNtk->vFfs, NameId );
+            // save flop input
+            assert( Vec_IntSize(vFanins) == 1 );
+            Vec_IntPush( &pNtk->vFfs, Vec_IntEntry(vFanins, 0) );
+            continue;
+        }
         if ( Type == ABC_OPER_SLICE )
             Vec_IntPushTwo( vFanins, End, Beg );
         else if ( Type == ABC_OPER_CONST )
@@ -365,6 +397,13 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
             ABC_SWAP( int, Vec_IntEntryP(vFanins, 1)[0], Vec_IntEntryP(vFanins, 2)[0] );
         Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
         Wlc_ObjSetNameId( pNtk, iObj, NameId );
+        if ( Type == ABC_OPER_ARI_SMUL )
+        {
+            pObj = Wlc_NtkObj(pNtk, iObj);
+            assert( Wlc_ObjFaninNum(pObj) == 2 );
+            Wlc_ObjFanin0(pNtk, pObj)->Signed = 1;
+            Wlc_ObjFanin1(pNtk, pObj)->Signed = 1;
+        }
     }
     // mark primary outputs
     Ndr_ModForEachPo( p, Mod, Obj )
@@ -388,6 +427,27 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
         for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ )
             pFanins[k] = Vec_IntEntry(vName2Obj, pFanins[k]);
     }
+    if ( pNtk->vInits )
+    {
+        Vec_IntForEachEntry( &pNtk->vFfs, NameId, i )
+            Vec_IntWriteEntry( &pNtk->vFfs, i, Vec_IntEntry(vName2Obj, NameId) );
+        Vec_IntForEachEntry( pNtk->vInits, NameId, i )
+            if ( NameId > 0 )
+                Vec_IntWriteEntry( pNtk->vInits, i, Vec_IntEntry(vName2Obj, NameId) );
+        // move FO/FI to be part of CI/CO
+        assert( (Vec_IntSize(&pNtk->vFfs) & 1) == 0 );
+        assert( Vec_IntSize(&pNtk->vFfs) == 2 * Vec_IntSize(pNtk->vInits) );
+        Wlc_NtkForEachFf( pNtk, pObj, i )
+            if ( i & 1 )
+                Wlc_ObjSetCo( pNtk, pObj, 1 );
+            //else
+            //    Wlc_ObjSetCi( pNtk, pObj );
+        Vec_IntClear( &pNtk->vFfs );
+        // convert init values into binary string
+        //Vec_IntPrint( &p->pNtk->vInits );
+        pNtk->pInits = Wlc_PrsConvertInitValues( pNtk );
+        //printf( "%s", p->pNtk->pInits );
+    }
     Vec_IntFree(vName2Obj);
     // create fake object names
     NameIdMax = Vec_IntFindMax(&pNtk->vNameIds);
@@ -395,14 +455,17 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
     pNtk->pManName = Abc_NamStart( NameIdMax+1, 10 );
     for ( i = 1; i <= NameIdMax; i++ )
     {
-        char pName[20]; sprintf( pName, "n%0*d", nDigits, i );
+        char pName[20]; sprintf( pName, "s%0*d", nDigits, i );
         NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
         assert( !fFound && i == NameId );
     }
+    //Ndr_NtkPrintNodes( pNtk );
     // derive topological order
     pNtk = Wlc_NtkDupDfs( pTemp = pNtk, 0, 1 );
     Wlc_NtkFree( pTemp );
     //Ndr_NtkPrintNodes( pNtk );
+    pNtk->fMemPorts = 1;          // the network contains memory ports
+    pNtk->fEasyFfs = 1;           // the network contains simple flops
     return pNtk;
 }
 
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index b3b87f9e..b8a4b9b1 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -860,6 +860,7 @@ void Wlc_NtkDupDfs_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * v
     int i, iFanin;
     if ( Wlc_ObjCopy(p, iObj) )
         return;
+    //printf( "Visiting node %d\n", iObj );
     pObj = Wlc_NtkObj( p, iObj );
     Wlc_ObjForEachFanin( pObj, iFanin, i )
         Wlc_NtkDupDfs_rec( pNew, p, iFanin, vFanins );
@@ -876,6 +877,8 @@ Wlc_Ntk_t * Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p )
     vFanins = Vec_IntAlloc( 100 );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
+    pNew->fMemPorts = p->fMemPorts;
+    pNew->fEasyFfs = p->fEasyFfs;
     Wlc_NtkForEachCi( p, pObj, i )
         Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
     Wlc_NtkForEachCo( p, pObj, i )
@@ -902,6 +905,8 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
     Wlc_NtkCleanCopy( p );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
+    pNew->fMemPorts = p->fMemPorts;
+    pNew->fEasyFfs = p->fEasyFfs;
     Wlc_NtkForEachCi( p, pObj, i )
         if ( !fMarked || pObj->Mark )
         {
@@ -951,6 +956,8 @@ Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vP
     Wlc_NtkCleanCopy( p );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
+    pNew->fMemPorts = p->fMemPorts;
+    pNew->fEasyFfs = p->fEasyFfs;
 
     // duplicate marked PIs
     vFanins = Vec_IntAlloc( 100 );
@@ -1132,6 +1139,8 @@ Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p )
     vFanins = Vec_IntAlloc( 100 );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
+    pNew->fMemPorts = p->fMemPorts;
+    pNew->fEasyFfs = p->fEasyFfs;
     Wlc_NtkForEachObj( p, pObj, i )
     {
         if ( Wlc_ObjIsCi(pObj) )
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 42fab688..9974dd44 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1275,6 +1275,123 @@ startword:
             // printf( "Created flop %s with range %d and init value %d (nameId = %d)\n", 
             //     Abc_NamStr(p->pNtk->pManName, NameIdOut), Wlc_ObjRange(pObj), nBits, NameId );
         }
+        else if ( Wlc_PrsStrCmp( pStart, "ABC_DFFRSE" ) )
+        {
+            int NameId[8], fFound, nBits = 1, fFlopIn, fFlopOut, fFlopClk, fFlopRst, fFlopSet, fFlopEna, fFlopAsync, fFlopInit;
+            pStart += strlen("ABC_DFF");
+            while ( 1 )
+            {
+                pStart = Wlc_PrsFindSymbol( pStart, '.' );
+                if ( pStart == NULL )
+                    break;
+                pStart = Wlc_PrsSkipSpaces( pStart+1 );
+                fFlopIn    = (pStart[0] == 'd');
+                fFlopOut   = (pStart[0] == 'q');
+                fFlopClk   = (pStart[0] == 'c');
+                fFlopRst   = (pStart[0] == 'r');
+                fFlopSet   = (pStart[0] == 's');
+                fFlopEna   = (pStart[0] == 'e');
+                fFlopAsync = (pStart[0] == 'a');
+                fFlopInit  = (pStart[0] == 'i');
+                pStart = Wlc_PrsFindSymbol( pStart, '(' );
+                if ( pStart == NULL )
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read opening parenthesis 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 ( fFlopIn )
+                    NameId[0] = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                else if ( fFlopOut ) 
+                    NameId[7] = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                else if ( fFlopClk ) 
+                    NameId[1] = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                else if ( fFlopRst ) 
+                    NameId[2] = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                else if ( fFlopSet ) 
+                    NameId[3] = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                else if ( fFlopEna ) 
+                    NameId[4] = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                else if ( fFlopAsync ) 
+                    NameId[5] = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                else if ( fFlopInit ) 
+                    NameId[6] = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                else
+                    assert( 0 );
+                if ( !fFound )
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Name %s is not declared.", pName );
+            }
+            if ( NameId[0] == -1 || NameId[7] == -1 )
+                return Wlc_PrsWriteErrorMessage( p, pStart, "Name of flop input or flop output is missing." );
+            // create output
+            pObj = Wlc_NtkObj( p->pNtk, NameId[7] );
+            Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_FF );
+            Vec_IntClear( p->vFanins );
+            Vec_IntPush( p->vFanins, NameId[0] );
+            Vec_IntPush( p->vFanins, NameId[1] );
+            Vec_IntPush( p->vFanins, NameId[2] );
+            Vec_IntPush( p->vFanins, NameId[3] );
+            Vec_IntPush( p->vFanins, NameId[4] );
+            Vec_IntPush( p->vFanins, NameId[5] );
+            Vec_IntPush( p->vFanins, NameId[6] );
+            Wlc_ObjAddFanins( p->pNtk, pObj, p->vFanins );
+        }
+        else if ( Wlc_PrsStrCmp( pStart, "ABC_DFF" ) )
+        {
+            int NameId = -1, NameIdIn = -1, NameIdOut = -1, fFound, nBits = 1, fFlopIn, fFlopOut;
+            pStart += strlen("ABC_DFFRSE");
+            while ( 1 )
+            {
+                pStart = Wlc_PrsFindSymbol( pStart, '.' );
+                if ( pStart == NULL )
+                    break;
+                pStart = Wlc_PrsSkipSpaces( pStart+1 );
+                fFlopIn = (pStart[0] == 'd');
+                fFlopOut = (pStart[0] == 'q');
+                pStart = Wlc_PrsFindSymbol( pStart, '(' );
+                if ( pStart == NULL )
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read opening parenthesis 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 ( fFlopIn )
+                    NameIdIn = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                else 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 ( NameIdIn == -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, NameIdOut );
+            Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_FO );
+            Vec_IntPush( &p->pNtk->vFfs, NameIdOut );
+            nBits = Wlc_ObjRange(Wlc_NtkObj(p->pNtk, NameIdOut));
+            // create flop input
+            pObj = Wlc_NtkObj( p->pNtk, NameIdIn );
+            Vec_IntPush( &p->pNtk->vFfs, NameIdIn );
+            // compare bit-width
+            if ( Wlc_ObjRange(Wlc_NtkObj(p->pNtk, NameIdIn)) != nBits )
+                printf( "Warning!  Flop input \"%s\" bit-width (%d) is different from that of flop output (%d)\n", 
+                    Abc_NamStr(p->pNtk->pManName, NameId), Wlc_ObjRange(Wlc_NtkObj(p->pNtk, NameIdIn)), nBits );
+            // save flop init value
+            if ( NameId == -1 )
+                printf( "Initial value of flop \"%s\" is not specified. Zero is assumed.\n", Abc_NamStr(p->pNtk->pManName, NameIdOut) );
+            else
+            {
+                if ( Wlc_ObjRange(Wlc_NtkObj(p->pNtk, NameId)) != nBits )
+                    printf( "Warning!  Flop init signal \"%s\" bit-width (%d) is different from that of flop output (%d)\n", 
+                        Abc_NamStr(p->pNtk->pManName, NameId), Wlc_ObjRange(Wlc_NtkObj(p->pNtk, NameId)), nBits );
+            }
+            if ( p->pNtk->vInits == NULL )
+                p->pNtk->vInits = Vec_IntAlloc( 100 );
+            Vec_IntPush( p->pNtk->vInits, NameId > 0 ? NameId : -Wlc_ObjRange(Wlc_NtkObj(p->pNtk, NameIdOut)) );
+            // printf( "Created flop %s with range %d and init value %d (nameId = %d)\n", 
+            //     Abc_NamStr(p->pNtk->pManName, NameIdOut), Wlc_ObjRange(pObj), nBits, NameId );
+            p->pNtk->fEasyFfs = 1;
+        }
         else if ( Wlc_PrsStrCmp( pStart, "CPL_MEM_" ) )
         {
             int * pNameId = NULL, NameOutput, NameMi = -1, NameMo = -1, NameAddr = -1, NameDi = -1, NameDo = -1, fFound, fRead = 1;
@@ -1324,6 +1441,87 @@ startword:
             //printf( "Memory %s ", fRead ? "Read" : "Write" ); printf( "Fanins: " );  Vec_IntPrint( p->vFanins );
             Wlc_ObjAddFanins( p->pNtk, pObj, p->vFanins );
         }
+        else if ( Wlc_PrsStrCmp( pStart, "ABC_READ" ) )
+        {
+            int * pNameId = NULL, NameMemIn = -1, NameData = -1, NameAddr = -1, fFound;
+            pStart += strlen("ABC_READ");
+            while ( 1 )
+            {
+                pStart = Wlc_PrsFindSymbol( pStart, '.' );
+                if ( pStart == NULL )
+                    break;
+                pStart = Wlc_PrsSkipSpaces( pStart+1 );
+                if ( !strncmp(pStart, "mem_in", 6) )
+                    pNameId = &NameMemIn;
+                else if ( !strncmp(pStart, "addr", 4) )
+                    pNameId = &NameAddr;
+                else if ( !strncmp(pStart, "data", 4) )
+                    pNameId = &NameData;
+                else
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read name of the input/output port." );
+                pStart = Wlc_PrsFindSymbol( pStart, '(' );
+                if ( pStart == NULL )
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read opening parenthesis in the flop description." );
+                pStart = Wlc_PrsFindName( pStart+1, &pName );
+                if ( pStart == NULL )
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read name inside flop description." );
+                *pNameId = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                if ( !fFound )
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Name %s is not declared.", pName );
+            }
+            if ( NameMemIn == -1 || NameAddr == -1 || NameData == -1 )
+                return Wlc_PrsWriteErrorMessage( p, pStart, "Name of one of signals of read port is missing." );
+            // create output
+            pObj = Wlc_NtkObj( p->pNtk, NameData );
+            Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_READ );
+            Vec_IntClear( p->vFanins );
+            Vec_IntPush( p->vFanins, NameMemIn );
+            Vec_IntPush( p->vFanins, NameAddr );
+            Wlc_ObjAddFanins( p->pNtk, pObj, p->vFanins );
+            p->pNtk->fMemPorts = 1;
+        }
+        else if ( Wlc_PrsStrCmp( pStart, "ABC_WRITE" ) )
+        {
+            int * pNameId = NULL, NameMemIn = -1, NameMemOut = -1, NameData = -1, NameAddr = -1, fFound;
+            pStart += strlen("ABC_WRITE");
+            while ( 1 )
+            {
+                pStart = Wlc_PrsFindSymbol( pStart, '.' );
+                if ( pStart == NULL )
+                    break;
+                pStart = Wlc_PrsSkipSpaces( pStart+1 );
+                if ( !strncmp(pStart, "mem_in", 6) )
+                    pNameId = &NameMemIn;
+                else if ( !strncmp(pStart, "mem_out", 7) )
+                    pNameId = &NameMemOut;
+                else if ( !strncmp(pStart, "data", 4) )
+                    pNameId = &NameData;
+                else if ( !strncmp(pStart, "addr", 4) )
+                    pNameId = &NameAddr;
+                else
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read name of the input/output port." );
+                pStart = Wlc_PrsFindSymbol( pStart, '(' );
+                if ( pStart == NULL )
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read opening parenthesis in the flop description." );
+                pStart = Wlc_PrsFindName( pStart+1, &pName );
+                if ( pStart == NULL )
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read name inside flop description." );
+                *pNameId = Abc_NamStrFindOrAdd( p->pNtk->pManName, pName, &fFound );
+                if ( !fFound )
+                    return Wlc_PrsWriteErrorMessage( p, pStart, "Name %s is not declared.", pName );
+            }
+            if ( NameMemIn == -1 || NameAddr == -1 || NameData == -1 || NameMemOut == -1 )
+                return Wlc_PrsWriteErrorMessage( p, pStart, "Name of one of signals of write port is missing." );
+            // create output
+            pObj = Wlc_NtkObj( p->pNtk, NameMemOut );
+            Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_WRITE );
+            Vec_IntClear( p->vFanins );
+            Vec_IntPush( p->vFanins, NameMemIn );
+            Vec_IntPush( p->vFanins, NameAddr );
+            Vec_IntPush( p->vFanins, NameData );
+            Wlc_ObjAddFanins( p->pNtk, pObj, p->vFanins );
+            p->pNtk->fMemPorts = 1;
+        }
         else if ( pStart[0] == '(' && pStart[1] == '*' ) // skip comments
         {
             while ( *pStart++ != ')' );
diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c
index 98d1b2dc..fe14eedb 100644
--- a/src/base/wlc/wlcWriteVer.c
+++ b/src/base/wlc/wlcWriteVer.c
@@ -186,13 +186,13 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
                 continue;
             Range[0] = 0;
         }
-        if ( pObj->fIsPo || (fNoFlops && pObj->fIsFi) )
+        if ( (pObj->fIsPo || (fNoFlops && pObj->fIsFi)) && pObj->Type != WLC_OBJ_FF )
         {
             if ( Wlc_ObjFaninNum(pObj) == 0 )
                 continue;
             fprintf( pFile, "  assign                         " );
         }
-        else if ( pObj->Type == WLC_OBJ_MUX && Wlc_ObjFaninNum(pObj) > 3 )
+        else if ( (pObj->Type == WLC_OBJ_MUX && Wlc_ObjFaninNum(pObj) > 3) || pObj->Type == WLC_OBJ_FF )
             fprintf( pFile, "reg  %s ", Range );
         else
             fprintf( pFile, "wire %s ", Range );
@@ -255,17 +255,41 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
         }
         else if ( pObj->Type == WLC_OBJ_READ || pObj->Type == WLC_OBJ_WRITE )
         {
-            int nBitsMem  = Wlc_ObjRange( Wlc_ObjFanin(p, pObj, 0) );
-            //int nBitsAddr = Wlc_ObjRange( Wlc_ObjFanin(p, pObj, 1) );
-            int nBitsDat  = pObj->Type == WLC_OBJ_READ ? Wlc_ObjRange(pObj) : Wlc_ObjRange(Wlc_ObjFanin(p, pObj, 2));
-            int Depth     = nBitsMem / nBitsDat;
-            assert( nBitsMem % nBitsDat == 0 );
+            if ( p->fMemPorts )
+            {
+                fprintf( pFile, "%s ;\n", Wlc_ObjName(p, i) );
+                fprintf( pFile, "         " );
+                fprintf( pFile, "%s (", pObj->Type == WLC_OBJ_READ ? "ABC_READ" : "ABC_WRITE" );
+                Wlc_ObjForEachFanin( pObj, iFanin, k )
+                    fprintf( pFile, " .%s(%s)", k==0 ? "mem_in" : (k==1 ? "addr": "data"), Wlc_ObjName(p, iFanin) );
+                fprintf( pFile, " .%s(%s) ) ;\n", pObj->Type == WLC_OBJ_READ ? "data" : "mem_out", Wlc_ObjName(p, i) );
+                continue;
+            }
+            else
+            {
+                int nBitsMem  = Wlc_ObjRange( Wlc_ObjFanin(p, pObj, 0) );
+                //int nBitsAddr = Wlc_ObjRange( Wlc_ObjFanin(p, pObj, 1) );
+                int nBitsDat  = pObj->Type == WLC_OBJ_READ ? Wlc_ObjRange(pObj) : Wlc_ObjRange(Wlc_ObjFanin(p, pObj, 2));
+                int Depth     = nBitsMem / nBitsDat;
+                assert( nBitsMem % nBitsDat == 0 );
+                fprintf( pFile, "%s ;\n", Wlc_ObjName(p, i) );
+                fprintf( pFile, "         " );
+                fprintf( pFile, "%s_%d (", pObj->Type == WLC_OBJ_READ ? "CPL_MEM_READ" : "CPL_MEM_WRITE", Depth );
+                Wlc_ObjForEachFanin( pObj, iFanin, k )
+                    fprintf( pFile, " .%s(%s)", k==0 ? "mem_data_in" : (k==1 ? "addr_in": "data_in"), Wlc_ObjName(p, iFanin) );
+                fprintf( pFile, " .%s(%s) ) ;\n", "data_out", Wlc_ObjName(p, i) );
+                continue;
+            }
+        }
+        else if ( pObj->Type == WLC_OBJ_FF )
+        {
+            char * pInNames[7] = {"d", "clk", "reset", "set", "enable", "async", "init"};
             fprintf( pFile, "%s ;\n", Wlc_ObjName(p, i) );
             fprintf( pFile, "         " );
-            fprintf( pFile, "%s_%d (", pObj->Type == WLC_OBJ_READ ? "CPL_MEM_READ" : "CPL_MEM_WRITE", Depth );
+            fprintf( pFile, "%s (", "ABC_DFFRSE" );
             Wlc_ObjForEachFanin( pObj, iFanin, k )
-                fprintf( pFile, " .%s(%s)", k==0 ? "mem_data_in" : (k==1 ? "addr_in": "data_in"), Wlc_ObjName(p, iFanin) );
-            fprintf( pFile, " .%s(%s) );\n", "data_out", Wlc_ObjName(p, i) );
+                fprintf( pFile, " .%s(%s)", pInNames[k], Wlc_ObjName(p, iFanin) );
+            fprintf( pFile, " .%s(%s) ) ;\n", "q", Wlc_ObjName(p, i) );
             continue;
         }
         else 
@@ -426,22 +450,35 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
             if ( pObj->Type == WLC_OBJ_PI )
                 continue;
             fprintf( pFile, "         " );
-            fprintf( pFile, "CPL_FF" );
-            if ( Wlc_ObjRange(pObj) > 1 )
-                fprintf( pFile, "#%d%*s", Wlc_ObjRange(pObj), 4 - Abc_Base10Log(Wlc_ObjRange(pObj)+1), "" );
-            else
-                fprintf( pFile, "     " );
-            fprintf( pFile, " reg%d (",       i );
-            fprintf( pFile, " .q( %s ),",      Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
-            fprintf( pFile, " .qbar()," );
-            fprintf( pFile, " .d( %s ),",      Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj))) );
-            fprintf( pFile, " .clk( %s ),",    "1\'b0" );
-            fprintf( pFile, " .arst( %s ),",   "1\'b0" );
-            if ( p->vInits )
-                fprintf( pFile, " .arstval( %s_init )", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
+            if ( p->fEasyFfs )
+            {
+                fprintf( pFile, "ABC_DFF" );
+                fprintf( pFile, " reg%d (",        i );
+                fprintf( pFile, " .q(%s),",      Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
+                fprintf( pFile, " .d(%s),",      Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj))) );
+                if ( p->vInits )
+                    fprintf( pFile, " .init(%s_init)", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
+                fprintf( pFile, " ) ;\n" );
+            }
             else
-                fprintf( pFile, " .arstval( %s )", "1\'b0" );
-            fprintf( pFile, " ) ;\n" );
+            {
+                fprintf( pFile, "CPL_FF" );
+                if ( Wlc_ObjRange(pObj) > 1 )
+                    fprintf( pFile, "#%d%*s", Wlc_ObjRange(pObj), 4 - Abc_Base10Log(Wlc_ObjRange(pObj)+1), "" );
+                else
+                    fprintf( pFile, "     " );
+                fprintf( pFile, " reg%d (",       i );
+                fprintf( pFile, " .q(%s),",      Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
+                fprintf( pFile, " .qbar()," );
+                fprintf( pFile, " .d(%s),",      Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj))) );
+                fprintf( pFile, " .clk(%s),",    "1\'b0" );
+                fprintf( pFile, " .arst(%s),",   "1\'b0" );
+                if ( p->vInits )
+                    fprintf( pFile, " .arstval(%s_init)", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
+                else
+                    fprintf( pFile, " .arstval(%s)", "1\'b0" );
+                fprintf( pFile, " ) ;\n" );
+            }
         }
         assert( !p->vInits || iFanin == (int)strlen(p->pInits) );
     }