Improvements to Cba data-structure.

5 files changed, 763 insertions, 192 deletions

diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index a23c2bc7..c0e0d91d 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -109,6 +109,7 @@ typedef enum {
     CBA_BOX_REM,
     CBA_BOX_POW,
     CBA_BOX_MIN,
+    CBA_BOX_SQRT,
     CBA_BOX_ABS,
 
     CBA_BOX_SLTHAN,
@@ -121,6 +122,7 @@ typedef enum {
 
     CBA_BOX_SHIL,
     CBA_BOX_SHIR,
+    CBA_BOX_SHILA,
     CBA_BOX_SHIRA,
     CBA_BOX_ROTL,
     CBA_BOX_ROTR,
@@ -142,6 +144,7 @@ typedef enum {
     CBA_BOX_LATCH,
     CBA_BOX_LATCHRS,
     CBA_BOX_DFF,
+    CBA_BOX_DFFCPL,
     CBA_BOX_DFFRS,
 
     CBA_BOX_LAST   // 67
@@ -278,29 +281,29 @@ static inline int            Cba_NtkBoxUserNum( Cba_Ntk_t * p )              { r
 static inline int            Cba_NtkBoxPrimNum( Cba_Ntk_t * p )              { return Vec_StrCountLarger(&p->vObjType, (char)CBA_OBJ_BOX);                                 }
 static inline int            Cba_NtkBoxSeqNum( Cba_Ntk_t * p )               { return Vec_IntSize(&p->vSeq);                                                               }
 
-static inline void           Cba_NtkCleanObjCopies( Cba_Ntk_t * p )          { Vec_IntFill(&p->vObjCopy, Vec_StrCap(&p->vObjType), -1);        }
-static inline void           Cba_NtkCleanObjFuncs( Cba_Ntk_t * p )           { Vec_IntFill(&p->vObjFunc, Vec_StrCap(&p->vObjType),  0);        }
-static inline void           Cba_NtkCleanObjNames( Cba_Ntk_t * p )           { Vec_IntFill(&p->vObjName, Vec_StrCap(&p->vObjType),  0);        }
-static inline void           Cba_NtkCleanObjAttrs( Cba_Ntk_t * p )           { Vec_IntFill(&p->vObjAttr, Vec_StrCap(&p->vObjType),  0); Vec_IntFill(&p->vAttrSto, 1, -1);  }
-static inline void           Cba_NtkCleanFonCopies( Cba_Ntk_t * p )          { Vec_IntFill(&p->vFonCopy, Vec_IntCap(&p->vFonObj),   0);        }
-static inline void           Cba_NtkCleanFonNames( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonName, Vec_IntCap(&p->vFonObj),   0);        }
-static inline void           Cba_NtkCleanFonRanges( Cba_Ntk_t * p )          { Vec_IntFill(&p->vFonRange,Vec_IntCap(&p->vFonObj),   0);        }
-static inline void           Cba_NtkCleanFonPrevs( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonPrev, Vec_IntCap(&p->vFonObj),   0);        }
-static inline void           Cba_NtkCleanFonNexts( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonNext, Vec_IntCap(&p->vFonObj),   0);        }
-static inline void           Cba_NtkCleanFinFon0( Cba_Ntk_t * p )            { Vec_IntFill(&p->vFinFon0, Vec_IntCap(&p->vFinFon),   0);        }
-static inline void           Cba_NtkCleanFinObjs( Cba_Ntk_t * p )            { Vec_IntFill(&p->vFinObj,  Vec_IntCap(&p->vFinFon),   0);        }
-
-static inline int            Cba_NtkHasObjCopies( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vObjCopy) > 0; }
-static inline int            Cba_NtkHasObjFuncs( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vObjFunc) > 0; }
-static inline int            Cba_NtkHasObjNames( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vObjName) > 0; }
-static inline int            Cba_NtkHasObjAttrs( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vObjAttr) > 0; }
-static inline int            Cba_NtkHasFonCopies( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vFonCopy) > 0; }
-static inline int            Cba_NtkHasFonNames( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonName) > 0; }
-static inline int            Cba_NtkHasFonRanges( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vFonRange)> 0; }
-static inline int            Cba_NtkHasFonPrevs( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonPrev) > 0; }
-static inline int            Cba_NtkHasFonNexts( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonNext) > 0; }
-static inline int            Cba_NtkHasFinFon0( Cba_Ntk_t * p )              { return Vec_IntSize(&p->vFinFon0) > 0; }
-static inline int            Cba_NtkHasFinObjs( Cba_Ntk_t * p )              { return Vec_IntSize(&p->vFinObj)  > 0; }
+static inline void           Cba_NtkCleanObjCopies( Cba_Ntk_t * p )          { Vec_IntFill(&p->vObjCopy,  Vec_StrCap(&p->vObjType), -1);        }
+static inline void           Cba_NtkCleanObjFuncs( Cba_Ntk_t * p )           { Vec_IntFill(&p->vObjFunc,  Vec_StrCap(&p->vObjType),  0);        }
+static inline void           Cba_NtkCleanObjNames( Cba_Ntk_t * p )           { Vec_IntFill(&p->vObjName,  Vec_StrCap(&p->vObjType),  0);        }
+static inline void           Cba_NtkCleanObjAttrs( Cba_Ntk_t * p )           { Vec_IntFill(&p->vObjAttr,  Vec_StrCap(&p->vObjType),  0); Vec_IntFill(&p->vAttrSto, 1, -1); }
+static inline void           Cba_NtkCleanFonCopies( Cba_Ntk_t * p )          { Vec_IntFill(&p->vFonCopy,  Vec_IntCap(&p->vFonObj),   0);        }
+static inline void           Cba_NtkCleanFonNames( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonName,  Vec_IntCap(&p->vFonObj),   0);        }
+static inline void           Cba_NtkCleanFonRanges( Cba_Ntk_t * p )          { Vec_IntFill(&p->vFonRange, Vec_IntCap(&p->vFonObj),   0);        }
+static inline void           Cba_NtkCleanFonPrevs( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonPrev,  Vec_IntCap(&p->vFonObj),   0);        }
+static inline void           Cba_NtkCleanFonNexts( Cba_Ntk_t * p )           { Vec_IntFill(&p->vFonNext,  Vec_IntCap(&p->vFonObj),   0);        }
+static inline void           Cba_NtkCleanFinFon0( Cba_Ntk_t * p )            { Vec_IntFill(&p->vFinFon0,  Vec_IntCap(&p->vFinFon),   0);        }
+static inline void           Cba_NtkCleanFinObjs( Cba_Ntk_t * p )            { Vec_IntFill(&p->vFinObj,   Vec_IntCap(&p->vFinFon),   0);        }
+
+static inline int            Cba_NtkHasObjCopies( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vObjCopy)  > 0; }
+static inline int            Cba_NtkHasObjFuncs( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vObjFunc)  > 0; }
+static inline int            Cba_NtkHasObjNames( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vObjName)  > 0; }
+static inline int            Cba_NtkHasObjAttrs( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vObjAttr)  > 0; }
+static inline int            Cba_NtkHasFonCopies( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vFonCopy)  > 0; }
+static inline int            Cba_NtkHasFonNames( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonName)  > 0; }
+static inline int            Cba_NtkHasFonRanges( Cba_Ntk_t * p )            { return Vec_IntSize(&p->vFonRange) > 0; }
+static inline int            Cba_NtkHasFonPrevs( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonPrev)  > 0; }
+static inline int            Cba_NtkHasFonNexts( Cba_Ntk_t * p )             { return Vec_IntSize(&p->vFonNext)  > 0; }
+static inline int            Cba_NtkHasFinFon0( Cba_Ntk_t * p )              { return Vec_IntSize(&p->vFinFon0)  > 0; }
+static inline int            Cba_NtkHasFinObjs( Cba_Ntk_t * p )              { return Vec_IntSize(&p->vFinObj)   > 0; }
 
 static inline void           Cba_NtkFreeObjCopies( Cba_Ntk_t * p )           { Vec_IntErase(&p->vObjCopy);   }
 static inline void           Cba_NtkFreeObjFuncs( Cba_Ntk_t * p )            { Vec_IntErase(&p->vObjFunc);   }
