Improvements to word-level Verilog parser.

src/base/wlc/wlc.h

@@ -42,8 +42,8 @@ ABC_NAMESPACE_HEADER_START
 // object types
 typedef enum { 
     WLC_OBJ_NONE = 0,      // 00: unknown
-    WLC_OBJ_PI,            // 01: primary input terminal
-    WLC_OBJ_PO,            // 02: primary output terminal
+    WLC_OBJ_PI,            // 01: primary input 
+    WLC_OBJ_PO,            // 02: primary output 
     WLC_OBJ_BO,            // 03: box output
     WLC_OBJ_BI,            // 04: box input
     WLC_OBJ_FF,            // 05: flop
@@ -54,34 +54,37 @@ typedef enum {
     WLC_OBJ_SHIFT_RA,      // 10: shift right (arithmetic)
     WLC_OBJ_SHIFT_L,       // 11: shift left
     WLC_OBJ_SHIFT_LA,      // 12: shift left (arithmetic)
-    WLC_OBJ_BIT_NOT,       // 13: bitwise NOT
-    WLC_OBJ_BIT_AND,       // 14: bitwise AND
-    WLC_OBJ_BIT_OR,        // 15: bitwise OR
-    WLC_OBJ_BIT_XOR,       // 16: bitwise XOR
-    WLC_OBJ_BIT_SELECT,    // 17: bit selection
-    WLC_OBJ_BIT_CONCAT,    // 18: bit concatenation
-    WLC_OBJ_BIT_ZEROPAD,   // 19: zero padding
-    WLC_OBJ_BIT_SIGNEXT,   // 20: sign extension
-    WLC_OBJ_LOGIC_NOT,     // 21: logic NOT
-    WLC_OBJ_LOGIC_AND,     // 22: logic AND
-    WLC_OBJ_LOGIC_OR,      // 23: logic OR
-    WLC_OBJ_COMP_EQU,      // 24: compare equal
-    WLC_OBJ_COMP_NOT,      // 25: compare not equal
-    WLC_OBJ_COMP_LESS,     // 26: compare less
-    WLC_OBJ_COMP_MORE,     // 27: compare more
-    WLC_OBJ_COMP_LESSEQU,  // 28: compare less or equal
-    WLC_OBJ_COMP_MOREEQU,  // 29: compare more or equal
-    WLC_OBJ_REDUCT_AND,    // 30: reduction AND
-    WLC_OBJ_REDUCT_OR,     // 31: reduction OR
-    WLC_OBJ_REDUCT_XOR,    // 32: reduction XOR
-    WLC_OBJ_ARI_ADD,       // 33: arithmetic addition
-    WLC_OBJ_ARI_SUB,       // 34: arithmetic subtraction
-    WLC_OBJ_ARI_MULTI,     // 35: arithmetic multiplier
-    WLC_OBJ_ARI_DIVIDE,    // 36: arithmetic division
-    WLC_OBJ_ARI_MODULUS,   // 37: arithmetic modulus
-    WLC_OBJ_ARI_POWER,     // 38: arithmetic power
-    WLC_OBJ_TABLE,         // 39: arithmetic power
-    WLC_OBJ_NUMBER         // 40: unused
+    WLC_OBJ_ROTATE_R,      // 13: rotate right
+    WLC_OBJ_ROTATE_L,      // 14: rotate left
+    WLC_OBJ_BIT_NOT,       // 15: bitwise NOT
+    WLC_OBJ_BIT_AND,       // 16: bitwise AND
+    WLC_OBJ_BIT_OR,        // 17: bitwise OR
+    WLC_OBJ_BIT_XOR,       // 18: bitwise XOR
+    WLC_OBJ_BIT_SELECT,    // 19: bit selection
+    WLC_OBJ_BIT_CONCAT,    // 20: bit concatenation
+    WLC_OBJ_BIT_ZEROPAD,   // 21: zero padding
+    WLC_OBJ_BIT_SIGNEXT,   // 22: sign extension
+    WLC_OBJ_LOGIC_NOT,     // 23: logic NOT
+    WLC_OBJ_LOGIC_AND,     // 24: logic AND
+    WLC_OBJ_LOGIC_OR,      // 25: logic OR
+    WLC_OBJ_COMP_EQU,      // 26: compare equal
+    WLC_OBJ_COMP_NOTEQU,   // 27: compare not equal
+    WLC_OBJ_COMP_LESS,     // 28: compare less
+    WLC_OBJ_COMP_MORE,     // 29: compare more
+    WLC_OBJ_COMP_LESSEQU,  // 30: compare less or equal
+    WLC_OBJ_COMP_MOREEQU,  // 31: compare more or equal
+    WLC_OBJ_REDUCT_AND,    // 32: reduction AND
+    WLC_OBJ_REDUCT_OR,     // 33: reduction OR
+    WLC_OBJ_REDUCT_XOR,    // 34: reduction XOR
+    WLC_OBJ_ARI_ADD,       // 35: arithmetic addition
+    WLC_OBJ_ARI_SUB,       // 36: arithmetic subtraction
+    WLC_OBJ_ARI_MULTI,     // 37: arithmetic multiplier
+    WLC_OBJ_ARI_DIVIDE,    // 38: arithmetic division
+    WLC_OBJ_ARI_MODULUS,   // 39: arithmetic modulus
+    WLC_OBJ_ARI_POWER,     // 40: arithmetic power
+    WLC_OBJ_ARI_MINUS,     // 41: arithmetic minus
+    WLC_OBJ_TABLE,         // 42: bit table
+    WLC_OBJ_NUMBER         // 43: unused
 } Wlc_ObjType_t;
 
 
@@ -89,9 +92,7 @@ typedef enum {
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Wlc_Ntk_t_  Wlc_Ntk_t;
 typedef struct Wlc_Obj_t_  Wlc_Obj_t;
-
 struct Wlc_Obj_t_ // 16 bytes
 {
     unsigned               Type    :  6;       // node type
@@ -104,6 +105,7 @@ struct Wlc_Obj_t_ // 16 bytes
             int *          pFanins[1]; };
 };
 
+typedef struct Wlc_Ntk_t_  Wlc_Ntk_t;
 struct Wlc_Ntk_t_ 
 {
     char *                 pName;              // model name
@@ -163,6 +165,7 @@ static inline int          Wlc_ObjRangeEnd( Wlc_Obj_t * p )
 static inline int          Wlc_ObjRangeBeg( Wlc_Obj_t * p )                       { assert(p->Type == WLC_OBJ_BIT_SELECT); return p->Fanins[1] & 0xFFFF;  }
 static inline int *        Wlc_ObjConstValue( Wlc_Obj_t * p )                     { assert(p->Type == WLC_OBJ_CONST);      return Wlc_ObjFanins(p);       }
 static inline int          Wlc_ObjTableId( Wlc_Obj_t * p )                        { assert(p->Type == WLC_OBJ_TABLE);      return p->Fanins[1];           }
+static inline word *       Wlc_ObjTable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )        { return (word *)Vec_PtrEntry( p->vTables, Wlc_ObjTableId(pObj) );      }
 
 static inline void         Wlc_NtkCleanCopy( Wlc_Ntk_t * p )                      { Vec_IntFill( &p->vCopies, p->nObjsAlloc, 0 );                         }
 static inline int          Wlc_NtkHasCopy( Wlc_Ntk_t * p )                        { return Vec_IntSize( &p->vCopies ) > 0;                                }

src/base/wlc/wlcBlast.c

@@ -33,7 +33,7 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Helper functions.]
 
   Description []
                
