diff --git a/.gitignore b/.gitignore index 203869de1..c745dfb57 100644 --- a/.gitignore +++ b/.gitignore @@ -6,6 +6,7 @@ ReleaseLib/ ReleaseExe/ ReleaseExt/ +_/ _TEST/ lib/abc* lib/m114* diff --git a/README.md b/README.md index 358f5ce9a..2bb34cd03 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,19 @@ # ABC: System for Sequential Logic Synthesis and Formal Verification -ABC is always changing but the current snapshot is believed to be stable. +ABC is always changing but the current snapshot is believed to be stable. + +## ABC fork with new features + +Here is a [fork](https://github.com/yongshiwo/abc.git) of ABC containing Agdmap, a novel technology mapper for LUT-based FPGAs. Agdmap is based on a technology mapping algorithm with adaptive gate decomposition [1]. It is a cut enumeration based mapping algorithm with bin packing for simultaneous wide gate decomposition, which is a patent pending technology. + +The mapper is developed and maintained by Longfei Fan and Prof. Chang Wu at Fudan University in Shanghai, China. The experimental results presented in [1] indicate that Agdmap can substantially improve area (by 10% or more) when compared against the best LUT mapping solutions in ABC, such as command "if". + +The source code is provided for research and evaluation only. For commercial usage, please contact Prof. Chang Wu at wuchang@fudan.edu.cn. + +References: + +[1] L. Fan and C. Wu, "FPGA technology mapping with adaptive gate decompostion", ACM/SIGDA FPGA International Symposium on FPGAs, 2023. ## Compiling: diff --git a/abclib.dsp b/abclib.dsp index 0fd96a8b8..7433c5139 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -387,6 +387,10 @@ SOURCE=.\src\base\abci\abcOrder.c # End Source File # Begin Source File +SOURCE=.\src\base\abci\abcOrchestration.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abci\abcPart.c # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index fed64b1ad..d4edc1237 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1527,7 +1527,7 @@ extern void Gia_ManPrintStatsMiter( Gia_Man_t * p, int fVerbose ) extern void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs ); extern void Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew ); extern void Gia_ManPrintNpnClasses( Gia_Man_t * p ); -extern void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs ); +extern void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter ); /*=== giaMem.c ===========================================================*/ extern Gia_MmFixed_t * Gia_MmFixedStart( int nEntrySize, int nEntriesMax ); extern void Gia_MmFixedStop( Gia_MmFixed_t * p, int fVerbose ); diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index aafe311b1..e3967e0ed 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -953,9 +953,12 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi } } pInit[i] = 0; - pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, fGiaSimple, 1 ); - pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0; - Gia_ManStop( pTemp ); + if ( !fSkipStrash ) + { + pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, fGiaSimple, 1 ); + pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0; + Gia_ManStop( pTemp ); + } ABC_FREE( pInit ); } Vec_IntFreeP( &vInits ); diff --git a/src/aig/gia/giaCTas.c b/src/aig/gia/giaCTas.c index 3dded68b3..cd0b4f480 100644 --- a/src/aig/gia/giaCTas.c +++ b/src/aig/gia/giaCTas.c @@ -1778,6 +1778,7 @@ void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Ve Tas_ManSatPrintStats( p ); Tas_ManStop( p ); Vec_PtrFree( vPres ); + Vec_StrFree( vStatus ); } diff --git a/src/aig/gia/giaDeep.c b/src/aig/gia/giaDeep.c index 815a546e4..b58169f42 100644 --- a/src/aig/gia/giaDeep.c +++ b/src/aig/gia/giaDeep.c @@ -120,6 +120,7 @@ Gia_Man_t * Gia_ManDeepSynOne( int nNoImpr, int TimeOut, int nAnds, int Seed, in } if ( nTimeToStop && Abc_Clock() > nTimeToStop ) { + if ( !Abc_FrameIsBatchMode() ) printf( "Runtime limit (%d sec) is reached after %d iterations.\n", TimeOut, i ); break; } diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 35ad6aab9..6dee2c26f 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1069,6 +1069,51 @@ Gia_Man_t * Gia_ManDupPiPerm( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManCreatePerm( int n ) +{ + Vec_Int_t * vPerm = Vec_IntStartNatural( n ); + int i, * pPerm = Vec_IntArray( vPerm ); + for ( i = 0; i < n; i++ ) + { + int j = Abc_Random(0) % n; + ABC_SWAP( int, pPerm[i], pPerm[j] ); + + } + return vPerm; +} +Gia_Man_t * Gia_ManDupRandPerm( Gia_Man_t * p ) +{ + Vec_Int_t * vPiPerm = Gia_ManCreatePerm( Gia_ManCiNum(p) ); + Vec_Int_t * vPoPerm = Gia_ManCreatePerm( Gia_ManCoNum(p) ); + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachPi( p, pObj, i ) + Gia_ManPi(p, Vec_IntEntry(vPiPerm,i))->Value = Gia_ManAppendCi(pNew) ^ (Abc_Random(0) & 1); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, Vec_IntEntry(vPoPerm,i))) ^ (Abc_Random(0) & 1) ); + Vec_IntFree( vPiPerm ); + Vec_IntFree( vPoPerm ); + return pNew; +} + /**Function************************************************************* Synopsis [Appends second AIG without any changes.] @@ -1559,6 +1604,47 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates while adding self-loops to the registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupMiterCones( Gia_Man_t * p, Vec_Int_t * vPairs ) +{ + Vec_Int_t * vTemp = Vec_IntAlloc( 100 ); + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, iLit0, iLit1; + pNew = Gia_ManStart( Gia_ManObjNum(p) + 3 * Vec_IntSize(vPairs) ); + pNew->pName = Abc_UtilStrsav( "miter" ); + Gia_ManHashAlloc( pNew ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Vec_IntForEachEntryDouble( vPairs, iLit0, iLit1, i ) + { + int Lit0 = Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(iLit0))->Value, Abc_LitIsCompl(iLit0) ); + int Lit1 = Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(iLit1))->Value, Abc_LitIsCompl(iLit1) ); + Vec_IntPush( vTemp, Gia_ManHashXor(pNew, Lit0, Lit1) ); + } + Vec_IntForEachEntry( vTemp, iLit0, i ) + Gia_ManAppendCo( pNew, iLit0 ); + Vec_IntFree( vTemp ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + /**Function************************************************************* Synopsis [Duplicates the AIG in the DFS order.] @@ -5539,6 +5625,100 @@ void Gia_ManProdAdderGen( int nArgA, int nArgB, int Seed, int fSigned, int fCla Vec_IntFree( vRes ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 ); + pNew->pName = Abc_UtilStrsav(p->pName); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManAppendCo( pNew, 0 ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p)+1 ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) +{ + Vec_Int_t * vLits; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, iLit; + if ( Gia_ManBufNum(p1) == 0 ) { + printf( "The first AIG should have a boundary.\n" ); + return NULL; + } + if ( Gia_ManBufNum(p2) != 0 ) { + printf( "The second AIG should have no boundary.\n" ); + return NULL; + } + assert( Gia_ManBufNum(p1) > 0 ); + assert( Gia_ManBufNum(p2) == 0 ); + assert( Gia_ManRegNum(p1) == 0 ); + assert( Gia_ManRegNum(p2) == 0 ); + assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) ); + assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) ); + vLits = Vec_IntAlloc( Gia_ManBufNum(p1) ); + if ( fVerbose ) + printf( "Creating a boundary miter with %d inputs, %d outputs, and %d buffers.\n", + Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) ); + pNew = Gia_ManStart( Gia_ManObjNum(p1) + Gia_ManObjNum(p2) ); + pNew->pName = ABC_ALLOC( char, strlen(p1->pName) + 10 ); + sprintf( pNew->pName, "%s_bmiter", p1->pName ); + Gia_ManHashStart( pNew ); + Gia_ManConst0(p1)->Value = 0; + Gia_ManConst0(p2)->Value = 0; + Gia_ManForEachCi( p1, pObj, i ) + pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p2, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachAnd( p1, pObj, i ) { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( Gia_ObjIsBuf(pObj) ) + Vec_IntPush( vLits, pObj->Value ); + } + Gia_ManForEachCo( p2, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachCo( p1, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Vec_IntForEachEntry( vLits, iLit, i ) + Gia_ManAppendCo( pNew, iLit ); + Vec_IntFree( vLits ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaKf.c b/src/aig/gia/giaKf.c index a823f7262..6909851f1 100644 --- a/src/aig/gia/giaKf.c +++ b/src/aig/gia/giaKf.c @@ -21,13 +21,18 @@ #include "gia.h" #include "misc/vec/vecSet.h" +#ifdef _MSC_VER +#define unlink _unlink +#else +#include +#endif + #ifdef ABC_USE_PTHREADS #ifdef _WIN32 #include "../lib/pthread.h" #else #include -#include #endif #endif diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index ec733b852..e8f9bca32 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -803,7 +803,7 @@ void Gia_ManPrintNpnClasses( Gia_Man_t * p ) Vec_Int_t * vLeaves, * vTruth, * vVisited; int * pLutClass, ClassCounts[222] = {0}; int i, k, iFan, Class, OtherClasses, OtherClasses2, nTotal, Counter, Counter2; - unsigned * pTruth; + unsigned * pTruth; int nLutSize = 0; assert( Gia_ManHasMapping(p) ); assert( Gia_ManLutSizeMax( p ) <= 4 ); vLeaves = Vec_IntAlloc( 100 ); @@ -813,6 +813,7 @@ void Gia_ManPrintNpnClasses( Gia_Man_t * p ) Gia_ManCleanTruth( p ); Gia_ManForEachLut( p, i ) { + nLutSize = Abc_MaxInt( nLutSize, Gia_ObjLutSize(p,i) ); if ( Gia_ObjLutSize(p,i) > 4 ) continue; Vec_IntClear( vLeaves ); @@ -872,6 +873,55 @@ void Gia_ManPrintNpnClasses( Gia_Man_t * p ) Abc_Print( 1, "Approximate number of 4:1 MUX structures: All = %6d (%7.2f %%) MFFC = %6d (%7.2f %%)\n", OtherClasses, 100.0 * OtherClasses / (nTotal+1), OtherClasses2, 100.0 * OtherClasses2 / (nTotal+1) ); + // print information about LUT pairs + if ( nLutSize <= 4 ) + { + int nTopPairs = 100, nTopShow = 30; + int i, j, k, iFan, * pVec = NULL; + Vec_Int_t * vPairs = Vec_IntAlloc( 3 * nTopPairs ); + Gia_ManForEachLut( p, j ) { + Gia_LutForEachFanin( p, j, iFan, k ) { + int Num1 = pLutClass[iFan]; + int Num2 = pLutClass[j]; + assert( Vec_IntSize(vPairs) % 3 == 0 ); + for ( i = 0; i < Vec_IntSize(vPairs); i += 3 ) + if ( Vec_IntEntry(vPairs, i+0) == Num1 && Vec_IntEntry(vPairs, i+1) == Num2 ) + break; + if ( i == Vec_IntSize(vPairs) ) { + if ( Vec_IntSize(vPairs) < 3*nTopPairs ) { + Vec_IntPush( vPairs, Num1 ); + Vec_IntPush( vPairs, Num2 ); + Vec_IntPush( vPairs, 1 ); + } + continue; + } + // found this pair + assert( Vec_IntEntry(vPairs, i+0) == Num1 ); + assert( Vec_IntEntry(vPairs, i+1) == Num2 ); + Vec_IntAddToEntry( vPairs, i+2, 1 ); + // sort + pVec = Vec_IntArray( vPairs ); + while ( i > 0 && pVec[i+2] > pVec[i-1] ) { + ABC_SWAP( int, pVec[i+0], pVec[i-3] ) + ABC_SWAP( int, pVec[i+1], pVec[i-2] ) + ABC_SWAP( int, pVec[i+2], pVec[i-1] ) + i -= 3; + } + while ( i < Vec_IntSize(vPairs) - 3 && pVec[i+2] < pVec[i+5] ) { + ABC_SWAP( int, pVec[i+0], pVec[i+3] ) + ABC_SWAP( int, pVec[i+1], pVec[i+4] ) + ABC_SWAP( int, pVec[i+2], pVec[i+5] ) + i += 3; + assert( 0 ); + } + } + } + pVec = Vec_IntArray( vPairs ); + nTopShow = Abc_MinInt( nTopShow, Vec_IntSize(vPairs)/3 ); + for ( i = 0; i < 3*nTopShow; i += 3 ) + printf( "%3d : (%3d %3d) x %3d\n", i/3, pVec[i+0], pVec[i+1], pVec[i+2] ); + Vec_IntFree( vPairs ); + } ABC_FREE( pLutClass ); } @@ -1191,6 +1241,90 @@ void Gia_ManDfsSlacksPrint( Gia_Man_t * p ) } +/**Function************************************************************* + + Synopsis [Dump interface module] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManWriteNamesInter( FILE * pFile, char c, int n, int Start, int Skip, int nRegs ) +{ + int Length = Start, i, fFirst = 1; + char pName[100]; + for ( i = 0; i < n-nRegs; i++ ) + { + sprintf( pName, "%c[%d]", c, i ); + Length += strlen(pName) + 2; + if ( Length > 60 ) + { + fprintf( pFile, ",\n " ); + Length = Skip; + fFirst = 1; + } + fprintf( pFile, "%s%s", fFirst ? "":", ", pName ); + fFirst = 0; + } + for ( i = n-nRegs; i < n; i++ ) + { + sprintf( pName, "%c%c[%d]", c, c, i ); + Length += strlen(pName) + 2; + if ( Length > 60 ) + { + fprintf( pFile, ",\n " ); + Length = Skip; + fFirst = 1; + } + fprintf( pFile, "%s%s", fFirst ? "":", ", pName ); + fFirst = 0; + }} +void Gia_ManDumpModuleName( FILE * pFile, char * pName ) +{ + int i; + for ( i = 0; i < (int)strlen(pName); i++ ) + if ( isalpha(pName[i]) || isdigit(pName[i]) ) + fprintf( pFile, "%c", pName[i] ); + else + fprintf( pFile, "_" ); +} +void Gia_ManDumpInterface( Gia_Man_t * p, FILE * pFile ) +{ + int fPrintClk = 0; + fprintf( pFile, "module " ); + Gia_ManDumpModuleName( pFile, p->pName ); + fprintf( pFile, "_wrapper" ); + fprintf( pFile, " (%s i, o );\n\n", fPrintClk && Gia_ManRegNum(p) ? " clk," : "" ); + if ( fPrintClk && Gia_ManRegNum(p) ) + fprintf( pFile, " input clk;\n" ); + fprintf( pFile, " input [%d:0] i;\n", Gia_ManPiNum(p)-1 ); + fprintf( pFile, " output [%d:0] o;\n\n", Gia_ManPoNum(p)-1 ); + + if ( Gia_ManRegNum(p) ) { + fprintf( pFile, " wire [%d:%d] ii;\n", Gia_ManCiNum(p)-1, Gia_ManPiNum(p) ); + fprintf( pFile, " wire [%d:%d] oo;\n\n", Gia_ManCoNum(p)-1, Gia_ManPoNum(p) ); + fprintf( pFile, " always @ (posedge %s)\n ii <= oo;\n\n", fPrintClk ? "clk" : "i[0]" ); + } + + fprintf( pFile, " " ); + Gia_ManDumpModuleName( pFile, p->pName ); + fprintf( pFile, " " ); + Gia_ManDumpModuleName( pFile, p->pName ); + fprintf( pFile, "_inst" ); + + fprintf( pFile, " (\n " ); + Gia_ManWriteNamesInter( pFile, 'i', Gia_ManCiNum(p), 4, 4, Gia_ManRegNum(p) ); + fprintf( pFile, ",\n " ); + Gia_ManWriteNamesInter( pFile, 'o', Gia_ManCoNum(p), 4, 4, Gia_ManRegNum(p) ); + fprintf( pFile, "\n );\n\n" ); + + fprintf( pFile, "endmodule\n\n" ); +} + + /**Function************************************************************* Synopsis [Compute arrival/required times.] @@ -1273,38 +1407,33 @@ void Gia_ManWriteNames( FILE * pFile, char c, int n, Vec_Ptr_t * vNames, int Sta fFirst = 0; } } -void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs ) +void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter ) { - FILE * pFile; Gia_Obj_t * pObj; Vec_Bit_t * vInvs, * vUsed; int nDigits = Abc_Base10Log( Gia_ManObjNum(p) ); int nDigitsI = Abc_Base10Log( Gia_ManPiNum(p) ); int nDigitsO = Abc_Base10Log( Gia_ManPoNum(p) ); - int i, k, iObj; - if ( Gia_ManRegNum(p) ) - { - printf( "Currently cannot write sequential AIG.\n" ); - return; - } - pFile = fopen( pFileName, "wb" ); + int i, k, iObj, nRegs = Gia_ManRegNum(p); + FILE * pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) { printf( "Cannot open output file \"%s\".\n", pFileName ); return; } + if ( fInter || nRegs ) + Gia_ManDumpInterface( p, pFile ); + //Gia_ManSetRegNum( p, 0 ); + p->nRegs = 0; + vInvs = Gia_ManGenUsed( p, 0 ); vUsed = Gia_ManGenUsed( p, 1 ); //fprintf( pFile, "// This Verilog file is written by ABC on %s\n\n", Extra_TimeStamp() ); fprintf( pFile, "module " ); - for ( i = 0; i < (int)strlen(p->pName); i++ ) - if ( isalpha(p->pName[i]) || isdigit(p->pName[i]) ) - fprintf( pFile, "%c", p->pName[i] ); - else - fprintf( pFile, "_" ); + Gia_ManDumpModuleName( pFile, p->pName ); if ( fVerBufs ) { @@ -1455,6 +1584,8 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int Vec_BitFree( vInvs ); Vec_BitFree( vUsed ); + + Gia_ManSetRegNum( p, nRegs ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c index 6ba85706d..c0473fea3 100644 --- a/src/aig/gia/giaMini.c +++ b/src/aig/gia/giaMini.c @@ -813,6 +813,13 @@ int * Abc_FrameReadMiniAigEquivClasses( Abc_Frame_t * pAbc ) printf( "Equivalence classes of internal GIA are not available.\n" ); return NULL; } + else if ( 0 ) + { + int i; + for ( i = 1; i < Gia_ManObjNum(pAbc->pGia2); i++ ) + if ( Gia_ObjHasRepr(pAbc->pGia2, i) ) + printf( "Obj %3d : Repr %3d Proved %d Failed %d\n", i, Gia_ObjRepr(pAbc->pGia2, i), Gia_ObjProved(pAbc->pGia2, i), Gia_ObjFailed(pAbc->pGia2, i) ); + } if ( Gia_ManObjNum(pAbc->pGia2) != Gia_ManObjNum(pAbc->pGiaMiniAig) ) printf( "Internal GIA with equivalence classes is not directly derived from MiniAig.\n" ); // derive the set of equivalent node pairs diff --git a/src/aig/gia/giaSatMap.c b/src/aig/gia/giaSatMap.c index 5c17b74eb..a73950fba 100644 --- a/src/aig/gia/giaSatMap.c +++ b/src/aig/gia/giaSatMap.c @@ -269,6 +269,118 @@ static inline int sat_solver_add_and2( sat_solver * pSat, int iVar, int iVar0, i return 3; } + +/**Function************************************************************* + + Synopsis [Adds a general cardinality constraint in terms of vVars.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Card_AddClause( Vec_Int_t * p, int* begin, int* end ) +{ + Vec_IntPush( p, (int)(end-begin) ); + while ( begin < end ) + Vec_IntPush( p, (int)*begin++ ); + return 1; +} +static inline int Card_AddHalfSorter( Vec_Int_t * p, int iVarA, int iVarB, int iVar0, int iVar1 ) +{ + lit Lits[3]; + int Cid; + + Lits[0] = toLitCond( iVarA, 0 ); + Lits[1] = toLitCond( iVar0, 1 ); + Cid = Card_AddClause( p, Lits, Lits + 2 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarA, 0 ); + Lits[1] = toLitCond( iVar1, 1 ); + Cid = Card_AddClause( p, Lits, Lits + 2 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarB, 0 ); + Lits[1] = toLitCond( iVar0, 1 ); + Lits[2] = toLitCond( iVar1, 1 ); + Cid = Card_AddClause( p, Lits, Lits + 3 ); + assert( Cid ); + return 3; +} +static inline void Card_AddSorter( Vec_Int_t * p, int * pVars, int i, int k, int * pnVars ) +{ + int iVar1 = (*pnVars)++; + int iVar2 = (*pnVars)++; + Card_AddHalfSorter( p, iVar1, iVar2, pVars[i], pVars[k] ); + pVars[i] = iVar1; + pVars[k] = iVar2; +} +static inline void Card_AddCardinConstrMerge( Vec_Int_t * p, int * pVars, int lo, int hi, int r, int * pnVars ) +{ + int i, step = r * 2; + if ( step < hi - lo ) + { + Card_AddCardinConstrMerge( p, pVars, lo, hi-r, step, pnVars ); + Card_AddCardinConstrMerge( p, pVars, lo+r, hi, step, pnVars ); + for ( i = lo+r; i < hi-r; i += step ) + Card_AddSorter( p, pVars, i, i+r, pnVars ); + for ( i = lo+r; i < hi-r-1; i += r ) + { + lit Lits[2] = { Abc_Var2Lit(pVars[i], 0), Abc_Var2Lit(pVars[i+r], 1) }; + int Cid = Card_AddClause( p, Lits, Lits + 2 ); + assert( Cid ); + } + } +} +static inline void Card_AddCardinConstrRange( Vec_Int_t * p, int * pVars, int lo, int hi, int * pnVars ) +{ + if ( hi - lo >= 1 ) + { + int i, mid = lo + (hi - lo) / 2; + for ( i = lo; i <= mid; i++ ) + Card_AddSorter( p, pVars, i, i + (hi - lo + 1) / 2, pnVars ); + Card_AddCardinConstrRange( p, pVars, lo, mid, pnVars ); + Card_AddCardinConstrRange( p, pVars, mid+1, hi, pnVars ); + Card_AddCardinConstrMerge( p, pVars, lo, hi, 1, pnVars ); + } +} +int Card_AddCardinConstrPairWise( Vec_Int_t * p, Vec_Int_t * vVars ) +{ + int nVars = Vec_IntSize(vVars); + Card_AddCardinConstrRange( p, Vec_IntArray(vVars), 0, nVars - 1, &nVars ); + return nVars; +} +int Card_AddCardinSolver( int LogN, Vec_Int_t ** pvVars, Vec_Int_t ** pvRes ) +{ + int nVars = 1 << LogN; + int nVarsAlloc = nVars + 2 * (nVars * LogN * (LogN-1) / 4 + nVars - 1); + Vec_Int_t * vRes = Vec_IntAlloc( 1000 ); + Vec_Int_t * vVars = Vec_IntStartNatural( nVars ); + int nVarsReal = Card_AddCardinConstrPairWise( vRes, vVars ); + assert( nVarsReal == nVarsAlloc ); + Vec_IntPush( vRes, -1 ); + *pvVars = vVars; + *pvRes = vRes; + return nVarsReal; +} +sat_solver * Sbm_AddCardinSolver2( int LogN, Vec_Int_t ** pvVars, Vec_Int_t ** pvRes ) +{ + Vec_Int_t * vVars = NULL; + Vec_Int_t * vRes = NULL; + int nVarsReal = Card_AddCardinSolver( LogN, &vVars, &vRes ), i, size; + sat_solver * pSat = sat_solver_new(); + sat_solver_setnvars( pSat, nVarsReal ); + for ( i = 0, size = Vec_IntEntry(vRes, i++); i < Vec_IntSize(vRes); i += size, size = Vec_IntEntry(vRes, i++) ) + sat_solver_addclause( pSat, Vec_IntEntryP(vRes, i), Vec_IntEntryP(vRes, i+size) ); + if ( pvVars ) *pvVars = vVars; + if ( pvRes ) *pvRes = vRes; + return pSat; +} + + /**Function************************************************************* Synopsis [Adds a general cardinality constraint in terms of vVars.] diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index 47f645413..97335d378 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -3689,6 +3689,58 @@ Vec_Str_t * Gia_ManComputeRange( Gia_Man_t * p ) return vOut; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManComparePrint( Gia_Man_t * p, Gia_Man_t * q ) +{ + Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) ); + Vec_Wrd_t * vSimsP = Gia_ManSimPatSimOut( p, vSimsPi, 0 ); + Vec_Wrd_t * vSimsQ = Gia_ManSimPatSimOut( q, vSimsPi, 0 ); + int i, k, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p), Count = 0; + Gia_Obj_t * pObjP, * pObjQ; + Gia_ManSetPhase( p ); + Gia_ManSetPhase( q ); + Gia_ManForEachObj( p, pObjP, i ) { + word * pSim = Vec_WrdEntryP( vSimsP, i * nWords ); + if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords ); + } + Gia_ManForEachObj( q, pObjQ, i ) { + word * pSim = Vec_WrdEntryP( vSimsQ, i * nWords ); + if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords ); + } + Gia_ManForEachAnd( q, pObjQ, i ) { + word * pSimQ = Vec_WrdEntryP( vSimsQ, i * nWords ); + int fFirst = 1; + Gia_ManForEachObj( p, pObjP, k ) { + word * pSimP = Vec_WrdEntryP( vSimsP, k * nWords ); + if ( !Abc_TtEqual(pSimQ, pSimP, nWords) ) + continue; + if ( fFirst ) { + printf( "%5d :", i ); + fFirst = 0; + Count++; + } + printf( " %5d(%d)", k, pObjQ->fPhase ^ pObjP->fPhase ); + } + if ( !fFirst ) + printf( "\n"); + } + printf( "Found %d equivalent nodes.\n", Count ); + Vec_WrdFree( vSimsP ); + Vec_WrdFree( vSimsQ ); + Vec_WrdFree( vSimsPi ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaStoch.c b/src/aig/gia/giaStoch.c index 94f539988..78fe2cb67 100644 --- a/src/aig/gia/giaStoch.c +++ b/src/aig/gia/giaStoch.c @@ -22,6 +22,23 @@ #include "base/main/main.h" #include "base/cmd/cmd.h" +#ifdef _MSC_VER +#define unlink _unlink +#else +#include +#endif + +#ifdef ABC_USE_PTHREADS + +#ifdef _WIN32 +#include "../lib/pthread.h" +#else +#include +#endif + +#endif + + ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// @@ -32,6 +49,169 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Processing on a single core.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_StochProcessOne( Gia_Man_t * p, char * pScript, int Rand, int TimeSecs ) +{ + Gia_Man_t * pNew; + char FileName[100], Command[1000]; + sprintf( FileName, "%06x.aig", Rand ); + Gia_AigerWrite( p, FileName, 0, 0, 0 ); + sprintf( Command, "./abc -q \"&read %s; %s; &write %s\"", FileName, pScript, FileName ); + if ( system( (char *)Command ) ) + { + fprintf( stderr, "The following command has returned non-zero exit status:\n" ); + fprintf( stderr, "\"%s\"\n", (char *)Command ); + fprintf( stderr, "Sorry for the inconvenience.\n" ); + fflush( stdout ); + unlink( FileName ); + return Gia_ManDup(p); + } + pNew = Gia_AigerRead( FileName, 0, 0, 0 ); + unlink( FileName ); + if ( pNew && Gia_ManAndNum(pNew) < Gia_ManAndNum(p) ) + return pNew; + Gia_ManStopP( &pNew ); + return Gia_ManDup(p); +} +void Gia_StochProcessArray( Vec_Ptr_t * vGias, char * pScript, int TimeSecs, int fVerbose ) +{ + Gia_Man_t * pGia, * pNew; int i; + Vec_Int_t * vRands = Vec_IntAlloc( Vec_PtrSize(vGias) ); + Abc_Random(1); + for ( i = 0; i < Vec_PtrSize(vGias); i++ ) + Vec_IntPush( vRands, Abc_Random(0) % 0x1000000 ); + Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i ) + { + pNew = Gia_StochProcessOne( pGia, pScript, Vec_IntEntry(vRands, i), TimeSecs ); + Gia_ManStop( pGia ); + Vec_PtrWriteEntry( vGias, i, pNew ); + } + Vec_IntFree( vRands ); +} + +/**Function************************************************************* + + Synopsis [Processing on a many cores.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +#ifndef ABC_USE_PTHREADS + +void Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSecs, int fVerbose ) +{ + Gia_StochProcessArray( vGias, pScript, TimeSecs, fVerbose ); +} + +#else // pthreads are used + + +#define PAR_THR_MAX 100 +typedef struct Gia_StochThData_t_ +{ + Vec_Ptr_t * vGias; + char * pScript; + int Index; + int Rand; + int nTimeOut; + int fWorking; +} Gia_StochThData_t; + +void * Gia_StochWorkerThread( void * pArg ) +{ + Gia_StochThData_t * pThData = (Gia_StochThData_t *)pArg; + volatile int * pPlace = &pThData->fWorking; + Gia_Man_t * pGia, * pNew; + while ( 1 ) + { + while ( *pPlace == 0 ); + assert( pThData->fWorking ); + if ( pThData->Index == -1 ) + { + pthread_exit( NULL ); + assert( 0 ); + return NULL; + } + pGia = (Gia_Man_t *)Vec_PtrEntry( pThData->vGias, pThData->Index ); + pNew = Gia_StochProcessOne( pGia, pThData->pScript, pThData->Rand, pThData->nTimeOut ); + Gia_ManStop( pGia ); + Vec_PtrWriteEntry( pThData->vGias, pThData->Index, pNew ); + pThData->fWorking = 0; + } + assert( 0 ); + return NULL; +} + +void Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSecs, int fVerbose ) +{ + Gia_StochThData_t ThData[PAR_THR_MAX]; + pthread_t WorkerThread[PAR_THR_MAX]; + int i, k, status; + if ( fVerbose ) + printf( "Running concurrent synthesis with %d processes.\n", nProcs ); + fflush( stdout ); + if ( nProcs < 2 ) + return Gia_StochProcessArray( vGias, pScript, TimeSecs, fVerbose ); + // subtract manager thread + nProcs--; + assert( nProcs >= 1 && nProcs <= PAR_THR_MAX ); + // start threads + Abc_Random(1); + for ( i = 0; i < nProcs; i++ ) + { + ThData[i].vGias = vGias; + ThData[i].pScript = pScript; + ThData[i].Index = -1; + ThData[i].Rand = Abc_Random(0) % 0x1000000; + ThData[i].nTimeOut = TimeSecs; + ThData[i].fWorking = 0; + status = pthread_create( WorkerThread + i, NULL, Gia_StochWorkerThread, (void *)(ThData + i) ); assert( status == 0 ); + } + // look at the threads + for ( k = 0; k < Vec_PtrSize(vGias); k++ ) + { + for ( i = 0; i < nProcs; i++ ) + { + if ( ThData[i].fWorking ) + continue; + ThData[i].Index = k; + ThData[i].fWorking = 1; + break; + } + if ( i == nProcs ) + k--; + } + // wait till threads finish + for ( i = 0; i < nProcs; i++ ) + if ( ThData[i].fWorking ) + i = -1; + // stop threads + for ( i = 0; i < nProcs; i++ ) + { + assert( !ThData[i].fWorking ); + // stop + ThData[i].Index = -1; + ThData[i].fWorking = 1; + } +} + +#endif // pthreads are used + + /**Function************************************************************* Synopsis [] @@ -184,7 +364,7 @@ Gia_Man_t * Gia_ManDupDivideOne( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vA pNew->vMapping = vMapping; return pNew; } -Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, char * pScript ) +Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, char * pScript, int nProcs, int TimeOut ) { Vec_Ptr_t * vAigs = Vec_PtrAlloc( Vec_WecSize(vCis) ); int i; for ( i = 0; i < Vec_WecSize(vCis); i++ ) @@ -192,7 +372,8 @@ Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds Gia_ManCollectNodes( p, Vec_WecEntry(vCis, i), Vec_WecEntry(vAnds, i), Vec_WecEntry(vCos, i) ); Vec_PtrPush( vAigs, Gia_ManDupDivideOne(p, Vec_WecEntry(vCis, i), Vec_WecEntry(vAnds, i), Vec_WecEntry(vCos, i)) ); } - Gia_ManStochSynthesis( vAigs, pScript ); + //Gia_ManStochSynthesis( vAigs, pScript ); + Gia_StochProcess( vAigs, pScript, nProcs, TimeOut, 0 ); return vAigs; } Gia_Man_t * Gia_ManDupStitch( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, Vec_Ptr_t * vAigs, int fHash ) @@ -388,7 +569,7 @@ Vec_Wec_t * Gia_ManStochOutputs( Gia_Man_t * p, Vec_Wec_t * vAnds ) SeeAlso [] ***********************************************************************/ -void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript ) +void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs ) { abctime nTimeToStop = TimeOut ? Abc_Clock() + TimeOut * CLOCKS_PER_SEC : 0; abctime clkStart = Abc_Clock(); @@ -407,7 +588,7 @@ void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerb Vec_Wec_t * vAnds = Gia_ManStochNodes( pGia, nMaxSize, Abc_Random(0) & 0x7FFFFFFF ); Vec_Wec_t * vIns = Gia_ManStochInputs( pGia, vAnds ); Vec_Wec_t * vOuts = Gia_ManStochOutputs( pGia, vAnds ); - Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript ); + Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript, nProcs, TimeOut ); Gia_Man_t * pNew = Gia_ManDupStitchMap( pGia, vIns, vAnds, vOuts, vAigs ); int fMapped = Gia_ManHasMapping(pGia) && Gia_ManHasMapping(pNew); Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew ); diff --git a/src/aig/gia/giaTranStoch.c b/src/aig/gia/giaTranStoch.c index efc358dde..aa600c0c0 100644 --- a/src/aig/gia/giaTranStoch.c +++ b/src/aig/gia/giaTranStoch.c @@ -29,13 +29,18 @@ #include #include +#ifdef _MSC_VER +#define unlink _unlink +#else +#include +#endif + #ifdef ABC_USE_PTHREADS #ifdef _WIN32 #include "../lib/pthread.h" #else #include -#include #endif #endif diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c index 7b8d488a6..7ab8486e4 100644 --- a/src/aig/saig/saigIso.c +++ b/src/aig/saig/saigIso.c @@ -493,7 +493,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV // report the results // Vec_VecPrintInt( (Vec_Vec_t *)vClasses ); -// printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) ); +// printf( "Divided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) ); /* if ( fVerbose ) { diff --git a/src/aig/saig/saigIsoFast.c b/src/aig/saig/saigIsoFast.c index 10d1384da..90a04df37 100644 --- a/src/aig/saig/saigIsoFast.c +++ b/src/aig/saig/saigIsoFast.c @@ -328,7 +328,7 @@ Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig ) // report the results // Vec_VecPrintInt( (Vec_Vec_t *)vClasses ); - printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) ); + printf( "Divided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) ); Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i ) if ( Vec_IntSize(vLevel) > 1 ) diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index 598103de9..5b15f9329 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -946,7 +946,7 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) if ( (pFlop0->fMarkA && pFlop0->fMarkB) || (pFlop1->fMarkA && pFlop1->fMarkB) || (pFlop0->fMarkA && pFlop1->fMarkA) || (pFlop0->fMarkB && pFlop1->fMarkB) ) - printf( "Ouput pair %4d: Difficult case...\n", i/2 ); + printf( "Output pair %4d: Difficult case...\n", i/2 ); if ( pFlop0->fMarkB ) { diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c index 3621cdd3b..18df50079 100644 --- a/src/aig/saig/saigSimMv.c +++ b/src/aig/saig/saigSimMv.c @@ -903,14 +903,14 @@ ABC_PRT( "Constructing the problem", Abc_Clock() - clk ); if ( f == nFramesSatur ) { if ( fVerbose ) - printf( "Begining to saturate simulation after %d frames\n", f ); + printf( "Beginning to saturate simulation after %d frames\n", f ); // find all flops that have at least one X value in the past and set them to X forever p->vXFlops = Saig_MvManFindXFlops( p ); } if ( f == 2 * nFramesSatur ) { if ( fVerbose ) - printf( "Agressively saturating simulation after %d frames\n", f ); + printf( "Aggressively saturating simulation after %d frames\n", f ); Vec_IntFree( p->vXFlops ); p->vXFlops = Saig_MvManCreateNextSkip( p ); } diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c index 217d32692..6d6a2f226 100644 --- a/src/aig/saig/saigTrans.c +++ b/src/aig/saig/saigTrans.c @@ -6,7 +6,7 @@ PackageName [Sequential AIG package.] - Synopsis [Dynamic simplication of the transition relation.] + Synopsis [Dynamic simplification of the transition relation.] Author [Alan Mishchenko] diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 636fe30ae..e3f3ce457 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -860,7 +860,8 @@ int Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fU pOld = (Abc_Obj_t *)Vec_PtrPop( pMan->vStackReplaceOld ); pNew = (Abc_Obj_t *)Vec_PtrPop( pMan->vStackReplaceNew ); if ( Abc_ObjFanoutNum(pOld) == 0 ) - return 0; + //return 0; + continue; Abc_AigReplace_int( pMan, pOld, pNew, fUpdateLevel ); } if ( fUpdateLevel ) @@ -897,7 +898,20 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i { if ( Abc_ObjIsCo(pFanout) ) { - Abc_ObjPatchFanin( pFanout, pOld, pNew ); + pFanin1 = Abc_ObjRegular( pNew ); + if ( pFanin1->fMarkB ) + Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pFanin1 ); + if ( fUpdateLevel && pMan->pNtkAig->vLevelsR ) + { + Abc_ObjSetReverseLevel( pFanin1, Abc_ObjReverseLevel(pOld) ); + assert( pFanin1->fMarkB == 0 ); + if ( !Abc_ObjIsCi(pFanin1) ) + { + pFanin1->fMarkB = 1; + Vec_VecPush( pMan->vLevelsR, Abc_ObjReverseLevel(pFanin1), pFanin1 ); + } + } + Abc_ObjPatchFanin( pFanout, pOld, pNew ); continue; } // find the old node as a fanin of this fanout diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index 84ecf7bf3..805b91daa 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -1265,6 +1265,42 @@ int Abc_NtkToAig( Abc_Ntk_t * pNtk ) } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ObjFaninSort( Abc_Obj_t * pObj ) +{ + Vec_Int_t * vFanins = Abc_ObjFaninVec( pObj ); + char * pCube, * pSop = (char*)pObj->pData; + int i, j, nVars = Abc_SopGetVarNum( pSop ); + assert( nVars == Vec_IntSize(vFanins) ); + for ( i = 0; i < Vec_IntSize(vFanins); i++ ) + for ( j = i+1; j < Vec_IntSize(vFanins); j++ ) + { + if ( Vec_IntEntry(vFanins, i) < Vec_IntEntry(vFanins, j) ) + continue; + ABC_SWAP( int, Vec_IntArray(vFanins)[i], Vec_IntArray(vFanins)[j] ); + for ( pCube = pSop; *pCube; pCube += nVars + 3 ) { + ABC_SWAP( char, pCube[i], pCube[j] ); + } + } +} +void Abc_NtkFaninSort( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; int i; + assert( Abc_NtkIsSopLogic(pNtk) ); + Abc_NtkForEachNode( pNtk, pObj, i ) + Abc_ObjFaninSort( pObj ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c index d8432382b..653d855fe 100644 --- a/src/base/abc/abcLatch.c +++ b/src/base/abc/abcLatch.c @@ -426,7 +426,7 @@ Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk ) return Abc_NtkDup( pNtk ); if ( nFlops > 16 ) { - printf( "Cannot reencode %d flops because it will lead to 2^%d states.\n", nFlops, nFlops ); + printf( "Cannot re-encode %d flops because it will lead to 2^%d states.\n", nFlops, nFlops ); return NULL; } // check if there are latches with DC values diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c index 75aa51ad9..8a2e9f184 100644 --- a/src/base/abc/abcNetlist.c +++ b/src/base/abc/abcNetlist.c @@ -220,7 +220,7 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk ) if ( pObj->pCopy->pCopy ) // the net of the new object is already created continue; // create the new net - sprintf( Buffer, "new_%s_", Abc_ObjName(pObj) ); + sprintf( Buffer, "new_%s", Abc_ObjName(pObj) ); //pNet = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pObj) ); // here we create net names such as "n48", where 48 is the ID of the node pNet = Abc_NtkFindOrCreateNet( pNtkNew, Buffer ); Abc_ObjAddFanin( pNet, pObj->pCopy ); diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c index 8250102ac..f24c55593 100644 --- a/src/base/abc/abcSop.c +++ b/src/base/abc/abcSop.c @@ -922,6 +922,8 @@ int Abc_SopCheckReadTruth( Vec_Ptr_t * vRes, char * pToken, int fHex ) { char * pBase; int nVars; int Log2 = Abc_Base2Log( strlen(pToken) ); + if ( fHex && strlen(pToken) == 1 ) + Log2 = 0; if ( (1 << Log2) != (int)strlen(pToken) ) { printf( "The truth table length (%d) is not power-of-2.\n", (int)strlen(pToken) ); @@ -984,29 +986,41 @@ char * Abc_SopFromTruthBin( char * pTruth ) if ( Digit == 1 ) Vec_IntPush( vMints, nTruthSize - 1 - i ); } +/* if ( Vec_IntSize( vMints ) == 0 || Vec_IntSize( vMints ) == nTruthSize ) { Vec_IntFree( vMints ); printf( "Cannot create constant function.\n" ); return NULL; } - - // create the SOP representation of the minterms - Length = Vec_IntSize(vMints) * (nVars + 3); - pSopCover = ABC_ALLOC( char, Length + 1 ); - pSopCover[Length] = 0; - Vec_IntForEachEntry( vMints, Mint, i ) +*/ + if ( Vec_IntSize(vMints) == 0 || Vec_IntSize(vMints) == (1 << nVars) ) { - pCube = pSopCover + i * (nVars + 3); - for ( b = 0; b < nVars; b++ ) -// if ( Mint & (1 << (nVars-1-b)) ) - if ( Mint & (1 << b) ) - pCube[b] = '1'; - else - pCube[b] = '0'; - pCube[nVars + 0] = ' '; - pCube[nVars + 1] = '1'; - pCube[nVars + 2] = '\n'; + pSopCover = ABC_ALLOC( char, 4 ); + pSopCover[0] = ' '; + pSopCover[1] = '0' + (Vec_IntSize(vMints) > 0); + pSopCover[2] = '\n'; + pSopCover[3] = 0; + } + else + { + // create the SOP representation of the minterms + Length = Vec_IntSize(vMints) * (nVars + 3); + pSopCover = ABC_ALLOC( char, Length + 1 ); + pSopCover[Length] = 0; + Vec_IntForEachEntry( vMints, Mint, i ) + { + pCube = pSopCover + i * (nVars + 3); + for ( b = 0; b < nVars; b++ ) + // if ( Mint & (1 << (nVars-1-b)) ) + if ( Mint & (1 << b) ) + pCube[b] = '1'; + else + pCube[b] = '0'; + pCube[nVars + 0] = ' '; + pCube[nVars + 1] = '1'; + pCube[nVars + 2] = '\n'; + } } Vec_IntFree( vMints ); return pSopCover; @@ -1074,37 +1088,34 @@ char * Abc_SopFromTruthHex( char * pTruth ) } // create the SOP representation of the minterms - Length = Vec_IntSize(vMints) * (nVars + 3); - pSopCover = ABC_ALLOC( char, Length + 1 ); - pSopCover[Length] = 0; - Vec_IntForEachEntry( vMints, Mint, i ) + if ( Vec_IntSize(vMints) == 0 || Vec_IntSize(vMints) == (1 << nVars) ) { - pCube = pSopCover + i * (nVars + 3); - for ( b = 0; b < nVars; b++ ) -// if ( Mint & (1 << (nVars-1-b)) ) - if ( Mint & (1 << b) ) - pCube[b] = '1'; - else - pCube[b] = '0'; - pCube[nVars + 0] = ' '; - pCube[nVars + 1] = '1'; - pCube[nVars + 2] = '\n'; + pSopCover = ABC_ALLOC( char, 4 ); + pSopCover[0] = ' '; + pSopCover[1] = '0' + (Vec_IntSize(vMints) > 0); + pSopCover[2] = '\n'; + pSopCover[3] = 0; } -/* - // create TT representation + else { - extern void Bdc_ManDecomposeTest( unsigned uTruth, int nVars ); - unsigned uTruth = 0; - int nVarsAll = 4; - assert( nVarsAll == 4 ); - assert( nVars <= nVarsAll ); + Length = Vec_IntSize(vMints) * (nVars + 3); + pSopCover = ABC_ALLOC( char, Length + 1 ); + pSopCover[Length] = 0; Vec_IntForEachEntry( vMints, Mint, i ) - uTruth |= (1 << Mint); -// uTruth = uTruth | (uTruth << 8) | (uTruth << 16) | (uTruth << 24); - uTruth = uTruth | (uTruth << 16); - Bdc_ManDecomposeTest( uTruth, nVarsAll ); + { + pCube = pSopCover + i * (nVars + 3); + for ( b = 0; b < nVars; b++ ) + // if ( Mint & (1 << (nVars-1-b)) ) + if ( Mint & (1 << b) ) + pCube[b] = '1'; + else + pCube[b] = '0'; + pCube[nVars + 0] = ' '; + pCube[nVars + 1] = '1'; + pCube[nVars + 2] = '\n'; + } } -*/ + Vec_IntFree( vMints ); return pSopCover; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2acd485d6..26f49799f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -163,6 +163,7 @@ static int Abc_CommandLutExact ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAllExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMajGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandOrchestrate ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -539,6 +540,7 @@ static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9GroupProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SplitProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9SplitSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ChainBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -591,6 +593,8 @@ static int Abc_CommandAbc9Gla2Fla ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Gen ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Cfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ProdAdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9AddFlop ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9BMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -772,7 +776,7 @@ void Abc_FrameUpdateGia( Abc_Frame_t * pAbc, Gia_Man_t * pNew ) { if ( pNew == NULL ) { - Abc_Print( -1, "Abc_FrameUpdateGia(): Tranformation has failed.\n" ); + Abc_Print( -1, "Abc_FrameUpdateGia(): Transformation has failed.\n" ); return; } if ( Gia_ManPoNum(pNew) == 0 ) @@ -914,6 +918,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "varmin", Abc_CommandVarMin, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "faultclasses", Abc_CommandFaultClasses, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "exact", Abc_CommandExact, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "orchestrate", Abc_CommandOrchestrate, 1 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_start", Abc_CommandBmsStart, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_stop", Abc_CommandBmsStop, 0 ); @@ -1298,6 +1303,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&gprove", Abc_CommandAbc9GroupProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&splitprove", Abc_CommandAbc9SplitProve, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&splitsat", Abc_CommandAbc9SplitSat, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmcs", Abc_CommandAbc9SBmc, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&chainbmc", Abc_CommandAbc9ChainBmc, 0 ); @@ -1356,6 +1362,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&gen", Abc_CommandAbc9Gen, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&cfs", Abc_CommandAbc9Cfs, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&prodadd", Abc_CommandAbc9ProdAdd, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&addflop", Abc_CommandAbc9AddFlop, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); { @@ -6997,7 +7005,7 @@ int Abc_CommandTestNpn( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: testnpn [-AN ] [-dbvh] \n" ); Abc_Print( -2, "\t testbench for computing (semi-)canonical forms\n" ); - Abc_Print( -2, "\t of completely-specified Boolean functions up to 16 varibles\n" ); + Abc_Print( -2, "\t of completely-specified Boolean functions up to 16 variables\n" ); Abc_Print( -2, "\t-A : semi-caninical form computation algorithm [default = %d]\n", NpnType ); Abc_Print( -2, "\t 0: uniqifying truth tables\n" ); Abc_Print( -2, "\t 1: exact NPN canonical form by brute-force enumeration\n" ); @@ -7345,6 +7353,194 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [Orchestration synthesis] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandOrchestrate( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pDup; + int c, RetValue; + + int nNodeSizeMax; + int nConeSizeMax; + int fUpdateLevel; + int fUseZeros_rwr; + int fUseZeros_ref; + int fUseDcs; + int RS_CUT_MIN = 4;//rs option + int RS_CUT_MAX = 16;//rs option + int nCutsMax; //rs option + int nNodesMax; //rs option + int nLevelsOdc; //rs option + + int fPrecompute; //rewrite option (not enabled) + int fPlaceEnable; //rewrite option (not enabled) + + int fVerbose; //rewrite/rs/rf verbose + int fVeryVerbose; //very verbose option for all + //size_t NtkSize; + extern void Rwr_Precompute(); + + //local greedy + extern int Abc_NtkOrchLocal( Abc_Ntk_t * pNtk, int fUseZeros_rwr, int fUseZeros_ref, int fPlaceEnable, int nCutsMax, int nNodesMax, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose, int nNodeSizeMax, int nConeSizeMax, int fUseDcs ); + //priority orch + extern int Abc_NtkOchestration( Abc_Ntk_t * pNtk, Vec_Int_t **pGain_rwr, Vec_Int_t **pGain_res,Vec_Int_t **pGain_ref, int sOpsOrder, int fUseZeros_rwr, int fUseZeros_ref, int fPlaceEnable, int nCutsMax, int nNodesMax, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose, int nNodeSizeMax, int nConeSizeMax, int fUseDcs ); + // set defaults + nNodeSizeMax = 10; + nConeSizeMax = 16; + fUpdateLevel = 1; + fUseZeros_rwr = 1; + fUseZeros_ref = 1; + fUseDcs = 0; + fVerbose = 0; + fVeryVerbose = 0; + fPlaceEnable = 0; + fPrecompute = 0; + nCutsMax = 8; + nNodesMax = 1; + nLevelsOdc = 0; + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "KNFZzlvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nCutsMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCutsMax < 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; + } + nNodesMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nNodesMax < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nLevelsOdc = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLevelsOdc < 0 ) + goto usage; + break; + case 'l': + fUpdateLevel ^= 1; + break; + case 'z': + fUseZeros_rwr ^= 1; + break; + case 'Z': + fUseZeros_ref ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'w': + fVeryVerbose ^= 1; + break; + case 'h': + goto usage; + break; + } + } + if ( fPrecompute ) + { + Rwr_Precompute(); + return 0; + } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( nCutsMax < RS_CUT_MIN || nCutsMax > RS_CUT_MAX ) + { + Abc_Print( -1, "Can only compute cuts for %d <= K <= %d.\n", RS_CUT_MIN, RS_CUT_MAX ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -1, "This command can only be applied to an AIG (run \"strash\").\n" ); + return 1; + } + if ( Abc_NtkGetChoiceNum(pNtk) ) + { + Abc_Print( -1, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" ); + return 1; + } + if ( nNodeSizeMax > 15 ) + { + Abc_Print( -1, "The cone size cannot exceed 15.\n" ); + return 1; + } + + if ( fUseDcs && nNodeSizeMax >= nConeSizeMax ) + { + Abc_Print( -1, "For don't-care to work, containing cone should be larger than collapsed node.\n" ); + return 1; + } + + // modify the current network + pDup = Abc_NtkDup( pNtk ); + RetValue = Abc_NtkOrchLocal( pNtk, fUseZeros_rwr, fUseZeros_ref, fPlaceEnable, nCutsMax, nNodesMax, nLevelsOdc, fUpdateLevel, fVerbose, fVeryVerbose, nNodeSizeMax, nConeSizeMax, fUseDcs ); + if ( RetValue == -1 ) + { + Abc_FrameReplaceCurrentNetwork( pAbc, pDup ); + printf( "An error occurred during computation. The original network is restored.\n" ); + } + else + { + Abc_NtkDelete( pDup ); + if ( RetValue == 0 ) + { + Abc_Print( 0, "Ochestration (local greedy) has failed.\n" ); + return 1; + } + } + return 0; + +usage: + Abc_Print( -2, "usage: orchestrate [-KNFZzlvwh]\n" ); + Abc_Print( -2, "\t performs technology-independent AIG synthesis using orchestration method (currently orchestrating rw/rf/rs)\n" ); + Abc_Print( -2, "\t-K : (resub)the max cut size (%d <= num <= %d) [default = %d]\n", RS_CUT_MIN, RS_CUT_MAX, nCutsMax ); + Abc_Print( -2, "\t-N : (resub)the max number of nodes to add (0 <= num <= 3) [default = %d]\n", nNodesMax ); + Abc_Print( -2, "\t-F : (resub)the number of fanout levels for ODC computation [default = %d]\n", nLevelsOdc ); + Abc_Print( -2, "\t-l : (resub/rw/refactor)toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); + Abc_Print( -2, "\t-z : (rw)toggle using zero-cost replacements [default = %s]\n", fUseZeros_rwr? "yes": "no" ); + Abc_Print( -2, "\t-Z : (refactor)toggle using zero-cost replacements [default = %s]\n", fUseZeros_ref? "yes": "no" ); + Abc_Print( -2, "\t-v : (resub/rw/refactor)toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : (resub/rw/refactor)toggle detailed verbose printout [default = %s]\n", fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + + + + + /**Function************************************************************* @@ -10827,6 +11023,7 @@ usage: ***********************************************************************/ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern void Abc_NtkFaninSort( Abc_Ntk_t * pNtk ); Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int c, fCubeSort = 1, fMode = -1, nCubeLimit = 1000000; @@ -10882,6 +11079,8 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Converting to SOP has failed.\n" ); return 0; } + if ( !fCubeSort ) + Abc_NtkFaninSort( pNtk ); return 0; usage: @@ -13175,6 +13374,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) int fFpga; int fOneHot; int fRandom; + int fGraph; int fVerbose; char * FileName; char Command[1000]; @@ -13186,6 +13386,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars ); extern void Abc_GenOneHot( char * pFileName, int nVars ); extern void Abc_GenRandom( char * pFileName, int nPis ); + extern void Abc_GenGraph( char * pFileName, int nPis ); extern void Abc_GenAdderTree( char * pFileName, int nArgs, int nBits ); // set defaults @@ -13200,9 +13401,10 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) fFpga = 0; fOneHot = 0; fRandom = 0; + fGraph = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NAKLatsembfnrvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NAKLatsembfnrgvh" ) ) != EOF ) { switch ( c ) { @@ -13277,6 +13479,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fRandom ^= 1; break; + case 'g': + fGraph ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -13316,6 +13521,8 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_GenOneHot( FileName, nVars ); else if ( fRandom ) Abc_GenRandom( FileName, nVars ); + else if ( fGraph ) + Abc_GenGraph( FileName, nVars ); else if ( fAdderTree ) { printf( "Generating adder tree with %d arguments and %d bits.\n", nArgs, nVars ); @@ -13335,10 +13542,10 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: gen [-NAKL num] [-atsembfnrvh] \n" ); + Abc_Print( -2, "usage: gen [-NAKL num] [-atsembfnrgvh] \n" ); Abc_Print( -2, "\t generates simple circuits\n" ); Abc_Print( -2, "\t-N num : the number of variables [default = %d]\n", nVars ); - Abc_Print( -2, "\t-A num : the number of agruments (for adder tree) [default = %d]\n", nArgs ); + Abc_Print( -2, "\t-A num : the number of arguments (for adder tree) [default = %d]\n", nArgs ); Abc_Print( -2, "\t-K num : the LUT size (to be used with switch -f) [default = %d]\n", nLutSize ); Abc_Print( -2, "\t-L num : the LUT count (to be used with switch -f) [default = %d]\n", nLuts ); Abc_Print( -2, "\t-a : generate ripple-carry adder [default = %s]\n", fAdder? "yes": "no" ); @@ -13348,6 +13555,7 @@ usage: Abc_Print( -2, "\t-m : generate a multiplier [default = %s]\n", fMulti? "yes": "no" ); Abc_Print( -2, "\t-b : generate a signed Booth multiplier [default = %s]\n", fBooth? "yes": "no" ); Abc_Print( -2, "\t-f : generate a LUT FPGA structure [default = %s]\n", fFpga? "yes": "no" ); + Abc_Print( -2, "\t-g : generate a graph structure [default = %s]\n", fGraph? "yes": "no" ); Abc_Print( -2, "\t-n : generate one-hotness conditions [default = %s]\n", fOneHot? "yes": "no" ); Abc_Print( -2, "\t-r : generate random single-output function [default = %s]\n", fRandom? "yes": "no" ); Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); @@ -17610,7 +17818,7 @@ int Abc_CommandRecPs3( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_NtkRecIsRunning3() ) { - Abc_Print( -1, "This command works for AIGs only after calling \"rec_start2\".\n" ); + Abc_Print( -1, "This command works for AIGs only after calling \"rec_start3\".\n" ); return 0; } Abc_NtkRecPs3(fPrintLib); @@ -17662,7 +17870,7 @@ int Abc_CommandRecAdd3( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_NtkRecIsRunning3() ) { - Abc_Print( -1, "This command works for AIGs after calling \"rec_start2\".\n" ); + Abc_Print( -1, "This command works for AIGs after calling \"rec_start3\".\n" ); return 0; } Abc_NtkRecAdd3( pNtk, fUseSOPB ); @@ -19935,7 +20143,7 @@ usage: Abc_Print( -2, "\t prints statistics of the DSD manager\n" ); Abc_Print( -2, "\t-N num : show structures whose ID divides by N [default = %d]\n", Number ); Abc_Print( -2, "\t-S num : show structures whose support size is S [default = %d]\n", Support ); - Abc_Print( -2, "\t-o : toggles printing occurence distribution [default = %s]\n", fOccurs? "yes": "no" ); + Abc_Print( -2, "\t-o : toggles printing occurrence distribution [default = %s]\n", fOccurs? "yes": "no" ); Abc_Print( -2, "\t-t : toggles dumping truth tables [default = %s]\n", fTtDump? "yes": "no" ); Abc_Print( -2, "\t-b : toggles processing second manager [default = %s]\n", fSecond? "yes": "no" ); Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); @@ -25974,7 +26182,7 @@ usage: Abc_Print( -2, "\t-Q num : Min clause LBD for binary resolution [default = %d]\n", opts.clause_min_lbd_bin_resol ); Abc_Print( -2, "\n\tConstants used for branching (VSIDS heuristic):\n"); Abc_Print( -2, "\t-R num : Clause activity decay factor (when using float clause activity) [default = %f]\n", opts.clause_decay ); - Abc_Print( -2, "\t-S num : Varibale activity decay factor [default = %f]\n", opts.var_decay ); + Abc_Print( -2, "\t-S num : Variable activity decay factor [default = %f]\n", opts.var_decay ); #ifdef SATOKO_ACT_VAR_FIXED Abc_Print( -2, "\t-T num : Variable activity limit valeu [default = 0x%08X]\n", opts.var_act_limit ); Abc_Print( -2, "\t-U num : Variable activity re-scale factor [default = 0x%08X]\n", opts.var_act_rescale ); @@ -27328,7 +27536,7 @@ usage: Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart ); Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-T num : runtime limit, in seconds [default = %d]\n", pPars->nTimeOut ); - Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); + Abc_Print( -2, "\t-H num : runtime limit per output, in milliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); Abc_Print( -2, "\t-G num : runtime gap since the last CEX, in seconds [default = %d]\n", pPars->nTimeOutGap ); Abc_Print( -2, "\t-C num : max conflicts at an output [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump ); @@ -28891,7 +29099,7 @@ int Abc_CommandSaucy( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Obj_t * pNodePo; FILE * hadi = fopen("hadi.txt", "w"); Abc_NtkForEachPo( pNtk, pNodePo, i ) { - printf("Ouput %s\n\n", Abc_ObjName(pNodePo)); + printf("Output %s\n\n", Abc_ObjName(pNodePo)); saucyGateWay( pNtk, pNodePo, gFile, 0, fLookForSwaps, fFixOutputs, fFixInputs, fQuiet, fPrintTree ); printf("----------------------------------------\n"); } @@ -28917,7 +29125,7 @@ int Abc_CommandSaucy( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: saucy3 [-O ] [-F ] [-iosqvh]\n\n" ); - Abc_Print( -2, "\t computes functional symmetries of the netowrk\n" ); + Abc_Print( -2, "\t computes functional symmetries of the network\n" ); Abc_Print( -2, "\t prints symmetry generators to the standard output\n" ); Abc_Print( -2, "\t-O : (optional) compute symmetries only for output given by name\n"); Abc_Print( -2, "\t only inputs in the output cone are permuted\n"); @@ -29305,7 +29513,7 @@ usage: Abc_Print( -2, "\t-D num : limit on conflicts during ind-generalization (0 = no limit) [default = %d]\n",pPars->nConfGenLimit ); Abc_Print( -2, "\t-Q num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit ); Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut ); - Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); + Abc_Print( -2, "\t-H num : runtime limit per output, in milliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n", pPars->nTimeOutGap ); Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); @@ -31305,12 +31513,15 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SaveAig( Abc_Frame_t * pAbc, int argc, char ** argv ) { - int c, fArea = 0; + int c, fClear = 0, fArea = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cah" ) ) != EOF ) { switch ( c ) { + case 'c': + fClear ^= 1; + break; case 'a': fArea ^= 1; break; @@ -31325,16 +31536,24 @@ int Abc_CommandAbc9SaveAig( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Empty network.\n" ); return 1; } + if ( fClear && pAbc->pGiaSaved != NULL ) + { + Gia_ManStopP( &pAbc->pGiaSaved ); + return 0; + } if ( fArea && pAbc->pGiaSaved != NULL && Gia_ManAndNum(pAbc->pGiaSaved) <= Gia_ManAndNum(pAbc->pGia) ) return 0; + if ( !fArea && pAbc->pGiaSaved != NULL && !(Gia_ManLevelNum(pAbc->pGiaSaved) > Gia_ManLevelNum(pAbc->pGia) || (Gia_ManLevelNum(pAbc->pGiaSaved) == Gia_ManLevelNum(pAbc->pGia) && Gia_ManAndNum(pAbc->pGiaSaved) > Gia_ManAndNum(pAbc->pGia))) ) + return 0; // save the design as best Gia_ManStopP( &pAbc->pGiaSaved ); pAbc->pGiaSaved = Gia_ManDupWithAttributes( pAbc->pGia ); return 0; usage: - Abc_Print( -2, "usage: &saveaig [-ah]\n" ); + Abc_Print( -2, "usage: &saveaig [-cah]\n" ); Abc_Print( -2, "\t saves the current AIG into the internal storage\n" ); + Abc_Print( -2, "\t-c : toggle clearing the saved AIG [default = %s]\n", fClear? "yes": "no" ); Abc_Print( -2, "\t-a : toggle saving AIG with the smaller area [default = %s]\n", fArea? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -31571,13 +31790,14 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) int c, nArgcNew; int fUnique = 0; int fVerilog = 0; + int fInter = 0; int fVerBufs = 0; int fMiniAig = 0; int fMiniLut = 0; int fWriteNewLine = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "upbmlnvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "upibmlnvh" ) ) != EOF ) { switch ( c ) { @@ -31587,6 +31807,9 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'p': fVerilog ^= 1; break; + case 'i': + fInter ^= 1; + break; case 'b': fVerBufs ^= 1; break; @@ -31628,7 +31851,7 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ManStop( pGia ); } else if ( fVerilog ) - Gia_ManDumpVerilog( pAbc->pGia, pFileName, NULL, fVerBufs ); + Gia_ManDumpVerilog( pAbc->pGia, pFileName, NULL, fVerBufs, fInter ); else if ( fMiniAig ) Gia_ManWriteMiniAig( pAbc->pGia, pFileName ); else if ( fMiniLut ) @@ -31638,10 +31861,11 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &w [-upbmlnvh] \n" ); + Abc_Print( -2, "usage: &w [-upibmlnvh] \n" ); Abc_Print( -2, "\t writes the current AIG into the AIGER file\n" ); Abc_Print( -2, "\t-u : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" ); Abc_Print( -2, "\t-p : toggle writing Verilog with 'and' and 'not' [default = %s]\n", fVerilog? "yes" : "no" ); + Abc_Print( -2, "\t-i : toggle writing the interface module in Verilog [default = %s]\n", fInter? "yes" : "no" ); Abc_Print( -2, "\t-b : toggle writing additional buffers in Verilog [default = %s]\n", fVerBufs? "yes" : "no" ); Abc_Print( -2, "\t-m : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" ); Abc_Print( -2, "\t-l : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "yes" : "no" ); @@ -31815,8 +32039,8 @@ usage: Abc_Print( -2, "\t-a : toggle printing miter statistics [default = %s]\n", pPars->fMiter? "yes": "no" ); Abc_Print( -2, "\t-s : toggle printing slack distribution [default = %s]\n", pPars->fSlacks? "yes": "no" ); Abc_Print( -2, "\t-z : skip mapping statistics even if mapped [default = %s]\n", pPars->fSkipMap? "yes": "no" ); - Abc_Print( -2, "\t-n : toggle using no color in the printout [default = %s]\n", pPars->fNoColor? "yes": "no" ); - Abc_Print( -2, "\t-x : toggle printing saved AIG statistics [default = %s]\n", fBest? "yes": "no" ); + Abc_Print( -2, "\t-x : toggle using no color in the printout [default = %s]\n", pPars->fNoColor? "yes": "no" ); + Abc_Print( -2, "\t-b : toggle printing saved AIG statistics [default = %s]\n", fBest? "yes": "no" ); Abc_Print( -2, "\t-D file : file name to dump statistics [default = none]\n" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -34621,7 +34845,7 @@ usage: Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-s : toggle seq vs. comb simulation [default = %s]\n", pPars->fSeqSimulate? "yes": "no" ); Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); - Abc_Print( -2, "\t-d : toggle using two POs intead of XOR [default = %s]\n", pPars->fDualOut? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle using two POs instead of XOR [default = %s]\n", pPars->fDualOut? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -35072,7 +35296,7 @@ usage: Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); - Abc_Print( -2, "\t-d : toggle using two POs intead of XOR [default = %s]\n", pPars->fDualOut? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle using two POs instead of XOR [default = %s]\n", pPars->fDualOut? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -37060,13 +37284,15 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Gia_Man_t * Cec_ManScorrCorrespondence( Gia_Man_t * p, Cec_ParCor_t * pPars ); extern Gia_Man_t * Gia_ManScorrDivideTest( Gia_Man_t * p, Cec_ParCor_t * pPars ); + extern Gia_Man_t * Gia_SignalCorrespondencePart( Gia_Man_t * p, Cec_ParCor_t * pPars ); Cec_ParCor_t Pars, * pPars = &Pars; Gia_Man_t * pTemp; int fPartition = 0; int fUseOld = 0, c; Cec_ManCorSetDefaultParams( pPars ); + pPars->nProcs = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCPXpkrecqowvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSpkrecqowvh" ) ) != EOF ) { switch ( c ) { @@ -37092,7 +37318,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nBTLimit < 0 ) goto usage; break; - case 'P': + case 'G': if ( globalUtilOptind >= argc ) { Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); @@ -37114,6 +37340,28 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nLimitMax < 0 ) goto usage; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nProcs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nProcs < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nPartSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nPartSize < 0 ) + goto usage; + break; case 'p': fPartition ^= 1; break; @@ -37166,7 +37414,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 0, "The network is combinational.\n" ); return 0; } - if ( fUseOld ) + if ( pPars->nPartSize > 0 ) + pTemp = Gia_SignalCorrespondencePart( pAbc->pGia, pPars ); + else if ( fUseOld ) pTemp = Cec_ManScorrCorrespondence( pAbc->pGia, pPars ); else if ( fPartition ) pTemp = Gia_ManScorrDivideTest( pAbc->pGia, pPars ); @@ -37176,12 +37426,14 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &scorr [-FCPX num] [-pkrecqowvh]\n" ); + Abc_Print( -2, "usage: &scorr [-FCGXPS num] [-pkrecqowvh]\n" ); Abc_Print( -2, "\t performs signal correpondence computation\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); - Abc_Print( -2, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix ); + Abc_Print( -2, "\t-G num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix ); Abc_Print( -2, "\t-X num : the number of iterations of little or no improvement [default = %d]\n", pPars->nLimitMax ); + Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", pPars->nProcs ); + Abc_Print( -2, "\t-S num : the number of flops in one partition [default = %d]\n", pPars->nPartSize ); Abc_Print( -2, "\t-p : toggle using partitioning for the input AIG [default = %s]\n", fPartition? "yes": "no" ); Abc_Print( -2, "\t-k : toggle using constant correspondence [default = %s]\n", pPars->fConstCorr? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" ); @@ -43769,14 +44021,25 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Permute( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManDupPiPerm( Gia_Man_t * p ); + extern Gia_Man_t * Gia_ManDupRandPerm( Gia_Man_t * p ); Gia_Man_t * pTemp; - int c, fVerbose = 0; + int c, RandSeed = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Svh" ) ) != EOF ) { switch ( c ) { + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + RandSeed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( RandSeed < 0 ) + goto usage; + break; case 'v': fVerbose ^= 1; break; @@ -43788,16 +44051,25 @@ int Abc_CommandAbc9Permute( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9Posplit(): There is no AIG.\n" ); + Abc_Print( -1, "Abc_CommandAbc9Permute(): There is no AIG.\n" ); return 1; } - pTemp = Gia_ManDupPiPerm( pAbc->pGia ); + if ( Gia_ManRegNum(pAbc->pGia) > 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9Permute(): This command does not work for sequential AIGs.\n" ); + return 1; + } + Abc_Random(1); + for ( c = 0; c < RandSeed; c++ ) + Abc_Random(0); + pTemp = Gia_ManDupRandPerm( pAbc->pGia ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &permute [-vh]\n" ); - Abc_Print( -2, "\t permutes primary inputs\n" ); + Abc_Print( -2, "usage: &permute [-S num] [-vh]\n" ); + Abc_Print( -2, "\t generates a random NPNP transformation of the combinational AIG\n" ); + Abc_Print( -2, "\t-S num : the seed used to randomize the process [default = %d]\n", RandSeed ); 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; @@ -44812,17 +45084,21 @@ usage: int Abc_CommandAbc9Compare( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_Iso4TestTwo( Gia_Man_t * pGia0, Gia_Man_t * pGia1 ); + extern void Gia_ManComparePrint( Gia_Man_t * p, Gia_Man_t * q ); Gia_Man_t * pGia0, * pGia1; char ** pArgvNew; int nArgcNew; - int c, fVerbose = 0; + int c, fFunc = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "fvh" ) ) != EOF ) { switch ( c ) { + case 'f': + fFunc ^= 1; + break; case 'v': fVerbose ^= 1; - break; + break; case 'h': goto usage; default: @@ -44843,14 +45119,18 @@ int Abc_CommandAbc9Compare( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Compare(): Reading input files did not work.\n" ); return 1; } - Gia_Iso4TestTwo( pGia0, pGia1 ); + if ( fFunc ) + Gia_ManComparePrint( pGia0, pGia1 ); + else + Gia_Iso4TestTwo( pGia0, pGia1 ); Gia_ManStop( pGia0 ); Gia_ManStop( pGia1 ); return 0; usage: - Abc_Print( -2, "usage: &compare [-vh]\n" ); + Abc_Print( -2, "usage: &compare [-fvh]\n" ); Abc_Print( -2, "\t compared two AIGs for structural similarity\n" ); + Abc_Print( -2, "\t-f : toggle functional comparison [default = %s]\n", fFunc? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -45723,7 +46003,7 @@ usage: Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n", pPars->TimeOutLoc ); Abc_Print( -2, "\t-M num : percentage of local runtime limit increase [default = %d]\n", pPars->TimeOutInc ); Abc_Print( -2, "\t-G num : approximate gap runtime limit in seconds [default = %d]\n", pPars->TimeOutGap ); - Abc_Print( -2, "\t-H num : timeout per output in miliseconds [default = %d]\n", pPars->TimePerOut ); + Abc_Print( -2, "\t-H num : timeout per output in milliseconds [default = %d]\n", pPars->TimePerOut ); Abc_Print( -2, "\t-s : toggle using combinational synthesis [default = %s]\n", pPars->fUseSyn? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dumping invariant into a file [default = %s]\n", pPars->fDumpFinal? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); @@ -45842,6 +46122,163 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9SplitSat( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Cnf_SplitSat( char * pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fPrepro, int fVerbose ); + int c, iVarBeg = 0, iVarEnd = ABC_INFINITY, nLits = 10, Value = 2, TimeOut = 5, nProcs = 1, nIters = 1, Seed = 0, fPrepro = 0, fVerbose = 0; char * pFileName = NULL; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "BENVTPISpvh" ) ) != EOF ) + { + switch ( c ) + { + case 'B': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-B\" should be followed by a positive integer.\n" ); + goto usage; + } + iVarBeg = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iVarBeg < 0 ) + goto usage; + break; + case 'E': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-E\" should be followed by a positive integer.\n" ); + goto usage; + } + iVarEnd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iVarEnd < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by a positive integer.\n" ); + goto usage; + } + nLits = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLits < 0 ) + goto usage; + break; + case 'V': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-V\" should be followed by a positive integer.\n" ); + goto usage; + } + Value = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Value < 0 || Value > 2 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by a positive integer.\n" ); + goto usage; + } + TimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( TimeOut < 0 ) + goto usage; + break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" ); + goto usage; + } + nProcs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nProcs <= 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nIters < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + Seed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Seed < 0 ) + goto usage; + break; + case 'p': + fPrepro ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + // get the file name + if ( argc != globalUtilOptind + 1 ) + { + Abc_Print( -1, "Abc_CommandAbc9SplitSat(): CNF file names should be given on the command line.\n" ); + return 1; + } + { + FILE * pFile; + pFileName = argv[globalUtilOptind]; + pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + Abc_Print( -1, "Cannot open file \"%s\" with the input test patterns.\n", pFileName ); + return 0; + } + fclose( pFile ); + } + Cnf_SplitSat( pFileName, iVarBeg, iVarEnd, nLits, Value, TimeOut, nProcs, nIters, Seed, fPrepro, fVerbose ); + return 0; + +usage: + Abc_Print( -2, "usage: &splitsat [-BENVTPIS num] [-pvh]\n" ); + Abc_Print( -2, "\t solves CNF-based SAT problem by randomized case-splitting\n" ); + Abc_Print( -2, "\t-B num : the first CNF variable to use for splitting [default = %d]\n", iVarBeg ); + Abc_Print( -2, "\t-E num : the last CNF variable to use for splitting [default = %d]\n", iVarEnd ); + Abc_Print( -2, "\t-N num : the number of CNF variables to use for splitting [default = %d]\n", nLits ); + Abc_Print( -2, "\t-V num : the variable values to use (0, 1, or 2 for \"any\") [default = %d]\n", Value ); + Abc_Print( -2, "\t-T num : the runtime limit in seconds per subproblem [default = %d]\n", TimeOut ); + Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", nProcs ); + Abc_Print( -2, "\t-I num : the max number of iterations (0 = infinity) [default = %d]\n", nIters ); + Abc_Print( -2, "\t-S num : the random seed used to generate cofactors [default = %d]\n", Seed ); + Abc_Print( -2, "\t-p : toggle using SatELIte (http://minisat.se/SatELite.html) [default = %s]\n", fPrepro? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -49198,10 +49635,10 @@ usage: ***********************************************************************/ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript ); - int c, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, fVerbose = 0; char * pScript; + extern void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs ); + int c, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, nProcs = 1, fVerbose = 0; char * pScript; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NITSvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NITSPvh" ) ) != EOF ) { switch ( c ) { @@ -49249,6 +49686,17 @@ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Seed < 0 ) goto usage; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nProcs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nProcs < 0 ) + goto usage; + break; case 'v': fVerbose ^= 1; break; @@ -49269,17 +49717,18 @@ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } pScript = Abc_UtilStrsav( argv[globalUtilOptind] ); - Gia_ManStochSyn( nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript ); + Gia_ManStochSyn( nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript, nProcs ); ABC_FREE( pScript ); return 0; usage: - Abc_Print( -2, "usage: &stochsyn [-NITS ] [-tvh]