@@ -318,7 +321,7 @@ static inline Cba_ObjType_t  Cba_ObjType( Cba_Ntk_t * p, int i )             { a
 static inline void           Cba_ObjCleanType( Cba_Ntk_t * p, int i )        { assert(i>0); Vec_StrWriteEntry( &p->vObjType, i, (char)CBA_OBJ_NONE );                      }
 static inline int            Cba_TypeIsBox( Cba_ObjType_t Type )             { return Type >= CBA_OBJ_BOX && Type < CBA_BOX_LAST;                                          }
 static inline int            Cba_TypeIsSeq( Cba_ObjType_t Type )             { return Type >= CBA_BOX_RAM && Type <= CBA_BOX_DFFRS;                                        }
-static inline int            Cba_TypeIsUnary( Cba_ObjType_t Type )           { return Type == CBA_BOX_BUF || Type == CBA_BOX_INV || Type == CBA_BOX_LNOT || Type == CBA_BOX_MIN || Type == CBA_BOX_ABS || (Type >= CBA_BOX_RAND && Type <= CBA_BOX_RXNOR);  }
+static inline int            Cba_TypeIsUnary( Cba_ObjType_t Type )           { return Type == CBA_BOX_BUF || Type == CBA_BOX_INV || Type == CBA_BOX_LNOT || Type == CBA_BOX_MIN || Type == CBA_BOX_SQRT || Type == CBA_BOX_ABS || (Type >= CBA_BOX_RAND && Type <= CBA_BOX_RXNOR);  }
 static inline int            Cba_TypeIsMux( Cba_ObjType_t Type )             { return Type == CBA_BOX_MUX || Type == CBA_BOX_NMUX || Type == CBA_BOX_SEL || Type == CBA_BOX_PSEL;  }
 
 static inline int            Cba_ObjIsPi( Cba_Ntk_t * p, int i )             { return Cba_ObjType(p, i) == CBA_OBJ_PI;                                                     }
@@ -375,18 +378,20 @@ static inline int            Cba_FonFromConst( int c )                       { a
 static inline int            Cba_FonConstRange( Cba_Ntk_t * p, int f )       { assert(Cba_FonIsConst(f)); return atoi(Cba_NtkConst(p, Cba_FonConst(f)));                   }
 
 static inline int            Cba_FonObj( Cba_Ntk_t * p, int f )              { return Cba_FonIsReal(f) ? Vec_IntEntry(&p->vFonObj, f) : 0;                                 }
-static inline int            Cba_FonRange( Cba_Ntk_t * p, int f )            { assert(Cba_FonIsReal(f)); return Cba_NtkHasFonRanges(p)?Vec_IntGetEntry(&p->vFonRange, f):0;}
+static inline int            Cba_FonRange( Cba_Ntk_t * p, int f )            { assert(Cba_FonIsReal(f)); return Cba_NtkHasFonRanges(p)?Abc_Lit2Var(Vec_IntGetEntry(&p->vFonRange, f)):0;    }
+static inline int            Cba_FonSigned( Cba_Ntk_t * p, int f )           { assert(Cba_FonIsReal(f)); return Cba_NtkHasFonRanges(p)?Abc_LitIsCompl(Vec_IntGetEntry(&p->vFonRange, f)):0; }
 static inline int            Cba_FonLeft( Cba_Ntk_t * p, int f )             { return Cba_NtkRangeLeft(p, Cba_FonRange(p, f));                                             }
 static inline int            Cba_FonRight( Cba_Ntk_t * p, int f )            { return Cba_NtkRangeRight(p, Cba_FonRange(p, f));                                            }
 static inline int            Cba_FonRangeSize( Cba_Ntk_t * p, int f )        { return Cba_FonIsConst(f) ? Cba_FonConstRange(p, f):Cba_NtkRangeSize(p, Cba_FonRange(p, f)); }
-static inline void           Cba_FonSetRange( Cba_Ntk_t * p, int f, int x )  { assert(Cba_NtkHasFonRanges(p));  Vec_IntSetEntry(&p->vFonRange, f, x);                      }
+static inline void           Cba_FonSetRangeSign( Cba_Ntk_t * p, int f, int x )  { assert(Cba_NtkHasFonRanges(p));  Vec_IntSetEntry(&p->vFonRange, f, x);                  }
+static inline void           Cba_FonSetRange( Cba_Ntk_t * p, int f, int x )  { assert(Cba_NtkHasFonRanges(p));  Vec_IntSetEntry(&p->vFonRange, Abc_Var2Lit(f,0), x);       }
 static inline void           Cba_FonHashRange( Cba_Ntk_t * p, int f, int l, int r ) { Cba_FonSetRange( p, f, Cba_NtkHashRange(p, l, r) );                                  }
 static inline int            Cba_FonCopy( Cba_Ntk_t * p, int f )             { return Cba_FonIsReal(f) ? Vec_IntEntry(&p->vFonCopy, f) : f;                                }
 static inline void           Cba_FonSetCopy( Cba_Ntk_t * p, int f, int x )   { assert(Cba_FonIsReal(f)); assert(Cba_FonCopy(p, f) == 0); Vec_IntWriteEntry(&p->vFonCopy, f, x); }
 static inline int            Cba_FonName( Cba_Ntk_t * p, int f )             { assert(Cba_NtkHasFonNames(p)); assert(Cba_FonIsReal(f)); return Vec_IntGetEntry( &p->vFonName, f );                        }
 static inline char *         Cba_FonNameStr( Cba_Ntk_t * p, int f )          { assert(Cba_NtkHasFonNames(p)); assert(Cba_FonIsReal(f)); return Cba_NtkStr(p, Cba_FonName(p, f));                          }
-static inline void           Cba_FonSetName( Cba_Ntk_t * p, int f, int x )   { assert(Cba_NtkHasFonNames(p)); assert(Cba_FonIsReal(f)); assert(Cba_FonName(p, f) == 0); Vec_IntSetEntry(&p->vFonName, f, x);   }
-static inline void           Cba_FonCleanName( Cba_Ntk_t * p, int f )        { assert(Cba_NtkHasFonNames(p)); assert(Cba_FonIsReal(f)); assert(Cba_FonName(p, f) != 0); Vec_IntSetEntry(&p->vFonName, f, 0);   }
+static inline void           Cba_FonSetName( Cba_Ntk_t * p, int f, int x )   { assert(Cba_NtkHasFonNames(p)); assert(Cba_FonIsReal(f)); assert(Cba_FonName(p, f) == 0); Vec_IntSetEntry(&p->vFonName, f, x); }
+static inline void           Cba_FonCleanName( Cba_Ntk_t * p, int f )        { assert(Cba_NtkHasFonNames(p)); assert(Cba_FonIsReal(f)); assert(Cba_FonName(p, f) != 0); Vec_IntSetEntry(&p->vFonName, f, 0); }
 static inline void           Cba_FonPatchName( Cba_Ntk_t * p, int f, int x)  { assert(Cba_NtkHasFonNames(p)); assert(Cba_FonIsReal(f)); Cba_FonCleanName(p, f); Cba_FonSetName(p, f, x);                  }
 static inline int            Cba_FonIndex( Cba_Ntk_t * p, int f )            { assert(Cba_FonIsReal(f)); return f - Cba_ObjFon0( p, Cba_FonObj(p, f) );                    }
 static inline int            Cba_FonNtkId( Cba_Ntk_t * p, int f )            { assert(Cba_FonIsReal(f)); return Cba_ObjNtkId( p, Cba_FonObj(p, f) );                       }
diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c
index ca86766e..b01f0d4e 100644
--- a/src/base/cba/cbaCom.c
+++ b/src/base/cba/cbaCom.c
@@ -213,7 +213,10 @@ int Cba_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( argc == globalUtilOptind + 1 )
         pFileName = argv[globalUtilOptind];
     else if ( argc == globalUtilOptind && p )
-        pFileName = Extra_FileNameGenericAppend( Cba_ManName(p), "_out.v" );
+    {
+        pFileName = Extra_FileNameGenericAppend( Cba_ManSpec(p) ? Cba_ManSpec(p) : Cba_ManName(p), "_out.v" );
+        printf( "Generated output file name \"%s\".\n", pFileName );
+    }
     else 
     {
         printf( "Output file name should be given on the command line.\n" );
diff --git a/src/base/cba/cbaPrs.h b/src/base/cba/cbaPrs.h
index 2f5220d3..5183762d 100644
--- a/src/base/cba/cbaPrs.h
+++ b/src/base/cba/cbaPrs.h
@@ -42,15 +42,19 @@ typedef enum {
     PRS_VER_OUTPUT,    // 2:  output
     PRS_VER_INOUT,     // 3:  inout
     PRS_VER_WIRE,      // 4:  wire
-    PRS_VER_MODULE,    // 5:  module
-    PRS_VER_ASSIGN,    // 6:  assign
-    PRS_VER_REG,       // 7:  reg
+    PRS_VER_REG,       // 5:  reg
+    PRS_VER_MODULE,    // 6:  module
+    PRS_VER_ASSIGN,    // 7:  assign
     PRS_VER_ALWAYS,    // 8:  always
-    PRS_VER_DEFPARAM,  // 9:  always
-    PRS_VER_BEGIN,     // 10: begin
-    PRS_VER_END,       // 11: end
-    PRS_VER_ENDMODULE, // 12: endmodule
-    PRS_VER_UNKNOWN    // 13: unknown
+    PRS_VER_FUNCTION,  // 9:  function
+    PRS_VER_DEFPARAM,  // 10: defparam
+    PRS_VER_BEGIN,     // 11: begin
+    PRS_VER_END,       // 12: end
+    PRS_VER_CASE,      // 13: case
+    PRS_VER_ENDCASE,   // 14: endcase
+    PRS_VER_SIGNED,    // 15: signed
+    PRS_VER_ENDMODULE, // 16: endmodule
+    PRS_VER_UNKNOWN    // 17: unknown
 } Cba_VerType_t;
 
 // parser name types
@@ -117,13 +121,17 @@ struct Prs_Man_t_
     Vec_Str_t       vCover;      // one SOP cover
     Vec_Int_t       vTemp;       // array of tokens
     Vec_Int_t       vTemp2;      // array of tokens
+    Vec_Int_t       vTemp3;      // array of tokens
+    Vec_Int_t       vTemp4;      // array of tokens
     // statistics
     Vec_Int_t       vKnown;
     Vec_Int_t       vFailed;
     Vec_Int_t       vSucceeded;
     // error handling
     int             fUsingTemp2; // vTemp2 is in use
-    char ErrorStr[1000];      // error
+    int             FuncNameId;  // temp value
+    int             FuncRangeId; // temp value
+    char ErrorStr[1000];         // error
 };
 
 static inline Prs_Ntk_t * Prs_ManNtk( Vec_Ptr_t * vPrs, int i )        { return i >= 0 && i < Vec_PtrSize(vPrs) ? (Prs_Ntk_t *)Vec_PtrEntry(vPrs, i) : NULL; }
@@ -142,6 +150,7 @@ static inline char *      Prs_NtkSop( Prs_Ntk_t * p, int h )           { return
 static inline char *      Prs_NtkConst( Prs_Ntk_t * p, int h )         { return Abc_NamStr(p->pFuns, h);                         }
 static inline char *      Prs_NtkName( Prs_Ntk_t * p )                 { return Prs_NtkStr(p, Prs_NtkId(p));                     }
 static inline int         Prs_NtkSigName( Prs_Ntk_t * p, int i )       { if (!p->fSlices) return i; assert(Abc_Lit2Att2(i) == CBA_PRS_NAME); return Abc_Lit2Var2(i); }
+static inline int         Ptr_NtkRangeSize( Prs_Ntk_t * p, int h )     { int l = Hash_IntObjData0(p->vHash, h), r = Hash_IntObjData1(p->vHash, h); return 1 + (l > r ? l-r : r-l); }
 
 static inline int         Prs_SliceName( Prs_Ntk_t * p, int h )        { return Vec_IntEntry(&p->vSlices, h);                    }
 static inline int         Prs_SliceRange( Prs_Ntk_t * p, int h )       { return Vec_IntEntry(&p->vSlices, h+1);                  }
@@ -353,6 +362,8 @@ static inline void Prs_ManFree( Prs_Man_t * p )
     Vec_StrErase( &p->vCover );
     Vec_IntErase( &p->vTemp );
     Vec_IntErase( &p->vTemp2 );
+    Vec_IntErase( &p->vTemp3 );
+    Vec_IntErase( &p->vTemp4 );
     Vec_IntErase( &p->vKnown );
     Vec_IntErase( &p->vFailed );
     Vec_IntErase( &p->vSucceeded );
diff --git a/src/base/cba/cbaReadVer.c b/src/base/cba/cbaReadVer.c
index 3e78e5f9..a5bdb219 100644
--- a/src/base/cba/cbaReadVer.c
+++ b/src/base/cba/cbaReadVer.c
@@ -33,15 +33,19 @@ static const char * s_VerTypes[PRS_VER_UNKNOWN+1] = {
     "output",          // 2:  output
     "inout",           // 3:  inout
     "wire",            // 4:  wire
-    "module",          // 5:  module
-    "assign",          // 6:  assign
-    "reg",             // 7:  reg
+    "reg",             // 5:  reg
+    "module",          // 6:  module
+    "assign",          // 7:  assign
     "always",          // 8:  always
-    "defparam",        // 9:  defparam
-    "begin",           // 10: begin
-    "end",             // 11: end
-    "endmodule",       // 12: endmodule
-    NULL               // 13: unknown 
+    "function",        // 9:  function
+    "defparam",        // 10: defparam
+    "begin",           // 11: begin
+    "end",             // 12: end
+    "case",            // 13: case
+    "endcase",         // 14: endcase
+    "signed",          // 15: signed
+    "endmodule",       // 16: endmodule
+    NULL               // 17: unknown 
 };
 
 void Prs_NtkAddVerilogDirectives( Prs_Man_t * p )
@@ -157,7 +161,10 @@ static const char * s_VerNames[100] =
     "wide_prio_select_",     
     "pow_",                  
     "PrioEncoder_",          
-    "abs_",                   
+    "abs_",
+    "CPL_NMACROFF",
+    "CPL_MACROFF",
+    "CPL_FF",
     NULL
 };
 
@@ -252,6 +259,7 @@ static const Prs_VerInfo_t s_VerInfo[100] =
     {CBA_BOX_POW,     2, "pow_",                   /* "OPER_POW"                */ {"a","b","o"}},
     {CBA_BOX_PENC,    1, "PrioEncoder_",           /* "OPER_PRIO_ENCODER"       */ {"sel","o"}},
     {CBA_BOX_ABS,     1, "abs_",                   /* "OPER_ABS"                */ {"i","o"}},
+    {CBA_BOX_DFFCPL,  4, "CPL_FF",                 /* "OPER_WIDE_DFF - 2"       */ {"d","arstval","arst","clk","q","qbar"}},
     {-1,              0, NULL,                     /* "PRIM_END"                */ {NULL}}
 }; 
 
@@ -374,6 +382,40 @@ static inline int Prs_ManUtilSkipUntilWord( Prs_Man_t * p, char * pWord )
     p->pCur = pPlace + strlen(pWord);
     return 0;
 }