@@ -54,7 +54,87 @@ int Wlc_NtkPrepareBits( Wlc_Ntk_t * p )
     }
     return nBits;
 }
-int Wlc_NtkComputeReduction( Gia_Man_t * pNew, int * pFans, int nFans, int Type )
+int * Wlc_VecCopy( Vec_Int_t * vOut, int * pArray, int nSize )
+{
+    int i; Vec_IntClear( vOut );
+    for( i = 0; i < nSize; i++) 
+        Vec_IntPush( vOut, pArray[i] );
+    return Vec_IntArray( vOut );
+}
+int * Wlc_VecLoadFanins( Vec_Int_t * vOut, int * pFanins, int nFanins, int nTotal, int fSigned )
+{
+    int Fill = fSigned ? pFanins[nFanins-1] : 0;
+    int i; Vec_IntClear( vOut );
+    assert( nFanins <= nTotal );
+    for( i = 0; i < nTotal; i++) 
+        Vec_IntPush( vOut, i < nFanins ? pFanins[i] : Fill );
+    return Vec_IntArray( vOut );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Bit blasting for specific operations.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_BlastShiftRight( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int nShift, int fSticky, Vec_Int_t * vRes )
+{
+    int * pRes = Wlc_VecCopy( vRes, pNum, nNum );
+    int Fill = fSticky ? pNum[nNum-1] : 0;
+    int i, j, fShort = 0;
+    for( i = 0; i < nShift; i++ ) 
+        for( j = 0; j < nNum - fSticky; j++ ) 
+        {
+            if( fShort || j + (1<<i) >= nNum ) 
+            {
+                pRes[j] = Gia_ManHashMux( pNew, pShift[i], Fill, pRes[j] );
+                if ( (1<<i) > nNum ) 
+                    fShort = 1;
+            } 
+            else 
+                pRes[j] = Gia_ManHashMux( pNew, pShift[i], pRes[j+(1<<i)], pRes[j] );
+        }
+}
+void Wlc_BlastShiftLeft( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int nShift, int fSticky, Vec_Int_t * vRes )
+{
+    int * pRes = Wlc_VecCopy( vRes, pNum, nNum );
+    int Fill = fSticky ? pNum[0] : 0;
+    int i, j, fShort = 0;
+    for( i = 0; i < nShift; i++ ) 
+        for( j = nNum-1; j >= fSticky; j-- ) 
+        {
+            if( fShort || (1<<i) > j ) 
+            {
+                pRes[j] = Gia_ManHashMux( pNew, pShift[i], Fill, pRes[j] );
+                if ( (1<<i) > nNum ) 
+                    fShort = 1;
+            } 
+            else 
+                pRes[j] = Gia_ManHashMux( pNew, pShift[i], pRes[j-(1<<i)], pRes[j] );
+        }
+}
+void Wlc_BlastRotateRight( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int nShift, Vec_Int_t * vRes )
+{
+    int i, j, * pTemp = ABC_ALLOC( int, nNum );
+    for( i = 0; i < nShift; i++, Wlc_VecCopy(vRes, pTemp, nNum) ) 
+        for( j = 0; j < nNum; j++ ) 
+            pTemp[j] = Gia_ManHashMux( pNew, pShift[i], pNum[(j+(1<<i))%nNum], pNum[j] );
+    ABC_FREE( pTemp );
+}
+void Wlc_BlastRotateLeft( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int nShift, Vec_Int_t * vRes )
+{
+    int i, j, * pTemp = ABC_ALLOC( int, nNum );
+    for( i = 0; i < nShift; i++, Wlc_VecCopy(vRes, pTemp, nNum) ) 
+        for( j = 0; j < nNum; j++ ) 
+            pTemp[j] = Gia_ManHashMux( pNew, pShift[i], pNum[(nNum-(1<<i)+j)%nNum], pNum[j] );
+    ABC_FREE( pTemp );
+}
+int Wlc_BlastReduction( Gia_Man_t * pNew, int * pFans, int nFans, int Type )
 {
     if ( Type == WLC_OBJ_REDUCT_AND )
     {
@@ -80,16 +160,21 @@ int Wlc_NtkComputeReduction( Gia_Man_t * pNew, int * pFans, int nFans, int Type
     assert( 0 );
     return -1;
 }
-int Wlc_NtkMuxTree_rec( Gia_Man_t * pNew, int * pCtrl, int nCtrl, Vec_Int_t * vData, int Shift )
+int Wlc_BlastLess( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits )
 {
-    int iLit0, iLit1;
-    if ( nCtrl == 0 )
-        return Vec_IntEntry( vData, Shift );
-    iLit0 = Wlc_NtkMuxTree_rec( pNew, pCtrl, nCtrl-1, vData, Shift );
-    iLit1 = Wlc_NtkMuxTree_rec( pNew, pCtrl, nCtrl-1, vData, Shift + (1<<(nCtrl-1)) );
-    return Gia_ManHashMux( pNew, pCtrl[nCtrl-1], iLit1, iLit0 );
+    int k, iTerm, iEqu = 1, iLit = 0;
+    for ( k = nBits - 1; k >= 0; k-- )
+    {
+        iTerm = Gia_ManHashAnd( pNew, Abc_LitNot(pArg0[k]), pArg1[k] );
+        iTerm = Gia_ManHashAnd( pNew, iTerm, iEqu );
+        if ( iTerm == 1 )
+            return 1;
+        iLit  = Gia_ManHashOr( pNew, iLit, iTerm ); 
+        iEqu  = Abc_LitNot( Gia_ManHashXor( pNew, pArg0[k], pArg1[k] ) );
+    }
+    return iLit;
 }
-void Wlc_NtkAdderChain( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits )
+void Wlc_BlastAdder( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits ) // result is in pAdd0
 {
     int iCarry = 0, iTerm1, iTerm2, iTerm3, iSum, b;
     for ( b = 0; b < nBits; b++ )
@@ -102,11 +187,119 @@ void Wlc_NtkAdderChain( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits )
         pAdd0[b] = iSum;
     }
 }
+void Wlc_BlastMultiplier( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits, Vec_Int_t * vTemp, Vec_Int_t * vRes )
+{
+    int i, j;
+    Vec_IntFill( vRes, nBits, 0 );
+    for ( i = 0; i < nBits; i++ )
+    {
+        Vec_IntFill( vTemp, i, 0 );
+        for ( j = 0; Vec_IntSize(vTemp) < nBits; j++ )
+            Vec_IntPush( vTemp, Gia_ManHashAnd(pNew, pArg0[j], pArg1[i]) );
+        assert( Vec_IntSize(vTemp) == nBits );
+        Wlc_BlastAdder( pNew, Vec_IntArray(vRes), Vec_IntArray(vTemp), nBits );
+    }
+}
+void Wlc_BlastDivider( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes )
+{
+    int * pRes  = Wlc_VecCopy( vRes, pNum, nNum );
+    int * pQuo  = ABC_ALLOC( int, nNum );
+    int * pTemp = ABC_ALLOC( int, nNum );
+    int i, j, known, borrow, y_bit, top_bit;
+    assert( nNum == nDiv );
+    for ( j = nNum - 1; j >= 0; j-- ) 
+    {
+        known = 0;
+        for ( i = nNum - 1; i > nNum - 1 - j; i-- ) 
+        {
+            known = Gia_ManHashOr( pNew, known, pDiv[i] );
+            if( known == 1 ) 
+                break;
+        }
+        pQuo[j] = known;
+        for ( i = nNum - 1; i >= 0; i-- ) 
+        {
+            if ( known == 1 ) 
+                break;
+            y_bit = (i >= j) ? pDiv[i-j] : 0;
+            pQuo[j] = Gia_ManHashMux( pNew, known, pQuo[j], Gia_ManHashAnd( pNew, y_bit, Abc_LitNot(pRes[i]) ) );
+            known = Gia_ManHashOr( pNew, known, Gia_ManHashXor(pNew, y_bit, pRes[i]));
+        }
+        pQuo[j] = Abc_LitNot(pQuo[j]);
+        if ( pQuo[j] == 0 )
+            continue;
+        borrow = 0;
+        for ( i = 0; i < nNum; i++ ) 
+        {
+            top_bit  = Gia_ManHashMux( pNew, borrow, Abc_LitNot(pRes[i]), pRes[i] );
+            y_bit    = (i >= j) ? pDiv[i-j] : 0;
+            borrow   = Gia_ManHashMux( pNew, pRes[i], Gia_ManHashAnd(pNew, borrow, y_bit), Gia_ManHashOr(pNew, borrow, y_bit) );
+            pTemp[i] = Gia_ManHashXor( pNew, top_bit, y_bit );
+        }
+        if ( pQuo[j] == 1 ) 
+            Wlc_VecCopy( vRes, pTemp, nNum );
+        else 
+            for( i = 0; i < nNum; i++ ) 
+                pRes[i] = Gia_ManHashMux( pNew, pQuo[j], pTemp[i], pRes[i] );
+    }
+    ABC_FREE( pTemp );
+    if ( fQuo )
+        Wlc_VecCopy( vRes, pQuo, nNum );
+    ABC_FREE( pQuo );
+}
+void Wlc_BlastMinus( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vRes )
+{
+    int i, * pRes, invert = 0;
+    Vec_IntFill( vRes, nNum, 0 );
+    pRes = Vec_IntArray( vRes );
+    for ( i = 0; i < nNum; i++ )
+    {
+        pRes[i] = Gia_ManHashMux( pNew, invert, Abc_LitNot(pRes[i]), pRes[i] );
+        invert = Gia_ManHashOr( pNew, invert, pNum[i] );    
+    }
+}
+void Wlc_BlastTable( Gia_Man_t * pNew, word * pTable, int * pFans, int nFans, int nOuts, Vec_Int_t * vRes )
+{
+    extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
+    Vec_Int_t * vMemory = Vec_IntAlloc( 0 );
+    Vec_Int_t vLeaves = { nFans, nFans, pFans };
+    word * pTruth = ABC_ALLOC( word, Abc_TtWordNum(nFans) );
+    int o, i, m, iLit, nMints = (1 << nFans);
+    Vec_IntClear( vRes );
+    for ( o = 0; o < nOuts; o++ )
+    {
+        // derive truth table
+        memset( pTruth, 0, sizeof(word) * Abc_TtWordNum(nFans) );
+        for ( m = 0; m < nMints; m++ )
+            for ( i = 0; i < nFans; i++ )
+                if ( Abc_TtGetBit( pTable, m * nFans + i ) )
+                    Abc_TtSetBit( pTruth, m );
+        // implement truth table
+        if ( nFans < 6 )
+            pTruth[0] = Abc_Tt6Stretch( pTruth[0], nFans );
+        iLit = Kit_TruthToGia( pNew, (unsigned *)pTruth, nFans, vMemory, &vLeaves, 1 );
+        Vec_IntPush( vRes, iLit );
+    }
+    Vec_IntFree( vMemory );
+    ABC_FREE( pTruth );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
 {
     Gia_Man_t * pTemp, * pNew;
-    Wlc_Obj_t * pObj;
-    Vec_Int_t * vBits, * vTemp0, * vTemp1, * vTemp2, * vTemp3;
+    Wlc_Obj_t * pObj, * pPrev = NULL;
+    Vec_Int_t * vBits, * vTemp0, * vTemp1, * vTemp2, * vRes;
     int nBits = Wlc_NtkPrepareBits( p );
     int nRange, nRange0, nRange1, nRange2;
     int i, k, b, iLit, * pFans0, * pFans1, * pFans2;
@@ -114,8 +307,8 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
     vTemp0 = Vec_IntAlloc( 1000 );
     vTemp1 = Vec_IntAlloc( 1000 );
     vTemp2 = Vec_IntAlloc( 1000 );
-    vTemp3 = Vec_IntAlloc( 1000 );
-    // craete AIG manager
+    vRes   = Vec_IntAlloc( 1000 );
+    // create AIG manager
     pNew = Gia_ManStart( 5 * Wlc_NtkObjNum(p) + 1000 );
     pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
@@ -130,82 +323,76 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
         pFans0  = Wlc_ObjFaninNum(pObj) > 0 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) ) : NULL;
         pFans1  = Wlc_ObjFaninNum(pObj) > 1 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId1(pObj)) ) : NULL;
         pFans2  = Wlc_ObjFaninNum(pObj) > 2 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId2(pObj)) ) : NULL;
