diff --git a/.github/workflows/build-posix-cmake.yml b/.github/workflows/build-posix-cmake.yml index 5e101cd79..50f9ef902 100644 --- a/.github/workflows/build-posix-cmake.yml +++ b/.github/workflows/build-posix-cmake.yml @@ -6,10 +6,10 @@ on: jobs: - build-posix: + build-posix-cmake: strategy: matrix: - os: [macos-11, ubuntu-latest] + os: [macos-latest, ubuntu-latest] use_namespace: [false, true] runs-on: ${{ matrix.os }} @@ -22,7 +22,7 @@ jobs: steps: - name: Git Checkout - uses: actions/checkout@v2 + uses: actions/checkout@v4 with: submodules: recursive @@ -44,6 +44,10 @@ jobs: run: | cmake --build build + - name: Run Unit Tests + run: | + ctest --output-on-failure + - name: Test Executable run: | ./build/abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec" @@ -60,7 +64,7 @@ jobs: cp build/abc build/libabc.a staging/ - name: Upload pacakge artifact - uses: actions/upload-artifact@v1 + uses: actions/upload-artifact@v4 with: - name: package + name: package-cmake-${{ matrix.os }}-${{ matrix.use_namespace }} path: staging/ diff --git a/.github/workflows/build-posix.yml b/.github/workflows/build-posix.yml index e26b67b89..080c6e045 100644 --- a/.github/workflows/build-posix.yml +++ b/.github/workflows/build-posix.yml @@ -22,7 +22,7 @@ jobs: steps: - name: Git Checkout - uses: actions/checkout@v2 + uses: actions/checkout@v4 with: submodules: recursive @@ -60,7 +60,7 @@ jobs: cp abc libabc.a staging/ - name: Upload pacakge artifact - uses: actions/upload-artifact@v1 + uses: actions/upload-artifact@v4 with: - name: package + name: package-posix-${{ matrix.os }}-${{ matrix.use_namespace }} path: staging/ diff --git a/.github/workflows/build-windows.yml b/.github/workflows/build-windows.yml index 8e1ac37df..2d0894364 100644 --- a/.github/workflows/build-windows.yml +++ b/.github/workflows/build-windows.yml @@ -13,7 +13,7 @@ jobs: steps: - name: Git Checkout - uses: actions/checkout@v2 + uses: actions/checkout@v4 with: submodules: recursive @@ -46,7 +46,7 @@ jobs: copy UpgradeLog.htm staging/ - name: Upload pacakge artifact - uses: actions/upload-artifact@v1 + uses: actions/upload-artifact@v4 with: - name: package + name: package-windows path: staging/ diff --git a/.gitignore b/.gitignore index cbb424152..cdf34f18d 100644 --- a/.gitignore +++ b/.gitignore @@ -13,6 +13,7 @@ lib/m114* lib/bip* docs/ .vscode/ +.cache/ src/ext* src/xxx/ diff --git a/CMakeLists.txt b/CMakeLists.txt index ce541b994..05e6001f9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -112,3 +112,17 @@ add_library(libabc-pic EXCLUDE_FROM_ALL ${ABC_SRC}) abc_properties(libabc-pic PUBLIC) set_property(TARGET libabc-pic PROPERTY POSITION_INDEPENDENT_CODE ON) set_property(TARGET libabc-pic PROPERTY OUTPUT_NAME abc-pic) + +if(NOT DEFINED ABC_SKIP_TESTS) + enable_testing() + include(FetchContent) + FetchContent_Declare( + googletest + DOWNLOAD_EXTRACT_TIMESTAMP TRUE + # Specify the commit you depend on and update it regularly. + URL "https://github.com/google/googletest/archive/refs/tags/v1.14.0.zip" + ) + FetchContent_MakeAvailable(googletest) + include(GoogleTest) + add_subdirectory(test) +endif() \ No newline at end of file diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 79b8b3f08..bb9e7ad7a 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -554,9 +554,11 @@ static inline int Gia_ObjFaninIdp( Gia_Man_t * p, Gia_Obj_t * pObj, int static inline int Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId ) { return Abc_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); } static inline int Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId ) { return Abc_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); } static inline int Gia_ObjFaninLit2( Gia_Man_t * p, int ObjId ) { return (p->pMuxes && p->pMuxes[ObjId]) ? p->pMuxes[ObjId] : -1; } +static inline int Gia_ObjFaninLit( Gia_Obj_t * pObj, int ObjId, int n ){ return n ? Gia_ObjFaninLit1(pObj, ObjId) : Gia_ObjFaninLit0(pObj, ObjId);} static inline int Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) ); } static inline int Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) ); } static inline int Gia_ObjFaninLit2p( Gia_Man_t * p, Gia_Obj_t * pObj) { return (p->pMuxes && p->pMuxes[Gia_ObjId(p, pObj)]) ? p->pMuxes[Gia_ObjId(p, pObj)] : -1; } +static inline int Gia_ObjFaninLitp( Gia_Man_t * p, Gia_Obj_t * pObj, int n ){ return n ? Gia_ObjFaninLit1p(p, pObj) : Gia_ObjFaninLit0p(p, pObj);} static inline void Gia_ObjFlipFaninC0( Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1; } static inline int Gia_ObjFaninNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { if ( Gia_ObjIsMux(p, pObj) ) return 3; if ( Gia_ObjIsAnd(pObj) ) return 2; if ( Gia_ObjIsCo(pObj) ) return 1; return 0; } static inline int Gia_ObjWhatFanin( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) { if ( Gia_ObjFanin0(pObj) == pFanin ) return 0; if ( Gia_ObjFanin1(pObj) == pFanin ) return 1; if ( Gia_ObjFanin2(p, pObj) == pFanin ) return 2; assert(0); return -1; } @@ -1729,6 +1731,7 @@ extern word Gia_ManRandomW( int fReset ); extern void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop ); extern char * Gia_TimeStamp(); extern char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix ); +extern Vec_Ptr_t * Gia_GetFakeNames( int nNames, int fCaps ); extern void Gia_ManIncrementTravId( Gia_Man_t * p ); extern void Gia_ManCleanMark01( Gia_Man_t * p ); extern void Gia_ManSetMark0( Gia_Man_t * p ); @@ -1755,6 +1758,7 @@ extern Vec_Int_t * Gia_ManReverseLevel( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManRequiredLevel( Gia_Man_t * p ); extern void Gia_ManCreateValueRefs( Gia_Man_t * p ); extern void Gia_ManCreateRefs( Gia_Man_t * p ); +extern void Gia_ManCreateLitRefs( Gia_Man_t * p ); extern int * Gia_ManCreateMuxRefs( Gia_Man_t * p ); extern int Gia_ManCrossCut( Gia_Man_t * p, int fReverse ); extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p ); diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index de94c4602..9c6ca8992 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -1464,6 +1464,18 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in Vec_StrFree( vStrExt ); if ( fVerbose ) printf( "Finished writing extension \"m\".\n" ); } + // write cell mapping + if ( Gia_ManHasCellMapping(p) ) + { + extern Vec_Str_t * Gia_AigerWriteCellMappingDoc( Gia_Man_t * p ); + fprintf( pFile, "M" ); + vStrExt = Gia_AigerWriteCellMappingDoc( p ); + Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); + fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); + Vec_StrFree( vStrExt ); + if ( fVerbose ) printf( "Finished writing extension \"M\".\n" ); + + } // write placement if ( p->pPlacement ) { diff --git a/src/aig/gia/giaAigerExt.c b/src/aig/gia/giaAigerExt.c index 50c3588d9..d149b0a5e 100644 --- a/src/aig/gia/giaAigerExt.c +++ b/src/aig/gia/giaAigerExt.c @@ -19,6 +19,9 @@ ***********************************************************************/ #include "gia.h" +#include "misc/st/st.h" +#include "map/mio/mio.h" +#include "map/mio/mioInt.h" ABC_NAMESPACE_IMPL_START @@ -288,6 +291,101 @@ Vec_Str_t * Gia_AigerWriteMappingDoc( Gia_Man_t * p ) return Vec_StrAllocArray( (char *)pBuffer, 4*nSize ); } +int Gia_AigerWriteCellMappingInstance( Gia_Man_t * p, unsigned char * pBuffer, int nSize2, int i ) +{ + int k, iFan; + if ( !Gia_ObjIsCellInv(p, i) ) { + Gia_AigerWriteInt( pBuffer + nSize2, Gia_ObjCellId(p, i) ); nSize2 += 4; + Gia_AigerWriteInt( pBuffer + nSize2, i ); nSize2 += 4; + Gia_CellForEachFanin( p, i, iFan, k ) + { + Gia_AigerWriteInt( pBuffer + nSize2, iFan ); + nSize2 += 4; + } + } else { + Gia_AigerWriteInt( pBuffer + nSize2, 3 ); nSize2 += 4; + Gia_AigerWriteInt( pBuffer + nSize2, i ); nSize2 += 4; + Gia_AigerWriteInt( pBuffer + nSize2, Abc_LitNot(i) ); nSize2 += 4; + } + + return nSize2; +} + +Vec_Str_t * Gia_AigerWriteCellMappingDoc( Gia_Man_t * p ) +{ + unsigned char * pBuffer; + int i, iFan, nCells = 0, nInstances = 0, nSize = 8, nSize2 = 0; + Mio_Cell2_t * pCells = Mio_CollectRootsNewDefault2( 6, &nCells, 0 ); + assert( pCells ); + + for (int i = 0; i < nCells; i++) + { + Mio_Gate_t *pGate = (Mio_Gate_t *) pCells[i].pMioGate; + Mio_Pin_t *pPin; + nSize += strlen(Mio_GateReadName(pGate)) + 1; + nSize += strlen(Mio_GateReadOutName(pGate)) + 1 + 4; + Mio_GateForEachPin( pGate, pPin ) + nSize += strlen(Mio_PinReadName(pPin)) + 1; + } + + Gia_ManForEachCell( p, i ) + { + assert ( !Gia_ObjIsCellBuf(p, i) ); // not implemented + nInstances++; + if ( Gia_ObjIsCellInv(p, i) ) + nSize += 12; + else + nSize += Gia_ObjCellSize(p, i) * 4 + 8; + } + + pBuffer = ABC_ALLOC( unsigned char, nSize ); + Gia_AigerWriteInt( pBuffer + nSize2, nCells ); nSize2 += 4; + Gia_AigerWriteInt( pBuffer + nSize2, nInstances ); nSize2 += 4; + + for (int i = 0; i < nCells; i++) + { + int nPins = 0; + Mio_Gate_t *pGate = (Mio_Gate_t *) pCells[i].pMioGate; + Mio_Pin_t *pPin; + + strcpy((char *) pBuffer + nSize2, Mio_GateReadName(pGate)); + nSize2 += strlen(Mio_GateReadName(pGate)) + 1; + strcpy((char *) pBuffer + nSize2, Mio_GateReadOutName(pGate)); + nSize2 += strlen(Mio_GateReadOutName(pGate)) + 1; + + Mio_GateForEachPin( pGate, pPin ) + nPins++; + Gia_AigerWriteInt( pBuffer + nSize2, nPins ); nSize2 += 4; + + Mio_GateForEachPin( pGate, pPin ) + { + strcpy((char *) pBuffer + nSize2, Mio_PinReadName(pPin)); + nSize2 += strlen(Mio_PinReadName(pPin)) + 1; + } + } + + Gia_ManForEachCell( p, i ) + { + if ( Gia_ObjIsCellBuf(p, i) ) + continue; + + if ( Gia_ObjIsCellInv(p, i) && !Abc_LitIsCompl(i) ) { + // swap the order so that the inverter is after the driver + // of the inverter's input + nSize2 = Gia_AigerWriteCellMappingInstance(p, pBuffer, nSize2, Abc_LitNot(i) ); + nSize2 = Gia_AigerWriteCellMappingInstance(p, pBuffer, nSize2, i ); + i += 1; + continue; + } + + nSize2 = Gia_AigerWriteCellMappingInstance(p, pBuffer, nSize2, i ); + } + + assert( nSize2 == nSize ); + ABC_FREE( pCells ); + return Vec_StrAllocArray( (char *)pBuffer, nSize ); +} + /**Function************************************************************* Synopsis [Read/write packing information.] diff --git a/src/aig/gia/giaClp.c b/src/aig/gia/giaClp.c index 873cea2eb..dba81637e 100644 --- a/src/aig/gia/giaClp.c +++ b/src/aig/gia/giaClp.c @@ -42,42 +42,6 @@ extern int Gia_ManFactorNode( Gia_Man_t * p, char * pSop, Vec_Int_t * vLeaves ); /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Gia_GetFakeNames( int nNames ) -{ - Vec_Ptr_t * vNames; - char Buffer[5]; - int i; - - vNames = Vec_PtrAlloc( nNames ); - for ( i = 0; i < nNames; i++ ) - { - if ( nNames < 26 ) - { - Buffer[0] = 'a' + i; - Buffer[1] = 0; - } - else - { - Buffer[0] = 'a' + i%26; - Buffer[1] = '0' + i/26; - Buffer[2] = 0; - } - Vec_PtrPush( vNames, Extra_UtilStrsav(Buffer) ); - } - return vNames; -} - /**Function************************************************************* Synopsis [] @@ -378,8 +342,8 @@ Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose ) Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) ); if ( fVerbose ) { - Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) ); - Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) ); + Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p), 0 ); + Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p), 1 ); char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi ); char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo ); Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, 0 ); @@ -404,6 +368,41 @@ void Gia_ManCollapseTestTest( Gia_Man_t * p ) Gia_ManStop( pNew ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintDsdOne( Dsd_Manager_t * pManDsd, int Output, int OffSet ) +{ + Vec_Str_t * vStr = Vec_StrAlloc( 100 ); + Dsd_TreePrint4( vStr, pManDsd, Output ); + for ( int i = 0; i < OffSet; i++ ) + printf( " " ); + printf( "Supp %2d nDsd %2d %s\n", Dsd_TreeSuppSize(pManDsd, Output), Dsd_TreeNonDsdMax(pManDsd, Output), Vec_StrArray(vStr) ); + Vec_StrFree( vStr ); + fflush( stdout ); +} +void Gia_ManPrintDsd( Dsd_Manager_t * pManDsd, int Output, int nOutputs, int OffSet ) +{ + if ( Output == -1 ) + { + for ( int i = 0; i < nOutputs; i++ ) + Gia_ManPrintDsdOne( pManDsd, i, OffSet ); + } + else + { + assert( Output >= 0 && Output < nOutputs ); + Gia_ManPrintDsdOne( pManDsd, Output, OffSet ); + } +} + void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose ) { DdManager * dd; @@ -425,22 +424,89 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose ) Cudd_Quit( dd ); return; } - Dsd_Decompose( pManDsd, (DdNode **)vFuncs->pArray, Gia_ManCoNum(p) ); + Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) ); + if ( fVerbose ) { - Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) ); - Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) ); + Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p), 0 ); + Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p), 1 ); char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi ); char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo ); Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, OffSet ); Vec_PtrFreeFree( vNamesCi ); Vec_PtrFreeFree( vNamesCo ); } + else + Gia_ManPrintDsd( pManDsd, 0, Vec_PtrSize(vFuncs), 0 ); + Dsd_ManagerStop( pManDsd ); Gia_ManCollapseDeref( dd, vFuncs ); Extra_StopManager( dd ); } +Vec_Ptr_t * Gia_ManRecurDsdCof( DdManager * dd, Vec_Ptr_t * vFuncs, int iVar ) +{ + Vec_Ptr_t * vNew = Vec_PtrAlloc( 2 * Vec_PtrSize(vFuncs) ); DdNode * bFunc; int i; + Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i ) { + DdNode * bCof0 = Cudd_Cofactor( dd, bFunc, Cudd_Not(Cudd_bddIthVar(dd, iVar)) ); Cudd_Ref( bCof0 ); + DdNode * bCof1 = Cudd_Cofactor( dd, bFunc, Cudd_bddIthVar(dd, iVar) ); Cudd_Ref( bCof1 ); + Vec_PtrPush( vNew, bCof0 ); + Vec_PtrPush( vNew, bCof1 ); + } + return vNew; +} +void Gia_ManRecurDsd( Gia_Man_t * p, int fVerbose ) +{ + DdManager * dd; + Dsd_Manager_t * pManDsd; + Vec_Ptr_t * vFuncs, * vAux; + dd = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + vFuncs = Gia_ManCollapse( p, dd, 10000, 0 ); + Cudd_AutodynDisable( dd ); + if ( vFuncs == NULL ) + { + Extra_StopManager( dd ); + return; + } + pManDsd = Dsd_ManagerStart( dd, Gia_ManCiNum(p), 0 ); + if ( pManDsd == NULL ) + { + Gia_ManCollapseDeref( dd, vFuncs ); + Cudd_Quit( dd ); + return; + } + Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) ); + + printf( "Function:\n" ); + Gia_ManPrintDsd( pManDsd, 0, Vec_PtrSize(vFuncs), 0 ); + + for ( int i = 0; i < 5 && Dsd_TreeNonDsdMax(pManDsd, -1) > 0; i++ ) + { + int v, iBestV = -1, DsdMin = ABC_INFINITY, SuppMin = ABC_INFINITY; + for ( v = 0; v < Gia_ManCiNum(p); v++ ) + { + Vec_Ptr_t * vTemp = Gia_ManRecurDsdCof( dd, vFuncs, v ); + Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vTemp), Vec_PtrSize(vTemp) ); + int DsdCur = Dsd_TreeNonDsdMax( pManDsd, -1 ); + int SuppCur = Dsd_TreeSuppSize( pManDsd, -1 ); + if ( DsdMin > DsdCur || (DsdMin == DsdCur && SuppMin > SuppCur) ) + DsdMin = DsdCur, SuppMin = SuppCur, iBestV = v; + Gia_ManCollapseDeref( dd, vTemp ); + } + assert( iBestV >= 0 ); + vFuncs = Gia_ManRecurDsdCof( dd, vAux = vFuncs, iBestV ); + Gia_ManCollapseDeref( dd, vAux ); + printf( "Cofactoring variable %c:\n", (int)(iBestV >= 26 ? 'A' - 26 : 'a') + iBestV ); + Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) ); + Gia_ManPrintDsd( pManDsd, -1, Vec_PtrSize(vFuncs), (i+1)*2 ); + } + + Dsd_ManagerStop( pManDsd ); + Gia_ManCollapseDeref( dd, vFuncs ); + Extra_StopManager( dd ); +} + #else Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose ) @@ -452,6 +518,10 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose ) { } +void Gia_ManRecurDsd( Gia_Man_t * p, int fVerbose ) +{ +} + #endif //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaCut.c b/src/aig/gia/giaCut.c index 47dc5ec7b..19d98c3be 100644 --- a/src/aig/gia/giaCut.c +++ b/src/aig/gia/giaCut.c @@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// #define GIA_MAX_CUTSIZE 8 -#define GIA_MAX_CUTNUM 65 +#define GIA_MAX_CUTNUM 257 #define GIA_MAX_TT_WORDS ((GIA_MAX_CUTSIZE > 6) ? 1 << (GIA_MAX_CUTSIZE-6) : 1) #define GIA_CUT_NO_LEAF 0xF @@ -45,6 +45,7 @@ struct Gia_Cut_t_ unsigned nTreeLeaves : 28; // tree leaves unsigned nLeaves : 4; // leaf count int pLeaves[GIA_MAX_CUTSIZE]; // leaves + float CostF; }; typedef struct Gia_Sto_t_ Gia_Sto_t; @@ -281,7 +282,7 @@ static inline int Gia_CutSetLastCutIsContained( Gia_Cut_t ** pCuts, int nCuts ) SeeAlso [] ***********************************************************************/ -static inline int Gia_CutCompare( Gia_Cut_t * pCut0, Gia_Cut_t * pCut1 ) +static inline int Gia_CutCompare2( Gia_Cut_t * pCut0, Gia_Cut_t * pCut1 ) { if ( pCut0->nTreeLeaves < pCut1->nTreeLeaves ) return -1; if ( pCut0->nTreeLeaves > pCut1->nTreeLeaves ) return 1; @@ -289,6 +290,14 @@ static inline int Gia_CutCompare( Gia_Cut_t * pCut0, Gia_Cut_t * pCut1 ) if ( pCut0->nLeaves > pCut1->nLeaves ) return 1; return 0; } +static inline int Gia_CutCompare( Gia_Cut_t * pCut0, Gia_Cut_t * pCut1 ) +{ + if ( pCut0->CostF > pCut1->CostF ) return -1; + if ( pCut0->CostF < pCut1->CostF ) return 1; + if ( pCut0->nLeaves < pCut1->nLeaves ) return -1; + if ( pCut0->nLeaves > pCut1->nLeaves ) return 1; + return 0; +} static inline int Gia_CutSetLastCutContains( Gia_Cut_t ** pCuts, int nCuts ) { int i, k, fChanges = 0; @@ -432,6 +441,13 @@ static inline int Gia_CutTreeLeaves( Gia_Sto_t * p, Gia_Cut_t * pCut ) Cost += Vec_IntEntry( p->vRefs, pCut->pLeaves[i] ) == 1; return Cost; } +static inline float Gia_CutGetCost( Gia_Sto_t * p, Gia_Cut_t * pCut ) +{ + int i, Cost = 0; + for ( i = 0; i < (int)pCut->nLeaves; i++ ) + Cost += Vec_IntEntry( p->vRefs, pCut->pLeaves[i] ); + return (float)Cost / Abc_MaxInt(1, pCut->nLeaves); +} static inline int Gia_StoPrepareSet( Gia_Sto_t * p, int iObj, int Index ) { Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj ); @@ -445,6 +461,7 @@ static inline int Gia_StoPrepareSet( Gia_Sto_t * p, int iObj, int Index ) pCutTemp->iFunc = pCut[pCut[0]+1]; pCutTemp->Sign = Gia_CutGetSign( pCutTemp ); pCutTemp->nTreeLeaves = Gia_CutTreeLeaves( p, pCutTemp ); + pCutTemp->CostF = Gia_CutGetCost( p, pCutTemp ); } return pList[0]; } @@ -512,6 +529,7 @@ void Gia_StoMergeCuts( Gia_Sto_t * p, int iObj ) if ( p->fCutMin && Gia_CutComputeTruth(p, pCut0, pCut1, fComp0, fComp1, pCutsR[nCutsR], fIsXor) ) pCutsR[nCutsR]->Sign = Gia_CutGetSign(pCutsR[nCutsR]); pCutsR[nCutsR]->nTreeLeaves = Gia_CutTreeLeaves( p, pCutsR[nCutsR] ); + pCutsR[nCutsR]->CostF = Gia_CutGetCost( p, pCutsR[nCutsR] ); nCutsR = Gia_CutSetAddCut( pCutsR, nCutsR, nCutNum ); } p->CutCount[3] += nCutsR; @@ -1048,8 +1066,9 @@ Gia_Sto_t * Gia_ManMatchCutsInt( Gia_Man_t * pGia, int nCutSize0, int nCutNum0, void Gia_ManMatchCuts( Vec_Mem_t * vTtMem, Gia_Man_t * pGia, int nCutSize, int nCutNum, int fVerbose ) { Gia_Sto_t * p = Gia_ManMatchCutsInt( pGia, nCutSize, nCutNum, fVerbose ); - Vec_Int_t * vLevel; int i, k, * pCut; + Vec_Int_t * vLevel; int i, j, k, * pCut; Vec_Int_t * vNodes = Vec_IntAlloc( 100 ); + Vec_Wec_t * vCuts = Vec_WecAlloc( 100 ); abctime clkStart = Abc_Clock(); assert( Abc_Truth6WordNum(nCutSize) == Vec_MemEntrySize(vTtMem) ); Vec_WecForEachLevel( p->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) ) @@ -1061,11 +1080,19 @@ void Gia_ManMatchCuts( Vec_Mem_t * vTtMem, Gia_Man_t * pGia, int nCutSize, int n if ( *pSpot == -1 ) continue; Vec_IntPush( vNodes, i ); + vLevel = Vec_WecPushLevel( vCuts ); + Vec_IntPush( vLevel, i ); + for ( j = 1; j <= pCut[0]; j++ ) + Vec_IntPush( vLevel, pCut[j] ); break; } } printf( "Nodes with matching cuts: " ); Vec_IntPrint( vNodes ); + if ( Vec_WecSize(vCuts) > 32 ) + Vec_WecShrink(vCuts, 32); + Vec_WecPrint( vCuts, 0 ); + Vec_WecFree( vCuts ); Vec_IntFree( vNodes ); Gia_StoFree( p ); if ( fVerbose ) @@ -1107,6 +1134,251 @@ Vec_Ptr_t * Gia_ManMatchCutsArray( Vec_Ptr_t * vTtMems, Gia_Man_t * pGia, int nC } return vRes; } +Vec_Ptr_t * Gia_ManMatchCutsMany( Vec_Mem_t * vTtMem, Vec_Int_t * vMap, int nFuncs, Gia_Man_t * pGia, int nCutSize, int nCutNum, int fVerbose ) +{ + Gia_Sto_t * p = Gia_ManMatchCutsInt( pGia, nCutSize, nCutNum, fVerbose ); + Vec_Int_t * vLevel; int i, j, k, * pCut; + abctime clkStart = Abc_Clock(); + assert( Abc_Truth6WordNum(nCutSize) == Vec_MemEntrySize(vTtMem) ); + Vec_Ptr_t * vRes = Vec_PtrAlloc( nFuncs ); + for ( i = 0; i < nFuncs; i++ ) + Vec_PtrPush( vRes, Vec_WecAlloc(10) ); + Vec_WecForEachLevel( p->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) ) + { + Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k ) if ( pCut[0] > 1 ) + { + word * pTruth = Vec_MemReadEntry( p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]) ); + assert( (pTruth[0] & 1) == 0 ); + int * pSpot = Vec_MemHashLookup( vTtMem, pTruth ); + if ( *pSpot == -1 ) + continue; + int iFunc = vMap ? Vec_IntEntry( vMap, *pSpot ) : 0; + assert( iFunc < nFuncs ); + Vec_Wec_t * vCuts = (Vec_Wec_t *)Vec_PtrEntry( vRes, iFunc ); + vLevel = Vec_WecPushLevel( vCuts ); + Vec_IntPush( vLevel, i ); + for ( j = 1; j <= pCut[0]; j++ ) + Vec_IntPush( vLevel, pCut[j] ); + break; + } + } + Gia_StoFree( p ); + if ( fVerbose ) + Abc_PrintTime( 1, "Cut matching time", Abc_Clock() - clkStart ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Function enumeration.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wrd_t * Gia_ManCollectCutFuncs( Gia_Man_t * p, int nCutSize, int nCutNum, int fVerbose ) +{ + Gia_Sto_t * pSto = Gia_ManMatchCutsInt( p, nCutSize, nCutNum, 0 ); + Vec_Wrd_t * vFuncs = Vec_WrdAlloc( 1000 ); Vec_Int_t * vLevel; int i, k, * pCut; + Vec_WecForEachLevel( pSto->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) ) + Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k ) if ( pCut[0] == nCutSize ) { + word * pTruth = Vec_MemReadEntry( pSto->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]) ); + Vec_WrdPush( vFuncs, pTruth[0] ); + } + Gia_StoFree( pSto ); + if ( fVerbose ) + printf( "Collected %d cut functions using the AIG with %d nodes.\n", Vec_WrdSize(vFuncs), Gia_ManAndNum(p) ); + return vFuncs; +} +Vec_Int_t * Gia_ManCountNpnClasses( Vec_Mem_t * vTtMem, Vec_Int_t * vMap, int nClasses, Vec_Wrd_t * vOrig ) +{ + assert( Vec_MemEntryNum(vTtMem) == Vec_IntSize(vMap) ); + Vec_Int_t * vClassCounts = Vec_IntStart( nClasses ); int i; word Func; + Vec_WrdForEachEntry( vOrig, Func, i ) { + int * pSpot = Vec_MemHashLookup( vTtMem, &Func ); + if ( *pSpot == -1 ) + continue; + int iClass = Vec_IntEntry( vMap, *pSpot ); + if ( iClass == -1 ) + continue; + assert( iClass < Vec_IntSize(vClassCounts) ); + Vec_IntAddToEntry( vClassCounts, iClass, 1 ); + } + return vClassCounts; +} +Vec_Wrd_t * Gia_ManMatchFilterClasses( Vec_Mem_t * vTtMem, Vec_Int_t * vMap, Vec_Int_t * vClassCounts, int nNumFuncs, int fVerbose ) +{ + int * pPerm = Abc_MergeSortCost( Vec_IntArray(vClassCounts), Vec_IntSize(vClassCounts) ); + Vec_Wrd_t * vBest = Vec_WrdAlloc( nNumFuncs ); int i, k, Entry; + Vec_Int_t * vMapNew = Vec_IntStartFull( Vec_IntSize(vMap) ); + for ( i = Vec_IntSize(vClassCounts)-1; i >= 0; i-- ) { + word Best = ~(word)0; + Vec_IntForEachEntry( vMap, Entry, k ) { + if ( Entry != pPerm[i] ) + continue; + if ( Best > Vec_MemReadEntry(vTtMem, k)[0] ) + Best = Vec_MemReadEntry(vTtMem, k)[0]; + Vec_IntWriteEntry( vMapNew, k, Vec_WrdSize(vBest) ); + } + Vec_WrdPush( vBest, Best ); + assert( ~Best ); + if ( Vec_WrdSize(vBest) == nNumFuncs ) + break; + } + ABC_SWAP( Vec_Int_t, *vMap, *vMapNew ); + Vec_IntFree( vMapNew ); + ABC_FREE( pPerm ); + if ( fVerbose ) + printf( "Isolated %d (out of %d) most frequently occuring classes.\n", Vec_WrdSize(vBest), Vec_IntSize(vClassCounts) ); + return vBest; +} +void Gia_ManMatchProfileFunctions( Vec_Wrd_t * vBestReprs, Vec_Mem_t * vTtMem, Vec_Int_t * vMap, Vec_Wrd_t * vFuncs, int nCutSize ) +{ + int BarSize = 60; + extern void Dau_DsdPrintFromTruth( word * pTruth, int nVarsInit ); + Vec_Int_t * vCounts = Gia_ManCountNpnClasses( vTtMem, vMap, Vec_WrdSize(vBestReprs), vFuncs ); + word Repr; int c, i, MaxCount = Vec_IntFindMax( vCounts ); + Vec_WrdForEachEntry( vBestReprs, Repr, c ) + { + int nSymb = BarSize*Vec_IntEntry(vCounts, c)/Abc_MaxInt(MaxCount, 1); + printf( "Class%4d : ", c ); + printf( "Count =%6d ", Vec_IntEntry(vCounts, c) ); + for ( i = 0; i < nSymb; i++ ) + printf( "*" ); + for ( i = nSymb; i < BarSize+3; i++ ) + printf( " " ); + Dau_DsdPrintFromTruth( &Repr, nCutSize ); + } + Vec_IntFree( vCounts ); +} +void Gia_ManMatchCones( Gia_Man_t * pBig, Gia_Man_t * pSmall, int nCutSize, int nCutNum, int nNumFuncs, int nNumCones, int fVerbose ) +{ + abctime clkStart = Abc_Clock(); + extern void Dau_CanonicizeArray( Vec_Wrd_t * vFuncs, int nVars, int fVerbose ); + extern Vec_Mem_t * Dau_CollectNpnFunctionsArray( Vec_Wrd_t * vFuncs, int nVars, Vec_Int_t ** pvMap, int fVerbose ); + Vec_Wrd_t * vFuncs = Gia_ManCollectCutFuncs( pSmall, nCutSize, nCutNum, fVerbose ); + Vec_Wrd_t * vOrig = Vec_WrdDup( vFuncs ); + Dau_CanonicizeArray( vFuncs, nCutSize, fVerbose ); + Vec_Int_t * vMap = NULL; int n; + Vec_Mem_t * vTtMem = Dau_CollectNpnFunctionsArray( vFuncs, nCutSize, &vMap, fVerbose ); + Vec_WrdFree( vFuncs ); + Vec_Int_t * vClassCounts = Gia_ManCountNpnClasses( vTtMem, vMap, Vec_IntEntryLast(vMap)+1, vOrig ); + Vec_Wrd_t * vBestReprs = Gia_ManMatchFilterClasses( vTtMem, vMap, vClassCounts, nNumFuncs, fVerbose ); + assert( Vec_WrdSize(vBestReprs) == nNumFuncs ); + Vec_IntFree( vClassCounts ); + printf( "Frequency profile for %d most popular classes in the small AIG:\n", nNumFuncs ); + Gia_ManMatchProfileFunctions( vBestReprs, vTtMem, vMap, vOrig, nCutSize ); + Vec_WrdFree( vOrig ); + Abc_Random( 1 ); + for ( n = 0; n < nNumCones; n++ ) { + int nRand = Abc_Random( 0 ) % Gia_ManCoNum(pBig); + Gia_Man_t * pCone = Gia_ManDupCones( pBig, &nRand, 1, 1 ); + Vec_Wrd_t * vCutFuncs = Gia_ManCollectCutFuncs( pCone, nCutSize, nCutNum, 0 ); + printf( "ITER %d: Considering output cone %d with %d and-nodes. ", n+1, nRand, Gia_ManAndNum(pCone) ); + printf( "Profiling %d functions of %d-cuts:\n", Vec_WrdSize(vCutFuncs), nCutSize ); + Gia_ManMatchProfileFunctions( vBestReprs, vTtMem, vMap, vCutFuncs, nCutSize ); + Vec_WrdFree( vCutFuncs ); + Gia_ManStop( pCone ); + } + Vec_WrdFree( vBestReprs ); + Vec_IntFree( vMap ); + Vec_MemHashFree( vTtMem ); + Vec_MemFree( vTtMem ); + Abc_PrintTime( 1, "Total computation time", Abc_Clock() - clkStart ); +} + +/**Function************************************************************* + + Synopsis [Function enumeration.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManMatchConesMinimizeTts( Vec_Wrd_t * vSims, int nVarsMax ) +{ + int nVars = 0; + int nWordsMax = Abc_Truth6WordNum( nVarsMax ), nWords; + int i, k = 0, nTruths = Vec_WrdSize(vSims) / nWordsMax; + assert( nTruths * nWordsMax == Vec_WrdSize(vSims) ); + // support-minimize and find the largest supp size + for ( i = 0; i < nTruths; i++ ) { + word * pTruth = Vec_WrdEntryP( vSims, i * nWordsMax ); + int nVarsCur = Abc_TtMinBase( pTruth, NULL, nVarsMax, nVarsMax ); + nVars = Abc_MaxInt( nVars, nVarsCur ); + } + // remap truth tables + nWords = Abc_Truth6WordNum( nVars ); + for ( i = 0; i < nTruths; i++ ) { + word * pTruth = Vec_WrdEntryP( vSims, i * nWordsMax ); + word * pTruth2 = Vec_WrdEntryP( vSims, k * nWords ); + if ( Abc_TtSupportSize(pTruth, nVars) < 3 ) + continue; + memmove( pTruth2, pTruth, nWords * sizeof(word) ); + k++; + if ( 0 ) { + extern void Extra_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars ); + printf( "Type%d : ", i ); + Extra_PrintHexadecimal( stdout, (unsigned *)pTruth2, nVars ); + printf( "\n" ); + } + } + Vec_WrdShrink ( vSims, k * nWords ); + return nVars; +} +void Gia_ManMatchConesOutputPrint( Vec_Ptr_t * p, int fVerbose ) +{ + Vec_Wec_t * vCuts; int i; + printf( "Nodes with matching cuts:\n" ); + Vec_PtrForEachEntry( Vec_Wec_t *, p, vCuts, i ) { + if ( fVerbose ) { + printf( "Type %d:\n", i ); + Vec_WecPrint( vCuts, 0 ); + } + else + printf( "Type %d present in %d cuts\n", i, Vec_WecSize(vCuts) ); + } +} +void Gia_ManMatchConesOutputFree( Vec_Ptr_t * p ) +{ + Vec_Wec_t * vCuts; int i; + Vec_PtrForEachEntry( Vec_Wec_t *, p, vCuts, i ) + Vec_WecFree( vCuts ); + Vec_PtrFree( p ); +} +void Gia_ManMatchConesOutput( Gia_Man_t * pBig, Gia_Man_t * pSmall, int nCutNum, int fVerbose ) +{ + abctime clkStart = Abc_Clock(); + extern Vec_Mem_t * Dau_CollectNpnFunctionsArray( Vec_Wrd_t * vFuncs, int nVars, Vec_Int_t ** pvMap, int fVerbose ); + Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(pSmall) ); + Vec_Wrd_t * vSims = Gia_ManSimPatSimOut( pSmall, vSimsPi, 1 ); + int nVars = Gia_ManMatchConesMinimizeTts( vSims, Gia_ManCiNum(pSmall) ); + Vec_WrdFree( vSimsPi ); + if ( nVars > 10 ) { + printf( "Some output functions have support size more than 10.\n" ); + Vec_WrdFree( vSims ); + return; + } + Vec_Int_t * vMap = NULL; + Vec_Mem_t * vTtMem = Dau_CollectNpnFunctionsArray( vSims, nVars, &vMap, fVerbose ); + int nFuncs = Vec_WrdSize(vSims) / Abc_Truth6WordNum(nVars); + assert( Vec_WrdSize(vSims) == nFuncs * Abc_Truth6WordNum(nVars) ); + Vec_WrdFree( vSims ); + printf( "Using %d output functions with the support size between 3 and %d.\n", nFuncs, nVars ); + Vec_Ptr_t * vRes = Gia_ManMatchCutsMany( vTtMem, vMap, nFuncs, pBig, nVars, nCutNum, fVerbose ); + Vec_MemHashFree( vTtMem ); + Vec_MemFree( vTtMem ); + Vec_IntFree( vMap ); + Gia_ManMatchConesOutputPrint( vRes, fVerbose ); + Gia_ManMatchConesOutputFree( vRes ); + Abc_PrintTime( 1, "Total computation time", Abc_Clock() - clkStart ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index aec9d39ca..09def827d 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -2732,6 +2732,54 @@ void Gia_ManTransferTest( Gia_Man_t * p ) Gia_ManStop( pNew ); } +/**Function************************************************************* + + Synopsis [Transfer from new to old.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManTransferEquivs2( Gia_Man_t * p, Gia_Man_t * pOld ) +{ + Gia_Obj_t * pObj; + Vec_Int_t * vClass; + int i, k, iNode, iRepr; + assert( p->pReprs != NULL ); + assert( p->pNexts != NULL ); + assert( pOld->pReprs == NULL ); + assert( pOld->pNexts == NULL ); + // create map + Gia_ManFillValue( p ); + Gia_ManForEachObj( pOld, pObj, i ) + if ( ~pObj->Value ) + Gia_ManObj(p, Abc_Lit2Var(pObj->Value))->Value = Abc_Var2Lit(i, 0); + // start representatives + pOld->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pOld) ); + for ( i = 0; i < Gia_ManObjNum(pOld); i++ ) + Gia_ObjSetRepr( pOld, i, GIA_VOID ); + // iterate over constant candidates + Gia_ManForEachConst( p, i ) + Gia_ObjSetRepr( pOld, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 ); + // iterate over class candidates + vClass = Vec_IntAlloc( 100 ); + Gia_ManForEachClass( p, i ) + { + Vec_IntClear( vClass ); + Gia_ClassForEachObj( p, i, k ) + Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) ); + assert( Vec_IntSize( vClass ) > 1 ); + Vec_IntSort( vClass, 0 ); + iRepr = Vec_IntEntry( vClass, 0 ); + Vec_IntForEachEntryStart( vClass, iNode, k, 1 ) + Gia_ObjSetRepr( pOld, iNode, iRepr ); + } + Vec_IntFree( vClass ); + pOld->pNexts = Gia_ManDeriveNexts( pOld ); +} /**Function************************************************************* diff --git a/src/aig/gia/giaGen.c b/src/aig/gia/giaGen.c index cb56ef64d..03b194e7c 100644 --- a/src/aig/gia/giaGen.c +++ b/src/aig/gia/giaGen.c @@ -924,6 +924,384 @@ void Gia_ManTestWordFile( Gia_Man_t * p, char * pFileName, char * pDumpFile, int Abc_PrintTime( 1, "Total checking time", Abc_Clock() - clk ); } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManSumCount( char * p, Vec_Int_t * vDec, int b ) +{ + int i, Ent, Count = 0, Sum = 0; + for ( i = 0; p[i]; i++ ) { + Ent = (p[i] >= '0' && p[i] <= '9') ? p[i]-'0' : p[i]-'A'+10; + Count += Vec_IntEntry(vDec, Ent) + b * (1 << (Sum += Ent)); + } + return Count + b * ((1 << Sum) - 1); +} +Vec_Str_t * Gia_ManSumEnum_rec( int Num ) +{ + if ( Num == 1 ) { + Vec_Str_t * vRes = Vec_StrAlloc(2); + Vec_StrPush( vRes, '1' ); + Vec_StrPush( vRes, '\0' ); + return vRes; + } + Vec_Str_t * vRes = Vec_StrAlloc( 16 ); + for ( int i = 1; i < Num; i++ ) { + Vec_Str_t * vRes0 = Gia_ManSumEnum_rec(i); + Vec_Str_t * vRes1 = Gia_ManSumEnum_rec(Num-i); + for ( int c0 = 0; c0 < Vec_StrSize(vRes0); c0 += strlen(Vec_StrEntryP(vRes0,c0))+1 ) + for ( int c1 = 0; c1 < Vec_StrSize(vRes1); c1 += strlen(Vec_StrEntryP(vRes1,c1))+1 ) + Vec_StrPrintF( vRes, "%s%s%c", Vec_StrEntryP(vRes0,c0), Vec_StrEntryP(vRes1,c1), '\0' ); + Vec_StrPrintF( vRes, "%c%c", Num < 10 ? '0'+Num : 'A'+Num-10, '\0' ); + Vec_StrFree( vRes0 ); + Vec_StrFree( vRes1 ); + } + return vRes; +} +void Gia_ManSumEnum( int n, Vec_Int_t * vDec ) +{ + Vec_Str_t * vRes = Gia_ManSumEnum_rec( n ); + for ( int b = 1; b <= 256; b <<= 1 ) { + int iBest = -1, CountCur, CountBest = ABC_INFINITY; + for ( int c0 = 0; c0 < Vec_StrSize(vRes); c0 += strlen(Vec_StrEntryP(vRes,c0))+1 ) { + CountCur = Gia_ManSumCount( Vec_StrEntryP(vRes,c0), vDec, b ); + if ( CountBest > CountCur ) + CountBest = CountCur, iBest = c0; + } + printf( " %8d", CountBest ); + //printf( " %8s", Vec_StrEntryP(vRes,iBest) ); + //printf( " %.3f", (float)CountBest/(3*b*((1<> b) & 1 ) + Vec_IntWriteEntry( vLev, b, 1 ); + Vec_WrdForEachEntryStop( vData, Data, i, Vec_WrdSize(vData)-1 ) { + for ( n = 0; n < nIBits; n++, nLits += 2 ) { + Vec_Int_t * vLev = Vec_WecPushLevel( vArgs ); + Vec_IntFill( vLev, nOBits, 0 ); + for ( b = 0; b < nOBits; b++ ) + if ( ((Data >> b) & 1) && b+n < nOBits ) + Vec_IntWriteEntry( vLev, b+n, nLits ); + } + } + return vArgs; +} +Vec_Wec_t * Gia_ManGenNeuronTransformArgs( Gia_Man_t * pNew, Vec_Wec_t * vArgs, int nLutSize, int nOBits ) +{ + int i, nParts = (Vec_WecSize(vArgs) + nLutSize - 2) / nLutSize; + while ( Vec_WecSize(vArgs) < nLutSize*nParts+1 ) + Vec_IntFill( Vec_WecPushLevel(vArgs), nOBits, 0 ); + assert( Vec_WecSize(vArgs) == nLutSize*nParts+1 ); + Vec_Wec_t * vNew = Vec_WecAlloc( nParts ); + Vec_Int_t * vRes = Vec_WecPushLevel( vNew ), * vArg; + Vec_IntAppend( vRes, Vec_WecEntry(vArgs, 0) ); + Vec_WecForEachLevelStart( vArgs, vArg, i, 1 ) { + Gia_ManGenNeuronAdder( pNew, nOBits, Vec_IntArray(vArg), Vec_IntArray(vRes), 0, vRes ); + if ( (i-1) % nLutSize == nLutSize-1 && i < Vec_WecSize(vArgs)-1 ) { + vRes = Vec_WecPushLevel( vNew ); + Vec_IntFill( vRes, nOBits, 0 ); + } + } + assert( Vec_WecSize(vNew) == nParts ); + return vNew; +} +Vec_Wec_t * Gia_ManGenNeuronCompactArgs( Gia_Man_t * pNew, Vec_Wec_t * vArgs, int nLutSize, int nOBits ) +{ + int i, nParts = Vec_WecSize(vArgs) / 3; + Vec_Wec_t * vNew = Vec_WecAlloc( 2 * nParts + Vec_WecSize(vArgs) % 3 ); + for ( i = 0; i < nParts; i++ ) { + Vec_Int_t * vIn0 = Vec_WecEntry(vArgs, 3*i+0); + Vec_Int_t * vIn1 = Vec_WecEntry(vArgs, 3*i+1); + Vec_Int_t * vIn2 = Vec_WecEntry(vArgs, 3*i+2); + Vec_Int_t * vOut0 = Vec_WecPushLevel(vNew); + Vec_Int_t * vOut1 = Vec_WecPushLevel(vNew); + Gia_ManGenCompact( pNew, vIn0, vIn1, vIn2, vOut0, vOut1 ); + } + for ( i = 3*nParts; i < Vec_WecSize(vArgs); i++ ) + Vec_IntAppend( Vec_WecPushLevel(vNew), Vec_WecEntry(vArgs, i) ); + assert( Vec_WecSize(vNew) == 2 * nParts + Vec_WecSize(vArgs) % 3 ); + return vNew; +} +Vec_Int_t * Gia_ManGenNeuronFinal( Gia_Man_t * pNew, Vec_Wec_t * vArgs, int nOBits ) +{ + Vec_Int_t * vRes = Vec_IntAlloc( nOBits ), * vArg; int i; + Vec_IntAppend( vRes, Vec_WecEntry(vArgs, 0) ); + Vec_WecForEachLevelStart( vArgs, vArg, i, 1 ) + Gia_ManGenNeuronAdder( pNew, nOBits, Vec_IntArray(vArg), Vec_IntArray(vRes), 0, vRes ); + return vRes; +} +int Gia_ManGenNeuronBitWidth( Vec_Wrd_t * vData, int nIBits ) +{ + int i, InMask = (1<pName = Abc_UtilStrsav( "neuron" ); + for ( i = 0; i < nIBits * (Vec_WrdSize(vData)-1); i++ ) + Gia_ManAppendCi( pNew ); + Gia_ManHashAlloc( pNew ); + + Vec_Wec_t * vTemp, * vArgs = Gia_ManGenNeuronCreateArgs( vData, nIBits, nOBits ); + Vec_WrdFree( vData ); + + if ( nLutSize ) { + vArgs = Gia_ManGenNeuronTransformArgs( pNew, vTemp = vArgs, nLutSize, nOBits ); + Vec_WecFree( vTemp ); + while ( Vec_WecSize(vArgs) > 2 ) { + vArgs = Gia_ManGenNeuronCompactArgs( pNew, vTemp = vArgs, nLutSize, nOBits ); + Vec_WecFree( vTemp ); + } + } + + Vec_Int_t * vRes = Gia_ManGenNeuronFinal( pNew, vArgs, nOBits ); + Vec_IntForEachEntry( vRes, Lit, i ) + Gia_ManAppendCo( pNew, Lit ); + Vec_IntFree( vRes ); + Vec_WecFree( vArgs ); + + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Generates minimum-node AIG for n-bit comparator (a > b).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupGenComp( int nBits, int fInterleave ) +{ + Gia_Man_t * pNew, * pTemp; int i, iLit = 1; + Vec_Int_t * vBitsA = Vec_IntAlloc( nBits + 1 ); + Vec_Int_t * vBitsB = Vec_IntAlloc( nBits + 1 ); + pNew = Gia_ManStart( 6*nBits+10 ); + pNew->pName = Abc_UtilStrsav( "comp" ); + Gia_ManHashAlloc( pNew ); + if ( fInterleave ) { + for ( i = 0; i < nBits; i++ ) + Vec_IntPush( vBitsA, Gia_ManAppendCi(pNew) ), + Vec_IntPush( vBitsB, Gia_ManAppendCi(pNew) ); + } + else { + for ( i = 0; i < nBits; i++ ) + Vec_IntPush( vBitsA, Gia_ManAppendCi(pNew) ); + for ( i = 0; i < nBits; i++ ) + Vec_IntPush( vBitsB, Gia_ManAppendCi(pNew) ); + } + Vec_IntPush( vBitsA, 0 ); + Vec_IntPush( vBitsB, 0 ); + for ( i = 0; i < nBits; i++ ) { + int iLitA0 = Vec_IntEntry(vBitsA, i); + int iLitA1 = Vec_IntEntry(vBitsA, i+1); + int iLitB0 = Vec_IntEntry(vBitsB, i); + int iLitB1 = Vec_IntEntry(vBitsB, i+1); + int iOrLit0; + if ( i == 0 ) + iOrLit0 = Gia_ManHashOr(pNew, Abc_LitNotCond(iLitA0, !(i&1)), Abc_LitNotCond(iLitB0, i&1)); + else + iOrLit0 = Gia_ManHashAnd(pNew, Abc_LitNotCond(iLitA0, !(i&1)), Abc_LitNotCond(iLitB0, i&1)); + int iOrLit1 = Gia_ManHashAnd(pNew, Abc_LitNotCond(iLitA1, !(i&1)), Abc_LitNotCond(iLitB1, i&1)); + int iOrLit = Gia_ManHashOr(pNew, iOrLit0, iOrLit1 ); + iLit = Gia_ManHashOr(pNew, Abc_LitNot(iLit), iOrLit ); + } + Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, nBits&1) ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + Vec_IntFree( vBitsA ); + Vec_IntFree( vBitsB ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Generates optimized AIG for the decoder and the multiplexer.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_GenDecoder( Gia_Man_t * p, int * pLits, int nLits ) +{ + if ( nLits == 1 ) + { + Vec_Int_t * vRes = Vec_IntAlloc( 2 ); + Vec_IntPush( vRes, Abc_LitNot(pLits[0]) ); + Vec_IntPush( vRes, pLits[0] ); + return vRes; + } + assert( nLits > 1 ); + int nPart1 = nLits / 2; + int nPart2 = nLits - nPart1; + Vec_Int_t * vRes1 = Gia_GenDecoder( p, pLits, nPart1 ); + Vec_Int_t * vRes2 = Gia_GenDecoder( p, pLits+nPart1, nPart2 ); + Vec_Int_t * vRes = Vec_IntAlloc( Vec_IntSize(vRes1) * Vec_IntSize(vRes2) ); + int i, k, Lit1, Lit2; + Vec_IntForEachEntry( vRes2, Lit2, k ) + Vec_IntForEachEntry( vRes1, Lit1, i ) + Vec_IntPush( vRes, Gia_ManHashAnd(p, Lit1, Lit2) ); + Vec_IntFree( vRes1 ); + Vec_IntFree( vRes2 ); + return vRes; +} +Gia_Man_t * Gia_ManGenMux( int nIns, char * pNums ) +{ + Vec_Int_t * vIns = Vec_IntAlloc( nIns ); + Vec_Int_t * vData = Vec_IntAlloc( 1 << nIns ); + Gia_Man_t * p = Gia_ManStart( 4*(1 << nIns) + nIns ), * pTemp; + int i, iStart = 0, nSize = 1 << nIns; + p->pName = Abc_UtilStrsav( "mux" ); + for ( i = 0; i < nIns; i++ ) + Vec_IntPush( vIns, Gia_ManAppendCi(p) ); + for ( i = 0; i < nSize; i++ ) + Vec_IntPush( vData, Gia_ManAppendCi(p) ); + Gia_ManHashAlloc( p ); + for ( i = (int)strlen(pNums)-1; i >= 0; i-- ) + { + int k, b, nBits = (int)(pNums[i] - '0'); + Vec_Int_t * vDec = Gia_GenDecoder( p, Vec_IntEntryP(vIns, iStart), nBits ); + for ( k = 0; k < nSize; k++ ) + Vec_IntWriteEntry( vData, k, Gia_ManHashAnd(p, Vec_IntEntry(vData, k), Vec_IntEntry(vDec, k%Vec_IntSize(vDec))) ); + for ( b = 0; b < nBits; b++, nSize /= 2 ) + for ( k = 0; k < nSize/2; k++ ) + Vec_IntWriteEntry( vData, k, Gia_ManHashOr(p, Vec_IntEntry(vData, 2*k), Vec_IntEntry(vData, 2*k+1)) ); + Vec_IntFree( vDec ); + iStart += nBits; + } + assert( nSize == 1 ); + Gia_ManAppendCo( p, Vec_IntEntry(vData, 0) ); + Vec_IntFree( vIns ); + Vec_IntFree( vData ); + p = Gia_ManCleanup( pTemp = p ); + Gia_ManStop( pTemp ); + return p; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 1ffca1789..c08a91ecd 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -2208,7 +2208,7 @@ void Gia_ManMappingVerify( Gia_Man_t * p ) continue; if ( !Gia_ObjIsLut(p, Gia_ObjId(p, pFanin)) ) { - Abc_Print( -1, "Gia_ManMappingVerify: CO driver %d does not have mapping.\n", Gia_ObjId(p, pFanin) ); + Abc_Print( -1, "Gia_ManMappingVerify: Buffer driver %d does not have mapping.\n", Gia_ObjId(p, pFanin) ); Result = 0; continue; } diff --git a/src/aig/gia/giaMinLut.c b/src/aig/gia/giaMinLut.c index 5304486de..e08ebec56 100644 --- a/src/aig/gia/giaMinLut.c +++ b/src/aig/gia/giaMinLut.c @@ -193,7 +193,7 @@ Gia_Man_t * Vec_WrdReadTest( char * pFileName ) void Vec_WrdReadText( char * pFileName, Vec_Wrd_t ** pvSimI, Vec_Wrd_t ** pvSimO, int nIns, int nOuts ) { int i, nSize, iLine, nLines, nWords; - char pLine[1000]; + char pLine[2000]; Vec_Wrd_t * vSimI, * vSimO; FILE * pFile = fopen( pFileName, "rb" ); if ( pFile == NULL ) @@ -214,7 +214,7 @@ void Vec_WrdReadText( char * pFileName, Vec_Wrd_t ** pvSimI, Vec_Wrd_t ** pvSimO nWords = (nLines + 63)/64; vSimI = Vec_WrdStart( nIns *nWords ); vSimO = Vec_WrdStart( nOuts*nWords ); - for ( iLine = 0; fgets( pLine, 1000, pFile ); iLine++ ) + for ( iLine = 0; fgets( pLine, 2000, pFile ); iLine++ ) { for ( i = 0; i < nIns; i++ ) if ( pLine[nIns-1-i] == '1' ) @@ -233,7 +233,7 @@ void Vec_WrdReadText( char * pFileName, Vec_Wrd_t ** pvSimI, Vec_Wrd_t ** pvSimO int Vec_WrdReadText2( char * pFileName, Vec_Wrd_t ** pvSimI ) { int i, nSize, iLine, nLines, nWords, nIns; - char pLine[1000]; + char pLine[2000]; Vec_Wrd_t * vSimI; FILE * pFile = fopen( pFileName, "rb" ); if ( pFile == NULL ) @@ -241,7 +241,7 @@ int Vec_WrdReadText2( char * pFileName, Vec_Wrd_t ** pvSimI ) printf( "Cannot open file \"%s\" for reading.\n", pFileName ); return 0; } - if ( !fgets(pLine, 1000, pFile) || (nIns = strlen(pLine)-1) < 1 ) + if ( !fgets(pLine, 2000, pFile) || (nIns = strlen(pLine)-1) < 1 ) { printf( "Cannot find the number of inputs in file \"%s\".\n", pFileName ); fclose( pFile ); @@ -259,7 +259,7 @@ int Vec_WrdReadText2( char * pFileName, Vec_Wrd_t ** pvSimI ) nLines = nSize / (nIns + 1); nWords = (nLines + 63)/64; vSimI = Vec_WrdStart( nIns *nWords ); - for ( iLine = 0; fgets( pLine, 1000, pFile ); iLine++ ) + for ( iLine = 0; fgets( pLine, 2000, pFile ); iLine++ ) { for ( i = 0; i < nIns; i++ ) if ( pLine[nIns-1-i] == '1' ) diff --git a/src/aig/gia/giaMulFind.c b/src/aig/gia/giaMulFind.c index 0c074094a..b7bc0b0b6 100644 --- a/src/aig/gia/giaMulFind.c +++ b/src/aig/gia/giaMulFind.c @@ -31,6 +31,403 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManMulFindXors2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXor ) +{ + if ( !Gia_ObjIsAnd(pObj) ) + return; + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( !pObj->fMark0 ) + { + if ( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) + && Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) >= 4 + && Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) >= 4 ) + Vec_IntPushTwo( vXor, Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninId1p(p, pObj) ); + return; + } + Gia_Obj_t * pFan0, * pFan1; + int RetValue = Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1); + assert( RetValue ); + Gia_ManMulFindXors2_rec( p, Gia_Regular(pFan0), vXor ); + Gia_ManMulFindXors2_rec( p, Gia_Regular(pFan1), vXor ); +} +Vec_Wec_t * Gia_ManMulFindXors2( Gia_Man_t * p ) +{ + Vec_Wec_t * vXors = Vec_WecAlloc( 100 ); + Vec_Int_t * vTemp = Vec_IntAlloc( 100 ); + Gia_Obj_t * pObj, * pFan0, * pFan1; int i; + Gia_ManCreateRefs( p ); + Gia_ManCleanMark01( p ); + Gia_ManForEachAnd( p, pObj, i ) { + if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) + continue; + Gia_Regular(pFan0)->fMark1 = 1; + Gia_Regular(pFan1)->fMark1 = 1; + pObj->fMark0 = 1; + } + Gia_ManForEachAnd( p, pObj, i ) { + if ( pObj->fMark0 && !pObj->fMark1 ) { + Gia_ManIncrementTravId( p ); + Vec_IntClear( vTemp ); + Gia_ManMulFindXors2_rec( p, pObj, vTemp ); + if ( Vec_IntSize(vTemp) > 0 ) + Vec_IntAppend( Vec_WecPushLevel(vXors), vTemp ); + } + } + Vec_IntFree( vTemp ); + return vXors; +} +int Gia_ManMulFindMaxSize( Vec_Wec_t * vXors, Vec_Int_t * vUsed ) +{ + Vec_Int_t * vLevel; int i, iBest = -1, nBestSize = 0; + Vec_WecForEachLevel( vXors, vLevel, i ) + if ( !Vec_IntEntry(vUsed, i) && nBestSize < Vec_IntSize(vLevel) ) + nBestSize = Vec_IntSize(vLevel), iBest = i; + return iBest; +} +int Gia_ManMulFindGetOverlap( Vec_Int_t * p1, Vec_Int_t * p2 ) +{ + int i, k, ObjI, ObjK, Counter = 0; + Vec_IntForEachEntry( p1, ObjI, i ) + Vec_IntForEachEntry( p2, ObjK, k ) + if ( ObjI == ObjK ) + Counter++; + return Counter; +} +int Gia_ManMulFindGetOverlap2( Vec_Int_t * p1, Vec_Int_t * p2 ) +{ + int i, k, ObjI, ObjK, Counter = 0; + Vec_IntForEachEntryStart( p1, ObjI, i, 1 ) + Vec_IntForEachEntry( p2, ObjK, k ) + if ( ObjI == ObjK ) + Counter++; + return Counter; +} +int Gia_ManMulFindMaxOverlap( Vec_Wec_t * vXors, Vec_Int_t * vUsed, Vec_Int_t * vFound ) +{ + Vec_Int_t * vLevel; int i, iBest = -1, nThisSize, nBestSize = 0; + Vec_WecForEachLevel( vXors, vLevel, i ) + if ( !Vec_IntEntry(vUsed, i) && nBestSize < (nThisSize = Gia_ManMulFindGetOverlap(vFound, vLevel)) ) + nBestSize = nThisSize, iBest = i; + return iBest; +} +Vec_Wec_t * Gia_ManMulFindSets( Gia_Man_t * p, Vec_Wec_t * vXors ) +{ + Vec_Wec_t * vSets = Vec_WecAlloc( 100 ); + Vec_Int_t * vUsed = Vec_IntStart( Vec_WecSize(vXors) ); + Vec_Int_t * vFound = Vec_IntAlloc( 100 ); int Item, k, Obj; + while ( (Item = Gia_ManMulFindMaxSize(vXors, vUsed)) != -1 ) { + Vec_Int_t * vTemp = Vec_WecEntry(vXors, Item); + Vec_Int_t * vNew = Vec_WecPushLevel( vSets ); + Vec_IntPush( vNew, Item ); + Vec_IntWriteEntry( vUsed, Item, 1 ); + Vec_IntClear( vFound ); + Vec_IntAppend( vFound, vTemp ); + while ( (Item = Gia_ManMulFindMaxOverlap(vXors, vUsed, vFound)) != -1 ) { + Vec_IntPush( vNew, Item ); + Vec_IntWriteEntry( vUsed, Item, 1 ); + vTemp = Vec_WecEntry(vXors, Item); + Vec_IntForEachEntry( vTemp, Obj, k ) + Vec_IntPushUnique( vFound, Obj ); + } + } + Vec_IntFree( vUsed ); + Vec_IntFree( vFound ); + return vSets; +} +int Gia_ManMulFindOne( Gia_Man_t * p, Vec_Wec_t * vXors, Vec_Int_t * vSet, Vec_Int_t * vMap, Vec_Int_t * vA, Vec_Int_t * vB, int fVerbose ) +{ + Vec_Int_t * vObjs = Vec_IntAlloc( 100 ); int i, j, Obj, Obj1, Obj2; + Vec_IntForEachEntry( vSet, Obj, i ) + Vec_IntAppend( vObjs, Vec_WecEntry(vXors, Obj) ); + Vec_IntForEachEntry( vObjs, Obj, i ) + Vec_IntAddToEntry( vMap, Obj, 1 ); + Vec_IntForEachEntry( vSet, Obj, i ) { + Vec_Int_t * vTemp = Vec_WecEntry(vXors, Obj); int k = 0; + Vec_IntForEachEntryDouble( vTemp, Obj1, Obj2, j ) + if ( Vec_IntEntry(vMap, Obj1) > 1 || Vec_IntEntry(vMap, Obj2) > 1 ) + Vec_IntWriteEntry(vTemp, k++, Obj1), Vec_IntWriteEntry(vTemp, k++, Obj2); + Vec_IntShrink( vTemp, k ); + } + Vec_IntForEachEntry( vObjs, Obj, i ) + Vec_IntWriteEntry( vMap, Obj, 0 ); + Vec_IntClear( vObjs ); + Vec_IntForEachEntry( vSet, Obj, i ) + Vec_IntAppend( vObjs, Vec_WecEntry(vXors, Obj) ); + if ( Vec_IntSize(vObjs) == 0 ) { + Vec_IntFree(vObjs); + return 0; + } + + Vec_IntClear( vA ); + Vec_IntClear( vB ); + Vec_IntPush( vA, Vec_IntPop(vObjs) ); + Vec_IntPush( vB, Vec_IntPop(vObjs) ); + while ( Vec_IntSize(vObjs) > 0 ) { + int k = 0; + Vec_IntForEachEntryDouble( vObjs, Obj1, Obj2, j ) { + if ( Vec_IntFind(vA, Obj1) >= 0 ) + Vec_IntPushUnique(vB, Obj2); + else if ( Vec_IntFind(vA, Obj2) >= 0 ) + Vec_IntPushUnique(vB, Obj1); + else if ( Vec_IntFind(vB, Obj1) >= 0 ) + Vec_IntPushUnique(vA, Obj2); + else if ( Vec_IntFind(vB, Obj2) >= 0 ) + Vec_IntPushUnique(vA, Obj1); + else { + Vec_IntWriteEntry(vObjs, k++, Obj1); + Vec_IntWriteEntry(vObjs, k++, Obj2); + } + } + Vec_IntShrink( vObjs, k ); + } + Vec_IntSort( vA, 0 ); + Vec_IntSort( vB, 0 ); + Vec_IntClear( vObjs ); + Vec_IntForEachEntry( vSet, Obj, i ) + Vec_IntAppend( vObjs, Vec_WecEntry(vXors, Obj) ); + Vec_IntForEachEntryDouble( vObjs, Obj1, Obj2, j ) + if ( !((Vec_IntFind(vA, Obj1) >= 0 && Vec_IntFind(vB, Obj2) >= 0) || + (Vec_IntFind(vA, Obj2) >= 0 && Vec_IntFind(vB, Obj1) >= 0)) ) { + if ( fVerbose ) + printf( "Internal verification failed.\n" ); + Vec_IntFree( vObjs ); + Vec_IntClear( vA ); + Vec_IntClear( vB ); + return 0; + } + if ( fVerbose ) + printf( "Generated system with %d+%d+%d=%d variables and %d equations.\n", + Vec_IntSize(vA),Vec_IntSize(vB),Vec_IntSize(vSet), + Vec_IntSize(vA)+Vec_IntSize(vB)+Vec_IntSize(vSet), Vec_IntSize(vObjs)/2 ); + Vec_IntFree( vObjs ); + return 1; +} +Vec_Wec_t * Gia_ManMulFindAInputs2( Gia_Man_t * p, int fVerbose ) +{ + Vec_Wec_t * vMuls = Vec_WecAlloc( 10 ); + Vec_Wec_t * vXors = Gia_ManMulFindXors2( p ); + Vec_Wec_t * vSets = Gia_ManMulFindSets( p, vXors ); + Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(p) ); + Vec_Int_t * vA = Vec_IntAlloc( 100 ); + Vec_Int_t * vB = Vec_IntAlloc( 100 ); + Vec_Int_t * vSet; int i; + Vec_WecForEachLevel( vSets, vSet, i ) + { + if ( !Gia_ManMulFindOne(p, vXors, vSet, vMap, vA, vB, fVerbose) ) + continue; + Vec_IntAppend( Vec_WecPushLevel(vMuls), vA ); + Vec_IntAppend( Vec_WecPushLevel(vMuls), vB ); + Vec_WecPushLevel(vMuls); + } + Vec_WecFree( vXors ); + Vec_WecFree( vSets ); + Vec_IntFree( vMap ); + Vec_IntFree( vA ); + Vec_IntFree( vB ); + return vMuls; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManMulFindAddEntry1( Vec_Int_t * vPairs, int Obj ) +{ + int Entry, Sum, k; + Vec_IntForEachEntryDouble( vPairs, Entry, Sum, k ) + if ( Obj == Entry ) { + Vec_IntAddToEntry( vPairs, k+1, 1 ); + break; + } + if ( k == Vec_IntSize(vPairs) ) + Vec_IntPushTwo( vPairs, Obj, 1 ); +} +Vec_Int_t * Gia_ManMulFindCounts( Vec_Wec_t * vCuts4, Vec_Int_t * vSet ) +{ + Vec_Int_t * vCounts = Vec_IntAlloc( 10 ); + int i, k, Obj, Item; + Vec_IntForEachEntry( vSet, Item, i ) { + Vec_Int_t * vCut = Vec_WecEntry(vCuts4, Item); + Vec_IntForEachEntryStart( vCut, Obj, k, 1 ) + Gia_ManMulFindAddEntry1( vCounts, Obj ); + } + return vCounts; +} +int Gia_ManMulFindNextEntry( Vec_Wec_t * vCuts4, Vec_Int_t * vSet, int Entry ) +{ + int i, Item; + Vec_IntForEachEntry( vSet, Item, i ) { + Vec_Int_t * vCut = Vec_WecEntry(vCuts4, Item); + if ( Vec_IntSize(vCut) == 0 ) + continue; + assert( Vec_IntSize(vCut) == 3 ); + int RetValue = -1; + if ( Vec_IntEntry(vCut, 1) == Entry ) + RetValue = Vec_IntEntry(vCut, 2); + if ( Vec_IntEntry(vCut, 2) == Entry ) + RetValue = Vec_IntEntry(vCut, 1); + if ( RetValue == -1 ) + continue; + Vec_IntClear( vCut ); + return RetValue; + } + return -1; +} +void Gia_ManMulFindArg1( Vec_Wec_t * vCuts4, Vec_Int_t * vSet, Vec_Int_t * vArg1 ) +{ + Vec_Int_t * vCounts = Gia_ManMulFindCounts( vCuts4, vSet ); + int Entry = -1, Sum, k; + Vec_IntClear( vArg1 ); + Vec_IntForEachEntryDouble( vCounts, Entry, Sum, k ) + if ( Sum == 1 ) { + Vec_IntPush( vArg1, Entry ); + break; + } + assert( Entry != -1 ); + while ( (Entry = Gia_ManMulFindNextEntry(vCuts4, vSet, Entry)) != -1 ) + Vec_IntPush( vArg1, Entry ); + Vec_IntFree( vCounts ); +} +int Gia_ManMulFindNextEntryCount( Vec_Int_t * vCounts, int Entry0 ) +{ + int Entry, Sum, k; + Vec_IntForEachEntryDouble( vCounts, Entry, Sum, k ) + if ( Entry == Entry0 ) + return Sum; + return -1; +} +int Gia_ManMulFindNextEntry2( Vec_Wec_t * vCuts4, Vec_Int_t * vSet, int Entry, Vec_Int_t * vCounts, int * pEntry0, int * pEntry1 ) +{ + int i, Item; + Vec_IntForEachEntry( vSet, Item, i ) { + Vec_Int_t * vCut = Vec_WecEntry(vCuts4, Item); + if ( Vec_IntSize(vCut) == 0 ) + continue; + assert( Vec_IntSize(vCut) == 4 ); + int Entry0, Entry1, iPlace = Vec_IntFind( vCut, Entry ); + if ( iPlace == -1 ) + continue; + if ( iPlace == 1 ) + Entry0 = Vec_IntEntry(vCut, 2), Entry1 = Vec_IntEntry(vCut, 3); + else if ( iPlace == 2 ) + Entry0 = Vec_IntEntry(vCut, 1), Entry1 = Vec_IntEntry(vCut, 3); + else if ( iPlace == 3 ) + Entry0 = Vec_IntEntry(vCut, 1), Entry1 = Vec_IntEntry(vCut, 2); + else assert( 0 ); + int Count0 = Gia_ManMulFindNextEntryCount(vCounts, Entry0); + int Count1 = Gia_ManMulFindNextEntryCount(vCounts, Entry1); + *pEntry0 = Count0 <= Count1 ? Entry0 : Entry1; + *pEntry1 = Count0 <= Count1 ? Entry1 : Entry0; + // remove entries + Vec_IntForEachEntry( vSet, Item, i ) { + Vec_Int_t * vCut = Vec_WecEntry(vCuts4, Item); + if ( Vec_IntSize(vCut) == 0 ) + continue; + if ( Vec_IntFind( vCut, Entry ) >= 0 ) + Vec_IntClear( vCut ); + } + return 1; + } + return 0; +} +void Gia_ManMulFindArg2( Vec_Wec_t * vCuts5, Vec_Int_t * vSet, Vec_Int_t * vArg2, int Entry0, int Entry1 ) +{ + Vec_Int_t * vCounts = Gia_ManMulFindCounts( vCuts5, vSet ); + int Entry, Sum, k, SumMin = ABC_INFINITY, SumMax = 0; + Vec_IntForEachEntryDouble( vCounts, Entry, Sum, k ) { + SumMin = Abc_MinInt( SumMin, Sum ); + SumMax = Abc_MaxInt( SumMax, Sum ); + } + Vec_IntClear( vArg2 ); + Vec_IntForEachEntryDouble( vCounts, Entry, Sum, k ) + if ( Entry == Entry0 || Entry == Entry1 ) { + Vec_IntPush( vArg2, Entry == Entry0 ? Entry1 : Entry0 ); + Vec_IntPush( vArg2, Entry ); + break; + } + Entry = Vec_IntEntry(vArg2, 1); + while ( Gia_ManMulFindNextEntry2(vCuts5, vSet, Entry, vCounts, &Entry0, &Entry1) ) + Vec_IntPushTwo( vArg2, Entry0, Entry1 ), Entry = Entry1; + Vec_IntFree( vCounts ); +} +void Gia_ManMulFindAddEntry( Vec_Int_t * vPairs, int Obj0, int Obj1 ) +{ + int Entry0, Entry1, Sum, k; + Vec_IntForEachEntryTriple( vPairs, Entry0, Entry1, Sum, k ) + if ( Obj0 == Entry0 && Obj1 == Entry1 ) { + Vec_IntAddToEntry( vPairs, k+2, 1 ); + break; + } + if ( k == Vec_IntSize(vPairs) ) + Vec_IntPushThree( vPairs, Obj0, Obj1, 1 ); +} +Vec_Wec_t * Gia_ManMulFindBInputs2( Gia_Man_t * p, Vec_Wec_t * vCuts4, Vec_Wec_t * vCuts5, int fVerbose ) +{ + Vec_Wec_t * vRes = Vec_WecAlloc( 10 ); + Vec_Int_t * vPairs = Vec_IntAlloc( 1000 ); + Vec_Int_t * vSet = Vec_IntAlloc( 100 ); + Vec_Int_t * vCut, * vArg1, * vArg2; + int i, j, k, n, Entry0, Entry1, Sum, Obj0, Obj1; + Vec_WecForEachLevel( vCuts4, vCut, i ) + Vec_IntForEachEntryStart( vCut, Obj0, j, 1 ) + Vec_IntForEachEntryStart( vCut, Obj1, k, j+1 ) + Gia_ManMulFindAddEntry( vPairs, Obj0, Obj1 ); + Vec_IntForEachEntryTriple( vPairs, Entry0, Entry1, Sum, n ) { + if ( Sum < 3 ) + continue; + Vec_IntClear( vSet ); + Vec_WecForEachLevel( vCuts4, vCut, i ) + Vec_IntForEachEntryStart( vCut, Obj0, j, 1 ) + Vec_IntForEachEntryStart( vCut, Obj1, k, j+1 ) + if ( Obj0 == Entry0 && Obj1 == Entry1 ) { + Vec_IntPush( vSet, i ); + Vec_IntDrop( vCut, k ); + Vec_IntDrop( vCut, j ); + j = k = Vec_IntSize(vCut); + } + vArg1 = Vec_WecPushLevel(vRes); + vArg2 = Vec_WecPushLevel(vRes); + Vec_WecPushLevel(vRes); + Gia_ManMulFindArg1( vCuts4, vSet, vArg1 ); + // find overlapping with arg1 and remove nodes in arg1 + Vec_IntClear( vSet ); + Vec_WecForEachLevel( vCuts5, vCut, i ) + if ( Gia_ManMulFindGetOverlap2(vCut, vArg1) ) { + k = 1; + Vec_IntForEachEntryStart( vCut, Obj0, j, 1 ) + if ( Vec_IntFind(vArg1, Obj0) == -1 ) + Vec_IntWriteEntry( vCut, k++, Obj0 ); + Vec_IntShrink( vCut, k ); + Vec_IntPush( vSet, i ); + } + Gia_ManMulFindArg2( vCuts5, vSet, vArg2, Entry0, Entry1 ); + } + Vec_IntFree( vSet ); + Vec_IntFree( vPairs ); + return vRes; +} + /**Function************************************************************* Synopsis [] @@ -331,6 +728,7 @@ Vec_Wrd_t * Gia_ManMulFindSim( Vec_Wrd_t * vSim0, Vec_Wrd_t * vSim1, int fSigned } void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fVerbose ) { + Abc_Random(1); for ( int m = 0; m < Vec_WecSize(vTerms)/3; m++ ) { Vec_Int_t * vIn0 = Vec_WecEntry(vTerms, 3*m+0); Vec_Int_t * vIn1 = Vec_WecEntry(vTerms, 3*m+1); @@ -341,46 +739,47 @@ void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fVerbose ) Vec_Wrd_t * vSimS = Gia_ManMulFindSim( vSim0, vSim1, 1 ); Vec_Int_t * vTfo = Gia_ManMulFindTfo( p, vIn0, vIn1 ); Vec_Wrd_t * vSims = Gia_ManMulFindSimCone( p, vIn0, vIn1, vSim0, vSim1, vTfo ); + Vec_Int_t * vOutU = Vec_IntAlloc( 100 ); + Vec_Int_t * vOutS = Vec_IntAlloc( 100 ); word Word; int w, iPlace; - assert( Vec_IntSize(vOut) == 0 ); Vec_WrdForEachEntry( vSimU, Word, w ) { if ( (iPlace = Vec_WrdFind(vSims, Word)) >= 0 ) - Vec_IntPush( vOut, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 0) ); + Vec_IntPush( vOutU, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 0) ); else if ( (iPlace = Vec_WrdFind(vSims, ~Word)) >= 0 ) - Vec_IntPush( vOut, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 1) ); + Vec_IntPush( vOutU, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 1) ); else - break; + Vec_IntPush( vOutU, -1 ); } - if ( w == Vec_WrdSize(vSimU) ) - Vec_IntPush(vOut, 0); - else - Vec_IntClear(vOut); - if ( Vec_IntSize(vOut) == 0 ) + Vec_WrdForEachEntry( vSimS, Word, w ) { + if ( (iPlace = Vec_WrdFind(vSims, Word)) >= 0 ) + Vec_IntPush( vOutS, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 0) ); + else if ( (iPlace = Vec_WrdFind(vSims, ~Word)) >= 0 ) + Vec_IntPush( vOutS, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 1) ); + else + Vec_IntPush( vOutS, -1 ); + } + assert( Vec_IntSize(vOut) == 0 ); + if ( Vec_IntCountEntry(vOutU, -1) < Vec_IntSize(vOutU) || + Vec_IntCountEntry(vOutS, -1) < Vec_IntSize(vOutS) ) { - Vec_IntClear(vOut); - Vec_WrdForEachEntry( vSimS, Word, w ) { - if ( (iPlace = Vec_WrdFind(vSims, Word)) >= 0 ) - Vec_IntPush( vOut, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 0) ); - else if ( (iPlace = Vec_WrdFind(vSims, ~Word)) >= 0 ) - Vec_IntPush( vOut, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 1) ); - else - break; - } - if ( w == Vec_WrdSize(vSimS) ) - Vec_IntPush(vOut, 1); + if ( Vec_IntCountEntry(vOutU, -1) < Vec_IntCountEntry(vOutS, -1) ) + Vec_IntAppend( vOut, vOutU ), Vec_IntPush(vOut, 0); else - Vec_IntClear(vOut); + Vec_IntAppend( vOut, vOutS ), Vec_IntPush(vOut, 1); } + else + { + Vec_IntClear(vIn0); + Vec_IntClear(vIn1); + } Vec_WrdFree( vSim0 ); Vec_WrdFree( vSim1 ); Vec_WrdFree( vSimU ); Vec_WrdFree( vSimS ); Vec_WrdFree( vSims ); Vec_IntFree( vTfo ); - if ( Vec_IntSize(vOut) ) - continue; - Vec_IntClear(vIn0); - Vec_IntClear(vIn1); + Vec_IntFree( vOutU ); + Vec_IntFree( vOutS ); } Vec_WecRemoveEmpty( vTerms ); } @@ -413,7 +812,7 @@ Vec_Ptr_t * Gia_ManMulFindCuts( Gia_Man_t * p, int nCutNum, int fVerbose ) Vec_Wec_t * Gia_ManMulFindA( Gia_Man_t * p, Vec_Wec_t * vCuts3, int fVerbose ) { Vec_Wec_t * vXors = Gia_ManMulFindXors( p, vCuts3, fVerbose ); - Vec_Wec_t * vTerms = Gia_ManMulFindAInputs( p, vXors, fVerbose ); + Vec_Wec_t * vTerms = Gia_ManMulFindAInputs2( p, fVerbose ); if ( Vec_WecSize(vTerms) ) Gia_ManMulFindOutputs( p, vTerms, fVerbose ); Vec_WecFree( vXors ); @@ -423,7 +822,7 @@ Vec_Wec_t * Gia_ManMulFindB( Gia_Man_t * p, Vec_Wec_t * vCuts4, Vec_Wec_t * vCut { Vec_Wec_t * vTerms = Vec_WecAlloc( 12 ); if ( Vec_WecSize(vCuts4) && Vec_WecSize(vCuts5) ) - vTerms = Gia_ManMulFindBInputs( p, vCuts4, vCuts5, fVerbose ); + vTerms = Gia_ManMulFindBInputs2( p, vCuts4, vCuts5, fVerbose ); if ( Vec_WecSize(vTerms) ) Gia_ManMulFindOutputs( p, vTerms, fVerbose ); return vTerms; @@ -432,8 +831,12 @@ void Gia_ManMulFindPrintSet( Vec_Int_t * vSet, int fLit, int fSkipLast ) { int i, Temp, Limit = Vec_IntSize(vSet) - fSkipLast; printf( "{" ); - Vec_IntForEachEntryStop( vSet, Temp, i, Limit ) - printf( "%s%d%s", (fLit & Abc_LitIsCompl(Temp)) ? "~":"", fLit ? Abc_Lit2Var(Temp) : Temp, i < Limit-1 ? " ":"" ); + Vec_IntForEachEntryStop( vSet, Temp, i, Limit ) { + if ( Temp == -1 ) + printf( "n/a%s", i < Limit-1 ? " ":"" ); + else + printf( "%s%d%s", (fLit & Abc_LitIsCompl(Temp)) ? "~":"", fLit ? Abc_Lit2Var(Temp) : Temp, i < Limit-1 ? " ":"" ); + } printf( "}" ); } void Gia_ManMulFindPrintOne( Vec_Wec_t * vTerms, int m, int fBooth ) @@ -441,7 +844,7 @@ void Gia_ManMulFindPrintOne( Vec_Wec_t * vTerms, int m, int fBooth ) Vec_Int_t * vIn0 = Vec_WecEntry(vTerms, 3*m+0); Vec_Int_t * vIn1 = Vec_WecEntry(vTerms, 3*m+1); Vec_Int_t * vOut = Vec_WecEntry(vTerms, 3*m+2); - printf( "%sooth %ssigned : ", fBooth ? "B" : "Non-b", Vec_IntEntryLast(vOut) ? "" : "un" ); + printf( "%sooth %ssigned %d x %d: ", fBooth ? "B" : "Non-b", Vec_IntEntryLast(vOut) ? "" : "un", Vec_IntSize(vIn0), Vec_IntSize(vIn1) ); Gia_ManMulFindPrintSet( vIn0, 0, 0 ); printf( " * " ); Gia_ManMulFindPrintSet( vIn1, 0, 0 ); diff --git a/src/aig/gia/giaPat2.c b/src/aig/gia/giaPat2.c index b557ac6f8..93c4b1da9 100644 --- a/src/aig/gia/giaPat2.c +++ b/src/aig/gia/giaPat2.c @@ -1372,6 +1372,65 @@ void Min_ManTest2( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ +void Gia_GenerateCexesDumpBlif( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCexes ) +{ + extern Vec_Ptr_t * Gia_GetFakeNames( int nNames, int fCaps ); + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) { + printf( "Cannot open output file name \"%s\".\n", pFileName ); + return; + } + int fFakeIns = 0, fFakeOuts = 0; + if ( p->vNamesIn == NULL ) + p->vNamesIn = Gia_GetFakeNames( Gia_ManCiNum(p), 0 ), fFakeIns = 1; + if ( p->vNamesOut == NULL ) + p->vNamesOut = Gia_GetFakeNames( Gia_ManCoNum(p), 1 ), fFakeOuts = 1; + + Gia_Obj_t * pObj, * pObj2; + char * pLine = ABC_CALLOC( char, Gia_ManCiNum(p)+3 ); + int i, k, c, iLit, nOuts[2] = {0}, nCexes = Vec_WecSize(vCexes) / Gia_ManCoNum(p); + fprintf( pFile, "# Satisfying assignments for the primary outputs generated by ABC on %s\n", Gia_TimeStamp() ); + fprintf( pFile, ".model %s\n", p->pName ); + fprintf( pFile, ".inputs" ); + Gia_ManForEachCi( p, pObj, i ) + fprintf( pFile, " %s", Gia_ObjCiName(p, i) ); + fprintf( pFile, "\n.outputs" ); + Gia_ManForEachCo( p, pObj, i ) + fprintf( pFile, " %s", Gia_ObjCoName(p, i) ); + fprintf( pFile, "\n" ); + Gia_ManForEachCo( p, pObj, i ) { + if ( Gia_ObjFaninLit0p(p, pObj) == 0 ) { + fprintf( pFile, ".names %s\n", Gia_ObjCoName(p, i) ); + nOuts[0]++; + } + else if ( Gia_ObjFaninLit0p(p, pObj) == 1 ) { + fprintf( pFile, ".names %s\n 1\n", Gia_ObjCiName(p, i) ); + nOuts[1]++; + } + else { + fprintf( pFile, ".names" ); + Gia_ManForEachCi( p, pObj2, c ) + fprintf( pFile, " %s", Gia_ObjCiName(p, c) ); + fprintf( pFile, " %s\n", Gia_ObjCoName(p, i) ); + for ( c = 0; c < nCexes; c++ ) { + Vec_Int_t * vPat = Vec_WecEntry( vCexes, i*nCexes+c ); + memset(pLine, '-', Gia_ManCiNum(p) ); + Vec_IntForEachEntry( vPat, iLit, k ) + pLine[Abc_Lit2Var(iLit)-1] = '1' - Abc_LitIsCompl(iLit); + fprintf( pFile, "%s 1\n", pLine ); + } + nOuts[1]++; + } + } + fprintf( pFile, ".end\n\n" ); + fclose( pFile ); + printf( "Information about %d sat, %d unsat, and %d undecided primary outputs was written into BLIF file \"%s\".\n", + nOuts[1], nOuts[0], Gia_ManCoNum(p)-nOuts[1]-nOuts[0], pFileName ); + free( pLine ); + + if ( fFakeIns ) Vec_PtrFreeFree( p->vNamesIn ), p->vNamesIn = NULL; + if ( fFakeOuts ) Vec_PtrFreeFree( p->vNamesOut ), p->vNamesOut = NULL; +} void Gia_GenerateCexesDumpFile( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCexes, int fShort ) { FILE * pFile = fopen( pFileName, "wb" ); @@ -1416,13 +1475,16 @@ void Gia_GenerateCexesDumpFile( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCe fclose( pFile ); free( pLine ); } -void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fVerbose, int fVeryVerbose ) +void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fBlif, int fVerbose, int fVeryVerbose ) { unsigned Start = Abc_Random(1); Vec_Int_t * vStats[3] = {0}; int i; Vec_Wec_t * vCexes = Min_ManComputeCexes( p, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose ); assert( Vec_WecSize(vCexes) == Gia_ManCoNum(p) * nMinCexes ); - Gia_GenerateCexesDumpFile( pFileName, p, vCexes, fShort ); + if ( fBlif ) + Gia_GenerateCexesDumpBlif( pFileName, p, vCexes ); + else + Gia_GenerateCexesDumpFile( pFileName, p, vCexes, fShort ); for ( i = 0; i < 3; i++ ) Vec_IntFreeP( &vStats[i] ); Vec_WecFree( vCexes ); diff --git a/src/aig/gia/giaTtopt.cpp b/src/aig/gia/giaTtopt.cpp index a765633f8..7f16b0d06 100644 --- a/src/aig/gia/giaTtopt.cpp +++ b/src/aig/gia/giaTtopt.cpp @@ -1176,6 +1176,17 @@ Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, c { vSupp = Gia_ManCollectSuppNew( p, g, nOuts ); nInputs = Vec_IntSize( vSupp ); + if ( nInputs == 0 ) + { + for ( k = 0; k < nOuts; k++ ) + { + pObj = Gia_ManCo( p, g+k ); + pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ObjFanin0(pObj), vSupp ); + Gia_ManAppendCo( pNew, pTruth[0] & 1 ); + } + Vec_IntFree( vSupp ); + continue; + } Ttopt::TruthTableLevelTSM tt( nInputs, nOuts ); for ( k = 0; k < nOuts; k++ ) { diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index b60b039be..41c56c1fa 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -140,6 +140,42 @@ char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix ) return Buffer; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Gia_GetFakeNames( int nNames, int fCaps ) +{ + Vec_Ptr_t * vNames; + char Buffer[5]; + int i; + + vNames = Vec_PtrAlloc( nNames ); + for ( i = 0; i < nNames; i++ ) + { + if ( nNames < 26 ) + { + Buffer[0] = (fCaps ? 'A' : 'a') + i; + Buffer[1] = 0; + } + else + { + Buffer[0] = (fCaps ? 'A' : 'a') + i%26; + Buffer[1] = '0' + i/26; + Buffer[2] = 0; + } + Vec_PtrPush( vNames, Extra_UtilStrsav(Buffer) ); + } + return vNames; +} + /**Function************************************************************* Synopsis [] @@ -760,6 +796,23 @@ void Gia_ManCreateRefs( Gia_Man_t * p ) Gia_ObjRefFanin0Inc( p, pObj ); } } +void Gia_ManCreateLitRefs( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i; + assert( p->pRefs == NULL ); + p->pRefs = ABC_CALLOC( int, 2*Gia_ManObjNum(p) ); + Gia_ManForEachObj( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + { + p->pRefs[Gia_ObjFaninLit0(pObj, i)]++; + p->pRefs[Gia_ObjFaninLit1(pObj, i)]++; + } + else if ( Gia_ObjIsCo(pObj) ) + p->pRefs[Gia_ObjFaninLit0(pObj, i)]++; + } +} /**Function************************************************************* @@ -3279,73 +3332,6 @@ void Gia_ManTestProblem() } } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_GenDecoder( Gia_Man_t * p, int * pLits, int nLits ) -{ - if ( nLits == 1 ) - { - Vec_Int_t * vRes = Vec_IntAlloc( 2 ); - Vec_IntPush( vRes, Abc_LitNot(pLits[0]) ); - Vec_IntPush( vRes, pLits[0] ); - return vRes; - } - assert( nLits > 1 ); - int nPart1 = nLits / 2; - int nPart2 = nLits - nPart1; - Vec_Int_t * vRes1 = Gia_GenDecoder( p, pLits, nPart1 ); - Vec_Int_t * vRes2 = Gia_GenDecoder( p, pLits+nPart1, nPart2 ); - Vec_Int_t * vRes = Vec_IntAlloc( Vec_IntSize(vRes1) * Vec_IntSize(vRes2) ); - int i, k, Lit1, Lit2; - Vec_IntForEachEntry( vRes2, Lit2, k ) - Vec_IntForEachEntry( vRes1, Lit1, i ) - Vec_IntPush( vRes, Gia_ManHashAnd(p, Lit1, Lit2) ); - Vec_IntFree( vRes1 ); - Vec_IntFree( vRes2 ); - return vRes; -} -Gia_Man_t * Gia_ManGenMux( int nIns, char * pNums ) -{ - Vec_Int_t * vIns = Vec_IntAlloc( nIns ); - Vec_Int_t * vData = Vec_IntAlloc( 1 << nIns ); - Gia_Man_t * p = Gia_ManStart( 4*(1 << nIns) + nIns ), * pTemp; - int i, iStart = 0, nSize = 1 << nIns; - p->pName = Abc_UtilStrsav( "mux" ); - for ( i = 0; i < nIns; i++ ) - Vec_IntPush( vIns, Gia_ManAppendCi(p) ); - for ( i = 0; i < nSize; i++ ) - Vec_IntPush( vData, Gia_ManAppendCi(p) ); - Gia_ManHashAlloc( p ); - for ( i = (int)strlen(pNums)-1; i >= 0; i-- ) - { - int k, b, nBits = (int)(pNums[i] - '0'); - Vec_Int_t * vDec = Gia_GenDecoder( p, Vec_IntEntryP(vIns, iStart), nBits ); - for ( k = 0; k < nSize; k++ ) - Vec_IntWriteEntry( vData, k, Gia_ManHashAnd(p, Vec_IntEntry(vData, k), Vec_IntEntry(vDec, k%Vec_IntSize(vDec))) ); - for ( b = 0; b < nBits; b++, nSize /= 2 ) - for ( k = 0; k < nSize/2; k++ ) - Vec_IntWriteEntry( vData, k, Gia_ManHashOr(p, Vec_IntEntry(vData, 2*k), Vec_IntEntry(vData, 2*k+1)) ); - Vec_IntFree( vDec ); - iStart += nBits; - } - assert( nSize == 1 ); - Gia_ManAppendCo( p, Vec_IntEntry(vData, 0) ); - Vec_IntFree( vIns ); - Vec_IntFree( vData ); - p = Gia_ManCleanup( pTemp = p ); - Gia_ManStop( pTemp ); - return p; -} - /**Function************************************************************* Synopsis [Returns 1 if this window has a topo error (forward path from an output to an input).] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c61e3f437..ed4a88f6d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -182,6 +182,7 @@ static int Abc_CommandSwapPos ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandRemovePo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDropSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAddPi ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAddFlop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAppend ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPutOnTop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -427,6 +428,7 @@ static int Abc_CommandAbc9Strash ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Topand ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Add1Hot ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Cofs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Sim ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -613,6 +615,8 @@ static int Abc_CommandAbc9GenCex ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Odc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenRel ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenMux ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GenComp ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GenNeuron ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Window ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9FunAbs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9DsdInfo ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -978,6 +982,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "removepo", Abc_CommandRemovePo, 1 ); Cmd_CommandAdd( pAbc, "Various", "dropsat", Abc_CommandDropSat, 1 ); Cmd_CommandAdd( pAbc, "Various", "addpi", Abc_CommandAddPi, 1 ); + Cmd_CommandAdd( pAbc, "Various", "addflop", Abc_CommandAddFlop, 1 ); Cmd_CommandAdd( pAbc, "Various", "append", Abc_CommandAppend, 1 ); Cmd_CommandAdd( pAbc, "Various", "putontop", Abc_CommandPutOnTop, 1 ); Cmd_CommandAdd( pAbc, "Various", "frames", Abc_CommandFrames, 1 ); @@ -1221,6 +1226,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&topand", Abc_CommandAbc9Topand, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&add1hot", Abc_CommandAbc9Add1Hot, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&cof", Abc_CommandAbc9Cof, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&cofs", Abc_CommandAbc9Cofs, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&trim", Abc_CommandAbc9Trim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&dfs", Abc_CommandAbc9Dfs, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sim", Abc_CommandAbc9Sim, 0 ); @@ -1413,6 +1419,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&odc", Abc_CommandAbc9Odc, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&genrel", Abc_CommandAbc9GenRel, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&genmux", Abc_CommandAbc9GenMux, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&gencomp", Abc_CommandAbc9GenComp, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&genneuron", Abc_CommandAbc9GenNeuron, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&window", Abc_CommandAbc9Window, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&funabs", Abc_CommandAbc9FunAbs, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&dsdinfo", Abc_CommandAbc9DsdInfo, 0 ); @@ -9802,7 +9810,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INKTiaogvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INKTiaocgvh" ) ) != EOF ) { switch ( c ) { @@ -9859,6 +9867,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'o': pPars->fFewerVars ^= 1; break; + case 'c': + pPars->fLutCascade ^= 1; + break; case 'g': pPars->fGlucose ^= 1; break; @@ -9905,7 +9916,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutexact [-INKT ] [-iaogvh] \n" ); + Abc_Print( -2, "usage: lutexact [-INKT ] [-iaocgvh] \n" ); Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N : the number of K-input nodes [default = %d]\n", pPars->nNodes ); @@ -9914,6 +9925,7 @@ usage: Abc_Print( -2, "\t-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" ); Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" ); + Abc_Print( -2, "\t-c : toggle synthesizing a single-rail cascade [default = %s]\n", pPars->fLutCascade ? "yes" : "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" ); Abc_Print( -2, "\t-h : print the command usage\n" ); @@ -11166,7 +11178,7 @@ usage: ***********************************************************************/ int Abc_CommandAddPi( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int c; // set defaults @@ -11188,14 +11200,14 @@ int Abc_CommandAddPi( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkDup( pNtk ); - if ( Abc_NtkPiNum(pNtkRes) == 0 ) + if ( Abc_NtkPiNum(pNtk) == 0 ) { + Abc_Ntk_t * pNtkRes = Abc_NtkDup( pNtk ); Abc_Obj_t * pObj = Abc_NtkCreatePi( pNtkRes ); Abc_ObjAssignName( pObj, "dummy_pi", NULL ); Abc_NtkOrderCisCos( pNtkRes ); + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); } - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: @@ -11205,6 +11217,59 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAddFlop( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + int c; + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n"); + return 0; + } + // get the new network + if ( Abc_NtkLatchNum(pNtk) == 0 ) + { + Abc_Ntk_t * pNtkRes = Abc_NtkDup( pNtk ); + Abc_NtkAddLatch( pNtkRes, Abc_AigConst1(pNtkRes), ABC_INIT_ONE ); + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + } + return 0; + +usage: + Abc_Print( -2, "usage: addflop [-h]\n" ); + Abc_Print( -2, "\t if the network has no flops, add one dummy flop\n" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -32742,7 +32807,7 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } Abc_NtkInsertHierarchyGia( pNtkSpec, pAbc->pNtkCur, fVerbose ); - Io_WriteVerilog( pNtkSpec, pFileName, 0 ); + Io_WriteVerilog( pNtkSpec, pFileName, 0, 0 ); Abc_NtkDelete( pNtkSpec ); return 0; @@ -33904,8 +33969,9 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv ) int fAddMuxes = 0; int fStrMuxes = 0; int fRehashMap = 0; + int fInvert = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "LMbacmrsh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "LMbacmrsih" ) ) != EOF ) { switch ( c ) { @@ -33949,6 +34015,9 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': fStrMuxes ^= 1; break; + case 'i': + fInvert ^= 1; + break; case 'h': goto usage; default: @@ -33960,6 +34029,13 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Strash(): There is no AIG.\n" ); return 1; } + if ( fInvert ) + { + Gia_Obj_t * pObj; int i; + Gia_ManForEachPo( pAbc->pGia, pObj, i ) + Gia_ObjFlipFaninC0( pObj ); + return 0; + } if ( fAddBuffs ) { extern Gia_Man_t * Gia_ManDupAddBufs( Gia_Man_t * p ); @@ -34041,7 +34117,7 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &st [-LM num] [-bacmrsh]\n" ); + Abc_Print( -2, "usage: &st [-LM num] [-bacmrsih]\n" ); Abc_Print( -2, "\t performs structural hashing\n" ); Abc_Print( -2, "\t-b : toggle adding buffers at the inputs and outputs [default = %s]\n", fAddBuffs? "yes": "no" ); Abc_Print( -2, "\t-a : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" ); @@ -34052,6 +34128,7 @@ usage: Abc_Print( -2, "\t-M num : create an AIG with additional primary inputs [default = %d]\n", Multi ); Abc_Print( -2, "\t-r : toggle rehashing AIG while preserving mapping [default = %s]\n", fRehashMap? "yes": "no" ); Abc_Print( -2, "\t-s : toggle using MUX restructuring [default = %s]\n", fStrMuxes? "yes": "no" ); + Abc_Print( -2, "\t-i : toggle complementing the POs of the AIG [default = %s]\n", fInvert? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -34276,6 +34353,96 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Cofs( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManDupCofs( Gia_Man_t * p, Vec_Int_t * vVarNums ); + Gia_Man_t * pTemp; Vec_Int_t * vVars = NULL; + int c, iVar = 0, nVars = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "VNvh" ) ) != EOF ) + { + switch ( c ) + { + case 'V': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" ); + goto usage; + } + iVar = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iVar < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nVars < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Cof(): There is no AIG.\n" ); + return 1; + } + if ( iVar ) { + Abc_Print( 0, "Cofactoring one variable with ID %d.\n", iVar ); + vVars = Vec_IntAlloc( 1 ); + Vec_IntPush( vVars, iVar ); + } + else if ( nVars ) { + Abc_Print( 0, "Cofactoring the first %d inputs.\n", nVars ); + vVars = Vec_IntStartNatural( nVars ); + } + else if ( globalUtilOptind < argc ) { + vVars = Vec_IntAlloc( argc ); + for ( c = globalUtilOptind; c < argc; c++ ) + Vec_IntPush( vVars, atoi(argv[c]) ); + } + else { + Abc_Print( -1, "One of the parameters, -V or -L , should be set on the command line.\n" ); + goto usage; + } + pTemp = Gia_ManDupCofs( pAbc->pGia, vVars ); + Abc_FrameUpdateGia( pAbc, pTemp ); + Vec_IntFree( vVars ); + return 0; + +usage: + Abc_Print( -2, "usage: &cofs [-VN num] [-vh]\n" ); + Abc_Print( -2, "\t derives cofactors w.r.t the set of variables\n" ); + Abc_Print( -2, "\t-V num : the zero-based ID of one variable to cofactor [default = %d]\n", iVar ); + Abc_Print( -2, "\t-N num : cofactoring the given number of first input variables [default = %d]\n", nVars ); + 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 [] @@ -38518,6 +38685,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) Vec_Int_t * vStops = Gia_ManFindStopFlops( pAbc->pGia, nFlopIncFreq, pPars->fVerbose ); if ( vStops ) { + extern void Gia_ManTransferEquivs2( Gia_Man_t * p, Gia_Man_t * pNew ); Gia_Man_t * pUsed = Gia_ManDupStopsAdd( pAbc->pGia, vStops ); if ( pPars->nPartSize > 0 ) pTemp = Gia_SignalCorrespondencePart( pUsed, pPars ); @@ -38527,6 +38695,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) pTemp = Gia_ManScorrDivideTest( pUsed, pPars ); else pTemp = Cec_ManLSCorrespondence( pUsed, pPars ); + Gia_ManTransferEquivs2( pUsed, pAbc->pGia ); Gia_ManStop( pUsed ); pTemp = Gia_ManDupStopsRem( pUsed = pTemp, vStops ); Gia_ManStop( pUsed ); @@ -41314,7 +41483,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - + if ( pAbc->pGia == NULL ) { if ( !Abc_FrameReadFlag("silentmode") ) @@ -52862,13 +53031,16 @@ int Abc_CommandAbc9AddFlop( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9AddFlop(): There is no AIG.\n" ); return 0; } - pTemp = Gia_ManDupAddFlop( pAbc->pGia ); - Abc_FrameUpdateGia( pAbc, pTemp ); + if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + { + pTemp = Gia_ManDupAddFlop( pAbc->pGia ); + Abc_FrameUpdateGia( pAbc, pTemp ); + } return 0; usage: Abc_Print( -2, "usage: &addflop [-vh]\n" ); - Abc_Print( -2, "\t adds one flop to the design\n" ); + Abc_Print( -2, "\t if the design has no flops, adds one flop to the design\n" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -53449,17 +53621,18 @@ usage: ***********************************************************************/ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fVerbose, int fVeryVerbose ); + extern void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fBlif, int fVerbose, int fVeryVerbose ); char * pFileName = (char *)"cexes.txt"; int nMinCexes = 1; int nMaxTries = 10; int fUseSim = 1; int fUseSat = 1; int fShort = 0; + int fBlif = 0; int fVerbose = 0; int c; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CMFstcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CMFstcbvh" ) ) != EOF ) { switch ( c ) { @@ -53503,6 +53676,9 @@ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': fShort ^= 1; break; + case 'b': + fBlif ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -53517,19 +53693,20 @@ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Bmci(): There is no AIG.\n" ); return 0; } - Gia_GenerateCexes( pFileName, pAbc->pGia, nMaxTries, nMinCexes, fUseSim, fUseSat, fShort, fVerbose, 0 ); + Gia_GenerateCexes( pFileName, pAbc->pGia, nMaxTries, nMinCexes, fUseSim, fUseSat, fShort, fBlif, fVerbose, 0 ); return 0; usage: - Abc_Print( -2, "usage: &gencex [-CM num] [-F file] [-stcvh]\n" ); + Abc_Print( -2, "usage: &gencex [-CM num] [-F file] [-stcbvh]\n" ); Abc_Print( -2, "\t generates satisfying assignments for each output of the miter\n" ); Abc_Print( -2, "\t-C num : the number of timeframes [default = %d]\n", nMinCexes ); Abc_Print( -2, "\t-M num : the max simulation runs before using SAT [default = %d]\n", nMaxTries ); Abc_Print( -2, "\t-F file : the output file name [default = %s]\n", pFileName ); - Abc_Print( -2, "\t-s : toggles using reverse simulation [default = %d]\n", fUseSim ? "yes": "no" ); - Abc_Print( -2, "\t-t : toggles using SAT solving [default = %d]\n", fUseSat ? "yes": "no" ); - Abc_Print( -2, "\t-c : toggles outputing care literals only [default = %d]\n", fShort ? "yes": "no" ); - Abc_Print( -2, "\t-v : toggles printing verbose information [default = %d]\n", fVerbose ? "yes": "no" ); + Abc_Print( -2, "\t-s : toggles using reverse simulation [default = %s]\n", fUseSim ? "yes": "no" ); + Abc_Print( -2, "\t-t : toggles using SAT solving [default = %s]\n", fUseSat ? "yes": "no" ); + Abc_Print( -2, "\t-c : toggles outputing care literals only [default = %s]\n", fShort ? "yes": "no" ); + Abc_Print( -2, "\t-b : toggles outputing the BLIF file [default = %s]\n", fBlif ? "yes": "no" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -53739,36 +53916,9 @@ int Abc_CommandAbc9GenMux( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( argc == globalUtilOptind && nIns > 0 ) { - if ( nIns == 2 ) - pNums = "11"; - else if ( nIns == 3 ) - pNums = "111"; - else if ( nIns == 4 ) - pNums = "112"; - else if ( nIns == 5 ) - pNums = "113"; - else if ( nIns == 6 ) - pNums = "123"; - else if ( nIns == 7 ) - pNums = "1123"; - else if ( nIns == 8 ) - pNums = "1124"; - else if ( nIns == 9 ) - pNums = "1134"; - else if ( nIns == 10 ) - pNums = "1135"; - else if ( nIns == 11 ) - pNums = "1235"; - else if ( nIns == 12 ) - pNums = "1245"; - else if ( nIns == 13 ) - pNums = "1246"; - else if ( nIns == 14 ) - pNums = "1247"; - else if ( nIns == 15 ) - pNums = "1248"; - else if ( nIns == 16 ) - pNums = "1348"; + extern char * Wlc_NtkMuxTreeString( int nIns ); + if ( nIns <= 16 ) + pNums = Wlc_NtkMuxTreeString( nIns ); else { Abc_Print( -1, "Abc_CommandAbc9GenMux(): The number of controls should not be in the range: 2 <= n <= 16.\n" ); @@ -53808,6 +53958,154 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9GenComp( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManDupGenComp( int nBits, int fInterleave ); + Gia_Man_t * pTemp = NULL; + int c, nBits = 0, fInter = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Kivh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nBits = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nBits < 0 ) + goto usage; + break; + case 'i': + fInter ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( nBits == 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9GenComp(): The number of inputs should be defined on the command line \"-K num\".\n" ); + return 0; + } + pTemp = Gia_ManDupGenComp( nBits, fInter ); + Abc_FrameUpdateGia( pAbc, pTemp ); + if ( fVerbose ) + Abc_Print( 1, "Generated %d-bit comparator.\n", nBits ); + return 0; + +usage: + Abc_Print( -2, "usage: &gencomp [-K ] [-ivh]\n" ); + Abc_Print( -2, "\t generates the comparator\n" ); + Abc_Print( -2, "\t-K num : the number of control inputs [default = undefined]\n" ); + Abc_Print( -2, "\t-i : toggles using interleaved variable ordering [default = %s]\n", fInter ? "yes": "no" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\tstring : the sizes of control input groups\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9GenNeuron( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManGenNeuron( char * pFileName, int nIBits, int nLutSize, int fDump, int fVerbose ); + Gia_Man_t * pTemp = NULL; + int c, nBits = 0, nLutSize = 0, fDump = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "IKdvh" ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nBits = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nBits < 0 ) + goto usage; + break; + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLutSize < 0 ) + goto usage; + break; + case 'd': + fDump ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( nBits < 1 || nBits > 31 ) + { + Abc_Print( -1, "Abc_CommandAbc9GenNeuron(): The number of inputs (0 < K < 32) should be defined on the command line \"-K num\".\n" ); + return 0; + } + if ( argc != globalUtilOptind + 1 ) + { + Abc_Print( 1, "Input file is not given.\n" ); + return 0; + } + pTemp = Gia_ManGenNeuron( argv[globalUtilOptind], nBits, nLutSize, fDump, fVerbose ); + if ( fVerbose ) + printf( "Generated %d-argument neuron with %d-bit inputs and %d-bit output.\n", Gia_ManCiNum(pTemp)/nBits, nBits, Gia_ManCoNum(pTemp) ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &genneuron [-IK ] [-dvh] \n" ); + Abc_Print( -2, "\t generates the implementation of one neuron\n" ); + Abc_Print( -2, "\t-I num : the bit-width of each input [default = undefined]\n" ); + Abc_Print( -2, "\t-K num : the LUT size for logic structuring [default = undefined]\n" ); + Abc_Print( -2, "\t-d : toggles dumping RTL Verilog [default = %s]\n", fDump ? "yes": "no" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : the weights one per line followed by the bias (in hex notation)\n"); + return 1; +} /**Function************************************************************* @@ -54008,9 +54306,10 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_ManPrintDsdMatrix( Gia_Man_t * p, int iIn ); extern void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose ); - int c, iIn = -1, fDsd = 0, fAll = 0, fVerbose = 0; + extern void Gia_ManRecurDsd( Gia_Man_t * p, int fVerbose ); + int c, iIn = -1, fDsd = 0, fAll = 0, fRecur = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Vdavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Vdarvh" ) ) != EOF ) { switch ( c ) { @@ -54030,7 +54329,10 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv ) break; case 'a': fAll ^= 1; - break; + break; + case 'r': + fRecur ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -54045,16 +54347,22 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9DsdInfo(): There is no AIG.\n" ); return 0; } + if ( fRecur ) + { + Gia_ManRecurDsd( pAbc->pGia, fVerbose ); + return 0; + } if ( fDsd ) { if ( iIn == -1 ) { - Gia_ManCheckDsd( pAbc->pGia, 0, 1 ); + printf( "Function = " ); + Gia_ManCheckDsd( pAbc->pGia, 0, fVerbose ); if ( fAll ) { for ( iIn = 0; iIn < Gia_ManPiNum(pAbc->pGia); iIn++ ) for ( c = 0; c < 2; c++ ) { Gia_Man_t * pTemp = Gia_ManDupCofactorVar( pAbc->pGia, iIn, c ); - printf( "%s %2d = %d:\n", c ? " " : "Var", iIn, c ); - Gia_ManCheckDsd( pTemp, 12, 1 ); + printf( "Cof(%c=%d) = ", 'a' + iIn, c ); + Gia_ManCheckDsd( pTemp, 12, fVerbose ); Gia_ManStop( pTemp ); } } @@ -54062,14 +54370,14 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv ) } for ( c = 0; c < 2; c++ ) { Gia_Man_t * pTemp = Gia_ManDupCofactorVar( pAbc->pGia, iIn, c ); - printf( "Var %2d Cof %d:\n", iIn, c ); - Gia_ManCheckDsd( pTemp, 0, 1 ); + printf( " Cof(%c=%d) = ", 'a' + iIn, c ); + Gia_ManCheckDsd( pTemp, 0, fVerbose ); if ( fAll ) { - for ( int iIn = 0; iIn < Gia_ManPiNum(pAbc->pGia); iIn++ ) - for ( int c = 0; c < 2; c++ ) { - Gia_Man_t * pTemp2 = Gia_ManDupCofactorVar( pTemp, iIn, c ); - printf( "%s %2d = %d:\n", c ? " " : "Var", iIn, c ); - Gia_ManCheckDsd( pTemp2, 12, 1 ); + for ( int iIn2 = 0; iIn2 < Gia_ManPiNum(pAbc->pGia); iIn2++ ) if ( iIn2 != iIn ) + for ( int c2 = 0; c2 < 2; c2++ ) { + Gia_Man_t * pTemp2 = Gia_ManDupCofactorVar( pTemp, iIn2, c2 ); + printf( "Cof(%c=%d,%c=%d) = ", 'a' + iIn, c, 'a' + iIn2, c2 ); + Gia_ManCheckDsd( pTemp2, 12, fVerbose ); Gia_ManStop( pTemp2 ); } } @@ -54086,10 +54394,11 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &dsdinfo [-V num] [-dvh]\n" ); + Abc_Print( -2, "usage: &dsdinfo [-V num] [-drvh]\n" ); Abc_Print( -2, "\t computes and displays information related to DSD\n" ); Abc_Print( -2, "\t-V num : the zero-based index of the input variable [default = %d]\n", iIn ); Abc_Print( -2, "\t-d : toggles showing DSD structure [default = %s]\n", fDsd ? "yes": "no" ); + Abc_Print( -2, "\t-r : toggles recursive cofactoring to get a full DSD [default = %s]\n", fRecur ? "yes": "no" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -54111,10 +54420,12 @@ int Abc_CommandAbc9FunTrace( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Vec_Mem_t * Dau_CollectNpnFunctions( word * p, int nVars, int fVerbose ); extern void Gia_ManMatchCuts( Vec_Mem_t * vTtMem, Gia_Man_t * pGia, int nCutSize, int nCutNum, int fVerbose ); - int c, nVars, nVars2, nCutNum = 8, fVerbose = 0; word * pTruth = NULL; - char * pStr = NULL; Vec_Mem_t * vTtMem = NULL; + extern Vec_Mem_t * Abc_TruthDecRead( char * pFileName, int nVarNum ); + extern void Abc_TtStoreDump( char * pFileName, Vec_Mem_t * vTtMem, int nBytes ); + int c, nVars, nVars2, nCutNum = 8, nCutSize = 0, nNumFuncs = 5, nNumCones = 3, fOutputs = 0, fVerbose = 0; word * pTruth = NULL; + char * pStr = NULL, * pFuncFileName = "_npn_member_funcs_.data"; Vec_Mem_t * vTtMem = NULL; Gia_Man_t * pTemp; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CKNMFovh" ) ) != EOF ) { switch ( c ) { @@ -54129,6 +54440,51 @@ int Abc_CommandAbc9FunTrace( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nCutNum < 0 ) goto usage; break; + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nCutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCutSize < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nNumFuncs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nNumFuncs < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + nNumCones = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nNumCones < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" ); + goto usage; + } + pFuncFileName = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'o': + fOutputs ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -54143,9 +54499,53 @@ int Abc_CommandAbc9FunTrace( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9FunTrace(): There is no AIG.\n" ); return 0; } - if ( argc != globalUtilOptind + 1 ) + if ( argc == globalUtilOptind ) { - Abc_Print( -1, "Abc_CommandAbc9FunTrace(): Truth table in hex notation should be given on the command line.\n" ); + abctime clkStart = Abc_Clock(); + int nFileSize = Gia_FileSize( pFuncFileName ); + if ( nFileSize == 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9FunTrace(): Truth table in hex notation (or file name with the functions) should be given on the command line.\n" ); + return 0; + } + if ( nCutSize == 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9FunTrace(): The cut size needs to be specified on the command line (-K ) when precomputed functions are used.\n" ); + return 0; + } + vTtMem = Abc_TruthDecRead( pFuncFileName, nCutSize ); + printf( "Finished reading %d %d-input function from file \"%s\". ", nFileSize / 8 / Abc_Truth6WordNum(nCutSize), nCutSize, pFuncFileName ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); + Gia_ManMatchCuts( vTtMem, pAbc->pGia, nCutSize, nCutNum, fVerbose ); + Vec_MemHashFree( vTtMem ); + Vec_MemFree( vTtMem ); + return 0; + } + if ( strstr(argv[globalUtilOptind], ".aig") ) + { // the entry on the command line is an AIGER file + extern void Gia_ManMatchCones( Gia_Man_t * pBig, Gia_Man_t * pSmall, int nCutSize, int nCutNum, int nNumFuncs, int nNumCones, int fVerbose ); + extern void Gia_ManMatchConesOutput( Gia_Man_t * pBig, Gia_Man_t * pSmall, int nCutNum, int fVerbose ); + pTemp = Gia_AigerRead( argv[globalUtilOptind], 0, 0, 0 ); + if ( pTemp == NULL ) { + Abc_Print( -1, "Abc_CommandAbc9FunTrace(): Cannot read input AIG \"%s\".\n", argv[globalUtilOptind] ); + return 0; + } + if ( fOutputs ) { + if ( Gia_ManCiNum(pTemp) > 16 ) { + Abc_Print( -1, "Abc_CommandAbc9FunTrace(): The AIG \"%s\" has more than 16 primary inputs.\n", argv[globalUtilOptind] ); + Gia_ManStop( pTemp ); + return 0; + } + Gia_ManMatchConesOutput( pAbc->pGia, pTemp, nCutNum, fVerbose ); + } + else { + if ( nCutSize == 0 ) { + Abc_Print( -1, "Abc_CommandAbc9FunTrace(): The LUT size for profiling should be given on the command line.\n" ); + return 0; + } + Gia_ManMatchCones( pAbc->pGia, pTemp, nCutSize, nCutNum, nNumFuncs, nNumCones, fVerbose ); + } + Gia_ManStop( pTemp ); return 0; } pStr = argv[globalUtilOptind]; @@ -54168,17 +54568,27 @@ int Abc_CommandAbc9FunTrace( Abc_Frame_t * pAbc, int argc, char ** argv ) //Abc_TtPrintHexRev( stdout, pTruth, nVars ); printf( "\n" ); vTtMem = Dau_CollectNpnFunctions( pTruth, nVars, fVerbose ); Gia_ManMatchCuts( vTtMem, pAbc->pGia, nVars, nCutNum, fVerbose ); + if ( pFuncFileName ) { + Abc_TtStoreDump( pFuncFileName, vTtMem, 8 * Vec_MemEntrySize(vTtMem) ); + printf( "Dumped %d NPN class member functions into file \"%s\".\n", Vec_MemEntryNum(vTtMem), pFuncFileName ); + } Vec_MemHashFree( vTtMem ); Vec_MemFree( vTtMem ); return 0; usage: - Abc_Print( -2, "usage: &funtrace [-C num] [-vh] \n" ); + Abc_Print( -2, "usage: &funtrace [-CKNM num] [-F file] [-ovh] { or }\n" ); Abc_Print( -2, "\t traces the presence of the function in the current AIG\n" ); Abc_Print( -2, "\t-C num : the number of cuts to compute at each node [default = %d]\n", nCutNum ); + Abc_Print( -2, "\t-K num : the LUT size to use when is given [default = %d]\n", nCutSize ); + Abc_Print( -2, "\t-N num : the number of functions to use when or -F are used [default = %d]\n", nNumFuncs ); + Abc_Print( -2, "\t-M num : the number of logic cones to use when is given [default = %d]\n", nNumCones ); + Abc_Print( -2, "\t-F file : the file name to store the NPN member functions [default = %s]\n", pFuncFileName ); + Abc_Print( -2, "\t-o : toggles using AIG output functions instead of frequent cut functions [default = %s]\n", fOutputs ? "yes": "no" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); - Abc_Print( -2, "\t : truth table in the hexadecimal notation\n"); + Abc_Print( -2, "\t : truth table in the hexadecimal notation used for tracing\n"); + Abc_Print( -2, "\t : AIG whose K-input functions will be used for tracing\n"); return 1; } diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c index 7803f539b..62d58fbca 100644 --- a/src/base/abci/abcDec.c +++ b/src/base/abci/abcDec.c @@ -458,6 +458,31 @@ void Abc_TtStoreLoadSave( char * pFileName ) printf( "Input file \"%s\" was copied into output file \"%s\".\n", pFileInput, pFileOutput ); } +/**Function************************************************************* + + Synopsis [Read truth tables from input file and write them into output file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_TtStoreDump( char * pFileName, Vec_Mem_t * vTtMem, int nBytes ) +{ + word * pTruth; int i; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return; + } + Vec_MemForEachEntry( vTtMem, pTruth, i ) + fwrite( pTruth, nBytes, 1, pFile ); + fclose( pFile ); +} + /**Function************************************************************* Synopsis [Read truth tables in binary text form and write them into file as binary data.] @@ -709,6 +734,38 @@ void Abc_TruthDecTest( char * pFileName, int DecType, int nVarNum, int fVerbose // printf( "Finished decomposing truth tables from file \"%s\".\n", pFileName ); } +/**Function************************************************************* + + Synopsis [Read truth tables from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Mem_t * Abc_TruthDecRead( char * pFileName, int nVarNum ) +{ + Abc_TtStore_t * p; int i; + if ( nVarNum < 6 ) + nVarNum = 6; + + // allocate data-structure + p = Abc_TtStoreLoad( pFileName, nVarNum ); + if ( p == NULL ) return NULL; + + // consider functions from the file + Vec_Mem_t * vTtMem = Vec_MemAllocForTTSimple( nVarNum ); + for ( i = 0; i < p->nFuncs; i++ ) + Vec_MemHashInsert( vTtMem, (word *)p->pFuncs[i] ); + + // delete data-structure + Abc_TtStoreFree( p, nVarNum ); +// printf( "Finished decomposing truth tables from file \"%s\".\n", pFileName ); + return vTtMem; +} + /**Function************************************************************* diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c index 487aee3c6..c69d6b887 100644 --- a/src/base/abci/abcFx.c +++ b/src/base/abci/abcFx.c @@ -287,8 +287,11 @@ int Abc_NtkFxCheck( Abc_Ntk_t * pNtk ) // Abc_NtkForEachObj( pNtk, pNode, i ) // Abc_ObjPrint( stdout, pNode ); Abc_NtkForEachNode( pNtk, pNode, i ) - if ( !Vec_IntCheckUniqueSmall( &pNode->vFanins ) ) + if ( !Vec_IntCheckUniqueSmall( &pNode->vFanins ) ) { + printf( "Fanins of node %d: ", i ); + Vec_IntPrint( &pNode->vFanins ); return 0; + } return 1; } diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index 803b88e91..cb22e8a60 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -170,6 +170,8 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nMinS pManRes->nNodesBeg = Abc_NtkNodeNum(pNtk); nNodes = Abc_NtkObjNumMax(pNtk); pProgress = Extra_ProgressBarStart( stdout, nNodes ); + //clear markAB at the beginning + Abc_NtkCleanMarkAB( pNtk ); Abc_NtkForEachNode( pNtk, pNode, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); diff --git a/src/base/io/io.c b/src/base/io/io.c index 8f805d639..3327a9dfd 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -59,6 +59,7 @@ static int IoCommandReadStatus ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadGig ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadJson ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadSF ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandReadRom ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWrite ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteHie ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -133,6 +134,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "&read_gig", IoCommandReadGig, 0 ); Cmd_CommandAdd( pAbc, "I/O", "read_json", IoCommandReadJson, 0 ); Cmd_CommandAdd( pAbc, "I/O", "read_sf", IoCommandReadSF, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "read_rom", IoCommandReadRom, 1 ); Cmd_CommandAdd( pAbc, "I/O", "write", IoCommandWrite, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_hie", IoCommandWriteHie, 0 ); @@ -1927,6 +1929,73 @@ usage: } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandReadRom( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Io_TransformROM2PLA( char * pNameIn, char * pNameOut ); + + Abc_Ntk_t * pNtk; + FILE * pFile; + char * pFileName, * pFileTemp = "_temp_rom_.pla"; + int c; + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + { + goto usage; + } + + // get the input file name + pFileName = argv[globalUtilOptind]; + if ( (pFile = fopen( pFileName, "r" )) == NULL ) + { + fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName ); + return 1; + } + fclose( pFile ); + Io_TransformROM2PLA( pFileName, pFileTemp ); + pNtk = Io_Read( pFileTemp, IO_FILE_PLA, 1, 0 ); + //unlink( pFileTemp ); + if ( pNtk == NULL ) + return 1; + ABC_FREE( pNtk->pName ); + pNtk->pName = Extra_FileNameGeneric( pFileName ); + ABC_FREE( pNtk->pSpec ); + pNtk->pSpec = Abc_UtilStrsav( pFileName ); + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); + Abc_FrameClearVerifStatus( pAbc ); + + return 0; + +usage: + fprintf( pAbc->Err, "usage: read_rom [-h] \n" ); + fprintf( pAbc->Err, "\t reads ROM file\n" ); + fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); + fprintf( pAbc->Err, "\tfile : the name of a file to read\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -3530,13 +3599,13 @@ usage: ***********************************************************************/ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv ) { - extern void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules ); + extern void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules, int fNewInterface ); char * pFileName; - int c, fFixed = 0, fOnlyAnds = 0, fNoModules = 0; + int c, fFixed = 0, fOnlyAnds = 0, fNoModules = 0, fNewInterface = 0; int nLutSize = -1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Kfamh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Kfamnh" ) ) != EOF ) { switch ( c ) { @@ -3560,6 +3629,9 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv ) case 'm': fNoModules ^= 1; break; + case 'n': + fNewInterface ^= 1; + break; case 'h': goto usage; default: @@ -3578,27 +3650,26 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv ) // get the output file name pFileName = argv[globalUtilOptind]; // call the corresponding file writer - if ( fOnlyAnds ) + if ( nLutSize >= 2 && nLutSize <= 6 ) + Io_WriteVerilogLut( pAbc->pNtkCur, pFileName, nLutSize, fFixed, fNoModules, fNewInterface ); + else { Abc_Ntk_t * pNtkTemp = Abc_NtkToNetlist( pAbc->pNtkCur ); if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) ) Abc_NtkToAig( pNtkTemp ); - Io_WriteVerilog( pNtkTemp, pFileName, 1 ); + Io_WriteVerilog( pNtkTemp, pFileName, fOnlyAnds, fNewInterface ); Abc_NtkDelete( pNtkTemp ); } - else if ( nLutSize >= 2 && nLutSize <= 6 ) - Io_WriteVerilogLut( pAbc->pNtkCur, pFileName, nLutSize, fFixed, fNoModules ); - else - Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_VERILOG ); return 0; usage: - fprintf( pAbc->Err, "usage: write_verilog [-K num] [-famh] \n" ); + fprintf( pAbc->Err, "usage: write_verilog [-K num] [-famnh] \n" ); fprintf( pAbc->Err, "\t writes the current network in Verilog format\n" ); fprintf( pAbc->Err, "\t-K num : write the network using instances of K-LUTs (2 <= K <= 6) [default = not used]\n" ); fprintf( pAbc->Err, "\t-f : toggle using fixed format [default = %s]\n", fFixed? "yes":"no" ); fprintf( pAbc->Err, "\t-a : toggle writing expressions with only ANDs (without XORs and MUXes) [default = %s]\n", fOnlyAnds? "yes":"no" ); fprintf( pAbc->Err, "\t-m : toggle writing additional modules [default = %s]\n", !fNoModules? "yes":"no" ); + fprintf( pAbc->Err, "\t-n : toggle writing generic PO names and assign-statements [default = %s]\n", fNewInterface? "yes":"no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); return 1; diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h index 9a0d82098..cf30196f2 100644 --- a/src/base/io/ioAbc.h +++ b/src/base/io/ioAbc.h @@ -137,7 +137,7 @@ extern int Io_WriteMoPla( Abc_Ntk_t * pNtk, char * FileName ); /*=== abcWriteSmv.c ===========================================================*/ extern int Io_WriteSmv( Abc_Ntk_t * pNtk, char * FileName ); /*=== abcWriteVerilog.c =======================================================*/ -extern void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName, int fOnlyAnds ); +extern void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName, int fOnlyAnds, int fNewInterface ); /*=== abcUtil.c ===============================================================*/ extern Io_FileType_t Io_ReadFileType( char * pFileName ); extern Io_FileType_t Io_ReadLibType( char * pFileName ); diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index eee2dda53..52cadc274 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -20,6 +20,7 @@ #include "ioAbc.h" #include "base/main/main.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -464,7 +465,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) { if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) ) Abc_NtkToAig( pNtkTemp ); - Io_WriteVerilog( pNtkTemp, pFileName, 0 ); + Io_WriteVerilog( pNtkTemp, pFileName, 0, 0 ); } else fprintf( stderr, "Unknown file format.\n" ); @@ -592,7 +593,7 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName ) if ( !Abc_NtkHasAig(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) ) Abc_NtkToAig( pNtkResult ); } - Io_WriteVerilog( pNtkResult, pFileName, 0 ); + Io_WriteVerilog( pNtkResult, pFileName, 0, 0 ); } else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV ) { @@ -890,7 +891,7 @@ void Io_TransformSF2PLA( char * pNameIn, char * pNameOut ) if ( pFileOut == NULL ) { if ( pFileIn ) fclose( pFileIn ); - printf( "Cannot open file \"%s\" for reading.\n", pNameOut ); + printf( "Cannot open file \"%s\" for writing.\n", pNameOut ); return; } pBuffer = ABC_ALLOC( char, Size ); @@ -920,6 +921,58 @@ void Io_TransformSF2PLA( char * pNameIn, char * pNameOut ) ABC_FREE( pBuffer ); } +/**Function************************************************************* + + Synopsis [Tranform SF into PLA.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_TransformROM2PLA( char * pNameIn, char * pNameOut ) +{ + FILE * pFileOut = fopen( pNameOut, "wb" ); + if ( pFileOut == NULL ) { + printf( "Cannot open file \"%s\" for writing.\n", pNameOut ); + return; + } + int nWords = -1; + Vec_Wrd_t * vData = Vec_WrdReadHex( pNameIn, &nWords, 0 ); + if ( vData == NULL ) { + fclose( pFileOut ); + return; + } + //Vec_WrdDumpHex( "temp.txt", vData, 1, 1 ); + int v, i, nLines = Vec_WrdSize(vData) / nWords; + int nIns = Abc_Base2Log(nLines), nOuts; + assert( nLines * nWords == Vec_WrdSize(vData) ); + word * pTemp = ABC_CALLOC( word, nWords ); + for ( i = 0; i < nLines; i++ ) + Abc_TtOr( pTemp, pTemp, Vec_WrdEntryP(vData, nWords*i), nWords ); + for ( nOuts = nWords*64; nOuts > 0; nOuts-- ) + if ( Abc_TtGetBit(pTemp, nOuts-1) ) + break; + ABC_FREE( pTemp ); + assert( nOuts > 0 ); + fprintf( pFileOut, ".i %d\n", nIns ); + fprintf( pFileOut, ".o %d\n", nOuts ); + fprintf( pFileOut, ".p %d\n", nLines ); + fprintf( pFileOut, ".type fr\n" ); + for ( i = 0; i < nLines; i++ ) { + word * pData = Vec_WrdEntryP(vData, nWords*i); + for ( v = 0; v < nIns; v++ ) + fprintf( pFileOut, "%d", (i >> v) & 1 ); + fprintf( pFileOut, " " ); + for ( v = 0; v < nOuts; v++ ) + fprintf( pFileOut, "%d", Abc_TtGetBit(pData, v) ); + fprintf( pFileOut, "\n" ); + } + fprintf( pFileOut, ".e\n\n" ); + fclose( pFileOut ); +} /**Function************************************************************* Synopsis [Reads CNF from file.] diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c index 5e4438a5d..acddb7551 100644 --- a/src/base/io/ioWriteVerilog.c +++ b/src/base/io/ioWriteVerilog.c @@ -29,9 +29,10 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds ); +static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds, int fNewInterface ); static void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start ); -static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start ); +static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start, int fNewInterface ); +static void Io_WriteVerilogAssigns( FILE * pFile, Abc_Ntk_t * pNtk ); static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ); static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start ); static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk ); @@ -54,11 +55,12 @@ static char * Io_WriteVerilogGetName( char * pName ); SeeAlso [] ***********************************************************************/ -void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fOnlyAnds ) +void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fOnlyAnds, int fNewInterface ) { Abc_Ntk_t * pNetlist; FILE * pFile; int i; + // can only write nodes represented using local AIGs if ( !Abc_NtkIsAigNetlist(pNtk) && !Abc_NtkIsMappedNetlist(pNtk) ) { @@ -81,7 +83,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fOnlyAnds ) if ( pNtk->pDesign ) { // write the network first - Io_WriteVerilogInt( pFile, pNtk, fOnlyAnds ); + Io_WriteVerilogInt( pFile, pNtk, fOnlyAnds, fNewInterface ); // write other things Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pNetlist, i ) { @@ -89,12 +91,12 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fOnlyAnds ) if ( pNetlist == pNtk ) continue; fprintf( pFile, "\n" ); - Io_WriteVerilogInt( pFile, pNetlist, fOnlyAnds ); + Io_WriteVerilogInt( pFile, pNetlist, fOnlyAnds, fNewInterface ); } } else { - Io_WriteVerilogInt( pFile, pNtk, fOnlyAnds ); + Io_WriteVerilogInt( pFile, pNtk, fOnlyAnds, fNewInterface ); } fprintf( pFile, "\n" ); @@ -112,7 +114,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fOnlyAnds ) SeeAlso [] ***********************************************************************/ -void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds ) +void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds, int fNewInterface ) { // write inputs and outputs // fprintf( pFile, "module %s ( gclk,\n ", Abc_NtkName(pNtk) ); @@ -128,7 +130,7 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds ) fprintf( pFile, ",\n " ); } if ( Abc_NtkPoNum(pNtk) > 0 ) - Io_WriteVerilogPos( pFile, pNtk, 3 ); + Io_WriteVerilogPos( pFile, pNtk, 3, fNewInterface ); fprintf( pFile, " );\n" ); // add the clock signal if it does not exist if ( Abc_NtkLatchNum(pNtk) > 0 && Nm_ManFindIdByName(pNtk->pManName, "clock", ABC_OBJ_PI) == -1 ) @@ -144,7 +146,7 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds ) if ( Abc_NtkPoNum(pNtk) > 0 ) { fprintf( pFile, " output" ); - Io_WriteVerilogPos( pFile, pNtk, 5 ); + Io_WriteVerilogPos( pFile, pNtk, 5, fNewInterface ); fprintf( pFile, ";\n" ); } // if this is not a blackbox, write internal signals @@ -168,6 +170,8 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds ) if ( Abc_NtkLatchNum(pNtk) > 0 ) Io_WriteVerilogLatches( pFile, pNtk ); } + if ( fNewInterface ) + Io_WriteVerilogAssigns( pFile, pNtk ); // finalize the file fprintf( pFile, "endmodule\n\n" ); } @@ -222,9 +226,10 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) SeeAlso [] ***********************************************************************/ -void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) +void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start, int fNewInterface ) { Abc_Obj_t * pTerm, * pNet, * pSkip; + char Name[100], * pName = Name; int LineLength; int AddedLength; int NameCounter; @@ -252,7 +257,11 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) } // get the line length after this name is written - AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2; + if ( fNewInterface ) + sprintf( Name, "po_username%d", i ); + else + pName = Abc_ObjName(pNet); + AddedLength = strlen(Io_WriteVerilogGetName(pName)) + 2; if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) { // write the line extender fprintf( pFile, "\n " ); @@ -260,7 +269,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) LineLength = 3; NameCounter = 0; } - fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," ); + fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pName), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," ); LineLength += AddedLength; NameCounter++; } @@ -274,6 +283,37 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) } +/**Function************************************************************* + + Synopsis [Writes the primary outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteVerilogAssigns( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pTerm, * pNet, * pSkip; + int i; + Abc_NtkForEachPo( pNtk, pTerm, i ) + { + pNet = Abc_ObjFanin0(pTerm); + if ( Abc_ObjIsPi(Abc_ObjFanin0(pNet)) ) + { + // Skip this output since it is a feedthrough -- the same + // name will appear as an input and an output which other + // tools reading verilog do not like. + + pSkip = pNet; // save an example of skipped net + continue; + } + fprintf( pFile, " assign po_username%d = %s;\n", i, Abc_ObjName(pNet) ); + } +} + /**Function************************************************************* Synopsis [Writes the wires.] @@ -816,7 +856,7 @@ void Io_WriteVerilogObjectsLut( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, in fprintf( pFile, "}, %*s );\n", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) ); } } -void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fFixed ) +void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fFixed, int fNewInterface ) { // write inputs and outputs // fprintf( pFile, "module %s ( gclk,\n ", Abc_NtkName(pNtk) ); @@ -832,7 +872,7 @@ void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fF fprintf( pFile, ",\n " ); } if ( Abc_NtkPoNum(pNtk) > 0 ) - Io_WriteVerilogPos( pFile, pNtk, 3 ); + Io_WriteVerilogPos( pFile, pNtk, 3, fNewInterface ); fprintf( pFile, " );\n\n" ); // add the clock signal if it does not exist if ( Abc_NtkLatchNum(pNtk) > 0 && Nm_ManFindIdByName(pNtk->pManName, "clock", ABC_OBJ_PI) == -1 ) @@ -848,7 +888,7 @@ void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fF if ( Abc_NtkPoNum(pNtk) > 0 ) { fprintf( pFile, " output" ); - Io_WriteVerilogPos( pFile, pNtk, 5 ); + Io_WriteVerilogPos( pFile, pNtk, 5, fNewInterface ); fprintf( pFile, ";\n\n" ); } // if this is not a blackbox, write internal signals @@ -875,10 +915,12 @@ void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fF Io_WriteVerilogLatches( pFile, pNtk ); } } + if ( fNewInterface ) + Io_WriteVerilogAssigns( pFile, pNtk ); // finalize the file fprintf( pFile, "\nendmodule\n\n" ); } -void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules ) +void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules, int fNewInterface ) { FILE * pFile; Abc_Ntk_t * pNtkTemp; @@ -917,7 +959,7 @@ void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int f } pNtkTemp = Abc_NtkToNetlist( pNtk ); Abc_NtkToSop( pNtkTemp, -1, ABC_INFINITY ); - Io_WriteVerilogLutInt( pFile, pNtkTemp, nLutSize, fFixed ); + Io_WriteVerilogLutInt( pFile, pNtkTemp, nLutSize, fFixed, fNewInterface ); Abc_NtkDelete( pNtkTemp ); fprintf( pFile, "\n" ); diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index ac4743338..715b3c29f 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -223,6 +223,7 @@ struct Wlc_BstPar_t_ int fCreateWordMiter; int fDecMuxes; int fSaveFfNames; + int fBlastNew; int fVerbose; Vec_Int_t * vBoxIds; }; diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 2e419d344..271b52d99 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -20,6 +20,8 @@ #include "wlc.h" #include "misc/tim/tim.h" +#include "base/main/main.h" +#include "base/cmd/cmd.h" ABC_NAMESPACE_IMPL_START @@ -131,6 +133,61 @@ int Wlc_NtkMuxTree2( Gia_Man_t * pNew, int * pCtrl, int nCtrl, Vec_Int_t * vData Vec_IntPush( vTemp, Abc_LitNot( Gia_ManHashAnd(pNew, iLit, Vec_IntEntry(vData, m)) ) ); return Abc_LitNot( Gia_ManHashAndMulti(pNew, vTemp) ); } +int Wlc_NtkMuxTree3( Gia_Man_t * p, Vec_Int_t * vData, char * pNums, Vec_Int_t ** pvDecs ) +{ + int i, iStart = 0, nSize = Vec_IntSize(vData); + for ( i = (int)strlen(pNums)-1; i >= 0; i-- ) + { + int k, b, nBits = (int)(pNums[i] - '0'); + Vec_Int_t * vDec = pvDecs[i]; + for ( k = 0; k < nSize; k++ ) + Vec_IntWriteEntry( vData, k, Gia_ManHashAnd(p, Vec_IntEntry(vData, k), Vec_IntEntry(vDec, k%Vec_IntSize(vDec))) ); + for ( b = 0; b < nBits; b++, nSize /= 2 ) + for ( k = 0; k < nSize/2; k++ ) + Vec_IntWriteEntry( vData, k, Gia_ManHashOr(p, Vec_IntEntry(vData, 2*k), Vec_IntEntry(vData, 2*k+1)) ); + iStart += nBits; + } + assert( nSize == 1 ); + return Vec_IntEntry(vData, 0); +} +Vec_Int_t ** Wlc_NtkMuxTree3DecsDerive( Gia_Man_t * p, int * pIns, int nIns, char * pNums ) +{ + extern Vec_Int_t * Wlc_BlastDecoder2_rec( Gia_Man_t * p, int * pLits, int nLits ); + Vec_Int_t ** pvDecs = ABC_ALLOC( Vec_Int_t *, strlen(pNums) ); int i, iStart = 0; + for ( i = (int)strlen(pNums)-1; i >= 0; i-- ) { + pvDecs[i] = Wlc_BlastDecoder2_rec( p, pIns + iStart, (int)(pNums[i] - '0') ); + iStart += (int)(pNums[i] - '0'); + } + assert( iStart == nIns ); + return pvDecs; +} +void Wlc_NtkMuxTree3DecsFree( Vec_Int_t ** pvDecs, char * pNums ) +{ + int i; + for ( i = (int)strlen(pNums)-1; i >= 0; i-- ) + Vec_IntFree( pvDecs[i] ); + ABC_FREE( pvDecs ); +} +char * Wlc_NtkMuxTreeString( int nIns ) +{ + if ( nIns == 1 ) return (char*)"1"; + if ( nIns == 2 ) return (char*)"11"; + if ( nIns == 3 ) return (char*)"111"; + if ( nIns == 4 ) return (char*)"112"; + if ( nIns == 5 ) return (char*)"1112"; + if ( nIns == 6 ) return (char*)"1113"; + if ( nIns == 7 ) return (char*)"1114"; + if ( nIns == 8 ) return (char*)"1124"; + if ( nIns == 9 ) return (char*)"11124"; + if ( nIns == 10 ) return (char*)"11125"; + if ( nIns == 11 ) return (char*)"11126"; + if ( nIns == 12 ) return (char*)"11136"; + if ( nIns == 13 ) return (char*)"11137"; + if ( nIns == 14 ) return (char*)"11147"; + if ( nIns == 15 ) return (char*)"11148"; + if ( nIns == 16 ) return (char*)"11248"; + return NULL; +} void Wlc_NtkPrintNameArray( Vec_Ptr_t * vNames ) { int i; char * pTemp; @@ -317,6 +374,30 @@ int Wlc_BlastLessSigned( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits ) int iDiffSign = Gia_ManHashXor( pNew, pArg0[nBits-1], pArg1[nBits-1] ); return Gia_ManHashMux( pNew, iDiffSign, pArg0[nBits-1], Wlc_BlastLess(pNew, pArg0, pArg1, nBits-1) ); } +int Wlc_BlastLess3( Gia_Man_t * p, int * pArg1, int * pArg0, int nBits ) +{ + int i, iLit = 1; + for ( i = 0; i < nBits; i++ ) { + int iLitA0 = pArg0[i]; + int iLitA1 = i == nBits-1 ? 0 : pArg0[i+1]; + int iLitB0 = pArg1[i]; + int iLitB1 = i == nBits-1 ? 0 : pArg1[i+1]; + int iOrLit0; + if ( i == 0 ) + iOrLit0 = Gia_ManHashOr(p, Abc_LitNotCond(iLitA0, !(i&1)), Abc_LitNotCond(iLitB0, i&1)); + else + iOrLit0 = Gia_ManHashAnd(p, Abc_LitNotCond(iLitA0, !(i&1)), Abc_LitNotCond(iLitB0, i&1)); + int iOrLit1 = Gia_ManHashAnd(p, Abc_LitNotCond(iLitA1, !(i&1)), Abc_LitNotCond(iLitB1, i&1)); + int iOrLit = Gia_ManHashOr(p, iOrLit0, iOrLit1 ); + iLit = Gia_ManHashOr(p, Abc_LitNot(iLit), iOrLit ); + } + return Abc_LitNotCond(iLit, nBits&1); +} +int Wlc_BlastLessSigned3( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits ) +{ + int iDiffSign = Gia_ManHashXor( pNew, pArg0[nBits-1], pArg1[nBits-1] ); + return Gia_ManHashMux( pNew, iDiffSign, pArg0[nBits-1], Wlc_BlastLess3(pNew, pArg0, pArg1, nBits-1) ); +} void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps ) { int fUseXor = 0; @@ -1127,6 +1208,37 @@ void Wlc_BlastDecoder( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vTmp, Vec_IntPush( vRes, iMint ); } } +Vec_Int_t * Wlc_BlastDecoder2_rec( Gia_Man_t * p, int * pLits, int nLits ) +{ + if ( nLits == 1 ) + { + Vec_Int_t * vRes = Vec_IntAlloc( 2 ); + Vec_IntPush( vRes, Abc_LitNot(pLits[0]) ); + Vec_IntPush( vRes, pLits[0] ); + return vRes; + } + assert( nLits > 1 ); + int nPart1 = nLits / 2; + int nPart2 = nLits - nPart1; + Vec_Int_t * vRes1 = Wlc_BlastDecoder2_rec( p, pLits, nPart1 ); + Vec_Int_t * vRes2 = Wlc_BlastDecoder2_rec( p, pLits+nPart1, nPart2 ); + Vec_Int_t * vRes = Vec_IntAlloc( Vec_IntSize(vRes1) * Vec_IntSize(vRes2) ); + int i, k, Lit1, Lit2; + Vec_IntForEachEntry( vRes2, Lit2, k ) + Vec_IntForEachEntry( vRes1, Lit1, i ) + Vec_IntPush( vRes, Gia_ManHashAnd(p, Lit1, Lit2) ); + Vec_IntFree( vRes1 ); + Vec_IntFree( vRes2 ); + return vRes; +} +Vec_Int_t * Wlc_BlastDecoder2( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vTmp, Vec_Int_t * vRes ) +{ + Vec_Int_t * vRes2 = Wlc_BlastDecoder2_rec( pNew, pNum, nNum ); + Vec_IntClear( vRes ); + Vec_IntAppend( vRes, vRes2 ); + Vec_IntFree( vRes2 ); + return vRes; +} void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds, int fVerbose ) { Vec_Wec_t * vProds = Vec_WecStart( nArgA + nArgB + 3 ); @@ -1162,6 +1274,7 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int int Prev = i ? pArgA[i-1] : 0; int Part = Gia_ManHashOr( pNew, Gia_ManHashAnd(pNew, One, This), Gia_ManHashAnd(pNew, Two, Prev) ); pp = Gia_ManHashXor( pNew, Part, Neg ); + if ( fVerbose ) printf( "%4d = PP(%5d %5d %5d %5d %5d)\n", pp, Prev, This, Q2jM1, Q2j, Q2jP1 ); if ( pp == 0 || (fSigned && i == nArgA) ) continue; if ( pp ) @@ -1208,6 +1321,8 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int //Vec_WecShrink( vLevels, nArgA + nArgB ); if ( fVerbose ) Vec_WecPrint( vProds, 0 ); + if ( fVerbose ) + printf( "Total PPs = %d.\n", Vec_WecSizeSize(vProds) ); //Wlc_BlastPrintMatrix( pNew, vProds, 1 ); //printf( "Cutoff ID for partial products = %d.\n", Gia_ManObjNum(pNew) ); if ( pvProds ) @@ -1548,34 +1663,60 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) Wlc_ObjForEachFanin( pObj, iFanin, k ) if ( k > 0 ) fSigned &= Wlc_NtkObj(p, iFanin)->Signed; - Vec_IntClear( vTemp1 ); - if ( pPar->fDecMuxes ) + if ( pParIn->fBlastNew && nRange0 <= 16 ) { - for ( k = 0; k < (1 << nRange0); k++ ) + char * pNums = Wlc_NtkMuxTreeString( nRange0 ); + Vec_Int_t ** pvDecs = Wlc_NtkMuxTree3DecsDerive( pNew, pFans0, nRange0, pNums ); + for ( b = 0; b < nRange; b++ ) { - int iLitAnd = 1; - for ( b = 0; b < nRange0; b++ ) - iLitAnd = Gia_ManHashAnd( pNew, iLitAnd, Abc_LitNotCond(pFans0[b], ((k >> b) & 1) == 0) ); - Vec_IntPush( vTemp1, iLitAnd ); - } - } - for ( b = 0; b < nRange; b++ ) - { - Vec_IntClear( vTemp0 ); - Wlc_ObjForEachFanin( pObj, iFanin, k ) - if ( k > 0 ) - { - nRange1 = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) ); - pFans1 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, iFanin) ); - if ( Wlc_ObjFaninNum(pObj) == 3 ) // Statement 1 - Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (fSigned? pFans1[nRange1-1] : 0) ); - else // Statement 2 - Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (Wlc_NtkObj(p, iFanin)->Signed? pFans1[nRange1-1] : 0) ); + Vec_IntClear( vTemp0 ); + Wlc_ObjForEachFanin( pObj, iFanin, k ) { + if ( k > 0 ) + { + nRange1 = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) ); + pFans1 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, iFanin) ); + if ( Wlc_ObjFaninNum(pObj) == 3 ) // Statement 1 + Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (fSigned? pFans1[nRange1-1] : 0) ); + else // Statement 2 + Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (Wlc_NtkObj(p, iFanin)->Signed? pFans1[nRange1-1] : 0) ); + } } + assert( (1 << nRange0) == Vec_IntSize(vTemp0) ); + Vec_IntPush( vRes, Wlc_NtkMuxTree3(pNew, vTemp0, pNums, pvDecs) ); + } + Wlc_NtkMuxTree3DecsFree( pvDecs, pNums ); + } + else + { + Vec_IntClear( vTemp1 ); if ( pPar->fDecMuxes ) - Vec_IntPush( vRes, Wlc_NtkMuxTree2(pNew, pFans0, nRange0, vTemp0, vTemp1, vTemp2) ); - else - Vec_IntPush( vRes, Wlc_NtkMuxTree_rec(pNew, pFans0, nRange0, vTemp0, 0) ); + { + for ( k = 0; k < (1 << nRange0); k++ ) + { + int iLitAnd = 1; + for ( b = 0; b < nRange0; b++ ) + iLitAnd = Gia_ManHashAnd( pNew, iLitAnd, Abc_LitNotCond(pFans0[b], ((k >> b) & 1) == 0) ); + Vec_IntPush( vTemp1, iLitAnd ); + } + } + for ( b = 0; b < nRange; b++ ) + { + Vec_IntClear( vTemp0 ); + Wlc_ObjForEachFanin( pObj, iFanin, k ) + if ( k > 0 ) + { + nRange1 = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) ); + pFans1 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, iFanin) ); + if ( Wlc_ObjFaninNum(pObj) == 3 ) // Statement 1 + Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (fSigned? pFans1[nRange1-1] : 0) ); + else // Statement 2 + Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (Wlc_NtkObj(p, iFanin)->Signed? pFans1[nRange1-1] : 0) ); + } + if ( pPar->fDecMuxes ) + Vec_IntPush( vRes, Wlc_NtkMuxTree2(pNew, pFans0, nRange0, vTemp0, vTemp1, vTemp2) ); + else + Vec_IntPush( vRes, Wlc_NtkMuxTree_rec(pNew, pFans0, nRange0, vTemp0, 0) ); + } } } else if ( pObj->Type == WLC_OBJ_SEL ) @@ -1779,9 +1920,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) int fCompl = (pObj->Type == WLC_OBJ_COMP_MOREEQU || pObj->Type == WLC_OBJ_COMP_LESSEQU); if ( fSwap ) ABC_SWAP( int *, pArg0, pArg1 ); if ( fSigned ) - iLit = Wlc_BlastLessSigned( pNew, pArg0, pArg1, nRangeMax ); + iLit = pParIn->fBlastNew ? Wlc_BlastLessSigned3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLessSigned( pNew, pArg0, pArg1, nRangeMax ); else - iLit = Wlc_BlastLess( pNew, pArg0, pArg1, nRangeMax ); + iLit = pParIn->fBlastNew ? Wlc_BlastLess3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLess( pNew, pArg0, pArg1, nRangeMax ); iLit = Abc_LitNotCond( iLit, fCompl ); Vec_IntFill( vRes, 1, iLit ); for ( k = 1; k < nRange; k++ ) @@ -1842,7 +1983,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) int nRangeMax = Abc_MaxInt(nRange0, nRange1); int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, fSigned ); int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, fSigned ); - if ( Wlc_NtkCountConstBits(pArg0, nRangeMax) < Wlc_NtkCountConstBits(pArg1, nRangeMax) ) + if ( nRange0 == nRange1 && Wlc_NtkCountConstBits(pArg0, nRangeMax) < Wlc_NtkCountConstBits(pArg1, nRangeMax) ) ABC_SWAP( int *, pArg0, pArg1 ); if ( pPar->fBooth ) Wlc_BlastBooth( pNew, pArg0, pArg1, nRange0, nRange1, vRes, fSigned, pPar->fCla, NULL, pParIn->fVerbose ); @@ -1912,7 +2053,10 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) else if ( pObj->Type == WLC_OBJ_DEC ) { int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRange0, 0 ); - Wlc_BlastDecoder( pNew, pArg0, nRange0, vTemp2, vRes ); + if ( pParIn->fBlastNew ) + Wlc_BlastDecoder2( pNew, pArg0, nRange0, vTemp2, vRes ); + else + Wlc_BlastDecoder( pNew, pArg0, nRange0, vTemp2, vRes ); if ( nRange > Vec_IntSize(vRes) ) Vec_IntFillExtra( vRes, nRange, 0 ); else @@ -2745,6 +2889,47 @@ void Wlc_TransferPioNames( Wlc_Ntk_t * p, Gia_Man_t * pNew ) printf( "Successfully transferred the primary input/output names from the word-level design to the current AIG.\n" ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_MultBlastFileGen( int a, int b, int s ) +{ + FILE * pFile = fopen( "_test13_.v", "wb" ); + fprintf( pFile, "module test ( a, b, z );\n" ); + fprintf( pFile, "input %s [%d:0] a;\n", s ? "signed":"", a-1 ); + fprintf( pFile, "input %s [%d:0] b;\n", s ? "signed":"", b-1 ); + fprintf( pFile, "output %s [%d:0] z;\n", s ? "signed":"", a+b-1 ); + fprintf( pFile, "assign z = a * b;\n" ); + fprintf( pFile, "endmodule\n" ); + fclose( pFile ); +} +void Wlc_MultBlastTest() +{ + char * Command = "%read _test13_.v; %blast; &ps; &w 1.aig; %read _test13_.v; %blast -b; &ps; &w 2.aig; cec -n 1.aig 2.aig"; + int a, b, s, Iters = 0; + for ( a = 1; a < 8; a++ ) + for ( b = 1; b < 8; b++ ) + for ( s = 0; s < 2; s++ ) + { + Wlc_MultBlastFileGen( a, b, s ); + if ( Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) ) + { + fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); + return; + } + Iters++; + } + printf( "Finished %d iterations.\n", Iters ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index d15a7723b..a3747fcfd 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -1046,7 +1046,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_BstParDefault( pPar ); pPar->nOutputRange = 2; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ORAMcombqaydestrnizvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ORAMcombqaydestrfnizvh" ) ) != EOF ) { switch ( c ) { @@ -1131,9 +1131,12 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fReorder ^= 1; break; - case 'n': + case 'f': fDumpNames ^= 1; break; + case 'n': + pPar->fBlastNew ^= 1; + break; case 'i': fPrintInputInfo ^= 1; break; @@ -1222,7 +1225,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameUpdateGia( pAbc, pNew ); return 0; usage: - Abc_Print( -2, "usage: %%blast [-ORAM num] [-combqaydestrnizvh]\n" ); + Abc_Print( -2, "usage: %%blast [-ORAM num] [-combqaydestrfnizvh]\n" ); Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" ); Abc_Print( -2, "\t-O num : zero-based index of the first word-level PO to bit-blast [default = %d]\n", pPar->iOutput ); Abc_Print( -2, "\t-R num : the total number of word-level POs to bit-blast [default = %d]\n", pPar->nOutputRange ); @@ -1240,7 +1243,8 @@ usage: Abc_Print( -2, "\t-s : toggle creating decoded MUXes [default = %s]\n", pPar->fDecMuxes? "yes": "no" ); Abc_Print( -2, "\t-t : toggle creating regular multi-output miter [default = %s]\n", fMiter? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using interleaved variable ordering [default = %s]\n", fReorder? "yes": "no" ); - Abc_Print( -2, "\t-n : toggle dumping signal names into a text file [default = %s]\n", fDumpNames? "yes": "no" ); + Abc_Print( -2, "\t-f : toggle dumping signal names into a text file [default = %s]\n", fDumpNames? "yes": "no" ); + Abc_Print( -2, "\t-n : toggle using improved bit-blasting procedures [default = %s]\n", pPar->fBlastNew? "yes": "no" ); Abc_Print( -2, "\t-i : toggle to print input names after blasting [default = %s]\n", fPrintInputInfo ? "yes": "no" ); Abc_Print( -2, "\t-z : toggle saving flop names after blasting [default = %s]\n", pPar->fSaveFfNames ? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPar->fVerbose? "yes": "no" ); diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h index 2990c0259..e8d017fe0 100644 --- a/src/bdd/dsd/dsd.h +++ b/src/bdd/dsd/dsd.h @@ -117,7 +117,11 @@ extern Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNo extern Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes ); extern void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output, int OffSet ); extern void Dsd_TreePrint2( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int Output ); +extern void Dsd_TreePrint3( void * pStr, Dsd_Manager_t * pDsdMan, int Output ); +extern void Dsd_TreePrint4( void * pStr, Dsd_Manager_t * pDsdMan, int Output ); extern void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode ); +extern int Dsd_TreeNonDsdMax( Dsd_Manager_t * pDsdMan, int Output ); +extern int Dsd_TreeSuppSize( Dsd_Manager_t * pDsdMan, int Output ); /*=== dsdLocal.c =======================================================*/ extern DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode ); diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c index 42eee2cc5..1873ae0c1 100644 --- a/src/bdd/dsd/dsdTree.c +++ b/src/bdd/dsd/dsdTree.c @@ -627,6 +627,195 @@ void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], in ppNodes[ (*pnNodes)++ ] = pNode; } +/**Function************************************************************* + + Synopsis [Returns the size of the largest non-DSD block.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dsd_TreeNonDsdMax_rec( Dsd_Node_t * pNode ) +{ + if ( pNode->Type == DSD_NODE_CONST1 ) + return 0; + if ( pNode->Type == DSD_NODE_BUF ) + return 0; + int MaxBlock = pNode->Type == DSD_NODE_PRIME ? pNode->nDecs : 0; + for ( int i = 0; i < pNode->nDecs; i++ ) + { + int MaxThis = Dsd_TreeNonDsdMax_rec( Dsd_Regular( pNode->pDecs[i] ) ); + MaxBlock = Abc_MaxInt( MaxBlock, MaxThis ); + } + return MaxBlock; +} +int Dsd_TreeNonDsdMax( Dsd_Manager_t * pDsdMan, int Output ) +{ + if ( Output == -1 ) + { + int i, Res = 0; + for ( i = 0; i < pDsdMan->nRoots; i++ ) + Res = Abc_MaxInt( Res, Dsd_TreeNonDsdMax_rec( Dsd_Regular( pDsdMan->pRoots[i] ) ) ); + return Res; + } + else + { + assert( Output >= 0 && Output < pDsdMan->nRoots ); + return Dsd_TreeNonDsdMax_rec( Dsd_Regular( pDsdMan->pRoots[Output] ) ); + } +} + +/**Function************************************************************* + + Synopsis [Returns the support size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dsd_TreeSuppSize_rec( Dsd_Node_t * pNode ) +{ + if ( pNode->Type == DSD_NODE_CONST1 ) + return 0; + if ( pNode->Type == DSD_NODE_BUF ) + return 1; + int nSuppSize = 0; + for ( int i = 0; i < pNode->nDecs; i++ ) + nSuppSize += Dsd_TreeSuppSize_rec( Dsd_Regular( pNode->pDecs[i] ) ); + return nSuppSize; +} +int Dsd_TreeSuppSize( Dsd_Manager_t * pDsdMan, int Output ) +{ + if ( Output == -1 ) + { + int i, Res = 0; + for ( i = 0; i < pDsdMan->nRoots; i++ ) + Res += Dsd_TreeSuppSize_rec( Dsd_Regular( pDsdMan->pRoots[i] ) ); + return Res; + } + else + { + assert( Output >= 0 && Output < pDsdMan->nRoots ); + return Dsd_TreeSuppSize_rec( Dsd_Regular( pDsdMan->pRoots[Output] ) ); + } +} + +/**Function************************************************************* + + Synopsis [Prints the decompostion tree into a string.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dsd_TreePrint3_rec( Vec_Str_t * p, Dsd_Node_t * pNode ) +{ + if ( pNode->Type == DSD_NODE_BUF ) { + Vec_StrPush( p, (int)(pNode->S->index >= 26 ? 'A' - 26 : 'a') + pNode->S->index ); + return; + } + if ( pNode->Type == DSD_NODE_PRIME ) + Vec_StrPush( p, '{' ); + else if ( pNode->Type == DSD_NODE_OR ) + Vec_StrPush( p, '(' ); + else if ( pNode->Type == DSD_NODE_EXOR ) + Vec_StrPush( p, '[' ); + else assert( 0 ); + for ( int i = 0; i < pNode->nDecs; i++ ) + { + Dsd_Node_t * pInput = Dsd_Regular( pNode->pDecs[i] ); + if ( pInput != pNode->pDecs[i] ) + Vec_StrPush( p, '~' ); + Dsd_TreePrint3_rec( p, pInput ); + } + if ( pNode->Type == DSD_NODE_PRIME ) + Vec_StrPush( p, '}' ); + else if ( pNode->Type == DSD_NODE_OR ) + Vec_StrPush( p, ')' ); + else if ( pNode->Type == DSD_NODE_EXOR ) + Vec_StrPush( p, ']' ); + else assert( 0 ); +} +void Dsd_TreePrint3( void * pStr, Dsd_Manager_t * pDsdMan, int Output ) +{ + Vec_Str_t * p = (Vec_Str_t *)pStr; + assert( Output >= 0 && Output < pDsdMan->nRoots ); + Dsd_Node_t * pNode = Dsd_Regular( pDsdMan->pRoots[Output] ); + int fCompl = pNode != pDsdMan->pRoots[Output]; + if ( pNode->Type == DSD_NODE_CONST1 ) + Vec_StrPush( p, fCompl ? '0' : '1' ); + else { + if ( fCompl ) + Vec_StrPush( p, '~' ); + Dsd_TreePrint3_rec( p, pNode ); + } + Vec_StrPush( p, '\0' ); +} + +/**Function************************************************************* + + Synopsis [Prints the decompostion tree into a string.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dsd_TreePrint4_rec( Vec_Str_t * p, Dsd_Node_t * pNode ) +{ + if ( pNode->Type == DSD_NODE_BUF ) { + Vec_StrPush( p, (int)(pNode->S->index >= 26 ? 'A' - 26 : 'a') + pNode->S->index ); + return; + } + if ( pNode->Type == DSD_NODE_PRIME ) + Vec_StrPush( p, '{' ); + else if ( pNode->Type == DSD_NODE_OR ) + Vec_StrPush( p, '(' ); + else if ( pNode->Type == DSD_NODE_EXOR ) + Vec_StrPush( p, '[' ); + else assert( 0 ); + for ( int i = 0; i < pNode->nDecs; i++ ) + { + Dsd_Node_t * pInput = Dsd_Regular( pNode->pDecs[i] ); + if ( (pInput != pNode->pDecs[i]) ^ (pNode->Type == DSD_NODE_OR) ^ (pInput->Type == DSD_NODE_OR) ) + Vec_StrPush( p, '~' ); + Dsd_TreePrint4_rec( p, pInput ); + } + if ( pNode->Type == DSD_NODE_PRIME ) + Vec_StrPush( p, '}' ); + else if ( pNode->Type == DSD_NODE_OR ) + Vec_StrPush( p, ')' ); + else if ( pNode->Type == DSD_NODE_EXOR ) + Vec_StrPush( p, ']' ); + else assert( 0 ); +} +void Dsd_TreePrint4( void * pStr, Dsd_Manager_t * pDsdMan, int Output ) +{ + Vec_Str_t * p = (Vec_Str_t *)pStr; + assert( Output >= 0 && Output < pDsdMan->nRoots ); + Dsd_Node_t * pNode = Dsd_Regular( pDsdMan->pRoots[Output] ); + int fCompl = pNode != pDsdMan->pRoots[Output]; + if ( pNode->Type == DSD_NODE_CONST1 ) + Vec_StrPush( p, fCompl ? '0' : '1' ); + else { + if ( fCompl ^ (pNode->Type == DSD_NODE_OR) ) + Vec_StrPush( p, '~' ); + Dsd_TreePrint4_rec( p, pNode ); + } + Vec_StrPush( p, '\0' ); +} + /**Function************************************************************* Synopsis [Prints the decompostion tree into file.] diff --git a/src/bdd/extrab/extraLutCas.h b/src/bdd/extrab/extraLutCas.h index df7a14010..1308c2bee 100644 --- a/src/bdd/extrab/extraLutCas.h +++ b/src/bdd/extrab/extraLutCas.h @@ -32,7 +32,9 @@ #include #include +#include "aig/miniaig/miniaig.h" #include "bdd/cudd/cuddInt.h" +#include "bdd/dsd/dsd.h" ABC_NAMESPACE_HEADER_START @@ -50,6 +52,8 @@ ABC_NAMESPACE_HEADER_START If the LUT cascade contains a 6-LUT followed by a 4-LUT, the record contains 1+10+8=19 words. */ +#define Mini_AigForEachNonPo( p, i ) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( Mini_AigNodeIsPo(p, i) ) {} else + /**Function************************************************************* Synopsis [] @@ -61,12 +65,128 @@ ABC_NAMESPACE_HEADER_START SeeAlso [] ***********************************************************************/ +void Abc_LutCasCollapseDeref( DdManager * dd, Vec_Ptr_t * vFuncs ) +{ + DdNode * bFunc; int i; + Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i ) + if ( bFunc ) + Cudd_RecursiveDeref( dd, bFunc ); + Vec_PtrFree( vFuncs ); +} +Vec_Ptr_t * Abc_LutCasCollapse( Mini_Aig_t * p, DdManager * dd, int nBddLimit, int fVerbose ) +{ + DdNode * bFunc0, * bFunc1, * bFunc; int Id, nOuts = 0; + Vec_Ptr_t * vFuncs = Vec_PtrStart( Mini_AigNodeNum(p) ); + Vec_PtrWriteEntry( vFuncs, 0, Cudd_ReadLogicZero(dd) ), Cudd_Ref(Cudd_ReadLogicZero(dd)); + Mini_AigForEachPi( p, Id ) + Vec_PtrWriteEntry( vFuncs, Id, Cudd_bddIthVar(dd,Id-1) ), Cudd_Ref(Cudd_bddIthVar(dd,Id-1)); + Mini_AigForEachAnd( p, Id ) { + bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Mini_AigLit2Var(Mini_AigNodeFanin0(p, Id))), Mini_AigLitIsCompl(Mini_AigNodeFanin0(p, Id)) ); + bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Mini_AigLit2Var(Mini_AigNodeFanin1(p, Id))), Mini_AigLitIsCompl(Mini_AigNodeFanin1(p, Id)) ); + bFunc = Cudd_bddAndLimit( dd, bFunc0, bFunc1, nBddLimit ); + if ( bFunc == NULL ) + { + Abc_LutCasCollapseDeref( dd, vFuncs ); + return NULL; + } + Cudd_Ref( bFunc ); + Vec_PtrWriteEntry( vFuncs, Id, bFunc ); + } + Mini_AigForEachPo( p, Id ) { + bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Mini_AigLit2Var(Mini_AigNodeFanin0(p, Id))), Mini_AigLitIsCompl(Mini_AigNodeFanin0(p, Id)) ); + Vec_PtrWriteEntry( vFuncs, Id, bFunc0 ); Cudd_Ref( bFunc0 ); + } + Mini_AigForEachNonPo( p, Id ) { + bFunc = (DdNode *)Vec_PtrEntry(vFuncs, Id); + Cudd_RecursiveDeref( dd, bFunc ); + Vec_PtrWriteEntry( vFuncs, Id, NULL ); + } + Mini_AigForEachPo( p, Id ) + Vec_PtrWriteEntry( vFuncs, nOuts++, Vec_PtrEntry(vFuncs, Id) ); + Vec_PtrShrink( vFuncs, nOuts ); + return vFuncs; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_LutCasFakeNames( int nNames ) +{ + Vec_Ptr_t * vNames; + char Buffer[5]; + int i; + + vNames = Vec_PtrAlloc( nNames ); + for ( i = 0; i < nNames; i++ ) + { + if ( nNames < 26 ) + { + Buffer[0] = 'a' + i; + Buffer[1] = 0; + } + else + { + Buffer[0] = 'a' + i%26; + Buffer[1] = '0' + i/26; + Buffer[2] = 0; + } + Vec_PtrPush( vNames, Extra_UtilStrsav(Buffer) ); + } + return vNames; +} +void Abc_LutCasPrintDsd( DdManager * dd, DdNode * bFunc, int fVerbose ) +{ + Dsd_Manager_t * pManDsd = Dsd_ManagerStart( dd, dd->size, 0 ); + Dsd_Decompose( pManDsd, &bFunc, 1 ); + if ( fVerbose ) + { + Vec_Ptr_t * vNamesCi = Abc_LutCasFakeNames( dd->size ); + Vec_Ptr_t * vNamesCo = Abc_LutCasFakeNames( 1 ); + char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi ); + char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo ); + Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, 0 ); + Vec_PtrFreeFree( vNamesCi ); + Vec_PtrFreeFree( vNamesCo ); + } + Dsd_ManagerStop( pManDsd ); +} +DdNode * Abc_LutCasBuildBdds( Mini_Aig_t * p, DdManager ** pdd ) +{ + DdManager * dd = Cudd_Init( Mini_AigPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + Vec_Ptr_t * vFuncs = Abc_LutCasCollapse( p, dd, 10000, 0 ); + Cudd_AutodynDisable( dd ); + if ( vFuncs == NULL ) { + Extra_StopManager( dd ); + return NULL; + } + DdNode * bNode = (DdNode *)Vec_PtrEntry(vFuncs, 0); + Vec_PtrFree(vFuncs); + *pdd = dd; + return bNode; +} static inline word * Abc_LutCascade( Mini_Aig_t * p, int nLutSize, int fVerbose ) { + DdManager * dd = NULL; + DdNode * bFunc = Abc_LutCasBuildBdds( p, &dd ); + if ( bFunc == NULL ) return NULL; + Abc_LutCasPrintDsd( dd, bFunc, 1 ); + Cudd_RecursiveDeref( dd, bFunc ); + Extra_StopManager( dd ); + word * pLuts = NULL; return pLuts; } ABC_NAMESPACE_HEADER_END -#endif /* __EXTRA_H__ */ +#endif /* ABC__misc__extra__extra_lutcas_h */ diff --git a/src/map/if/acd/ac_decomposition.hpp b/src/map/if/acd/ac_decomposition.hpp index 7628ab39e..c6a526e08 100644 --- a/src/map/if/acd/ac_decomposition.hpp +++ b/src/map/if/acd/ac_decomposition.hpp @@ -510,7 +510,7 @@ private: } } while ( combinations_offset_next( free_set_size, offset, pComb, pInvPerm, tt ) ); - std::array res_perm; + std::array res_perm = {0}; if ( best_cost > ( 1 << ( ps.lut_size - free_set_size ) ) ) { @@ -543,7 +543,7 @@ private: } /* enumerate combinations */ - std::array res_perm; + std::array res_perm = {0}; do { diff --git a/src/map/scl/scl.c b/src/map/scl/scl.c index 6ddd60944..9112bceca 100644 --- a/src/map/scl/scl.c +++ b/src/map/scl/scl.c @@ -185,13 +185,14 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv ) int fVeryVerbose = 0; int fMerge = 0; int fUsePrefix = 0; + int fUseAll = 0; SC_DontUse dont_use = {0}; dont_use.dont_use_list = ABC_ALLOC(char *, argc); dont_use.size = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SGMXdnuvwmph" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SGMXdnuvwmpah" ) ) != EOF ) { switch ( c ) { @@ -259,6 +260,9 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'p': fUsePrefix ^= 1; break; + case 'a': + fUseAll ^= 1; + break; case 'h': goto usage; default: @@ -318,13 +322,13 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv ) // extract genlib library if ( pAbc->pLibScl ) { - Abc_SclInstallGenlib( pAbc->pLibScl, Slew, Gain, nGatesMin ); + Abc_SclInstallGenlib( pAbc->pLibScl, Slew, Gain, fUseAll, nGatesMin ); Mio_LibraryTransferCellIds(); } return 0; usage: - fprintf( pAbc->Err, "usage: read_lib [-SG float] [-M num] [-dnuvwmph] [-X cell_name] \n" ); + fprintf( pAbc->Err, "usage: read_lib [-SG float] [-M num] [-dnuvwmpah] [-X cell_name] \n" ); fprintf( pAbc->Err, "\t reads Liberty library from file\n" ); fprintf( pAbc->Err, "\t-S float : the slew parameter used to generate the library [default = %.2f]\n", Slew ); fprintf( pAbc->Err, "\t-G float : the gain parameter used to generate the library [default = %.2f]\n", Gain ); @@ -336,6 +340,7 @@ usage: fprintf( pAbc->Err, "\t-v : toggle writing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pAbc->Err, "\t-w : toggle writing information about skipped gates [default = %s]\n", fVeryVerbose? "yes": "no" ); fprintf( pAbc->Err, "\t-m : toggle merging library with exisiting library [default = %s]\n", fMerge? "yes": "no" ); + fprintf( pAbc->Err, "\t-a : toggle using prefix for the cell names [default = %s]\n", fUseAll? "yes": "no" ); fprintf( pAbc->Err, "\t-p : toggle using prefix for the cell names [default = %s]\n", fUsePrefix? "yes": "no" ); fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); fprintf( pAbc->Err, "\t : the name of a file to read\n" ); @@ -606,7 +611,7 @@ int Scl_CommandReadScl( Abc_Frame_t * pAbc, int argc, char ** argv ) // extract genlib library if ( pAbc->pLibScl ) { - Abc_SclInstallGenlib( pAbc->pLibScl, 0, 0, 0 ); + Abc_SclInstallGenlib( pAbc->pLibScl, 0, 0, 0, 0 ); Mio_LibraryTransferCellIds(); } return 0; diff --git a/src/map/scl/sclBufSize.c b/src/map/scl/sclBufSize.c index 4d438af09..9f4e07885 100644 --- a/src/map/scl/sclBufSize.c +++ b/src/map/scl/sclBufSize.c @@ -345,7 +345,7 @@ Abc_Obj_t * Abc_SclAddOneInv( Bus_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFano SC_Cell * pCellNew; Abc_Obj_t * pFanout, * pInv; float Target = SC_CellPinCap(p->pInv, 0) * Gain; - float LoadWirePrev, LoadWireThis, LoadNew, Load = 0; + float LoadWirePrev, LoadWireThis, Load = 0; int Limit = Abc_MinInt( p->pPars->nDegree, Vec_PtrSize(vFanouts) ); int i, iStop; Bus_SclCheckSortedFanout( vFanouts ); @@ -384,8 +384,7 @@ Abc_Obj_t * Abc_SclAddOneInv( Bus_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFano Vec_IntSetEntry( p->pNtk->vGates, Abc_ObjId(pInv), pCellNew->Id ); // set departure and load Abc_NtkComputeNodeDeparture( pInv, p->pPars->Slew ); - LoadNew = Abc_NtkComputeNodeLoad( p, pInv ); - assert( LoadNew - Load < 1 && Load - LoadNew < 1 ); + Abc_NtkComputeNodeLoad( p, pInv ); // set fanout info for the inverter Bus_SclObjSetCin( pInv, SC_CellPinCap(pCellNew, 0) ); Bus_SclObjSetETime( pInv, Abc_NtkComputeEdgeDept(pInv, 0, p->pPars->Slew) ); @@ -400,7 +399,7 @@ void Abc_SclBufSize( Bus_Man_t * p, float Gain ) Abc_Obj_t * pObj, * pFanout; abctime clk = Abc_Clock(); int i, k, nObjsOld = Abc_NtkObjNumMax(p->pNtk); - float GainGate, GainInv, Load, LoadNew, Cin, DeptMax = 0; + float GainGate, GainInv, Load, Cin, DeptMax = 0; GainGate = p->pPars->fAddBufs ? (float)pow( (double)Gain, (double)2.0 ) : Gain; GainInv = p->pPars->fAddBufs ? (float)pow( (double)Gain, (double)2.0 ) : Gain; Abc_NtkForEachObjReverse( p->pNtk, pObj, i ) @@ -453,8 +452,7 @@ void Abc_SclBufSize( Bus_Man_t * p, float Gain ) if ( Abc_ObjFaninNum(pFanout) == 0 ) Abc_ObjAddFanin( pFanout, pObj ); Bus_SclObjSetLoad( pObj, 0 ); - LoadNew = Abc_NtkComputeNodeLoad( p, pObj ); - assert( LoadNew - Load < 1 && Load - LoadNew < 1 ); + Abc_NtkComputeNodeLoad( p, pObj ); } if ( Abc_ObjIsCi(pObj) ) continue; diff --git a/src/map/scl/sclLib.h b/src/map/scl/sclLib.h index c08f30c09..2b616a20d 100644 --- a/src/map/scl/sclLib.h +++ b/src/map/scl/sclLib.h @@ -766,7 +766,7 @@ extern SC_WireLoad * Abc_SclFetchWireLoadModel( SC_Lib * p, char * pName ); extern int Abc_SclHasDelayInfo( void * pScl ); extern float Abc_SclComputeAverageSlew( SC_Lib * p ); extern void Abc_SclDumpGenlib( char * pFileName, SC_Lib * p, float Slew, float Gain, int nGatesMin ); -extern void Abc_SclInstallGenlib( void * pScl, float Slew, float Gain, int nGatesMin ); +extern void Abc_SclInstallGenlib( void * pScl, float Slew, float Gain, int fUseAll, int nGatesMin ); ABC_NAMESPACE_HEADER_END diff --git a/src/map/scl/sclLibUtil.c b/src/map/scl/sclLibUtil.c index 147c67f3e..88e8e514e 100644 --- a/src/map/scl/sclLibUtil.c +++ b/src/map/scl/sclLibUtil.c @@ -867,13 +867,13 @@ Mio_Library_t * Abc_SclDeriveGenlibSimple( void * pScl ) SeeAlso [] ***********************************************************************/ -Vec_Str_t * Abc_SclProduceGenlibStr( SC_Lib * p, float Slew, float Gain, int nGatesMin, int * pnCellCount ) +Vec_Str_t * Abc_SclProduceGenlibStr( SC_Lib * p, float Slew, float Gain, int nGatesMin, int fUseAll, int * pnCellCount ) { char Buffer[200]; Vec_Str_t * vStr; SC_Cell * pRepr; - SC_Pin * pPin; - int i, k, Count = 2, nClassMax = 0; + SC_Pin * pPin, * pPinOut; + int i, j, k, Count = 2, nClassMax = 0; // find the largest number of cells in a class SC_LibForEachCellClass( p, pRepr, i ) if ( pRepr->n_outputs == 1 ) @@ -886,38 +886,80 @@ Vec_Str_t * Abc_SclProduceGenlibStr( SC_Lib * p, float Slew, float Gain, int nGa vStr = Vec_StrAlloc( 1000 ); Vec_StrPrintStr( vStr, "GATE _const0_ 0.00 z=CONST0;\n" ); Vec_StrPrintStr( vStr, "GATE _const1_ 0.00 z=CONST1;\n" ); - SC_LibForEachCellClass( p, pRepr, i ) + if ( fUseAll ) { - if ( pRepr->n_inputs == 0 ) - continue; - if ( pRepr->n_outputs > 1 ) - continue; - if ( nGatesMin && pRepr->n_inputs > 2 && Abc_SclClassCellNum(pRepr) < nGatesMin ) - continue; - assert( strlen(pRepr->pName) < 200 ); - Vec_StrPrintStr( vStr, "GATE " ); - sprintf( Buffer, "%-16s", pRepr->pName ); - Vec_StrPrintStr( vStr, Buffer ); - Vec_StrPrintStr( vStr, " " ); -// sprintf( Buffer, "%7.2f", Abc_SclComputeAreaClass(pRepr) ); - sprintf( Buffer, "%7.2f", pRepr->area ); - Vec_StrPrintStr( vStr, Buffer ); - Vec_StrPrintStr( vStr, " " ); - Vec_StrPrintStr( vStr, SC_CellPinName(pRepr, pRepr->n_inputs) ); - Vec_StrPrintStr( vStr, "=" ); - Vec_StrPrintStr( vStr, SC_CellPinOutFunc(pRepr, 0) ? SC_CellPinOutFunc(pRepr, 0) : "?" ); - Vec_StrPrintStr( vStr, ";\n" ); - SC_CellForEachPinIn( pRepr, pPin, k ) + SC_LibForEachCell( p, pRepr, i ) { - float Delay = Abc_SclComputeDelayClassPin( p, pRepr, k, Slew, Gain ); - assert( Delay > 0 ); - Vec_StrPrintStr( vStr, " PIN " ); - sprintf( Buffer, "%-4s", pPin->pName ); - Vec_StrPrintStr( vStr, Buffer ); - sprintf( Buffer, " UNKNOWN 1 999 %7.2f 0.00 %7.2f 0.00\n", Delay, Delay ); - Vec_StrPrintStr( vStr, Buffer ); + if ( pRepr->n_inputs == 0 ) + continue; + //if ( pRepr->n_outputs > 1 ) + // continue; + if ( nGatesMin && pRepr->n_inputs > 2 && Abc_SclClassCellNum(pRepr) < nGatesMin ) + continue; + SC_CellForEachPinOut( pRepr, pPinOut, j ) + { + assert( strlen(pRepr->pName) < 200 ); + Vec_StrPrintStr( vStr, "GATE " ); + sprintf( Buffer, "%-16s", pRepr->pName ); + Vec_StrPrintStr( vStr, Buffer ); + Vec_StrPrintStr( vStr, " " ); + // sprintf( Buffer, "%7.2f", Abc_SclComputeAreaClass(pRepr) ); + sprintf( Buffer, "%7.2f", pRepr->area ); + Vec_StrPrintStr( vStr, Buffer ); + Vec_StrPrintStr( vStr, " " ); + Vec_StrPrintStr( vStr, SC_CellPinName(pRepr, j) ); + Vec_StrPrintStr( vStr, "=" ); + Vec_StrPrintStr( vStr, SC_CellPinOutFunc(pRepr, j-pRepr->n_inputs) ? SC_CellPinOutFunc(pRepr, j-pRepr->n_inputs) : "?" ); + Vec_StrPrintStr( vStr, ";\n" ); + SC_CellForEachPinIn( pRepr, pPin, k ) + { + float Delay = Abc_SclComputeDelayClassPin( p, pRepr, k, Slew, Gain ); + assert( Delay > 0 ); + Vec_StrPrintStr( vStr, " PIN " ); + sprintf( Buffer, "%-4s", pPin->pName ); + Vec_StrPrintStr( vStr, Buffer ); + sprintf( Buffer, " UNKNOWN 1 999 %7.2f 0.00 %7.2f 0.00\n", Delay, Delay ); + Vec_StrPrintStr( vStr, Buffer ); + } + Count++; + } + } + } + else + { + SC_LibForEachCellClass( p, pRepr, i ) + { + if ( pRepr->n_inputs == 0 ) + continue; + if ( pRepr->n_outputs > 1 ) + continue; + if ( nGatesMin && pRepr->n_inputs > 2 && Abc_SclClassCellNum(pRepr) < nGatesMin ) + continue; + assert( strlen(pRepr->pName) < 200 ); + Vec_StrPrintStr( vStr, "GATE " ); + sprintf( Buffer, "%-16s", pRepr->pName ); + Vec_StrPrintStr( vStr, Buffer ); + Vec_StrPrintStr( vStr, " " ); + // sprintf( Buffer, "%7.2f", Abc_SclComputeAreaClass(pRepr) ); + sprintf( Buffer, "%7.2f", pRepr->area ); + Vec_StrPrintStr( vStr, Buffer ); + Vec_StrPrintStr( vStr, " " ); + Vec_StrPrintStr( vStr, SC_CellPinName(pRepr, pRepr->n_inputs) ); + Vec_StrPrintStr( vStr, "=" ); + Vec_StrPrintStr( vStr, SC_CellPinOutFunc(pRepr, 0) ? SC_CellPinOutFunc(pRepr, 0) : "?" ); + Vec_StrPrintStr( vStr, ";\n" ); + SC_CellForEachPinIn( pRepr, pPin, k ) + { + float Delay = Abc_SclComputeDelayClassPin( p, pRepr, k, Slew, Gain ); + assert( Delay > 0 ); + Vec_StrPrintStr( vStr, " PIN " ); + sprintf( Buffer, "%-4s", pPin->pName ); + Vec_StrPrintStr( vStr, Buffer ); + sprintf( Buffer, " UNKNOWN 1 999 %7.2f 0.00 %7.2f 0.00\n", Delay, Delay ); + Vec_StrPrintStr( vStr, Buffer ); + } + Count++; } - Count++; } Vec_StrPrintStr( vStr, "\n.end\n" ); Vec_StrPush( vStr, '\0' ); @@ -1012,7 +1054,7 @@ void Abc_SclDumpGenlib( char * pFileName, SC_Lib * p, float SlewInit, float Gain printf( "Cannot open file \"%s\" for writing.\n", FileName ); return; } - vStr = Abc_SclProduceGenlibStr( p, Slew, Gain, nGatesMin, &nCellCount ); + vStr = Abc_SclProduceGenlibStr( p, Slew, Gain, nGatesMin, 0, &nCellCount ); fprintf( pFile, "%s", Vec_StrArray(vStr) ); Vec_StrFree( vStr ); fclose( pFile ); @@ -1026,7 +1068,7 @@ Mio_Library_t * Abc_SclDeriveGenlib( void * pScl, void * pMio, float SlewInit, f Vec_Str_t * vStr; Mio_Library_t * pLib; if ( pMio == NULL ) - vStr = Abc_SclProduceGenlibStr( p, Slew, Gain, nGatesMin, &nCellCount ); + vStr = Abc_SclProduceGenlibStr( p, Slew, Gain, nGatesMin, 0, &nCellCount ); else vStr = Abc_SclProduceGenlibStrProfile( p, (Mio_Library_t *)pMio, Slew, Gain, nGatesMin, &nCellCount ); pLib = Mio_LibraryRead( p->pFileName, Vec_StrArray(vStr), NULL, 0, 0 ); @@ -1049,7 +1091,7 @@ Mio_Library_t * Abc_SclDeriveGenlib( void * pScl, void * pMio, float SlewInit, f SeeAlso [] ***********************************************************************/ -void Abc_SclInstallGenlib( void * pScl, float SlewInit, float Gain, int nGatesMin ) +void Abc_SclInstallGenlib( void * pScl, float SlewInit, float Gain, int fUseAll, int nGatesMin ) { SC_Lib * p = (SC_Lib *)pScl; Vec_Str_t * vStr, * vStr2; @@ -1058,7 +1100,7 @@ void Abc_SclInstallGenlib( void * pScl, float SlewInit, float Gain, int nGatesMi if ( Gain == 0 ) vStr = Abc_SclProduceGenlibStrSimple(p); else - vStr = Abc_SclProduceGenlibStr( p, Slew, Gain, nGatesMin, &nGateCount ); + vStr = Abc_SclProduceGenlibStr( p, Slew, Gain, nGatesMin, fUseAll, &nGateCount ); vStr2 = Vec_StrDup( vStr ); RetValue = Mio_UpdateGenlib2( vStr, vStr2, p->pName, 0 ); Vec_StrFree( vStr ); diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c index 54e6efc25..6585b7a72 100644 --- a/src/misc/extra/extraUtilFile.c +++ b/src/misc/extra/extraUtilFile.c @@ -18,6 +18,13 @@ ***********************************************************************/ +#ifdef WIN32 +#include +#define PATH_MAX MAX_PATH +#else +#include +#endif + #include "extra.h" ABC_NAMESPACE_IMPL_START @@ -184,9 +191,9 @@ char * Extra_FileNameGeneric( char * FileName ) ***********************************************************************/ char * Extra_FileNameGenericAppend( char * pBase, char * pSuffix ) { - static char Buffer[1000]; + static char Buffer[PATH_MAX]; char * pDot; - assert( strlen(pBase) + strlen(pSuffix) < 1000 ); + assert( strlen(pBase) + strlen(pSuffix) < PATH_MAX ); strcpy( Buffer, pBase ); if ( (pDot = strrchr( Buffer, '.' )) ) *pDot = 0; diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index 96944d7cc..4bc3c1c15 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -287,6 +287,9 @@ static inline double Abc_Word2Dbl( word Num ) { union { word x; static inline int Abc_Base2Log( unsigned n ) { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n >>= 1, r++ ) {}; return r; } static inline int Abc_Base10Log( unsigned n ) { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n /= 10, r++ ) {}; return r; } static inline int Abc_Base16Log( unsigned n ) { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n /= 16, r++ ) {}; return r; } +static inline int Abc_Base2LogW( word n ) { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n >>= 1, r++ ) {}; return r; } +static inline int Abc_Base10LogW( word n ) { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n /= 10, r++ ) {}; return r; } +static inline int Abc_Base16LogW( word n ) { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n /= 16, r++ ) {}; return r; } static inline char * Abc_UtilStrsav( char * s ) { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL; } static inline char * Abc_UtilStrsavTwo( char * s, char * a ){ char * r; if (!a) return Abc_UtilStrsav(s); r = ABC_ALLOC(char, strlen(s)+strlen(a)+1); sprintf(r, "%s%s", s, a ); return r; } static inline char * Abc_UtilStrsavNum( char * s, int n ) { char * r; if (!s) return NULL; r = ABC_ALLOC(char, strlen(s)+12+1); sprintf(r, "%s%d", s, n ); return r; } diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 35f0f83e4..323c96467 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -225,6 +225,33 @@ static inline void Abc_TtMask( word * pTruth, int nWords, int nBits ) pTruth[w] = 0; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline word Abc_TtWordReverseBits( word w ) +{ + int Rev[16] = {0, 8, 4, 12, 2, 10, 6, 14, 1, 9, 5, 13, 3, 11, 7, 15}; + word r = 0; int i; + for ( i = 0; i < 16; i++ ) + r |= (word)Rev[(w >> (i<<2))&15] << ((15-i)<<2); + return r; +} +static inline word Abc_TtWordReverseHexDigits( word w ) +{ + word r = 0; int i; + for ( i = 0; i < 16; i++ ) + r |= ((w >> (i<<2))&15) << ((15-i)<<2); + return r; +} + /**Function************************************************************* Synopsis [] diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index e4ea6cfe3..0b1ae6d30 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -65,6 +65,8 @@ struct Vec_Int_t_ for ( i = Start; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- ) #define Vec_IntForEachEntryTwo( vVec1, vVec2, Entry1, Entry2, i ) \ for ( i = 0; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ ) +#define Vec_IntForEachEntryThree( vVec1, vVec2, vVec3, Entry1, Entry2, Entry3, i ) \ + for ( i = 0; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1) && (((Entry3) = Vec_IntEntry(vVec3, i)), 1); i++ ) #define Vec_IntForEachEntryTwoStart( vVec1, vVec2, Entry1, Entry2, i, Start ) \ for ( i = Start; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ ) #define Vec_IntForEachEntryDouble( vVec, Entry1, Entry2, i ) \ diff --git a/src/opt/dau/dauNpn.c b/src/opt/dau/dauNpn.c index 71cc857b6..a654695c5 100644 --- a/src/opt/dau/dauNpn.c +++ b/src/opt/dau/dauNpn.c @@ -859,6 +859,128 @@ Vec_Mem_t * Dau_CollectNpnFunctions( word * p, int nVars, int fVerbose ) return vTtMem; } +/**Function************************************************************* + + Synopsis [Compute NPN class members.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Mem_t * Dau_CollectNpnFunctionsArray( Vec_Wrd_t * vFuncs, int nVars, Vec_Int_t ** pvMap, int fVerbose ) +{ + assert( nVars <= 10 ); + abctime clkStart = Abc_Clock(); + Vec_Int_t * vMap = Vec_IntAlloc( 100 ); + Vec_Int_t * vCnts = Vec_IntAlloc( Vec_WrdSize(vFuncs) ); + Vec_Mem_t * vTtMem = Vec_MemAllocForTTSimple( nVars ); + int nWords = Abc_Truth6WordNum(nVars); + int nPerms = Extra_Factorial( nVars ); + int nMints = 1 << nVars; + int * pPerm = Extra_PermSchedule( nVars ); + int * pComp = Extra_GreyCodeSchedule( nVars ); + int m, i, k, t, Entry; + word * pCopy = ABC_ALLOC( word, nWords ); + int nClasses = Vec_WrdSize(vFuncs) / nWords; + assert( nClasses * nWords == Vec_WrdSize(vFuncs) ); + for ( t = 0; t < nClasses; t++ ) + { + word * pTruth = Vec_WrdEntryP( vFuncs, nWords * t ); + int nFuncs = Vec_MemEntryNum(vTtMem); + Abc_TtCopy( pCopy, pTruth, nWords, pTruth[0] & 1 ); + Vec_MemHashInsert( vTtMem, pCopy ); + for ( m = 0; m < nMints; m++ ) { + Abc_TtFlip( pCopy, nWords, pComp[m] ); + if ( pCopy[0] & 1 ) { + Abc_TtNot( pCopy, nWords ); + assert( (pCopy[0] & 1) == 0 ); + Vec_MemHashInsert( vTtMem, pCopy ); + Abc_TtNot( pCopy, nWords ); + } + else + Vec_MemHashInsert( vTtMem, pCopy ); + } + if ( pTruth[0] & 1 ) + assert( Abc_TtOpposite(pCopy, pTruth, nWords) ); + else + assert( Abc_TtEqual(pCopy, pTruth, nWords) ); + int nFuncs2 = Vec_MemEntryNum(vTtMem); + for ( i = nFuncs; i < nFuncs2; i++ ) { + Abc_TtCopy( pCopy, Vec_MemReadEntry(vTtMem, i), nWords, 0 ); + for ( k = 0; k < nPerms; k++ ) { + Abc_TtSwapAdjacent( pCopy, nWords, pPerm[k] ); + assert( (pCopy[0] & 1) == 0 ); + Vec_MemHashInsert( vTtMem, pCopy ); + } + assert( Abc_TtEqual(pCopy, Vec_MemReadEntry(vTtMem, i), nWords) ); + } + for ( i = nFuncs; i < Vec_MemEntryNum(vTtMem); i++ ) + Vec_IntPush( vMap, t ); + Vec_IntPush( vCnts, Vec_MemEntryNum(vTtMem) - nFuncs ); + } + ABC_FREE( pCopy ); + ABC_FREE( pPerm ); + ABC_FREE( pComp ); + if ( fVerbose ) { + int Lim = Abc_MinInt( Vec_IntSize(vCnts), 7 ); + printf( "Collected %d", Vec_MemEntryNum(vTtMem) ); + Vec_IntForEachEntryStop( vCnts, Entry, i, Lim ) + printf( " %c %d", i ? '+' : '=', Entry ); + if ( Vec_IntSize(vCnts) > Lim ) + printf( " + ..." ); + printf( " NPN class members. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); + fflush(stdout); + } + Vec_IntFree( vCnts ); + if ( pvMap ) + *pvMap = vMap; + else + Vec_IntFree( vMap ); + return vTtMem; +} + +/**Function************************************************************* + + Synopsis [Canonicize a set of functions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dau_CanonicizeArray( Vec_Wrd_t * vFuncs, int nVars, int fVerbose ) +{ + abctime clkStart = Abc_Clock(); + extern unsigned Abc_TtCanonicizeCA(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres); + if ( fVerbose ) printf( "Functions: %d (original) ", Vec_WrdSize(vFuncs) ); + unsigned uCanonPhase; char pCanonPerm[16]; word Func; int i; + Vec_WrdUniqify( vFuncs ); + + if ( fVerbose ) printf( "-> %d (unique) ", Vec_WrdSize(vFuncs) ); + Vec_WrdForEachEntry( vFuncs, Func, i ) { + uCanonPhase = Abc_TtCanonicize( &Func, nVars, pCanonPerm ); + Vec_WrdWriteEntry( vFuncs, i, Func ); + } + Vec_WrdUniqify( vFuncs ); + if ( fVerbose ) printf( "-> %d (approx NPN) ", Vec_WrdSize(vFuncs) ); + Abc_TtHieMan_t * pMan = Abc_TtHieManStart(nVars, 5); + Vec_WrdForEachEntry( vFuncs, Func, i ) { + uCanonPhase = Abc_TtCanonicizeWrap(Abc_TtCanonicizeCA, pMan, &Func, nVars, pCanonPerm, 1); + Vec_WrdWriteEntry( vFuncs, i, Func ); + } + Vec_WrdUniqify( vFuncs ); + if ( fVerbose ) printf( "-> %d (exact NPN). ", Vec_WrdSize(vFuncs) ); + Abc_TtHieManStop(pMan); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); + fflush( stdout ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/fxu/fxuReduce.c b/src/opt/fxu/fxuReduce.c index 84e2bf87a..6e5dd0fed 100644 --- a/src/opt/fxu/fxuReduce.c +++ b/src/opt/fxu/fxuReduce.c @@ -84,6 +84,8 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota nBitsMax = nFanins; } assert( iPair == nPairsTotal ); + if ( nBitsMax == -1 ) + nBitsMax = 0; // allocate storage for counters of cube pairs by difference pnPairCounters = ABC_CALLOC( int, 2 * nBitsMax ); diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c index 550ea4541..c3edf61ff 100644 --- a/src/proof/cec/cecCorr.c +++ b/src/proof/cec/cecCorr.c @@ -1320,8 +1320,12 @@ Vec_Int_t * Gia_ManFindStopFlops( Gia_Man_t * p, int nFlopIncFreq, int fVerbose if ( Spot >= 0 && Vec_IntEntry(vAvail, i) == 0 ) Vec_IntPush( vHeads, i ); Vec_IntForEachEntry( vHeads, Spot, i ) { - for ( k = 0, Temp = Spot; Vec_IntEntry(vNexts, Temp) >= 0; k++, Temp = Vec_IntEntry(vNexts, Temp) ) - ; + Vec_IntFill( vAvail, Gia_ManRegNum(p), 0 ); + for ( k = 0, Temp = Spot; Vec_IntEntry(vNexts, Temp) >= 0; k++, Temp = Vec_IntEntry(vNexts, Temp) ) { + if ( Vec_IntEntry(vAvail, Temp) ) + break; + Vec_IntWriteEntry( vAvail, Temp, 1 ); + } if ( k > 100 ) { nItems++; diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 343563598..795296e6f 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -62,6 +62,7 @@ struct Bmc_EsPar_t_ int fFewerVars; int fQuadrEnc; int fUniqFans; + int fLutCascade; int RuntimeLim; int fVerbose; char * pTtStr; @@ -84,7 +85,8 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars ) pPars->fEnumSols = 0; pPars->fFewerVars = 0; pPars->fQuadrEnc = 0; - pPars->fUniqFans = 0; + pPars->fUniqFans = 0; + pPars->fLutCascade = 0; pPars->RuntimeLim = 0; pPars->fVerbose = 1; } diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 5e9c1310c..b6ff80a58 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -24,6 +24,8 @@ #include "sat/glucose/AbcGlucose.h" #include "aig/miniaig/miniaig.h" #include "base/io/ioResub.h" +#include "base/main/main.h" +#include "base/cmd/cmd.h" ABC_NAMESPACE_IMPL_START @@ -1045,6 +1047,23 @@ static int Exa3_ManMarkup( Exa3_Man_t * p ) // assign connectivity variables for ( i = p->nVars; i < p->nObjs; i++ ) { + if ( p->pPars->fLutCascade ) + { + if ( i > p->nVars ) + { + Vec_WecPush( p->vOutLits, i-1, Abc_Var2Lit(p->iVar, 0) ); + p->VarMarks[i][0][i-1] = p->iVar++; + } + for ( k = (int)(i > p->nVars); k < p->nLutSize; k++ ) + { + for ( j = 0; j < p->nVars - k + (int)(i > p->nVars); j++ ) + { + Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); + p->VarMarks[i][k][j] = p->iVar++; + } + } + continue; + } for ( k = 0; k < p->nLutSize; k++ ) { if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 ) @@ -1209,6 +1228,61 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl ) } } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl ) +{ + int i, k, b, iVar; + char pFileName[1000]; + sprintf( pFileName, "%s.blif", p->pPars->pTtStr ); + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) return; + fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() ); + fprintf( pFile, ".model %s\n", p->pPars->pTtStr ); + fprintf( pFile, ".inputs" ); + for ( k = 0; k < p->nVars; k++ ) + fprintf( pFile, " %c", 'a'+k ); + fprintf( pFile, "\n.outputs F\n" ); + for ( i = p->nObjs - 1; i >= p->nVars; i-- ) + { + fprintf( pFile, ".names" ); + for ( k = 0; k < p->nLutSize; k++ ) + { + iVar = Exa3_ManFindFanin( p, i, k ); + if ( iVar >= 0 && iVar < p->nVars ) + fprintf( pFile, " %c", 'a'+iVar ); + else + fprintf( pFile, " %02d", iVar ); + } + if ( i == p->nObjs - 1 ) + fprintf( pFile, " F\n" ); + else + fprintf( pFile, " %02d\n", i ); + int iVarStart = 1 + p->LutMask*(i - p->nVars); + for ( k = 0; k < p->LutMask; k++ ) + { + int Val = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+k); + if ( Val == 0 ) + continue; + for ( b = 0; b < p->nLutSize; b++ ) + fprintf( pFile, "%d", ((k+1) >> b) & 1 ); + fprintf( pFile, " %d\n", i != p->nObjs - 1 || !fCompl ); + } + } + fprintf( pFile, ".end\n\n" ); + fclose( pFile ); + printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName ); +} + /**Function************************************************************* @@ -1464,8 +1538,10 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) else printf( "The problem has no solution.\n" ); printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] ); - Exa3_ManFree( p ); Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + if ( iMint == -1 ) + Exa3_ManDumpBlif( p, fCompl ); + Exa3_ManFree( p ); } /**Function************************************************************* @@ -3916,6 +3992,62 @@ void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize ) Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Exa_NpnCascadeTest() +{ + char Buffer[100]; + char Command[1000]; int i; + FILE * pFile = fopen( "npn3.txt", "r" ); + for ( i = 0; i < 14; i++ ) +// FILE * pFile = fopen( "npn4.txt", "r" ); +// for ( i = 0; i < 222; i++ ) +// FILE * pFile = fopen( "npn5.txt", "r" ); +// for ( i = 0; i < 616126; i++ ) + { + int Value = fscanf( pFile, "%s", Buffer ); + assert( Value == 1 ); + if ( i == 0 ) continue; + if ( Buffer[strlen(Buffer)-1] == '\n' ) + Buffer[strlen(Buffer)-1] = '\0'; + if ( Buffer[strlen(Buffer)-1] == '\r' ) + Buffer[strlen(Buffer)-1] = '\0'; + sprintf( Command, "lutexact -I 3 -N 2 -K 2 -gvc %s", Buffer+2 ); + printf( "\nNPN class %6d : Command \"%s\":\n", i, Command ); + if ( Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) ) + { + fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); + return; + } + } + fclose( pFile ); +} +void Exa_NpnCascadeTest6() +{ + char Command[1000]; int i; + Abc_Random(1); + for ( i = 0; i < 10000; i++ ) + { + word Truth = Abc_RandomW(0); + sprintf( Command, "lutexact -I 6 -N 2 -K 5 -gvc %016lx", Truth ); + printf( "\nIter %4d : Command \"%s\":\n", i, Command ); + if ( Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) ) + { + fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); + return; + } + } +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c index 32bbc102f..8becc6321 100644 --- a/src/sat/bmc/bmcMaj2.c +++ b/src/sat/bmc/bmcMaj2.c @@ -944,6 +944,23 @@ static int Exa3_ManMarkup( Exa3_Man_t * p ) // assign connectivity variables for ( i = p->nVars; i < p->nObjs; i++ ) { + if ( p->pPars->fLutCascade ) + { + if ( i > p->nVars ) + { + Vec_WecPush( p->vOutLits, i-1, Abc_Var2Lit(p->iVar, 0) ); + p->VarMarks[i][0][i-1] = p->iVar++; + } + for ( k = (int)(i > p->nVars); k < p->nLutSize; k++ ) + { + for ( j = 0; j < p->nVars - k + (int)(i > p->nVars); j++ ) + { + Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); + p->VarMarks[i][k][j] = p->iVar++; + } + } + continue; + } for ( k = 0; k < p->nLutSize; k++ ) { if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 ) @@ -1159,6 +1176,61 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl ) } } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl ) +{ + int i, k, b, iVar; + char pFileName[1000]; + sprintf( pFileName, "%s.blif", p->pPars->pTtStr ); + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) return; + fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() ); + fprintf( pFile, ".model %s\n", p->pPars->pTtStr ); + fprintf( pFile, ".inputs" ); + for ( k = 0; k < p->nVars; k++ ) + fprintf( pFile, " %c", 'a'+k ); + fprintf( pFile, "\n.outputs F\n" ); + for ( i = p->nObjs - 1; i >= p->nVars; i-- ) + { + fprintf( pFile, ".names" ); + for ( k = 0; k < p->nLutSize; k++ ) + { + iVar = Exa3_ManFindFanin( p, i, k ); + if ( iVar >= 0 && iVar < p->nVars ) + fprintf( pFile, " %c", 'a'+iVar ); + else + fprintf( pFile, " %02d", iVar ); + } + if ( i == p->nObjs - 1 ) + fprintf( pFile, " F\n" ); + else + fprintf( pFile, " %02d\n", i ); + int iVarStart = 1 + p->LutMask*(i - p->nVars); + for ( k = 0; k < p->LutMask; k++ ) + { + int Val = sat_solver_var_value(p->pSat, iVarStart+k); + if ( Val == 0 ) + continue; + for ( b = 0; b < p->nLutSize; b++ ) + fprintf( pFile, "%d", ((k+1) >> b) & 1 ); + fprintf( pFile, " %d\n", i != p->nObjs - 1 || !fCompl ); + } + } + fprintf( pFile, ".end\n\n" ); + fclose( pFile ); + printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName ); +} + /**Function************************************************************* @@ -1347,8 +1419,10 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ) } if ( iMint == -1 ) Exa3_ManPrintSolution( p, fCompl ); - Exa3_ManFree( p ); Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + if ( iMint == -1 ) + Exa3_ManDumpBlif( p, fCompl ); + Exa3_ManFree( p ); } diff --git a/test.ps b/test.ps new file mode 100644 index 000000000..7634275b2 --- /dev/null +++ b/test.ps @@ -0,0 +1,388 @@ +%!PS-Adobe-3.0 +%%Creator: graphviz version 2.43.0 (0) +%%Title: network +%%Pages: (atend) +%%BoundingBox: (atend) +%%EndComments +save +%%BeginProlog +/DotDict 200 dict def +DotDict begin + +/setupLatin1 { +mark +/EncodingVector 256 array def + EncodingVector 0 + +ISOLatin1Encoding 0 255 getinterval putinterval +EncodingVector 45 /hyphen put + +% Set up ISO Latin 1 character encoding +/starnetISO { + dup dup findfont dup length dict begin + { 1 index /FID ne { def }{ pop pop } ifelse + } forall + /Encoding EncodingVector def + currentdict end definefont +} def +/Times-Roman starnetISO def +/Times-Italic starnetISO def +/Times-Bold starnetISO def +/Times-BoldItalic starnetISO def +/Helvetica starnetISO def +/Helvetica-Oblique starnetISO def +/Helvetica-Bold starnetISO def +/Helvetica-BoldOblique starnetISO def +/Courier starnetISO def +/Courier-Oblique starnetISO def +/Courier-Bold starnetISO def +/Courier-BoldOblique starnetISO def +cleartomark +} bind def + +%%BeginResource: procset graphviz 0 0 +/coord-font-family /Times-Roman def +/default-font-family /Times-Roman def +/coordfont coord-font-family findfont 8 scalefont def + +/InvScaleFactor 1.0 def +/set_scale { + dup 1 exch div /InvScaleFactor exch def + scale +} bind def + +% styles +/solid { [] 0 setdash } bind def +/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def +/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def +/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def +/bold { 2 setlinewidth } bind def +/filled { } bind def +/unfilled { } bind def +/rounded { } bind def +/diagonals { } bind def +/tapered { } bind def + +% hooks for setting color +/nodecolor { sethsbcolor } bind def +/edgecolor { sethsbcolor } bind def +/graphcolor { sethsbcolor } bind def +/nopcolor {pop pop pop} bind def + +/beginpage { % i j npages + /npages exch def + /j exch def + /i exch def + /str 10 string def + npages 1 gt { + gsave + coordfont setfont + 0 0 moveto + (\() show i str cvs show (,) show j str cvs show (\)) show + grestore + } if +} bind def + +/set_font { + findfont exch + scalefont setfont +} def + +% draw text fitted to its expected width +/alignedtext { % width text + /text exch def + /width exch def + gsave + width 0 gt { + [] 0 setdash + text stringwidth pop width exch sub text length div 0 text ashow + } if + grestore +} def + +/boxprim { % xcorner ycorner xsize ysize + 4 2 roll + moveto + 2 copy + exch 0 rlineto + 0 exch rlineto + pop neg 0 rlineto + closepath +} bind def + +/ellipse_path { + /ry exch def + /rx exch def + /y exch def + /x exch def + matrix currentmatrix + newpath + x y translate + rx ry scale + 0 0 1 0 360 arc + setmatrix +} bind def + +/endpage { showpage } bind def +/showpage { } def + +/layercolorseq + [ % layer color sequence - darkest to lightest + [0 0 0] + [.2 .8 .8] + [.4 .8 .8] + [.6 .8 .8] + [.8 .8 .8] + ] +def + +/layerlen layercolorseq length def + +/setlayer {/maxlayer exch def /curlayer exch def + layercolorseq curlayer 1 sub layerlen mod get + aload pop sethsbcolor + /nodecolor {nopcolor} def + /edgecolor {nopcolor} def + /graphcolor {nopcolor} def +} bind def + +/onlayer { curlayer ne {invis} if } def + +/onlayers { + /myupper exch def + /mylower exch def + curlayer mylower lt + curlayer myupper gt + or + {invis} if +} def + +/curlayer 0 def + +%%EndResource +%%EndProlog +%%BeginSetup +14 default-font-family set_font +% /arrowlength 10 def +% /arrowwidth 5 def + +% make sure pdfmark is harmless for PS-interpreters other than Distiller +/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse +% make '<<' and '>>' safe on PS Level 1 devices +/languagelevel where {pop languagelevel}{1} ifelse +2 lt { + userdict (<<) cvn ([) cvn load put + userdict (>>) cvn ([) cvn load put +} if + +%%EndSetup +setupLatin1 +%%Page: 1 1 +%%PageBoundingBox: 37 212 575 580 +%%PageOrientation: Portrait +0 0 1 beginpage +gsave +37 212 538 368 boxprim clip newpath +1 1 set_scale 0 rotate 41 216 translate +% LevelTitle1 +gsave +grestore +% LevelTitle2 +gsave +grestore +% LevelTitle1->LevelTitle2 +% Level2 +gsave +grestore +% LevelTitle2->Level2 +% Level1 +gsave +grestore +% Level2->Level1 +% Level0 +gsave +grestore +% Level1->Level0 +% title1 +gsave +0 0 0 nodecolor +20 /Times-Roman set_font +151.5 340 moveto 299 (Network structure visualized by ABC) alignedtext +0 0 0 nodecolor +20 /Times-Roman set_font +80 318 moveto 442 (Benchmark "test". Time was Fri Sep 6 06:13:38 2024. ) alignedtext +grestore +% title2 +gsave +0 0 0 nodecolor +18 /Times-Roman set_font +119 249.6 moveto 364 (The network contains 1 logic nodes and 0 latches.) alignedtext +grestore +% title1->title2 +% Node4 +gsave +1 setlinewidth +0.043137 0.68627 1 nodecolor +newpath 263 154 moveto +290.0966 188.5 lineto +235.9034 188.5 lineto +closepath stroke +0 0 0 nodecolor +14 /Times-Roman set_font +260.5 173.3 moveto 5 (f) alignedtext +grestore +% title2->Node4 +% Node5 +gsave +1 setlinewidth +0.043137 0.68627 1 nodecolor +newpath 338 154 moveto +367.795 188.5 lineto +308.205 188.5 lineto +closepath stroke +0 0 0 nodecolor +14 /Times-Roman set_font +334.5 173.3 moveto 7 (g) alignedtext +grestore +% title2->Node5 +% Node4->Node5 +% Node6 +gsave +1 setlinewidth +0 0 0 nodecolor +300 100 27 18 ellipse_path stroke +0 0 0 nodecolor +14 /Times-Roman set_font +296.5 96.3 moveto 7 (6) alignedtext +grestore +% Node4->Node6 +gsave +1 setlinewidth +solid +0 0 0 edgecolor +newpath 274.2701 153.1552 moveto +279.9849 141.5712 286.7919 127.7731 291.9687 117.2797 curveto +stroke +0 0 0 edgecolor +newpath 271.0718 151.7273 moveto +269.7864 162.2438 lineto +277.3495 154.8243 lineto +closepath fill +1 setlinewidth +solid +0 0 0 edgecolor +newpath 271.0718 151.7273 moveto +269.7864 162.2438 lineto +277.3495 154.8243 lineto +closepath stroke +grestore +% Node5->Node6 +gsave +1 setlinewidth +solid +0 0 0 edgecolor +newpath 326.2775 152.8634 moveto +320.4603 141.3822 313.571 127.785 308.3062 117.3939 curveto +stroke +0 0 0 edgecolor +newpath 323.2107 154.5546 moveto +330.8525 161.8931 lineto +329.4549 151.3908 lineto +closepath fill +1 setlinewidth +solid +0 0 0 edgecolor +newpath 323.2107 154.5546 moveto +330.8525 161.8931 lineto +329.4549 151.3908 lineto +closepath stroke +grestore +% Node1 +gsave +1 setlinewidth +0.043137 0.68627 1 nodecolor +newpath 261 46 moveto +231.205 11.5 lineto +290.795 11.5 lineto +closepath stroke +0 0 0 nodecolor +14 /Times-Roman set_font +257.5 19.3 moveto 7 (a) alignedtext +grestore +% Node6->Node1 +gsave +1 setlinewidth +solid +0 0 0 edgecolor +newpath 286.8586 73.7282 moveto +280.7027 61.8898 273.5973 48.2257 268.3944 38.2199 curveto +stroke +0 0 0 edgecolor +newpath 283.8187 75.4687 moveto +291.5376 82.7261 lineto +290.0293 72.2392 lineto +closepath fill +1 setlinewidth +solid +0 0 0 edgecolor +newpath 283.8187 75.4687 moveto +291.5376 82.7261 lineto +290.0293 72.2392 lineto +closepath stroke +grestore +% Node2 +gsave +1 setlinewidth +0.043137 0.68627 1 nodecolor +newpath 339 46 moveto +309.205 11.5 lineto +368.795 11.5 lineto +closepath stroke +0 0 0 nodecolor +14 /Times-Roman set_font +335.5 19.3 moveto 7 (b) alignedtext +grestore +% Node6->Node2 +gsave +1 setlinewidth +solid +0 0 0 edgecolor +newpath 313.1414 73.7282 moveto +319.2973 61.8898 326.4027 48.2257 331.6056 38.2199 curveto +stroke +0 0 0 edgecolor +newpath 309.9707 72.2392 moveto +308.4624 82.7261 lineto +316.1813 75.4687 lineto +closepath fill +1 setlinewidth +solid +0 0 0 edgecolor +newpath 309.9707 72.2392 moveto +308.4624 82.7261 lineto +316.1813 75.4687 lineto +closepath stroke +grestore +% Node3 +gsave +1 setlinewidth +0.043137 0.68627 1 nodecolor +newpath 417 46 moveto +387.205 11.5 lineto +446.795 11.5 lineto +closepath stroke +0 0 0 nodecolor +14 /Times-Roman set_font +413.5 19.3 moveto 7 (c) alignedtext +grestore +endpage +showpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +%%BoundingBox: 37 212 575 580 +end +restore +%%EOF diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt new file mode 100644 index 000000000..5a187fcac --- /dev/null +++ b/test/CMakeLists.txt @@ -0,0 +1 @@ +add_subdirectory(gia) \ No newline at end of file diff --git a/test/gia/CMakeLists.txt b/test/gia/CMakeLists.txt new file mode 100644 index 000000000..c9022dc8c --- /dev/null +++ b/test/gia/CMakeLists.txt @@ -0,0 +1,11 @@ +add_executable(gia_test gia_test.cc) + +target_link_libraries(gia_test + gtest + gtest_main + libabc +) + +gtest_discover_tests(gia_test + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} +) \ No newline at end of file diff --git a/test/gia/gia_test.cc b/test/gia/gia_test.cc new file mode 100644 index 000000000..a6b288f79 --- /dev/null +++ b/test/gia/gia_test.cc @@ -0,0 +1,54 @@ +#include "gtest/gtest.h" + +#include "aig/gia/gia.h" + +ABC_NAMESPACE_IMPL_START + +TEST(GiaTest, CanAllocateGiaManager) { + Gia_Man_t* aig_manager = Gia_ManStart(100); + + EXPECT_TRUE(aig_manager != nullptr); + Gia_ManStop(aig_manager); +} + +TEST(GiaTest, CanAddACi) { + Gia_Man_t* aig_manager = Gia_ManStart(100); + Gia_ManAppendCi(aig_manager); + + EXPECT_EQ(Gia_ManCiNum(aig_manager), 1); + Gia_ManStop(aig_manager); +} + +TEST(GiaTest, CanAddACo) { + Gia_Man_t* aig_manager = Gia_ManStart(100); + int input1 = Gia_ManAppendCi(aig_manager); + Gia_ManAppendCo(aig_manager, input1); + + EXPECT_EQ(Gia_ManCiNum(aig_manager), 1); + EXPECT_EQ(Gia_ManCoNum(aig_manager), 1); + Gia_ManStop(aig_manager); +} + +TEST(GiaTest, CanAddAnAndGate) { + Gia_Man_t* aig_manager = Gia_ManStart(100); + + int input1 = Gia_ManAppendCi(aig_manager); + int input2 = Gia_ManAppendCi(aig_manager); + + int and_output = Gia_ManAppendAnd(aig_manager, input1, input2); + Gia_ManAppendCo(aig_manager, and_output); + + Vec_Wrd_t* stimulus = Vec_WrdAlloc(2); + Vec_WrdPush(stimulus, /*A*/1); + Vec_WrdPush(stimulus, /*B*/1); + Vec_Wrd_t* output = Gia_ManSimPatSimOut(aig_manager, stimulus, /*fouts*/1); + + EXPECT_EQ(Gia_ManCiNum(aig_manager), 2); + EXPECT_EQ(Gia_ManCoNum(aig_manager), 1); + // A = 1, B = 1 -> A & B == 1 + EXPECT_EQ(Vec_WrdGetEntry(output, 0), 1); + Vec_WrdFree(output); + Gia_ManStop(aig_manager); +} + +ABC_NAMESPACE_IMPL_END