+// detect two symbols on the same line
+static inline int Prs_ManUtilDetectTwo( Prs_Man_t * p, char Sym1, char Sym2 )
+{
+    char * pTemp;
+    for ( pTemp = p->pCur; *pTemp != ';'; pTemp++ )
+        if ( *pTemp == Sym1 && *pTemp == Sym2 )
+            return 1;
+    return 0;
+}
+// find closing paren
+static inline char * Prs_ManFindClosingParenthesis( Prs_Man_t * p, char Open, char Close )
+{
+    char * pTemp;
+    int Counter = 0;
+    int fNotName = 1;
+    assert( Prs_ManIsChar(p, Open) );
+    for ( pTemp = p->pCur; *pTemp; pTemp++ )
+    {
+        if ( fNotName )
+        {
+            if ( *pTemp == Open )
+                Counter++;
+            if ( *pTemp == Close )
+                Counter--;
+            if ( Counter == 0 )
+                return pTemp;
+        }
+        if ( *pTemp == '\\' )
+            fNotName = 0;
+        else if ( !fNotName && *pTemp == ' ' )
+            fNotName = 1;
+    }
+    return NULL;
+}
 
 /**Function*************************************************************
 
@@ -429,8 +471,11 @@ static inline int Prs_ManReadConstant( Prs_Man_t * p )
     assert( Prs_ManIsDigit(p) );
     while ( Prs_ManIsDigit(p) ) 
         p->pCur++;
-    if ( !Prs_ManIsChar(p, '\'') )          return Prs_ManErrorSet(p, "Cannot read constant.", 0);
+    if ( !Prs_ManIsChar(p, '\'') )
+        return Abc_NamStrFindOrAddLim( p->pFuns, pStart, p->pCur, NULL );
     p->pCur++;
+    if ( Prs_ManIsChar(p, 's') )
+        p->pCur++;
     if ( Prs_ManIsChar(p, 'b') )
     {
         p->pCur++;
@@ -520,24 +565,51 @@ static inline int Prs_ManReadSignal( Prs_Man_t * p )
     if ( Prs_ManIsDigit(p) )
     {
         Item = Prs_ManReadConstant(p);
-        if ( Item == 0 )                    return Prs_ManErrorSet(p, "Error number 9.", 0);
+        if ( Item == 0 )                    return 0;
         if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 10.", 0);
         return Abc_Var2Lit2( Item, CBA_PRS_CONST );
     }
     if ( Prs_ManIsChar(p, '{') )
     {
+        if ( Prs_CharIsDigit(p->pCur[1]) )
+        {
+            p->pCur++;
+            if ( Prs_ManIsDigit(p) )
+            {
+                int i, Num = atoi(p->pCur);
+                while ( Prs_ManIsDigit(p) )
+                    p->pCur++;
+                if ( Prs_ManUtilSkipSpaces(p) ) return Prs_ManErrorSet(p, "Error number 10.", 0);
+                assert( Prs_ManIsChar(p, '{') );
+                p->pCur++;
+                if ( Prs_ManUtilSkipSpaces(p) ) return Prs_ManErrorSet(p, "Error number 10.", 0);
+                Item = Prs_ManReadSignal( p );
+                assert( Prs_ManIsChar(p, '}') );
+                p->pCur++;
+                if ( Prs_ManUtilSkipSpaces(p) ) return Prs_ManErrorSet(p, "Error number 10.", 0);
+                // add to concat all, expect the last one
+                assert( p->fUsingTemp2 );
+                for ( i = 0; i < Num-1; i++ )
+                    Vec_IntPush( &p->vTemp2, Item );
+                if ( Prs_ManUtilSkipSpaces(p) ) return Prs_ManErrorSet(p, "Error number 10.", 0);
+                assert( Prs_ManIsChar(p, '}') );
+                p->pCur++;
+                if ( Prs_ManUtilSkipSpaces(p) ) return Prs_ManErrorSet(p, "Error number 10.", 0);
+                return Item;
+            }
+        }
         if ( p->fUsingTemp2 )               return Prs_ManErrorSet(p, "Cannot read nested concatenations.", 0);
         p->fUsingTemp2 = 1;
         Item = Prs_ManReadConcat(p, &p->vTemp2);
         p->fUsingTemp2 = 0;
-        if ( Item == 0 )                    return Prs_ManErrorSet(p, "Error number 11.", 0);
+        if ( Item == 0 )                    return 0;
         if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 12.", 0);
         return Item;
     }
     else
     {
         Item = Prs_ManReadName( p );
-        if ( Item == 0 )                    return Prs_ManErrorSet(p, "Error number 13.", 0);    // was        return 1;                
+        if ( Item == 0 )                    return 1; // no actual name               
         if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 14.", 0);
         if ( Prs_ManIsChar(p, '[') )
         {
@@ -580,10 +652,11 @@ static inline int Prs_ManReadSignalList2( Prs_Man_t * p, Vec_Int_t * vTemp )
         p->pCur++;
         if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 17.", 0);
         ActItem = Prs_ManReadSignal( p );
-        if ( ActItem == 0 )                 return Prs_ManErrorSet(p, "Cannot read actual name of the instance.", 0);
+        if ( ActItem == 0 )                 return Prs_ManErrorSet(p, "Cannot read actual name of an instance.", 0);
         if ( !Prs_ManIsChar(p, ')') )       return Prs_ManErrorSet(p, "Cannot read \")\" in the instance.", 0);
         p->pCur++;
-        Vec_IntPushTwo( vTemp, FormId, ActItem );
+        if ( ActItem != 1 )
+            Vec_IntPushTwo( vTemp, FormId, ActItem );
         if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 18.", 0);
         if ( Prs_ManIsChar(p, ')') )        break;
         if ( !Prs_ManIsChar(p, ',') )       return Prs_ManErrorSet(p, "Expecting comma in the instance.", 0);
@@ -606,33 +679,111 @@ static inline int Prs_ManReadSignalList2( Prs_Man_t * p, Vec_Int_t * vTemp )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Prs_ManReadDeclaration( Prs_Man_t * p, int Type )
+static inline int Prs_ManReadFunction( Prs_Man_t * p )
 {
-    int i, NameId, RangeId = 0;
-    Vec_Int_t * vNames[4]  = { &p->pNtk->vInputs,  &p->pNtk->vOutputs,  &p->pNtk->vInouts,  &p->pNtk->vWires };
-    Vec_Int_t * vNamesR[4] = { &p->pNtk->vInputsR, &p->pNtk->vOutputsR, &p->pNtk->vInoutsR, &p->pNtk->vWiresR };
-    assert( Type >= PRS_VER_INPUT && Type <= PRS_VER_WIRE );
-    if ( Prs_ManUtilSkipSpaces(p) )                                   return Prs_ManErrorSet(p, "Error number 20.", 0);
-    if ( Prs_ManIsChar(p, '[') && !(RangeId = Prs_ManReadRange(p)) )  return Prs_ManErrorSet(p, "Error number 21.", 0);
-    if ( !Prs_ManReadNameList( p, &p->vTemp, ';' ) )                  return Prs_ManErrorSet(p, "Error number 22.", 0);
-    Vec_IntForEachEntry( &p->vTemp, NameId, i )
+    // this is a hack to read functions produced by ABC Verilog writer
+    p->FuncNameId = p->FuncRangeId = 0;
+    if ( Prs_ManUtilSkipUntilWord( p, "_func_" ) ) return Prs_ManErrorSet(p, "Cannot find \"_func_\" keyword.", 0);
+    p->pCur -= 6;
+    p->FuncNameId = Prs_ManReadName( p );          
+    if ( p->FuncNameId == 0 )                      return Prs_ManErrorSet(p, "Error number 30a.", 0);
+    if ( Prs_ManUtilSkipUntilWord( p, "input" ) )  return Prs_ManErrorSet(p, "Cannot find \"input\" keyword.", 0);
+    if ( Prs_ManUtilSkipSpaces(p) )                return Prs_ManErrorSet(p, "Error number 30b.", 0);
+    if ( Prs_ManIsChar(p, '[') )
+        p->FuncRangeId = Prs_ManReadRange(p);
+    else if ( Prs_ManReadName(p) == PRS_VER_SIGNED ) 
     {
-        Vec_IntPush( vNames[Type - PRS_VER_INPUT], NameId );
-        Vec_IntPush( vNamesR[Type - PRS_VER_INPUT], RangeId );
-        if ( Type < PRS_VER_WIRE )
-            Vec_IntPush( &p->pNtk->vOrder, Abc_Var2Lit2(NameId, Type) );
+        if ( Prs_ManUtilSkipSpaces(p) )            return Prs_ManErrorSet(p, "Error number 30c.", 0);
+        if ( Prs_ManIsChar(p, '[') )
+            p->FuncRangeId = Prs_ManReadRange(p);
     }
+    if ( Prs_ManUtilSkipUntilWord( p, "endfunction" ) ) return Prs_ManErrorSet(p, "Cannot find \"endfunction\" keyword.", 0);
     return 1;
 }
-static inline int Prs_ManReadAssign( Prs_Man_t * p )
+static inline int Prs_ManReadAlways( Prs_Man_t * p )
 {
-    int OutItem, InItem, fCompl = 0, fCompl2 = 0, Oper = 0;
-    // read output name
-    OutItem = Prs_ManReadSignal( p );
-    if ( OutItem == 0 )                     return Prs_ManErrorSet(p, "Cannot read output in assign-statement.", 0);
-    if ( !Prs_ManIsChar(p, '=') )           return Prs_ManErrorSet(p, "Expecting \"=\" in assign-statement.", 0);
-    p->pCur++;
+    // this is a hack to read always-statement representing case-statement
+    int iToken;
+    char * pClose; 
     if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 23.", 0);
+    if ( !Prs_ManIsChar(p, '@') )           return Prs_ManErrorSet(p, "Cannot parse always statement.", 0);
+    p->pCur++;
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 23a.", 0);
+    if ( !Prs_ManIsChar(p, '(') )           return Prs_ManErrorSet(p, "Cannot parse always statement.", 0);
+    pClose = Prs_ManFindClosingParenthesis( p, '(', ')' );
+    if ( pClose == NULL )
+        return Prs_ManErrorSet(p, "Expecting closing parenthesis 1.", 0); 
+    p->pCur = pClose;
+    if ( !Prs_ManIsChar(p, ')') )           return Prs_ManErrorSet(p, "Cannot parse always statement.", 0);
+    p->pCur++;
+    // read begin
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 23a.", 0);
+    iToken = Prs_ManReadName( p );
+    if ( iToken != PRS_VER_BEGIN )          return Prs_ManErrorSet(p, "Cannot read \"begin\" keyword.", 0);
+    // read case
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 23a.", 0);
+    iToken = Prs_ManReadName( p );
+    if ( iToken != PRS_VER_CASE )           return Prs_ManErrorSet(p, "Cannot read \"case\" keyword.", 0);
+    // read control
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 23a.", 0);
+    if ( !Prs_ManIsChar(p, '(') )           return Prs_ManErrorSet(p, "Cannot parse always statement.", 0);
+    p->pCur++;
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 23a.", 0);
+    iToken = Prs_ManReadSignal( p );
+    if ( iToken == 0 )                      return Prs_ManErrorSet(p, "Cannot read output in assign-statement.", 0);
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 23a.", 0);
+    if ( !Prs_ManIsChar(p, ')') )           return Prs_ManErrorSet(p, "Cannot parse always statement.", 0);
+    p->pCur++;
+    // save control
+    Vec_IntClear( &p->vTemp3 );
+    Vec_IntPushTwo( &p->vTemp3, 0, 0 );  // output will go here
+    Vec_IntPushTwo( &p->vTemp3, 0, iToken );
+    // read conditions
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 23a.", 0);
+    if ( !Prs_ManIsDigit(p) )               return Prs_ManErrorSet(p, "Cannot parse always statement.", 0);
+    while ( Prs_ManIsDigit(p) )
+    {
+        while ( Prs_ManIsDigit(p) )
+            p->pCur++;
+        if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 23a.", 0);
+        if ( !Prs_ManIsChar(p, ':') )       return Prs_ManErrorSet(p, "Cannot parse always statement.", 0);
+        p->pCur++;
+        if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 23a.", 0);
+        // read output
+        iToken = Prs_ManReadSignal( p );
+        if ( iToken == 0 )                  return Prs_ManErrorSet(p, "Cannot read output in assign-statement.", 0);
+        if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 23a.", 0);
+        if ( !Prs_ManIsChar(p, '=') )       return Prs_ManErrorSet(p, "Cannot parse always statement.", 0);
+        p->pCur++;
+        // save output
+        Vec_IntWriteEntry( &p->vTemp3, 1, iToken );
+        // read input
+        iToken = Prs_ManReadSignal( p );
+        if ( iToken == 0 )                  return Prs_ManErrorSet(p, "Cannot read output in assign-statement.", 0);
+        if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 23a.", 0);
+        if ( !Prs_ManIsChar(p, ';') )       return Prs_ManErrorSet(p, "Cannot parse always statement.", 0);
+        p->pCur++;
+        if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 23a.", 0);
+        // save input
+        Vec_IntPushTwo( &p->vTemp3, 0, iToken );
+    }
+    // read endcase
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 23a.", 0);
+    iToken = Prs_ManReadName( p );
+    if ( iToken != PRS_VER_ENDCASE )        return Prs_ManErrorSet(p, "Cannot read \"endcase\" keyword.", 0);
+    // read end
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 23a.", 0);
+    iToken = Prs_ManReadName( p );
+    if ( iToken != PRS_VER_END )            return Prs_ManErrorSet(p, "Cannot read \"end\" keyword.", 0);
+    // save binary operator
+    Prs_NtkAddBox( p->pNtk, CBA_BOX_NMUX, 0, &p->vTemp3 );
+    return 1;
+}
+/*
+static inline int Prs_ManReadExpression( Prs_Man_t * p, int OutItem )
+{
+    int InItem, fCompl = 0, fCompl2 = 0, Oper = 0;
+    // read output name
     if ( Prs_ManIsChar(p, '~') ) 
     { 
         fCompl = 1; 
@@ -717,17 +868,248 @@ static inline int Prs_ManReadAssign( Prs_Man_t * p )
     Prs_NtkAddBox( p->pNtk, Oper, 0, &p->vTemp );
     return 1;
 }
+*/
+static inline int Prs_ManReadExpression( Prs_Man_t * p, int OutItem )
+{
+    char * pClose;
+    int Item, Type = CBA_OBJ_NONE;
+    int fRotating = 0;
+
+    // write output name
+    Vec_IntClear( &p->vTemp );
+    Vec_IntPush( &p->vTemp, 0 );
+    Vec_IntPush( &p->vTemp, OutItem );
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 24.", 0);
+    if ( Prs_ManIsChar(p, '(') )
+    {
+        // THIS IS A HACK TO DETECT rotating shifters:  try to find both << and >> on the same line
+        if ( Prs_ManUtilDetectTwo(p, '>', '>') && Prs_ManUtilDetectTwo(p, '<', '<') )
+            fRotating = 1;
+        pClose = Prs_ManFindClosingParenthesis( p, '(', ')' );
+        if ( pClose == NULL )
+            return Prs_ManErrorSet(p, "Expecting closing parenthesis 1.", 0); 
+        *p->pCur = *pClose = ' ';
+    }
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 24.", 0);
+    // read constant or concatenation
+    if ( Prs_ManIsDigit(p) || Prs_ManIsChar(p, '{') )
+    {
+        Item = Prs_ManReadSignal( p );
+        // write constant
+        Vec_IntPush( &p->vTemp, 0 );
+        Vec_IntPush( &p->vTemp, Item );
+        Type = CBA_BOX_BUF;
+    }
+    else if ( Prs_ManIsChar(p, '!') || Prs_ManIsChar(p, '~') || Prs_ManIsChar(p, '@') ||
+              Prs_ManIsChar(p, '&') || Prs_ManIsChar(p, '|') || Prs_ManIsChar(p, '^') || Prs_ManIsChar(p, '-') )
+    {
+        if ( Prs_ManIsChar(p, '!') )
+            Type = CBA_BOX_LNOT;
+        else if ( Prs_ManIsChar(p, '~') )
+            Type = CBA_BOX_INV;
+        else if ( Prs_ManIsChar(p, '@') )
+            Type = CBA_BOX_SQRT;
+        else if ( Prs_ManIsChar(p, '&') )
+            Type = CBA_BOX_RAND;
+        else if ( Prs_ManIsChar(p, '|') )
+            Type = CBA_BOX_ROR;
+        else if ( Prs_ManIsChar(p, '^') )
+            Type = CBA_BOX_RXOR;
+        else if ( Prs_ManIsChar(p, '-') )
+            Type = CBA_BOX_MIN;
+        else assert( 0 );
+        p->pCur++;
+        if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 24.", 0);
+        // skip parentheses
+        if ( Prs_ManIsChar(p, '(') )
+        {
+            pClose = Prs_ManFindClosingParenthesis( p, '(', ')' );
+            if ( pClose == NULL )
+                return Prs_ManErrorSet(p, "Expecting closing parenthesis 2.", 0); 
+            *p->pCur = *pClose = ' ';
+        }
+        if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 24.", 0);
+        // read first name
+        Item = Prs_ManReadSignal( p );
+        if ( Item == 0 )                        return Prs_ManErrorSet(p, "Cannot read name after a unary operator.", 0);
+        Vec_IntPush( &p->vTemp, 0 );
+        Vec_IntPush( &p->vTemp, Item );
+    }
+    else
+    {
+        // read first name
+        Item = Prs_ManReadSignal( p );
+        if ( Item == 0 )                        return Prs_ManErrorSet(p, "Cannot read name after a binary operator.", 0);
+        // check if this is a recent function
+        if ( Abc_Lit2Var2(Item) == p->FuncNameId )
+        {
+            int Status, nInputs, RangeSize;
+            if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 24.", 0);
+            if ( !Prs_ManIsChar(p, '(') )       return Prs_ManErrorSet(p, "Error number 24.", 0);
+            p->pCur++;
+            Status = Prs_ManReadSignalList( p, &p->vTemp, ')', 1 );
+            nInputs = Vec_IntSize(&p->vTemp)/2;
+            RangeSize = p->FuncRangeId ? Ptr_NtkRangeSize(p->pNtk, p->FuncRangeId) : 1;
+            p->FuncNameId = p->FuncRangeId = 0;
+            if ( Status == 0 )                  return 0;
+            if ( nInputs == 1 )
+                Type = CBA_BOX_DEC;
+            else if ( nInputs == RangeSize + 1 )
+                Type = CBA_BOX_SEL;
+            else if ( nInputs == (1 << RangeSize) + 1 )
+                Type = CBA_BOX_NMUX;
+            else                                return Prs_ManErrorSet(p, "Cannot determine word-level operator.", 0);
+            p->pCur++;
+            if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 24.", 0);
+            // save word-level operator
+            Vec_IntInsert( &p->vTemp, 0, 0 );
+            Vec_IntInsert( &p->vTemp, 1, OutItem );
+            Prs_NtkAddBox( p->pNtk, Type, 0, &p->vTemp );
+            return 1;
+        }
+        Vec_IntPush( &p->vTemp, 0 );
+        Vec_IntPush( &p->vTemp, Item );
+        if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 24.", 0);
+        assert( !Prs_ManIsChar(p, '[') );
+
+        // get the next symbol
+        if ( Prs_ManIsChar(p, ',') || Prs_ManIsChar(p, ';') )
+            Type = CBA_BOX_BUF;
+        else if ( Prs_ManIsChar(p, '?') )
+        {
+            p->pCur++;
+            Item = Prs_ManReadSignal( p );
+            if ( Item == 0 )                    return 0;
+            Vec_IntPush( &p->vTemp, 0 );
+            Vec_IntPush( &p->vTemp, Item );
+            if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 24.", 0);
+            if ( !Prs_ManIsChar(p, ':') )       return Prs_ManErrorSet(p, "MUX lacks the colon symbol (:).", 0);
+
+            p->pCur++;
+            Item = Prs_ManReadSignal( p );
+            if ( Item == 0 )                    return 0;
+            Vec_IntPush( &p->vTemp, 0 );
+            Vec_IntPush( &p->vTemp, Item );
+            if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 24.", 0);
+            assert( Vec_IntSize(&p->vTemp) == 8 );
+            //ABC_SWAP( int, Vec_IntArray(&p->vTemp)[3], Vec_IntArray(&p->vTemp)[5] );
+            Type = CBA_BOX_MUX;
+        }
+        else 
+        {
+                 if ( p->pCur[0] == '>' && p->pCur[1] == '>' && p->pCur[2] != '>' )  p->pCur += 2, Type = fRotating ? CBA_BOX_ROTR : CBA_BOX_SHIR;
+            else if ( p->pCur[0] == '>' && p->pCur[1] == '>' && p->pCur[2] == '>' )  p->pCur += 3, Type = CBA_BOX_SHIRA;      
+            else if ( p->pCur[0] == '<' && p->pCur[1] == '<' && p->pCur[2] != '<' )  p->pCur += 2, Type = fRotating ? CBA_BOX_ROTL : CBA_BOX_SHIL;
+            else if ( p->pCur[0] == '<' && p->pCur[1] == '<' && p->pCur[2] == '<' )  p->pCur += 3, Type = CBA_BOX_SHILA;      
+            else if ( p->pCur[0] == '&' && p->pCur[1] != '&'                      )  p->pCur += 1, Type = CBA_BOX_AND;       
+            else if ( p->pCur[0] == '|' && p->pCur[1] != '|'                      )  p->pCur += 1, Type = CBA_BOX_OR;        
+            else if ( p->pCur[0] == '^' && p->pCur[1] != '^'                      )  p->pCur += 1, Type = CBA_BOX_XOR;       
+            else if ( p->pCur[0] == '&' && p->pCur[1] == '&'                      )  p->pCur += 2, Type = CBA_BOX_LAND;     
+            else if ( p->pCur[0] == '|' && p->pCur[1] == '|'                      )  p->pCur += 2, Type = CBA_BOX_LOR;      
+            else if ( p->pCur[0] == '=' && p->pCur[1] == '='                      )  p->pCur += 2, Type = CBA_BOX_EQU;      
+            else if ( p->pCur[0] == '!' && p->pCur[1] == '='                      )  p->pCur += 2, Type = CBA_BOX_NEQU;      
+            else if ( p->pCur[0] == '<' && p->pCur[1] != '='                      )  p->pCur += 1, Type = CBA_BOX_LTHAN;     
+            else if ( p->pCur[0] == '>' && p->pCur[1] != '='                      )  p->pCur += 1, Type = CBA_BOX_MTHAN;     
+            else if ( p->pCur[0] == '<' && p->pCur[1] == '='                      )  p->pCur += 2, Type = CBA_BOX_LETHAN;
+            else if ( p->pCur[0] == '>' && p->pCur[1] == '='                      )  p->pCur += 2, Type = CBA_BOX_METHAN;  
+            else if ( p->pCur[0] == '+'                                           )  p->pCur += 1, Type = CBA_BOX_ADD;       
+            else if ( p->pCur[0] == '-'                                           )  p->pCur += 1, Type = CBA_BOX_SUB;       
+            else if ( p->pCur[0] == '*' && p->pCur[1] != '*'                      )  p->pCur += 1, Type = CBA_BOX_MUL;     
+            else if ( p->pCur[0] == '/'                                           )  p->pCur += 1, Type = CBA_BOX_DIV;        
+            else if ( p->pCur[0] == '%'                                           )  p->pCur += 1, Type = CBA_BOX_MOD;   
+            else if ( p->pCur[0] == '*' && p->pCur[1] == '*'                      )  p->pCur += 2, Type = CBA_BOX_POW;
+            else return Prs_ManErrorSet(p, "Unsupported operation.", 0);
+
+            Item = Prs_ManReadSignal( p );
+            if ( Item == 0 )                    return 0;
+            Vec_IntPush( &p->vTemp, 0 );
+            Vec_IntPush( &p->vTemp, Item );
+            // for adder insert carry-in
+            if ( Type == CBA_BOX_ADD )
+                Vec_IntInsert( &p->vTemp, 2, 0 );
+            if ( Type == CBA_BOX_ADD )
+                Vec_IntInsert( &p->vTemp, 3, 0 );
+        }
+    }
+    if ( Prs_ManUtilSkipSpaces(p) )                              return Prs_ManErrorSet(p, "Error number 24.", 0);
+    // make sure there is nothing left there
+    if ( fRotating )
+    {
+        Prs_ManUtilSkipUntilWord(p, ";");
+        p->pCur--;
+    }
+    else if ( !Prs_ManIsChar(p, ',') && !Prs_ManIsChar(p, ';') ) return Prs_ManErrorSet(p, "Trailing symbols on this line.", 0);
+    // save binary operator
+    Prs_NtkAddBox( p->pNtk, Type, 0, &p->vTemp );
+    return 1;
+}
+static inline int Prs_ManReadDeclaration( Prs_Man_t * p, int Type )
+{
+    int i, Item = 0, NameId, RangeId = 0, fSigned = 0;
+    Vec_Int_t * vNames[4]  = { &p->pNtk->vInputs,  &p->pNtk->vOutputs,  &p->pNtk->vInouts,  &p->pNtk->vWires };
+    Vec_Int_t * vNamesR[4] = { &p->pNtk->vInputsR, &p->pNtk->vOutputsR, &p->pNtk->vInoutsR, &p->pNtk->vWiresR };
+    assert( Type >= PRS_VER_INPUT && Type <= PRS_VER_WIRE );
+    // read first word
+    if ( Prs_ManUtilSkipSpaces(p) )                                       return Prs_ManErrorSet(p, "Error number 20.", 0);
+    if ( Prs_ManIsChar(p, '[') && !(RangeId = Prs_ManReadRange(p)) )      return Prs_ManErrorSet(p, "Error number 21.", 0);
+    Item = Prs_ManReadName(p);
+    if ( Item == PRS_VER_SIGNED )
+    {
+        fSigned = 1;
+        if ( Prs_ManUtilSkipSpaces(p) )                                   return Prs_ManErrorSet(p, "Error number 20.", 0);
+        if ( Prs_ManIsChar(p, '[') && !(RangeId = Prs_ManReadRange(p)) )  return Prs_ManErrorSet(p, "Error number 21.", 0);
+        Item = Prs_ManReadName(p);
+    }
+    if ( Item == PRS_VER_WIRE )
+    {
+        if ( Prs_ManUtilSkipSpaces(p) )                                   return Prs_ManErrorSet(p, "Error number 20.", 0);
+        if ( Prs_ManIsChar(p, '[') && !(RangeId = Prs_ManReadRange(p)) )  return Prs_ManErrorSet(p, "Error number 21.", 0);
+        Item = Prs_ManReadName(p);
+    }
+    // read variable names
+    Vec_IntClear( &p->vTemp3 );
+    while ( 1 )
+    {
+        if ( Item == 0 )                    return Prs_ManErrorSet(p, "Cannot read name in the list.", 0);
+        if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 22a", 0);
+        if ( Item == PRS_VER_WIRE  )
+            continue;
+        Vec_IntPush( &p->vTemp3, Item );
+        if ( Prs_ManIsChar(p, '=') )
+        {
+            if ( Type == PRS_VER_INPUT )    return Prs_ManErrorSet(p, "Input cannot be defined", 0);
+            p->pCur++;
+            if ( Prs_ManUtilSkipSpaces(p) ) return Prs_ManErrorSet(p, "Error number 23.", 0);
+            if ( !Prs_ManReadExpression(p, Abc_Var2Lit2(Item, CBA_PRS_NAME)) ) 
+                return 0;
+        }
+        if ( Prs_ManIsChar(p, ';') )   
+            break;
+        if ( !Prs_ManIsChar(p, ',') )       return Prs_ManErrorSet(p, "Expecting comma in the list.", 0);
+        p->pCur++;
+        if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 22b.", 0);
+        Item = Prs_ManReadName(p);
+    }
+    Vec_IntForEachEntry( &p->vTemp3, NameId, i )
+    {
+        Vec_IntPush( vNames[Type - PRS_VER_INPUT],  NameId );
+        Vec_IntPush( vNamesR[Type - PRS_VER_INPUT], Abc_Var2Lit(RangeId, fSigned) );
+        if ( Type < PRS_VER_WIRE )
+            Vec_IntPush( &p->pNtk->vOrder, Abc_Var2Lit2(NameId, Type) );
+    }
+    return 1;
+}
 static inline int Prs_ManReadInstance( Prs_Man_t * p, int Func )
 {
     int InstId, Status;
-/*
-    static Counter = 0;
-    if ( ++Counter == 7 )
+    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 25.", 0);
+    if ( Prs_ManIsChar(p, '#') )
     {
-        int s=0;
+        p->pCur++;
+        while ( Prs_ManIsDigit(p) )
+            p->pCur++;
+        if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 25.", 0);
     }
-*/
-    if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 25.", 0);
     if ( (InstId = Prs_ManReadName(p)) )
         if (Prs_ManUtilSkipSpaces(p))       return Prs_ManErrorSet(p, "Error number 26.", 0);
     if ( !Prs_ManIsChar(p, '(') )           return Prs_ManErrorSet(p, "Expecting \"(\" in module instantiation.", 0);
@@ -767,6 +1149,7 @@ static inline int Prs_ManReadArguments( Prs_Man_t * p )
     {
         int fEscape = Prs_ManIsChar(p, '\\');
         int iName = Prs_ManReadName( p );
+        int fSigned = 0;
         if ( iName == 0 )                       return Prs_ManErrorSet(p, "Error number 31.", 0);
         if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 32.", 0);
         if ( iName >= PRS_VER_INPUT && iName <= PRS_VER_INOUT && !fEscape ) // declaration
@@ -780,13 +1163,27 @@ static inline int Prs_ManReadArguments( Prs_Man_t * p )
             }
             iName = Prs_ManReadName( p );
             if ( iName == 0 )                   return Prs_ManErrorSet(p, "Error number 35.", 0);
+            if ( iName == PRS_VER_SIGNED )
+            {
+                fSigned = 1;
+                if ( Prs_ManUtilSkipSpaces(p) ) return Prs_ManErrorSet(p, "Error number 32.", 0);
+                if ( Prs_ManIsChar(p, '[') )
+                {
+                    iRange = Prs_ManReadRange(p);
+                    if ( iRange == 0 )              return Prs_ManErrorSet(p, "Error number 33.", 0);
+                    if ( Prs_ManUtilSkipSpaces(p) ) return Prs_ManErrorSet(p, "Error number 34.", 0);
+                }
+                iName = Prs_ManReadName( p );
+                if ( iName == 0 )               return Prs_ManErrorSet(p, "Error number 35.", 0);
+            }
         }
         if ( iType > 0 )
         {
             Vec_IntPush( vSigs[iType - PRS_VER_INPUT], iName );
-            Vec_IntPush( vSigsR[iType - PRS_VER_INPUT], iRange );
+            Vec_IntPush( vSigsR[iType - PRS_VER_INPUT], Abc_Var2Lit(iRange, fSigned) );
             Vec_IntPush( &p->pNtk->vOrder, Abc_Var2Lit2(iName, iType) );
         }