+        Vec_IntClear( vRes );
         if ( pObj->Type == WLC_OBJ_PI )
         {
             for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vBits, Gia_ManAppendCi(pNew) );
+                Vec_IntPush( vRes, Gia_ManAppendCi(pNew) );
         }
         else if ( pObj->Type == WLC_OBJ_PO || pObj->Type == WLC_OBJ_BUF )
         {
 //            assert( nRange <= nRange0 );
             for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vBits, k < nRange0 ? pFans0[k] : 0 );
+                Vec_IntPush( vRes, k < nRange0 ? pFans0[k] : 0 );
         }
         else if ( pObj->Type == WLC_OBJ_CONST )
         {
             word * pTruth = (word *)Wlc_ObjFanins(pObj);
             for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vBits, Abc_TtGetBit(pTruth, k) );
+                Vec_IntPush( vRes, Abc_TtGetBit(pTruth, k) );
         }
         else if ( pObj->Type == WLC_OBJ_MUX )
         {
-            assert( nRange0 == 1 );
-            assert( nRange1 == nRange );
-            assert( nRange2 == nRange );
+            assert( nRange0 == 1 && nRange1 == nRange && nRange2 == nRange );
             for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vBits, Gia_ManHashMux(pNew, pFans0[0], pFans1[k], pFans2[k]) );
