diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/base/cba/cba.h | 112 | ||||
-rw-r--r-- | src/base/cba/cbaBlast.c | 48 | ||||
-rw-r--r-- | src/base/cba/cbaBuild.c | 5 | ||||
-rw-r--r-- | src/base/cba/cbaCom.c | 305 | ||||
-rw-r--r-- | src/base/cba/cbaNtk.c | 15 | ||||
-rw-r--r-- | src/base/cba/cbaPrs.h | 16 | ||||
-rw-r--r-- | src/base/cba/cbaReadBlif.c | 7 | ||||
-rw-r--r-- | src/base/cba/cbaReadVer.c | 11 | ||||
-rw-r--r-- | src/base/cba/cbaSimple.c | 65 | ||||
-rw-r--r-- | src/base/cba/cbaWriteBlif.c | 5 | ||||
-rw-r--r-- | src/base/cba/cbaWriteVer.c | 180 |
11 files changed, 606 insertions, 163 deletions
diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h index 70f479ab..5c13efdc 100644 --- a/src/base/cba/cba.h +++ b/src/base/cba/cba.h @@ -66,16 +66,16 @@ typedef enum { CBA_NODE_BUF, // 3: buffer CBA_NODE_INV, // 4: inverter CBA_NODE_AND, // 5: AND - CBA_NODE_NAND, // 6: NAND - CBA_NODE_OR, // 7: OR - CBA_NODE_NOR, // 8: NOR - CBA_NODE_XOR, // 9: XOR - CBA_NODE_XNOR, // 10 XNOR - CBA_NODE_MUX, // 11: MUX - CBA_NODE_MAJ, // 12: MAJ - CBA_NODE_AND00, // 13: AND00 - CBA_NODE_AND01, // 14: AND01 - CBA_NODE_AND10, // 15: AND10 + CBA_NODE_AND00, // 6: AND00 + CBA_NODE_AND01, // 7: AND01 + CBA_NODE_AND10, // 8: AND10 + CBA_NODE_NAND, // 9: NAND + CBA_NODE_OR, // 10: OR + CBA_NODE_NOR, // 11: NOR + CBA_NODE_XOR, // 12: XOR + CBA_NODE_XNOR, // 13 XNOR + CBA_NODE_MUX, // 14: MUX + CBA_NODE_MAJ, // 15: MAJ CBA_NODE_UNKNOWN // 16: unknown } Cba_NodeType_t; @@ -130,6 +130,7 @@ struct Cba_Ntk_t_ static inline char * Cba_ManName( Cba_Man_t * p ) { return p->pName; } +static inline char * Cba_ManSpec( Cba_Man_t * p ) { return p->pSpec; } static inline int Cba_ManNtkNum( Cba_Man_t * p ) { return Vec_PtrSize(&p->vNtks) - 1; } static inline int Cba_ManNtkId( Cba_Man_t * p, char * pName ) { return Abc_NamStrFind(p->pModels, pName); } static inline Cba_Ntk_t * Cba_ManNtk( Cba_Man_t * p, int i ) { assert( i > 0 ); return (Cba_Ntk_t *)Vec_PtrEntry(&p->vNtks, i); } @@ -145,6 +146,9 @@ static inline int Cba_NtkObjNum( Cba_Ntk_t * p ) { r static inline int Cba_NtkPiNum( Cba_Ntk_t * p ) { return Vec_IntSize(&p->vInputs); } static inline int Cba_NtkPoNum( Cba_Ntk_t * p ) { return Vec_IntSize(&p->vOutputs); } static inline int Cba_NtkBoxNum( Cba_Ntk_t * p ) { return Vec_IntSize(&p->vBoxes); } +static inline int Cba_NtkBoxNumCount( Cba_Ntk_t * p ) { return Vec_IntCountEntry(&p->vTypes, CBA_OBJ_BOX); } +static inline int Cba_NtkNodeNum( Cba_Ntk_t * p ) { return Vec_IntCountEntry(&p->vTypes, CBA_OBJ_NODE); } + static inline int Cba_NtkPi( Cba_Ntk_t * p, int i ) { return Vec_IntEntry(&p->vInputs, i); } static inline int Cba_NtkPo( Cba_Ntk_t * p, int i ) { return Vec_IntEntry(&p->vOutputs, i); } static inline char * Cba_NtkStr( Cba_Ntk_t * p, int i ) { return Abc_NamStr(p->pDesign->pNames, i); } @@ -263,23 +267,31 @@ static inline int Cba_ManHandleBuffer( Cba_Man_t * p, int iFanin ) pArray[1] = iFanin; return h; } -static inline void Cba_ManSetupArray( Cba_Man_t * p, Vec_Int_t * vTo, Vec_Int_t * vFrom ) +static inline void Cba_ManAllocArray( Cba_Man_t * p, Vec_Int_t * vTo, int nSize ) { - if ( Vec_IntSize(vFrom) == 0 ) + if ( nSize == 0 ) return; - vTo->nSize = vTo->nCap = Vec_IntSize(vFrom); - vTo->pArray = (int *)Vec_SetFetch( Cba_ManMem(p), sizeof(int) * Vec_IntSize(vFrom) ); - memcpy( Vec_IntArray(vTo), Vec_IntArray(vFrom), sizeof(int) * Vec_IntSize(vFrom) ); - Vec_IntClear( vFrom ); + vTo->nSize = 0; + vTo->nCap = nSize; + vTo->pArray = (int *)Vec_SetFetch( Cba_ManMem(p), sizeof(int) * nSize ); } static inline void Cba_ManFetchArray( Cba_Man_t * p, Vec_Int_t * vTo, int nSize ) { if ( nSize == 0 ) return; - vTo->nSize = vTo->nCap = nSize; + vTo->nSize = vTo->nCap = nSize; vTo->pArray = (int *)Vec_SetFetch( Cba_ManMem(p), sizeof(int) * nSize ); memset( Vec_IntArray(vTo), 0xff, sizeof(int) * nSize ); } +static inline void Cba_ManSetupArray( Cba_Man_t * p, Vec_Int_t * vTo, Vec_Int_t * vFrom ) +{ + if ( Vec_IntSize(vFrom) == 0 ) + return; + vTo->nSize = vTo->nCap = Vec_IntSize(vFrom); + vTo->pArray = (int *)Vec_SetFetch( Cba_ManMem(p), sizeof(int) * Vec_IntSize(vFrom) ); + memcpy( Vec_IntArray(vTo), Vec_IntArray(vFrom), sizeof(int) * Vec_IntSize(vFrom) ); + Vec_IntClear( vFrom ); +} // constructors desctructors static inline Cba_Ntk_t * Cba_NtkAlloc( Cba_Man_t * p, char * pName ) @@ -303,37 +315,29 @@ static inline void Cba_NtkResize( Cba_Ntk_t * p, int nObjs ) Cba_ManFetchArray( p->pDesign, &p->vFanins, nObjs ); Cba_ManFetchArray( p->pDesign, &p->vNameIds, nObjs ); } -static inline Cba_Man_t * Cba_ManAlloc( char * pFileName ) +static inline Cba_Man_t * Cba_ManAlloc( Cba_Man_t * pOld, char * pFileName ) { Cba_Man_t * p = ABC_CALLOC( Cba_Man_t, 1 ); - p->pName = Extra_FileDesignName( pFileName ); - p->pSpec = Abc_UtilStrsav( pFileName ); - p->pNames = Abc_NamStart( 1000, 24 ); - p->pModels = Abc_NamStart( 1000, 24 ); - p->pFuncs = Abc_NamStart( 1000, 24 ); - Vec_SetAlloc_( &p->Mem, 20 ); + p->pName = pOld ? Abc_UtilStrsav( Cba_ManName(pOld) ) : Extra_FileDesignName( pFileName ); + p->pSpec = pOld ? Abc_UtilStrsav( Cba_ManSpec(pOld) ) : Abc_UtilStrsav( pFileName ); + p->pNames = pOld ? Abc_NamRef( pOld->pNames ) : Abc_NamStart( 1000, 24 ); + p->pModels = pOld ? Abc_NamRef( pOld->pModels ) : Abc_NamStart( 1000, 24 ); + p->pFuncs = pOld ? Abc_NamRef( pOld->pFuncs ) : Abc_NamStart( 1000, 24 ); + p->iRoot = 1; + Vec_SetAlloc_( &p->Mem, 18 ); Vec_PtrPush( &p->vNtks, NULL ); - p->iRoot = 1; return p; } static inline Cba_Man_t * Cba_ManClone( Cba_Man_t * pOld ) { Cba_Ntk_t * pNtk, * pNtkNew; int i; - Cba_Man_t * p = ABC_CALLOC( Cba_Man_t, 1 ); - p->pName = Extra_FileDesignName( pOld->pName ); - p->pSpec = Abc_UtilStrsav( pOld->pSpec ); - p->pNames = Abc_NamRef( pOld->pNames ); - p->pModels = Abc_NamRef( pOld->pModels ); - p->pFuncs = Abc_NamRef( pOld->pFuncs ); - p->iRoot = 1; - Vec_SetAlloc_( &p->Mem, 20 ); - Vec_PtrPush( &p->vNtks, NULL ); + Cba_Man_t * p = Cba_ManAlloc( pOld, NULL ); Cba_ManForEachNtk( pOld, pNtk, i ) { pNtkNew = Cba_NtkAlloc( p, Cba_NtkName(pNtk) ); Cba_ManFetchArray( p, &pNtkNew->vInputs, Cba_NtkPiNum(pNtk) ); Cba_ManFetchArray( p, &pNtkNew->vOutputs, Cba_NtkPoNum(pNtk) ); - Cba_ManFetchArray( p, &pNtkNew->vBoxes, Cba_NtkBoxNum(pNtk) ); + Cba_ManFetchArray( p, &pNtkNew->vBoxes, Cba_NtkBoxNumCount(pNtk) ); Vec_IntShrink( &pNtkNew->vBoxes, 0 ); } assert( Cba_ManNtkNum(p) == Cba_ManNtkNum(pOld) ); @@ -367,6 +371,26 @@ static inline int Cba_ManMemory( Cba_Man_t * p ) return nMem; } +static inline Cba_NtkPrintStats( Cba_Ntk_t * p ) +{ + printf( "%-32s ", Cba_NtkName(p) ); + printf( "pi =%5d ", Cba_NtkPiNum(p) ); + printf( "pi =%5d ", Cba_NtkPoNum(p) ); + printf( "box =%6d ", Cba_NtkBoxNum(p) ); + printf( "node =%6d ", Cba_NtkNodeNum(p) ); + printf( "obj =%6d ", Cba_NtkObjNum(p) ); + printf( "\n" ); +} +static inline Cba_ManPrintStats( Cba_Man_t * p, int fVerbose ) +{ + Cba_Ntk_t * pNtk; int i; + Cba_ManForEachNtk( p, pNtk, i ) + { + printf( "Module %4d : ", i ); + Cba_NtkPrintStats( pNtk ); + } +} + static inline Cba_NodeType_t Ptr_SopToType( char * pSop ) { if ( !strcmp(pSop, " 1\n") ) return CBA_NODE_C0; @@ -397,9 +421,13 @@ static inline char * Ptr_TypeToName( Cba_NodeType_t Type ) if ( Type == CBA_NODE_AND00 ) return "and00"; if ( Type == CBA_NODE_AND01 ) return "and01"; if ( Type == CBA_NODE_AND10 ) return "and10"; + if ( Type == CBA_NODE_NAND ) return "nand"; if ( Type == CBA_NODE_OR ) return "or"; + if ( Type == CBA_NODE_NOR ) return "nor"; if ( Type == CBA_NODE_XOR ) return "xor"; if ( Type == CBA_NODE_XNOR ) return "xnor"; + if ( Type == CBA_NODE_MUX ) return "mux"; + if ( Type == CBA_NODE_MAJ ) return "maj"; assert( 0 ); return "???"; } @@ -413,13 +441,22 @@ static inline char * Ptr_TypeToSop( Cba_NodeType_t Type ) if ( Type == CBA_NODE_AND00 ) return "00 1\n"; if ( Type == CBA_NODE_AND01 ) return "01 1\n"; if ( Type == CBA_NODE_AND10 ) return "10 1\n"; + if ( Type == CBA_NODE_NAND ) return "11 0\n"; if ( Type == CBA_NODE_OR ) return "00 0\n"; + if ( Type == CBA_NODE_NOR ) return "00 1\n"; if ( Type == CBA_NODE_XOR ) return "01 1\n10 1\n"; if ( Type == CBA_NODE_XNOR ) return "00 1\n11 1\n"; + if ( Type == CBA_NODE_MUX ) return "11- 1\n0-1 1\n"; + if ( Type == CBA_NODE_MAJ ) return "11- 1\n1-1 1\n-11 1\n"; assert( 0 ); return "???"; } + +/*=== cbaBlast.c =========================================================*/ +extern Gia_Man_t * Cba_ManExtract( Cba_Man_t * p, int fBuffers, int fVerbose ); +extern Cba_Man_t * Cba_ManInsertGia( Cba_Man_t * p, Gia_Man_t * pGia ); +extern void * Cba_ManInsertAbc( Cba_Man_t * p, void * pAbc ); /*=== cbaBuild.c =========================================================*/ extern Cba_Man_t * Cba_ManBuild( Cba_Man_t * p ); /*=== cbaReadBlif.c =========================================================*/ @@ -431,13 +468,16 @@ extern void Cba_PrsWriteBlif( char * pFileName, Cba_Man_t * p ); extern void Cba_ManWriteBlif( char * pFileName, Cba_Man_t * p ); /*=== cbaWriteVer.c =========================================================*/ extern void Cba_PrsWriteVerilog( char * pFileName, Cba_Man_t * p ); +extern void Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p ); /*=== cbaNtk.c =========================================================*/ extern void Cba_ManAssignInternNames( Cba_Man_t * p ); extern int Cba_NtkNodeNum( Cba_Ntk_t * p ); extern int Cba_ManObjNum( Cba_Man_t * p ); extern Cba_Man_t * Cba_ManDupStart( Cba_Man_t * p, Vec_Int_t * vNtkSizes ); extern Cba_Man_t * Cba_ManDup( Cba_Man_t * p ); - +/*=== cbaSimple.c =========================================================*/ +extern Cba_Man_t * Cba_PrsReadPtr( Vec_Ptr_t * vDes ); +extern void Ptr_ManFreeDes( Vec_Ptr_t * vDes ); ABC_NAMESPACE_HEADER_END diff --git a/src/base/cba/cbaBlast.c b/src/base/cba/cbaBlast.c index 25476f43..808f3035 100644 --- a/src/base/cba/cbaBlast.c +++ b/src/base/cba/cbaBlast.c @@ -63,26 +63,28 @@ int Cba_ManAddBarbuf( Gia_Man_t * pNew, int iRes, Cba_Man_t * p, int iLNtk, int } return iBufLit; } -int Cba_ManExtract_rec( Gia_Man_t * pNew, Cba_Ntk_t * p, int i, Vec_Int_t * vMap ) +int Cba_ManExtract_rec( Gia_Man_t * pNew, Cba_Ntk_t * p, int i, int fBuffers, Vec_Int_t * vMap ) { int iRes = Cba_NtkCopy( p, i ); if ( iRes >= 0 ) return iRes; if ( Cba_ObjIsCo(p, i) ) - iRes = Cba_ManExtract_rec( pNew, p, Cba_ObjFanin0(p, i), vMap ); + iRes = Cba_ManExtract_rec( pNew, p, Cba_ObjFanin0(p, i), fBuffers, vMap ); else if ( Cba_ObjIsBo(p, i) ) { Cba_Ntk_t * pBox = Cba_ObjBoModel( p, i ); int iObj = Cba_NtkPo( pBox, Cba_ObjCioIndex(p, i) ); - iRes = Cba_ManExtract_rec( pNew, pBox, iObj, vMap ); - iRes = Cba_ManAddBarbuf( pNew, iRes, p->pDesign, Cba_NtkId(p), i, Cba_NtkId(pBox), iObj, vMap ); + iRes = Cba_ManExtract_rec( pNew, pBox, iObj, fBuffers, vMap ); + if ( fBuffers ) + iRes = Cba_ManAddBarbuf( pNew, iRes, p->pDesign, Cba_NtkId(p), i, Cba_NtkId(pBox), iObj, vMap ); } else if ( Cba_ObjIsPi(p, i) ) { Cba_Ntk_t * pHost = Cba_NtkHostNtk( p ); int iObj = Cba_ObjBoxBi( pHost, Cba_NtkHostObj(p), Cba_ObjCioIndex(p, i) ); - iRes = Cba_ManExtract_rec( pNew, pHost, iObj, vMap ); - iRes = Cba_ManAddBarbuf( pNew, iRes, p->pDesign, Cba_NtkId(p), i, Cba_NtkId(pHost), iObj, vMap ); + iRes = Cba_ManExtract_rec( pNew, pHost, iObj, fBuffers, vMap ); + if ( fBuffers ) + iRes = Cba_ManAddBarbuf( pNew, iRes, p->pDesign, Cba_NtkId(p), i, Cba_NtkId(pHost), iObj, vMap ); } else if ( Cba_ObjIsNode(p, i) ) { @@ -100,15 +102,15 @@ int Cba_ManExtract_rec( Gia_Man_t * pNew, Cba_Ntk_t * p, int i, Vec_Int_t * vMap else if ( pFanins[0] == 1 ) { if ( Type == CBA_NODE_BUF ) - iRes = Cba_ManExtract_rec( pNew, p, pFanins[1], vMap ); + iRes = Cba_ManExtract_rec( pNew, p, pFanins[1], fBuffers, vMap ); else if ( Type == CBA_NODE_INV ) - iRes = Abc_LitNot( Cba_ManExtract_rec( pNew, p, pFanins[1], vMap ) ); + iRes = Abc_LitNot( Cba_ManExtract_rec( pNew, p, pFanins[1], fBuffers, vMap ) ); else assert( 0 ); } else { for ( k = 0; k < pFanins[0]; k++ ) - pLits[k] = Cba_ManExtract_rec( pNew, p, pFanins[k+1], vMap ); + pLits[k] = Cba_ManExtract_rec( pNew, p, pFanins[k+1], fBuffers, vMap ); if ( Type == CBA_NODE_AND ) iRes = Gia_ManHashAnd( pNew, pLits[0], pLits[1] ); else if ( Type == CBA_NODE_OR ) @@ -124,7 +126,7 @@ int Cba_ManExtract_rec( Gia_Man_t * pNew, Cba_Ntk_t * p, int i, Vec_Int_t * vMap Cba_NtkSetCopy( p, i, iRes ); return iRes; } -Gia_Man_t * Cba_ManExtract( Cba_Man_t * p, int fVerbose ) +Gia_Man_t * Cba_ManExtract( Cba_Man_t * p, int fBuffers, int fVerbose ) { Cba_Ntk_t * pRoot = Cba_ManRoot(p); Gia_Man_t * pNew, * pTemp; @@ -154,7 +156,7 @@ Gia_Man_t * Cba_ManExtract( Cba_Man_t * p, int fVerbose ) pNew->vBarBufs = Vec_IntAlloc( 10000 ); vMap = Vec_IntStartFull( 10000 ); Cba_NtkForEachPo( pRoot, iObj, i ) - Cba_ManExtract_rec( pNew, pRoot, iObj, vMap ); + Cba_ManExtract_rec( pNew, pRoot, iObj, fBuffers, vMap ); Vec_IntFreeP( &vMap ); Gia_ManHashStop( pNew ); @@ -166,7 +168,7 @@ Gia_Man_t * Cba_ManExtract( Cba_Man_t * p, int fVerbose ) // cleanup pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); - Gia_ManPrintStats( pNew, NULL ); + //Gia_ManPrintStats( pNew, NULL ); return pNew; } @@ -347,7 +349,7 @@ Cba_Man_t * Cba_ManInsertGia( Cba_Man_t * p, Gia_Man_t * pGia ) ***********************************************************************/ Cba_Man_t * Cba_ManBlastTest( Cba_Man_t * p ) { - Gia_Man_t * pGia = Cba_ManExtract( p, 0 ); + Gia_Man_t * pGia = Cba_ManExtract( p, 1, 0 ); Cba_Man_t * pNew = Cba_ManInsertGia( p, pGia ); Gia_ManStop( pGia ); Cba_ManAssignInternNames( pNew ); @@ -355,6 +357,26 @@ Cba_Man_t * Cba_ManBlastTest( Cba_Man_t * p ) } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Cba_ManInsertAbc( Cba_Man_t * p, void * pAbc ) +{ + Abc_Ntk_t * pNtk = pAbc; + Cba_Man_t * pNew = NULL; + return pNew; +} + + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/cba/cbaBuild.c b/src/base/cba/cbaBuild.c index b353e8f6..ddacc409 100644 --- a/src/base/cba/cbaBuild.c +++ b/src/base/cba/cbaBuild.c @@ -204,7 +204,6 @@ Cba_Ntk_t * Cba_NtkBuild( Cba_Man_t * pNew, Cba_Ntk_t * pNtk, Vec_Int_t * vMap, { ObjId = Vec_IntEntry( &pNtkNew->vBoxes, nBoxes++ ); pNtkBox = Cba_ObjBoxModel( pNtk, iObj ); - Cba_NtkSetHost( pNtkBox, Cba_NtkId(pNtk), ObjId ); // collect fanins Vec_IntFill( vTemp, Cba_NtkPiNum(pNtkBox), -1 ); Vec_IntForEachEntry( vFanins, Index, i ) @@ -227,6 +226,7 @@ Cba_Ntk_t * Cba_NtkBuild( Cba_Man_t * pNew, Cba_Ntk_t * pNtk, Vec_Int_t * vMap, // create box Vec_IntWriteEntry( &pNtkNew->vTypes, ObjId, CBA_OBJ_BOX ); Vec_IntWriteEntry( &pNtkNew->vFuncs, ObjId, Cba_ManNtkId(pNew, Cba_NtkName(pNtkBox)) ); + Cba_NtkSetHost( Cba_ObjBoxModel(pNtkNew, ObjId), Cba_NtkId(pNtkNew), ObjId ); // create box inputs Cba_BoxForEachBi( pNtkNew, ObjId, FaninId, i ) { @@ -311,7 +311,8 @@ Cba_Man_t * Cba_ManBuild( Cba_Man_t * p ) Vec_Int_t * vMap = Vec_IntStartFull( Abc_NamObjNumMax(p->pNames) + 1 ); Vec_Int_t * vNonDr = Vec_IntAlloc( 1000 ); Vec_Int_t * vTemp = Vec_IntAlloc( 1000 ); - Cba_Ntk_t * pNtk; int i, nObjs; + Cba_Ntk_t * pNtk; + int i, nObjs; assert( Abc_NamObjNumMax(p->pModels) == Cba_ManNtkNum(p) + 1 ); Cba_ManForEachNtk( p, pNtk, i ) { diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c index 94eb4b88..05f4dfe6 100644 --- a/src/base/cba/cbaCom.c +++ b/src/base/cba/cbaCom.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "cba.h" +#include "proof/cec/cec.h" #include "base/main/mainInt.h" ABC_NAMESPACE_IMPL_START @@ -30,12 +31,14 @@ ABC_NAMESPACE_IMPL_START static int Cba_CommandRead ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Cba_CommandWrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Cba_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Cba_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Cba_CommandPut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Cba_CommandGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Cba_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Cba_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static inline Cba_Ntk_t * Cba_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Cba_Ntk_t *)pAbc->pAbcCba; } -static inline void Cba_AbcFreeNtk( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcCba ) Cba_ManFree(Cba_NtkMan(Cba_AbcGetNtk(pAbc))); } -static inline void Cba_AbcUpdateNtk( Abc_Frame_t * pAbc, Cba_Ntk_t * pNtk ) { Cba_AbcFreeNtk(pAbc); pAbc->pAbcCba = pNtk; } +static inline Cba_Man_t * Cba_AbcGetMan( Abc_Frame_t * pAbc ) { return (Cba_Man_t *)pAbc->pAbcCba; } +static inline void Cba_AbcFreeMan( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcCba ) Cba_ManFree(Cba_AbcGetMan(pAbc)); } +static inline void Cba_AbcUpdateMan( Abc_Frame_t * pAbc, Cba_Man_t * p ) { Cba_AbcFreeMan(pAbc); pAbc->pAbcCba = p; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -57,7 +60,9 @@ void Cba_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "New word level", "@read", Cba_CommandRead, 0 ); Cmd_CommandAdd( pAbc, "New word level", "@write", Cba_CommandWrite, 0 ); Cmd_CommandAdd( pAbc, "New word level", "@ps", Cba_CommandPs, 0 ); - Cmd_CommandAdd( pAbc, "New word level", "@blast", Cba_CommandBlast, 0 ); + Cmd_CommandAdd( pAbc, "New word level", "@put", Cba_CommandPut, 0 ); + Cmd_CommandAdd( pAbc, "New word level", "@get", Cba_CommandGet, 0 ); + Cmd_CommandAdd( pAbc, "New word level", "@cec", Cba_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "New word level", "@test", Cba_CommandTest, 0 ); } @@ -74,7 +79,7 @@ void Cba_Init( Abc_Frame_t * pAbc ) ******************************************************************************/ void Cba_End( Abc_Frame_t * pAbc ) { - Cba_AbcFreeNtk( pAbc ); + Cba_AbcFreeMan( pAbc ); } @@ -92,14 +97,17 @@ void Cba_End( Abc_Frame_t * pAbc ) int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pFile; - Cba_Ntk_t * pNtk = NULL; + Cba_Man_t * p = NULL, * pTemp; char * pFileName = NULL; - int c, fVerbose = 0; + int c, fUseAbc = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "avh" ) ) != EOF ) { switch ( c ) { + case 'a': + fUseAbc ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -127,12 +135,30 @@ int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv ) fclose( pFile ); // perform reading - //pNtk = Cba_ReadVer( pFileName ); - Cba_AbcUpdateNtk( pAbc, pNtk ); + if ( fUseAbc ) + { + extern Vec_Ptr_t * Ptr_AbcDeriveDes( Abc_Ntk_t * pNtk ); + Abc_Ntk_t * pAbcNtk = Io_ReadNetlist( pFileName, Io_ReadFileType(pFileName), 0 ); + Vec_Ptr_t * vDes = Ptr_AbcDeriveDes( pAbcNtk ); + p = Cba_PrsReadPtr( vDes ); + ABC_FREE( p->pSpec ); + p->pSpec = Abc_UtilStrsav( pAbcNtk->pSpec ); + Abc_NtkDelete( pAbcNtk ); + Ptr_ManFreeDes( vDes ); // points to names in pAbcNtk + } + else if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) ) + p = Cba_PrsReadBlif( pFileName ); + else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) + p = Cba_PrsReadVerilog( pFileName ); + else assert( 0 ); + p = Cba_ManBuild( pTemp = p ); + Cba_ManFree( pTemp ); + Cba_AbcUpdateMan( pAbc, p ); return 0; usage: - Abc_Print( -2, "usage: @read [-vh] <file_name>\n" ); - Abc_Print( -2, "\t reads word-level design from Verilog file\n" ); + Abc_Print( -2, "usage: @read [-avh] <file_name>\n" ); + Abc_Print( -2, "\t reads hierarchical design in BLIF or Verilog\n" ); + Abc_Print( -2, "\t-a : toggle using old ABC parser [default = %s]\n", fUseAbc? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -151,7 +177,7 @@ usage: ******************************************************************************/ int Cba_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Cba_Ntk_t * pNtk = Cba_AbcGetNtk(pAbc); + Cba_Man_t * p = Cba_AbcGetMan(pAbc); char * pFileName = NULL; int c, fVerbose = 0; Extra_UtilGetoptReset(); @@ -168,26 +194,35 @@ int Cba_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( pNtk == NULL ) + if ( p == NULL ) { Abc_Print( 1, "Cba_CommandWrite(): There is no current design.\n" ); return 0; } - if ( argc == globalUtilOptind ) - pFileName = Extra_FileNameGenericAppend( Cba_NtkMan(pNtk)->pName, "_out.v" ); - else if ( argc == globalUtilOptind + 1 ) + if ( argc == globalUtilOptind + 1 ) pFileName = argv[globalUtilOptind]; - else + else if ( argc == globalUtilOptind && p ) + pFileName = Extra_FileNameGenericAppend( Cba_ManName(p), "_out.v" ); + else { printf( "Output file name should be given on the command line.\n" ); return 0; } - //Cba_WriteVer( pNtk, pFileName ); + // perform writing + if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) ) + Cba_ManWriteBlif( pFileName, p ); + else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) + Cba_ManWriteVerilog( pFileName, p ); + else + { + printf( "Unrecognized output file extension.\n" ); + return 0; + } return 0; usage: Abc_Print( -2, "usage: @write [-vh]\n" ); - Abc_Print( -2, "\t writes the design into a file\n" ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t writes the design into a file in BLIF or Verilog\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -206,7 +241,7 @@ usage: ******************************************************************************/ int Cba_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Cba_Ntk_t * pNtk = Cba_AbcGetNtk(pAbc); + Cba_Man_t * p = Cba_AbcGetMan(pAbc); int c, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) @@ -222,12 +257,12 @@ int Cba_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( pNtk == NULL ) + if ( p == NULL ) { Abc_Print( 1, "Cba_CommandPs(): There is no current design.\n" ); return 0; } -// Cba_NtkPrintStats( pNtk, fDistrib, fVerbose ); + Cba_ManPrintStats( p, fVerbose ); return 0; usage: Abc_Print( -2, "usage: @ps [-vh]\n" ); @@ -248,19 +283,68 @@ usage: SeeAlso [] ******************************************************************************/ -int Cba_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Cba_CommandPut( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Cba_Man_t * p = Cba_AbcGetMan(pAbc); + Gia_Man_t * pGia = NULL; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( p == NULL ) + { + Abc_Print( 1, "Cba_CommandPut(): There is no current design.\n" ); + return 0; + } + pGia = Cba_ManExtract( p, 1, 0 ); + if ( pGia == NULL ) + { + Abc_Print( 1, "Cba_CommandPut(): Conversion to AIG has failed.\n" ); + return 0; + } + Abc_FrameUpdateGia( pAbc, pGia ); + return 0; +usage: + Abc_Print( -2, "usage: @put [-mvh]\n" ); + Abc_Print( -2, "\t extracts AIG with barrier buffers from the hierarchical design\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Cba_CommandGet( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Cba_Ntk_t * pNtk = Cba_AbcGetNtk(pAbc); - //Vec_Int_t * vBoxIds = NULL; - Gia_Man_t * pNew = NULL; - int c, fMulti = 0, fVerbose = 0; + Cba_Man_t * pNew, * p = Cba_AbcGetMan(pAbc); + int c, fMapped = 0, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF ) { switch ( c ) { case 'm': - fMulti ^= 1; + fMapped ^= 1; break; case 'v': fVerbose ^= 1; @@ -271,31 +355,148 @@ int Cba_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( pNtk == NULL ) + if ( p == NULL ) + { + Abc_Print( 1, "Cba_CommandGet(): There is no current design.\n" ); + return 0; + } + if ( fMapped ) + { + if ( pAbc->pNtkCur == NULL ) + { + Abc_Print( 1, "Cba_CommandGet(): There is no current mapped design.\n" ); + return 0; + } + pNew = Cba_ManInsertAbc( p, pAbc->pNtkCur ); + } + else + { + if ( pAbc->pGia == NULL ) + { + Abc_Print( 1, "Cba_CommandGet(): There is no current AIG.\n" ); + return 0; + } + pNew = Cba_ManInsertGia( p, pAbc->pGia ); + } + Cba_AbcUpdateMan( pAbc, pNew ); + return 0; +usage: + Abc_Print( -2, "usage: @get [-mvh]\n" ); + Abc_Print( -2, "\t extracts AIG or mapped network into the hierarchical design\n" ); + Abc_Print( -2, "\t-m : toggle using mapped network from main-space [default = %s]\n", fMapped? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Cba_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Cba_Man_t * pTemp, * p = Cba_AbcGetMan(pAbc); + Cec_ParCec_t ParsCec, * pPars = &ParsCec; + Gia_Man_t * pFirst, * pSecond, * pMiter; + char * FileName, * pStr, ** pArgvNew; + int c, nArgcNew, fDumpMiter = 0, fVerbose = 0; + FILE * pFile; + Cec_ManCecSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( p == NULL ) { - Abc_Print( 1, "Cba_CommandBlast(): There is no current design.\n" ); + Abc_Print( 1, "Cba_CommandCec(): There is no current design.\n" ); return 0; } - if ( fMulti ) + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( nArgcNew != 1 ) { -// vBoxIds = Cba_NtkCollectMultipliers( pNtk ); -// if ( vBoxIds == NULL ) -// Abc_Print( 1, "Warning: There is no multipliers in the design.\n" ); + if ( p->pSpec == NULL ) + { + Abc_Print( -1, "File name is not given on the command line.\n" ); + return 1; + } + FileName = p->pSpec; + } + else + FileName = pArgvNew[0]; + // fix the wrong symbol + for ( pStr = FileName; *pStr; pStr++ ) + if ( *pStr == '>' ) + *pStr = '\\'; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", FileName ); + if ( (FileName = Extra_FileGetSimilarName( FileName, ".v", ".blif", NULL, NULL, NULL )) ) + Abc_Print( 1, "Did you mean \"%s\"?", FileName ); + Abc_Print( 1, "\n" ); + return 1; + } + fclose( pFile ); + // extract AIG from the current design + pFirst = Cba_ManExtract( p, 0, 0 ); + if ( pFirst == NULL ) + { + Abc_Print( -1, "Extracting AIG from the current design has failed.\n" ); + return 0; } - // transform -// pNew = Cba_NtkBitBlast( pNtk, vBoxIds ); -// Vec_IntFreeP( &vBoxIds ); - if ( pNew == NULL ) + // extract AIG from the second design + if ( !strcmp( Extra_FileNameExtension(FileName), "blif" ) ) + p = Cba_PrsReadBlif( FileName ); + else if ( !strcmp( Extra_FileNameExtension(FileName), "v" ) ) + p = Cba_PrsReadVerilog( FileName ); + else assert( 0 ); + p = Cba_ManBuild( pTemp = p ); + Cba_ManFree( pTemp ); + pSecond = Cba_ManExtract( p, 0, 0 ); + Cba_ManFree( p ); + if ( pSecond == NULL ) { - Abc_Print( 1, "Cba_CommandBlast(): Bit-blasting has failed.\n" ); + Gia_ManStop( pFirst ); + Abc_Print( -1, "Extracting AIG from the original design has failed.\n" ); return 0; } - Abc_FrameUpdateGia( pAbc, pNew ); + // compute the miter + pMiter = Gia_ManMiter( pFirst, pSecond, 0, 1, 0, 0, pPars->fVerbose ); + if ( pMiter ) + { + int fDumpMiter = 0; + if ( fDumpMiter ) + { + Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" ); + Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 ); + } + pAbc->Status = Cec_ManVerify( pMiter, pPars ); + //Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb ); + Gia_ManStop( pMiter ); + } + Gia_ManStop( pFirst ); + Gia_ManStop( pSecond ); return 0; usage: - Abc_Print( -2, "usage: @blast [-mvh]\n" ); - Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" ); - Abc_Print( -2, "\t-m : toggle creating boxes for all multipliers in the design [default = %s]\n", fMulti? "yes": "no" ); + Abc_Print( -2, "usage: @cec [-vh]\n" ); + Abc_Print( -2, "\t combinational equivalence checking for the hierarchical design\n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -314,12 +515,7 @@ usage: ******************************************************************************/ int Cba_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Cba_ManReadDesExperiment( Abc_Ntk_t * pNtk ); - Abc_Ntk_t * pAbcNtk; - //Cba_Ntk_t * pNtk = Cba_AbcGetNtk(pAbc); -// char * pFileName = "c/hie/dump/1/netlist_1.v"; -// char * pFileName = "c/hie/dump/3/netlist_18.v"; - char * pFileName = "c/hie/dump/1/netlist_0.v"; + extern void Cba_PrsReadVerilogTest( char * pFileName ); int c, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) @@ -342,10 +538,7 @@ int Cba_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } */ - // transform - pAbcNtk = Io_ReadNetlist( pFileName, Io_ReadFileType(pFileName), 0 ); - Cba_ManReadDesExperiment( pAbcNtk ); - Abc_NtkDelete( pAbcNtk ); + Cba_PrsReadVerilogTest( NULL ); return 0; usage: Abc_Print( -2, "usage: @test [-vh]\n" ); diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c index 13949606..af48f227 100644 --- a/src/base/cba/cbaNtk.c +++ b/src/base/cba/cbaNtk.c @@ -74,13 +74,6 @@ void Cba_ManAssignInternNames( Cba_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Cba_NtkNodeNum( Cba_Ntk_t * p ) -{ - int iObj, Count = 0; - Cba_NtkForEachNode( p, iObj ) - Count++; - return Count; -} int Cba_ManObjNum( Cba_Man_t * p ) { Cba_Ntk_t * pNtk; @@ -136,6 +129,9 @@ void Cba_NtkDupStart( Cba_Ntk_t * pNew, Cba_Ntk_t * p ) Cba_ObjDupStart( pNew, p, iObj ); Cba_BoxForEachBo( p, iObj, iTerm, k ) Cba_ObjDupStart( pNew, p, iTerm ); + // connect box outputs to boxes + Cba_BoxForEachBo( p, iObj, iTerm, k ) + Vec_IntWriteEntry( &pNew->vFanins, Cba_NtkCopy(p, iTerm), Cba_NtkCopy(p, Cba_ObjFanin0(p, iTerm)) ); } assert( Cba_NtkBoxNum(p) == Cba_NtkBoxNum(pNew) ); } @@ -174,10 +170,11 @@ void Cba_NtkDupNodes( Cba_Ntk_t * pNew, Cba_Ntk_t * p, Vec_Int_t * vTemp ) // connect Cba_NtkForEachObjType( p, Type, i ) { - if ( Type == CBA_OBJ_PI || Type == CBA_OBJ_BOX ) + if ( Type == CBA_OBJ_PI || Type == CBA_OBJ_BOX || Type == CBA_OBJ_BO ) continue; - if ( Type == CBA_OBJ_PO || Type == CBA_OBJ_BI || Type == CBA_OBJ_BO ) + if ( Type == CBA_OBJ_PO || Type == CBA_OBJ_BI ) { + assert( Vec_IntEntry(&pNew->vFanins, Cba_NtkCopy(p, i)) == -1 ); Vec_IntWriteEntry( &pNew->vFanins, Cba_NtkCopy(p, i), Cba_NtkCopy(p, Cba_ObjFanin0(p, i)) ); continue; } diff --git a/src/base/cba/cbaPrs.h b/src/base/cba/cbaPrs.h index 3715935e..12a2c065 100644 --- a/src/base/cba/cbaPrs.h +++ b/src/base/cba/cbaPrs.h @@ -168,7 +168,7 @@ static inline Cba_Prs_t * Cba_PrsAlloc( char * pFileName ) p->pBuffer = pBuffer; p->pLimit = pLimit; p->pCur = pBuffer; - p->pDesign = Cba_ManAlloc( pFileName ); + p->pDesign = Cba_ManAlloc( NULL, pFileName ); return p; } static inline void Cba_PrsFree( Cba_Prs_t * p ) @@ -195,6 +195,20 @@ static inline void Cba_PrsFree( Cba_Prs_t * p ) ABC_FREE( p->pBuffer ); ABC_FREE( p ); } +static inline void Cba_PrsRemapBoxModels( Cba_Man_t * p ) +{ + Cba_Ntk_t * pNtk; + int i, Type, iObj; + Cba_ManForEachNtk( p, pNtk, i ) + Cba_NtkForEachObjType( pNtk, Type, iObj ) + if ( Type == CBA_OBJ_BOX ) + { + char * pName = Abc_NamStr( p->pNames, Cba_ObjFuncId(pNtk, iObj) ); + int iModelId = Abc_NamStrFind( p->pModels, pName ); + assert( iModelId > 0 ); + Vec_IntWriteEntry( &pNtk->vFuncs, iObj, iModelId ); + } +} //////////////////////////////////////////////////////////////////////// /// ITERATORS /// diff --git a/src/base/cba/cbaReadBlif.c b/src/base/cba/cbaReadBlif.c index 08152075..83ec12f5 100644 --- a/src/base/cba/cbaReadBlif.c +++ b/src/base/cba/cbaReadBlif.c @@ -64,9 +64,9 @@ static inline void Cba_PrsAddBlifDirectives( Cba_Prs_t * p ) for ( i = 1; s_BlifTypes[i]; i++ ) Abc_NamStrFindOrAdd( p->pDesign->pNames, (char *)s_BlifTypes[i], NULL ); assert( Abc_NamObjNumMax(p->pDesign->pNames) == i ); - Abc_NamStrFindOrAdd( p->pDesign->pFuncs, (char *)" 0\n", NULL ); // default const 0 function - Abc_NamStrFindOrAdd( p->pDesign->pFuncs, (char *)"1 1\n", NULL ); // default buffer function - assert( Abc_NamObjNumMax(p->pDesign->pFuncs) == 3 ); + for ( i = 1; i < CBA_NODE_UNKNOWN; i++ ) + Abc_NamStrFindOrAdd( p->pDesign->pFuncs, Ptr_TypeToSop(i), NULL ); + assert( Abc_NamObjNumMax(p->pDesign->pFuncs) == i-1 ); } @@ -408,6 +408,7 @@ Cba_Man_t * Cba_PrsReadBlif( char * pFileName ) if ( Cba_PrsErrorPrint(p) ) ABC_SWAP( Cba_Man_t *, pDesign, p->pDesign ); Cba_PrsFree( p ); + Cba_PrsRemapBoxModels( pDesign ); return pDesign; } diff --git a/src/base/cba/cbaReadVer.c b/src/base/cba/cbaReadVer.c index c5718dc1..714830ab 100644 --- a/src/base/cba/cbaReadVer.c +++ b/src/base/cba/cbaReadVer.c @@ -80,7 +80,7 @@ static inline int Cba_IsChar( char c ) { return (c >= 'a' && c <= 'z') || (c static inline int Cba_IsSymb1( char c ) { return Cba_IsChar(c) || c == '_'; } static inline int Cba_IsSymb2( char c ) { return Cba_IsSymb1(c) || Cba_IsDigit(c) || c == '$'; } -static inline int Cba_PrsIsChar( Cba_Prs_t * p, char c ) { return *p->pCur == c; } +static inline int Cba_PrsIsChar( Cba_Prs_t * p, char c ) { return p->pCur[0] == c; } static inline int Cba_PrsIsChar1( Cba_Prs_t * p, char c ) { return p->pCur[1] == c; } static inline int Cba_PrsIsDigit( Cba_Prs_t * p ) { return Cba_IsDigit(*p->pCur); } @@ -720,6 +720,7 @@ Cba_Man_t * Cba_PrsReadVerilog( char * pFileName ) if ( Cba_PrsErrorPrint(p) ) ABC_SWAP( Cba_Man_t *, pDesign, p->pDesign ); Cba_PrsFree( p ); + Cba_PrsRemapBoxModels( pDesign ); return pDesign; } @@ -727,18 +728,18 @@ void Cba_PrsReadVerilogTest( char * pFileName ) { abctime clk = Abc_Clock(); extern void Cba_PrsWriteVerilog( char * pFileName, Cba_Man_t * p ); -// Cba_Man_t * p = Cba_PrsReadVerilog( "c/hie/dump/1/netlist_1.v" ); + Cba_Man_t * p = Cba_PrsReadVerilog( "c/hie/dump/1/netlist_1.v" ); // Cba_Man_t * p = Cba_PrsReadVerilog( "aga/me/me_wide.v" ); - Cba_Man_t * p = Cba_PrsReadVerilog( "aga/ray/ray_wide.v" ); +// Cba_Man_t * p = Cba_PrsReadVerilog( "aga/ray/ray_wide.v" ); if ( !p ) return; printf( "Finished reading %d networks. ", Cba_ManNtkNum(p) ); printf( "NameIDs = %d. ", Abc_NamObjNumMax(p->pNames) ); printf( "Memory = %.2f MB. ", 1.0*Cba_ManMemory(p)/(1<<20) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); // Abc_NamPrint( p->pDesign->pNames ); -// Cba_PrsWriteVerilog( "c/hie/dump/1/netlist_1_out.v", p ); + Cba_PrsWriteVerilog( "c/hie/dump/1/netlist_1_out.v", p ); // Cba_PrsWriteVerilog( "aga/me/me_wide_out.v", p ); - Cba_PrsWriteVerilog( "aga/ray/ray_wide_out.v", p ); +// Cba_PrsWriteVerilog( "aga/ray/ray_wide_out.v", p ); Cba_ManFree( p ); } diff --git a/src/base/cba/cbaSimple.c b/src/base/cba/cbaSimple.c index 7d363be9..7fe6cb0a 100644 --- a/src/base/cba/cbaSimple.c +++ b/src/base/cba/cbaSimple.c @@ -60,6 +60,8 @@ Cba_NodeType_t Ptr_HopToType( Abc_Obj_t * pObj ) }; assert( Abc_ObjIsNode(pObj) ); uTruth = Hop_ManComputeTruth6( (Hop_Man_t *)Abc_ObjNtk(pObj)->pManFunc, (Hop_Obj_t *)pObj->pData, Abc_ObjFaninNum(pObj) ); + if ( uTruth == 0 ) return CBA_NODE_C0; + if ( uTruth == ~(word)0 ) return CBA_NODE_C1; if ( uTruth == uTruths6[0] ) return CBA_NODE_BUF; if ( uTruth == ~uTruths6[0] ) return CBA_NODE_INV; if ( uTruth == (uTruths6[0] & uTruths6[1]) ) return CBA_NODE_AND; @@ -107,7 +109,11 @@ Vec_Ptr_t * Ptr_AbcDeriveNode( Abc_Obj_t * pObj ) Vec_Ptr_t * vNode = Vec_PtrAlloc( 2 + Abc_ObjFaninNum(pObj) ); assert( Abc_ObjIsNode(pObj) ); Vec_PtrPush( vNode, Ptr_AbcObjName(pObj) ); - Vec_PtrPush( vNode, Abc_Int2Ptr(Ptr_HopToType(pObj)) ); + if ( Abc_NtkHasAig(pObj->pNtk) ) + Vec_PtrPush( vNode, Abc_Int2Ptr(Ptr_HopToType(pObj)) ); + else if ( Abc_NtkHasSop(pObj->pNtk) ) + Vec_PtrPush( vNode, Abc_Int2Ptr(Ptr_SopToType((char *)pObj->pData)) ); + else assert( 0 ); Abc_ObjForEachFanin( pObj, pFanin, i ) Vec_PtrPush( vNode, Ptr_AbcObjName(pFanin) ); assert( Ptr_CheckArray(vNode) ); @@ -601,47 +607,36 @@ void Cba_PrsReadBoxes( Cba_Man_t * p, Vec_Ptr_t * vBoxes, Vec_Int_t * vTypesCur, Vec_IntPush( vFaninsCur, Cba_ManHandleArray(p, Cba_PrsReadList(p, vBox, vList, 0, 1)) ); } } -void Cba_PrsReadModule( Cba_Man_t * p, Cba_Ntk_t * pNtk, Vec_Ptr_t * vNtk ) -{ - Vec_Int_t * vInputsCur = Vec_IntAlloc( 1000 ); - Vec_Int_t * vOutputsCur = Vec_IntAlloc( 1000 ); - Vec_Int_t * vTypesCur = Vec_IntAlloc( 1000 ); - Vec_Int_t * vFuncsCur = Vec_IntAlloc( 1000 ); - Vec_Int_t * vInstIdsCur = Vec_IntAlloc( 1000 ); - Vec_Int_t * vFaninsCur = Vec_IntAlloc( 1000 ); - Vec_Int_t * vList = Vec_IntAlloc( 1000 ); - Vec_Int_t * vBoxes = Vec_IntStart( Vec_PtrSize((Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4)) ); - - Cba_PrsReadList( p, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1), vInputsCur, -1, -1 ); - Cba_PrsReadList( p, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2), vOutputsCur, -1, -1 ); - Cba_PrsReadNodes( p, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3), vTypesCur, vFuncsCur, vInstIdsCur, vFaninsCur, vList ); - Cba_PrsReadBoxes( p, (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4), vTypesCur, vFuncsCur, vInstIdsCur, vFaninsCur, vList ); - - Cba_ManSetupArray( p, &pNtk->vInputs, vInputsCur ); - Cba_ManSetupArray( p, &pNtk->vOutputs, vOutputsCur ); - Cba_ManSetupArray( p, &pNtk->vTypes, vTypesCur ); - Cba_ManSetupArray( p, &pNtk->vFuncs, vFuncsCur ); - Cba_ManSetupArray( p, &pNtk->vInstIds, vInstIdsCur ); - Cba_ManSetupArray( p, &pNtk->vFanins, vFaninsCur ); - Cba_ManSetupArray( p, &pNtk->vBoxes, vBoxes ); - - Vec_IntFree( vInputsCur ); - Vec_IntFree( vOutputsCur ); - Vec_IntFree( vTypesCur ); - Vec_IntFree( vFuncsCur ); - Vec_IntFree( vInstIdsCur ); - Vec_IntFree( vFaninsCur ); - Vec_IntFree( vList ); - Vec_IntFree( vBoxes ); +void Cba_PrsReadModule( Cba_Man_t * p, Cba_Ntk_t * pNtk, Vec_Ptr_t * vNtk, Vec_Int_t * vList ) +{ + Vec_Ptr_t * vInputs = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 1); + Vec_Ptr_t * vOutputs = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 2); + Vec_Ptr_t * vNodes = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 3); + Vec_Ptr_t * vBoxes = (Vec_Ptr_t *)Vec_PtrEntry(vNtk, 4); + + Cba_ManAllocArray( p, &pNtk->vInputs, Vec_PtrSize(vInputs) ); + Cba_ManAllocArray( p, &pNtk->vOutputs, Vec_PtrSize(vOutputs) ); + Cba_ManAllocArray( p, &pNtk->vTypes, Vec_PtrSize(vNodes) + Vec_PtrSize(vBoxes) ); + Cba_ManAllocArray( p, &pNtk->vFuncs, Vec_PtrSize(vNodes) + Vec_PtrSize(vBoxes) ); + Cba_ManAllocArray( p, &pNtk->vInstIds, Vec_PtrSize(vNodes) + Vec_PtrSize(vBoxes) ); + Cba_ManAllocArray( p, &pNtk->vFanins, Vec_PtrSize(vNodes) + Vec_PtrSize(vBoxes) ); + Cba_ManAllocArray( p, &pNtk->vBoxes, Vec_PtrSize(vBoxes) ); + + Cba_PrsReadList( p, vInputs, &pNtk->vInputs, -1, -1 ); + Cba_PrsReadList( p, vOutputs, &pNtk->vOutputs, -1, -1 ); + Cba_PrsReadNodes( p, vNodes, &pNtk->vTypes, &pNtk->vFuncs, &pNtk->vInstIds, &pNtk->vFanins, vList ); + Cba_PrsReadBoxes( p, vBoxes, &pNtk->vTypes, &pNtk->vFuncs, &pNtk->vInstIds, &pNtk->vFanins, vList ); } Cba_Man_t * Cba_PrsReadPtr( Vec_Ptr_t * vDes ) { Vec_Ptr_t * vNtk; int i; - Cba_Man_t * p = Cba_ManAlloc( (char *)Vec_PtrEntry(vDes, 0) ); + Vec_Int_t * vList = Vec_IntAlloc( 100 ); + Cba_Man_t * p = Cba_ManAlloc( NULL, (char *)Vec_PtrEntry(vDes, 0) ); Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 ) Cba_NtkAlloc( p, (char *)Vec_PtrEntry(vNtk, 0) ); Vec_PtrForEachEntryStart( Vec_Ptr_t *, vDes, vNtk, i, 1 ) - Cba_PrsReadModule( p, Cba_ManNtk(p, i), vNtk ); + Cba_PrsReadModule( p, Cba_ManNtk(p, i), vNtk, vList ); + Vec_IntFree( vList ); return p; } diff --git a/src/base/cba/cbaWriteBlif.c b/src/base/cba/cbaWriteBlif.c index 01749754..656ae8c0 100644 --- a/src/base/cba/cbaWriteBlif.c +++ b/src/base/cba/cbaWriteBlif.c @@ -114,7 +114,7 @@ void Cba_PrsWriteBlif( char * pFileName, Cba_Man_t * p ) printf( "Cannot open output file \"%s\".\n", pFileName ); return; } - fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", Cba_ManName(p), Extra_TimeStamp() ); + fprintf( pFile, "# Design \"%s\" written by ABC on %s\n\n", Cba_ManName(p), Extra_TimeStamp() ); Cba_ManForEachNtk( p, pNtk, i ) Cba_PrsWriteBlifNtk( pFile, pNtk ); fclose( pFile ); @@ -207,7 +207,8 @@ void Cba_ManWriteBlif( char * pFileName, Cba_Man_t * p ) printf( "Cannot open output file \"%s\".\n", pFileName ); return; } - fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", Cba_ManName(p), Extra_TimeStamp() ); + fprintf( pFile, "# Design \"%s\" written by ABC on %s\n\n", Cba_ManName(p), Extra_TimeStamp() ); + Cba_ManAssignInternNames( p ); Cba_ManForEachNtk( p, pNtk, i ) Cba_ManWriteBlifNtk( pFile, pNtk ); fclose( pFile ); diff --git a/src/base/cba/cbaWriteVer.c b/src/base/cba/cbaWriteVer.c index 8e72ee9a..d928da4b 100644 --- a/src/base/cba/cbaWriteVer.c +++ b/src/base/cba/cbaWriteVer.c @@ -120,7 +120,7 @@ void Cba_PrsWriteVerilogBoxes( FILE * pFile, Cba_Ntk_t * p ) Cba_NtkForEachObjType( p, Type, i ) if ( Type == CBA_OBJ_BOX ) // .subckt/.gate/box (formal/actual binding) { - fprintf( pFile, " %s %s (", Cba_ObjFuncStr(p, i), Cba_ObjInstStr(p, i) ); + fprintf( pFile, " %s %s (", Cba_NtkName(Cba_ObjBoxModel(p, i)), Cba_ObjInstStr(p, i) ); Cba_PrsWriteVerilogArray3( pFile, p, Cba_ObjFaninVec(p, i) ); fprintf( pFile, ");\n" ); } @@ -186,6 +186,61 @@ void Cba_PrsWriteVerilog( char * pFileName, Cba_Man_t * p ) /**Function************************************************************* + Synopsis [Collect all nodes names used that are not inputs/outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Cba_NtkCollectWires( Cba_Ntk_t * p, Vec_Int_t * vMap ) +{ + Vec_Int_t * vWires = &p->vWires; + int i, iObj, iFanin, Type, NameId; + Vec_IntClear( vWires ); + Cba_NtkForEachPi( p, iObj, i ) + Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 1 ); + Cba_NtkForEachPo( p, iObj, i ) + Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 1 ); + Cba_NtkForEachObjType( p, Type, iObj ) + { + if ( Type == CBA_OBJ_NODE ) + { + Vec_Int_t * vFanins = Cba_ObjFaninVec( p, iObj ); + Vec_IntForEachEntry( vFanins, iFanin, i ) + { + NameId = Cba_ObjNameId( p, iFanin ); + if ( Vec_IntEntry(vMap, NameId) == 0 ) + { + Vec_IntWriteEntry( vMap, NameId, 1 ); + Vec_IntPush( vWires, NameId ); + } + } + } + else if ( Cba_ObjIsPo(p, iObj) || Cba_ObjIsBi(p, iObj) ) + { + iFanin = Cba_ObjFanin0( p, iObj ); + NameId = Cba_ObjNameId( p, iFanin ); + if ( Vec_IntEntry(vMap, NameId) == 0 ) + { + Vec_IntWriteEntry( vMap, NameId, 1 ); + Vec_IntPush( vWires, NameId ); + } + } + } + Cba_NtkForEachPi( p, iObj, i ) + Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 0 ); + Cba_NtkForEachPo( p, iObj, i ) + Vec_IntWriteEntry( vMap, Cba_ObjNameId(p, iObj), 0 ); + Vec_IntForEachEntry( vWires, NameId, i ) + Vec_IntWriteEntry( vMap, NameId, 0 ); + return vWires; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -195,6 +250,129 @@ void Cba_PrsWriteVerilog( char * pFileName, Cba_Man_t * p ) SeeAlso [] ***********************************************************************/ +void Cba_ManWriteVerilogArray2( FILE * pFile, Cba_Ntk_t * p, int iObj, Vec_Int_t * vFanins ) +{ + int i, iFanin; + fprintf( pFile, "%s%s", Cba_ObjNameStr(p, iObj), (Vec_IntSize(vFanins) == 0) ? "" : ", " ); + Vec_IntForEachEntry( vFanins, iFanin, i ) + fprintf( pFile, "%s%s", Cba_ObjNameStr(p, iFanin), (i == Vec_IntSize(vFanins) - 1) ? "" : ", " ); +} +void Cba_ManWriteVerilogNodes( FILE * pFile, Cba_Ntk_t * p ) +{ + int Type, Func, i; + Cba_NtkForEachObjType( p, Type, i ) + if ( Type == CBA_OBJ_NODE ) // .names/assign/box2 (no formal/actual binding) + { + Func = Cba_ObjFuncId(p, i); + if ( Func >= CBA_NODE_BUF && Func <= CBA_NODE_XNOR ) + { + fprintf( pFile, " %s (", Ptr_TypeToName(Func) ); + Cba_ManWriteVerilogArray2( pFile, p, i, Cba_ObjFaninVec(p, i) ); + fprintf( pFile, ");\n" ); + } +// else if ( Func == CBA_NODE_MUX ) +// Cba_PrsWriteVerilogMux( pFile, p, Cba_ObjFaninVec(p, i) ); + else + { + //char * pName = Cba_NtkStr(p, Func); + assert( 0 ); + } + } +} +void Cba_ManWriteVerilogBoxes( FILE * pFile, Cba_Ntk_t * p ) +{ + int i, k, iTerm, Type; + Cba_NtkForEachObjType( p, Type, i ) + if ( Type == CBA_OBJ_BOX ) // .subckt/.gate/box (formal/actual binding) + { + Cba_Ntk_t * pModel = Cba_ObjBoxModel( p, i ); + fprintf( pFile, " %s %s (", Cba_NtkName(pModel), Vec_IntSize(&p->vInstIds) ? Cba_ObjInstStr(p, i) : "" ); + Cba_NtkForEachPi( pModel, iTerm, k ) + fprintf( pFile, " %s=%s", Cba_ObjNameStr(pModel, iTerm), Cba_ObjNameStr(p, Cba_ObjBoxBi(p, i, k)) ); + Cba_NtkForEachPo( pModel, iTerm, k ) + fprintf( pFile, " %s=%s", Cba_ObjNameStr(pModel, iTerm), Cba_ObjNameStr(p, Cba_ObjBoxBo(p, i, k)) ); + fprintf( pFile, "\n" ); + } +} +void Cba_ManWriteVerilogSignals( FILE * pFile, Cba_Ntk_t * p, int SigType, int fNoRange ) +{ + int NameId, RangeId, i; + char * pSigNames[4] = { "inout", "input", "output", "wire" }; + Vec_Int_t * vSigs[4] = { &p->vInouts, &p->vInputs, &p->vOutputs, &p->vWires }; + if ( fNoRange ) + { + Vec_IntForEachEntry( vSigs[SigType], NameId, i ) + fprintf( pFile, " %s %s;\n", pSigNames[SigType], SigType==3 ? Cba_NtkStr(p, NameId) : Cba_ObjNameStr(p, NameId) ); + } + else + { + Vec_IntForEachEntryDouble( vSigs[SigType], NameId, RangeId, i ) + fprintf( pFile, " %s %s%s;\n", pSigNames[SigType], RangeId ? Cba_NtkStr(p, RangeId) : "", SigType==3 ? Cba_NtkStr(p, NameId) : Cba_ObjNameStr(p, NameId) ); + } +} +void Cba_ManWriteVerilogSignalList( FILE * pFile, Cba_Ntk_t * p, int SigType, int fSkipComma, int fNoRange ) +{ + int NameId, RangeId, i; + Vec_Int_t * vSigs[4] = { &p->vInouts, &p->vInputs, &p->vOutputs, &p->vWires }; + if ( fNoRange ) + { + Vec_IntForEachEntry( vSigs[SigType], NameId, i ) + fprintf( pFile, "%s%s", Cba_ObjNameStr(p, NameId), (fSkipComma && i == Vec_IntSize(vSigs[SigType]) - 1) ? "" : ", " ); + } + else + { + Vec_IntForEachEntryDouble( vSigs[SigType], NameId, RangeId, i ) + fprintf( pFile, "%s%s", Cba_ObjNameStr(p, NameId), (fSkipComma && i == Vec_IntSize(vSigs[SigType]) - 2) ? "" : ", " ); + } +} +void Cba_ManWriteVerilogNtk( FILE * pFile, Cba_Ntk_t * p, Vec_Int_t * vMap ) +{ + int s; + assert( Vec_IntSize(&p->vTypes) == Cba_NtkObjNum(p) ); + assert( Vec_IntSize(&p->vFuncs) == Cba_NtkObjNum(p) ); + // collect wires + Cba_NtkCollectWires( p, vMap ); + // write header + fprintf( pFile, "module %s (\n", Cba_NtkName(p) ); + for ( s = 0; s < 3; s++ ) + { + if ( s == 0 && Vec_IntSize(&p->vInouts) == 0 ) + continue; + fprintf( pFile, " " ); + Cba_ManWriteVerilogSignalList( pFile, p, s, s==2, 1 ); + fprintf( pFile, "\n" ); + } + fprintf( pFile, " );\n" ); + // write declarations + for ( s = 0; s < 4; s++ ) + Cba_ManWriteVerilogSignals( pFile, p, s, 1 ); + fprintf( pFile, "\n" ); + // write objects + Cba_ManWriteVerilogNodes( pFile, p ); + Cba_ManWriteVerilogBoxes( pFile, p ); + fprintf( pFile, "endmodule\n\n" ); + Vec_IntErase( &p->vWires ); +} +void Cba_ManWriteVerilog( char * pFileName, Cba_Man_t * p ) +{ + FILE * pFile; + Cba_Ntk_t * pNtk; + Vec_Int_t * vMap; + int i; + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open output file \"%s\".\n", pFileName ); + return; + } + fprintf( pFile, "// Design \"%s\" written by ABC on %s\n\n", Cba_ManName(p), Extra_TimeStamp() ); + Cba_ManAssignInternNames( p ); + vMap = Vec_IntStart( Abc_NamObjNumMax(p->pNames) + 1 ); + Cba_ManForEachNtk( p, pNtk, i ) + Cba_ManWriteVerilogNtk( pFile, pNtk, vMap ); + Vec_IntFree( vMap ); + fclose( pFile ); +} //////////////////////////////////////////////////////////////////////// |