+        if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 36.", 0);
         if ( Prs_ManIsChar(p, ')') )
             break;
         if ( !Prs_ManIsChar(p, ',') )           return Prs_ManErrorSet(p, "Expecting comma in the instance.", 0);
@@ -801,7 +1198,7 @@ static inline int Prs_ManReadArguments( Prs_Man_t * p )
 // 0 = reached end-of-file; 1 = successfully parsed; 2 = recognized as primitive; 3 = failed and skipped; 4 = error (failed and could not skip)
 static inline int Prs_ManReadModule( Prs_Man_t * p )
 {
-    int iToken, Status;
+    int iToken, Status, fAlways = 0;
     if ( p->pNtk != NULL )                  return Prs_ManErrorSet(p, "Parsing previous module is unfinished.", 4);
     if ( Prs_ManUtilSkipSpaces(p) )
     { 
@@ -809,6 +1206,15 @@ static inline int Prs_ManReadModule( Prs_Man_t * p )
         return 0; 
     }
     // read keyword
+    while ( Prs_ManIsChar(p, '`') )
+    {
+        Prs_ManUtilSkipUntilWord(p, "\n");
+        if ( Prs_ManUtilSkipSpaces(p) )
+        { 
+            Prs_ManErrorClear( p );       
+            return 0; 
+        }
+    }
     iToken = Prs_ManReadName( p );
     if ( iToken != PRS_VER_MODULE )         return Prs_ManErrorSet(p, "Cannot read \"module\" keyword.", 4);
     if ( Prs_ManUtilSkipSpaces(p) )         return 4;
@@ -831,9 +1237,10 @@ static inline int Prs_ManReadModule( Prs_Man_t * p )
     p->pCur++;
     if ( Prs_ManUtilSkipSpaces(p) )         return 4;
     // read declarations and instances
-    while ( Prs_ManIsChar(p, ';') )
+    while ( Prs_ManIsChar(p, ';') || fAlways )
     {
-        p->pCur++;
+        if ( !fAlways ) p->pCur++;
+        fAlways = 0;
         if ( Prs_ManUtilSkipSpaces(p) )     return 4;
         iToken = Prs_ManReadName( p );
         if ( iToken == PRS_VER_ENDMODULE )
@@ -842,18 +1249,47 @@ static inline int Prs_ManReadModule( Prs_Man_t * p )
             Prs_ManFinalizeNtk( p );
             return 1;
         }
-        if ( iToken >= PRS_VER_INPUT && iToken <= PRS_VER_WIRE ) // declaration
-            Status = Prs_ManReadDeclaration( p, iToken );
+        if ( iToken >= PRS_VER_INPUT && iToken <= PRS_VER_REG ) // declaration
+            Status = Prs_ManReadDeclaration( p, iToken == PRS_VER_REG ? PRS_VER_WIRE : iToken );
         else if ( iToken == PRS_VER_REG || iToken == PRS_VER_DEFPARAM ) // unsupported keywords
             Status = Prs_ManUtilSkipUntil( p, ';' );
         else // read instance
         {
             if ( iToken == PRS_VER_ASSIGN )
-                Status = Prs_ManReadAssign( p );
+            {
+                // read output name
+                int OutItem = Prs_ManReadSignal( p );
+                if ( OutItem == 0 )                     return Prs_ManErrorSet(p, "Cannot read output in assign-statement.", 0);
+                if ( !Prs_ManIsChar(p, '=') )           return Prs_ManErrorSet(p, "Expecting \"=\" in assign-statement.", 0);
+                p->pCur++;
+                if ( Prs_ManUtilSkipSpaces(p) )         return Prs_ManErrorSet(p, "Error number 23.", 0);
+                // read expression
+                while ( 1 )
+                {
+                    if ( !Prs_ManReadExpression(p, OutItem) )    return 0;
+                    if ( Prs_ManIsChar(p, ';') )
+                        break;
+                    assert( Prs_ManIsChar(p, ',') );
+                    p->pCur++;
+                    if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 23a.", 0);
+                    // read output name
+                    OutItem = Prs_ManReadSignal( p );
+                    if ( OutItem == 0 )                 return Prs_ManErrorSet(p, "Cannot read output in assign-statement.", 0);
+                    if ( !Prs_ManIsChar(p, '=') )       return Prs_ManErrorSet(p, "Expecting \"=\" in assign-statement.", 0);
+                    p->pCur++;
+                    if ( Prs_ManUtilSkipSpaces(p) )     return Prs_ManErrorSet(p, "Error number 23.", 0);
+                }
+            }
+            else if ( iToken == PRS_VER_ALWAYS )
+                Status = Prs_ManReadAlways(p), fAlways = 1;
+            else if ( iToken == PRS_VER_FUNCTION )
+                Status = Prs_ManReadFunction(p), fAlways = 1;
             else
                 Status = Prs_ManReadInstance( p, iToken );
             if ( Status == 0 )
             {
+                return 4;
+
                 if ( Prs_ManUtilSkipUntilWord( p, "endmodule" ) ) return Prs_ManErrorSet(p, "Cannot find \"endmodule\" keyword.", 4);
                 //printf( "Warning! Failed to parse \"%s\". Adding module \"%s\" as blackbox.\n", 
                 //    Abc_NamStr(p->pStrs, iToken), Abc_NamStr(p->pStrs, p->pNtk->iModuleName) );
@@ -1062,7 +1498,7 @@ int Prs_CreateRange( Cba_Ntk_t * p, int iFon, int NameId )
     if ( RangeId == 0 )
         return 1;
     assert( RangeId > 0 );
-    Cba_FonSetRange( p, iFon, RangeId );
+    Cba_FonSetRangeSign( p, iFon, RangeId );
     return Cba_FonRangeSize( p, iFon );
 }
 /*
@@ -1396,7 +1832,7 @@ void Prs_CreateVerilogPio( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
         iObj = Cba_ObjAlloc( p, CBA_OBJ_PI, 0, 1 );
         Cba_ObjSetName( p, iObj, NameId ); // direct name
         iFon = Cba_ObjFon0(p, iObj);
-        Cba_FonSetRange( p, iFon, RangeId );
+        Cba_FonSetRangeSign( p, iFon, RangeId );
         Cba_FonSetName( p, iFon, NameId );
         Cba_NtkSetMap( p, NameId, iObj );
     }
@@ -1482,8 +1918,17 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
     {
         if ( Prs_BoxIsNode(pNtk, i) ) // node
         {
+            int Type = Prs_BoxNtk(pNtk, i);
             int nSigs = Prs_BoxIONum( pNtk, i );
-            iObj = Cba_ObjAlloc( p, Prs_BoxNtk(pNtk, i), nSigs-1, 1 );
+/*
+            int NameId = Abc_Lit2Var2(Vec_IntEntry(vBox, 1));
+            char * pName = Cba_NtkStr( p, NameId );
+            if ( !strcmp(pName, "E_336717") )
+            {
+                int s = 0;
+            }
+*/
+            iObj = Cba_ObjAlloc( p, Type, nSigs-1, Type == CBA_BOX_ADD ? 2 : 1 );
             Prs_CreateSignalOut( p, Cba_ObjFon0(p, iObj), pNtk, Vec_IntEntry(vBox, 1) ); // node output
             //Cba_ObjSetFunc( p, iObj, FuncId );
         }
@@ -1505,7 +1950,7 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
                 nInputs = Cba_NtkPiNum(pBox);
                 nOutputs = Cba_NtkPoNum(pBox);
             }