+                Vec_IntPush( vRes, Gia_ManHashMux(pNew, pFans0[0], pFans1[k], pFans2[k]) );
         }
         else if ( pObj->Type == WLC_OBJ_SHIFT_R || pObj->Type == WLC_OBJ_SHIFT_RA )
         {
-            // prepare data
-            int Fill = pObj->Type == WLC_OBJ_SHIFT_R ? 0 : pFans0[nRange0-1];
-            int nTotal = nRange + (1 << nRange1);
-            Vec_IntClear( vTemp0 );
-            for ( k = 0; k < nRange0; k++ )
-                Vec_IntPush( vTemp0, pFans0[k] );
-            for ( k = 0; k < nTotal; k++ )
-                Vec_IntPush( vTemp0, Fill );
-            // derive the result
-            for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vBits, Wlc_NtkMuxTree_rec(pNew, pFans1, nRange1, vTemp0, k) );
+            assert( nRange0 >= nRange );
+            Wlc_BlastShiftRight( pNew, pFans0, nRange0, pFans1, nRange1, pObj->Type == WLC_OBJ_SHIFT_RA, vRes );
+            if ( nRange0 > nRange )
+                Vec_IntShrink( vRes, nRange );
         }
         else if ( pObj->Type == WLC_OBJ_SHIFT_L || pObj->Type == WLC_OBJ_SHIFT_LA )
         {
-            // prepare data
-            int Fill = pObj->Type == WLC_OBJ_SHIFT_L ? 0 : pFans0[0];
-            int nTotal = nRange + (1 << nRange1);
-            Vec_IntClear( vTemp0 );
-            for ( k = 0; k < nRange0; k++ )
-                Vec_IntPush( vTemp0, pFans0[k] );
-            for ( k = 0; k < nTotal; k++ )
-                Vec_IntPush( vTemp0, Fill );
-            // derive the result
-            for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vBits, Wlc_NtkMuxTree_rec(pNew, pFans1, nRange1, vTemp0, k) );
+            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRange, Wlc_ObjFanin0(p, pObj)->Signed );
+            assert( nRange0 <= nRange );
+            Wlc_BlastShiftLeft( pNew, pArg0, nRange, pFans1, nRange1, pObj->Type == WLC_OBJ_SHIFT_LA, vRes );
+        }
+        else if ( pObj->Type == WLC_OBJ_ROTATE_R )
+        {
+            assert( nRange0 == nRange );
+            Wlc_BlastRotateRight( pNew, pFans0, nRange0, pFans1, nRange1, vRes );
+        }
+        else if ( pObj->Type == WLC_OBJ_ROTATE_L )
+        {
+            assert( nRange0 == nRange );
+            Wlc_BlastRotateLeft( pNew, pFans0, nRange0, pFans1, nRange1, vRes );
         }
         else if ( pObj->Type == WLC_OBJ_BIT_NOT )
         {
             assert( nRange == nRange0 );
             for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vBits, Abc_LitNot(pFans0[k]) );
+                Vec_IntPush( vRes, Abc_LitNot(pFans0[k]) );
         }
         else if ( pObj->Type == WLC_OBJ_BIT_AND )
         {
             assert( nRange0 == nRange && nRange1 == nRange );
             for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vBits, Gia_ManHashAnd(pNew, pFans0[k], pFans1[k]) );
+                Vec_IntPush( vRes, Gia_ManHashAnd(pNew, pFans0[k], pFans1[k]) );
         }
         else if ( pObj->Type == WLC_OBJ_BIT_OR )
         {
             assert( nRange0 == nRange && nRange1 == nRange );
             for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vBits, Gia_ManHashOr(pNew, pFans0[k], pFans1[k]) );
+                Vec_IntPush( vRes, Gia_ManHashOr(pNew, pFans0[k], pFans1[k]) );
         }
         else if ( pObj->Type == WLC_OBJ_BIT_XOR )
         {
             assert( nRange0 == nRange && nRange1 == nRange );
             for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vBits, Gia_ManHashXor(pNew, pFans0[k], pFans1[k]) );
+                Vec_IntPush( vRes, Gia_ManHashXor(pNew, pFans0[k], pFans1[k]) );
         }
         else if ( pObj->Type == WLC_OBJ_BIT_SELECT )
         {
@@ -213,7 +400,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
             int Beg = Wlc_ObjRangeBeg(pObj);
             assert( nRange == End - Beg + 1 );
             for ( k = Beg; k <= End; k++ )
-                Vec_IntPush( vBits, pFans0[k] );
+                Vec_IntPush( vRes, pFans0[k] );
         }
         else if ( pObj->Type == WLC_OBJ_BIT_CONCAT )
         {
@@ -226,7 +413,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
                 nRange0 = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
                 pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, iFanin) );
                 for ( b = 0; b < nRange0; b++ )
-                    Vec_IntPush( vBits, pFans0[b] );
+                    Vec_IntPush( vRes, pFans0[b] );
             }
         }
         else if ( pObj->Type == WLC_OBJ_BIT_ZEROPAD || pObj->Type == WLC_OBJ_BIT_SIGNEXT )
@@ -234,113 +421,89 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
             int Pad = pObj->Type == WLC_OBJ_BIT_ZEROPAD ? 0 : pFans0[nRange0-1];
             assert( nRange0 < nRange );
             for ( k = 0; k < nRange0; k++ )
-                Vec_IntPush( vBits, pFans0[k] );
+                Vec_IntPush( vRes, pFans0[k] );
             for (      ; k < nRange; k++ )
-                Vec_IntPush( vBits, Pad );
+                Vec_IntPush( vRes, Pad );
         }
         else if ( pObj->Type == WLC_OBJ_LOGIC_NOT )
         {
-            iLit = Wlc_NtkComputeReduction( pNew, pFans0, nRange, WLC_OBJ_REDUCT_OR );
+            iLit = Wlc_BlastReduction( pNew, pFans0, nRange, WLC_OBJ_REDUCT_OR );
             assert( nRange == 1 );
-            Vec_IntPush( vBits, Abc_LitNot(iLit) );
+            Vec_IntFill( vRes, 1, Abc_LitNot(iLit) );
         }
         else if ( pObj->Type == WLC_OBJ_LOGIC_AND )
         {
-            int iLit0 = Wlc_NtkComputeReduction( pNew, pFans0, nRange, WLC_OBJ_REDUCT_OR );
-            int iLit1 = Wlc_NtkComputeReduction( pNew, pFans0, nRange, WLC_OBJ_REDUCT_OR );
+            int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange, WLC_OBJ_REDUCT_OR );
+            int iLit1 = Wlc_BlastReduction( pNew, pFans0, nRange, WLC_OBJ_REDUCT_OR );
             assert( nRange == 1 );
