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/src/aig/gia/gia.h b/src/aig/gia/gia.h index fed64b1ad..68266bb2d 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, int fInterComb ); /*=== 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/giaDup.c b/src/aig/gia/giaDup.c index 3822497af..db4072d71 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1604,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.] @@ -5584,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 6a3f2c458..0efb5b29f 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -1241,6 +1241,89 @@ 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_ManDumpInterface2( 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.] @@ -1323,38 +1406,40 @@ 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, int fInterComb ) { - 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) ) + int i, k, iObj, nRegs = Gia_ManRegNum(p); + if ( fInterComb ) { - printf( "Currently cannot write sequential AIG.\n" ); + extern void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName ); + Gia_ManDumpInterface( p, pFileName ); return; } - pFile = fopen( pFileName, "wb" ); + + FILE * pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) { printf( "Cannot open output file \"%s\".\n", pFileName ); return; } + if ( fInter || nRegs ) + Gia_ManDumpInterface2( 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 ) { @@ -1505,6 +1590,203 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int Vec_BitFree( vInvs ); Vec_BitFree( vUsed ); + + Gia_ManSetRegNum( p, nRegs ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName ) +{ + 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; + + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open output file \"%s\".\n", pFileName ); + return; + } + + vInvs = Gia_ManGenUsed( p, 0 ); + vUsed = Gia_ManGenUsed( p, 1 ); + + fprintf( pFile, "module " ); + Gia_ManDumpModuleName( pFile, p->pName ); + fprintf( pFile, "_wrapper" ); + fprintf( pFile, " ( _i_, _o_ );\n\n" ); + fprintf( pFile, " input [%d:0] _i_;\n", Gia_ManCiNum(p)-1 ); + fprintf( pFile, " output [%d:0] _o_;\n\n", Gia_ManCoNum(p)-1 ); + + fprintf( pFile, " wire " ); + Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL ); + fprintf( pFile, ";\n\n" ); + + fprintf( pFile, " wire " ); + Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL ); + fprintf( pFile, ";\n\n" ); + + fprintf( pFile, " assign { " ); + Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL ); + fprintf( pFile, " } = _i_;\n\n" ); + + fprintf( pFile, " assign _o_ = { " ); + Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL ); + fprintf( pFile, " };\n\n" ); + + if ( Vec_BitCount(vUsed) ) + { + fprintf( pFile, " wire " ); + Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed ); + fprintf( pFile, ";\n\n" ); + } + + if ( Vec_BitCount(vInvs) ) + { + fprintf( pFile, " wire " ); + Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs ); + fprintf( pFile, ";\n\n" ); + } + + // input inverters + Gia_ManForEachCi( p, pObj, i ) + { + if ( Vec_BitEntry(vUsed, Gia_ObjId(p, pObj)) ) + { + fprintf( pFile, " buf ( %s,", Gia_ObjGetDumpName(NULL, 'n', Gia_ObjId(p, pObj), nDigits) ); + fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) ); + } + if ( Vec_BitEntry(vInvs, Gia_ObjId(p, pObj)) ) + { + fprintf( pFile, " not ( %s,", Gia_ObjGetDumpName(NULL, 'i', Gia_ObjId(p, pObj), nDigits) ); + fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) ); + } + } + + // internal nodes and their inverters + fprintf( pFile, "\n" ); + Gia_ManForEachAnd( p, pObj, i ) + { + fprintf( pFile, " and ( %s,", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) ); + fprintf( pFile, " %s,", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0(pObj, i), nDigits) ); + fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC1(pObj)? 'i':'n'), Gia_ObjFaninId1(pObj, i), nDigits) ); + if ( Vec_BitEntry(vInvs, i) ) + { + fprintf( pFile, " not ( %s,", Gia_ObjGetDumpName(NULL, 'i', i, nDigits) ); + fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) ); + } + } + + // output drivers + fprintf( pFile, "\n" ); + Gia_ManForEachCo( p, pObj, i ) + { + fprintf( pFile, " buf ( %s, ", Gia_ObjGetDumpName(p->vNamesOut, 'z', i, nDigitsO) ); + if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) ) + fprintf( pFile, "1\'b%d );\n", Gia_ObjFaninC0(pObj) ); + else + fprintf( pFile, "%s );\n", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0p(p, pObj), nDigits) ); + } + + fprintf( pFile, "\nendmodule\n\n" ); + fclose( pFile ); + + Vec_BitFree( vInvs ); + Vec_BitFree( vUsed ); +} + + +/**Function************************************************************* + + Synopsis [Generate hierarchical design.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_FreeMany( Gia_Man_t ** pGias, int nGias ) +{ + int i; + for ( i = 0; i < nGias; i++ ) + Gia_ManStopP( &pGias[i] ); +} +void Gia_GenSandwich( char ** pFNames, int nFNames ) +{ + FILE * pFile = NULL; + char * pFileName = (char *)"sandwich.v"; + Gia_Man_t * pGias[16] = {0}; + int i, k; + assert( nFNames <= 16 ); + for ( i = 0; i < nFNames; i++ ) + { + FILE * pFile = fopen( pFNames[i], "rb" ); + if ( pFile == NULL ) { + printf( "Cannot open input file \"%s\".\n", pFNames[i] ); + Gia_FreeMany( pGias, nFNames ); + return; + } + fclose( pFile ); + pGias[i] = Gia_AigerRead( pFNames[i], 0, 0, 0 ); + if ( pGias[i] == NULL ) { + printf( "Failed to read an AIG from file \"%s\".\n", pFNames[i] ); + Gia_FreeMany( pGias, nFNames ); + return; + } + } + for ( i = 0; i < nFNames-1; i++ ) + if ( Gia_ManPoNum(pGias[i]) < Gia_ManPiNum(pGias[i+1]) ) { + printf( "AIG in file \"%s\" has fewer outputs than inputs of AIG in file \"%s\".\n", pFNames[i], pFNames[i+1] ); + Gia_FreeMany( pGias, nFNames ); + return; + } + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open output file \"%s\".\n", pFileName ); + Gia_FreeMany( pGias, nFNames ); + return; + } + fprintf( pFile, "\n" ); + for ( i = 0; i < nFNames; i++ ) + fprintf( pFile, "`include \"%s\"\n", Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v") ); + fprintf( pFile, "\n" ); + fprintf( pFile, "module sandwich ( in, out );\n" ); + fprintf( pFile, " input [%3d:0] in;\n", Gia_ManPiNum(pGias[0])-1 ); + fprintf( pFile, " output [%3d:0] out;\n", Gia_ManPoNum(pGias[nFNames-1])-1 ); + fprintf( pFile, " wire [%3d:0] tmp0 = in;\n", Gia_ManPiNum(pGias[0])-1 ); + for ( i = 0; i < nFNames; i++ ) { + fprintf( pFile, " wire [%3d:0] tmp%d; ", Gia_ManPoNum(pGias[i])-1, i+1 ); + Gia_ManDumpModuleName( pFile, pGias[i]->pName ); + fprintf( pFile, "_wrapper" ); + for ( k = strlen(pGias[i]->pName); k < 24; k++ ) + fprintf( pFile, " " ); + fprintf( pFile, " i%d ( tmp%d, tmp%d );\n", i+1, i, i+1 ); + } + fprintf( pFile, " assign out = tmp%d;\n", nFNames ); + fprintf( pFile, "endmodule\n" ); + fclose( pFile ); + for ( i = 0; i < nFNames; i++ ) { + Gia_ManDumpVerilog( pGias[i], Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v"), NULL, 0, 0, 1 ); + printf( "Dumped Verilog file \"%s\"\n", Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v") ); + } + Gia_FreeMany( pGias, nFNames ); + printf( "Dumped hierarchical design into file \"%s\"\n", pFileName ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaStoch.c b/src/aig/gia/giaStoch.c index 57775b5cc..78fe2cb67 100644 --- a/src/aig/gia/giaStoch.c +++ b/src/aig/gia/giaStoch.c @@ -22,6 +22,11 @@ #include "base/main/main.h" #include "base/cmd/cmd.h" +#ifdef _MSC_VER +#define unlink _unlink +#else +#include +#endif #ifdef ABC_USE_PTHREADS @@ -29,7 +34,6 @@ #include "../lib/pthread.h" #else #include -#include #endif #endif 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 ff6022b8e..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 ) 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/abcSop.c b/src/base/abc/abcSop.c index be5b5dd0b..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) ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 94ca326df..5a755ea1f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -594,6 +594,9 @@ 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_CommandAbc9GenHie ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -775,7 +778,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 ) @@ -1362,6 +1365,9 @@ 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", "&gen_hie", Abc_CommandAbc9GenHie, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); { @@ -7003,7 +7009,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" ); @@ -13708,7 +13714,7 @@ usage: 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" ); @@ -17981,7 +17987,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); @@ -18033,7 +18039,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 ); @@ -20306,7 +20312,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" ); @@ -26345,7 +26351,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 ); @@ -27699,7 +27705,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 ); @@ -29233,7 +29239,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"); } @@ -29259,7 +29265,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"); @@ -29647,7 +29653,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" ); @@ -31924,13 +31930,15 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) int c, nArgcNew; int fUnique = 0; int fVerilog = 0; + int fInter = 0; + int fInterComb = 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, "upicbmlnvh" ) ) != EOF ) { switch ( c ) { @@ -31940,6 +31948,12 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'p': fVerilog ^= 1; break; + case 'i': + fInter ^= 1; + break; + case 'c': + fInterComb ^= 1; + break; case 'b': fVerBufs ^= 1; break; @@ -31981,7 +31995,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, fInterComb ); else if ( fMiniAig ) Gia_ManWriteMiniAig( pAbc->pGia, pFileName ); else if ( fMiniLut ) @@ -31991,10 +32005,12 @@ 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 [-upicbmlnvh] \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-c : toggle writing the interface module in Verilog [default = %s]\n", fInterComb? "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" ); @@ -34974,7 +34990,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; @@ -35425,7 +35441,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; @@ -46132,7 +46148,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" ); @@ -51605,6 +51621,173 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9AddFlop( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p ); + Gia_Man_t * pTemp; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9AddFlop(): There is no AIG.\n" ); + return 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-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ); + Gia_Man_t * pTemp, * pSecond; + char * FileName = NULL; + FILE * pFile = NULL; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9BMiter(): There is no AIG.\n" ); + return 0; + } + if ( argc != globalUtilOptind + 1 ) + { + Abc_Print( -1, "Abc_CommandAbc9BMiter(): AIG should be given on the command line.\n" ); + return 0; + } + + // get the input file name + FileName = argv[globalUtilOptind]; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", FileName ); + if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) ) + Abc_Print( 1, "Did you mean \"%s\"?", FileName ); + Abc_Print( 1, "\n" ); + return 1; + } + fclose( pFile ); + + pSecond = Gia_AigerRead( FileName, 0, 0, 0 ); + if ( pSecond == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9BMiter(): Cannot read the file name on the command line.\n" ); + return 0; + } + pTemp = Gia_ManBoundaryMiter( pAbc->pGia, pSecond, fVerbose ); + Gia_ManStop( pSecond ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &bmiter [-vh] \n" ); + Abc_Print( -2, "\t creates the boundary miter\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"); + Abc_Print( -2, "\t : the implementation file\n"); + return 1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9GenHie( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Gia_GenSandwich( char ** pFNames, int nFNames ); + int c, fVerbose = 0; + char ** pArgvNew; + int nArgcNew; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + Gia_GenSandwich( pArgvNew, nArgcNew ); + return 0; +usage: + Abc_Print( -2, "usage: &gen_hie [-vh] ... \n" ); + Abc_Print( -2, "\t generates a hierarchical 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"); + Abc_Print( -2, "\t : the AIG files for the instance modules\n"); + Abc_Print( -2, "\t (the PO count of should not be less than the PI count of )\n"); + return 1;} + /**Function************************************************************* diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c index abf5b55ab..7cdd20584 100644 --- a/src/base/abci/abcCut.c +++ b/src/base/abci/abcCut.c @@ -72,7 +72,7 @@ void Abc_NtkCutsSubtractFanunt( Abc_Ntk_t * pNtk ) Counter++; } } - printf("Substracted %d fanouts\n", Counter ); + printf("Subtracted %d fanouts\n", Counter ); } /**Function************************************************************* diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c index 7bac74bf5..11605eb14 100644 --- a/src/base/abci/abcLutmin.c +++ b/src/base/abci/abcLutmin.c @@ -112,6 +112,7 @@ void Abc_NtkCheckAbsorb( Abc_Ntk_t * pNtk, int nLutSize ) Counter, 100.0 * Counter / Abc_NtkNodeNum(pNtk), Counter2, 100.0 * Counter2 / Abc_NtkNodeNum(pNtk) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + Vec_IntFree( vCounts ); } /**Function************************************************************* diff --git a/src/base/abci/abcSaucy.c b/src/base/abci/abcSaucy.c index faf870bf3..0fc3b4b9c 100644 --- a/src/base/abci/abcSaucy.c +++ b/src/base/abci/abcSaucy.c @@ -2483,6 +2483,8 @@ saucy_search( /* Keep running till we're out of automorphisms */ while (do_search(s)); + + ABC_FREE(g); } void diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c index 1341630bd..762156520 100644 --- a/src/base/abci/abcTiming.c +++ b/src/base/abci/abcTiming.c @@ -652,7 +652,7 @@ void Abc_NtkTimePrint( Abc_Ntk_t * pNtk ) /**Function************************************************************* - Synopsis [Expends the storage for timing information.] + Synopsis [Expands the storage for timing information.] Description [] diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index fe7286b77..67c02cab8 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -740,7 +740,7 @@ int CmdCommandSource( Abc_Frame_t * pAbc, int argc, char **argv ) usage: fprintf( pAbc->Err, "usage: source [-psxh] \n" ); fprintf( pAbc->Err, "\t-p supply prompt before reading each line [default = %s]\n", prompt? "yes": "no" ); - fprintf( pAbc->Err, "\t-s silently ignore nonexistant file [default = %s]\n", silent? "yes": "no" ); + fprintf( pAbc->Err, "\t-s silently ignore nonexistent file [default = %s]\n", silent? "yes": "no" ); fprintf( pAbc->Err, "\t-x echo each line as it is executed [default = %s]\n", echo? "yes": "no" ); fprintf( pAbc->Err, "\t-h print the command usage\n" ); return 1; @@ -2445,7 +2445,7 @@ int CmdCommandStarter( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: starter [-N num] [-C cmd] [-vh] \n" ); Abc_Print( -2, "\t runs command lines listed in concurrently on CPUs\n" ); - Abc_Print( -2, "\t-N num : the number of concurrent jobs including the controler [default = %d]\n", nCores ); + Abc_Print( -2, "\t-N num : the number of concurrent jobs including the controller [default = %d]\n", nCores ); Abc_Print( -2, "\t-C cmd : (optional) ABC command line to execute on benchmarks in \n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -2557,7 +2557,7 @@ int CmdCommandAutoTuner( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: autotuner [-N num] [-C file] [-F file] [-vh]\n" ); Abc_Print( -2, "\t performs autotuning\n" ); - Abc_Print( -2, "\t-N num : the number of concurrent jobs including the controler [default = %d]\n", nCores ); + Abc_Print( -2, "\t-N num : the number of concurrent jobs including the controller [default = %d]\n", nCores ); Abc_Print( -2, "\t-C cmd : configuration file with settings for autotuning\n" ); Abc_Print( -2, "\t-F cmd : list of AIGER files to be used for autotuning\n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); diff --git a/src/base/cmd/cmdHist.c b/src/base/cmd/cmdHist.c index b8cfc98f9..0aaf6d5cf 100644 --- a/src/base/cmd/cmdHist.c +++ b/src/base/cmd/cmdHist.c @@ -102,7 +102,7 @@ void Cmd_HistoryAddCommand( Abc_Frame_t * p, const char * command ) ***********************************************************************/ void Cmd_HistoryRead( Abc_Frame_t * p ) { -#if defined(WIN32) && defined(ABC_USE_HISTORY) +#if defined(ABC_USE_HISTORY) char Buffer[ABC_MAX_STR]; FILE * pFile; assert( Vec_PtrSize(p->aHistory) == 0 ); @@ -133,7 +133,7 @@ void Cmd_HistoryRead( Abc_Frame_t * p ) ***********************************************************************/ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit ) { -#if defined(WIN32) && defined(ABC_USE_HISTORY) +#if defined(ABC_USE_HISTORY) FILE * pFile; char * pStr; int i; @@ -163,7 +163,7 @@ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit ) ***********************************************************************/ void Cmd_HistoryPrint( Abc_Frame_t * p, int Limit ) { -#if defined(WIN32) && defined(ABC_USE_HISTORY) +#if defined(ABC_USE_HISTORY) char * pStr; int i; Limit = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory)-Limit ); diff --git a/src/base/exor/exorUtil.c b/src/base/exor/exorUtil.c index 105a64903..bd0fcf277 100644 --- a/src/base/exor/exorUtil.c +++ b/src/base/exor/exorUtil.c @@ -189,7 +189,7 @@ int WriteResultIntoFile( char * pFileName ) pFile = fopen( pFileName, "w" ); if ( pFile == NULL ) { - fprintf( pFile, "\n\nCannot open the output file\n" ); + fprintf( stderr, "\n\nCannot open the output file\n" ); return 1; } diff --git a/src/base/io/io.c b/src/base/io/io.c index 524cff34d..7b8ca184e 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -1192,7 +1192,7 @@ usage: fprintf( pAbc->Err, "\t-x : toggles between bin and hex notation [default = %s]\n", fHex? "hex":"bin" ); fprintf( pAbc->Err, "\t-f : toggles reading truth table(s) from file [default = %s]\n", fFile? "yes": "no" ); fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); - fprintf( pAbc->Err, "\ttruth : truth table with most signficant bit first (e.g. 1000 for AND(a,b))\n" ); + fprintf( pAbc->Err, "\ttruth : truth table with most significant bit first (e.g. 1000 for AND(a,b))\n" ); fprintf( pAbc->Err, "\tfile : file name with the truth table\n" ); return 1; } @@ -1542,7 +1542,7 @@ int IoCommandWrite( Abc_Frame_t * pAbc, int argc, char **argv ) if ( !strcmp( Extra_FileNameExtension(pFileName), "genlib" ) ) sprintf( Command, "write_genlib %s", pFileName ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "lib" ) ) - sprintf( Command, "write_liberty %s", pFileName ); + sprintf( Command, "write_lib %s", pFileName ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "dsd" ) ) sprintf( Command, "dsd_save %s", pFileName ); if ( Command[0] ) diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index e5c6fe49e..c8c14581a 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -548,10 +548,10 @@ typedef struct buflist { struct buflist * next; } buflist; -char * Io_MvLoadFileBz2( char * pFileName, int * pnFileSize ) +char * Io_MvLoadFileBz2( char * pFileName, long * pnFileSize ) { FILE * pFile; - int nFileSize = 0; + long nFileSize = 0; char * pContents; BZFILE * b; int bzError, RetValue; @@ -628,12 +628,12 @@ char * Io_MvLoadFileBz2( char * pFileName, int * pnFileSize ) SeeAlso [] ***********************************************************************/ -static char * Io_MvLoadFileGz( char * pFileName, int * pnFileSize ) +static char * Io_MvLoadFileGz( char * pFileName, long * pnFileSize ) { const int READ_BLOCK_SIZE = 100000; gzFile pFile; char * pContents; - int amtRead, readBlock, nFileSize = READ_BLOCK_SIZE; + long amtRead, readBlock, nFileSize = READ_BLOCK_SIZE; pFile = gzopen( pFileName, "rb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen pContents = ABC_ALLOC( char, nFileSize ); readBlock = 0; @@ -665,7 +665,7 @@ static char * Io_MvLoadFileGz( char * pFileName, int * pnFileSize ) static char * Io_MvLoadFile( char * pFileName ) { FILE * pFile; - int nFileSize; + long nFileSize; char * pContents; int RetValue; if ( !strncmp(pFileName+strlen(pFileName)-4,".bz2",4) ) diff --git a/src/base/io/ioReadDsd.c b/src/base/io/ioReadDsd.c index 098456998..6d64a053c 100644 --- a/src/base/io/ioReadDsd.c +++ b/src/base/io/ioReadDsd.c @@ -205,7 +205,7 @@ Abc_Obj_t * Io_ReadDsd_rec( Abc_Ntk_t * pNtk, char * pCur, char * pSop ) pEnd++; if ( *pEnd != '(' ) { - printf( "Cannot find the end of hexidecimal truth table.\n" ); + printf( "Cannot find the end of hexadecimal truth table.\n" ); return NULL; } diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index ddfcc91a8..eef80efa3 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -157,8 +157,10 @@ Abc_Ntk_t * Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck fprintf( stdout, "Reading network from file has failed.\n" ); return NULL; } - if ( fCheck && (Abc_NtkBlackboxNum(pNtk) || Abc_NtkWhiteboxNum(pNtk)) ) + + if ( fCheck && (Abc_NtkBlackboxNum(pNtk) || Abc_NtkWhiteboxNum(pNtk)) && pNtk->pDesign ) { + int i, fCycle = 0; Abc_Ntk_t * pModel; // fprintf( stdout, "Warning: The network contains hierarchy.\n" ); @@ -390,7 +392,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) pNtkTemp = Abc_NtkToNetlist( pNtk ); else { - fprintf( stdout, "Latches are writen into the PLA file at PI/PO pairs.\n" ); + fprintf( stdout, "Latches are written into the PLA file at PI/PO pairs.\n" ); pNtkCopy = Abc_NtkDup( pNtk ); Abc_NtkMakeComb( pNtkCopy, 0 ); pNtkTemp = Abc_NtkToNetlist( pNtk ); diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c index 09cbe90f3..06e4392c9 100644 --- a/src/base/wln/wlnCom.c +++ b/src/base/wln/wlnCom.c @@ -206,7 +206,7 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: %%yosys [-T ] [-D ] [-bismcvh] \n" ); Abc_Print( -2, "\t reads Verilog or SystemVerilog using Yosys\n" ); - Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\"\n" ); + Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\")\n" ); Abc_Print( -2, "\t-D : specify defines to be used by Yosys (default \"not used\")\n" ); Abc_Print( -2, "\t-b : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", fBlast? "yes": "no" ); Abc_Print( -2, "\t-i : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" ); diff --git a/src/base/wln/wlnRead.c b/src/base/wln/wlnRead.c index 83dd850ba..dfbe74f8a 100644 --- a/src/base/wln/wlnRead.c +++ b/src/base/wln/wlnRead.c @@ -2748,6 +2748,7 @@ Gia_Man_t * Gia_ManDupPermIO( Gia_Man_t * p, Vec_Int_t * vPermI, Vec_Int_t * vPe assert( Vec_IntSize(vPermI) == Gia_ManCiNum(p) ); assert( Vec_IntSize(vPermO) == Gia_ManCoNum(p) ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav(p->pName); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) Gia_ManCi(p, Vec_IntEntry(vPermI, i))->Value = Gia_ManAppendCi(pNew); diff --git a/src/bdd/cudd/cuddSubsetSP.c b/src/bdd/cudd/cuddSubsetSP.c index dc490f162..46442d547 100644 --- a/src/bdd/cudd/cuddSubsetSP.c +++ b/src/bdd/cudd/cuddSubsetSP.c @@ -1099,7 +1099,7 @@ CreatePathTable( st__free_table(pathTable); goto OUT_OF_MEM; } else if (insertValue == 1) { - fprintf(fp, "Something wrong, the entry exists but didnt show up in st__lookup\n"); + fprintf(fp, "Something wrong, the entry exists but didn't show up in st__lookup\n"); return(NULL); } diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c index 13e45f47e..9195fc8e0 100644 --- a/src/map/if/ifTune.c +++ b/src/map/if/ifTune.c @@ -269,7 +269,7 @@ int Ifn_NtkParseInt_rec( char * pStr, Ifn_Ntk_t * p, char ** ppFinal, int * piNo pFanins[nFanins++] = *piNode - 1; } else - return Ifn_ErrorMessage( "Substring \"%s\" contans unrecognized symbol \'%c\'.\n", pStr, pStr[0] ); + return Ifn_ErrorMessage( "Substring \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[0] ); } assert( pStr == pLim ); pObj = p->Nodes + (*piNode)++; @@ -400,7 +400,7 @@ int Ifn_NtkParseInt2( char * pStr, Ifn_Ntk_t * p ) else if ( pStr[k+2] == '{' ) p->Nodes[i].Type = IFN_DSD_PRIME, Next = '}'; else - return Ifn_ErrorMessage( "Cannot find openning operation symbol in the definition of signal \'%c\'.\n", 'a' + i ); + return Ifn_ErrorMessage( "Cannot find opening operation symbol in the definition of signal \'%c\'.\n", 'a' + i ); for ( n = k + 3; pStr[n]; n++ ) if ( pStr[n] == Next ) break; diff --git a/src/map/mpm/mpmMan.c b/src/map/mpm/mpmMan.c index d2777b575..4648148de 100644 --- a/src/map/mpm/mpmMan.c +++ b/src/map/mpm/mpmMan.c @@ -188,7 +188,7 @@ void Mpm_ManPrintStats( Mpm_Man_t * p ) Abc_Print( 1, "Runtime breakdown:\n" ); ABC_PRTP( "Complete cut computation ", p->timeDerive , p->timeTotal ); ABC_PRTP( "- Merging cuts ", p->timeMerge , p->timeTotal ); - ABC_PRTP( "- Evaluting cut parameters ", p->timeEval , p->timeTotal ); + ABC_PRTP( "- Evaluating cut parameters ", p->timeEval , p->timeTotal ); ABC_PRTP( "- Checking cut containment ", p->timeCompare, p->timeTotal ); ABC_PRTP( "- Adding cuts to storage ", p->timeStore , p->timeTotal ); ABC_PRTP( "Other ", p->timeOther , p->timeTotal ); diff --git a/src/map/scl/scl.c b/src/map/scl/scl.c index 7c3927ec0..8671d958e 100644 --- a/src/map/scl/scl.c +++ b/src/map/scl/scl.c @@ -130,7 +130,36 @@ void Scl_End( Abc_Frame_t * pAbc ) Scl_ConUpdateMan( pAbc, NULL ); } +/**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +SC_Lib * Scl_ReadLibraryFile( Abc_Frame_t * pAbc, char * pFileName, int fVerbose, int fVeryVerbose, SC_DontUse dont_use ) +{ + SC_Lib * pLib; + FILE * pFile; + if ( (pFile = fopen( pFileName, "rb" )) == NULL ) + { + fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName ); + return NULL; + } + fclose( pFile ); + // read new library + pLib = Abc_SclReadLiberty( pFileName, fVerbose, fVeryVerbose, dont_use); + if ( pLib == NULL ) + { + fprintf( pAbc->Err, "Reading SCL library from file \"%s\" has failed. \n", pFileName ); + return NULL; + } + return pLib; +} /**Function************************************************************* @@ -145,8 +174,6 @@ void Scl_End( Abc_Frame_t * pAbc ) ***********************************************************************/ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv ) { - char * pFileName; - FILE * pFile; SC_Lib * pLib; int c, fDump = 0; float Slew = 0; @@ -230,25 +257,29 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( argc != globalUtilOptind + 1 ) - goto usage; - // get the input file name - pFileName = argv[globalUtilOptind]; - if ( (pFile = fopen( pFileName, "rb" )) == NULL ) - { - fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName ); + if ( argc == globalUtilOptind + 2 ) { // expecting two files + SC_Lib * pLib1 = Scl_ReadLibraryFile( pAbc, argv[globalUtilOptind], fVerbose, fVeryVerbose, dont_use ); + SC_Lib * pLib2 = Scl_ReadLibraryFile( pAbc, argv[globalUtilOptind+1], fVerbose, fVeryVerbose, dont_use ); ABC_FREE(dont_use.dont_use_list); - return 1; + if ( pLib1 == NULL || pLib2 == NULL ) { + if (pLib1) Abc_SclLibFree(pLib1); + if (pLib2) Abc_SclLibFree(pLib2); + return 1; + } + pLib = Abc_SclMergeLibraries( pLib1, pLib2 ); + Abc_SclLibFree(pLib1); + Abc_SclLibFree(pLib2); } - fclose( pFile ); - // read new library - pLib = Abc_SclReadLiberty( pFileName, fVerbose, fVeryVerbose, dont_use); - ABC_FREE(dont_use.dont_use_list); - if ( pLib == NULL ) - { - fprintf( pAbc->Err, "Reading SCL library from file \"%s\" has failed. \n", pFileName ); - return 1; + else if ( argc == globalUtilOptind + 1 ) { // expecting one file + pLib = Scl_ReadLibraryFile( pAbc, argv[globalUtilOptind], fVerbose, fVeryVerbose, dont_use ); + ABC_FREE(dont_use.dont_use_list); } + else { + ABC_FREE(dont_use.dont_use_list); + goto usage; + } + if ( pLib == NULL ) + return 1; if ( Abc_SclLibClassNum(pLib) < 3 ) { fprintf( pAbc->Err, "Library with only %d cell classes cannot be used.\n", Abc_SclLibClassNum(pLib) ); @@ -261,7 +292,7 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_SclShortNames( pLib ); // dump the resulting library if ( fDump && pAbc->pLibScl ) - Abc_SclWriteLiberty( Extra_FileNameGenericAppend(pFileName, "_temp.lib"), (SC_Lib *)pAbc->pLibScl ); + Abc_SclWriteLiberty( Extra_FileNameGenericAppend(argv[globalUtilOptind], "_temp.lib"), (SC_Lib *)pAbc->pLibScl ); if ( fUnit ) { SC_Cell * pCell; int i; @@ -277,7 +308,7 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pAbc->Err, "usage: read_lib [-SG float] [-M num] [-dnuvwh] [-X cell_name] \n" ); + fprintf( pAbc->Err, "usage: read_lib [-SG float] [-M num] [-dnuvwh] [-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 ); @@ -290,6 +321,7 @@ usage: fprintf( pAbc->Err, "\t-w : toggle writing information about skipped gates [default = %s]\n", fVeryVerbose? "yes": "no" ); fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); fprintf( pAbc->Err, "\t : the name of a file to read\n" ); + fprintf( pAbc->Err, "\t : the name of a file to read (optional)\n" ); return 1; } @@ -1083,7 +1115,7 @@ int Scl_CommandBuffer( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !pPars->fSizeOnly && !pPars->fAddBufs && pNtk->vPhases == NULL ) { - Abc_Print( -1, "Fanin phase information is not avaiable.\n" ); + Abc_Print( -1, "Fanin phase information is not available.\n" ); return 1; } if ( !pAbc->pLibScl || !Abc_SclHasDelayInfo(pAbc->pLibScl) ) @@ -1104,9 +1136,9 @@ int Scl_CommandBuffer( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pAbc->Err, "usage: buffer [-GSN num] [-sbpcvwh]\n" ); - fprintf( pAbc->Err, "\t performs buffering and sizing and mapped network\n" ); + fprintf( pAbc->Err, "\t performs buffering and sizing on mapped network\n" ); fprintf( pAbc->Err, "\t-G : target gain percentage [default = %d]\n", pPars->GainRatio ); - fprintf( pAbc->Err, "\t-S : target slew in pisoseconds [default = %d]\n", pPars->Slew ); + fprintf( pAbc->Err, "\t-S : target slew in picoseconds [default = %d]\n", pPars->Slew ); fprintf( pAbc->Err, "\t-N : the maximum fanout count [default = %d]\n", pPars->nDegree ); fprintf( pAbc->Err, "\t-s : toggle performing only sizing [default = %s]\n", pPars->fSizeOnly? "yes": "no" ); fprintf( pAbc->Err, "\t-b : toggle using buffers instead of inverters [default = %s]\n", pPars->fAddBufs? "yes": "no" ); @@ -1219,7 +1251,7 @@ int Scl_CommandBufferOld( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( fAddInvs && pNtk->vPhases == NULL ) { - Abc_Print( -1, "Fanin phase information is not avaiable.\n" ); + Abc_Print( -1, "Fanin phase information is not available.\n" ); return 1; } if ( !pAbc->pLibScl || !Abc_SclHasDelayInfo(pAbc->pLibScl) ) @@ -1755,9 +1787,9 @@ int Scl_CommandDnsize( Abc_Frame_t * pAbc, int argc, char **argv ) usage: fprintf( pAbc->Err, "usage: dnsize [-IJNDGTX num] [-csdvwh]\n" ); fprintf( pAbc->Err, "\t selectively decreases gate sizes while maintaining delay\n" ); - fprintf( pAbc->Err, "\t-I : the number of upsizing iterations to perform [default = %d]\n", pPars->nIters ); + fprintf( pAbc->Err, "\t-I : the number of downsizing iterations to perform [default = %d]\n", pPars->nIters ); fprintf( pAbc->Err, "\t-J : the number of iterations without improvement to stop [default = %d]\n", pPars->nIterNoChange ); - fprintf( pAbc->Err, "\t-N : limit on discrete upsizing steps at a node [default = %d]\n", pPars->Notches ); + fprintf( pAbc->Err, "\t-N : limit on discrete downsizing steps at a node [default = %d]\n", pPars->Notches ); fprintf( pAbc->Err, "\t-D : delay target set by the user, in picoseconds [default = %d]\n", pPars->DelayUser ); fprintf( pAbc->Err, "\t-G : delay gap during updating, in picoseconds [default = %d]\n", pPars->DelayGap ); fprintf( pAbc->Err, "\t-T : approximate timeout in seconds [default = %d]\n", pPars->TimeOut ); diff --git a/src/map/scl/sclDnsize.c b/src/map/scl/sclDnsize.c index 19e4b30c7..5be9e3a34 100644 --- a/src/map/scl/sclDnsize.c +++ b/src/map/scl/sclDnsize.c @@ -265,7 +265,7 @@ void Abc_SclDnsizePerformInt( SC_Lib * pLib, Abc_Ntk_t * pNtk, SC_SizePars * pPa assert( p->vGatesBest == NULL ); p->vGatesBest = Vec_IntDup( p->pNtk->vGates ); - // perform upsizing + // perform downsizing vNodes = Vec_IntAlloc( 1000 ); vEvals = Vec_IntAlloc( 1000 ); vTryLater = Vec_IntAlloc( 1000 ); diff --git a/src/map/scl/sclLib.h b/src/map/scl/sclLib.h index 46fb8da6f..08a9066a5 100644 --- a/src/map/scl/sclLib.h +++ b/src/map/scl/sclLib.h @@ -748,6 +748,7 @@ extern SC_Lib * Abc_SclReadFromStr( Vec_Str_t * vOut ); extern SC_Lib * Abc_SclReadFromFile( char * pFileName ); extern void Abc_SclWriteScl( char * pFileName, SC_Lib * p ); extern void Abc_SclWriteLiberty( char * pFileName, SC_Lib * p ); +extern SC_Lib * Abc_SclMergeLibraries( SC_Lib * pLib1, SC_Lib * pLib2 ); /*=== sclLibUtil.c ===============================================================*/ extern void Abc_SclHashCells( SC_Lib * p ); extern int Abc_SclCellFind( SC_Lib * p, char * pName ); diff --git a/src/map/scl/sclLibScl.c b/src/map/scl/sclLibScl.c index a06d01343..e13a746e6 100644 --- a/src/map/scl/sclLibScl.c +++ b/src/map/scl/sclLibScl.c @@ -483,71 +483,22 @@ static void Abc_SclWriteSurface( Vec_Str_t * vOut, SC_Surface * p ) for ( i = 0; i < 6; i++ ) Vec_StrPutF( vOut, p->approx[2][i] ); } -static void Abc_SclWriteLibrary( Vec_Str_t * vOut, SC_Lib * p ) +static void Abc_SclWriteLibraryCellsOnly( Vec_Str_t * vOut, SC_Lib * p, int fAddOn ) { - SC_WireLoad * pWL; - SC_WireLoadSel * pWLS; SC_Cell * pCell; SC_Pin * pPin; - int n_valid_cells; - int i, j, k; - - Vec_StrPutI( vOut, ABC_SCL_CUR_VERSION ); - - // Write non-composite fields: - Vec_StrPutS( vOut, p->pName ); - Vec_StrPutS( vOut, p->default_wire_load ); - Vec_StrPutS( vOut, p->default_wire_load_sel ); - Vec_StrPutF( vOut, p->default_max_out_slew ); - - assert( p->unit_time >= 0 ); - assert( p->unit_cap_snd >= 0 ); - Vec_StrPutI( vOut, p->unit_time ); - Vec_StrPutF( vOut, p->unit_cap_fst ); - Vec_StrPutI( vOut, p->unit_cap_snd ); - - // Write 'wire_load' vector: - Vec_StrPutI( vOut, Vec_PtrSize(&p->vWireLoads) ); - SC_LibForEachWireLoad( p, pWL, i ) - { - Vec_StrPutS( vOut, pWL->pName ); - Vec_StrPutF( vOut, pWL->cap ); - Vec_StrPutF( vOut, pWL->slope ); - - Vec_StrPutI( vOut, Vec_IntSize(&pWL->vFanout) ); - for ( j = 0; j < Vec_IntSize(&pWL->vFanout); j++ ) - { - Vec_StrPutI( vOut, Vec_IntEntry(&pWL->vFanout, j) ); - Vec_StrPutF( vOut, Vec_FltEntry(&pWL->vLen, j) ); - } - } - - // Write 'wire_load_sel' vector: - Vec_StrPutI( vOut, Vec_PtrSize(&p->vWireLoadSels) ); - SC_LibForEachWireLoadSel( p, pWLS, i ) - { - Vec_StrPutS( vOut, pWLS->pName ); - Vec_StrPutI( vOut, Vec_FltSize(&pWLS->vAreaFrom) ); - for ( j = 0; j < Vec_FltSize(&pWLS->vAreaFrom); j++) - { - Vec_StrPutF( vOut, Vec_FltEntry(&pWLS->vAreaFrom, j) ); - Vec_StrPutF( vOut, Vec_FltEntry(&pWLS->vAreaTo, j) ); - Vec_StrPutS( vOut, (char *)Vec_PtrEntry(&pWLS->vWireLoadModel, j) ); - } - } - - // Write 'cells' vector: - n_valid_cells = 0; - SC_LibForEachCell( p, pCell, i ) - if ( !(pCell->seq || pCell->unsupp) ) - n_valid_cells++; - - Vec_StrPutI( vOut, n_valid_cells ); + int i, j, k; SC_LibForEachCell( p, pCell, i ) { if ( pCell->seq || pCell->unsupp ) continue; + if ( fAddOn ) { + Vec_StrPush( vOut, 'L' ); + Vec_StrPush( vOut, '0'+(char)fAddOn ); + Vec_StrPush( vOut, '_' ); + } + Vec_StrPutS( vOut, pCell->pName ); Vec_StrPutF( vOut, pCell->area ); Vec_StrPutF( vOut, pCell->leakage ); @@ -608,13 +559,78 @@ static void Abc_SclWriteLibrary( Vec_Str_t * vOut, SC_Lib * p ) assert( Vec_PtrSize(&pRTime->vTimings) == 0 ); } } + } +} +int Abc_SclCountValidCells( SC_Lib * p ) +{ + SC_Cell * pCell; + int i, n_valid_cells = 0; + SC_LibForEachCell( p, pCell, i ) + if ( !(pCell->seq || pCell->unsupp) ) + n_valid_cells++; + return n_valid_cells; +} +static void Abc_SclWriteLibrary( Vec_Str_t * vOut, SC_Lib * p, int nExtra ) +{ + SC_WireLoad * pWL; + SC_WireLoadSel * pWLS; + int n_valid_cells; + int i, j; + + Vec_StrPutI( vOut, ABC_SCL_CUR_VERSION ); + + // Write non-composite fields: + Vec_StrPutS( vOut, p->pName ); + Vec_StrPutS( vOut, p->default_wire_load ); + Vec_StrPutS( vOut, p->default_wire_load_sel ); + Vec_StrPutF( vOut, p->default_max_out_slew ); + + assert( p->unit_time >= 0 ); + assert( p->unit_cap_snd >= 0 ); + Vec_StrPutI( vOut, p->unit_time ); + Vec_StrPutF( vOut, p->unit_cap_fst ); + Vec_StrPutI( vOut, p->unit_cap_snd ); + + // Write 'wire_load' vector: + Vec_StrPutI( vOut, Vec_PtrSize(&p->vWireLoads) ); + SC_LibForEachWireLoad( p, pWL, i ) + { + Vec_StrPutS( vOut, pWL->pName ); + Vec_StrPutF( vOut, pWL->cap ); + Vec_StrPutF( vOut, pWL->slope ); + + Vec_StrPutI( vOut, Vec_IntSize(&pWL->vFanout) ); + for ( j = 0; j < Vec_IntSize(&pWL->vFanout); j++ ) + { + Vec_StrPutI( vOut, Vec_IntEntry(&pWL->vFanout, j) ); + Vec_StrPutF( vOut, Vec_FltEntry(&pWL->vLen, j) ); + } } + + // Write 'wire_load_sel' vector: + Vec_StrPutI( vOut, Vec_PtrSize(&p->vWireLoadSels) ); + SC_LibForEachWireLoadSel( p, pWLS, i ) + { + Vec_StrPutS( vOut, pWLS->pName ); + Vec_StrPutI( vOut, Vec_FltSize(&pWLS->vAreaFrom) ); + for ( j = 0; j < Vec_FltSize(&pWLS->vAreaFrom); j++) + { + Vec_StrPutF( vOut, Vec_FltEntry(&pWLS->vAreaFrom, j) ); + Vec_StrPutF( vOut, Vec_FltEntry(&pWLS->vAreaTo, j) ); + Vec_StrPutS( vOut, (char *)Vec_PtrEntry(&pWLS->vWireLoadModel, j) ); + } + } + + // Write 'cells' vector: + n_valid_cells = Abc_SclCountValidCells( p ); + Vec_StrPutI( vOut, n_valid_cells + nExtra ); + Abc_SclWriteLibraryCellsOnly( vOut, p, (int)(nExtra > 0) ); } void Abc_SclWriteScl( char * pFileName, SC_Lib * p ) { Vec_Str_t * vOut; vOut = Vec_StrAlloc( 10000 ); - Abc_SclWriteLibrary( vOut, p ); + Abc_SclWriteLibrary( vOut, p, 0 ); if ( Vec_StrSize(vOut) > 0 ) { FILE * pFile = fopen( pFileName, "wb" ); @@ -835,10 +851,36 @@ void Abc_SclWriteLiberty( char * pFileName, SC_Lib * p ) { Abc_SclWriteLibraryText( pFile, p ); fclose( pFile ); - printf( "Dumped internal library into Liberty file \"%s\".\n", pFileName ); + printf( "Dumped internal library with %d cells into Liberty file \"%s\".\n", SC_LibCellNum(p), pFileName ); } } +/**Function************************************************************* + + Synopsis [Appends cells of pLib2 to those of pLib1.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +SC_Lib * Abc_SclMergeLibraries( SC_Lib * pLib1, SC_Lib * pLib2 ) +{ + Vec_Str_t * vOut = Vec_StrAlloc( 10000 ); + int n_valid_cells2 = Abc_SclCountValidCells( pLib2 ); + Abc_SclWriteLibrary( vOut, pLib1, n_valid_cells2 ); + Abc_SclWriteLibraryCellsOnly( vOut, pLib2, 2 ); + SC_Lib * p = Abc_SclReadFromStr( vOut ); + p->pFileName = Abc_UtilStrsav( pLib1->pFileName ); + p->pName = ABC_ALLOC( char, strlen(pLib1->pName) + strlen(pLib2->pName) + 10 ); + sprintf( p->pName, "%s__and__%s", pLib1->pName, pLib2->pName ); + Vec_StrFree( vOut ); + printf( "Updated library \"%s\" with additional %d cells from library \"%s\".\n", pLib1->pName, n_valid_cells2, pLib2->pName ); + return p; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/scl/sclLiberty.c b/src/map/scl/sclLiberty.c index 24737f35b..674f65549 100644 --- a/src/map/scl/sclLiberty.c +++ b/src/map/scl/sclLiberty.c @@ -70,7 +70,7 @@ struct Scl_Tree_t_ { char * pFileName; // input Liberty file name char * pContents; // file contents - int nContents; // file size + long nContents; // file size int nLines; // line counter int nItems; // number of items int nItermAlloc; // number of items allocated @@ -521,10 +521,10 @@ void Scl_LibertyFixFileName( char * pFileName ) if ( *pHead == '>' ) *pHead = '\\'; } -int Scl_LibertyFileSize( char * pFileName ) +long Scl_LibertyFileSize( char * pFileName ) { FILE * pFile; - int nFileSize; + long nFileSize; pFile = fopen( pFileName, "rb" ); if ( pFile == NULL ) { @@ -536,7 +536,7 @@ int Scl_LibertyFileSize( char * pFileName ) fclose( pFile ); return nFileSize; } -char * Scl_LibertyFileContents( char * pFileName, int nContents ) +char * Scl_LibertyFileContents( char * pFileName, long nContents ) { FILE * pFile = fopen( pFileName, "rb" ); char * pContents = ABC_ALLOC( char, nContents+1 ); @@ -573,7 +573,7 @@ void Scl_LibertyStringDump( char * pFileName, Vec_Str_t * vStr ) Scl_Tree_t * Scl_LibertyStart( char * pFileName ) { Scl_Tree_t * p; - int RetValue; + long RetValue; // read the file into the buffer Scl_LibertyFixFileName( pFileName ); RetValue = Scl_LibertyFileSize( pFileName ); @@ -867,7 +867,7 @@ int Scl_LibertyReadTimeUnit( Scl_Tree_t * p ) return 12; break; } - printf( "Libery parser cannot read \"time_unit\". Assuming time_unit : \"1ns\".\n" ); + printf( "Liberty parser cannot read \"time_unit\". Assuming time_unit : \"1ns\".\n" ); return 9; } void Scl_LibertyReadLoadUnit( Scl_Tree_t * p, Vec_Str_t * vOut ) @@ -887,7 +887,7 @@ void Scl_LibertyReadLoadUnit( Scl_Tree_t * p, Vec_Str_t * vOut ) else break; return; } - printf( "Libery parser cannot read \"capacitive_load_unit\". Assuming capacitive_load_unit(1, pf).\n" ); + printf( "Liberty parser cannot read \"capacitive_load_unit\". Assuming capacitive_load_unit(1, pf).\n" ); Vec_StrPutF_( vOut, 1.0 ); Vec_StrPutI_( vOut, 12 ); } diff --git a/src/map/scl/sclSize.c b/src/map/scl/sclSize.c index a6bfbeac7..e09c56e67 100644 --- a/src/map/scl/sclSize.c +++ b/src/map/scl/sclSize.c @@ -140,6 +140,9 @@ void Abc_SclTimeNtkPrint( SC_Man * p, int fShowAll, int fPrintPath ) Abc_Obj_t * pObj, * pPivot = Abc_SclFindCriticalCo( p, &fRise ); float maxDelay = Abc_SclObjTimeOne( p, pPivot, fRise ); p->ReportDelay = maxDelay; + // used for Floyds cycle detection algorithm + unsigned int tortoiseIndex = 0; + int tortoiseStep = 0; #ifdef WIN32 printf( "WireLoad = \"%s\" ", p->pWLoadUsed ? p->pWLoadUsed->pName : "none" ); @@ -197,7 +200,7 @@ void Abc_SclTimeNtkPrint( SC_Man * p, int fShowAll, int fPrintPath ) while ( pObj && Abc_ObjIsNode(pObj) ) { i++; - nLength = Abc_MaxInt( nLength, Abc_SclObjCell(pObj) ? strlen(Abc_SclObjCell(pObj)->pName) : 2 /* strlen("pi") */ ); + nLength = Abc_MaxInt( nLength, strlen(Abc_SclObjCell(pObj)->pName) ); pObj = Abc_SclFindMostCriticalFanin( p, &fRise, pObj ); } @@ -221,10 +224,18 @@ void Abc_SclTimeNtkPrint( SC_Man * p, int fShowAll, int fPrintPath ) Vec_PtrPush( vPath, pPivot ); pObj = Abc_ObjFanin0(pPivot); while ( pObj )//&& Abc_ObjIsNode(pObj) ) - { + { Vec_PtrPush( vPath, pObj ); pPrev = pObj; pObj = Abc_SclFindMostCriticalFanin( p, &fRise, pObj ); + + // move the tortoise at half the speed (trailing) + tortoiseStep = (tortoiseStep + 1) % 2; + tortoiseIndex += tortoiseStep; + // if they see the same element, we are in a loop + if(vPath->pArray[tortoiseIndex] == pObj) { + break; + } } Vec_PtrForEachEntryReverse( Abc_Obj_t *, vPath, pObj, i ) { @@ -913,3 +924,4 @@ void Abc_SclPrintBuffers( SC_Lib * pLib, Abc_Ntk_t * pNtk, int fVerbose ) ABC_NAMESPACE_IMPL_END + diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c index 81e4d3987..9029ddd03 100644 --- a/src/misc/extra/extraUtilUtil.c +++ b/src/misc/extra/extraUtilUtil.c @@ -394,9 +394,17 @@ ABC_NAMESPACE_IMPL_START double Extra_CpuTimeDouble() { +/* struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; +*/ + struct timespec ts; + if ( clock_gettime(CLOCK_MONOTONIC, &ts) < 0 ) + return (double)-1; + double res = ((double) ts.tv_sec); + res += ((double) ts.tv_nsec) / 1000000000; + return res; } #endif diff --git a/src/opt/dar/darRefact.c b/src/opt/dar/darRefact.c index 6083c035e..8016568a1 100644 --- a/src/opt/dar/darRefact.c +++ b/src/opt/dar/darRefact.c @@ -586,7 +586,7 @@ p->timeEval += Abc_Clock() - clk; // if we end up here, a rewriting step is accepted nNodeBefore = Aig_ManNodeNum( pAig ); pObjNew = Dar_RefactBuildGraph( pAig, p->vLeavesBest, p->pGraphBest ); - assert( (int)Aig_Regular(pObjNew)->Level <= Required ); + //assert( (int)Aig_Regular(pObjNew)->Level <= Required ); // replace the node Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel ); // compare the gains diff --git a/src/opt/dau/dauTree.c b/src/opt/dau/dauTree.c index 81bd51bc7..6279835af 100644 --- a/src/opt/dau/dauTree.c +++ b/src/opt/dau/dauTree.c @@ -1551,7 +1551,7 @@ int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned Counter++; if ( DAU_MAX_VAR < nKLutSize ) { - printf( "Paramater DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, nKLutSize ); + printf( "Parameter DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, nKLutSize ); return -1; } assert( iDsd[0] <= iDsd[1] ); @@ -1703,7 +1703,7 @@ int Mpm_FuncCompute( Dss_Man_t * p, int iDsd0, int iDsd1, Vec_Str_t * vShared, i assert( iDsd0 <= iDsd1 ); if ( DAU_MAX_VAR < *pnLeaves ) { - printf( "Paramater DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, *pnLeaves ); + printf( "Parameter DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, *pnLeaves ); return -1; } if ( fVerbose ) diff --git a/src/opt/rwr/rwrExp.c b/src/opt/rwr/rwrExp.c index 9d8455b49..92cc668dd 100644 --- a/src/opt/rwr/rwrExp.c +++ b/src/opt/rwr/rwrExp.c @@ -238,9 +238,9 @@ void Rwt_Man5ExplorePrint() if ( CountMax < Counter ) CountMax = Counter; } - printf( "Number of cuts considered = %8d.\n", nCuts ); - printf( "Classes occurring at least once = %8d.\n", stmm_count(s_pManRwrExp5->tTableNN) ); - printf( "The largest number of occurence = %8d.\n", CountMax ); + printf( "Number of cuts considered = %8d.\n", nCuts ); + printf( "Classes occurring at least once = %8d.\n", stmm_count(s_pManRwrExp5->tTableNN) ); + printf( "The largest number of occurrence = %8d.\n", CountMax ); // print the distribution of classes pDistrib = ABC_ALLOC( int, CountMax + 1 ); diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c index dc05df0f5..771577ca5 100644 --- a/src/opt/sim/simUtils.c +++ b/src/opt/sim/simUtils.c @@ -60,7 +60,8 @@ Vec_Ptr_t * Sim_UtilInfoAlloc( int nSize, int nWords, int fClean ) int i; assert( nSize > 0 && nWords > 0 ); vInfo = Vec_PtrAlloc( nSize ); - vInfo->pArray[0] = ABC_ALLOC( unsigned, nSize * nWords ); + vInfo->pArray[0] = ABC_ALLOC( unsigned, (long)nSize * (long)nWords ); + assert( vInfo->pArray[0]); if ( fClean ) memset( vInfo->pArray[0], 0, sizeof(unsigned) * nSize * nWords ); for ( i = 1; i < nSize; i++ ) diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index bd6b8c769..75f991d3b 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -1539,7 +1539,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) Abc_Print( 1, "LrnStart = %d LrnDelta = %d LrnRatio = %d %% Skip = %d SimpleCNF = %d Dump = %d\n", pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs ); if ( pPars->fDumpVabs || pPars->fDumpMabs ) - Abc_Print( 1, "%s will be continously dumped into file \"%s\".\n", + Abc_Print( 1, "%s will be continuously dumped into file \"%s\".\n", pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map", Ga2_GlaGetFileName(p, pPars->fDumpVabs) ); if ( pPars->fDumpMabs ) diff --git a/src/proof/abs/absRpmOld.c b/src/proof/abs/absRpmOld.c index fd5e82554..0833bd544 100644 --- a/src/proof/abs/absRpmOld.c +++ b/src/proof/abs/absRpmOld.c @@ -186,7 +186,7 @@ Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose ) Gia_ManStop( pTmp ); if ( fVerbose ) { - printf( "After FF-2-PI tranformation:\n" ); + printf( "After FF-2-PI transformation:\n" ); Gia_ManPrintStats( pNew, NULL ); } return pNew; diff --git a/src/proof/acec/acecFadds.c b/src/proof/acec/acecFadds.c index a2bdcfbeb..c17e81bca 100644 --- a/src/proof/acec/acecFadds.c +++ b/src/proof/acec/acecFadds.c @@ -860,7 +860,7 @@ Gia_Man_t * Gia_ManDupWithNaturalBoxes( Gia_Man_t * p, int nFaddMin, int fVerbos if ( Gia_ManRegNum(p) ) { if ( fVerbose ) - printf( "Warning: Sequential design is coverted into combinational one by adding white boxes.\n" ); + printf( "Warning: Sequential design is converted into combinational one by adding white boxes.\n" ); pNew->nRegs = 0; } assert( !Gia_ManHasDangling(pNew) ); diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 773bc6e3c..281deb0e9 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -101,6 +101,7 @@ struct Cec4_Man_t_ Vec_Int_t * vDisprPairs; Vec_Bit_t * vFails; Vec_Bit_t * vCoDrivers; + Vec_Int_t * vPairs; int iPosRead; // candidate reading position int iPosWrite; // candidate writing position int iLastConst; // last const node proved @@ -250,6 +251,7 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) p->vPat = Vec_IntAlloc( 100 ); p->vDisprPairs = Vec_IntAlloc( 100 ); p->vFails = Vec_BitStart( Gia_ManObjNum(pAig) ); + p->vPairs = pPars->fUseCones ? Vec_IntAlloc( 100 ) : NULL; //pAig->pData = p->pSat; // point AIG manager to the solver //Vec_IntFreeP( &p->pAig->vPats ); //p->pAig->vPats = Vec_IntAlloc( 1000 ); @@ -304,6 +306,7 @@ void Cec4_ManDestroy( Cec4_Man_t * p ) Vec_IntFreeP( &p->vPat ); Vec_IntFreeP( &p->vDisprPairs ); Vec_BitFreeP( &p->vFails ); + Vec_IntFreeP( &p->vPairs ); Vec_BitFreeP( &p->vCoDrivers ); Vec_IntFreeP( &p->vRefClasses ); Vec_IntFreeP( &p->vRefNodes ); @@ -1686,12 +1689,26 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr ) { p->nSatUndec++; assert( status == GLUCOSE_UNDEC ); - Gia_ObjSetFailed( p->pAig, iObj ); - Vec_BitWriteEntry( p->vFails, iObj, 1 ); - //if ( iRepr ) - //Vec_BitWriteEntry( p->vFails, iRepr, 1 ); - p->timeSatUndec += Abc_Clock() - clk; - RetValue = 2; + if ( p->vPairs ) // speculate + { + Vec_IntPushTwo( p->vPairs, Abc_Var2Lit(iRepr, 0), Abc_Var2Lit(iObj, fCompl) ); + p->timeSatUndec += Abc_Clock() - clk; + // mark as proved + pObj->Value = Abc_LitNotCond( pRepr->Value, fCompl ); + Gia_ObjSetProved( p->pAig, iObj ); + if ( iRepr == 0 ) + p->iLastConst = iObj; + RetValue = 1; + } + else + { + Gia_ObjSetFailed( p->pAig, iObj ); + Vec_BitWriteEntry( p->vFails, iObj, 1 ); + //if ( iRepr ) + //Vec_BitWriteEntry( p->vFails, iRepr, 1 ); + p->timeSatUndec += Abc_Clock() - clk; + RetValue = 2; + } } return RetValue; } @@ -1896,6 +1913,18 @@ finalize: pMan->nSatSat, pMan->nConflicts[0][0], (float)pMan->nConflicts[0][1]/Abc_MaxInt(1, pMan->nSatSat -pMan->nConflicts[0][0]), pMan->nConflicts[0][2], pMan->nSatUndec, pMan->nSimulates, pMan->nRecycles, 100.0*pMan->nGates[1]/Abc_MaxInt(1, pMan->nGates[0]+pMan->nGates[1]) ); + if ( pMan->vPairs && Vec_IntSize(pMan->vPairs) ) + { + extern char * Extra_FileNameGeneric( char * FileName ); + char pFileName[1000], * pBase = Extra_FileNameGeneric(p->pName); + extern Gia_Man_t * Gia_ManDupMiterCones( Gia_Man_t * p, Vec_Int_t * vPairs ); + Gia_Man_t * pM = Gia_ManDupMiterCones( p, pMan->vPairs ); + sprintf( pFileName, "%s_sm.aig", pBase ); + Gia_AigerWrite( pM, pFileName, 0, 0, 0 ); + Gia_ManStop( pM ); + ABC_FREE( pBase ); + printf( "Dumped miter \"%s\" with %d pairs.\n", pFileName, pMan->vPairs ? Vec_IntSize(pMan->vPairs)/2 : -1 ); + } Cec4_ManDestroy( pMan ); //Gia_ManStaticFanoutStop( p ); //Gia_ManEquivPrintClasses( p, 1, 0 ); diff --git a/src/proof/fraig/fraigInt.h b/src/proof/fraig/fraigInt.h index 37f007205..98e088e45 100644 --- a/src/proof/fraig/fraigInt.h +++ b/src/proof/fraig/fraigInt.h @@ -383,7 +383,7 @@ extern void Fraig_NodeSimulate( Fraig_Node_t * pNode, int iWordSt /*=== fraigPrime.c =============================================================*/ extern int s_FraigPrimes[FRAIG_MAX_PRIMES]; /*=== fraigSat.c ===============================================================*/ -extern int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ); +extern int Fraig_NodeIsImplification( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ); /*=== fraigTable.c =============================================================*/ extern Fraig_HashTable_t * Fraig_HashTableCreate( int nSize ); extern void Fraig_HashTableFree( Fraig_HashTable_t * p ); diff --git a/src/proof/fraig/fraigSat.c b/src/proof/fraig/fraigSat.c index 7cad3eab3..433cc4f99 100644 --- a/src/proof/fraig/fraigSat.c +++ b/src/proof/fraig/fraigSat.c @@ -548,7 +548,7 @@ p->time3 += Abc_Clock() - clk; SeeAlso [] ***********************************************************************/ -int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ) +int Fraig_NodeIsImplification( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ) { int RetValue, RetValue1, i, fComp; abctime clk; diff --git a/src/proof/fraig/fraigUtil.c b/src/proof/fraig/fraigUtil.c index 7869c6d61..d5e8b59bf 100644 --- a/src/proof/fraig/fraigUtil.c +++ b/src/proof/fraig/fraigUtil.c @@ -872,13 +872,13 @@ clk = Abc_Clock(); pNode2 = vPivots->pArray[k]; if ( Fraig_NodeSimsContained( pMan, pNode, pNode2 ) ) { - if ( Fraig_NodeIsImplication( pMan, pNode, pNode2, -1 ) ) + if ( Fraig_NodeIsImplification( pMan, pNode, pNode2, -1 ) ) nProved++; Counter++; } else if ( Fraig_NodeSimsContained( pMan, pNode2, pNode ) ) { - if ( Fraig_NodeIsImplication( pMan, pNode2, pNode, -1 ) ) + if ( Fraig_NodeIsImplification( pMan, pNode2, pNode, -1 ) ) nProved++; Counter++; } diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c index 2dd03f31c..f18c33363 100644 --- a/src/sat/bmc/bmcMulti.c +++ b/src/sat/bmc/bmcMulti.c @@ -175,7 +175,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d %%.\n", pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc ); if ( pPars->fVerbose ) - printf( "Gap timout = %d sec. Per-output timeout = %d msec. Use synthesis = %d. Dump final = %d. Verbose = %d.\n", + printf( "Gap timeout = %d sec. Per-output timeout = %d msec. Use synthesis = %d. Dump final = %d. Verbose = %d.\n", pPars->TimeOutGap, pPars->TimePerOut, pPars->fUseSyn, pPars->fDumpFinal, pPars->fVerbose ); // create output map vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c index 7886b8a3b..e67328171 100644 --- a/src/sat/cnf/cnfUtil.c +++ b/src/sat/cnf/cnfUtil.c @@ -21,8 +21,6 @@ #include "cnf.h" #include "sat/bsat/satSolver.h" -ABC_NAMESPACE_IMPL_START - #ifdef _MSC_VER #define unlink _unlink #else @@ -39,6 +37,8 @@ ABC_NAMESPACE_IMPL_START #endif +ABC_NAMESPACE_IMPL_START + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index 9c23e0d00..cbaedbe62 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -842,7 +842,7 @@ void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars, int fDumpCnf ) if ( pPars->pre ) { S.eliminate(true); - printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses ); + printf( "c Simplification removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); if ( fDumpCnf ) @@ -1510,7 +1510,7 @@ int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars) if (pPars->pre) { S.eliminate(true); - printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses ); + printf( "c Simplification removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp index 99ca112ae..0e4871187 100644 --- a/src/sat/glucose2/AbcGlucose2.cpp +++ b/src/sat/glucose2/AbcGlucose2.cpp @@ -869,7 +869,7 @@ void Glucose2_SolveCnf( char * pFileName, Glucose2_Pars * pPars ) if ( pPars->pre ) { S.eliminate(true); - printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses ); + printf( "c Simplification removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } @@ -1528,7 +1528,7 @@ int Glucose2_SolveAig(Gia_Man_t * p, Glucose2_Pars * pPars) if (pPars->pre) { S.eliminate(true); - printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses ); + printf( "c Simplification removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); }