-            else if ( Type == CBA_BOX_ADD )
+            else if ( Type == CBA_BOX_ADD || Type == CBA_BOX_DFFCPL )
                 nOutputs = 2;
             else if ( Type == CBA_BOX_NMUX )
             {
@@ -1717,8 +2162,8 @@ int Prs_CreateVerilogNtk( Cba_Ntk_t * p, Prs_Ntk_t * pNtk )
         Cba_ObjSetFinFon( p, iObj, 0, iFon );
         if ( RangeId )
         {
-            assert( Cba_NtkRangeLeft(p, RangeId)  == Cba_FonLeft(p, iFon) );
-            assert( Cba_NtkRangeRight(p, RangeId) == Cba_FonRight(p, iFon) );
+            assert( Cba_NtkRangeLeft(p, Abc_Lit2Var(RangeId))  == Cba_FonLeft(p, iFon) );
+            assert( Cba_NtkRangeRight(p, Abc_Lit2Var(RangeId)) == Cba_FonRight(p, iFon) );
         }
     }
     return 0;
diff --git a/src/base/cba/cbaWriteVer.c b/src/base/cba/cbaWriteVer.c
index b21b9f7e..cabc8111 100644
--- a/src/base/cba/cbaWriteVer.c
+++ b/src/base/cba/cbaWriteVer.c
@@ -34,6 +34,93 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
+  
+  Synopsis    []  
+  
+  Description []  
+                 
+  SideEffects []  
+  
+  SeeAlso     []  
+  
+***********************************************************************/
+void Cba_ManCreatePrimMap( char ** pMap )
+{
+    memset( pMap, 0, sizeof(char *) * CBA_BOX_LAST );
+
+    pMap[ CBA_BOX_SLICE  ] = "sli";
+    pMap[ CBA_BOX_CATIN  ] = "icc";
+    pMap[ CBA_BOX_CATOUT ] = "occ";
+
+    pMap[ CBA_BOX_BUF    ] = "";
+    pMap[ CBA_BOX_INV    ] = "~";
+    pMap[ CBA_BOX_AND    ] = "&"; 
+    pMap[ CBA_BOX_NAND   ] = "&"; 
+    pMap[ CBA_BOX_OR     ] = "|"; 
+    pMap[ CBA_BOX_NOR    ] = "|"; 
+    pMap[ CBA_BOX_XOR    ] = "^"; 
+    pMap[ CBA_BOX_XNOR   ] = "^"; 
+    pMap[ CBA_BOX_SHARP  ] = "&"; 
+    pMap[ CBA_BOX_SHARPL ] = "&"; 
+    pMap[ CBA_BOX_MUX    ] = "?"; 
+    pMap[ CBA_BOX_MAJ    ] = NULL; 
+    pMap[ CBA_BOX_RAND   ] = "&"; 
+    pMap[ CBA_BOX_RNAND  ] = "~&"; 
+    pMap[ CBA_BOX_ROR    ] = "|"; 
+    pMap[ CBA_BOX_RNOR   ] = "~|"; 
+    pMap[ CBA_BOX_RXOR   ] = "^"; 
+    pMap[ CBA_BOX_RXNOR  ] = "~^"; 
+    pMap[ CBA_BOX_LNOT   ] = "!"; 
+    pMap[ CBA_BOX_LAND   ] = "&&"; 
+    pMap[ CBA_BOX_LNAND  ] = NULL; 
+    pMap[ CBA_BOX_LOR    ] = "||"; 
+    pMap[ CBA_BOX_LNOR   ] = NULL; 
+    pMap[ CBA_BOX_LXOR   ] = "^^"; 
+    pMap[ CBA_BOX_LXNOR  ] = NULL; 
+    pMap[ CBA_BOX_NMUX   ] = "nmux"; 
+    pMap[ CBA_BOX_SEL    ] = "sel"; 
+    pMap[ CBA_BOX_PSEL   ] = NULL; 
+    pMap[ CBA_BOX_ENC    ] = NULL; 
+    pMap[ CBA_BOX_PENC   ] = NULL; 
+    pMap[ CBA_BOX_DEC    ] = "dec"; 
+    pMap[ CBA_BOX_EDEC   ] = NULL; 
+    pMap[ CBA_BOX_ADD    ] = "+"; 
+    pMap[ CBA_BOX_SUB    ] = "-"; 
+    pMap[ CBA_BOX_MUL    ] = "*"; 
+    pMap[ CBA_BOX_DIV    ] = "/"; 
+    pMap[ CBA_BOX_MOD    ] = "%"; 
+    pMap[ CBA_BOX_REM    ] = "%"; 
+    pMap[ CBA_BOX_POW    ] = "**"; 
+    pMap[ CBA_BOX_MIN    ] = "-"; 
+    pMap[ CBA_BOX_SQRT   ] = "@"; 
+    pMap[ CBA_BOX_ABS    ] = NULL; 
+    pMap[ CBA_BOX_LTHAN  ] = "<"; 
+    pMap[ CBA_BOX_LETHAN ] = "<="; 
+    pMap[ CBA_BOX_METHAN ] = ">="; 
+    pMap[ CBA_BOX_MTHAN  ] = ">"; 
+    pMap[ CBA_BOX_EQU    ] = "=="; 
+    pMap[ CBA_BOX_NEQU   ] = "!="; 
+    pMap[ CBA_BOX_SHIL   ] = "<<"; 
+    pMap[ CBA_BOX_SHIR   ] = ">>"; 
+    pMap[ CBA_BOX_SHILA  ] = "<<<"; 
+    pMap[ CBA_BOX_SHIRA  ] = ">>>"; 
+    pMap[ CBA_BOX_ROTL   ] = "rotL"; 
+    pMap[ CBA_BOX_ROTR   ] = "rotR"; 
+
+    pMap[ CBA_BOX_TRI    ] = "tri";
+    pMap[ CBA_BOX_RAM    ] = "ram";
+    pMap[ CBA_BOX_RAMR   ] = "ramR";
+    pMap[ CBA_BOX_RAMW   ] = "ramW";
+    pMap[ CBA_BOX_RAMWC  ] = "ramWC";
+    pMap[ CBA_BOX_RAMBOX ] = "ramBox";
+
+    pMap[ CBA_BOX_LATCH  ] = "lat";
+    pMap[ CBA_BOX_LATCHRS] = "latrs";
+    pMap[ CBA_BOX_DFF    ] = "dff";
+    pMap[ CBA_BOX_DFFRS  ] = "dffrs";
+}
+
+/**Function*************************************************************
 
   Synopsis    [Writing parser state into a file.]
 
@@ -115,26 +202,59 @@ static void Prs_ManWriteVerilogMux( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vSi
         fprintf( pFile, "%s", pStrs[i/2] );
     }
 }
-static void Prs_ManWriteVerilogBoxes( FILE * pFile, Prs_Ntk_t * p )
+static void Prs_ManWriteVerilogBoxes( FILE * pFile, Prs_Ntk_t * p, char ** pTypeNames )
 {
-    Vec_Int_t * vBox; int i;
+    Vec_Int_t * vBox; int i, k;
     Prs_NtkForEachBox( p, vBox, i )
     {
         Cba_ObjType_t NtkId = Prs_BoxNtk(p, i);
         //char * pNtkName = Prs_NtkStr(p, Prs_BoxName(p, i));
         if ( NtkId == CBA_BOX_MUX )
             Prs_ManWriteVerilogMux( pFile, p, vBox );
-        else if ( Prs_BoxIsNode(p, i) ) // node   ------- check order of fanins
+        else if ( Prs_BoxIsNode(p, i) ) // node
         {
-            fprintf( pFile, "  %s (", Ptr_TypeToName(NtkId) );
-            Prs_ManWriteVerilogArray( pFile, p, vBox, 1 );
-            fprintf( pFile, ");\n" );
+            fprintf( pFile, "  assign " );
+            Prs_ManWriteVerilogSignal( pFile, p, Vec_IntEntry(vBox, 1) );
+            fprintf( pFile, " = " );
+            if ( Cba_TypeIsUnary(NtkId) )
+            {
+                fprintf( pFile, "%s", pTypeNames[NtkId] );
+                Prs_ManWriteVerilogSignal( pFile, p, Vec_IntEntry(vBox, 3) );
+            }
+            else if ( NtkId == CBA_BOX_NMUX )
+            {
+                Prs_ManWriteVerilogSignal( pFile, p, Vec_IntEntry(vBox, 3) );
+                fprintf( pFile, " ? " );
+                for ( k = 5; k < Vec_IntSize(vBox); k += 2 )
+                {
+                    if ( k > 5 ) fprintf( pFile, " : " );
+                    Prs_ManWriteVerilogSignal( pFile, p, Vec_IntEntry(vBox, k) );
+                }
+            }
+            else if ( NtkId == CBA_BOX_ADD )
+            {
+                if ( Vec_IntEntry(vBox, 3) )
+                {
+                    Prs_ManWriteVerilogSignal( pFile, p, Vec_IntEntry(vBox, 3) );
+                    fprintf( pFile, " %s ", pTypeNames[NtkId] );
+                }
+                Prs_ManWriteVerilogSignal( pFile, p, Vec_IntEntry(vBox, 5) );
+                fprintf( pFile, " %s ", pTypeNames[NtkId] );
+                Prs_ManWriteVerilogSignal( pFile, p, Vec_IntEntry(vBox, 7) );
+            }
+            else
+            {
+                Prs_ManWriteVerilogSignal( pFile, p, Vec_IntEntry(vBox, 3) );
+                fprintf( pFile, " %s ", pTypeNames[NtkId] );
+                Prs_ManWriteVerilogSignal( pFile, p, Vec_IntEntry(vBox, 5) );
+            }
+            fprintf( pFile, ";\n" );
         }
         else // box
         {
-            fprintf( pFile, "  %s %s (", Prs_NtkStr(p, NtkId), Prs_BoxName(p, i) ? Prs_NtkStr(p, Prs_BoxName(p, i)) : "" );
+            fprintf( pFile, "  %s %s ( ", Prs_NtkStr(p, NtkId), Prs_BoxName(p, i) ? Prs_NtkStr(p, Prs_BoxName(p, i)) : "" );
             Prs_ManWriteVerilogArray2( pFile, p, vBox );
-            fprintf( pFile, ");\n" );
+            fprintf( pFile, " );\n" );
         }
     }
 }
@@ -147,7 +267,7 @@ static void Prs_ManWriteVerilogIos( FILE * pFile, Prs_Ntk_t * p, int SigType )
     if ( SigType == 3 )
         fprintf( pFile, "\n" );
     Vec_IntForEachEntryTwo( vSigs[SigType], vSigsR[SigType], NameId, RangeId, i )
-        fprintf( pFile, "  %s %s%s;\n", pSigNames[SigType], RangeId ? Prs_ManWriteRange(p, RangeId, 0) : "", Prs_NtkStr(p, NameId) );
+        fprintf( pFile, "  %s %s%s%s;\n", pSigNames[SigType], Abc_LitIsCompl(RangeId) ? "signed " : "", RangeId ? Prs_ManWriteRange(p, Abc_Lit2Var(RangeId), 0) : "", Prs_NtkStr(p, NameId) );
 }
 static void Prs_ManWriteVerilogIoOrder( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t * vOrder )
 {
@@ -155,7 +275,7 @@ static void Prs_ManWriteVerilogIoOrder( FILE * pFile, Prs_Ntk_t * p, Vec_Int_t *
     Vec_IntForEachEntry( vOrder, NameId, i )
         fprintf( pFile, "%s%s", Prs_NtkStr(p, Abc_Lit2Var2(NameId)), i == Vec_IntSize(vOrder) - 1 ? "" : ", " );
 }
-static void Prs_ManWriteVerilogNtk( FILE * pFile, Prs_Ntk_t * p )
+static void Prs_ManWriteVerilogNtk( FILE * pFile, Prs_Ntk_t * p, char ** pTypeNames )
 {
     int s;
     // write header
@@ -167,11 +287,12 @@ static void Prs_ManWriteVerilogNtk( FILE * pFile, Prs_Ntk_t * p )
         Prs_ManWriteVerilogIos( pFile, p, s );
     fprintf( pFile, "\n" );
     // write objects
-    Prs_ManWriteVerilogBoxes( pFile, p );
+    Prs_ManWriteVerilogBoxes( pFile, p, pTypeNames );
     fprintf( pFile, "endmodule\n\n" );
 }
 void Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * vPrs )
 {
+    char * pTypeNames[CBA_BOX_LAST];
     Prs_Ntk_t * pNtk = Prs_ManRoot(vPrs); int i;
     FILE * pFile = fopen( pFileName, "wb" );
     if ( pFile == NULL )
@@ -179,99 +300,16 @@ void Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * vPrs )
         printf( "Cannot open output file \"%s\".\n", pFileName );
         return;
     }
+    Cba_ManCreatePrimMap( pTypeNames );
     fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", Prs_NtkStr(pNtk, pNtk->iModuleName), Extra_TimeStamp() );
     Vec_PtrForEachEntry( Prs_Ntk_t *, vPrs, pNtk, i )
-        Prs_ManWriteVerilogNtk( pFile, pNtk );
+        Prs_ManWriteVerilogNtk( pFile, pNtk, pTypeNames );
     fclose( pFile );
 }
 
 
 
 
-/**Function*************************************************************
-  
-  Synopsis    []  
-  
-  Description []  
-                 
-  SideEffects []  
-  
-  SeeAlso     []  
-  
-***********************************************************************/
-void Cba_ManCreatePrimMap( char ** pMap )
-{
-    memset( pMap, 0, sizeof(char *) * CBA_BOX_LAST );
-
-    pMap[ CBA_BOX_SLICE  ] = "sli";
-    pMap[ CBA_BOX_CATIN  ] = "icc";
-    pMap[ CBA_BOX_CATOUT ] = "occ";
-
-    pMap[ CBA_BOX_BUF    ] = "";
-    pMap[ CBA_BOX_INV    ] = "~";
-    pMap[ CBA_BOX_AND    ] = "&"; 
-    pMap[ CBA_BOX_NAND   ] = "&"; 
-    pMap[ CBA_BOX_OR     ] = "|"; 
-    pMap[ CBA_BOX_NOR    ] = "|"; 
-    pMap[ CBA_BOX_XOR    ] = "^"; 
-    pMap[ CBA_BOX_XNOR   ] = "^"; 
-    pMap[ CBA_BOX_SHARP  ] = "&"; 
-    pMap[ CBA_BOX_SHARPL ] = "&"; 
-    pMap[ CBA_BOX_MUX    ] = "?"; 
-    pMap[ CBA_BOX_MAJ    ] = NULL; 
-    pMap[ CBA_BOX_RAND   ] = "&"; 
-    pMap[ CBA_BOX_RNAND  ] = "~&"; 
-    pMap[ CBA_BOX_ROR    ] = "|"; 
-    pMap[ CBA_BOX_RNOR   ] = "~|"; 
-    pMap[ CBA_BOX_RXOR   ] = "^"; 
-    pMap[ CBA_BOX_RXNOR  ] = "~^"; 
-    pMap[ CBA_BOX_LNOT   ] = "!"; 
-    pMap[ CBA_BOX_LAND   ] = "&&"; 
-    pMap[ CBA_BOX_LNAND  ] = NULL; 
-    pMap[ CBA_BOX_LOR    ] = "||"; 
-    pMap[ CBA_BOX_LNOR   ] = NULL; 
-    pMap[ CBA_BOX_LXOR   ] = "^^"; 
-    pMap[ CBA_BOX_LXNOR  ] = NULL; 
-    pMap[ CBA_BOX_NMUX   ] = "nmux"; 
-    pMap[ CBA_BOX_SEL    ] = "sel"; 
-    pMap[ CBA_BOX_PSEL   ] = NULL; 
-    pMap[ CBA_BOX_ENC    ] = NULL; 
-    pMap[ CBA_BOX_PENC   ] = NULL; 
-    pMap[ CBA_BOX_DEC    ] = "dec"; 
-    pMap[ CBA_BOX_EDEC   ] = NULL; 
-    pMap[ CBA_BOX_ADD    ] = "+"; 
-    pMap[ CBA_BOX_SUB    ] = "-"; 
-    pMap[ CBA_BOX_MUL    ] = "*"; 
-    pMap[ CBA_BOX_DIV    ] = "/"; 
-    pMap[ CBA_BOX_MOD    ] = NULL; 
-    pMap[ CBA_BOX_REM    ] = "%%"; 
-    pMap[ CBA_BOX_POW    ] = "**"; 
-    pMap[ CBA_BOX_MIN    ] = "-"; 
-    pMap[ CBA_BOX_ABS    ] = NULL; 
-    pMap[ CBA_BOX_LTHAN  ] = "<"; 
-    pMap[ CBA_BOX_LETHAN ] = "<="; 
-    pMap[ CBA_BOX_METHAN ] = ">="; 
-    pMap[ CBA_BOX_MTHAN  ] = ">"; 
-    pMap[ CBA_BOX_EQU    ] = "=="; 
-    pMap[ CBA_BOX_NEQU   ] = "!="; 
-    pMap[ CBA_BOX_SHIL   ] = "<<"; 
-    pMap[ CBA_BOX_SHIR   ] = ">>"; 
-    pMap[ CBA_BOX_ROTL   ] = "rotL"; 
-    pMap[ CBA_BOX_ROTR   ] = "rotR"; 
-
-    pMap[ CBA_BOX_TRI    ] = "tri";
-    pMap[ CBA_BOX_RAM    ] = "ram";
-    pMap[ CBA_BOX_RAMR   ] = "ramR";
-    pMap[ CBA_BOX_RAMW   ] = "ramW";
-    pMap[ CBA_BOX_RAMWC  ] = "ramWC";
-    pMap[ CBA_BOX_RAMBOX ] = "ramBox";
-
-    pMap[ CBA_BOX_LATCH  ] = "lat";
-    pMap[ CBA_BOX_LATCHRS] = "latrs";
-    pMap[ CBA_BOX_DFF    ] = "dff";
-    pMap[ CBA_BOX_DFFRS  ] = "dffrs";
-}
-
 
 static inline int Cba_NameIsLegalInVerilog( char * pName, int NameId )
 {
@@ -333,8 +371,9 @@ void Cba_ManWriteFonRange( Cba_Ntk_t * p, int iFon )
     Vec_Str_t * vStr = &p->pDesign->vOut;
     if ( !iFon || Cba_FonIsConst(iFon) || (Cba_FonRangeSize(p, iFon) == 1 && Cba_FonRight(p, iFon) == 0) )
         return;
+    if ( Cba_FonSigned(p, iFon) )
+        Vec_StrPrintF( vStr, "signed " );
     Vec_StrPrintF( vStr, "[%d:%d] ", Cba_FonLeft(p, iFon), Cba_FonRight(p, iFon) );
-
 }
 void Cba_ManWriteFonName( Cba_Ntk_t * p, int iFon, int fInlineConcat, int fInput )
 {
@@ -732,6 +771,47 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
             Cba_ManWriteFonName( p, iFonD, fInlineConcat, 0 );
             Vec_StrPrintStr( vStr, ";" );
         }