-            Vec_IntPush( vBits, Gia_ManHashAnd(pNew, iLit0, iLit1) );
+            Vec_IntFill( vRes, 1, Gia_ManHashAnd(pNew, iLit0, iLit1) );
         }
         else if ( pObj->Type == WLC_OBJ_LOGIC_OR )
         {
-            int iLit0 = Wlc_NtkComputeReduction( pNew, pFans0, nRange, WLC_OBJ_REDUCT_OR );
-            int iLit1 = Wlc_NtkComputeReduction( pNew, pFans0, nRange, WLC_OBJ_REDUCT_OR );
+            int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange, WLC_OBJ_REDUCT_OR );
+            int iLit1 = Wlc_BlastReduction( pNew, pFans0, nRange, WLC_OBJ_REDUCT_OR );
             assert( nRange == 1 );
-            Vec_IntPush( vBits, Gia_ManHashOr(pNew, iLit0, iLit1) );
+            Vec_IntFill( vRes, 1, Gia_ManHashOr(pNew, iLit0, iLit1) );
         }
-        else if ( pObj->Type == WLC_OBJ_COMP_EQU || pObj->Type == WLC_OBJ_COMP_NOT )
+        else if ( pObj->Type == WLC_OBJ_COMP_EQU || pObj->Type == WLC_OBJ_COMP_NOTEQU )
         {
             int iLit = 0;
-            assert( nRange == 1 );
-            assert( nRange0 == nRange1 );
+            assert( nRange == 1 && nRange0 == nRange1 );
             for ( k = 0; k < nRange0; k++ )
                 iLit = Gia_ManHashOr( pNew, iLit, Gia_ManHashXor(pNew, pFans0[k], pFans1[k]) ); 
-            Vec_IntPush( vBits, Abc_LitNotCond(iLit, pObj->Type == WLC_OBJ_COMP_EQU) );
+            Vec_IntFill( vRes, 1, Abc_LitNotCond(iLit, pObj->Type == WLC_OBJ_COMP_EQU) );
         }
         else if ( pObj->Type == WLC_OBJ_COMP_LESS || pObj->Type == WLC_OBJ_COMP_MOREEQU ||
                   pObj->Type == WLC_OBJ_COMP_MORE || pObj->Type == WLC_OBJ_COMP_LESSEQU )
         {
-            int iTerm, iEqu = 1, iLit = 0;
+            int fSwap  = (pObj->Type == WLC_OBJ_COMP_MORE    || pObj->Type == WLC_OBJ_COMP_LESSEQU);
+            int fCompl = (pObj->Type == WLC_OBJ_COMP_MOREEQU || pObj->Type == WLC_OBJ_COMP_LESSEQU);
             assert( nRange == 1 );
             assert( nRange0 == nRange1 );
-            if ( pObj->Type == WLC_OBJ_COMP_MORE || pObj->Type == WLC_OBJ_COMP_LESSEQU )
-                ABC_SWAP( int *, pFans0, pFans1 );
-            for ( k = nRange0 - 1; k >= 0; k-- )
-            {
-                iTerm = Gia_ManHashAnd( pNew, Abc_LitNot(pFans0[k]), pFans1[k] );
-                iTerm = Gia_ManHashAnd( pNew, iTerm, iEqu );
-                iLit  = Gia_ManHashOr( pNew, iLit, iTerm ); 
-                iEqu  = Abc_LitNot( Gia_ManHashXor( pNew, pFans0[k], pFans1[k] ) );
-            }
-            Vec_IntPush( vBits, Abc_LitNotCond(iLit, pObj->Type == WLC_OBJ_COMP_MOREEQU) );
+            if ( fSwap ) ABC_SWAP( int *, pFans0, pFans1 );
+            iLit = Wlc_BlastLess( pNew, pFans0, pFans1, nRange0 );
+            iLit = Abc_LitNotCond( iLit, fCompl );
+            Vec_IntFill( vRes, 1, iLit );
         }
         else if ( pObj->Type == WLC_OBJ_REDUCT_AND || pObj->Type == WLC_OBJ_REDUCT_OR || pObj->Type == WLC_OBJ_REDUCT_XOR )
-            Vec_IntPush( vBits, Wlc_NtkComputeReduction( pNew, pFans0, nRange, pObj->Type ) );
-        else if ( pObj->Type == WLC_OBJ_ARI_ADD )
+            Vec_IntPush( vRes, Wlc_BlastReduction( pNew, pFans0, nRange, pObj->Type ) );
+        else if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB )  // SUBTRACT is not implemented!
         {
-            int Pad0 = Wlc_ObjFanin0(p, pObj)->Signed ? pFans0[nRange0-1] : 0;
-            int Pad1 = Wlc_ObjFanin1(p, pObj)->Signed ? pFans1[nRange1-1] : 0;
-            assert( nRange0 <= nRange && nRange1 <= nRange );
-            Vec_IntClear( vTemp0 );
-            for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vTemp0, k < nRange0 ? pFans0[k] : Pad0 );
-            Vec_IntClear( vTemp1 );
-            for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vTemp1, k < nRange1 ? pFans1[k] : Pad1 );
-            Wlc_NtkAdderChain( pNew, Vec_IntArray(vTemp0), Vec_IntArray(vTemp1), nRange );
-            Vec_IntAppend( vBits, vTemp0 );
+            int * pArg0 = Wlc_VecLoadFanins( vRes,   pFans0, nRange0, nRange, Wlc_ObjFanin0(p, pObj)->Signed );
+            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRange, Wlc_ObjFanin1(p, pObj)->Signed );
+            Wlc_BlastAdder( pNew, pArg0, pArg1, nRange ); // result is in pFan0 (vRes)
         }
         else if ( pObj->Type == WLC_OBJ_ARI_MULTI )
         {
-            int Pad0 = Wlc_ObjFanin0(p, pObj)->Signed ? pFans0[nRange0-1] : 0;
-            int Pad1 = Wlc_ObjFanin1(p, pObj)->Signed ? pFans1[nRange1-1] : 0;
+            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRange, Wlc_ObjFanin0(p, pObj)->Signed );
+            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRange, Wlc_ObjFanin1(p, pObj)->Signed );
             assert( nRange0 <= nRange && nRange1 <= nRange );
