New word-level representation package.

1 files changed, 363 insertions, 0 deletions

diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
new file mode 100644
index 00000000..1e536014
--- /dev/null
+++ b/src/base/wlc/wlcBlast.c
@@ -0,0 +1,363 @@
+/**CFile****************************************************************
+
+  FileName    [wlcBlast.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Bit-blasting.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 22, 2014.]
+
+  Revision    [$Id: wlcBlast.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Wlc_NtkPrepareBits( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj;
+    int i, nBits = 0;
+    Wlc_NtkCleanCopy( p );
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        Wlc_ObjSetCopy( p, i, nBits );
+        nBits += Wlc_ObjRange(pObj);
+    }
+    return nBits;
+}
+int Wlc_NtkComputeReduction( Gia_Man_t * pNew, int * pFans, int nFans, int Type )
+{
+    if ( Type == WLC_OBJ_REDUCT_AND )
+    {
+        int k, iLit = 1;
+        for ( k = 0; k < nFans; k++ )
+            iLit = Gia_ManHashAnd( pNew, iLit, pFans[k] );
+        return iLit;
+    }
+    if ( Type == WLC_OBJ_REDUCT_OR )
+    {
+        int k, iLit = 0;
+        for ( k = 0; k < nFans; k++ )
+            iLit = Gia_ManHashOr( pNew, iLit, pFans[k] );
+        return iLit;
+    }
+    if ( Type == WLC_OBJ_REDUCT_XOR )
+    {
+        int k, iLit = 0;
+        for ( k = 0; k < nFans; k++ )
+            iLit = Gia_ManHashXor( pNew, iLit, pFans[k] );
+        return iLit;
+    }
+    assert( 0 );
+    return -1;
+}
+int Wlc_NtkMuxTree_rec( Gia_Man_t * pNew, int * pCtrl, int nCtrl, Vec_Int_t * vData, int Shift )
+{
+    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 );
+}
+void Wlc_NtkAdderChain( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits )
+{
+    int iCarry = 0, iTerm1, iTerm2, iTerm3, iSum, b;
+    for ( b = 0; b < nBits; b++ )
+    {
+        iSum   = Gia_ManHashXor( pNew, iCarry, Gia_ManHashXor(pNew, pAdd0[b], pAdd1[b]) );
+        iTerm1 = Gia_ManHashAnd( pNew, pAdd0[b], pAdd1[b] );
+        iTerm2 = Gia_ManHashAnd( pNew, pAdd0[b], iCarry );
+        iTerm3 = Gia_ManHashAnd( pNew, pAdd1[b], iCarry );
+        iCarry = Gia_ManHashOr( pNew, iTerm1, Gia_ManHashOr(pNew, iTerm2, iTerm3) );
+        pAdd0[b] = iSum;
+    }
+}
+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;
+    int nBits = Wlc_NtkPrepareBits( p );
+    int nRange, nRange0, nRange1, nRange2;
+    int i, k, b, iLit, * pFans0, * pFans1, * pFans2;
+    vBits  = Vec_IntAlloc( nBits );
+    vTemp0 = Vec_IntAlloc( 1000 );
+    vTemp1 = Vec_IntAlloc( 1000 );
+    vTemp2 = Vec_IntAlloc( 1000 );
+    vTemp3 = Vec_IntAlloc( 1000 );
+    // craete AIG manager
+    pNew = Gia_ManStart( 5 * Wlc_NtkObjNum(p) + 1000 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    // create primary inputs
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        char * pName = Wlc_ObjName(p, i);
+        nRange  = Wlc_ObjRange( pObj );
+        nRange0 = Wlc_ObjFaninNum(pObj) > 0 ? Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) ) : -1;
+        nRange1 = Wlc_ObjFaninNum(pObj) > 1 ? Wlc_ObjRange( Wlc_ObjFanin1(p, pObj) ) : -1;
+        nRange2 = Wlc_ObjFaninNum(pObj) > 2 ? Wlc_ObjRange( Wlc_ObjFanin2(p, pObj) ) : -1;
+        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;
+        if ( pObj->Type == WLC_OBJ_PI )
+        {
+            for ( k = 0; k < nRange; k++ )
+                Vec_IntPush( vBits, 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 );
+        }
+        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) );
+        }
+        else if ( pObj->Type == WLC_OBJ_MUX )
+        {
+            assert( nRange0 == 1 );
+            assert( nRange1 == nRange );
+            assert( nRange2 == nRange );
+            for ( k = 0; k < nRange; k++ )
+                Vec_IntPush( vBits, 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) );
+        }
+        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) );
+        }
+        else if ( pObj->Type == WLC_OBJ_BIT_NOT )
+        {
+            assert( nRange == nRange0 );
+            for ( k = 0; k < nRange; k++ )
+                Vec_IntPush( vBits, 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]) );
+        }
+        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]) );
+        }
+        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]) );
+        }
+        else if ( pObj->Type == WLC_OBJ_BIT_SELECT )
+        {
+            int End = Wlc_ObjRangeEnd(pObj);
+            int Beg = Wlc_ObjRangeBeg(pObj);
+            assert( nRange == End - Beg + 1 );
+            for ( k = Beg; k <= End; k++ )
+                Vec_IntPush( vBits, pFans0[k] );
+        }
+        else if ( pObj->Type == WLC_OBJ_BIT_CONCAT )
+        {
+            int iFanin, nTotal = 0;
+            Wlc_ObjForEachFanin( pObj, iFanin, k )
+                nTotal += Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
+            assert( nRange == nTotal );
+            Wlc_ObjForEachFaninReverse( pObj, iFanin, k )
+            {
+                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] );
+            }
+        }
+        else if ( pObj->Type == WLC_OBJ_BIT_ZEROPAD || pObj->Type == WLC_OBJ_BIT_SIGNEXT )
+        {
+            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] );
+            for (      ; k < nRange; k++ )
+                Vec_IntPush( vBits, Pad );
+        }
+        else if ( pObj->Type == WLC_OBJ_LOGIC_NOT )
+        {
+            iLit = Wlc_NtkComputeReduction( pNew, pFans0, nRange, WLC_OBJ_REDUCT_OR );
+            assert( nRange == 1 );
+            Vec_IntPush( vBits, 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 );
+            assert( nRange == 1 );
+            Vec_IntPush( vBits, 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 );
+            assert( nRange == 1 );
+            Vec_IntPush( vBits, Gia_ManHashOr(pNew, iLit0, iLit1) );
+        }
+        else if ( pObj->Type == WLC_OBJ_COMP_EQU || pObj->Type == WLC_OBJ_COMP_NOT )
+        {
+            int iLit = 0;
+            assert( nRange == 1 );
+            assert( 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) );
+        }
+        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;
+            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) );
+        }
+        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 )
+        {
+            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 );
+        }
+        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;
+            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 );
+            }
+            assert( Vec_IntSize(vTemp3) == nRange );
+            Vec_IntAppend( vBits, vTemp3 );
+        }
+        else assert( 0 );
+    }
+    assert( nBits == Vec_IntSize(vBits) );
+    Vec_IntFree( vTemp0 );
+    Vec_IntFree( vTemp1 );
+    Vec_IntFree( vTemp2 );
+    Vec_IntFree( vTemp3 );
+    // create POs
+    Wlc_NtkForEachPo( p, pObj, i )
+    {
+        nRange = Wlc_ObjRange( pObj );
+        nRange0 = Wlc_ObjFaninNum(pObj) > 0 ? Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) ) : -1;
+        assert( nRange == nRange0 );
+        pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) );
+        for ( k = 0; k < nRange; k++ )
+            Gia_ManAppendCo( pNew, pFans0[k] );
+    }
+    Vec_IntFree( vBits );
+    Vec_IntErase( &p->vCopies );
+    // finalize and cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+