+        else if ( Type == CBA_BOX_DFFCPL )
+        {
+            // CPL_FF#32 inst_reg( .d(s1), .arstval(s2), .arst(s3), .clk(s4), .q(s5), .qbar(s6) );
+            int iFon0 = Cba_ObjFon0(p, iObj);
+            int iFon1 = Cba_ObjFon(p, iObj, 1);
+            int Range = Cba_FonRangeSize( p, iFon0 );
+            if ( !Vec_BitEntry(vPoFons, iFon0) )
+            {
+                Vec_StrPrintStr( vStr, "  wire " );
+                Cba_ManWriteFonRange( p, iFon0 );
+                Cba_ManWriteFonName( p, iFon0, 0, 0 );
+                Vec_StrPrintStr( vStr, ";\n" );
+            }
+            if ( !Vec_BitEntry(vPoFons, iFon1) && Cba_FonName(p, iFon1) )
+            {
+                Vec_StrPrintStr( vStr, "  wire " );
+                Cba_ManWriteFonRange( p, iFon1 );
+                Cba_ManWriteFonName( p, iFon1, 0, 0 );
+                Vec_StrPrintStr( vStr, ";\n" );
+            }
+            Vec_StrPrintStr( vStr, "  CPL_FF" );
+            if ( Range > 1 )
+                Vec_StrPrintF( vStr, "#%d", Range );
+            Vec_StrPrintStr( vStr, " " );
+            if ( Cba_ObjName(p, iObj) )
+                Vec_StrPrintStr( vStr, Cba_ObjGetName(p, iObj) );
+            Vec_StrPrintStr( vStr, " ( .d(" );
+            Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 0), fInlineConcat, 0 );
+            Vec_StrPrintStr( vStr, "), .arstval(" );
+            Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 1), fInlineConcat, 0 );
+            Vec_StrPrintStr( vStr, "), .arst(" );
+            Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 2), fInlineConcat, 0 );
+            Vec_StrPrintStr( vStr, "), .clk(" );
+            Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 3), fInlineConcat, 0 );
+            Vec_StrPrintStr( vStr, "), .q(" );
+            Cba_ManWriteFonName( p, iFon0, fInlineConcat, 0 );
+            Vec_StrPrintStr( vStr, "), .qbar(" );
+            if ( Cba_FonName(p, iFon1) )
+                Cba_ManWriteFonName( p, iFon1, fInlineConcat, 0 );
+            Vec_StrPrintStr( vStr, ") );" );
+        }
         else if ( Type == CBA_BOX_ADD )
         {
             int iFon0 = Cba_ObjFon0(p, iObj);
@@ -772,7 +852,7 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
                 Vec_StrPrintStr( vStr, " = " );
             }
             // write carry-in