-            Vec_IntClear( vTemp0 );
-            for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vTemp0, k < nRange0 ? pFans0[k] : Pad0 );
-            Vec_IntClear( vTemp1 );
-            for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vTemp1, k < nRange1 ? pFans1[k] : Pad1 );
-            // iterate
-            Vec_IntFill( vTemp3, nRange, 0 );
-            for ( k = 0; k < nRange; k++ )
-            {
-                Vec_IntFill( vTemp2, k, 0 );
-                Vec_IntForEachEntry( vTemp0, iLit, b )
-                {
-                    Vec_IntPush( vTemp2, Gia_ManHashAnd(pNew, iLit, Vec_IntEntry(vTemp1, k)) );
-                    if ( Vec_IntSize(vTemp2) == nRange )
-                        break;
-                }
-                assert( Vec_IntSize(vTemp2) == nRange );
-                Wlc_NtkAdderChain( pNew, Vec_IntArray(vTemp3), Vec_IntArray(vTemp2), nRange );
+            Wlc_BlastMultiplier( pNew, pArg0, pArg1, nRange, vTemp2, vRes );
         }
-            assert( Vec_IntSize(vTemp3) == nRange );
-            Vec_IntAppend( vBits, vTemp3 );
+        else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_MODULUS )
+        {
+            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRange, Wlc_ObjFanin0(p, pObj)->Signed );
+            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRange, Wlc_ObjFanin1(p, pObj)->Signed );
+            assert( nRange0 <= nRange && nRange1 <= nRange );
+            Wlc_BlastDivider( pNew, pArg0, nRange0, pArg1, nRange1, pObj->Type == WLC_OBJ_ARI_DIVIDE, vRes );
         }
-        else if ( pObj->Type == WLC_OBJ_TABLE )
+        else if ( pObj->Type == WLC_OBJ_ARI_MINUS )
         {
-            assert( pObj->Type != WLC_OBJ_TABLE );
-            for ( k = 0; k < nRange; k++ )
-                Vec_IntPush( vBits, 0 );
+            assert( nRange0 == nRange );
+            Wlc_BlastMinus( pNew, pFans0, nRange0, vRes );
         }
+        else if ( pObj->Type == WLC_OBJ_TABLE )
+            Wlc_BlastTable( pNew, Wlc_ObjTable(p, pObj), pFans0, nRange0, nRange, vRes );
         else assert( 0 );
+        assert( Vec_IntSize(vBits) == Wlc_ObjCopy(p, i) );
+        Vec_IntAppend( vBits, vRes );
+        pPrev = pObj;
     }
     assert( nBits == Vec_IntSize(vBits) );
     Vec_IntFree( vTemp0 );
     Vec_IntFree( vTemp1 );
     Vec_IntFree( vTemp2 );
-    Vec_IntFree( vTemp3 );
+    Vec_IntFree( vRes );
     // create POs
     Wlc_NtkForEachPo( p, pObj, i )
     {

src/base/wlc/wlcNtk.c

@@ -42,34 +42,37 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
     ">>>",                 // 10: shift right (arithmetic)
     "<<",                  // 11: shift left
     "<<<",                 // 12: shift left (arithmetic)
-    "~",                   // 13: bitwise NOT
-    "&",                   // 14: bitwise AND
-    "|",                   // 15: bitwise OR
-    "^",                   // 16: bitwise XOR
-    "[:]",                 // 17: bit selection
-    "{,}",                 // 18: bit concatenation
-    "BitPad",              // 19: zero padding
-    "SgnExt",              // 20: sign extension
-    "!",                   // 21: logic NOT
-    "&&",                  // 22: logic AND
-    "||",                  // 23: logic OR
-    "==",                  // 24: compare equal
-    "!=",                  // 25: compare not equal
-    "<",                   // 26: compare less
-    ">",                   // 27: compare more
-    "<=",                  // 28: compare less or equal
-    ">=",                  // 29: compare more or equal
-    "&",                   // 30: reduction AND
-    "|",                   // 31: reduction OR
-    "^",                   // 32: reduction XOR
-    "+",                   // 33: arithmetic addition
-    "-",                   // 34: arithmetic subtraction
-    "*",                   // 35: arithmetic multiplier
-    "//",                  // 36: arithmetic division
-    "%%",                  // 37: arithmetic modulus
-    "**",                  // 38: arithmetic power
-    "table",               // 39: lookup table
-    NULL                   // 40: unused
+    "rotateR",             // 13: shift left (arithmetic)
+    "rotateL",             // 14: shift left (arithmetic)
+    "~",                   // 15: bitwise NOT
+    "&",                   // 16: bitwise AND
+    "|",                   // 17: bitwise OR
+    "^",                   // 18: bitwise XOR
+    "[:]",                 // 19: bit selection
+    "{,}",                 // 20: bit concatenation
+    "bitPad",              // 21: zero padding
+    "signExtend",          // 22: sign extension
+    "!",                   // 23: logic NOT
+    "&&",                  // 24: logic AND
+    "||",                  // 25: logic OR
+    "==",                  // 26: compare equal
+    "!=",                  // 27: compare not equal
+    "<",                   // 28: compare less
+    ">",                   // 29: compare more
+    "<=",                  // 30: compare less or equal
+    ">=",                  // 31: compare more or equal
+    "&",                   // 32: reduction AND
+    "|",                   // 33: reduction OR
+    "^",                   // 34: reduction XOR
+    "+",                   // 35: arithmetic addition
+    "-",                   // 36: arithmetic subtraction
+    "*",                   // 37: arithmetic multiplier
+    "//",                  // 38: arithmetic division
+    "%%",                  // 39: arithmetic modulus
+    "**",                  // 40: arithmetic power
+    "-",                   // 41: arithmetic minus
+    "table",               // 42: bit table
+    NULL                   // 43: unused
 };
 
 ////////////////////////////////////////////////////////////////////////

src/base/wlc/wlcReadVer.c

@@ -409,6 +409,7 @@ static inline char * Wlc_PrsReadConstant( Wlc_Prs_t * p, char * pStr, Vec_Int_t
         *pRange = Abc_Base2Log( Number );
         while ( Wlc_PrsIsDigit(pStr) )
             pStr++;
+        Vec_IntFill( vFanins, 1, Number );
         return pStr;
     }
     pStr = Wlc_PrsFindSymbol( pStr, '\'' );