-            if ( Cba_ObjFinFon(p, iObj, 0) != Cba_FonFromConst(1) )
+            if ( Cba_ObjFinFon(p, iObj, 0) && Cba_ObjFinFon(p, iObj, 0) != Cba_FonFromConst(1) )
             {
                 Vec_StrPush( vStr, ' ' );
                 Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 0), fInlineConcat, 0 );
@@ -808,6 +888,33 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
                 Vec_StrPrintStr( vStr, " : " );
                 Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 2), fInlineConcat, 0 );
             }
+            else if ( Type == CBA_BOX_ROTL || Type == CBA_BOX_ROTR )
+            {
+                //  wire [27:0] s4960 = (s57 >> 17) | (s57 << 11);
+                int Range = Cba_FonRangeSize( p, Cba_ObjFon0(p, iObj) );
+                int iFinFon1 = Cba_ObjFinFon(p, iObj, 1);
+                Vec_StrPush( vStr, '(' );
+                Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 0), fInlineConcat, 0 );
+                Vec_StrPrintStr( vStr, Type == CBA_BOX_ROTL ? " << " : " >> " );
+                if ( Cba_FonIsConst(iFinFon1) )
+                    Vec_StrPrintNum( vStr, Cba_FonConst(iFinFon1) );
+                else
+                    Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 1), fInlineConcat, 0 );
+                Vec_StrPrintStr( vStr, ") | (" );
+                Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 0), fInlineConcat, 0 );
+                Vec_StrPrintStr( vStr, Type == CBA_BOX_ROTL ? " >> " : " << " );
+                if ( Cba_FonIsConst(iFinFon1) )
+                    Vec_StrPrintNum( vStr, Range - Cba_FonConst(iFinFon1) );
+                else
+                {
+                    Vec_StrPush( vStr, '(' );
+                    Vec_StrPrintNum( vStr, Range );
+                    Vec_StrPrintStr( vStr, " - " );
+                    Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 1), fInlineConcat, 0 );
+                    Vec_StrPush( vStr, ')' );
+                }
+                Vec_StrPush( vStr, ')' );
+            }
             else if ( Type == CBA_BOX_LTHAN )
             {
                 int fLessThan = (Cba_ObjFinFon(p, iObj, 0) == Cba_FonFromConst(1)); // const0
@@ -826,7 +933,6 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
             else if ( Cba_NtkTypeName(p, Type) ) // binary operation
             {
                 int fCompl = (Type == CBA_BOX_NAND || Type == CBA_BOX_NOR || Type == CBA_BOX_XNOR);
-                Vec_StrPush( vStr, ' ' );
                 if ( fCompl )
                     Vec_StrPrintStr( vStr, "!(" );
                 Cba_ManWriteFonName( p, Cba_ObjFinFon(p, iObj, 0), fInlineConcat, 0 );
@@ -839,8 +945,9 @@ void Cba_ManWriteVerilogNtk( Cba_Ntk_t * p, int fInlineConcat )
             }
             else // unknown
             {
+                char * pName = Cba_FonGetName(p, Cba_ObjFon0(p, iObj));
                 Vec_StrPrintStr( vStr, "<unknown operator>" );
-                printf( "Cba_ManWriteVerilog(): In module \"%s\", cannot write object \"%s\".\n", Cba_NtkName(p), Cba_ObjGetName(p, iObj) );
+                printf( "Cba_ManWriteVerilog(): In module \"%s\", cannot write object \"%s\" with output name \"%s\".\n", Cba_NtkName(p), Cba_ObjGetName(p, iObj), pName );
             }
             Vec_StrPush( vStr, ';' );
         }