@@ -424,7 +425,7 @@ static inline char * Wlc_PrsReadConstant( Wlc_Prs_t * p, char * pStr, Vec_Int_t
     if ( nDigits != (nBits + 3)/4 )
     {
 //        return (char *)(ABC_PTRINT_T)Wlc_PrsWriteErrorMessage( p, pStr, "The length of a constant does not match." );
-        printf( "Warning: The length of a constant (%d hex digits) does not match the number of bits (%d).\n", nDigits, nBits );
+//        printf( "Warning: The length of a constant (%d hex digits) does not match the number of bits (%d).\n", nDigits, nBits );
     }
     *pRange = nBits;
     pStr += 2;
@@ -452,7 +453,7 @@ static inline char * Wlc_PrsReadName( Wlc_Prs_t * p, char * pStr, Vec_Int_t * vF
         Wlc_ObjAddFanins( p->pNtk, Wlc_NtkObj(p->pNtk, iObj), vFanins );
         Vec_IntFree( vFanins );
         // add node's name
-        sprintf( Buffer, "const%d", p->nConsts++ );
+        sprintf( Buffer, "_c%d_", p->nConsts++ );
         NameId = Abc_NamStrFindOrAdd( p->pNtk->pManName, Buffer, &fFound );
         if ( fFound )
             return (char *)(ABC_PTRINT_T)Wlc_PrsWriteErrorMessage( p, pStr, "Name %s is already used.", Buffer );
@@ -530,7 +531,7 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t *
         if ( !(pStr = Wlc_PrsReadName(p, pStr, vFanins)) )
             return Wlc_PrsWriteErrorMessage( p, pStr, "Cannot read name after !." );
     }
-    else if ( pStr[0] == '&' || pStr[0] == '|' || pStr[0] == '^' )
+    else if ( pStr[0] == '&' || pStr[0] == '|' || pStr[0] == '^' || pStr[0] == '-' )
     {
         if ( pStr[0] == '&' )
             Type = WLC_OBJ_REDUCT_AND;
@@ -538,9 +539,11 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t *
             Type = WLC_OBJ_REDUCT_OR;
         else if ( pStr[0] == '^' )
             Type = WLC_OBJ_REDUCT_XOR;
+        else if ( pStr[0] == '-' )
+            Type = WLC_OBJ_ARI_MINUS;
         else assert( 0 );
         if ( !(pStr = Wlc_PrsReadName(p, pStr+1, vFanins)) )
-            return Wlc_PrsWriteErrorMessage( p, pStr, "Cannot read name after reduction operator." );
+            return Wlc_PrsWriteErrorMessage( p, pStr, "Cannot read name after a unary operator." );
     }
     else if ( pStr[0] == '{' )
     {
@@ -603,9 +606,9 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t *
         }
         else 
         {
-                 if ( pStr[0] == '>' && pStr[1] == '>' && pStr[2] != '>' ) pStr += 2, Type = WLC_OBJ_SHIFT_R;
+                 if ( pStr[0] == '>' && pStr[1] == '>' && pStr[2] != '>' ) pStr += 2, Type = fRotating ? WLC_OBJ_ROTATE_R : WLC_OBJ_SHIFT_R;
             else if ( pStr[0] == '>' && pStr[1] == '>' && pStr[2] == '>' ) pStr += 3, Type = WLC_OBJ_SHIFT_RA;      
-            else if ( pStr[0] == '<' && pStr[1] == '<' && pStr[2] != '<' ) pStr += 2, Type = WLC_OBJ_SHIFT_L;       
+            else if ( pStr[0] == '<' && pStr[1] == '<' && pStr[2] != '<' ) pStr += 2, Type = fRotating ? WLC_OBJ_ROTATE_L : WLC_OBJ_SHIFT_L;
             else if ( pStr[0] == '<' && pStr[1] == '<' && pStr[2] == '<' ) pStr += 3, Type = WLC_OBJ_SHIFT_LA;      
             else if ( pStr[0] == '&' && pStr[1] != '&'                   ) pStr += 1, Type = WLC_OBJ_BIT_AND;       
             else if ( pStr[0] == '|' && pStr[1] != '|'                   ) pStr += 1, Type = WLC_OBJ_BIT_OR;        
@@ -613,7 +616,7 @@ static inline int Wlc_PrsFindDefinition( Wlc_Prs_t * p, char * pStr, Vec_Int_t *
             else if ( pStr[0] == '&' && pStr[1] == '&'                   ) pStr += 2, Type = WLC_OBJ_LOGIC_AND;     
             else if ( pStr[0] == '|' && pStr[1] == '|'                   ) pStr += 2, Type = WLC_OBJ_LOGIC_OR;      
             else if ( pStr[0] == '=' && pStr[1] == '='                   ) pStr += 2, Type = WLC_OBJ_COMP_EQU;      
-            else if ( pStr[0] == '!' && pStr[1] == '='                   ) pStr += 2, Type = WLC_OBJ_COMP_NOT;      
+            else if ( pStr[0] == '!' && pStr[1] == '='                   ) pStr += 2, Type = WLC_OBJ_COMP_NOTEQU;      
             else if ( pStr[0] == '<' && pStr[1] != '='                   ) pStr += 1, Type = WLC_OBJ_COMP_LESS;     
             else if ( pStr[0] == '>' && pStr[1] != '='                   ) pStr += 1, Type = WLC_OBJ_COMP_MORE;     
             else if ( pStr[0] == '<' && pStr[1] == '='                   ) pStr += 2, Type = WLC_OBJ_COMP_LESSEQU;
@@ -702,6 +705,7 @@ int Wlc_PrsDerive( Wlc_Prs_t * p )
             if ( Wlc_PrsStrCmp( pName, "table" ) )
             {
                 // THIS IS A HACK TO DETECT tables
+                int Width1, Width2;
                 int v, b, Value, nBits, nInts, * pTable;
                 Vec_Int_t * vValues = Vec_IntAlloc( 256 );
                 Wlc_PrsForEachLineStart( p, pStart, i, i+1 )
@@ -711,9 +715,11 @@ int Wlc_PrsDerive( Wlc_Prs_t * p )
                     pStart = Wlc_PrsFindSymbol( pStart, '\'' );
                     if ( pStart == NULL )
                         continue;
+                    Width1 = atoi(pStart-1);
                     pStart = Wlc_PrsFindSymbol( pStart+2, '\'' );
                     if ( pStart == NULL )
                         continue;
+                    Width2 = atoi(pStart-1);
                     Value = 0;
                     Abc_TtReadHexNumber( (word *)&Value, pStart+2 );
                     Vec_IntPush( vValues, Value );
@@ -725,14 +731,15 @@ int Wlc_PrsDerive( Wlc_Prs_t * p )
                     Vec_IntFree( vValues );
                     return Wlc_PrsWriteErrorMessage( p, pStart, "Cannot read module \"%s\".", pName );
                 }
+                assert( Width1 == nBits );
                 // create bitmap
-                nInts = Abc_BitWordNum( nBits * Vec_IntSize(vValues) );
+                nInts = Abc_BitWordNum( Width2 * Vec_IntSize(vValues) );
                 pTable = (unsigned *)Mem_FlexEntryFetch( p->pMemTable, nInts * sizeof(unsigned) );
                 memset( pTable, 0, nInts * sizeof(unsigned) );
                 Vec_IntForEachEntry( vValues, Value, v )
-                    for ( b = 0; b < nBits; b++ )
+                    for ( b = 0; b < Width2; b++ )
                         if ( (Value >> b) & 1 )
-                            Abc_InfoSetBit( pTable, v * nBits + b );
+                            Abc_InfoSetBit( pTable, v * Width2 + b );
                 Vec_PtrPush( p->vTables, pTable );
                 Vec_IntFree( vValues );
                 continue;

src/base/wlc/wlcWriteVer.c

@@ -42,6 +42,60 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+void Wlc_WriteTableOne( FILE * pFile, int nFans, int nOuts, word * pTable, int Id )
+{
+    int m, nMints = (1<<nFans);
+//    Abc_TtPrintHexArrayRev( stdout, pTable, nMints );  printf( "\n" );
+    assert( nOuts > 0 && nOuts <= 64 && (64 % nOuts) == 0 );
+    fprintf( pFile, "module table%d(ind, val);\n", Id );
+    fprintf( pFile, "  input  [%d:0] ind;\n", nFans-1 );
+    fprintf( pFile, "  output [%d:0] val;\n", nOuts-1 );
+    fprintf( pFile, "  reg    [%d:0] val;\n", nOuts-1 );
+    fprintf( pFile, "  always @(ind)\n" );
+    fprintf( pFile, "  begin\n" );
+    fprintf( pFile, "    case (ind)\n" );
+    for ( m = 0; m < nMints; m++ )
+    fprintf( pFile, "      %d\'h%x: val = %d\'h%x;\n", nFans, m, nOuts, (pTable[(nOuts * m) >> 6] >> ((nOuts * m) & 63)) & Abc_Tt6Mask(nOuts) );
+    fprintf( pFile, "    endcase\n" );
+    fprintf( pFile, "  end\n" );
+    fprintf( pFile, "endmodule\n" );
+    fprintf( pFile, "\n" );
+}
+void Wlc_WriteTables( FILE * pFile, Wlc_Ntk_t * p )
+{
+    Vec_Int_t * vNodes;
+    Wlc_Obj_t * pObj, * pFanin;
+    word * pTable;
+    int i;
+    if ( p->vTables == NULL || Vec_PtrSize(p->vTables) == 0 )
+        return;
+    // map tables into their nodes
+    vNodes = Vec_IntStart( Vec_PtrSize(p->vTables) );
+    Wlc_NtkForEachObj( p, pObj, i )
+        if ( pObj->Type == WLC_OBJ_TABLE )
+            Vec_IntWriteEntry( vNodes, Wlc_ObjTableId(pObj), i );
+    // write tables
+    Vec_PtrForEachEntry( word *, p->vTables, pTable, i )
+    {
+        pObj = Wlc_NtkObj( p, Vec_IntEntry(vNodes, i) );
+        assert( pObj->Type == WLC_OBJ_TABLE );
+        pFanin = Wlc_ObjFanin0( p, pObj );
+        Wlc_WriteTableOne( pFile, Wlc_ObjRange(pFanin), Wlc_ObjRange(pObj), pTable, i );
+    }
+    Vec_IntFree( vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Wlc_WriteVerIntVec( FILE * pFile, Wlc_Ntk_t * p, Vec_Int_t * vVec, int Start )
 {
     char * pName;
@@ -80,23 +134,50 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
     if ( Wlc_NtkPoNum(p) > 0  )
         Wlc_WriteVerIntVec( pFile, p, &p->vPos, 3 );
     fprintf( pFile, "  );\n" );
+    // mark fanins of rotation shifts
+    Wlc_NtkForEachObj( p, pObj, i )
+        if ( pObj->Type == WLC_OBJ_ROTATE_R || pObj->Type == WLC_OBJ_ROTATE_L )
+            Wlc_ObjFanin1(p, pObj)->Mark = 1;
     Wlc_NtkForEachObj( p, pObj, i )
     {
         char * pName  = Wlc_ObjName(p, i);
         char * pName0 = Wlc_ObjFaninNum(pObj) ? Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) : NULL;
         int nDigits   = Abc_Base10Log(pObj->End+1) + Abc_Base10Log(pObj->Beg+1);
+        if ( pObj->Mark ) 
+        {
+            pObj->Mark = 0;
+            continue;
+        }
         sprintf( Range, "%s[%d:%d]%*s", pObj->Signed ? "signed ":"       ", pObj->End, pObj->Beg, 8-nDigits, "" );
         fprintf( pFile, "  " );
-        assert( pObj->Type != WLC_OBJ_TABLE );
         if ( pObj->Type == WLC_OBJ_PI )
-            fprintf( pFile, "input  wire %s %-16s", Range, pName );
+            fprintf( pFile, "input  wire %s %s", Range, pName );
         else if ( pObj->Type == WLC_OBJ_PO )
             fprintf( pFile, "output wire %s %-16s = %s", Range, pName, pName0 );
+        else if ( pObj->Type == WLC_OBJ_TABLE )
+        {
+            // wire [3:0] s4972; table0 s4972_Index(s4971, s4972);
+            fprintf( pFile, "       wire %s %s ;              table%d s%d_Index(%s, %s)", Range, pName, Wlc_ObjTableId(pObj), i, pName0, pName );
+        }
         else if ( pObj->Type == WLC_OBJ_CONST )
         {
             fprintf( pFile, "       wire %s %-16s = %d\'%sh", Range, pName, Wlc_ObjRange(pObj), pObj->Signed ? "s":"" );
             Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pObj), (Wlc_ObjRange(pObj) + 3) / 4 );
         }
+        else if ( pObj->Type == WLC_OBJ_ROTATE_R || pObj->Type == WLC_OBJ_ROTATE_L )
+        {
+            //  wire [27:0] s4960 = (s57 >> 17) | (s57 << 11);
+            Wlc_Obj_t * pShift = Wlc_ObjFanin1(p, pObj);
+            int Num0 = *Wlc_ObjConstValue(pShift);
+            int Num1 = Wlc_ObjRange(pObj) - Num0;
+            assert( pShift->Type == WLC_OBJ_CONST );
+            assert( Num0 > 0 && Num0 < Wlc_ObjRange(pObj) );
+            fprintf( pFile, "       wire %s %-16s = ", Range, Wlc_ObjName(p, i) );
+            if ( pObj->Type == WLC_OBJ_ROTATE_R )
+                fprintf( pFile, "(%s >> %d) | (%s << %d)", pName0, Num0, pName0, Num1 );
+            else
+                fprintf( pFile, "(%s << %d) | (%s >> %d)", pName0, Num0, pName0, Num1 );
+        }
         else
         {
             fprintf( pFile, "       wire %s %-16s = ", Range, Wlc_ObjName(p, i) );
@@ -150,7 +231,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
                     fprintf( pFile, "||" );
                 else if ( pObj->Type == WLC_OBJ_COMP_EQU )
                     fprintf( pFile, "==" );
-                else if ( pObj->Type == WLC_OBJ_COMP_NOT )
+                else if ( pObj->Type == WLC_OBJ_COMP_NOTEQU )
                     fprintf( pFile, "!=" );
                 else if ( pObj->Type == WLC_OBJ_COMP_LESS )
                     fprintf( pFile, "<" );
@@ -191,6 +272,7 @@ void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName )
     }
     fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", p->pName, Extra_TimeStamp() );
     fprintf( pFile, "\n" );
+    Wlc_WriteTables( pFile, p );
     Wlc_WriteVerInt( pFile, p );
     fprintf( pFile, "\n" );
     fclose( pFile );